mod CCHANGE is

protecting BOOL .
protecting STRING .
protecting NATUTIL .

including CCOMMON .

var dseq seq' seq'' : Nat .
var index newindex oldindex oldindex' transindex : Nat .
var nat nat' : Nat .
var natlist natlist' : NatList .
var natset natset' : NatSet .
var localmsgs : NatSet .
var dseqs seqs : NatSet .
var proc proc' : Proc .
var member : 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 comp : ProcSet .
var comps : ProcSetSet .
var conf conf' oldconf newconf transconf regconf : Conf .
var mode : Mode .
var data : Data .
var message message'  : Message .
var src dest : Proc .
var knownmsgs : NatSet .
var ackedseq seq : Nat .
var transset : ProcSet .
var ackflag : Bool .
var messagelist messagelist' : MessageList .
var received : MessageSet .
var acked : MessageSet .
var delivered alldelivered : MessageList .
var messageset messageset' : MessageSet .
var recovered : MessageSet .
var constraint constraint' : Constraint .
var constraintset constraintset' : ConstraintSet .
var constraints : ConstraintSet .
var event event' : Event .
var eventlist eventlist' : EventList .
var events events' : EventList .
var reachable : ProcSet .
var success : Bool .
var broadcastset : BroadcastSet .

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

--- CHANGE is used to notify processors of configuration change

--- physical connectivity change signal

rl  reachable(proc,reachable)
    ENABLED(CHANGE(proc,newmembers)) =>
    reachable(proc,newmembers)
    PERFORMED(CHANGE(proc,newmembers)) .

--- processor failure (special kind of CHANGE)

rl  operational(proc)
    reachable(proc,reachable)
    received(proc,received)
    acked(proc,acked)
    delivered(proc,delivered)
    ENABLED(FAIL(proc)) =>
    failed(proc)
    reachable(proc,eProcSet)
    received(proc,eMessageSet)
    acked(proc,eMessageSet)
    delivered(proc,eMessageList)
    PERFORMED(FAIL(proc)) .

--- failure during evs algorithm is modelled differently by flag sucess = false,
--- not clear if a uniform notion of failure would be better

--- connectivity change triggering the evs algorithm
--- (an underlying connectivity monitoring algorithm 
--- could generate this signal)

--- success flag: set to false to model crash during evs algorithm
--- a process that fails will not participate actively in the evs algorithm
--- in particular,
--- it will not send any recovery messages to other processes
--- it will not receive any recovery messages

crl ENABLED(EVS-START(proc,success))
    operational(proc)
    reachable(proc,reachable)
    localconf(proc,conf) 
    sent(proc, broadcastset) =>
    PERFORMED(EVS-START(proc,success))
    evs-start(proc,reachable,success)
    reachable(proc,reachable)
    localconf(proc,conf)
    sent(proc, broadcastset)
    if no-self-messages(proc,broadcastset) .

--- The last condition ensures that local messages are
--- not sitting in the buffer anymore, which implies
--- that they must have been received (because they 
--- cannot get lost).

