关于ord.als库

Question

如何在合金4中使用ord.als库？

我从这里得到了库：http://stuff.mit.edu/afs/sipb/user/golem/papers/898/ord.als，但是当我尝试使用它时，我会遇到一些新错误。

提前感谢

Answer 1

我不知道ord.als文件是什么，但是您应该使用合金附带的排序库(ordering.als)。要访问该文件：

• 从主菜单中单击File -> Open Sample Models
• 选择util/ordering.als；

要在模型中打开它，只需编写

open util/ordering[S]

sig S {}