--- Execution with safe data message followed by join, both lost by
--- a, and delivered in transitional mode at b and c. Note the delay
--- between the change in the network and the time when the evs
--- algorithm is triggered. Note also that there is no
--- causal order between the data message and the following join
--- message from b, but since both are agreed they are delivered
--- in the same order everywhere. In this case, join can be delivered
--- immediately, but the safe data message not, because acks are lost.
--- In fact, the join message can be still delivered in the regular
--- configuration, but the data message only in the transitional one.

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

in test.maude 
in gtest.maude

mod TEST-SPREAD is

protecting SPREAD .
protecting TEST .
protecting GTEST .

eq allprocs = sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")) .

--- initial state 

op a : Nat -> State .
op b : Nat -> State .
op c : Nat -> State .

op init : -> State .
eq init =
    network(allprocs)
    mkinitialconf(allprocs)
    mkinitialprocs(allprocs)
    mkinitialagents(allprocs)

    a(0) b(0) c(0) 

    CONTROLLER(
      PERFORM(JOIN(agent("c"),group("Winners"))) ; --- c joins winners
      PERFORM(SEND(agent("c"),0)) ; 
      PERFORM(RECEIVE(agent("a"),0)) ;
      PERFORM(RECEIVE(agent("b"),0)) ;
      PERFORM(RECEIVE(agent("c"),0)) ;

      PERFORM(JOIN(agent("a"),group("Winners"))) ; --- a joins winners
      PERFORM(SEND(agent("a"),1)) ;
      PERFORM(RECEIVE(agent("a"),1)) ;
      PERFORM(RECEIVE(agent("b"),1)) ;
      PERFORM(RECEIVE(agent("c"),1)) ;

      PERFORM(CHANGE(agent("a"),sProcSet(agent("a")))) ;
      PERFORM(CHANGE(agent("b"),(sProcSet(agent("b")) sProcSet(agent("c"))))) ;
      PERFORM(CHANGE(agent("c"),(sProcSet(agent("b")) sProcSet(agent("c"))))) ;

      PERFORM(MULTICAST(agent("c"),group("Winners"))) ;
      PERFORM(SEND(agent("c"),2)) ;
      PERFORM(LOSE(agent("a"),2)) ;
      PERFORM(RECEIVE(agent("b"),2)) ;
      PERFORM(RECEIVE(agent("c"),2)) ;

      PERFORM(LOSE(agent("a"),3)) ;
      PERFORM(RECEIVE(agent("b"),3)) ;
      PERFORM(RECEIVE(agent("c"),3)) ;

      PERFORM(LOSE(agent("a"),4)) ;
      PERFORM(RECEIVE(agent("b"),4)) ;
      PERFORM(RECEIVE(agent("c"),4)) ;

      PERFORM(JOIN(agent("b"),group("Winners"))) ;
      PERFORM(SEND(agent("b"),5)) ; --- b joins winners
      PERFORM(LOSE(agent("a"),5)) ;
      PERFORM(RECEIVE(agent("b"),5)) ;
      PERFORM(RECEIVE(agent("c"),5)) ;

      ( PERFORM(EVS-START(agent("a"),true)) ||
        PERFORM(EVS-START(agent("b"),true)) ||
        PERFORM(EVS-START'(agent("c"),true)) ) --- a, b, and c finish sucessfully
      ;
      PERFORM(SENDGROUPMSG(agent("a"))) ;
      PERFORM(SEND(agent("a"),6)) ;  --- a sends group message
      PERFORM(RECEIVE(agent("a"),6)) ;
      PERFORM(LOSE(agent("b"),6)) ;
      PERFORM(LOSE(agent("c"),6)) ;

      PERFORM(SENDGROUPMSG(agent("b"))) ;
      PERFORM(SEND(agent("b"),7)) ;  --- b sends group message
      PERFORM(LOSE(agent("a"),7)) ;
      PERFORM(RECEIVE(agent("b"),7)) ;
      PERFORM(RECEIVE(agent("c"),7)) ;

      PERFORM(SENDGROUPMSG(agent("c"))) ;
      PERFORM(SEND(agent("c"),8)) ;  --- c sends group message
      PERFORM(LOSE(agent("a"),8)) ; 
      PERFORM(RECEIVE(agent("b"),8)) ;
      PERFORM(RECEIVE(agent("c"),8)) 

      )
      .

rl a(0) b(0) c(0) =>
   a(1) b(1) c(1)
   sp-connect-req(agent("a")) 
   sp-connect-req(agent("b")) 
   sp-connect-req(agent("c")) .

rl a(1) b(1) c(1)
   sp-connect-ack(agent("a"))  
   sp-connect-ack(agent("b")) 
   sp-connect-ack(agent("c")) => 
   a(2) b(2) c(2)
   sp-join-req(agent("a"), group("Winners"))
   sp-join-req(agent("c"), group("Winners")) .

rl c(2)
   sp-join-ack(agent("c")) =>
   c(3) .

rl a(2)
   sp-join-ack(agent("a")) =>
   a(3) .

rl a(3) b(2) =>
   a(4) b(4)
   sp-multicast-req(agent("c"), safe, group("Winners"), gdata("test")) .
   
rl a(4) b(4)
   sp-multicast-ack(agent("c")) =>
   a(5) b(5) .

rl a(5) b(5) =>
   a(6) b(6)
   sp-join-req(agent("b"), group("Winners")) .
   
rl a(6) b(6)
   sp-join-ack(agent("b")) =>
   a(7) b(7) .
   
endm

rew init .