--- Sending of safe message followed by network partition into {a},
--- {b,c}.  Processor c fails and recovers, while a and b complete the
--- evs algorithm. c loses all acks for safe messages during failure,
--- including its own, and hence cannot deliver the safe
--- message. Later, after the process recovers, a new run of the evs
--- algorithm is triggered that establishes full connectivity again.

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

in test.maude

mod TEST11 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("test")) 

    CONTROLLER(
      PERFORM(SEND(proc("a"),0)) ;     
      PERFORM(RECEIVE(proc("a"),0)) ;  
      PERFORM(RECEIVE(proc("b"),0)) ;  
      PERFORM(RECEIVE(proc("c"),0)) ;  

      PERFORM(RECEIVE(proc("a"),1)) ;  
      PERFORM(RECEIVE(proc("b"),1)) ;  

      PERFORM(RECEIVE(proc("a"),2)) ;  
      PERFORM(RECEIVE(proc("b"),2)) ;  

      PERFORM(RECEIVE(proc("a"),3)) ;  
      PERFORM(RECEIVE(proc("b"),3)) ;  

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

      PERFORM(LOSE(proc("c"),1)) ;  --- ack lost
      PERFORM(LOSE(proc("c"),2)) ;  --- ack lost
      PERFORM(LOSE(proc("c"),3)) ;  --- ack lost

      ( PERFORM(EVS-START(proc("a"),true)) ||
        PERFORM(EVS-START(proc("b"),true)) ) --- a, b finish sucessfully
      ;

      PERFORM(CRECOVER(proc("c"))) 
      ;

      ( PERFORM(CHANGE(proc("a"),(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))))) || --- a receives conf change
        PERFORM(CHANGE(proc("b"),(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))))) || --- b receives conf change
        PERFORM(CHANGE(proc("c"),(sProcSet(proc("a")) 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"),true)) ) --- a, b, and c finish sucessfully
      )

      .


endm

rew start .