对合金中的事件序列进行建模答案

【问题标题】：Modeling sequence of events in Alloy对合金中的事件序列进行建模
【发布时间】：2017-03-22 11:46:01
【问题描述】：

以下模型表示给定某个预定义顺序的一系列动作。

open util/ordering[Time]

abstract sig Action {pre: set Action}

one sig A, B, C, D extends Action {}

fact{
    pre = A -> B + D -> B + D -> C
}

sig Time { queue: Action -> lone State}

abstract sig State {}
one sig Acted, Ok, Nok extends State{}

pred Queue [t, t': Time] {
   some a: Action-(t.queue).State |
       a.pre in (t.queue).Ok + (t.queue).Nok and t'.queue=t.queue+(a->Acted)
}

pred Reply [t, t': Time] {
   some a: (t.queue).Acted | 
          some s: State-Acted | t'.queue=t.queue++(a->s)
}

fact {
  no first.queue 
  last.queue=Action->Ok or last.queue = Action -> Nok
  all t:Time-last | Queue[t,t.next] or Reply[t,t.next]
}


run {last.queue=Action->Ok and some t:Time-last | t.queue = Action->Nok} for 9

随着运行，我希望有一个序列，其中最后一个排队操作正常，但之前某些操作失败了。但是我没有得到任何实例。谁能解释一下我做错了什么？

问候，安德烈。

【问题讨论】：

标签： alloy

【解决方案1】：

问题来自这样一个事实，即一旦一个动作在给定时间具有Nok 的状态，那么它就不能在将来的时间更改回另一个状态（正如两个量词所建议的那样Queue 和 Reply 谓词）。

因此，分析器无法找到在最终时间中所有动作都处于Ok 状态以及在给定时间动作处于Nok 状态的实例。（这是您在运行命令中要求的）

希望对你有帮助

【讨论】：