op  no-self-messages : Proc BroadcastSet -> Bool .
eq  no-self-messages(proc, eBroadcastSet) = true .
eq  no-self-messages(proc, sBroadcastSet(broadcast(sProcSet(proc),message)) broadcastset) = false .
ceq no-self-messages(proc, sBroadcastSet(broadcast(sProcSet(proc'),message)) broadcastset) =
    no-self-messages(proc, broadcastset) if proc =/= proc' .

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

--- evs-start,evs-start',evs-start'',evs-start''':
--- synchronization phase: all new members agree on
--- the set of new members

op  evs-req : Proc ProcSet ProcSet -> State .
op  evs-rep : ProcSet Proc -> State .


rl  evs-start(proc,newmembers,success) =>
    evs-start'(proc,newmembers,newmembers,success)
    evs-req(proc,newmembers,newmembers) .

crl evs-req(proc, (members members'), newmembers) =>
    evs-req(proc, members, newmembers)
    evs-req(proc, members', newmembers)
    if members =/= eProcSet and members' =/= eProcSet .

rl  evs-start'(proc,newmembers,eProcSet,success) =>
    eState . 
crl evs-start'(proc,newmembers,(procset procset'),success) =>
    evs-start'(proc,newmembers,procset,success)
    evs-start'(proc,newmembers,procset',success)
    if procset =/= eProcSet and procset' =/= eProcSet .

rl  evs-start'(proc,newmembers,sProcSet(proc'),success)
    evs-req(proc', sProcSet(proc), newmembers) =>
    evs-start''(proc,newmembers,sProcSet(proc'),success)
    evs-rep(sProcSet(proc), proc') .

rl  evs-rep(members, proc)
    evs-rep(members', proc) =>
    evs-rep(members members', proc) .

rl  evs-start''(proc,newmembers,procset,success)
    evs-start''(proc,newmembers,procset',success) =>
    evs-start''(proc,newmembers,(procset procset'),success) .

rl  evs-start''(proc,newmembers,newmembers,success)
    evs-rep(newmembers,proc) =>
    evs-start'''(proc,newmembers,success) .

--- wake up other processes involved in new configuration:
				   
rl  ENABLED(EVS-START'(proc,success))
    operational(proc)
    evs-req(proc', sProcSet(proc), newmembers) =>
    PERFORMED(EVS-START'(proc,success))
    evs-start'(proc,newmembers,newmembers,success)
    evs-req(proc,newmembers,newmembers) 
    evs-req(proc', sProcSet(proc), newmembers) .
    
---------------------------------

--- evs-start,evs-collect,evs-collect':
--- collecting info about previous configurations from all members of
--- the new configuration, and determining the transitional set, i.e.
--- members which came with me in the new configuration

op  trans-req : Proc ProcSet Conf -> State .
op  trans-rep : ProcSet Proc ProcSet MessageSet -> State .

rl  localconf(proc,oldconf)
    evs-start'''(proc,newmembers,success) =>
    localconf(proc,oldconf)
    evs-collect(proc,newmembers,newmembers,success)
    trans-req(proc,newmembers,oldconf) .

rl  evs-collect(proc,newmembers,eProcSet,success) =>
    eState . 
crl evs-collect(proc,newmembers,(procset procset'),success) =>
    evs-collect(proc,newmembers,procset,success)
    evs-collect(proc,newmembers,procset',success)
    if procset =/= eProcSet and procset' =/= eProcSet .

crl trans-req(proc, members members', oldconf) =>
    trans-req(proc, members, oldconf)
    trans-req(proc, members', oldconf)
    if members =/= eProcSet and members' =/= eProcSet .

--- the following rules does not model the case of partial recovery,
--- i.e. some messages get exchanged and the evs algorithm fails

rl  evs-collect(proc,newmembers,sProcSet(proc'),success)
    trans-req(proc', sProcSet(proc), conf')
    localconf(proc,conf)
    received(proc,received)
    alldelivered(proc, alldelivered) =>
    evs-collect'(proc,newmembers,sProcSet(proc'),success)
    trans-rep(sProcSet(proc), proc', 
      (if conf == conf' then sProcSet(proc) else eProcSet fi), 
      (if success then (received data(alldelivered)) else eMessageSet fi))
    localconf(proc,conf)
    received(proc,received) 
    alldelivered(proc, alldelivered) .

rl  trans-rep(members, proc, transmembers, messageset) 
    trans-rep(members', proc, transmembers', messageset') =>
    trans-rep(members members', proc, union(transmembers,transmembers'), union(messageset,messageset')) .

rl  evs-collect'(proc,newmembers,procset,success)
    evs-collect'(proc,newmembers,procset',success) =>
    evs-collect'(proc,newmembers,(procset procset'),success) .

crl localconf(proc,oldconf)
    evs-collect'(proc,newmembers,newmembers,success)
    received(proc, received)
    alldelivered(proc, alldelivered)
    trans-rep(newmembers,proc,transmembers,messageset) =>
    localconf(proc,oldconf)
    received(proc, received recovered)
    alldelivered(proc, alldelivered)
    evs-deliver(proc,newmembers,transmembers,success)
    if recovered := (if success then rm(rm(messageset,data(alldelivered)),received) else eMessageSet fi) .

--- evs-deliver:
--- now deliver all messages that can be delivered in the old regular configuration

crl evs-deliver(proc,newmembers,transmembers,success)
    localconf(proc,conf)
    localmsgs(proc,conf, localmsgs)
    knownmsgs(proc,conf, knownmsgs)
    delivered(proc,delivered)
    alldelivered(proc,alldelivered)
    received(proc,(sMessageSet(message) received))
    causalorder(conf,constraints) 
    totalorder(conf,events) =>
    evs-deliver(proc,newmembers,transmembers,success)
    localconf(proc,conf)
    localmsgs(proc,conf, localmsgs)
    knownmsgs(proc,conf, (knownmsgs knownmsgs(message)) sNatSet(seq(message)))
    received(proc,received)
    delivered(proc,(delivered sMessageList(message)))
    alldelivered(proc,(alldelivered sMessageList(message)))
    causalorder(conf,constraints) 
    totalorder(conf,addEvent(events,src(message),seq(message),mode(message)))
    if success and deliverablesafe(proc,conf,received,alldelivered,message,constraints,events,false) .

crl evs-deliver(proc,newmembers,transmembers,success)
    localconf(proc,conf)
    localmsgs(proc,conf, localmsgs)
    alldelivered(proc,alldelivered)
    received(proc,received)
    causalorder(conf,constraints) 
    totalorder(conf,events) =>
    evs-trans(proc,newmembers,transmembers,success)
    localconf(proc,conf)
    localmsgs(proc,conf, localmsgs)
    alldelivered(proc,alldelivered)
    received(proc,received)
    causalorder(conf,constraints)
    totalorder(conf,events)
    if not(success and deliverablesafe(proc,conf,received,alldelivered,received,constraints,events,false)) .

--- evs-trans, evs-trans':
--- generate and deliver a new transitional configuration shared by all transmembers

op  transconf-req : ProcSet ProcSet Conf -> State .
op  transconf-rep : ProcSet ProcSet Conf -> State .

rl  evs-trans(proc,newmembers,transmembers,success) 
    localconf(proc,conf) =>
    evs-trans'(proc,newmembers,transmembers,success) 
    localconf(proc,conf)
    transconf-req(sProcSet(proc),transmembers,conf) .

rl  transconf-req(procset, transmembers, oldconf) 
    transconf-req(procset', transmembers, oldconf) =>
    transconf-req((procset procset'), transmembers, oldconf) .

crl transconf-req(transmembers, transmembers, oldconf)
    freshconf(newindex)
    causalorder(oldconf,constraints)
    totalorder(oldconf,events) =>
    transconf-rep(transmembers, transmembers, newconf)
    freshconf(s newindex)
    causalorder(oldconf,constraints)
    totalorder(oldconf,events)
    causalorder(newconf,constraints)
    totalorder(newconf,events)
    if newconf := transconf(transmembers,newindex,oldconf) .

crl transconf-rep(transmembers, procset procset', conf) =>
    transconf-rep(transmembers, procset, conf)
    transconf-rep(transmembers, procset', conf)
    if procset =/= eProcSet and procset' =/= eProcSet .

crl localconf(proc,regconf(members,index))
    evs-trans'(proc,newmembers,transmembers,success)
    transconf-rep(transmembers,sProcSet(proc),transconf)
    delivered(proc,delivered) 
    alldelivered(proc,alldelivered) =>
    localconf(proc,transconf)
    localmsgs(proc,transconf,eNatSet) 
    knownmsgs(proc,transconf,eNatSet)
    evs-trans-deliver(proc,newmembers,transmembers,success)
    delivered(proc,(delivered sMessageList(transmsg(transconf)))) 
    alldelivered(proc,(alldelivered sMessageList(transmsg(transconf)))) 
    if success == true .

crl localconf(proc,regconf(members,index))
    evs-trans'(proc,newmembers,transmembers,success)
    transconf-rep(transmembers,sProcSet(proc),transconf)
    alldelivered(proc,alldelivered) =>
    localconf(proc,regconf(members,index))
    evs-trans-deliver(proc,newmembers,transmembers,success)
    alldelivered(proc,alldelivered)
    if success == false .

--- evs-trans-deliver:
--- now deliver all messages that can be delivered in the new transitional configuration

crl evs-trans-deliver(proc,newmembers,transmembers,success)
    localconf(proc,conf)
    localmsgs(proc,conf, localmsgs)
    knownmsgs(proc,conf, knownmsgs)
    delivered(proc,delivered)
    alldelivered(proc,alldelivered)
    received(proc,(sMessageSet(message) received))
    causalorder(conf,constraints)
    totalorder(conf,events) =>
    evs-trans-deliver(proc,newmembers,transmembers,success)
    localconf(proc,conf)
    localmsgs(proc,conf, localmsgs)
    knownmsgs(proc,conf, (knownmsgs knownmsgs(message)) sNatSet(seq(message)))
    received(proc,received)
    delivered(proc,(delivered sMessageList(message)))
    alldelivered(proc,(alldelivered sMessageList(message)))
    causalorder(conf,constraints) 
    totalorder(conf,addEvent(events,src(message),seq(message),mode(message)))
    if success and deliverablesafe(proc,conf,received,alldelivered,message,constraints,events,true) .

crl evs-trans-deliver(proc,newmembers,transmembers,success)
    localconf(proc,conf)
    localmsgs(proc,conf, localmsgs)
    alldelivered(proc,alldelivered)
    received(proc,received)
    causalorder(conf,constraints)
    totalorder(conf,events) =>
    evs-reg(proc,newmembers,success)
    localconf(proc,conf)
    localmsgs(proc,conf, localmsgs)
    alldelivered(proc,alldelivered)
    received(proc,received)
    causalorder(conf,constraints) 
    totalorder(conf,events) 
    if not(success and deliverablesafe(proc,conf,received,alldelivered,received,constraints,events,true)) .

--- evs-reg, evs-reg':
--- generate and deliver a new regular configuration shared by all newmembers

op  regconf-req : ProcSet ProcSet -> State .
op  regconf-rep : ProcSet ProcSet Conf -> State .

rl  evs-reg(proc,newmembers,success)
    localconf(proc,transconf) =>
    evs-reg'(proc,newmembers,success)
    localconf(proc,transconf)
    regconf-req(sProcSet(proc),newmembers) .

rl  regconf-req(procset, newmembers) 
    regconf-req(procset', newmembers) =>
    regconf-req((procset procset'), newmembers) .

crl regconf-req(newmembers, newmembers)
    freshconf(newindex) =>
    regconf-rep(newmembers, newmembers, newconf) 
    freshconf(s newindex)
    causalorder(newconf,eConstraintSet)
    totalorder(newconf,eEventList)
    if newconf := regconf(newmembers,newindex) .

crl regconf-rep(newmembers, procset procset', conf) =>
    regconf-rep(newmembers, procset, conf)
    regconf-rep(newmembers, procset', conf)
    if procset =/= eProcSet and procset' =/= eProcSet .

crl localconf(proc,transconf)
    evs-reg'(proc,newmembers,success)
    regconf-rep(newmembers,sProcSet(proc),newconf)
    delivered(proc,delivered)
    alldelivered(proc,alldelivered) =>
    localconf(proc,newconf)
    localmsgs(proc,newconf,eNatSet) 
    knownmsgs(proc,newconf,eNatSet)
    operational(proc)
    delivered(proc,(delivered sMessageList(confmsg(newconf,members(transconf)))))
    alldelivered(proc,(alldelivered sMessageList(confmsg(newconf,members(transconf)))))
    if success == true .

crl localconf(proc,conf)
    evs-reg'(proc,newmembers,success)
    regconf-rep(newmembers,sProcSet(proc),newconf)
    alldelivered(proc,alldelivered) =>
    localconf(proc,conf)
    operational(proc)
    alldelivered(proc,alldelivered)
    if success == false .

--- rule for processor recovery

crl failed(proc)
    reachable(proc,procset)
    received(proc,received)
    acked(proc,acked)
    delivered(proc,delivered)
    alldelivered(proc,alldelivered)
    localconf(proc,conf)
    freshconf(newindex)
    ENABLED(RECOVER(proc)) =>
    operational(proc)
    reachable(proc,sProcSet(proc))
    received(proc,eMessageSet)
    acked(proc,eMessageSet)
    delivered(proc,sMessageList(confmsg(newconf,eProcSet)))
    alldelivered(proc,sMessageList(confmsg(newconf,eProcSet)))
    localconf(proc,newconf)
    localmsgs(proc,newconf,eNatSet) 
    knownmsgs(proc,newconf,eNatSet)
    causalorder(newconf,eConstraintSet)
    totalorder(newconf,eEventList)
    freshconf(s newindex)
    PERFORMED(RECOVER(proc)) 
    if newconf := regconf(sProcSet(proc),newindex) .

--- Note that all messages in alldelivered are deleted because they
--- are used in the evs algorithm to recover lost messages.  This
--- corresponds to the reality that a processor that crashes forgets
--- everything and cannot provide messages for recovery. So
--- alldelivered is not exactly a history variable, as it may seem
--- from the other rules.

endm