fmod CONSTRAINTS is

including NATUTIL .
including PROC .
including MODE .
including CONF .
including CMESSAGE .
including STATE .

var nat nat' : Nat .
var time : Nat .
var dseq seq' seq'' : Nat .
var dseqs seqs : NatSet .
var src dest : Proc .
var ackedseq seq : Nat .
var index newindex oldindex oldindex' transindex : Nat .
var proc proc' : Proc .
var procset procset' : ProcSet .
var destset destset' : ProcSet .
var everybody : ProcSet .
var members members' newmembers transmembers transmembers' : ProcSet .
var oldmembers oldmembers' : ProcSet .
var othernewmembers : ProcSet .
var mode : Mode .
var conf conf' oldconf newconf transconf regconf : Conf .
var localmsgs knownmsgs natmodeset : NatSet .
var message : Message .
var received : MessageSet .
var delivered : MessageList .
var messageset : MessageSet .
var sender : Proc .

sort Constraint .
op constraint : Proc Nat Nat -> Constraint .

var constraint constraint' : Constraint .

----------------------------

sort ConstraintSet .
op sConstraintSet : Constraint -> ConstraintSet .
op eConstraintSet : -> ConstraintSet .
op __ : ConstraintSet ConstraintSet -> ConstraintSet [assoc comm id: eConstraintSet] .

var constraintset constraintset' : ConstraintSet .
var constraints : ConstraintSet .

eq sConstraintSet(constraint) sConstraintSet(constraint) = sConstraintSet(constraint) .

