合金

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 
}