如何在同一 Alloy 执行中进行检查和 运行？
How do I do a check and run in the same Alloy execution?
我正在学习 Alloy，可以单独使用 check 和 run。但是，当我同时拥有它们时，check 似乎被忽略了。如何同时执行 check 和 run?
扩展问题：
- 如果我有
run，我还需要 check 吗？它不会自动检查我所有的断言吗？还是 check 的目标不仅是检查断言，而且是有意且详尽地（在范围内）搜索反例？
- 难道
run的目标只是为了找到满足谓词的实例吗？还是 运行 的另一种用法？
- 也许
check 应该是 search-counterexample 而 run 应该是 search-example?
- Alloy是否仅限于一次搜索（
check或run）执行？如果是这样，最好的做法是简单地注释掉除一个 check/run 之外的所有内容，然后一次取消注释一个吗？
How do I execute both the check and the run?
你不知道。你一次做一个。
给定两个谓词 P1 和 P2，总是可以定义一个新的谓词以根据需要组合它们（使用 and、or、and not、=>、等等，等等），这样做有时会很有帮助。
给定一个谓词 P 和一个断言 A，但是，可能没有您想象的那么需要同时检查它们。如果断言 A 在给定范围内成立，那么无论谓词 P 是否满足，它都成立。如果它始终在该范围内成立，那么在查找 P 的实例时，除了 P 之外，您不需要检查它。（无论您是否检查它都会保持。）
- If I have a run, do I even need a check? Won't it automatically check all my assertions? Or is the goal of the check not only to check the assertions, but to intentionally and exhaustively (within the scope) search for a counterexample?
只有当您要求分析器检查断言时，断言才会被检查。分析器通过查找反例来精确（且仅）检查断言。
在这一点上，断言不同于 Alloy 事实，后者根据定义（或：根据法令）始终为真，无需检查。 （不仅如此：它们不能被检查：因为反例是不可能的，分析器没有什么可寻找的，也没有动词可以用来请求分析器查找它。）
事实和断言的区别值得思考。
事实表达了对模型的约束；断言没有。非正式地，断言可以被认为是一个建议（或声明），即给定的约束 已经 强加于模型，它从逻辑上遵循已经说过的内容。陈述显而易见的断言是有用的，因为检查它们可以将我们的注意力吸引到那些显而易见的事情实际上并非如此的情况。陈述模型约束的非明显后果的断言也很有用，以不同的方式，将我们作为读者的注意力吸引到我们可能忽略的后果上。
事实也很有用，作为将模型限制在我们感兴趣的情况下的简单方法。但由于事实总是正确的，无论是否与其他约束无关，事实让我们感到惊讶的机会更少。 （与事实相关的最常见的惊喜是令人不快的发现，即我对事实的表述使得无法找到模型的任何实例。随着时间的推移，我开始尽可能避免使用事实：任何我想写的东西事实上，我最终重写为谓词。）
- Is the goal of run only to find an instance that meets the predicate? Or is there another usage of run?
这是 Alloy 的这个用户唯一知道的。
- Perhaps check should be search-counterexample and run should be search-example?
你可能有一点； find-example 和 find-counterexample 对于新用户来说可能更清楚。 （我不喜欢这里的 search，至少在没有 -for 的情况下不会。）但是一些用户的手指可能会反对用二十一个字符替换像 check 这样的五个字符的命令-等效字符。
- Is Alloy limited to one search (check or run) for execution? If so, is the best practice to simply comment out all but one check/run, and uncomment out one at a time?
没有必要；执行菜单让您选择要执行的命令。
我正在学习 Alloy，可以单独使用 check 和 run。但是，当我同时拥有它们时，check 似乎被忽略了。如何同时执行 check 和 run?
扩展问题：
- 如果我有
run，我还需要check吗？它不会自动检查我所有的断言吗？还是check的目标不仅是检查断言，而且是有意且详尽地（在范围内）搜索反例？ - 难道
run的目标只是为了找到满足谓词的实例吗？还是 运行 的另一种用法？ - 也许
check应该是search-counterexample而run应该是search-example? - Alloy是否仅限于一次搜索（
check或run）执行？如果是这样，最好的做法是简单地注释掉除一个 check/run 之外的所有内容，然后一次取消注释一个吗？
How do I execute both the check and the run?
你不知道。你一次做一个。
给定两个谓词 P1 和 P2，总是可以定义一个新的谓词以根据需要组合它们（使用 and、or、and not、=>、等等，等等），这样做有时会很有帮助。
给定一个谓词 P 和一个断言 A，但是，可能没有您想象的那么需要同时检查它们。如果断言 A 在给定范围内成立，那么无论谓词 P 是否满足，它都成立。如果它始终在该范围内成立，那么在查找 P 的实例时，除了 P 之外，您不需要检查它。（无论您是否检查它都会保持。）
- If I have a run, do I even need a check? Won't it automatically check all my assertions? Or is the goal of the check not only to check the assertions, but to intentionally and exhaustively (within the scope) search for a counterexample?
只有当您要求分析器检查断言时，断言才会被检查。分析器通过查找反例来精确（且仅）检查断言。
在这一点上，断言不同于 Alloy 事实，后者根据定义（或：根据法令）始终为真，无需检查。 （不仅如此：它们不能被检查：因为反例是不可能的，分析器没有什么可寻找的，也没有动词可以用来请求分析器查找它。）
事实和断言的区别值得思考。
事实表达了对模型的约束；断言没有。非正式地，断言可以被认为是一个建议（或声明），即给定的约束 已经 强加于模型，它从逻辑上遵循已经说过的内容。陈述显而易见的断言是有用的，因为检查它们可以将我们的注意力吸引到那些显而易见的事情实际上并非如此的情况。陈述模型约束的非明显后果的断言也很有用，以不同的方式，将我们作为读者的注意力吸引到我们可能忽略的后果上。
事实也很有用，作为将模型限制在我们感兴趣的情况下的简单方法。但由于事实总是正确的，无论是否与其他约束无关，事实让我们感到惊讶的机会更少。 （与事实相关的最常见的惊喜是令人不快的发现，即我对事实的表述使得无法找到模型的任何实例。随着时间的推移，我开始尽可能避免使用事实：任何我想写的东西事实上，我最终重写为谓词。）
- Is the goal of run only to find an instance that meets the predicate? Or is there another usage of run?
这是 Alloy 的这个用户唯一知道的。
- Perhaps check should be search-counterexample and run should be search-example?
你可能有一点； find-example 和 find-counterexample 对于新用户来说可能更清楚。 （我不喜欢这里的 search，至少在没有 -for 的情况下不会。）但是一些用户的手指可能会反对用二十一个字符替换像 check 这样的五个字符的命令-等效字符。
- Is Alloy limited to one search (check or run) for execution? If so, is the best practice to simply comment out all but one check/run, and uncomment out one at a time?
没有必要；执行菜单让您选择要执行的命令。