--- Scenario to explore the question:
--- What happens if evs algorithm fails (either due to disconnect or crash) ?

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

in test.maude

mod TEST5 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)

    CONTROLLER(
      ( PERFORM(CHANGE(proc("b"),(sProcSet(proc("b")) sProcSet(proc("c"))))) || 
        PERFORM(CHANGE(proc("c"),(sProcSet(proc("b")) sProcSet(proc("c"))))) )
      ;
      ( PERFORM(EVS-START(proc("b"),false)) ||    --- evs algorithm fails at b
        PERFORM(EVS-START'(proc("c"),true)) )      --- evs algorithm succeeds at c
      ;
      ( PERFORM(EVS-START(proc("b"),true)) ||  --- evs algorithm succeeds at b
        PERFORM(EVS-START'(proc("c"),true)) )   --- evs algorithm succeeds at c
      )

      .

endm

search start =>! state:State .