--- Scenario to explore the problem with self delivery due to use of
--- reliable and causal messages. The problem occured in an earlier
--- version of the specification that generlized Yair's causal
--- delivery condition to take into account arbitrary messages (that
--- is not only causal). The problem was that a cannot deliver its own
--- message because it depends on the first message send by b, which
--- was lost.

--- In the present version of the specification, we have relativized
--- the causal past cone (that is the messages that need to be
--- delivered before the current one) to messages sent by members of
--- the current configuration. This allows for gaps in the causal
--- order during the transitional configuration, and in this example
--- it allows the gap caused by the lost message from a, so that
--- the self delivery property is not violated.

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

in test.maude

mod TEST14 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("b"), reliable, data("test1")) 
    multicast-req(proc("b"), reliable, data("test2")) 
    multicast-req(proc("a"), causal, data("test3")) 

    CONTROLLER(

      PERFORM(SEND(proc("b"),0)) ;     
      PERFORM(RECEIVE(proc("b"),0)) ;  

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

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

      PERFORM(LOSE(proc("a"),0)) ;

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

      )

      .


endm

rew start .
--- search start =>! state:State .