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 命令来找到一个有效实例)，Alloy Analyzer 将找到一个模型，其中 s'.currentCall 的值对于某些(任意)h 等于 h.from 来自 s.start:

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

run p

我希望这是你想要实现的。