--- Simple scenario with two messages (one safe, one agreed) sent by
--- different processes. The network which upon startup forms a single
--- partition {a,b,c} splits into two partitions {a},{b,c} and
--- acknowledgements for the safe message are lost at b and c (so that
--- they cannot be recovered inside {b,c}). The EVS algorithm is
--- triggered by the network change and executes sucessfully. All
--- messages can be delivered in the previous regular configuration,
--- except for the safe messages which needs to be delivered in the
--- transitional configuration at b and c, because b and c don't know
--- if a has received it (which is the case here). But a knows that b
--- and c have received the safe message, hence, it can be delivered
--- in the regular configuration at a.

--- See delivered(proc,...) in the corresponding .out-file for the messages
--- delivered to the upper layer at proc.

in test.maude

mod TEST2 is

protecting TEST .

eq allprocs = sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")) .

--- initial state 

op start : -> State .
eq start =

    network(allprocs)
    mkinitialconf(allprocs)
    mkinitialprocs(allprocs)

    multicast-req(proc("a"), safe, data("test0")) 
    multicast-req(proc("c"), agreed, data("test1")) 

    CONTROLLER(
      PERFORM(SEND(proc("a"),0)) ;     --- a sends message 0
      PERFORM(SEND(proc("c"),1)) ;     --- c sends message 1
      PERFORM(RECEIVE(proc("c"),1)) ;  --- c receives message 1
      PERFORM(RECEIVE(proc("b"),1)) ;  --- b receives message 1
      PERFORM(RECEIVE(proc("b"),0)) ;  --- b receives message 0
      PERFORM(RECEIVE(proc("c"),0)) ;  --- c receives message 1
      PERFORM(RECEIVE(proc("a"),1)) ;  --- a receives message 1
      PERFORM(RECEIVE(proc("a"),0)) ;  --- a receives message 0

      PERFORM(RECEIVE(proc("a"),2)) ;  --- a receives message 2 (ack message)
      PERFORM(RECEIVE(proc("b"),2)) ;  --- b receives message 2 (ack message)
      PERFORM(RECEIVE(proc("c"),2)) ;  --- c receives message 2 (ack message)
      PERFORM(RECEIVE(proc("a"),3)) ;  --- a receives message 3 (ack message)
      PERFORM(RECEIVE(proc("b"),3)) ;  --- b receives message 3 (ack message)
      PERFORM(RECEIVE(proc("c"),3)) ;  --- c receives message 3 (ack message)
      PERFORM(RECEIVE(proc("a"),4)) ;  --- a receives message 4 (ack message)

      ( PERFORM(CHANGE(proc("a"),sProcSet(proc("a")))) || --- a receives conf change
        PERFORM(CHANGE(proc("b"),(sProcSet(proc("b")) sProcSet(proc("c"))))) || --- b receives conf change
        PERFORM(CHANGE(proc("c"),(sProcSet(proc("b")) sProcSet(proc("c")))))    --- c receives conf change
      ) ;

      PERFORM(LOSE(proc("b"),4)) ;     --- b loses message 4 (ack message)
      PERFORM(LOSE(proc("c"),4)) ;     --- c loses message 4 (ack message)

      ( PERFORM(EVS-START(proc("a"),true)) ||
        PERFORM(EVS-START(proc("b"),true)) ||
        PERFORM(EVS-START'(proc("c"),true)) ) --- a, b, and c execute evs algorithm sucessfully
      )
      .


endm

rew start .