--- Execution with cascading network changes.
--- Second change occurs before all group messages 
--- of first change have been received.

--- 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("b"),group("Winners"))) ;
      PERFORM(SEND(agent("b"),1)) ; --- b joins winners
      PERFORM(RECEIVE(agent("a"),1)) ;
      PERFORM(RECEIVE(agent("b"),1)) ;
      PERFORM(RECEIVE(agent("c"),1)) ;

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

      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(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"),3)) ;  --- a sends group message
      PERFORM(RECEIVE(agent("a"),3)) ;
      PERFORM(LOSE(agent("b"),3)) ;
      PERFORM(LOSE(agent("c"),3)) ;

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

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

      PERFORM(CHANGE(agent("a"),(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c"))))) ;
      PERFORM(CHANGE(agent("b"),(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c"))))) ;
      PERFORM(CHANGE(agent("c"),(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")))))
      ;
      ( 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(RECEIVE(agent("b"),6)) ;
      PERFORM(RECEIVE(agent("c"),6)) ;

      PERFORM(SENDGROUPMSG(agent("b"))) ;
      PERFORM(SEND(agent("b"),7)) ;  --- b sends group message
      PERFORM(RECEIVE(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(RECEIVE(agent("a"),8)) ;
      PERFORM(RECEIVE(agent("b"),8)) ;
      PERFORM(RECEIVE(agent("c"),8)) ;

      PERFORM(RECEIVE(agent("b"),5)) ; --- earlier group message arives too late
      PERFORM(RECEIVE(agent("c"),5)) ;

      PERFORM(LEAVE(agent("a"),group("Winners"))) ;
      PERFORM(SEND(agent("a"),9)) ;
      PERFORM(RECEIVE(agent("a"),9)) ;
      PERFORM(RECEIVE(agent("b"),9)) ;
      PERFORM(RECEIVE(agent("c"),9)) ;

      PERFORM(DISCONNECT(agent("b"))) ;
      PERFORM(SEND(agent("b"),10)) ;
      PERFORM(RECEIVE(agent("a"),10)) ;
      PERFORM(RECEIVE(agent("b"),10)) ;
      PERFORM(RECEIVE(agent("c"),10)) 

      )
      .

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("b"), 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 b(2) 
   sp-join-ack(agent("b")) =>
   b(3) .   

rl a(3) b(3) =>
   a(4) b(4)
   sp-leave-req(agent("a"), group("Winners")) .
   
rl a(4) b(4)
   sp-leave-ack(agent("a")) =>
   a(5) b(5) .

rl a(5) b(5) =>
   sp-disconnect-req(agent("b")) 
   a(6) b(6) .

rl a(6) b(6)
   sp-disconnect-ack(agent("b")) =>
   a(7) b(7) .
   
endm

--- search init =>! state:State .

rew init .