合金

Question

中一套的所有子集我正在努力如何定義一個事件可以發佈每個步驟，但多個刪除的狀態更改。我有這樣的模式：

open util/ordering[State] 
sig Event {} 
sig State { 
    queue : set Event 
} 

pred State.post(next' : State, event : Event) { 
    next'.queue = this.queue + event 
} 

pred State.deliver(next' : State) { 
    next'.queue = this.queue - this.queue // STRUGGLE! 
} 

fact traces { 
    no first.queue 
    all s : State - last, next : s.next { 
     some e : Event | s.post[next,e] or s.deliver[next] 
    } 
} 

不過，我想模式，在提供一步，我將其取出即可交付一些事件。在代碼中，我提供了所有的代碼，但是我怎麼編碼纔會真正嘗試this.queue的任何子集？

Answer 1

看來這個鬥爭來自於你試圖將這個謂詞寫成作業的事實。

對問題採用更具說明性的視圖時，解決方案變得清晰。很簡單，就是需要執行新的隊列前面的隊列中的一個子集：

pred State.deliver(next' : State) { 
    next'.queue in this.queue and next'.queue != this.queue 
}