--- Failure of evs algorithm at c.

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

in test.maude

mod TEST7 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"), reliable, data("test")) 

    CONTROLLER(
      PERFORM(SEND(proc("a"),0)) ;     --- a sends message 0

      PERFORM(RECEIVE(proc("a"),0)) ;  --- a receives message 0
      PERFORM(RECEIVE(proc("b"),0)) ;  --- b receives message 0
      PERFORM(RECEIVE(proc("c"),0)) ;  --- c receives message 0

      ( 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(EVS-START(proc("a"),true)) ||
        PERFORM(EVS-START(proc("b"),true)) ||
        PERFORM(EVS-START'(proc("c"),false)) ) --- a and b finish sucessfully, c fails
      )
      .


endm

search start =>! state:State .