如何在 Alloy 中创建静态模型？

Question

我有两个"Systems"，分别表示System1和System2。 我希望每个系统都有一个来自有限数量状态的状态（准确地说是 On 或 Off） 我还希望 System1 能够将 System2 的状态从 On 更改为 Off。 我很难理解我应该在哪里使用谓词、函数，以及我应该为字段分配什么？我已经找到了动态模型的资料，但我不想介绍时间。 我如何建模 System1 可以切换 System2 的状态？

非常感谢

abstract sig System{ state: states}
one sig System1 extends System{
switch: System2 -> states
}
one sig System2 extends System{}
abstract sig states{}
one sig On,Off extends states{}

run{}

Answer 1

如果您想对 System2（例如）具有变化状态的想法进行建模，这意味着您将需要以某种方式在不同时间表示不同状态。所以一些时间或状态的概念是不可避免的。