问电子2下的动力学模型是如何建立状态的？
EN

Stack Overflow用户

提问于 2020-08-19 08:38:35

回答 1查看 55关注 0票数 0

我从酒店门锁的例子，并提出了这个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

令我惊讶的是，在下面的例子中，有些门是锁着的，有些则没有。我如何确定所有的门在最早的时间都是锁着的条件？

alloy

回答 1

Stack Overflow用户

回答已采纳

发布于 2020-08-19 13:20:16

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

问题在于您将trace定义为谓词。如果将其定义为fact，则将始终应用它。但是，如果您将它作为谓词(我的偏好，因为它感觉不那么全局)，那么必须通过命令将它包含进来。选一个：

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

但是，您的模型仍然不能正常运行。

您提供了一个always，但没有目标。所以在一种状态下合金是快乐的。您应该提供一个satisfied.
You所以合金将尝试继续，直到它是set Door
Your允许车辆无门，我会使用some Door而不是set Door
Your init可以做更清洁的Door.state = Locked
In您的跟踪，每一步设置一个门。但是，您并没有指定其他门的状态。如果不为下一个状态指定值，则它们可以成为任意值。这些应该显式地设置为它们的旧值.

所以我想出了下面的模型：

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)
}

更新的添加了一个不变的谓词。

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/63483149

复制

相似问题

问电子2下的动力学模型是如何建立状态的？
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问电子2下的动力学模型是如何建立状态的？EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问电子2下的动力学模型是如何建立状态的？
EN