Alloy可以生成无约束关系的实例吗?

Question

下面的模型包含一个"run"命令，该命令指示Alloy Analyzer生成关系to.address的实例，其中关系被约束为一个元组。

sig Message {
    to: Name
}
sig Name {
    address: Address
}
sig Address {}  
run {one to.address}

但是我不想约束to.address关系。我想简单地这样写:

run {to.address}

Alloy Analyzer，生成关系to.address的实例

执行该运行命令会导致以下错误消息:{to.address} must be a formula.

是否有一种方法可以指示Alloy Analyzer生成关系to.address的实例而不指定关系上的约束?如果不是，为什么不呢?

Answer 1

我想你误解了可视化器的作用。每次执行Alloy都会生成一个绑定所有关系的实例。run命令体是一个约束，用于确定哪些实例是有效的;它对显示哪些关系没有影响。为了完成您想做的事情，您可以编写一个约束来命名关系(例如使用存在量词)。或者，如果您想查看特定表达式的值，您可以将其输入到求值器中。