--- Normal EVS-Group execution with split and merge of the network.
---
--- Parameters:
--- 	- EVS Semantics
---	- sending-time rekey 
---		- no key is generated until the application requests to
---		  send a message.
---		- after a view change no key is generated
---		- if no view change and the application request to send 
---		  another message, same key s used; if new view then rekey
---	- non-blocking data
---		- data is sent and received while rekey is in progress
---
---
--- Scenario:
--- 	- c joins group
--- 	- a joins group
--- 	- network splits (a separates from b and c)
--- 	- b joins group
--- 	- network merges (a, b, and c together again)
--- 	- c multicasts message "test"
---		- new key is generated
---	 	- message is sent
---		- everybody gets and delivers the multicast message
--- 	- a leaves group
--- 	- b disconects

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

in test.maude 
in gtest.maude
in stest.maude

mod TEST-SECURESPREAD is

protecting SECURESPREAD .
protecting TEST .
protecting GTEST .
protecting STEST .

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

--- program counter of agents

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)
    fresh(0) 		--- for cliques
    freshkeyid(0)  	--- for keyId 

    ssp-receive-req(agent("a"))
    ssp-receive-req(agent("b"))
    ssp-receive-req(agent("c"))
    sdelivered(agent("a"),eSMessageList)
    sdelivered(agent("b"),eSMessageList)
    sdelivered(agent("c"),eSMessageList)
    sdelivered'(agent("a"),eSMessageList)
    sdelivered'(agent("b"),eSMessageList)
    sdelivered'(agent("c"),eSMessageList)
    
    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(FLUSHOK(agent("a"))) ;
      PERFORM(MULTICAST(agent("a"),group("Winners"))) ;
      PERFORM(SEND(agent("a"),16)) ; 
      PERFORM(RECEIVE(agent("a"),16)) ;
      PERFORM(RECEIVE(agent("b"),16)) ;
      PERFORM(RECEIVE(agent("c"),16)) ;

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

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

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


      PERFORM(MULTICAST-TEST) ;	---no key has been generated

      PERFORM(MULTICAST(agent("c"),group("Winners"))) ;	 ---force rekey
      PERFORM(SEND(agent("c"),19)) ;  
      PERFORM(RECEIVE(agent("a"),19)) ;
      PERFORM(RECEIVE(agent("b"),19)) ;
      PERFORM(RECEIVE(agent("c"),19)) ;     

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

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

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

      PERFORM(MULTICAST(agent("a"),privategroup(agent("b")))) ;
      PERFORM(SEND(agent("a"),23)) ; 
      PERFORM(RECEIVE(agent("a"),23)) ;
      PERFORM(RECEIVE(agent("b"),23)) ;
      PERFORM(RECEIVE(agent("c"),23)) ;

      PERFORM(MULTICAST(agent("b"),privategroup(agent("c")))) ;
      PERFORM(SEND(agent("b"),24)) ; 
      PERFORM(RECEIVE(agent("a"),24)) ;
      PERFORM(RECEIVE(agent("b"),24)) ;
      PERFORM(RECEIVE(agent("c"),24)) ;

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

      PERFORM(MULTICAST(agent("a"),privategroup(agent("c")))) ;
      PERFORM(SEND(agent("a"),26)) ; 
      PERFORM(RECEIVE(agent("a"),26)) ;
      PERFORM(RECEIVE(agent("b"),26)) ;
      PERFORM(RECEIVE(agent("c"),26)) ;

      PERFORM(MULTICAST(agent("b"),privategroup(agent("c")))) ;
      PERFORM(SEND(agent("b"),27)) ; 
      PERFORM(RECEIVE(agent("a"),27)) ;
      PERFORM(RECEIVE(agent("b"),27)) ;
      PERFORM(RECEIVE(agent("c"),27)) ;

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

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


      PERFORM(MULTICAST(agent("c"),group("Winners"))) ;   ---key generated, message sent
      PERFORM(SEND(agent("c"),29)) ; 
      PERFORM(RECEIVE(agent("a"),29)) ;
      PERFORM(RECEIVE(agent("b"),29)) ;
      PERFORM(RECEIVE(agent("c"),29)) ;


      PERFORM(LEAVE(agent("a"),group("Winners"))) ; --- a leaves winners
      PERFORM(SEND(agent("a"),30)) ;
      PERFORM(RECEIVE(agent("a"),30)) ;
      PERFORM(RECEIVE(agent("b"),30)) ;
      PERFORM(RECEIVE(agent("c"),30)) ;

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

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


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

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

      PERFORM(DELIVERCHANGE(agent("c"))) 
            
      )
      .

op MULTICAST-TEST : -> Action .

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

rl a(1) b(1) c(1)
   ssp-connect-ack(agent("a"))  
   ssp-connect-ack(agent("b")) 
   ssp-connect-ack(agent("c")) 
   => 
   a(2) b(2) c(2)
   ssp-join-req(agent("a"), group("Winners"), group-evs, sending-time, non-blocking)
   ssp-join-req(agent("b"), group("Winners"), group-evs, sending-time, non-blocking)
   ssp-join-req(agent("c"), group("Winners"), group-evs, sending-time, non-blocking) .

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

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

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

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

rl b(3) 
   ENABLED(MULTICAST-TEST) 
   =>
   b(4)
   PERFORMED(MULTICAST-TEST)
   ssp-multicast-req(agent("c"), reliable, group("Winners"), sdata("TEST")) .

rl b(4)
   ssp-multicast-ack(agent("c")) 
   =>
   b(5) .
   
rl a(5) b(5) 
   =>
   ssp-disconnect-req(agent("b")) 
   a(6) b(6) .

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

endm 

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

rew init .