在合金中建模序列

Question

Alloy 有能力为序列建模吗？我可以手动完成（即创建一个succeeds 关系，并列出所有适用的one X），但想象一下还有一种更优雅的方法。

Answer 1

Alloy 有能力为序列建模吗？

是的。

我可以手动完成（即创建一个成功的关系，并列出它适用的所有 X），

是的，在某些情况下，这就是您想要的方式。

但想象一下还有一种更优雅的方法。

正如三十二号上校已经指出的那样，util/ordering 可以提供帮助，util/seqrel 和 util/sequence 也可以。

但在合金 4 中，最简单的序列路径是 seq 关键字记录在 on the Alloy website。我相信它是在第二版软件抽象出版之后引入的；至少，seq 没有索引条目。