如何在 Electrum 2 下的动态模型中建立初始状态？

Question

我借鉴了酒店门锁的例子，想出了这个用于车门的 MWE。

enum LockState {Locked, Unlocked}

sig Door {
    var state: LockState
}

sig Vehicle {
     doors :  disj set Door
}

//actions
pred unlock[d: Door]{
    d.state' = Unlocked
}

pred lock[d: Door]{
    d.state' = Locked
}

//traces
pred init{
    all s: Door.state | s = Locked
}

pred trace{
    init
    always {
        some d: Door | 
            unlock[d] or
            lock[d]
    }
}

//demonstrate
run {} for 4 but exactly 2 Vehicle, 4 Time

令我惊讶的是，下面显示的实例允许，其中一些门是锁着的，一些没有。如何在第一时间建立所有门都被锁上的条件？

Answer 1

初始状态的定义没有任何时间关键字，就像您在 init 中所做的那样。

问题是您将 trace 定义为谓词。如果您将其定义为 fact，它将始终被应用。但是，如果您将其设为谓词（我的偏好，因为它感觉不那么 global），您必须从运行命令中包含它。选择一个：

run trace for 4 but exactly 2 Vehicle, 4 Time
run  { trace } for 4 but exactly 2 Vehicle, 4 Time

但是，您的模型仍然运行不好。

您提供了一个 always 但没有目标。所以在一个状态 Alloy 之后是快乐的。您应该提供一个 eventually，这样 Alloy 将尝试继续，直到满意为止。
你允许没有门的车辆，我会用 some Door 而不是 set Door
你的init可以做得像Door.state = Locked
在您的踪迹中，每个步设置一扇门。但是，您没有指定其他门的状态。如果您不为下一个状态指定值，它们可以变成任何东西。这些应该明确设置为具有它们的旧值。

所以我想出了以下模型：

enum LockState { Locked, Unlocked }
sig Door       { var state: LockState }
sig Vehicle    { doors :  disj some Door }

pred Door.unlock { this.state' = Unlocked }
pred Door.lock   { this.state' = Locked }

pred trace {
    Door.state = Locked
    always (
        some d: Vehicle.doors {
            (d.unlock or d.lock) 
            unchanged[state,d]

        }
    )
    eventually Door.state = Unlocked
}

run trace for 4 but exactly 2 Vehicle


pred unchanged[ r : univ->univ, x : set univ ] {
    (r - x->univ)' = (r - x->univ)
}

已更新 添加了一个未更改的谓词。

如何在 Electrum 2 下的动态模型中建立初始状态？

How are inital states established in dynamic models under Electrum 2?

alloy