--- Private group unicast.
--- Sender is external to the group.

--- 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 FLUSHSPREAD .
protecting TEST .
protecting GTEST .

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)

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

    CONTROLLER(

      PERFORM(MULTICAST-TEST) ;

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

      )
      .

op MULTICAST-TEST : -> Action .

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(3) b(3) c(3) .

rl a(3) 
   ENABLED(MULTICAST-TEST) =>
   a(4)
   PERFORMED(MULTICAST-TEST)
   sp-multicast-req(agent("a"), agreed, privategroup(agent("c")), gdata("TEST")) .

rl a(4)
   sp-multicast-ack(agent("a")) =>
   a(5) .

endm

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

rew init .