fmod MODE is

protecting BOOL .
protecting NAT .

--- modes, i.e. service levels, of regular data messages

sort Mode .  
op reliable : -> Mode .
op fifo : -> Mode .
op causal : -> Mode .
op agreed : -> Mode .
op safe : -> Mode .

var mode mode' : Mode .

op fifo : Mode -> Bool .
eq fifo(reliable) = false .
eq fifo(fifo) = true .
eq fifo(causal) = true .
eq fifo(agreed) = true .
eq fifo(safe) = true .

op causal : Mode -> Bool .
eq causal(reliable) = false .
eq causal(fifo) = false .
eq causal(causal) = true .
eq causal(agreed) = true .
eq causal(safe) = true .

op agreed : Mode -> Bool .
eq agreed(reliable) = false .
eq agreed(fifo) = false .
eq agreed(causal) = false .
eq agreed(agreed) = true .
eq agreed(safe) = true .

op safe : Mode -> Bool .
eq safe(reliable) = false .
eq safe(fifo) = false .
eq safe(causal) = false .
eq safe(agreed) = false .
eq safe(safe) = true .

endfm