--- Execution which cascading network changes.  Another change occurs
--- before flush ok messages are send to confirm first one:
---
--- In detail:
--- c joins group with all necessary flush oks provided
--- a joins group with all necessary flush oks provided
--- network splits into {a},{b,c}
--- a and c confirm flush request with flush ok
--- b joins group 
--- b and c confirm flush request with flush ok
--- network merges
--- network splits again into {a,c},{b} before flusk oks are provided
--- a, b and c confirm flush request with flush ok
--- a leaves group
--- b and c confirm flush request with flush ok
--- b disconnects

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

in test.maude 
in gtest.maude
in ftest.maude

mod TEST-SPREAD is

protecting FLUSHSPREAD .
protecting TEST .
protecting GTEST .
protecting FTEST .

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

--- agents program counter

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

--- initial state 

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

    f-receive-req(agent("a"))
    f-receive-req(agent("b"))
    f-receive-req(agent("c"))
    fdelivered(agent("a"),eFMessageList)
    fdelivered(agent("b"),eFMessageList)
    fdelivered(agent("c"),eFMessageList)
    fdelivered'(agent("a"),eFMessageList)
    fdelivered'(agent("b"),eFMessageList)
    fdelivered'(agent("c"),eFMessageList)

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

      PERFORM(DELIVERCHANGE(agent("c"))) ;

      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(FLUSHOK(agent("a"))) ;
      PERFORM(MULTICAST(agent("a"),group("Winners"))) ;
      PERFORM(SEND(agent("a"),3)) ; 
      PERFORM(RECEIVE(agent("a"),3)) ;
      PERFORM(RECEIVE(agent("b"),3)) ;
      PERFORM(RECEIVE(agent("c"),3)) ;

      PERFORM(FLUSHOK(agent("c"))) ;
      PERFORM(MULTICAST(agent("c"),group("Winners"))) ;
      PERFORM(SEND(agent("c"),4)) ; 
      PERFORM(RECEIVE(agent("a"),4)) ;
      PERFORM(RECEIVE(agent("b"),4)) ;
      PERFORM(RECEIVE(agent("c"),4)) ;

      PERFORM(DELIVERCHANGE(agent("a"))) ;
      PERFORM(DELIVERCHANGE(agent("c"))) ;

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

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

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

      PERFORM(DELIVERCHANGE(agent("a"))) ;
      PERFORM(DELIVERCHANGE(agent("c"))) ;

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

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

      PERFORM(DELIVERCHANGE(agent("a"))) ;
      PERFORM(DELIVERCHANGE(agent("c"))) ;

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

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

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

      PERFORM(DELIVERCHANGE(agent("b"))) ;
      PERFORM(DELIVERCHANGE(agent("c"))) ;

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

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

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

      PERFORM(DELIVERCHANGE(agent("a"))) ;
      PERFORM(DELIVERCHANGE(agent("b"))) ;
      PERFORM(DELIVERCHANGE(agent("c"))) ;

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

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

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

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

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

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

      PERFORM(DELIVERCHANGE(agent("a"))) ;
      PERFORM(DELIVERCHANGE(agent("b"))) ;
      PERFORM(DELIVERCHANGE(agent("c"))) ;

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

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

      PERFORM(DELIVERCHANGE(agent("a"))) ;
      PERFORM(DELIVERCHANGE(agent("c"))) ;

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

      )
      .

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

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

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

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

rl b(2) 
   f-join-ack(agent("b")) =>
   b(3) .   


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

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

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


endm

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

rew init .