以下模型包含"run"命令，该命令指示Alloy Analyzer生成关系 to.address 的实例，其中关系仅限于一个元组 .
sig Message {
to: Name
}
sig Name {
address: Address
}
sig Address {}
run {one to.address}
但我不想限制 to.address 关系 . 我想简单地写一下：
run {to.address}
嘿合金分析仪，生成关系的实例 to.address
执行该运行命令会导致此错误消息： {to.address} must be a formula.
有没有办法指示Alloy Analyzer生成关系 to.address 的实例而不指定关系的约束？如果没有，为什么不呢？
1 回答
我认为你误解了可视化工具的作用 . Alloy的每次执行都会生成一个绑定所有关系的实例 . run命令的主体是一个约束，用于确定哪些实例有效;它对显示哪种关系没有影响 . 要做你想做的事，你可以写一个命名关系的约束（例如用一个存在量词） . 或者，如果要查看特定表达式的值，只需将其键入到赋值器中即可 .