合金约束规范

Question

我在Alloy中写了如下代码块：

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

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

s'.currentCall = h.from

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

Answer 1

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

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

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

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

run p

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