CODEWITHSUNDEEP
alloy
Peter Kriens
Peter Kriens

Reputation: 15372

All subsets of a set in Alloy

I am am struggling how to define a state change where one event can be posted per step but multiple removed. I have this model:

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

However, I want to model that in the deliver step I deliver some events by removing them. In the code I deliver all but how do I code it that it will actually try any subset of this.queue?

Upvotes: 0

Views: 180

Answers (1)

Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

It seems the struggle come from the fact you try to write this predicate as an assignment.

The solution becomes clear when adopting a more declarative view on the problem. It is simply needed to enforce that the new queue be a proper subset of the previous queue: 

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

Upvotes: 1

Related Questions