--- Simple scenario with two messages (one reliable, 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
--- one message is lost by a. 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
--- lost message which is not delivered at a.

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

in test.maude

mod TEST1 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"), agreed, data("test0"))
    multicast-req(proc("c"), reliable, 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(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("a"),1)) ;  --- a loses message 1
      PERFORM(RECEIVE(proc("a"),0)) ;  --- a receives message 0
      
      ( PERFORM(EVS-START(proc("a"),true)) || --- EVS algorithm initiated at a
        PERFORM(EVS-START(proc("b"),true)) || --- EVS algorithm initiated at b
        PERFORM(EVS-START'(proc("c"),true)) ) --- EVS algorithm starts at c (b wakes up c)
        --- true flag means that a, b, and c execute evs algorithm sucessfully
      )
      .

endm

rew start .