一句话：提出输出导向调试工作流：用户通过编辑模型查找器生成的场景而非形式约束来调试模型。
有限模型查找器允许用户用数学逻辑刻画系统属性，并自动求解出满足这些属性的具体实例，即场景（scenario）。这些场景通常被视为模型查找器的核心价值，因为它为开发者提供了探索模型的交互环境。然而实践中用户从场景中获得的收益低于预期。基于近期针对 Alloy（一种以有限模型查找器为后端的建模语言）的用户研究，作者认为症结在于场景与逻辑约束之间距离过远，用户难以借助场景迭代地构建和修正模型。为此，本文提出一种输出导向调试（output directed debugging）工作流的愿景：当模型存在缺陷时，用户直接编辑生成的场景，而不是去编辑形式化约束，从而让调试过程更贴近具体的输出实例。本文属于立场与愿景性工作，基于已有用户研究提出动机与设想，尚未给出实现与实证评估。
Finite model finders give users the ability to specify properties of a system in mathematical logic and then automatically find concrete examples, called scenarios, that satisfy the properties. These scenarios are often viewed as a key benefit of model finders, as they create an exploratory environment for developers to engage with their model. In practice, users find less benefit from these scenarios than expected. Based on a recent user study on Alloy, a modeling language backed by a finite model finder, we believe that the issue is that scenarios are too removed from the logical constraints for users to properly leverage them to iteratively build their model. Therefore, in this paper, we outline a vision for an output directed debugging workflow, in which the user debugs a faulty model by editing the scenario rather than editing the formal constraints.