我正在进行项目考试,当我切换到Alloy4时,难以理解与Alloy5中的默认Run命令等效。
大家都可以看到,如果我用Alloy5写模型,而不是命令(不检查不运行),如果我单击“执行”,它将执行以下命令:“为4运行默认值,但4 int,4 seq预期为1”哪个满足我的项目任务:检查所描述的模型是否具有实例。无需检查属性或其他内容。只要有实例。
在Alloy4中,如果我单击“执行”,它会告诉我“未定义命令”,因此没有预定义的运行命令。
我的问题是:Alloy4中的Allloy5-Default-Run-Command等效于什么?
我发疯了,因为我必须在Alloy4 API(在Java上)上工作,并且无法弄清楚如何解决此问题(因为如果我不在模型中放置命令,则isSolvable()无法正常工作)。
以下应该起作用:
run {} for 4