op contains : ConstraintSet Constraint -> Bool .
eq contains(eConstraintSet, constraint') = false .
eq contains((sConstraintSet(constraint) constraintset), constraint') = 
     (constraint' == constraint) or contains(constraintset, constraint') .

op add : ConstraintSet Constraint -> ConstraintSet .
eq add(constraintset,constraint) = (constraintset sConstraintSet(constraint)) .

op  add' : ConstraintSet Constraint -> ConstraintSet .
ceq add'(constraintset,constraint) = constraintset 
    if contains(constraintset, constraint) .
ceq add'(constraintset,constraint) = (constraintset sConstraintSet(constraint)) 
    if not(contains(constraintset, constraint)) .

op  rm : ConstraintSet Constraint -> ConstraintSet .
eq  rm(eConstraintSet,constraint) = eConstraintSet .
ceq rm((sConstraintSet(constraint) constraintset),constraint') = rm(constraintset,constraint')
    if (constraint' == constraint) .
ceq rm((sConstraintSet(constraint) constraintset),constraint') = (sConstraintSet(constraint) rm(constraintset,constraint'))
    if (constraint' =/= constraint) .

op subset : ConstraintSet ConstraintSet -> Bool .
eq subset(eConstraintSet,constraintset') = true .
eq subset((sConstraintSet(constraint) constraintset), constraintset') = 
    contains(constraintset',constraint) and subset(constraintset,constraintset') .

op  mkConstraintSet : Proc NatSet Nat -> ConstraintSet .
eq  mkConstraintSet(proc,eNatSet,nat') = eConstraintSet .
eq  mkConstraintSet(proc,sNatSet(nat) natmodeset, nat') =
    sConstraintSet(constraint(proc,nat,nat')) mkConstraintSet(proc,natmodeset,nat') .

----------------------------

sort Event .
op event : Proc Nat -> Event .

var event event' : Event .

----------------------------

sort EventList .
op sEventList : Event -> EventList .
op eEventList : -> EventList .
op __ : EventList EventList -> EventList [assoc id: eEventList] .

var eventlist eventlist' : EventList .

op contains : EventList Event -> Bool .
eq contains(eEventList, event') = false .
eq contains((sEventList(event) eventlist), event') = 
     (event' == event) or contains(eventlist, event') .

op add : EventList Event -> EventList .
eq add(eventlist,event) = (eventlist sEventList(event)) .

op  add' : EventList Event -> EventList .
ceq add'(eventlist,event) = eventlist 
    if contains(eventlist, event) .
ceq add'(eventlist,event) = (eventlist sEventList(event)) 
    if not(contains(eventlist, event)) .

op  rm : EventList Event -> EventList .
eq  rm(eEventList,event) = eEventList .
ceq rm((sEventList(event) eventlist),event') = rm(eventlist,event')
    if (event' == event) .
ceq rm((sEventList(event) eventlist),event') = (sEventList(event) rm(eventlist,event'))
    if (event' =/= event) .

op subset : EventList EventList -> Bool .
eq subset(eEventList,eventlist') = true .
eq subset((sEventList(event) eventlist), eventlist') = 
    contains(eventlist',event) and subset(eventlist,eventlist') .

var events events' : EventList .

op  seq : Event -> Nat .
eq  seq(event(proc,seq)) = seq .

op  seqs : EventList -> NatSet .
eq  seqs(eEventList) = eNatSet .
eq  seqs(sEventList(event) events) = (sNatSet(seq(event)) seqs(events)) .

op  preset : EventList Nat -> NatSet .
eq  preset(eEventList,seq) = eNatSet .
ceq preset((sEventList(event) events'),seq) = sNatSet(seq(event)) preset(events',seq)
    if seq(event) =/= seq .
ceq preset((sEventList(event) events'),seq) = eNatSet
    if seq(event) == seq .

op  restrict : EventList ProcSet -> EventList .
eq  restrict(eEventList,procset) = eEventList .
ceq restrict(sEventList(event(proc,seq)) events, procset) =
    (sEventList(event(proc,seq)) restrict(events,procset))
    if contains(procset,proc) .
ceq restrict(sEventList(event(proc,seq)) events, procset) =
    restrict(events,procset)
    if not(contains(procset,proc)) .

------------------------

--- causal delivery constraints are updated at sending time 

op  addConstraints : ConstraintSet Proc NatSet NatSet Nat Mode -> ConstraintSet .
ceq addConstraints(constraints,sender,localmsgs,knownmsgs,seq,mode) = constraints 
    if not(fifo(mode)) and not(causal(mode)) . 
    --- redundant, because fifo implies causal in Spread
ceq addConstraints(constraints,sender,localmsgs,knownmsgs,seq,mode) = 
    (constraints mkConstraintSet(sender,localmsgs,seq)) 
    if fifo(mode) and not(causal(mode)) .
ceq addConstraints(constraints,sender,localmsgs,knownmsgs,seq,mode) = 
    (constraints mkConstraintSet(sender,knownmsgs,seq)) 
    if causal(mode) .

--- auxiliary functions for delivery of messages

--- notion of pastcone w.r.t. a causal order

op  impastcone : ConstraintSet Nat -> NatSet .
eq  impastcone(eConstraintSet,seq'') = eNatSet .
ceq impastcone((sConstraintSet(constraint(proc,seq,seq')) constraints),seq'') = 
    sNatSet(seq) impastcone(constraints,seq'') 
    if seq' == seq'' .
ceq impastcone((sConstraintSet(constraint(proc,seq,seq')) constraints),seq'') = 
    impastcone(constraints,seq'')
    if seq' =/= seq'' .

op  impastcone : ConstraintSet NatSet -> NatSet .
eq  impastcone(constraints,eNatSet) = eNatSet . 
eq  impastcone(constraints,(sNatSet(seq) dseqs)) = 
    impastcone(constraints,seq) impastcone(constraints,dseqs) .

op  pastcone : ConstraintSet NatSet -> NatSet .
ceq pastcone(constraints,dseqs) = eNatSet
    if impastcone(constraints,dseqs) == eNatSet .
ceq pastcone(constraints,dseqs) = (impastcone(constraints,dseqs) pastcone(constraints,impastcone(constraints,dseqs)))
    if impastcone(constraints,dseqs) =/= eNatSet .

--- compute sequence numbers of all messages sent by members 
--- (only messages sent with constraints are considered)

op  localseqs : ProcSet ConstraintSet -> NatSet .
eq  localseqs(members, eConstraintSet) = eNatSet .
ceq localseqs(members, sConstraintSet(constraint(sender,seq,seq')) constraints) = 
    sNatSet(seq') localseqs(members, constraints)
    if contains(members, sender) .
ceq localseqs(members, sConstraintSet(constraint(sender,seq,seq')) constraints) = 
    localseqs(members, constraints)
    if not(contains(members, sender)) .

--- checking safisfaction of causality constraints (similar to condition used by Amir)
--- the difference between this and Amir's condition is that
--- - we restrict the pastcone to messages send by members of our current configuration (which could be a transitional one)
--- - the condition takes into account messsages send in any mode

op  co-satisfied : ProcSet ConstraintSet NatSet Nat -> Bool .
eq  co-satisfied(members,constraints,dseqs,seq'') = 
    subset(inter(pastcone(constraints,sNatSet(seq'')), localseqs(members,constraints)), dseqs) .

--- Amir's original condition (too strong for self delivery)
--- op  co-satisfied : ProcSet ConstraintSet NatSet Nat -> Bool .
--- eq  co-satisfied(members,constraints,dseqs,seq'') = 
---     subset(pastcone(constraints,sNatSet(seq'')), dseqs) .

--- The main purpose of the restriction to our configuration is to allow gaps caused by messages
--- send by members (which became disconnected) when we deliver messages in the transitional
--- configuration. This should in particular allow for self delivery, which in the worst case,
--- could happen in a singleton transitional configuration.

--- checking consistency with causality constraints (part of the condition used by Schultz)
--- currently not used, but should be implied

op  co-consistent : ProcSet ConstraintSet NatSet Nat -> Bool .
eq  co-consistent(members,constraints,dseqs,seq'') = 
    not(contains((dseqs pastcone(constraints,dseqs)),seq'')) .

--- checking consistency with total order (trace)
--- not that similar but different from the causal order constraints we restrict the condition
--- to the members of the current configuration (which could be again a transitional one)

op  to-consistent : ProcSet EventList NatSet Nat Mode -> Bool .
ceq to-consistent(members,events,dseqs,seq,mode) = 
    subset(preset(restrict(events,members),seq),dseqs) 
    if agreed(mode) .
ceq to-consistent(members,events,dseqs,seq,mode) = true 
    if not(agreed(mode)) .

--- checking if message can be delivered in principle (i.e. ignoring safe delivery requirement)

op  deliverable : Proc Conf MessageSet MessageList Message ConstraintSet EventList -> Bool .
ceq deliverable(proc,conf,received,delivered,message,constraints,events) =
    conf(message) == reg(conf) and
---    co-consistent(members(conf),constraints,seqs(restrict(delivered,reg(conf))),seq(message)) and --- schultz' condition
    co-satisfied(members(conf),constraints,seqs(restrict(delivered,reg(conf))),seq(message)) and --- amir's condition
    to-consistent(members(conf),events,seqs(restrict(delivered,reg(conf))),seq(message),mode(message))
    if isdata(message) .
ceq deliverable(proc,conf,received,delivered,message,constraints,events) = false
    if not(isdata(message)) .

--- checking safe delivery requirement (i.e. if all 
--- acknowledgements have been received)

op  safe : Proc Conf MessageSet Message ~> Bool .
ceq safe(proc,conf,received,message) = 
    subset(members(conf),srcs(restrict(acks(received,seq(message)),reg(conf)))) 
    if isdata(message) and safe(mode(message)) .
ceq safe(proc,conf,received,message) = true 
    if isdata(message) and not(safe(mode(message))) .

--- checking if message can be delivered (i.e. safe in case of safe messages) .

var trans : Bool .

op  deliverablesafe : Proc Conf MessageSet MessageList Message ConstraintSet EventList Bool -> Bool .
ceq deliverablesafe(proc,conf,received,delivered,message,constraints,events,trans) = 
    trans or safe(proc,conf,received,message) 
    if deliverable(proc,conf,received,delivered,message,constraints,events) .
ceq deliverablesafe(proc,conf,received,delivered,message,constraints,events,trans) = false
    if not(deliverable(proc,conf,received,delivered,message,constraints,events)) .

--- lift the previous predicate to sets (used in change.maude)
op deliverablesafe : Proc Conf MessageSet MessageList MessageSet ConstraintSet EventList Bool -> Bool .
eq deliverablesafe(proc,conf,received,delivered,eMessageSet,constraints,events,trans) = false .
eq deliverablesafe(proc,conf,received,delivered,(sMessageSet(message) messageset),constraints,events,trans) =
   deliverablesafe(proc,conf,received,delivered,message,constraints,events,trans) or
   deliverablesafe(proc,conf,received,delivered,messageset,constraints,events,trans) .

--- delivery of agreed (and safe) messages keeps track delivery history

op  addEvent : EventList Proc Nat Mode -> EventList .
ceq addEvent(events,src,seq,mode) = (events sEventList(event(src,seq))) if agreed(mode) .
ceq addEvent(events,src,seq,mode) = events if not(agreed(mode)) .

--- Note: Total order delivery is guaranteed among agreed (including
--- safe) messages, but not between an agreed message and a
--- causal,fifo, or reliable message (in spite of the fact that Spread
--- implements causal as agreed).  Note that this is different from
--- causal order constraints, where messages or all modes are relevant
--- i.e. a causal message can depend on messages of any other mode.

endfm