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

Question

我有两个“系统”，分别表示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（例如，状态2）具有变化的状态进行建模，那意味着您将需要以某种方式在不同的时间代表不同的状态。因此，不可避免地会有一些时间或状态的概念。