Alloy5中的默认运行命令: Alloy4中的等效值是什么？

Question

我正在做一个项目考试，当我切换到Alloy5时，我很难理解什么是Alloy4中的默认运行命令。

正如大家所看到的，如果我用Alloy5编写了一个模型，而不是一个命令(没有检查没有运行)，如果我单击'Execute'，它执行以下命令：“Rundefaultfor4，但4int，4seqExpect 1”，这满足了我的项目的任务:检查所描述的模型是否有实例。不需要检查财产或其他东西。如果有实例的话。

在Alloy4中，如果我单击'Execute'，它会告诉我“没有定义的命令”，因此没有预定义的run命令。

我的问题是:在Alloy4中，什么等同于Allloy5-默认运行命令？

我要发疯了，因为我必须使用Java(在Alloy4上)，并且无法解决这个问题(因为如果我不在模型中添加一个命令，isSolvable()就不能工作)。

Answer 1

下列措施应能发挥作用：

 run {} for 4