GCS.LOT:

 * UPDATE, AUGUST 15:
 *      - Splitting of GCS process in multiple processes. More readable.
 *      - DoubleBuffer now empties the request buffer when a group is deleted
 *        (accepted requests are not executed).
 *      - Other Multicast protocols defined.
 *
 * TO DO:
 * 	- A moderator should be implicitly member of a closed group
 *      - More systematic tests, inspired from UCM scenarios and combinations
 *      - Add several options as Multicast protocols.
 *      - Express group characteristics as policies?
---
 * UPDATE, JULY 8:
 *      - Creation of team processes corresponding to the UCM architecture.
 *      - Replacement of Listen by a bi-directional, infinite double buffer
 *        for requests and acknowledgements
 *      - Completion of ADTs. Renaming of several constructs and types.
 *        Creation of a generic FIFO type.
 *      - 7 test process defined, all with adequate use of ADTs. They all
 *        pass successfully.
 *      - Correct management of administered groups
 *      - Correct management of moderated groups
 *      - Management of opened/closed groups
 *      - Management of public/private groups
 *
 * TO DO:
 *      - More systematic tests, inspired from UCM scenarios and combinations
 *      - Split the GCS process (>200 lines) 
 *      - Add several options as Multicast protocols.
 *      - Express group characteristics as policies?
 
 ----
 
 (***************************************************************************
 *
 *      Multicast
 *
 *      Send the message to all subscriber of the group (concurrently).  
 *      No other message will be multicast until all members of the group 
 *      received it.
 *
 ***************************************************************************)

process Multicast[out](sender:MID, msg:Msg, mbrL:MemberList, UseChannel: Bool)
                  : exit :=

    [mbrL eq NoMBR] ->   
         exit

    []

    [mbrL ne NoMBR] ->
        (
            (
                [UseChannel] -> 
                    (* Multicasts message to members on their appropriate
                       data channel *)
                    out !Top(mbrL) !sender !msg; 
                        exit
                []
                [Not(UseChannel)] ->
                    (* Use request/ack channel *)
                    out !MID(Top(mbrl)) !GetAck(msg);
                        exit
            )
            |||
            Multicast[out](sender, msg, Tail(mbrL), UseChannel) (* loop... *)
        )

endproc (* Multicast *)



(***************************************************************************
 *
 *      Multicast
 *
 *      Send the message to all subscriber of the group (sequentially).  
 *      No other message will be multicast until all members of the group 
 *      received it.
 *
 ***************************************************************************)

process Multicast[out](sender:MID, msg:Msg, mbrL:MemberList, UseChannel: Bool)
                  : exit :=

    [mbrL eq NoMBR] ->   
         exit

    []

    [mbrL ne NoMBR] ->
        (
            [UseChannel] -> 
                (* Multicasts message to members on their appropriate
                   data channel *)
                out !Top(mbrL) !sender !msg; 
                    Multicast[out](sender, msg, Tail(mbrL), UseChannel) (* loop... *)
            []
            [Not(UseChannel)] ->
                (* Use request/ack channel *)
                out !MID(Top(mbrl)) !GetAck(msg);
                    Multicast[out](sender, msg, Tail(mbrL), UseChannel) (* loop... *)
        )

endproc (* Multicast *)


 (***************************************************************************
 *
 *      Multicast
 *
 *      Send the message to all subscriber of the group.  
 *      Best effort, without retry. Could be extended to include retries
 *
 ***************************************************************************)

process Multicast[out](sender:MID, msg:Msg, mbrL:MemberList, UseChannel: Bool)
                  : exit :=

    hide P, F in
    
        (
            BestMulticast[out, P, F](sender, msg, mbrL, UseChannel)
            |[P, F]|
            Counter[P, F](0 of Nat, 0 of Nat)
        )
        >>
        accept pass:Nat, fail:Nat in
            exit
            
    where
    
    process BestMulticast[out, P, F](sender:MID, msg:Msg, 
                          mbrL:MemberList, UseChannel: Bool): exit(Nat, Nat):=

      hide TimeOut in
      
        [mbrL eq NoMBR] ->   
             exit (any Nat, any Nat)

        []

        [mbrL ne NoMBR] ->
            (
                [UseChannel] -> 
                    (* Multicasts message to members on their appropriate
                       data channel *)
                  (
                    out !Top(mbrL) !sender !msg;
                      P;
                        BestMulticast[out, P, F](sender, msg, Tail(mbrL), UseChannel)
                    []
                    Timeout; 
                      F;
                        BestMulticast[out, P, F](sender, msg, Tail(mbrL), UseChannel)
                  )
                []
                [Not(UseChannel)] ->
                  (
                    (* Use request/ack channel *)
                    out !MID(Top(mbrl)) !GetAck(msg);
                      P;
                        BestMulticast[out, P, F](sender, msg, Tail(mbrL), UseChannel)
                    []
                    Timeout;
                      F;
                        BestMulticast[out, P, F](sender, msg, Tail(mbrL), UseChannel)
                  )
            )
                          
    endproc (* BestMulticast *)                          

    
    process Counter[P, F](pass:Nat, fail:Nat) : exit (Nat, Nat) :=
        
        P; Counter[P, F](succ(pass), fail)
        []
        F; Counter[P, F](pass, succ(fail))
        []
        exit(pass, fail)
        
    endproc (* Counter *)
        
    
endproc (* Multicast *)