合金内のイベントのモデル化シーケンス

Question

次のモデルは、あらかじめ定義された特定の順序のアクションのシーケンスを表します。

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 

実行すると、最後のキューイングアクションはOKになりますが、以前は何らかのアクションが失敗したシーケンスがあります。しかし、私はインスタンスを取得しません。 誰かが私に何かしら説明してくれるのですか？

よろしくお願いします。

Answer 1

問題は、特定の時点で、ある時点で、Nokの状態を持つと、後で別の状態に戻すことができないという事実に由来します。 QueueおよびReply述部）。

最後のTimeでは、すべてのアクションがOkの状態にあり、特定の時点でアクションがNokの状態にあるインスタンスは検出されません。 （これはあなたの実行コマンドであなたが要求するものです）

希望します。