--- Normal EVS-Group execution with split and merge of the network.
---
--- Parameters:
--- 	- EVS Semantics
---	- changingt-time rekey 
---		- if the members of the group shared a key before, 
---	  	  that key is used (key cached); otherwise a new key
---		  is generated
---	- non-blocking data
---		- data is sent and received while rekey is in progress
---
---	- requested-sending-view message
---		- application requested to send a message in a particular view
---
---
--- Scenario:
--- 	- c joins group
--- 	- c multicast message "mytest" 
---		- message is sent but not received
--- 	- a joins group
--- 	- everybody (a,b,c) received the multicast message
---   		- a is part of the group so it receives the 
---		  the message, but can not decripted so the
--- 	  	  message is tagged as "nondecryptable" and
---		  delivered to the application
---   	- b is not part of the group, so it does not deliver it
---   	  to the application
---   	- c delivers the message to the application 
--- 	- network splits (a separates from b and c)
--- 	- b joins group
--- 	- network merges (a, b, and c together again)
--- 	- c multicasts message "test" using requested sending view
---		- everybody gets and delivers the multicast message
--- 	- a leaves group
---	- c and b shared a key before, so key is cached and rekey is avoided
--- 	- 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(MULTICAST-TEST) ;

      PERFORM(MULTICAST(agent("c"),group("Winners"))) ;
      PERFORM(SEND(agent("c"),2)) ;  --- message sent, but not received
     

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

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

      PERFORM(FLUSHOK(agent("c"))) ;
      PERFORM(MULTICAST(agent("c"),group("Winners"))) ;

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

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

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

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

      PERFORM(MULTICAST(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(DELIVERCHANGE(agent("a"))) ;
      PERFORM(DELIVERCHANGE(agent("c"))) ;
      
     
      PERFORM(RECEIVE(agent("a"),2)) ;	--- message received
      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"),10)) ;  --- a sends group message
      PERFORM(RECEIVE(agent("a"),10)) ;
      PERFORM(LOSE(agent("b"),10)) ;
      PERFORM(LOSE(agent("c"),10)) ;

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


      PERFORM(MULTICAST-TEST) ;	--- message with sending requested view 
      
      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(LEAVE(agent("a"),group("Winners"))) ; --- a leaves winners
      PERFORM(SEND(agent("a"),35)) ;
      PERFORM(RECEIVE(agent("a"),35)) ;
      PERFORM(RECEIVE(agent("b"),35)) ;
      PERFORM(RECEIVE(agent("c"),35)) ;

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

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


      --- previous key cached, no rekey
      
      PERFORM(DELIVERCHANGE(agent("a"))) ;
      PERFORM(DELIVERCHANGE(agent("b"))) ; 
      PERFORM(DELIVERCHANGE(agent("c"))) ;


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

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

      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, changing-time, non-blocking)
   ssp-join-req(agent("b"), group("Winners"), group-evs, changing-time, non-blocking)
   ssp-join-req(agent("c"), group("Winners"), group-evs, changing-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"),req-sending-view) .

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

rl c(4) 
   ssp-multicast-ack(agent("c")) 
   =>
   c(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 .