logic - 合金约束规范

Question

我在 Alloy 中编写了以下代码块：

one h: Human | h in s.start => {
    s'.currentCall = h.from
}

我想从一组人（s.start）中选择一个“人”并设置一个等于h.from的变量（s'.currentCall）。但是我认为这段代码是在说：s.start 中只有一个人，其中

s'.currentCall = h.from

是真的。我的假设正确吗？我应该如何解决这个问题？

Answer 1

你是绝对正确的，one量词的意思是在给定的域（集合）中只有一个元素使得量词体成立。

关于您从集合中选择一个元素并将其字段值设置为某个值的最初目标：这听起来像是一个命令式更新，您不能直接在 Alloy 中真正做到这一点；Alloy 是完全声明性的，因此您只能断言关于有界语域的集合和关系的逻辑语句。

如果您只是更改one为some并将含义更改为合取，然后运行分析（run查找有效实例的简单命令），合金分析器将找到一个模型，其中值s'.currentCall等于h.from某些（任意）h来自s.start：

pred p[s, s': S] {
  some h: s.start | s'.currentCall = h.from
}

run p

我希望这是您想要实现的目标。