sort Bool
func T,F: -> Bool
map  and,or: Bool # Bool -> Bool
     not: Bool -> Bool
     if: Bool # Bool # Bool -> Bool
     eq: Bool # Bool -> Bool
var  b, b': Bool
rew  and(T,T) = T
     and(F,b) = F
     and(b,F) = F
     or(b,T) = T
     or(T,b) = T
     or(F,F) = F
     not(F) = T
     not(T) = F
     if(T,b,b') = b
     if(F,b,b') = b'
     eq(b,b) = T
     eq(T,F) = F
     eq(F,T) = F

sort Nat
func zero:-> Nat
     succ: Nat-> Nat
map  plus: Nat # Nat -> Nat
     monus: Nat # Nat -> Nat
     eq: Nat # Nat -> Bool
var  n,m: Nat
rew  plus(n,zero) = n
     plus(n,succ(m)) = succ(plus(n,m))
     monus(n,zero) = n
     monus(zero,n) = zero
     monus(succ(n),succ(m)) = monus(n,m)
     eq(zero,zero) = T
     eq(zero,succ(n)) = F
     eq(succ(n),zero) = F
     eq(succ(n),succ(m)) = eq(n,m)

sort PId
func p1,p2,p3: -> PId
map  greater: PId # PId -> Bool
     eq: PId # PId -> Bool
var  pid: PId
rew  greater(pid,pid) = F
     greater(p1,p2) = F
     greater(p1,p3) = F
     greater(p2,p1) = T
     greater(p2,p3) = F
     greater(p3,p1) = T
     greater(p3,p2) = T
     eq(pid,pid) = T
     eq(p1,p2) = F
     eq(p1,p3) = F
     eq(p2,p1) = F
     eq(p2,p3) = F
     eq(p3,p1) = F
     eq(p3,p2) = F

sort PIdList
func empty-pid-list: -> PIdList
     in: PId # PIdList -> PIdList
map  add: PId # PIdList -> PIdList
     head: PIdList -> PId
     tail: PIdList -> PIdList
     union: PIdList # PIdList -> PIdList
     empty: PIdList -> Bool
     length: PIdList -> Nat
     element: PId # PIdList -> Bool
     remove: PId # PIdList -> PIdList
     if: Bool # PIdList # PIdList -> PIdList
     eq: PIdList # PIdList -> Bool
var  pid, pid': PId
     pid-list, pid-list': PIdList
rew  add(pid,empty-pid-list) = in(pid,empty-pid-list)
     add(pid,in(pid',pid-list)) =
        if(greater(pid,pid'),in(pid',add(pid,pid-list)),in(pid,in(pid',pid-list)))
     head(in(pid,pid-list)) = pid
     tail(in(pid,pid-list)) = pid-list
     union(empty-pid-list,pid-list) = pid-list
     union(pid-list,empty-pid-list) = pid-list
     union(in(pid,pid-list),in(pid',pid-list')) =
        if(eq(pid,pid'),in(pid,union(pid-list,pid-list')),
	   if(greater(pid,pid'),in(pid',union(in(pid,pid-list),pid-list')),
	      in(pid,union(pid-list,in(pid',pid-list')))))
     empty(empty-pid-list) = T
     empty(in(pid,pid-list)) = F
     length(empty-pid-list) = zero
     length(in(pid,pid-list)) = succ(length(pid-list))
     element(pid,empty-pid-list) = F
     element(pid,in(pid',pid-list)) = or(eq(pid,pid'),element(pid,pid-list))
     remove(pid,in(pid',pid-list)) =
        if(eq(pid,pid'),pid-list,in(pid',remove(pid,pid-list)))
     remove(pid,empty-pid-list) = empty-pid-list
     if(T,pid-list,pid-list') = pid-list
     if(F,pid-list,pid-list') = pid-list'
     eq(empty-pid-list,empty-pid-list) = T
     eq(empty-pid-list,in(pid,pid-list)) = F
     eq(in(pid,pid-list),empty-pid-list) = F
     eq(in(pid,pid-list),in(pid',pid-list')) =
        and(eq(pid,pid'),eq(pid-list,pid-list'))

sort Op
func w1,w2,w3,nop: -> Op
map  eq: Op # Op -> Bool
     if: Bool # Op # Op -> Op
var  op, op': Op
rew  if(T,op,op') = op
     if(F,op,op') = op'
     eq(op,op) = T
     eq(w1,w2) = F
     eq(w1,w3) = F
     eq(w1,nop) = F
     eq(w2,w1) = F
     eq(w2,w3) = F
     eq(w2,nop) = F
     eq(w3,w1) = F
     eq(w3,w2) = F
     eq(w3,nop) = F
     eq(nop,w1) = F
     eq(nop,w2) = F
     eq(nop,w3) = F

sort OpList
func empty-op-list: -> OpList
     in: Op # OpList -> OpList
map  head: OpList -> Op
     tail: OpList -> OpList
     empty: OpList -> Bool
     if: Bool # OpList # OpList -> OpList
     eq: OpList # OpList -> Bool
var  op, op': Op
     op-list, op-list': OpList
rew  head(in(op,op-list)) = op
     tail(in(op,op-list)) = op-list
     empty(empty-op-list) = T
     empty(in(op,op-list)) = F
     if(T,op-list,op-list') = op-list
     if(F,op-list,op-list') = op-list'
     eq(empty-op-list,empty-op-list) = T
     eq(empty-op-list,in(op,op-list)) = F
     eq(in(op,op-list),empty-op-list) = F
     eq(in(op,op-list),in(op',op-list')) = and(eq(op,op'),eq(op-list,op-list'))

sort OpPIdList
func empty-oppid-list: -> OpPIdList
     in: Op # PId # OpPIdList -> OpPIdList
map  add: Op # PId # OpPIdList -> OpPIdList
     union: OpPIdList # OpPIdList -> OpPIdList
     empty: OpPIdList -> Bool
     length: OpPIdList -> Nat
     strip: OpPIdList -> OpList
     extract: PId # OpPIdList -> Op
     arrived: PId # OpPIdList -> Bool
     if: Bool # OpPIdList # OpPIdList -> OpPIdList
     eq: OpPIdList # OpPIdList -> Bool
var  op, op': Op
     pid,pid': PId
     oppid-list, oppid-list': OpPIdList
rew  add(op,pid,empty-oppid-list) = in(op,pid,empty-oppid-list)
     add(op,pid,in(op',pid',oppid-list)) =
        if(greater(pid,pid'),in(op',pid',add(op,pid,oppid-list)),
	   in(op,pid,in(op',pid',oppid-list)))
     union(empty-oppid-list,oppid-list) = oppid-list
     union(oppid-list,empty-oppid-list) = oppid-list
     union(in(op,pid,oppid-list),in(op',pid',oppid-list')) =
        if(eq(pid,pid'),in(op,pid,union(oppid-list,oppid-list')),
	   if(greater(pid,pid'),in(op',pid',union(in(op,pid,oppid-list),oppid-list')),
	      in(op,pid,union(oppid-list,in(op',pid',oppid-list')))))
     empty(empty-oppid-list) = T
     empty(in(op,pid,oppid-list)) = F
     length(empty-oppid-list) = zero
     length(in(op,pid,oppid-list)) = succ(length(oppid-list))
     strip(empty-oppid-list) = empty-op-list
     strip(in(op,pid,oppid-list)) = if(eq(op,nop),strip(oppid-list),in(op,strip(oppid-list)))
     extract(pid,in(op,pid',oppid-list)) = if(eq(pid,pid'),op,extract(pid,oppid-list))
     arrived(pid,empty-oppid-list) = F
     arrived(pid,in(op,pid',oppid-list)) = if(eq(pid,pid'),T,arrived(pid,oppid-list))
     if(T,oppid-list,oppid-list') = oppid-list
     if(F,oppid-list,oppid-list') = oppid-list'
     eq(empty-oppid-list,empty-oppid-list) = T
     eq(empty-oppid-list,in(op,pid,oppid-list)) = F
     eq(in(op,pid,oppid-list),empty-oppid-list) = F
     eq(in(op,pid,oppid-list),in(op',pid',oppid-list')) =
        and(and(eq(op,op'),eq(pid,pid')),eq(oppid-list,oppid-list'))

sort Bit
func 0,1:-> Bit
map  invert: Bit -> Bit
     eq: Bit # Bit -> Bool
var  bit: Bit
rew  eq(bit,bit) = T
     eq(0,1) = F
     eq(1,0) = F
     invert(1) = 0
     invert(0) = 1

sort OpBitPIdListList
func empty-opbitpidlist-list: -> OpBitPIdListList
     in: Op # Bit # PIdList # OpBitPIdListList -> OpBitPIdListList
map  ophead: OpBitPIdListList -> Op
     bithead: OpBitPIdListList -> Bit
     pidlisthead: OpBitPIdListList -> PIdList
     tail: OpBitPIdListList -> OpBitPIdListList
     attach: Op # Bit # PIdList # OpBitPIdListList -> OpBitPIdListList
     empty: OpBitPIdListList -> Bool
     eq: OpBitPIdListList # OpBitPIdListList -> Bool
var  op, op': Op
     bit,bit': Bit
     pid-list,pid-list': PIdList
     opbitpidlist-list, opbitpidlist-list': OpBitPIdListList
rew  ophead(in(op,bit,pid-list,opbitpidlist-list)) = op
     bithead(in(op,bit,pid-list,opbitpidlist-list)) = bit
     pidlisthead(in(op,bit,pid-list,opbitpidlist-list)) = pid-list
     tail(in(op,bit,pid-list,opbitpidlist-list)) = opbitpidlist-list
     attach(op,bit,pid-list,empty-opbitpidlist-list) = in(op,bit,pid-list,empty-opbitpidlist-list)
     attach(op,bit,pid-list,in(op',bit',pid-list',opbitpidlist-list)) = in(op',bit',pid-list',attach(op,bit,pid-list,opbitpidlist-list))
     empty(empty-opbitpidlist-list) = T
     empty(in(op,bit,pid-list,opbitpidlist-list)) = F
     eq(empty-opbitpidlist-list,empty-opbitpidlist-list) = T
     eq(empty-opbitpidlist-list,in(op,bit,pid-list,opbitpidlist-list)) = F
     eq(in(op,bit,pid-list,opbitpidlist-list),empty-opbitpidlist-list) = F
     eq(in(op,bit,pid-list,opbitpidlist-list),in(op',bit',pid-list',opbitpidlist-list')) =
        and(and(and(eq(op,op'),eq(bit,bit')),eq(pid-list,pid-list')),eq(opbitpidlist-list,opbitpidlist-list'))

act  send_w_lock_request, recv_w_lock_request, com_w_lock_request,
     send_w_lock_release, recv_w_lock_release, com_w_lock_release,
     send_notification, recv_notification, com_notification,
     join, crash: PId
     send_crash_lrm2cha, recv_crash_lrm2cha, com_crash_lrm2cha: PId
     send_crash_cha2lrm, recv_crash_cha2lrm, com_crash_cha2lrm: PId # PId
     send_localwrite, recv_localwrite, com_localwrite: PId # Op
     send_remotewrite, recv_remotewrite, com_remotewrite,
     send_lrm2cha, recv_lrm2cha, com_lrm2cha: PId # PId # Op # Bit # PIdList
     send_lrm2cha, recv_lrm2cha, com_lrm2cha: PId # PId # Bit # PIdList # Nat
     send_cha2lrm, recv_cha2lrm, com_cha2lrm: PId # PId # Op # Bit # PIdList
     send_cha2lrm, recv_cha2lrm, com_cha2lrm: PId # PId # Bit # PIdList # Nat
     ask_wolist, give_wolist, com_wolist: PId # PId # Bit # OpPIdList
     send_outbuffer, recv_outbuffer, com_outbuffer: PId # Op # Bit # PIdList # PIdList
     send_outbuffer, recv_outbuffer, com_outbuffer: PId # Bit # PIdList # Nat # PIdList
     send_joinreq, recv_joinreq, com_joinreq: PId # PId
     execute: PId # OpList

comm send_w_lock_request | recv_w_lock_request = com_w_lock_request
     send_w_lock_release | recv_w_lock_release = com_w_lock_release
     send_notification | recv_notification = com_notification
     send_localwrite | recv_localwrite = com_localwrite
     send_outbuffer | recv_outbuffer = com_outbuffer
     send_remotewrite | recv_remotewrite = com_remotewrite
     send_lrm2cha | recv_lrm2cha = com_lrm2cha
     send_cha2lrm | recv_cha2lrm = com_cha2lrm
     send_crash_lrm2cha | recv_crash_lrm2cha = com_crash_lrm2cha
     send_crash_cha2lrm | recv_crash_cha2lrm = com_crash_cha2lrm
     ask_wolist | give_wolist = com_wolist
     send_joinreq | recv_joinreq = com_joinreq


%% A thread gets the WriteLock at its node, sends a local write to LRM, waits
%% for a notification of LRM, and then releases the WriteLock.

proc Thread(pid:PId,prog:OpList) = (send_w_lock_request(pid) <| not(empty(prog)) |> delta).
                                    send_localwrite(pid,head(prog)).recv_notification(pid).
                                    send_w_lock_release(pid).Thread(pid,tail(prog))


%% A node that wants to join, contacts one of the nodes in the world, and then waits for the start
%% of a new round, to join the world.

  Join(pid:PId) = sum(pid':PId,send_joinreq(pid',pid).JoinWait(pid,pid'))


%% The contact node signals to the joining node that a new round has started, and communicates the
%% round number and world in this round.

  JoinWait(pid:PId,pid':PId) = sum(world:PIdList,sum(ts:Bit,sum(crash-nr:Nat,recv_cha2lrm(pid,pid',ts,world,crash-nr).join(pid).
                                   LocalRoundManager(pid,ts,empty-oppid-list,empty-oppid-list,empty-oppid-list,in(pid',remove(pid,world)),crash-nr,empty-pid-list,empty-pid-list,empty-pid-list,empty-pid-list,empty-pid-list,empty-pid-list))))


%% While waiting, the joining node can detect that the contact node has crashed. In that
%% case the joining node also crashes, so that other nodes in the world that already learned
%% of the presence of the joining node, will learn that the joining node is not part of the world.

    + recv_crash_cha2lrm(pid,pid').LRMCrashed(pid)


%% The joining node itself can also crash.

    + crash(pid).LRMCrashed(pid)


%% LRM at local node pid maintains the round number ts, wo-list / nwo-list / cwo-list, the
%% world, the number crash-nr of crashed processes in this round, joinack-list of local joins that
%% can enter the world after the current round, joinreq-list of local joins that can enter the world
%% after the next round, join-list of remote joins that can enter the world after the current round,
%% and next-join-list of remote joins that can enter the world after the next round.
%% The list oldjoinack-list contains the local joins that can be acknowledged in this round, and the
%% list oldworld is maintained to decide when these acknowledgements can be sent (namely when all
%% nodes active in the previous round have either sent a remote write in this round or crashed).

     LocalRoundManager(pid:PId,ts:Bit,wo-list:OpPIdList,nwo-list:OpPIdList,cwo-list:OpPIdList,world:PIdList,crash-nr:Nat,joinack-list:PIdList,joinreq-list:PIdList,join-list:PIdList,next-join-list:PIdList,oldjoinack-list:PIdList,oldworld:PIdList) =


%% LRM receives a local write. If wo-list is empty, it notifies the thread that sent the local
%% write, adds the write operation to wo-list, and communicates the local write to the other nodes
%% in the world (and joinack-list, which in this case is empty), via its OutBuffer.
%% If wo-list is non-empty, LRM adds the local write operation to nwo-list.

      sum(op:Op,recv_localwrite(pid,op).
         (send_notification(pid).send_outbuffer(pid,op,ts,world,empty-pid-list).
            LocalRoundManager(pid,ts,in(op,pid,empty-oppid-list),nwo-list,cwo-list,world,crash-nr,joinack-list,joinreq-list,join-list,next-join-list,oldjoinack-list,oldworld)
      <| empty(wo-list) |>
      LocalRoundManager(pid,ts,wo-list,add(op,pid,nwo-list),cwo-list,world,crash-nr,joinack-list,joinreq-list,join-list,next-join-list,oldjoinack-list,oldworld)))


%% LRM receives a remote write from node pid'. It removes pid' from oldworld. If pid' was the only element
%% of oldworld, and oldjoinack-list is not empty, then pid comunicates via its OutBuffer that all local
%% joins that can join in the current round can be acknowledged.
%% If the round number of the remote write from pid' equals the round number of pid, then pid adds this
%% write to wo-list, and the pid-list of joins attached to the write operation to its join-list. Moreover,
%% if wo-list was empty, it adds a local NOP to wo-list, and communicates this NOP to the other nodes
%% in the world, via its OutBuffer.
%% If the round number of the remote write from pid' is not equal to the round number of pid, then pid adds
%% the write operation to nwo-list, and the pid-list of joins attached to this write to its next-join-list.

    + sum(op:Op,sum(pid':PId,sum(ts':Bit,sum(pid-list:PIdList,(recv_cha2lrm(pid,pid',op,ts',pid-list) <| element(pid',world) |> delta).
         (((send_outbuffer(pid,ts,world,crash-nr,oldjoinack-list).
            ((send_outbuffer(pid,nop,ts,world,empty-pid-list).
               LocalRoundManager(pid,ts,add(nop,pid,in(op,pid',empty-oppid-list)),nwo-list,cwo-list,world,crash-nr,joinack-list,joinreq-list,union(pid-list,join-list),next-join-list,oldjoinack-list,empty-pid-list))
         <| empty(wo-list) |>
         ((LocalRoundManager(pid,ts,add(op,pid',wo-list),nwo-list,cwo-list,world,crash-nr,joinack-list,joinreq-list,union(pid-list,join-list),next-join-list,oldjoinack-list,empty-pid-list))
      <| eq(ts,ts') |>
         LocalRoundManager(pid,ts,wo-list,add(op,pid',nwo-list),cwo-list,world,crash-nr,joinack-list,joinreq-list,join-list,union(pid-list,next-join-list),oldjoinack-list,empty-pid-list))))
      <| and(eq(oldworld,in(pid',empty-pid-list)),not(empty(oldjoinack-list))) |> delta)

      + ((send_outbuffer(pid,nop,ts,world,empty-pid-list).
            LocalRoundManager(pid,ts,add(nop,pid,in(op,pid',empty-oppid-list)),nwo-list,cwo-list,world,crash-nr,joinack-list,joinreq-list,union(pid-list,join-list),next-join-list,oldjoinack-list,remove(pid',oldworld)))
         <| empty(wo-list) |>
         ((LocalRoundManager(pid,ts,add(op,pid',wo-list),nwo-list,cwo-list,world,crash-nr,joinack-list,joinreq-list,union(pid-list,join-list),next-join-list,oldjoinack-list,remove(pid',oldworld)))
      <| eq(ts,ts') |>
         LocalRoundManager(pid,ts,wo-list,add(op,pid',nwo-list),cwo-list,world,crash-nr,joinack-list,joinreq-list,join-list,union(pid-list,next-join-list),oldjoinack-list,remove(pid',oldworld))))
      <| or(not(eq(oldworld,in(pid',empty-pid-list))),empty(oldjoinack-list)) |> delta)))))


%% The failure detector signals that a node pid' in the world has crashed, without sending a write
%% operation in this round. pid' is removed from the world, and crash-nr is increased by one.
%% Moreover, pid' is removed from oldworld. If pid' was the only element of oldworld, and oldjoinack-list
%% is non-empty, then pid communicates via its OutBuffer that all local joins that can join in the current
%% round can be acknowledged.
%% Since failure detection works with time-outs, failures can only be detected if the wo-list is
%% non-empty, as else the node pid is idle in this round.

    + sum(pid':PId,recv_crash_cha2lrm(pid,pid').
         send_outbuffer(pid,ts,remove(pid',world),succ(crash-nr),oldjoinack-list).
            LocalRoundManager(pid,ts,wo-list,nwo-list,cwo-list,remove(pid',world),succ(crash-nr),joinack-list,joinreq-list,join-list,next-join-list,oldjoinack-list,empty-pid-list)
      <| and(and(eq(oldworld,in(pid',empty-pid-list)),not(empty(oldjoinack-list))),and(and(element(pid',world),not(arrived(pid',wo-list))),not(empty(wo-list)))) |> delta)

    + sum(pid':PId,recv_crash_cha2lrm(pid,pid').
         LocalRoundManager(pid,ts,wo-list,nwo-list,cwo-list,remove(pid',world),succ(crash-nr),joinack-list,joinreq-list,join-list,next-join-list,oldjoinack-list,remove(pid',oldworld))
      <| and(or(not(eq(oldworld,in(pid',empty-pid-list))),empty(oldjoinack-list)),and(and(element(pid',world),not(arrived(pid',wo-list))),not(empty(wo-list)))) |> delta)


%% Another node pid' asks for the cwo-list of node pid, to carry out crash recovery.
%% The check whether a local write from the requesting node pid' is present in wo-list
%% makes sure that pid' is referring to the previous (and not the next) round.

    + sum(pid':PId,give_wolist(pid,pid',invert(ts),cwo-list).
         LocalRoundManager(pid,ts,wo-list,nwo-list,cwo-list,world,crash-nr,joinack-list,joinreq-list,join-list,next-join-list,oldjoinack-list,oldworld)
      <| not(arrived(pid',wo-list)) |> delta)


%% A join request from a node pid' arrives. If wo-list is empty, this join request is added to
%% joinack-list (which at this time is empty), a NOP is added as a local write to wo-list,
%% and the join request and the NOP are sent to the other nodes in the world.
%% If wo-list is non-empty, the join request is added to joinreq-list.

    + sum(pid':PId,recv_joinreq(pid,pid').
         (send_outbuffer(pid,nop,ts,world,in(pid',empty-pid-list)).
            LocalRoundManager(pid,ts,in(nop,pid,empty-oppid-list),nwo-list,cwo-list,world,crash-nr,in(pid',empty-pid-list),joinreq-list,join-list,next-join-list,oldjoinack-list,oldworld)
         <| empty(wo-list) |>
            LocalRoundManager(pid,ts,wo-list,nwo-list,cwo-list,world,crash-nr,joinack-list,add(pid',joinreq-list),join-list,next-join-list,oldjoinack-list,oldworld)))


%% Let the length of wo-list be equal to the number of nodes in the world, plus one (to account for
%% the fact that a node excludes itself from its world).
%% If crash-nr is zero, then it executes wo-list, after stripping all node identities and NOPs. It
%% inverts the round number, the wo-list becomes the cwo-list,  the nwo-list becomes the wo-list,
%% joinack-list and join-list are added to the world, the crash-nr becomes zero, and LRM proceeds to
%% the next round.
%% If crash-nr is not zero, then a crash recovery is started, to obtain the wo-lists of the other
%% nodes in the world for this round. The second argument world is to keep track of which nodes still
%% have to be asked for their wo-list, and the bit 0 is set to 1 in case of a crash during crash recovery,
%% to mark that at the end of the crash recovery it has to be repeated.

    + execute(pid,strip(wo-list)).
         NextRound(pid,invert(ts),nwo-list,wo-list,union(union(world,joinack-list),join-list),zero,joinack-list,joinreq-list,next-join-list,world)
      <| and(eq(crash-nr,zero),eq(length(wo-list),succ(length(world)))) |> delta

    + tau.
         CrashRecovery(pid,ts,wo-list,nwo-list,cwo-list,world,world,0,joinack-list,joinreq-list,join-list,next-join-list)
      <| and(not(eq(crash-nr,zero)),eq(length(wo-list),succ(length(world)))) |> delta

%% LRM crashes.

    + crash(pid).LRMCrashed(pid)


%% LRM enters the next round. Its wo-list has become cwo-list, and its nwo-list has become wo-list.

  NextRound(pid:PId,ts:Bit,wo-list:OpPIdList,cwo-list:OpPIdList,world:PIdList,crash-nr:Nat,joinack-list:PIdList,joinreq-list:PIdList,next-join-list:PIdList,oldworld:PIdList) =


%% If pid was the only active process in the previous round (i.e. oldworld is empty) and joinack-list
%% is non-empty, then at the start of the current round, pid immediately sends join acknowledgements,
%% via its OutBuffer, to all nodes in joinack-list.
%% If there is a local write in wo-list at the start of the next round, LRM notifies the thread
%% that sent the local write, and communicates the local write to other nodes in the world, via
%% its OutBuffer. Else, if wo-list is non-empty, a NOP is added as a local write to wo-list, and
%% this NOP is sent to the other nodes in the world.

       (send_outbuffer(pid,ts,world,crash-nr,joinack-list).
          (send_notification(pid).send_outbuffer(pid,extract(pid,wo-list),ts,world,joinreq-list).
             LocalRoundManager(pid,ts,wo-list,empty-oppid-list,cwo-list,world,crash-nr,joinreq-list,empty-pid-list,next-join-list,empty-pid-list,joinack-list,oldworld)
          <| arrived(pid,wo-list) |>
          (LocalRoundManager(pid,ts,wo-list,empty-oppid-list,cwo-list,world,crash-nr,joinreq-list,empty-pid-list,next-join-list,empty-pid-list,joinack-list,oldworld)
             <| and(empty(wo-list),and(empty(joinack-list),empty(joinreq-list))) |>
	        send_outbuffer(pid,nop,ts,world,joinreq-list).
	           LocalRoundManager(pid,ts,add(nop,pid,wo-list),empty-oppid-list,cwo-list,world,crash-nr,joinreq-list,empty-pid-list,next-join-list,empty-pid-list,joinack-list,oldworld))))
       <| and(eq(oldworld,empty-pid-list),not(empty(joinack-list))) |> delta

    +  (send_notification(pid).send_outbuffer(pid,extract(pid,wo-list),ts,world,joinreq-list).
             LocalRoundManager(pid,ts,wo-list,empty-oppid-list,cwo-list,world,crash-nr,joinreq-list,empty-pid-list,next-join-list,empty-pid-list,joinack-list,oldworld)
          <| arrived(pid,wo-list) |>
          (LocalRoundManager(pid,ts,wo-list,empty-oppid-list,cwo-list,world,crash-nr,joinreq-list,empty-pid-list,next-join-list,empty-pid-list,joinack-list,oldworld)
             <| and(empty(wo-list),and(empty(joinack-list),empty(joinreq-list))) |>
                send_outbuffer(pid,nop,ts,world,joinreq-list).
                   LocalRoundManager(pid,ts,add(nop,pid,wo-list),empty-oppid-list,cwo-list,world,crash-nr,joinreq-list,empty-pid-list,next-join-list,empty-pid-list,joinack-list,oldworld)))
       <| or(not(eq(oldworld,empty-pid-list)),empty(joinack-list)) |> delta


%% LRM crashes.

     + crash(pid).LRMCrashed(pid)


%% LRM performs crash recovery at the end of round ts.

  CrashRecovery(pid:PId,ts:Bit,wo-list:OpPIdList,nwo-list:OpPIdList,cwo-list:OpPIdList,world:PIdList,pid-list:PIdList,bit:Bit,joinack-list:PIdList,joinreq-list:PIdList,join-list:PIdList,next-join-list:PIdList) =


%% LRM asks the head of pid-list to send its wo-list for round ts.

      sum(oppid-list:OpPIdList,ask_wolist(head(pid-list),pid,ts,oppid-list).
         CrashRecovery(pid,ts,union(wo-list,oppid-list),nwo-list,cwo-list,world,tail(pid-list),bit,joinack-list,joinreq-list,join-list,next-join-list)
      <| not(empty(pid-list)) |> delta)


%% LRM detects that a node in pid-list has crashed. The bit is set to 1, to ensure that in the end
%% crash recovery will be repeated.

    + sum(pid':PId,recv_crash_cha2lrm(pid,pid').
         CrashRecovery(pid,ts,wo-list,nwo-list,cwo-list,remove(pid',world),remove(pid',pid-list),1,joinack-list,joinreq-list,join-list,next-join-list)
      <| element(pid',pid-list) |> delta)


%% Another node pid' asks for the cwo-list of node pid, to carry out crash recovery.
%% The check whether a local write from the requesting node pid' is present in wo-list
%% makes sure that pid' is referring to the previous (and not the next) round.

    + sum(pid':PId,give_wolist(pid,pid',invert(ts),cwo-list).
         CrashRecovery(pid,ts,wo-list,nwo-list,cwo-list,world,pid-list,bit,joinack-list,joinreq-list,join-list,next-join-list)
      <| not(arrived(pid',wo-list)) |> delta)


%% Another node pid' asks for the wo-list of node pid, to carry out crash recovery.

    + sum(pid':PId,give_wolist(pid,pid',ts,wo-list).
         CrashRecovery(pid,ts,wo-list,nwo-list,cwo-list,world,pid-list,bit,joinack-list,joinreq-list,join-list,next-join-list))


%% Suppose pid-list has become empty. If b=0, LRM completes crash recovery and enters the next round.
%% It executes wo-list, after stripping all node identities and NOPs. It inverts the round number,
%% the wo-list becomes the cwo-list,  the nwo-list becomes the wo-list. joinack-list and join-list
%% are added to the world.
%% All nodes that were detected as crashed in round ts, but of which writes were recovered, count as
%% crashes in the next round. Also crashes that were detected during crash recovery count for the next
%% round. That is, the number of crashes for the next round is length(wo-list) - length(world).

    + execute(pid,strip(wo-list)).
         NextRound(pid,invert(ts),nwo-list,wo-list,union(union(world,joinack-list),join-list),monus(length(wo-list),length(world)),joinack-list,joinreq-list,next-join-list,world)
      <| and(eq(bit,0),empty(pid-list)) |> delta


%% Suppose pid-list has become empty. If b=1, crash recovery is repeated.

    + tau.CrashRecovery(pid,ts,wo-list,nwo-list,cwo-list,world,world,0,joinack-list,joinreq-list,join-list,next-join-list)
      <| and(eq(bit,1),empty(pid-list)) |> delta


%% LRM crashes.

    + crash(pid).LRMCrashed(pid)


%% OutBuffer is asked by LRM to inform all nodes in the world pid-list of the local write operation op
%% in round ts, and the list of local joins pid-list' that will join after this round.

  OutBuffer(pid:PId) = sum(op:Op,sum(ts:Bit,sum(pid-list:PIdList,sum(pid-list':PIdList,recv_outbuffer(pid,op,ts,pid-list,pid-list').
                          Broadcast(pid,op,ts,pid-list,pid-list')))))


%% OutBuffer is asked by LRM to acknowledge all local joins in pid-list' that they can join the world,
%% in round ts and with world pid-list.

    + sum(ts:Bit,sum(pid-list:PIdList,sum(crash-nr:Nat,sum(pid-list':PIdList,recv_outbuffer(pid,ts,pid-list,crash-nr,pid-list').JoinAck(pid,ts,pid-list,crash-nr,pid-list')))))


%% OutBuffer sends the write <op,pid,ts,pid-list'> to the channel in the direction of the head of pid-list,
%% and continues with the tail of pid-list.

  Broadcast(pid:PId,op:Op,ts:Bit,pid-list:PIdList,pid-list':PIdList) =

      send_lrm2cha(pid,head(pid-list),op,ts,pid-list').Broadcast(pid,op,ts,tail(pid-list),pid-list')
      <| and(not(empty(pid-list)),not(eq(length(pid-list),succ(zero)))) |> delta


%% When pid-list becomes empty, OutBuffer returns to its initial state.

    + send_lrm2cha(pid,head(pid-list),op,ts,pid-list').OutBuffer(pid)
      <| eq(length(pid-list),succ(zero)) |> delta

    + tau.OutBuffer(pid) <| empty(pid-list) |> delta


%% The FIFO channel from node pid to node pid'.

  Channel(pid:PId,pid':PId,opbitpidlist-list:OpBitPIdListList) =


%% The channel receives a join acknowledgement.

     sum(ts:Bit,sum(pid-list:PIdList,sum(crash-nr:Nat,recv_lrm2cha(pid,pid',ts,pid-list,crash-nr).Channel(pid,pid',opbitpidlist-list,ts,pid-list,crash-nr))))


%% The channel receives a write operation plus join-list.

   + sum(op:Op,sum(ts:Bit,sum(pid-list:PIdList,recv_lrm2cha(pid,pid',op,ts,pid-list).
        Channel(pid,pid',attach(op,ts,pid-list,opbitpidlist-list)))))


%% The channel passes on the head of its OpBitPIdListList to pid'.

    + send_cha2lrm(pid',pid,ophead(opbitpidlist-list),bithead(opbitpidlist-list),pidlisthead(opbitpidlist-list)).
         Channel(pid,pid',tail(opbitpidlist-list))
      <| not(empty(opbitpidlist-list)) |> delta


%% The channel crashes after its LRM has crashed. It sends a notification to the failure detector
%% of node pid'.

    + recv_crash_lrm2cha(pid).send_crash_cha2lrm(pid',pid).delta


%% The FIFO channel from node pid to node pid', carrying a join acknowledgement (ts,pid-list).

  Channel(pid:PId,pid':PId,opbitpidlist-list:OpBitPIdListList,ts:Bit,pid-list:PIdList,crash-nr:Nat) =


%% The channel passes on the join acknowledgement to pid'.

  send_cha2lrm(pid',pid,ts,pid-list,crash-nr).Channel(pid,pid',opbitpidlist-list)


%% The channel crashes after its LRM has crashed. It sends a notification to the failure detector
%% of node pid'.

    + recv_crash_lrm2cha(pid).send_crash_cha2lrm(pid',pid).delta


%% OutBuffer sends a join acknowledgement to the head of pid-list', informing about the round number and
%% the world. It continues with the tail of pid-list'.

  JoinAck(pid:PId,ts:Bit,pid-list:PIdList,crash-nr:Nat,pid-list':PIdList) =

      send_lrm2cha(pid,head(pid-list'),ts,pid-list,crash-nr).JoinAck(pid,ts,pid-list,crash-nr,tail(pid-list'))
      <| and(not(empty(pid-list')),not(eq(length(pid-list'),succ(zero)))) |> delta


%% When pid-list' becomes empty, OutBuffer returns to its initial state.

    + send_lrm2cha(pid,head(pid-list'),ts,pid-list,crash-nr).OutBuffer(pid)
      <| eq(length(pid-list'),succ(zero)) |> delta


%% The fact that node pid crashed, can be detected by failure detectors at other nodes.

  LRMCrashed(pid:PId) = send_crash_lrm2cha(pid).LRMCrashed(pid)


%% WriteLock can be claimed by a local thread, and later released again by this thread.

  WriteLock(pid:PId) = recv_w_lock_request(pid).recv_w_lock_release(pid).WriteLock(pid)


init hide({com_w_lock_request,com_w_lock_release,com_notification,com_localwrite,com_outbuffer,com_remotewrite,
           com_lrm2cha,com_cha2lrm,com_crash_lrm2cha,com_crash_cha2lrm,com_wolist,com_joinreq},
       encap({send_w_lock_request,send_w_lock_release,send_notification,send_localwrite,send_outbuffer,
              send_remotewrite,send_lrm2cha,send_cha2lrm,send_crash_lrm2cha,send_crash_cha2lrm,ask_wolist,
              send_joinreq,
              recv_w_lock_request,recv_w_lock_release,recv_notification,recv_localwrite,recv_outbuffer,
	      recv_remotewrite,recv_lrm2cha,recv_cha2lrm,recv_crash_lrm2cha,recv_crash_cha2lrm,give_wolist,
              recv_joinreq},
  LocalRoundManager(p1,0,empty-oppid-list,empty-oppid-list,empty-oppid-list,empty-pid-list,zero,empty-pid-list,empty-pid-list,empty-pid-list,empty-pid-list,empty-pid-list,empty-pid-list)
  || Thread(p1,in(w1,empty-op-list)) || WriteLock(p1) ||
  OutBuffer(p1) || Channel(p1,p2,empty-opbitpidlist-list) || Channel(p1,p3,empty-opbitpidlist-list) ||
  Join(p2) || Thread(p2,in(w2,empty-op-list)) || WriteLock(p2) ||
  OutBuffer(p2) || Channel(p2,p1,empty-opbitpidlist-list) || Channel(p2,p3,empty-opbitpidlist-list) ||
  Join(p3) || Thread(p3,in(w3,empty-op-list)) || WriteLock(p3) ||
  OutBuffer(p3) || Channel(p3,p1,empty-opbitpidlist-list) || Channel(p3,p2,empty-opbitpidlist-list)))