--- Scenario to explore the question:
--- What happens when conectivity changes asymmetrically ?

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

in test.maude

mod TEST3 is

protecting TEST .

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


--- initial state 

op start : -> State .
eq start =

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

    multicast-req(proc("a"), agreed, data("")) 
    multicast-req(proc("b"), reliable, data("")) 

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

      PERFORM(CHANGE(proc("b"),sProcSet(proc("b")))) ; 
                                       --- a gets disconnected from the viewpoint of b

      PERFORM(LOSE(proc("a"),1)) ;     --- a loses message 1

      PERFORM(EVS-START(proc("b"),true)) ;        --- evs algorithm gets triggered

      PERFORM(CHANGE(proc("b"),(sProcSet(proc("a")) sProcSet(proc("b"))))) ; 
                                       --- a gets reconnected from the viewpoint of b
      ( PERFORM(EVS-START(proc("b"),true)) ;
        PERFORM(EVS-START'(proc("a"),true)) )  --- evs algorithm succeeds at a and b
      )
    .

endm

search start =>! state:State .
--- essentially different solutions are due to order of delivery at b
--- (two possibilities)