(****************************************************************************)
(*                                                                          *)
(*      Group Communication Service, VERSION 2.02                           *)
(*      =========================================                           *)
(*                                                                          *)
(*      Daniel Amyot and Jacques Sincennes,                                 *)
(*      University of Ottawa,                                               *)
(*      Ver 2.02: June 9 - June 13, 1997                                    *)
(*      Ver 2.01: May 16 - May 18, 1997                                     *)
(*      Ver 2.00: April 18, 1997                                            *)
(*      Ver 1.15: January 24, 1997                                          *)
(*      Ver 1.14: January 14, 1997                                          *)
(*      Ver 1.13: August 15, 1996                                           *)
(*      Ver 1.12: July 8, 1996                                              *)
(*      Ver 1.0 : Spring 1996                                               *)
(*                                                                          *)
(*      Purpose:  Multicast messages to the members of a group.             *)
(*      =======                                                             *)
(*                                                                          *)
(*      Channels:                                                           *)
(*      ========                                                            *)
(*      mgcs_ch:  "Manager of Group Communication Servers" Channel (1)      *)
(*      gcs_ch:   Group Communication Server Channels (1 per group)         *)
(*      out_ch:   Output channels to distribute messages to group members   *)
(*                (1 per group)                                             *)
(*                                                                          *)
(*      Groups:                                                             *)
(*      ======                                                              *)
(*      - administered: Administrator alone creates and destroys group.     *)
(*                      Administrator can also change admin or moderator.   *)
(*                                                                          *)
(*      - moderated:    Moderator is the only one allowed to multicast.     *)
(*                      All other messages are forwarded to the moderator,  *)
(*                      by the group server, for approval.                  *)
(*                                                                          *)
(*      - public :      Anyone can register to a group (e.g. mailing lists) *)
(*      OR                                                                  *)
(*      - private:      Admin must register all new members. A user must be *)
(*                      member to see list of group members (e.g. telephone *)
(*                      conferences)                                        *)
(*                                                                          *)
(*      - opened:       Anyone can multicast to the group                   *)
(*                      (e.g. mailing lists)                                *)
(*      OR                                                                  *)
(*      - closed:       A user must be member of the group to multicast     *)
(*                      (e.g. Internet Relay Chat)                          *)
(*                                                                          *)
(****************************************************************************)

specification Group_Communication_Service[mgcs_ch, gcs_ch, out_ch]:noexit

library
    Boolean, NaturalNumber, HexDigit
endlib

(*=============================================*)
(*            IS8807 ADT definitions           *)
(*=============================================*)

(* Types FBoolean, Element, and Set contain corrections *)
(* to the library from the International Standard 8870  *)

type        FBoolean is
formalsorts FBool
formalopns  true        : -> FBool
            not         : FBool -> FBool
formaleqns
    forall  x : FBool
    ofsort  FBool
    not(not(x)) = x;
endtype     (* FBoolean *)

(*********************************************)

type        Element is FBoolean
formalsorts Element
formalopns  _eq_, _ne_          : Element, Element -> FBool
formaleqns
        forall  x, y, z : Element
        ofsort  Element
            x eq y = true =>
        x       = y             ;

        ofsort  FBool
            x = y =>
        x eq y  = true          ;
            x eq y =true , y eq z = true =>
        x eq z  = true          ;

        x ne y  = not(x eq y)   ;
endtype     (* Element *)

(*********************************************)

type    Set is Element, Boolean, NaturalNumber
sorts   Set
opns    {}                                      :               -> Set
        Insert, Remove                          : Element, Set  -> Set
        _IsIn_, _NotIn_                         : Element, Set  -> Bool
        _Union_, _Ints_, _Minus_                : Set, Set      -> Set
        _eq_, _ne_, _Includes_, _IsSubsetOf_    : Set, Set      -> Bool
        Card                                    : Set           -> Nat

eqns    forall  x, y    : Element,
                s, t    : Set
        ofsort  Set

            x IsIn Insert(y,s) =>
        Insert(x, Insert(y,s))  = Insert(y,s)           ;
        Remove(x, {})           = {}                    ;
        Remove(x, Insert(x,s))  = s                     ;
            x ne y = true of FBool =>
        Remove(x, Insert(y,s))  = Insert(y, Remove(x,s));

        {} Union s              = s                     ;
        Insert(x,s) Union t     = Insert(x,s Union t)   ;

        {} Ints s               = {}                    ;
            x IsIn t =>
        Insert(x,s) Ints t      = Insert(x,s Ints t)    ;
            x NotIn t =>
        Insert(x,s) Ints t      = s Ints t              ;

        s Minus {}              = s                     ;
        s Minus Insert(x, t)    = Remove(x,s) Minus t   ;

        ofsort  Bool

        x IsIn {}               = false                 ;
            x eq y = true of FBool =>
        x IsIn Insert(y,s)      = true                  ;
            x ne y = true of FBool =>
        x IsIn Insert(y,s)      = x IsIn s              ;
        x NotIn s               = not(x IsIn s)         ;

        s Includes {}           = true                  ;
        s Includes Insert(x,t)  = (x IsIn s) and (s Includes t)    ;

        s IsSubsetOf t          = t Includes s          ;

        s eq t                  = (s Includes t) and (t Includes s);

        s ne t                  = not(s eq t)           ;

        ofsort  Nat

        Card({})                = 0                     ;
            x NotIn s =>
        Card(Insert(x,s))       = Succ(Card(s))         ;
endtype (* Set *)


(*=============================================*)
(*             GCS ADT definitions             *)
(*=============================================*)

(* A group can be Administered or not, Moderated or not *)
(* Private or Public, Opened or Closed. We need four attributes. *)
type    GroupType is NaturalNumber
sorts   Attribute
opns
        Administered, NonAdministered,
        Moderated, NonModerated,
        Private, Public,
        Opened, Closed  :                      -> Attribute
        N               : Attribute            -> Nat
        _eq_, _ne_      : Attribute, Attribute -> Bool
eqns
        forall  at1, at2: Attribute

        ofsort Nat
        N(Administered)     = 0;
        N(NonAdministered)  = Succ(N(Administered));
        N(Moderated)        = Succ(N(NonAdministered));
        N(NonModerated)     = Succ(N(Moderated));
        N(Private)          = Succ(N(NonModerated));
        N(Public)           = Succ(N(Private));
        N(Opened)           = Succ(N(Public));
        N(Closed)           = Succ(N(Opened));

        ofsort Bool
        at1 eq at2 = N(at1) eq N(at2);
        at1 ne at2 = N(at1) ne N(at2);

endtype     (* GroupType *)

(*********************************************)

(* Generic ADT for identifiers and enumerations. *)
type    EnumType is NaturalNumber
sorts   Enum
opns
        (* Keep Elem0 for special purposes when necessary *)
        Elem0, Elem1, Elem2, Elem3, Elem4, Elem5 : -> Enum
        (* Mapping on Naturals, for comparison with other elements *)
        N            : Enum       -> Nat
        _eq_, _ne_   : Enum, Enum -> Bool
eqns
        forall  enum1, enum2: Enum

        ofsort Nat
        N(Elem0)  = 0;
        N(Elem1)  = Succ(N(Elem0));
        N(Elem2)  = Succ(N(Elem1));
        N(Elem3)  = Succ(N(Elem2));
        N(Elem4)  = Succ(N(Elem3));

        ofsort Bool
        enum1 eq enum2 = N(enum1) eq N(enum2);
        enum1 ne enum2 = N(enum1) ne N(enum2);
endtype (* EnumType *)

(*********************************************)

(* A group member (or any user) is identified by an member identifier. *)
type        MIDType is EnumType renamedby
sortnames   MID for Enum
opnnames
            Nobody for Elem0 (* Special MID reserved for admin/moder modif. *)
            User1  for Elem1
            User2  for Elem2
            User3  for Elem3
            User4  for Elem4
endtype (* MIDType *)

(*********************************************)

(* List of MIDs.  Used to answer "Members" requests *)
(* Implemented as a set. *)
(* We avoid the problem with ISLA's renaming in actualization *)
type            MIDListType0 is Set
actualizedby    MIDType using
sortnames
            MID for Element
            Bool  for FBool
endtype     (* MIDListType0 *)


type        MIDListType is MIDListType0 renamedby
sortnames
            MIDList for Set
opnnames
            Empty   for {}      (* Empty list of members *)
endtype     (* MIDListType *)

(*********************************************)

(* We define several Channel Identifiers (within a channel type) *)
(* Used to describe the specifics of the multicasting type (requestor's *)
(* host, IP, socket) according to group requirements *)
type        CIDType is EnumType renamedby
sortnames   CID for Enum
opnnames
            Chan5  for Elem0 (* No special CID reserved. *)
            Chan1  for Elem1
            Chan2  for Elem2
            Chan3  for Elem3
            Chan4  for Elem4
endtype (* CIDType *)

(*********************************************)

(* Set of pairs (member, channelID), to be registered in a group *)
type    MemberType is MIDType, CIDType
sorts   MBR
opns
        _._         : MID, CID      -> MBR
        MID         : MBR           -> MID
        CID         : MBR           -> CID
        _eq_, _ne_  : MBR, MBR      -> Bool
eqns
        forall  mid1, mid2: MID,
                cid1, cid2: CID,
                mbr1, mbr2: MBR

        ofsort MID
        MID(mid1.cid1)              = mid1;

        ofsort CID
        CID(mid1.cid1)              = cid1;

        ofsort Bool
        (mid1.cid1) eq (mid2.cid2)  = (mid1 eq mid2) and (cid1 eq cid2);

        mbr1 ne mbr2                = not(mbr1 eq mbr2);
endtype (* MemberType *)

(*********************************************)

(* Type for a list of member-channel pairs (implemented as a set) *)
(* We avoid the problem with ISLA's renaming in actualization *)
type            MemberListType0 is Set
actualizedby    MemberType using
sortnames
            MBR for Element
            Bool  for FBool
endtype     (* MemberType0 *)


type        MemberListType1 is MemberListType0 renamedby
sortnames
            MemberList for Set
opnnames
            NoMBR   for {}      (* Empty list of members *)
endtype     (* MemberListType1 *)


(* Additional operations needed to act like a list *)
type    MemberListType is MemberListType1, MIDListType
opns
        ErrorNoTop      :                   -> MBR
        ErrorNoTail     :                   -> MemberList
        Top             : MemberList        -> MBR
        Tail            : MemberList        -> MemberList

        (* The following functions act on the MID only. *)
        _IsIn_          : MID, MemberList   -> Bool
        _NotIn_         : MID, MemberList   -> Bool
        RemoveMBR       : MID, MemberList   -> MemberList
        MembersOnly     : MemberList        -> MIDList
eqns
        forall  member  : MBR,
                m       : MemberList,
                id1, id2: MID,
                chnl    : CID

        ofsort MBR
        Top (NoMBR)                 = ErrorNoTop;  (* Should not happen *)
        Top (Insert (member, m))    = member;

        ofsort MemberList
        Tail (NoMBR)                = ErrorNoTail; (* Should not happen *)
        Tail (Insert (member, m))   = m;

        RemoveMBR (id1, NoMBR)                  = NoMBR;
        RemoveMBR (id1, Insert(id1.chnl, m))    = m;
            id1 ne id2 = (true of Bool) =>
        RemoveMBR (id1, Insert(id2.chnl, m))    = Insert(id2.chnl,
                                                         RemoveMBR(id1, m));

        ofsort Bool
        id1 IsIn m                          = id1 IsIn MembersOnly(m);
        id1 NotIn m                         = not(id1 IsIn m);

        ofsort MIDList
        MembersOnly(NoMBR)                  = Empty;
        MembersOnly(Insert(id1.chnl, m))    = Insert(id1, MembersOnly(m));

endtype (* MemberListType *)

(*********************************************)

(* Several GCS IDentifiers *)
type        GIDType is EnumType renamedby
sortnames   GID for Enum
opnnames
            Group5  for Elem0 (* No special gID reserved. *)
            Group1  for Elem1
            Group2  for Elem2
            Group3  for Elem3
            Group4  for Elem4
endtype (* GIDType *)

(*********************************************)

(* List of channel multicasting types available *)
(* Others could be added. Those are only examples. *)
(* They do not really influence any behaviour here. *)
type        ChanType is EnumType renamedby
sortnames   Chan for Enum
opnnames
            Mail   for Elem0
            Socket for Elem1
            Text   for Elem2
            Audio  for Elem3
            Video  for Elem4
endtype (* ChanType *)

(* Indicate direction over bi-directional channels *)
type    DirectionType is
sorts   Direction
opns
        FromMGCS, ToMGCS,
        FromGCS, ToGCS      :   -> Direction
endtype (* DirectionType *)


(***************************************************************************)
(* A group contains characteristics and a list of members.                 *)
(* Characteristics are tuples (records):                                   *)
(*                  (ChannelType,       (of Chan)                          *)
(*                   Channel Identifier (of CID)                           *)
(*                   AdminAttribute,    (of Attribute)                     *)
(*                   Administrator,     (of MID)                           *)
(*                   OpenedAttribute,   (of Attribute)                     *)
(*                   PrivateAttribute,  (of Attribute)                     *)
(*                   ModerAttribute,    (of Attribute)                     *)
(*                   Moderator          (of MID) )                         *)
(*                                                                         *)
(* A "rationale" or "purpose" field could also be added (not shown here).  *)
(*                                                                         *)
(* Used in messages and in GCS databases.                                  *)
(***************************************************************************)

type    GCSinfoRecordType is GIDType, MemberListType, ChanType, GroupType
sorts   Msg
opns
        Encode      : Chan, CID, Attribute, MID, Attribute,
                      Attribute, Attribute, MID     -> Msg
        _eq_, _ne_  : Msg, Msg                      -> Bool
eqns
        forall  gcs1, gcs2  : Msg

        ofsort Bool
        gcs1 eq gcs2        = true;   (* Artificial eq needed by ISLA. *)
        gcs1 ne gcs2        = not(gcs1 eq gcs2); (* DO NOT USE!!! *)
endtype (* GCSinfoRecordType *)

(*********************************************)

(* List of Groups for Master GCS, implemented as a set. *)
(* We avoid the problem with ISLA's renaming in actualization *)
type            GroupListType0 is Set
actualizedby    GIDType using
sortnames
            GID for Element
            Bool  for FBool
endtype     (* GroupListType0 *)


type        GroupListType is GroupListType0 renamedby
sortnames
            GroupList for Set
opnnames
            NoGCS     for {}    (* Empty list of GCS *)
endtype     (* GroupListType *)

(*********************************************)

(* Request messages to be sent to the server *)
type        RequestType is HexDigit renamedby
sortnames   Request for HexDigit
opnnames
            CREATEGROUP     for 1
            GETATTRIBUTES   for 2
            DELETEGROUP     for 3
            REGISTER        for 4
            DEREGISTER      for 5
            MEMBERS         for 6
            GROUPS          for 7
            MULTICAST       for 8
            CHANGEADMIN     for 9
            CHANGEOPENATTR  for A
            CHANGEPRIVATTR  for B
            CHANGEMODER     for C
endtype     (* RequestType *)

(*********************************************)

(* Resulting acknowledgement and error messages from the server *)
type    AckErrorType is NaturalNumber, MIDListType, GCSinfoRecordType, GroupListType
sorts   AckError
opns
        (* Acknowledgements *)
        GROUPCREATED,
        GROUPDELETED,
        REGISTERED,
        DEREGISTERED,
        MESSAGESENT,
        ADMINCHANGED,
        MODERCHANGED,
        OPENATTRCHANGED,
        PRIVATTRCHANGED,
        SENTTOMODERATOR,
        GROUPWASDELETED,(* Multicast when a group is deleted *)

        (* Errors *)
        GROUPEXISTS,
        GROUPDOESNOTEXIST,
        MEMBERNOTINGROUP,
        NOTADMIN,
        NOTMODER,
        UNKNOWNREQUEST,
        NOADMINGROUP,
        NOMODERGROUP      : -> AckError

        (* Additional operation to encode lists of groups. *)
        GROUPSARE    : GroupList -> AckError
        (* Additional operation to encode lists of members. *)
        MEMBERSARE   : MIDList   -> AckError
        (* Additional operation to encode attributes. *)
        ATTRIBUTESARE: Msg       -> AckError

        (* Mapping on Naturals, for comparison with other AckError *)
        N            : AckError           -> Nat
        _eq_, _ne_   : AckError, AckError -> Bool
eqns
        forall  a1, a2: AckError, m: MIDList, g:GroupList, gi:Msg

        ofsort Nat
        N(GROUPCREATED)     = 0;
        N(GROUPDELETED)     = Succ(N(GROUPCREATED));
        N(REGISTERED)       = Succ(N(GROUPDELETED));
        N(DEREGISTERED)     = Succ(N(REGISTERED));
        N(MESSAGESENT)      = Succ(N(DEREGISTERED));
        N(ADMINCHANGED)     = Succ(N(MESSAGESENT));
        N(MODERCHANGED)     = Succ(N(ADMINCHANGED));
        N(OPENATTRCHANGED)  = Succ(N(MODERCHANGED));
        N(PRIVATTRCHANGED)  = Succ(N(OPENATTRCHANGED));
        N(SENTTOMODERATOR)  = Succ(N(PRIVATTRCHANGED));
        N(GROUPWASDELETED)  = Succ(N(SENTTOMODERATOR));
        N(GROUPEXISTS)      = Succ(N(GROUPWASDELETED));
        N(GROUPDOESNOTEXIST)= Succ(N(GROUPEXISTS));
        N(MEMBERNOTINGROUP) = Succ(N(GROUPDOESNOTEXIST));
        N(NOTADMIN)         = Succ(N(MEMBERNOTINGROUP));
        N(NOTMODER)         = Succ(N(NOTADMIN));
        N(UNKNOWNREQUEST)   = Succ(N(NOTMODER));
        N(NOADMINGROUP)     = Succ(N(UNKNOWNREQUEST));
        N(NOMODERGROUP)     = Succ(N(NOADMINGROUP));
        N(GROUPSARE(g))     = Succ(N(NOMODERGROUP));
        N(MEMBERSARE(m))    = Succ(Succ(N(NOMODERGROUP)));
        N(ATTRIBUTESARE(gi))= Succ(Succ(Succ(N(NOMODERGROUP))));

        ofsort Bool
        a1 eq a2    = N(a1) eq N(a2);
        a1 ne a2    = N(a1) ne N(a2);

endtype (* AckErrorType *)


(*********************************************)

(* Instances of messages that can be multicast (for readability). *)
(* A message type could be, for instance, a bit string. *)
type        InfoMsgType is EnumType renamedby
sortnames   InfoMsg for Enum
opnnames
            GroupIsDeleted  for Elem0 (* This one is necessary. *)
            Hello           for Elem1
            Salut           for Elem2
            GoodBye         for Elem3
            Packet          for Elem4
endtype (* InfoMsgType *)

(*********************************************)

(* Encoding/Decoding of messages *)
(* Several types of packets are needed. *)
type    MsgType is GCSinfoRecordType, RequestType, AckErrorType, InfoMsgType
opns
        (******************************************************************)
        (* No Message Packet.  Used for:                                  *)
        (*      Group deletion                                            *)
        (*      List members                                              *)
        (*      List groups                                               *)
        (*      Deregister (from public group)                            *)
        (******************************************************************)
        NoMsg   : -> Msg

        (******************************************************************)
        (* General Packet for Group Creation:                             *)
        (*       Channel Type    (of Chan)                                *)
        (*       ChanID          (of CID)                                 *)
        (*       AdminAttribute  (of Attribute)                           *)
        (*       Administrator   (of MID)                                 *)
        (*       OpenedAttribute (of Attribute)                           *)
        (*       PrivateAttribute(of Attribute)                           *)
        (*       ModerAttribute  (of Attribute)                           *)
        (*       Moderator       (of MID)                                 *)
        (******************************************************************)

        (* Encode  : Chan, CID, Attribute, MID, Attribute, Attribute,     *)
        (*           Attribute, MID                                -> Msg *)
        (* This packet is already defined in GCSinfoRecordType, as it     *)
        (* corresponds to the tuple that contains the GCS attributes.     *)

        (* Extraction Operations *)
        ChanType    : Msg                                      -> Chan
        ChanID      : Msg                                      -> CID
        IsAdmin     : Msg                                      -> Bool
        Admin       : Msg                                      -> MID
        IsOpened    : Msg                                      -> Bool
        IsPrivate   : Msg                                      -> Bool
        IsModerated : Msg                                      -> Bool
        Moderator   : Msg                                      -> MID

        (******************************************************************)
        (* Packet for Group Moderator modification:                       *)
        (*      Moderator       (of MID)                                  *)
        (*      ModerAttribute  (of Attribute)                            *)
        (******************************************************************)
        Encode      : MID, Attribute      -> Msg
        (* Modification Operations *)
        SetModer    : MID, Attribute, Msg -> Msg

        (******************************************************************)
        (* Packet for moderator approval:                                 *)
        (*      Sender     (of MID)                                       *)
        (*      Message    (of Msg)                                       *)
        (******************************************************************)
        ToApprove   : MID, Msg      -> AckError

        (******************************************************************)
        (* Packets for multicasting                                       *)
        (******************************************************************)
        Encode  : InfoMsg   -> Msg
        Encode  : AckError  -> Msg
        (* Modification Operations *)
        GetAck  : Msg       -> AckError
        GetInfo : Msg       -> InfoMsg

        (******************************************************************)
        (* Packet for subscription                                        *)
        (*      ChanID  (of CID)                                          *)
        (******************************************************************)
        Encode  : CID       -> Msg

        (******************************************************************)
        (* Packet for subscription by Administrator (for private groups)  *)
        (*      NewMember   (of MID)                                      *)
        (*      ChanID      (of CID)                                      *)
        (******************************************************************)
        Encode      : MID, CID  -> Msg
        NewMember   : Msg       -> MID

        (******************************************************************)
        (* Packet for unsubscription from private group                   *)
        (*      MemberID       (of MID)                                   *)
        (*                                                                *)
        (* Packet for Group Administrator modification:                   *)
        (*      Administrator  (of MID)                                   *)
        (******************************************************************)
        Encode  : MID                 -> Msg
        MemberID: Msg                 -> MID
        SetAdmin: MID, Attribute, Msg -> Msg

        (******************************************************************)
        (* Packet for modification of Opened attribute:                   *)
        (*      NewOpenAttr    (of Attribute)                             *)
        (*                                                                *)
        (* Packet for modification of Private attribute:                  *)
        (*      NewPrivAttr    (of Attribute)                             *)
        (******************************************************************)
        Encode    : Attribute        -> Msg
        SetOpened : Attribute, Msg   -> Msg
        SetPrivate: Attribute, Msg   -> Msg

eqns
        forall  msg                 : Msg,
                info                : InfoMsg,
                CT                  : Chan,
                ChID                : CID,
                Adm, NewAdm, Mem,
                Mod, NewMod, Sender : MID,
                AB, OB, PB, MB,
                NewAB, NewOB,
                NewPB, NewMB        : Attribute,
                ackerr              : AckError

        ofsort Chan
        ChanType(Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod))    = CT;

        ofsort CID
        ChanID(Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod))      = ChID;
        ChanID(Encode(ChID))                                    = ChID;
        ChanID(Encode(Mem, ChID))                               = ChID;

        ofsort Bool
        IsAdmin(Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod))
                                                        = AB eq Administered;
        IsOpened(Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod))
                                                        = OB eq Opened;
            IsOpened(Encode(OB))                        = OB eq Opened;
        IsPrivate(Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod))
                                                        = PB eq Private;
        IsPrivate(Encode(Adm, PB))                      = PB eq Private;
        IsPrivate(Encode(PB))                           = PB eq Private;
        IsModerated(Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod))
                                                        = MB eq Moderated;
        IsModerated(Encode(Mod, MB))                    = MB eq Moderated;

        ofsort MID
        Admin(Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod))       = Adm;
        Admin(Encode(Adm))                                      = Adm;
        Moderator(Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod))   = Mod;
        Moderator(Encode(Mod, MB))                              = Mod;
        NewMember(Encode(Mem, ChID))                            = Mem;
        MemberID(Encode(Mem))                                   = Mem;

        ofsort InfoMsg
        GetInfo(Encode(info))                                   = info;

        ofsort AckError
        GetAck(Encode(ackerr))                                  = ackerr;

        ofsort Msg
        SetAdmin(NewAdm, NewAB, Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod)) =
                        Encode(CT, ChID, NewAB, NewAdm, OB, PB, MB, Mod);
        SetOpened(NewOB, Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod)) =
                        Encode(CT, ChID, AB, Adm, NewOB, PB, MB, Mod);
        SetPrivate(NewPB, Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod)) =
                        Encode(CT, ChID, AB, Adm, OB, NewPB, MB, Mod);
        SetModer(NewMod, NewMB, Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod)) =
                        Encode(CT, ChID, AB, Adm, OB, PB, NewMB, NewMod);

        ofsort Nat
        (* Mapping for comparison with other Acks *)
        N(ToApprove(Sender, msg)) = Succ(Succ(Succ(Succ(N(NOMODERGROUP)))));

endtype (* MsgType *)

(*********************************************)

(***********************************************)
(*                                             *)
(* Buffering of requests and acknowledgements  *)
(*                                             *)
(* A generic type is created and actualized as *)
(* FIFO buffers for reqs and acks/errors.      *)
(*                                             *)
(***********************************************)

(* Generic FIFO type definition *)
type    FIFOType is Boolean
formalsorts
        Element

sorts   FIFO
opns
        Nothing :               -> FIFO
        Put     : Element, FIFO -> FIFO
        Get     : FIFO          -> Element
        Consume : FIFO          -> FIFO
        ErrorFIFO:              -> Element
        IsEmpty : FIFO          -> Bool
eqns
        forall f:FIFO, e, e2 :Element

        ofsort FIFO
        Consume(Nothing)            = Nothing;
        Consume(Put(e, Nothing))    = Nothing;
        Consume(Put(e2,Put(e,f)))   = Put(e2, Consume(Put(e, f)));
        ofsort Element
        Get(Nothing)                = ErrorFIFO;
        Get(Put(e, Nothing))        = e;
        Get(Put(e2, Put(e, f)))     = Get(Put(e, f));

        ofsort Bool
        IsEmpty(Nothing)            = true;
        IsEmpty(Put(e,f))           = false;
endtype (* FIFOType *)


(* Encoding of requests and acknowledgements as Records *)
type    BufferEncodingType is MIDType, AckErrorType, RequestType, MsgType
sorts   ReqRecord, AckErrorRecord
opns
        AckElem     : MID, AckError     -> AckErrorRecord
        ReqElem     : MID, Request, Msg -> ReqRecord

        S           : AckErrorRecord    -> MID      (* Extract Sender *)
        A           : AckErrorRecord    -> AckError (* Extract AckError *)
        S           : ReqRecord         -> MID      (* Extract Sender *)
        R           : ReqRecord         -> Request  (* Extract Request *)
        M           : ReqRecord         -> Msg      (* Extract Message *)
eqns
        forall S1:MID, A1:AckError, R1:Request, M1:Msg

        ofsort MID
        S(AckElem(S1, A1))      = S1;
        S(ReqElem(S1, R1, M1))  = S1;

        ofsort AckError
        A(AckElem(S1, A1))      = A1;

        ofsort Request
        R(ReqElem(S1, R1, M1))  = R1;

        ofsort Msg
        M(ReqElem(S1, R1, M1))  = M1;

endtype (* BufferEncodingType *)


(* Actualization (and renaming) of a Buffer type for records of requests *)
type            FIFOreqsType0 is FIFOType
actualizedby    BufferEncodingType using
sortnames
                ReqRecord for Element
endtype         (* FIFOreqsType0 *)

type        FIFOreqsType is FIFOreqsType0 renamedby
sortnames
            FIFOreqs for FIFO
opnnames
            NoReq    for Nothing
endtype     (* FIFOreqsType *)


(* Actualization (and renaming) of a Buffer type for records of acks *)
type            FIFOackerrsType0 is FIFOType
actualizedby    BufferEncodingType using
sortnames
                AckErrorRecord for Element
endtype         (* FIFOackerrsType0 *)

type        FIFOackerrsType is FIFOackerrsType0 renamedby
sortnames
            FIFOackerrs for FIFO
opnnames
            NoAckErr for Nothing
endtype     (* FIFOackerrsType *)

(*============================================*)
(*              Main behaviour                *)
(*============================================*)

behaviour

    Control_Team [mgcs_ch, gcs_ch, out_ch]

where

(*********************************************)
(*                                           *)
(*        Structure of Control Team          *)
(*                                           *)
(*********************************************)

process Control_Team [mgcs_ch, gcs_ch, out_ch] : noexit :=

    hide sgcs_ch, agcs_ch in (* Spawning and Administrative channels *)
    (
        MGCS[sgcs_ch, agcs_ch, mgcs_ch](NoGCS)           (* Management *)

        |[sgcs_ch, agcs_ch]|

        Spawn_GCS[sgcs_ch, agcs_ch, gcs_ch, out_ch]      (* GCS spawning *)
    )

endproc (* Control_Team *)


(***************************************************************************)
(*                                                                         *)
(*      Manager of Group Communication Servers (MGCS)                      *)
(*                                                                         *)
(*      Listens on the mgcs_ch channel for requests for:                   *)
(*          - the creation of a new Group Communication Server (GCS)       *)
(*          - the list of existing GCS                                     *)
(*      Uses sgcs_ch to:                                                   *)
(*          - spawn new groups                                             *)
(*      Uses agcs_ch to:                                                   *)
(*          - learn about the deletion of a group                          *)
(*                                                                         *)
(***************************************************************************)

process MGCS[sgcs_ch, agcs_ch, mgcs_ch](GCSlist:GroupList) :noexit:=

    (* Request for the creation of a new GCS *)
    (* the GID of the new group must not be used by an existing group *)

    mgcs_ch !ToMGCS ?caller:MID !CREATEGROUP ?newgroupid:GID ?infos:Msg;
    (
        [newgroupid IsIn GCSlist] ->
            mgcs_ch !FromMGCS !caller! GROUPEXISTS !newgroupid;
                (*_PROBE_*)
                MGCS[sgcs_ch, agcs_ch, mgcs_ch](GCSlist)
        []
        [newgroupid NotIn GCSlist] ->
            sgcs_ch !CREATEGROUP !newgroupid
                    !Insert(caller.ChanID(infos), NoMBR) ! infos;
                mgcs_ch !FromMGCS !caller !GROUPCREATED !newgroupid;
                    (*_PROBE_*)
                    MGCS[sgcs_ch, agcs_ch, mgcs_ch]
                                                (Insert(newgroupid, GCSlist))
    )

    []

    (* Request for the list of existing groups *)
    mgcs_ch !ToMGCS ?caller:MID !GROUPS;
        mgcs_ch !FromMGCS !caller !GROUPSARE(GCSlist);
            (*_PROBE_*)
            MGCS[sgcs_ch, agcs_ch, mgcs_ch](GCSlist)

    []

    (* Process destruction of a GCS. All verifications were done by the GCS *)
    (* Used to update the group list database *)
    [GCSlist ne NoGCS]->
        (* allowed only if there exists at least one group *)
        agcs_ch !GROUPDELETED ?id:GID;
            (*_PROBE_*)
            MGCS [sgcs_ch, agcs_ch, mgcs_ch](Remove(id, GCSlist))

endproc (* MGCS *)

(***************************************************************************)
(*                                                                         *)
(*      Spawn Group Communication Server                                   *)
(*                                                                         *)
(*      Creates a new GCS and forwards messages to it.                     *)
(*                                                                         *)
(***************************************************************************)

process Spawn_GCS[sgcs_ch, agcs_ch, gcs_ch, out_ch] :noexit:=

    sgcs_ch !CREATEGROUP ?id:GID ?mbrL:MemberList ?infos: Msg;
        (
            GCS_Team[agcs_ch, gcs_ch, out_ch] (id, mbrL, infos)
            |||
            Spawn_GCS[sgcs_ch, agcs_ch, gcs_ch, out_ch]
        )

endproc (* Spawn_GCS *)


(*****************************************)
(*                                       *)
(*        Structure of GCS Team          *)
(*                                       *)
(*****************************************)

process GCS_Team[agcs_ch, gcs_ch, out_ch]
                (id:GID, mbrL:MemberList, infos:Msg) : exit :=

    hide inter_ch in
        BiDirBuffer[agcs_ch, gcs_ch, inter_ch](id, false, NoReq, NoAckErr)
        |[inter_ch]|
        GCS[inter_ch, out_ch] (id, mbrL, infos)

endproc (* GCS_Team *)

(****************************************************************************)
(*                                                                          *)
(*      BiDirBuffer                                                         *)
(*                                                                          *)
(*      Routes messages for group ID from gcs_ch to inter_ch; ignores others*)
(*      Routes back acknowledgements to sender or to master.                *)
(*      Used for decoupling. Avoids waiting for all GCS to be ready for a   *)
(*      request to be processed. Increases concurrency.                     *)
(*                                                                          *)
(*      Requests and acknowledgements/errors are buffered.                  *)
(*      We use two infinite 2-way buffers that hold two ordered lists       *)
(*      (for acks/errors and requests).                                     *)
(*                                                                          *)
(****************************************************************************)

process BiDirBuffer[agcs_ch, gcs_ch, inter_ch](id:GID,
                                               terminated: Bool,
                                               bufreqs:FIFOreqs,
                                               bufackerrs:FIFOackerrs ):exit:=
    (* Buffer requests from senders. *)
    RequestBuffer[agcs_ch, gcs_ch, inter_ch](id,terminated,bufreqs,bufackerrs)

    []

    (* Buffer acks and errors from GCS. *)
    AckErrorBuffer[agcs_ch, gcs_ch, inter_ch](id,terminated,bufreqs,bufackerrs)

    []

    (* Terminate after everyone has been informed of a group deletion. *)
    (* Wait for Req and Ack buffers to be empty *)
    [IsEmpty(bufreqs) and IsEmpty(bufackerrs) and terminated] ->
        inter_ch ! ToGCS !GROUPDELETED;
            (*_PROBE_*)
            exit

    where

    process RequestBuffer[agcs_ch, gcs_ch, inter_ch](id:GID,
                                                     terminated: Bool,
                                                     bufreqs:FIFOreqs,
                                                     bufackerrs:FIFOackerrs)
                                                     :exit:=
        (* Buffer requests from senders. *)
        (* Refuse them if group is deleted (terminated) *)
        [not(terminated)] ->
            (
                gcs_ch !ToGCS ?sender:MID !id ?req:Request ?msg:Msg;
                    (*_PROBE_*)
                    BiDirBuffer[agcs_ch, gcs_ch, inter_ch](id, terminated,
                          Put(ReqElem(sender, req, msg), bufreqs), bufackerrs)
            )

        []

        (* Forward buffered requests to GCS *)
        [not(IsEmpty(bufreqs))] ->
            (
                inter_ch !ToGCS !S(Get(bufreqs)) !R(Get(bufreqs))
                                                 !M(Get(bufreqs));
                    (*_PROBE_*)
                    BiDirBuffer[agcs_ch, gcs_ch, inter_ch](id, terminated,
                                Consume(bufreqs), bufackerrs)
            )

    endproc (* RequestBuffer *)


    process AckErrorBuffer[agcs_ch, gcs_ch, inter_ch](id:GID,
                                                      terminated: Bool,
                                                      bufreqs:FIFOreqs,
                                                      bufackerrs:FIFOackerrs )
                                                      :exit:=
        (* Buffer acks from GCS. *)
        inter_ch !FromGCS ?sender:MID ?ackerr:AckError;
            (*_PROBE_*)
            BiDirBuffer[agcs_ch, gcs_ch, inter_ch](id, terminated,
                        bufreqs, Put(AckElem(sender, ackerr), bufackerrs))

        []

        (* Forward buffered acks to senders *)
        [not(IsEmpty(bufackerrs))] ->
            (
                [A(Get(bufackerrs)) eq GROUPDELETED] ->
                    (* Intercept this special case of ack. *)
                    (* Inform MGCS of deletion, for database update. *)
                    agcs_ch ! GROUPDELETED ! id;
                       (* Forward ack to sender, empty the request buffer, *)
                       (* and terminate listening. We could add a process *)
                       (* that would tell the senders of these buffered *)
                       (* requests that the goup was deleted... *)
                        gcs_ch !FromGCS !S(Get(bufackerrs)) !A(Get(bufackerrs))
                                                             of AckError !id;
                            (*_PROBE_*)
                            BiDirBuffer[agcs_ch, gcs_ch, inter_ch](id,
                                         true, NoReq, Consume(bufackerrs))

                []

                [A(Get(bufackerrs)) ne GROUPDELETED] ->
                    (* Forward ack to sender but don't empty the req buffer *)
                    gcs_ch !FromGCS !S(Get(bufackerrs)) !A(Get(bufackerrs))
                                                         of AckError !id;
                        (*_PROBE_*)
                        BiDirBuffer[agcs_ch, gcs_ch, inter_ch](id, terminated,
                                    bufreqs, Consume(bufackerrs))
            )

    endproc (* AckErrorBuffer *)

endproc (* BiDirBuffer *)


(****************************************************************************)
(*                                                                          *)
(*      Group Communication Server (GCS)                                    *)
(*                                                                          *)
(*      inter_ch: to communicate with sender and master (for administration)*)
(*      out_ch:   to multicast messages to members                          *)
(*                                                                          *)
(*      Receives requests on inter_ch with event structure:                 *)
(*                  !MID !Request !Msg                                      *)
(*      Gives acknowledgements with event structure:                        *)
(*                  !MID !AckError                                          *)
(*                                                                          *)
(****************************************************************************)


process GCS[inter_ch, out_ch](id:GID, mbrL:MemberList, infos:Msg) :exit:=

    (* gets the request from the sender *)
    inter_ch !ToGCS ?sender:MID ?req:Request ?msg:Msg [sender ne Nobody];
    (
        (* get the GCS attributes (infos) *)
        [req eq GETATTRIBUTES] ->
            Req_GetAttributes[inter_ch, out_ch](sender, msg, id, mbrL, infos)
        []
        (* group deletion *)
        [req eq DELETEGROUP] ->
            Req_DeleteGroup[inter_ch, out_ch](sender, msg, id, mbrL, infos)
        []
        (* registration *)
        [req eq REGISTER] ->
            Req_Register[inter_ch, out_ch](sender, msg, id, mbrL, infos)
        []
        (* provides the list of group members *)
        [req eq MEMBERS] ->
            Req_Members[inter_ch, out_ch](sender, msg, id, mbrL, infos)
        []
        (* deregistration *)
        [req eq DEREGISTER] ->
            Req_DeRegister[inter_ch, out_ch](sender, msg, id, mbrL, infos)
        []
        (* multicast messages; will block until successful *)
        [req eq MULTICAST] ->
            Req_Multicast[inter_ch, out_ch](sender, msg, id, mbrL, infos)
        []
        (* change the administrator and the Administered attribute *)
        [req eq CHANGEADMIN] ->
            Req_ChangeAdmin[inter_ch, out_ch](sender, msg, id, mbrL, infos)
        []
        (* change the Opened attribute *)
        [req eq CHANGEOPENATTR] ->
            Req_ChangeOpenAttr[inter_ch, out_ch](sender, msg, id, mbrL, infos)
        []
        (* change the Private attribute *)
        [req eq CHANGEPRIVATTR] ->
            Req_ChangePrivAttr[inter_ch, out_ch](sender, msg, id, mbrL, infos)
        []
        (* change the moderator and the Moderated attribute *)
        [req eq CHANGEMODER] ->
            Req_ChangeModer[inter_ch, out_ch](sender, msg, id, mbrL, infos)
    )

    where

    process Req_GetAttributes[inter_ch, out_ch](sender: MID, msg: Msg, id:GID,
                                          mbrL:MemberList, infos:Msg) :exit:=

        [not(IsAdmin(infos)) or (Admin(infos) eq sender)] ->
        (* Either NonAdministered, or sender is administrator *)
            (
                inter_ch !FromGCS !sender !ATTRIBUTESARE(infos);
                    (*_PROBE_*)
                    GCS[inter_ch, out_ch](id, mbrL, infos)
            )
        []
        [(IsAdmin(infos) and (Admin(infos) ne sender))] ->
        (* Administered group, and sender is not the administrator *)
            (
                inter_ch !FromGCS !sender !NOTADMIN;
                    (*_PROBE_*)
                    GCS[inter_ch, out_ch](id, mbrL, infos)
            )

    endproc (* Req_GetAttributes *)


    process Req_DeleteGroup[inter_ch, out_ch](sender: MID, msg: Msg, id:GID,
                                          mbrL:MemberList, infos:Msg) :exit:=

        [IsAdmin(infos) and (Admin(infos) eq sender)] ->
        (* Administered group, and sender is the administrator *)
            (
                (* Inform members other than sender *)
                Multicast[inter_ch](sender,Encode(GROUPWASDELETED),
                                    RemoveMBR(sender, mbrL), false)>>
                    inter_ch !FromGCS !sender !GROUPDELETED;
                         inter_ch !ToGCS !GROUPDELETED;
                             (*_PROBE_*)
                             exit
            )
        []
        [IsAdmin(infos) and (Admin(infos) ne sender)] ->
        (* Administered group, and sender is not the administrator *)
            inter_ch !FromGCS !sender !NOTADMIN;
                (*_PROBE_*)
                GCS[inter_ch, out_ch](id, mbrL, infos)
        []
        (* Non administered group *)
        [not(IsAdmin(infos))] ->
            inter_ch !FromGCS !sender !NOADMINGROUP;
                (*_PROBE_*)
                GCS[inter_ch, out_ch](id, mbrL, infos)

    endproc (* Req_DeleteGroup *)


    process Req_Register[inter_ch, out_ch](sender: MID, msg: Msg, id:GID,
                                           mbrL:MemberList, infos:Msg) :exit:=

        [not(IsPrivate(infos))] ->
        (* Register only if group is public *)
            inter_ch !FromGCS !sender !REGISTERED;
            (
                [sender NotIn MembersOnly(mbrL)] ->
                    (* Insert pair MID.CID *)
                    (*_PROBE_*)
                    GCS[inter_ch, out_ch]
                       (id, Insert(sender.ChanID(msg), mbrL), infos)
                []

                [sender IsIn MembersOnly(mbrL)] ->
                    (* Modify CID only *)
                    (*_PROBE_*)
                    GCS[inter_ch, out_ch]
                        (id, Insert(sender.ChanID(msg),
                                    RemoveMBR(sender,mbrL)), infos)
            )
        []
        [IsPrivate(infos)] ->
        (
            [sender ne Admin(infos)] ->
            (* Cannot register; group is private *)
                inter_ch !FromGCS !sender !NOTADMIN;
                    (*_PROBE_*)
                    GCS[inter_ch, out_ch](id, mbrL, infos)
            []
            [sender eq Admin(infos)] ->
            (* Admin can register another member in private group *)
                inter_ch !FromGCS !sender !REGISTERED;
                (
                    [NewMember(msg) NotIn MembersOnly(mbrL)] ->
                       (* Insert pair MID.CID *)
                        (*_PROBE_*)
                        GCS[inter_ch, out_ch]
                            (id, Insert(NewMember(msg).ChanID(msg),
                                        mbrL), infos)
                    []
                    [NewMember(msg) IsIn MembersOnly(mbrL)] ->
                        (* Modify CID only *)
                        (*_PROBE_*)
                        GCS[inter_ch, out_ch]
                            (id, Insert(NewMember(msg).ChanID(msg),
                             RemoveMBR(NewMember(msg),mbrL)), infos)
                )
        )

    endproc (* Req_Register *)


    process Req_Members[inter_ch, out_ch](sender: MID, msg: Msg, id:GID,
                                          mbrL:MemberList, infos:Msg) :exit:=

        (* Check whether group is private *)
        [not(IsPrivate(infos)) or
            (IsPrivate(infos) and (sender IsIn MembersOnly(mbrL)))] ->
            inter_ch !FromGCS !sender !MEMBERSARE(MembersOnly(mbrL));
                (*_PROBE_*)
                GCS[inter_ch, out_ch](id, mbrL, infos)
        []
        [IsPrivate(infos) and (sender NotIn MembersOnly(mbrL))] ->
            inter_ch !FromGCS !sender !MEMBERNOTINGROUP;
                (*_PROBE_*)
                GCS[inter_ch, out_ch](id, mbrL, infos)

    endproc (* Req_Members *)


    process Req_DeRegister[inter_ch, out_ch](sender: MID, msg: Msg, id:GID,
                                           mbrL:MemberList, infos:Msg) :exit:=

        [not(IsAdmin(infos)) or (sender ne Admin(infos))] ->
         (* When group is not administered, DeRegister only if member is in *)
         (* group. Same idea when administered and sender is not admin.     *)
            (
                [sender NotIn MembersOnly(mbrL)] ->
                    inter_ch !FromGCS !sender !MEMBERNOTINGROUP;
                        (*_PROBE_*)
                        GCS[inter_ch, out_ch](id, mbrL, infos)

                []

                [sender IsIn MembersOnly(mbrL)] ->
                    inter_ch !FromGCS !sender !DEREGISTERED;
                    (
                        [Card(mbrL) eq Succ(0)] ->
                            (* The GCS dies if no member left *)
                            (* We do not need to inform the members... *)
                                inter_ch !FromGCS !sender !GROUPDELETED;
                                    inter_ch !ToGCS !GROUPDELETED;
                                        (*_PROBE_*)
                                        exit
                        []
                        [Card(mbrL) ne Succ(0)] ->
                            (*_PROBE_*)
                            GCS[inter_ch, out_ch]
                               (id, RemoveMBR(sender, mbrL), infos)
                    )
            )
        []
        [IsAdmin(infos) and (sender eq Admin(infos))] ->
        (* When group is administered and the sender is the administrator, *)
        (* DeRegister the member named by the admin. *)
            (
                [MemberID(msg) IsIn MembersOnly(mbrL)] ->
                    inter_ch !FromGCS !sender !DEREGISTERED;
                    (
                        [Card(mbrL) eq Succ(0)] ->
                            (* The GCS dies if no member left *)
                            (* We do not need to inform the members... *)
                                inter_ch !FromGCS !sender !GROUPDELETED;
                                    inter_ch !ToGCS !GROUPDELETED;
                                        (*_PROBE_*)
                                        exit
                        []
                        [Card(mbrL) ne Succ(0)] ->
                            (*_PROBE_*)
                            GCS[inter_ch, out_ch]
                               (id, RemoveMBR(MemberID(msg), mbrL), infos)
                    )
                []
                [MemberID(msg) NotIn MembersOnly(mbrL)] ->
                    inter_ch !FromGCS !sender !MEMBERNOTINGROUP;
                        (*_PROBE_*)
                        GCS[inter_ch, out_ch](id, mbrL, infos)
            )

    endproc (* Req_DeRegister *)


   process Req_Multicast[inter_ch, out_ch](sender: MID, msg: Msg, id:GID,
                                           mbrL:MemberList, infos:Msg) :exit:=

    (* Is the group Opened, or is the sender a member of the group? *)
    [IsOpened(infos) or
     (not(IsOpened(infos)) and (sender IsIn MembersOnly(mbrL)))] ->
        (
            (* Not moderated, or sender is moderator *)
            [not(IsModerated(infos)) or (sender eq Moderator(infos))] ->
                (
                    Multicast[out_ch](sender, msg, mbrL, true) >>
                        inter_ch !FromGCS !sender !MESSAGESENT;
                            (*_PROBE_*)
                            GCS[inter_ch, out_ch](id, mbrL, infos)
                )
            []
            (* Moderated, and sender is not moderator. *)
            (* Forward to group moderator only, for approval *)
            [IsModerated(infos) and (sender ne Moderator(infos))] ->
                (
                    inter_ch !FromGCS !Moderator(infos) !ToApprove(sender,msg);
                        inter_ch !FromGCS !sender !SENTTOMODERATOR;
                            (*_PROBE_*)
                            GCS[inter_ch, out_ch](id, mbrL, infos)
                )
        )
    []
    [not(IsOpened(infos)) and (sender NotIn MembersOnly(mbrL))]->
        (
            inter_ch !FromGCS !sender !MEMBERNOTINGROUP;
                (*_PROBE_*)
                GCS[inter_ch, out_ch](id, mbrL, infos)
        )

    endproc (* Req_Multicast *)


    process Req_ChangeAdmin[inter_ch, out_ch](sender: MID, msg: Msg, id:GID,
                                           mbrL:MemberList, infos:Msg) :exit:=

        (* The sender has the privilege. *)
        [IsAdmin(infos) and (Admin(infos) eq sender)] ->
            (
                [Admin(msg) IsIn mbrL] ->
                    inter_ch !FromGCS !sender !ADMINCHANGED;
                        (*_PROBE_*)
                        GCS[inter_ch, out_ch]
                           (id, mbrL, SetAdmin(Admin(msg),Administered, infos))
                []
                [Admin(msg) eq Nobody] ->
                    (* If it's Nobody, then set the group to NonAdministered *)
                    inter_ch !FromGCS !sender !ADMINCHANGED;
                        (*_PROBE_*)
                        GCS[inter_ch, out_ch]
                           (id, mbrL, SetAdmin(Nobody, NonAdministered, infos))
                []
                [(Admin(msg) NotIn mbrL) and (Admin(msg) ne Nobody)] ->
                    inter_ch !FromGCS !sender !MEMBERNOTINGROUP;
                        (*_PROBE_*)
                        GCS[inter_ch, out_ch](id, mbrL, infos)
            )
        []
        (* The sender does not have the privilege to change the admin *)
        [IsAdmin(infos) and (Admin(infos) ne sender)] ->
            inter_ch !FromGCS !sender !NOTADMIN;
                (*_PROBE_*)
                GCS[inter_ch, out_ch](id, mbrL, infos)
        []
        (* The group does not have an administrator *)
        [not(IsAdmin(infos))] ->
            inter_ch !FromGCS !sender !NOADMINGROUP;
                (*_PROBE_*)
                GCS[inter_ch, out_ch](id, mbrL, infos)

    endproc (* Req_ChangeAdmin *)


    process Req_ChangeOpenAttr[inter_ch, out_ch](sender: MID, msg: Msg, id:GID,
                                          mbrL:MemberList, infos:Msg) :exit:=

        [IsAdmin(infos) and (Admin(infos) eq sender)] ->
        (* Administered group, and sender is the administrator *)
            (
                inter_ch !FromGCS !sender !OPENATTRCHANGED;
                (
                    [IsOpened(msg)]->
                        (*_PROBE_*)
                        GCS[inter_ch, out_ch](id,mbrL,SetOpened(Opened, infos))
                    []
                    [not(IsOpened(msg))]->
                        (*_PROBE_*)
                        GCS[inter_ch, out_ch](id,mbrL,SetOpened(Closed, infos))
                )
            )
        []
        [IsAdmin(infos) and (Admin(infos) ne sender)] ->
        (* Administered group, and sender is not the administrator *)
            (
                inter_ch !FromGCS !sender !NOTADMIN;
                    (*_PROBE_*)
                    GCS[inter_ch, out_ch](id, mbrL, infos)
            )
        []
        [not(IsAdmin(infos))] ->
        (* NonAdministered group *)
            (
                inter_ch !FromGCS !sender !NOADMINGROUP;
                    (*_PROBE_*)
                    GCS[inter_ch, out_ch](id, mbrL, infos)
            )

    endproc (* Req_ChangeOpenAttr *)


    process Req_ChangePrivAttr[inter_ch, out_ch](sender: MID, msg: Msg, id:GID,
                                          mbrL:MemberList, infos:Msg) :exit:=

        [IsAdmin(infos) and (Admin(infos) eq sender)] ->
        (* Administered group, and sender is the administrator *)
            (
                inter_ch !FromGCS !sender !PRIVATTRCHANGED;
                (
                    [IsPrivate(msg)]->
                        (*_PROBE_*)
                        GCS[inter_ch, out_ch](id, mbrL,
                                              SetPrivate(Private, infos))
                    []
                    [not(IsPrivate(msg))]->
                        (*_PROBE_*)
                        GCS[inter_ch, out_ch](id, mbrL,
                                              SetPrivate(Public, infos))
                )
            )
        []
        [IsAdmin(infos) and (Admin(infos) ne sender)] ->
        (* Administered group, and sender is not the administrator *)
            (
                inter_ch !FromGCS !sender !NOTADMIN;
                    (*_PROBE_*)
                    GCS[inter_ch, out_ch](id, mbrL, infos)
            )
        []
        [not(IsAdmin(infos))] ->
        (* NonAdministered group *)
            (
                inter_ch !FromGCS !sender !NOADMINGROUP;
                    (*_PROBE_*)
                    GCS[inter_ch, out_ch](id, mbrL, infos)
            )

    endproc (* Req_ChangePrivAttr *)


    process Req_ChangeModer[inter_ch, out_ch](sender: MID, msg: Msg, id:GID,
                                           mbrL:MemberList, infos:Msg) :exit:=

        (* The sender has the privilege. *)
        [(IsModerated(infos) and (Moderator(infos) eq sender)) or
         (IsAdmin(infos) and (Admin(infos) eq sender))] ->
            (
              [Moderator(msg) ne Nobody]->
                (
                  [IsOpened(infos) or (Moderator(msg) IsIn mbrL)] ->
                      inter_ch !FromGCS !sender !MODERCHANGED;
                      (
                          [IsModerated(msg)]->
                              (*_PROBE_*)
                              GCS[inter_ch, out_ch]
                                 (id, mbrL, SetModer(Moderator(msg),
                                                     Moderated, infos))
                          []
                          [not(IsModerated(msg))]->
                              (*_PROBE_*)
                              (* Put Nobody as new moderator *)
                              GCS[inter_ch, out_ch]
                                 (id, mbrL, SetModer(Nobody,
                                                     NonModerated, infos))
                      )
                  []
                  (* If the group is closed, *)
                  (* then moderator must be a group member *)
                  [not(IsOpened(infos)) and (Moderator(msg) NotIn mbrL)] ->
                      inter_ch !FromGCS !sender !MEMBERNOTINGROUP;
                          (*_PROBE_*)
                          GCS[inter_ch, out_ch](id, mbrL, infos)
                )
              []
              [Moderator(msg) eq Nobody]->
                  (* Special case where the group becomes NonModerated, *)
                  (* whatever the value of the new attribute *)
                  (
                      inter_ch !FromGCS !sender !MODERCHANGED;
                          (*_PROBE_*)
                          GCS[inter_ch, out_ch]
                             (id, mbrL, SetModer(Nobody,
                                                 NonModerated, infos))
                  )
            )
        []
        (* The sender does not have the privilege to change moder *)
        (* (neither admin, nor moderator)*)
        [(IsModerated(infos) and (Moderator(infos) ne sender)) and
         ( (IsAdmin(infos) and (Admin(infos) ne sender)) or
           not(IsAdmin(infos)) )] ->
                inter_ch !FromGCS !sender !NOTMODER;
                    (*_PROBE_*)
                    GCS[inter_ch, out_ch](id, mbrL, infos)
        []
        (* The group does not have a moderator *)
        (* (and the sender is not admin) *)
        [not(IsModerated(infos)) and
         not(IsAdmin(infos) and (Admin(infos) eq sender))] ->
            inter_ch !FromGCS !sender !NOMODERGROUP;
                (*_PROBE_*)
                GCS[inter_ch, out_ch](id, mbrL, infos)

    endproc (* Req_ChangeModer *)

endproc (* GCS *)


(***************************************************************************)
(*                                                                         *)
(*      Multicast                                                          *)
(*                                                                         *)
(*      Send the message to all subscribers of the group (concurrently).   *)
(*      No other message will be multicast until the first one is sent to  *)
(*      all members of the group.                                          *)
(*                                                                         *)
(***************************************************************************)

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

    [mbrL eq NoMBR] ->
         (*_PROBE_*)
         exit

    []

    [mbrL ne NoMBR] ->
        (
            (
                [UseChannel] ->
                    (
                        (* Multicasts message to members on their *)
                        (* appropriate data channel, concurrently *)
                        out !Top(mbrL) !sender !msg;
                            (*_PROBE_*)
                            exit
                        |||
                        (* loop... *)
                        (*_PROBE_*)
                        Multicast[out](sender, msg, Tail(mbrL), UseChannel)
                    )
                []
                [not(UseChannel)] ->
                    (* Use request/AckError channel, sequentially *)
                    (* (for group deletion) *)
                    out !FromGCS !MID(Top(mbrL)) !GetAck(msg);
                        (*_PROBE_*)
                        Multicast[out](sender, msg, Tail(mbrL), UseChannel)
            )
        )

endproc (* Multicast *)


(*============================================*)
(*           UCM-based Test Cases             *)
(*============================================*)

(***************************************************************************)
(*                                                                         *)
(*      Group Creation                                                     *)
(*                                                                         *)
(***************************************************************************)


(* Acceptance test : Checks group creation (3 tests) *)
process Test_1 [mgcs_ch, gcs_ch, success]:noexit :=

    (* Creates from empty GCS list *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    success; stop

    []

    (* Creates two different groups *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    mgcs_ch !ToMGCS !User2 !CREATEGROUP !Group2 !Encode(Video, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User2 !GROUPCREATED !Group2;
    success; stop

    []

    (* Uses twice the same GID *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    mgcs_ch !ToMGCS !User2 !CREATEGROUP !Group1 !Encode(Video, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User2 !GROUPEXISTS !Group1;
    success; stop

endproc (* Test_1: TestUCMcreationA *)


(* Rejection test : Checks group creation (2 tests) *)
process Test_2 [mgcs_ch, reject]:noexit :=

    (* Can't create from empty GCS list *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 ?reqack:AckError !Group1 [reqack ne GROUPCREATED];
    reject; stop

    []

    (* Uses twice the same GID *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    mgcs_ch !ToMGCS !User2 !CREATEGROUP !Group1 !Encode(Video, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User2 ?reqerr:AckError !Group1 [reqerr ne GROUPEXISTS];
    reject; stop

endproc (* Test_2: TestUCMcreationR *)



(***************************************************************************)
(*                                                                         *)
(*      List of Groups                                                     *)
(*                                                                         *)
(***************************************************************************)

(* Assumes that Creation request is operational. *)

(* Acceptance test : Checks list of groups (3 tests) *)
process Test_3 [mgcs_ch, success]:noexit :=

    (* Checks empty GCS list when starting MGCS *)
    mgcs_ch !ToMGCS !User1 !GROUPS;
    mgcs_ch !FromMGCS !User1 !GROUPSARE(NoGCS);
    success; stop

    []

    (* 1 group in list *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    mgcs_ch !ToMGCS !User1 !GROUPS;
    mgcs_ch !FromMGCS !User1 !GROUPSARE(Insert(Group1, NoGCS));
    success; stop

    []

    (* 2 groups in list *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    mgcs_ch !ToMGCS !User2 !CREATEGROUP !Group2 !Encode(Video, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User2 !GROUPCREATED !Group2;
    mgcs_ch !ToMGCS !User1 !GROUPS;
    mgcs_ch !FromMGCS !User1 !GROUPSARE(Insert(Group2, Insert(Group1, NoGCS)));
    success; stop

endproc (* Test_3: TestUCMgrouplistA *)


(* Rejection test : Checks list of groups (3 tests) *)
process Test_4 [mgcs_ch, reject]:noexit :=

    (* Checks empty GCS list when starting MGCS *)
    mgcs_ch !ToMGCS !User1 !GROUPS;
    mgcs_ch !FromMGCS !User1 ?thelist:AckError [thelist ne GROUPSARE(NoGCS)];
    reject; stop

    []
    (* 1 group in list *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    mgcs_ch !ToMGCS !User1 !GROUPS;
    mgcs_ch !FromMGCS !User1 ?thelist:AckError
                              [thelist ne GROUPSARE(Insert(Group1, NoGCS))];
    reject; stop

    []

    (* 2 groups in list *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    mgcs_ch !ToMGCS !User2 !CREATEGROUP !Group2 !Encode(Video, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User2 !GROUPCREATED !Group2;
    mgcs_ch !ToMGCS !User3 !GROUPS;
    mgcs_ch !FromMGCS !User3 ?thelist:AckError
                [thelist ne GROUPSARE(Insert(Group2, Insert(Group1, NoGCS)))];
    reject; stop

endproc (* Test_4: TestUCMgrouplistR *)

(***************************************************************************)
(*                                                                         *)
(*      Attributes Checking                                                *)
(*                                                                         *)
(***************************************************************************)

(* Assumes that Creation is operational. *)

(* Acceptance test : Checks the attributes of a group (3 tests) *)
process Test_5 [mgcs_ch, gcs_ch, success]:noexit :=

    (* Non-administered group, anyone can get the attributes *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User2 !ATTRIBUTESARE(Encode(Mail, Chan3,NonAdministered,
                      Nobody, Opened, Public, NonModerated, Nobody)) !Group4;
    success; stop

    []

    (* Administered group, request by admin *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Closed, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User3 !ATTRIBUTESARE(Encode(Mail, Chan3, Administered,
                       User3, Closed, Private, NonModerated, Nobody)) !Group4;
    success; stop

    []

    (* Administered, not by admin. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User2 !NOTADMIN !Group4;
    success; stop

endproc (* Test_5: TestUCMattrA *)


(* Rejection test : Checks the attributes of a group (3 tests) *)
process Test_6 [mgcs_ch, gcs_ch, reject]:noexit :=

    (* Non-administered group, anyone can get the attributes *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User2 ?reqack:AckError !Group4
           [reqack ne ATTRIBUTESARE(Encode(Mail, Chan3, NonAdministered,
                              Nobody, Opened, Public, NonModerated, Nobody))];
    reject; stop

    []

    (* Administered group, request by admin *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Closed, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4
           [reqack ne ATTRIBUTESARE(Encode(Mail, Chan3, Administered, User3,
                                     Closed, Private, NonModerated, Nobody))];
    reject; stop

    []

    (* Administered, not by admin. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User2 ?reqack:AckError !Group4 [reqack ne NOTADMIN];
    reject; stop

endproc (* Test_6: TestUCMattrR *)


(***************************************************************************)
(*                                                                         *)
(*      Member Registration                                                *)
(*                                                                         *)
(***************************************************************************)

(* Assumes that Creation request is operational. *)

(* Acceptance test : Checks member registration within a group (6 tests) *)
process Test_7 [mgcs_ch, gcs_ch, out_ch, success]:noexit :=

    (* 1 member in group (creator) *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Video, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User2 !Group1 !REGISTER !Encode(Chan3);
    gcs_ch !FromGCS !User2 !REGISTERED !Group1;
    success; stop

    []

    (* 2 new members in public group *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User2 !Group1 !REGISTER !Encode(Chan2);
    gcs_ch !FromGCS !User2 !REGISTERED !Group1;
    gcs_ch !ToGCS !User3 !Group1 !REGISTER !Encode(Chan3);
    gcs_ch !FromGCS !User3 !REGISTERED !Group1;
    success; stop

    []

    (* 1 new member in private, administered group, by admin *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             Administered, User1, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User1 !Group1 !REGISTER !Encode(User2, Chan2);
    gcs_ch !FromGCS !User1 !REGISTERED !Group1;
    success; stop

    []

    (* 1 new member in private, administered group, not by admin *)
    (* (self and 3rd party) *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             Administered, User1, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User2 !Group1 !REGISTER !Encode(Chan2);
    gcs_ch !FromGCS !User2 !NOTADMIN !Group1;
    gcs_ch !ToGCS !User2 !Group1 !REGISTER !Encode(User3, Chan3);
    gcs_ch !FromGCS !User2 !NOTADMIN !Group1;
    success; stop

    []

    (* Change the CID of a member in a non-administered group *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User1 !Group1 !REGISTER !Encode(Chan2);
    gcs_ch !FromGCS !User1 !REGISTERED !Group1;
    (* Verification *)
    gcs_ch !ToGCS !User1 !Group1 !MULTICAST !Encode(Hello);
    out_ch !User1.Chan2 !User1 !Encode(Hello);
    gcs_ch !FromGCS !User1 !MESSAGESENT !Group1;
    success; stop

    []

    (* Change the CID of a member in an administered private group *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan4,
             Administered, User1, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User1 !Group1 !REGISTER !Encode(User2, Chan3);
    gcs_ch !FromGCS !User1 !REGISTERED !Group1;
    gcs_ch !ToGCS !User1 !Group1 !REGISTER !Encode(User2, Chan1);
    gcs_ch !FromGCS !User1 !REGISTERED !Group1;
    (* Verification *)
    gcs_ch !ToGCS !User1 !Group1 !MULTICAST !Encode(Hello);
    out_ch !User1.Chan4 !User1 !Encode(Hello); (* Any order... *)
    out_ch !User2.Chan1 !User1 !Encode(Hello);
    gcs_ch !FromGCS !User1 !MESSAGESENT !Group1;
    success; stop

endproc (* Test_7: TestUCMmembersA *)


(* Rejection test : Checks member registration within a group (4 tests) *)
process Test_8 [mgcs_ch, gcs_ch, out_ch, reject]:noexit :=

    (* 1 new member in public group *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User2 !Group1 !REGISTER !Encode(Chan1);
    gcs_ch !FromGCS !User2 ?reqack:AckError !Group1 [reqack ne REGISTERED];
    reject; stop

    []

    (* 1 new member in private, administered group, by admin *)
    mgcs_ch !ToMGCS !User4 !CREATEGROUP !Group1 !Encode(Mail, Chan4,
             Administered, User4, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User4 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User4 !Group1 !REGISTER !Encode(User2, Chan3);
    gcs_ch !FromGCS !User4 ?reqack:AckError !Group1 [reqack ne REGISTERED];
    reject; stop

    []

    (* 1 new member in private, administered group, not by admin *)
    mgcs_ch !ToMGCS !User4 !CREATEGROUP !Group1 !Encode(Mail, Chan4,
             Administered, User4, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User4 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User1 !Group1 !REGISTER !Encode(Chan3);
    gcs_ch !FromGCS !User1 ?reqack:AckError !Group1 [reqack ne NOTADMIN];
    reject; stop

    []

    (* Change the CID of a group member *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User1 !Group1 !REGISTER !Encode(Chan2);
    gcs_ch !FromGCS !User1 !REGISTERED !Group1;
    (* Verification *)
    gcs_ch !ToGCS !User1 !Group1 !MULTICAST !Encode(Hello);
    out_ch !User1.Chan4 !User1 !Encode(Hello);  (* Should deadlock here *)
    gcs_ch !FromGCS !User1 ?reqack:AckError !Group1 [reqack ne MESSAGESENT];
    reject; stop

endproc (* Test_8: TestUCMregR *)


(***************************************************************************)
(*                                                                         *)
(*      List of Members                                                    *)
(*                                                                         *)
(***************************************************************************)

(* Assumes that Creation and Registration requests are operational. *)

(* Acceptance test : Checks member registration within a group (4 tests) *)
process Test_9 [mgcs_ch, gcs_ch, success]:noexit :=

    (* 1 member in group (creator) *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Video, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User2 !Group1 !MEMBERS !NoMsg;
    gcs_ch !FromGCS !User2 !MEMBERSARE(Insert(User1,Empty)) !Group1;
    success; stop

    []

    (* 2 members in group *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User3 !Group1 !REGISTER !Encode(Chan2 of CID);
    gcs_ch !FromGCS !User3 !REGISTERED !Group1;
    gcs_ch !ToGCS !User2 !Group1 !MEMBERS !NoMsg;
    gcs_ch !FromGCS !User2 !MEMBERSARE(Insert(User3, Insert(User1, Empty)))
                           !Group1;
    success; stop

    []

    (* Sender is a member of private group *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan4,
             Administered, User1, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User1 !Group1 !REGISTER !Encode(User3, Chan4);
    gcs_ch !FromGCS !User1 !REGISTERED !Group1;
    gcs_ch !ToGCS !User3 !Group1 !MEMBERS !NoMsg;
    gcs_ch !FromGCS !User3 !MEMBERSARE(Insert(User3, Insert(User1, Empty)))
                           !Group1;
    success; stop

    []

    (* Sender is not a member of private group *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             Administered, User1, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User2 !Group1 !MEMBERS !NoMsg;
    gcs_ch !FromGCS !User2 !MEMBERNOTINGROUP !Group1;
    success; stop

endproc (* Test_9: TestUCMmembersA *)


(* Rejection test : Checks member registration within a group (3 tests) *)
process Test_10 [mgcs_ch, gcs_ch, reject]:noexit :=

    (* 1 member in group (creator) *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User2 !Group1 !MEMBERS !NoMsg;
    gcs_ch !FromGCS !User2 ?reqack:AckError !Group1
                            [reqack ne MEMBERSARE(Insert(User1,Empty))];
    reject; stop

    []

    (* Sender is a member of private group *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan4,
             Administered, User1, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User1 !Group1 !REGISTER !Encode(User3, Chan3);
    gcs_ch !FromGCS !User1 !REGISTERED !Group1;
    gcs_ch !ToGCS !User3 !Group1 !MEMBERS !NoMsg;
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group1
                  [reqack ne MEMBERSARE(Insert(User3, Insert(User1, Empty)))];
    reject; stop

    []

    (* Sender is not a member of private group *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan1,
             Administered, User1, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User2 !Group1 !MEMBERS !NoMsg;
    gcs_ch !FromGCS !User2 ?reqack:AckError !Group1
                            [reqack ne MEMBERNOTINGROUP];
    reject; stop

endproc (* Test_10: TestUCMmembersR *)


(***************************************************************************)
(*                                                                         *)
(*      Member DeRegistration                                              *)
(*                                                                         *)
(***************************************************************************)

(* Assumes that Creation, Registration and Members (list) *)
(* requests are operational. *)

(* Acceptance test : Checks member deregistration within a group (7 tests) *)
process Test_11 [mgcs_ch, gcs_ch, success]:noexit :=

    (* Last member in non-administered group. Group is automatically deleted.*)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !DEREGISTER !NoMsg;
    gcs_ch !FromGCS !User3 !DEREGISTERED !Group4;
    gcs_ch !FromGCS !User3 !GROUPDELETED !Group4;
    success; stop

    []

    (* Last member in administered group. Group is automatically deleted. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             Administered, User3, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !DEREGISTER !Encode(User3);
    gcs_ch !FromGCS !User3 !DEREGISTERED !Group4;
    gcs_ch !FromGCS !User3 !GROUPDELETED !Group4;
    success; stop

    []

    (* 1st member in 2-members group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !REGISTER !Encode(Chan1 of CID);
    gcs_ch !FromGCS !User4 !REGISTERED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !DEREGISTER !NoMsg;
    gcs_ch !FromGCS !User3 !DEREGISTERED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User2 !Group4 !MEMBERS !NoMsg;
    gcs_ch !FromGCS !User2 !MEMBERSARE(Insert(User4, Empty)) !Group4;
    success; stop

    []

    (* 2nd member in 2-members group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !REGISTER !Encode(Chan1 of CID);
    gcs_ch !FromGCS !User4 !REGISTERED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !DEREGISTER !NoMsg;
    gcs_ch !FromGCS !User4 !DEREGISTERED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User2 !Group4 !MEMBERS !NoMsg;
    gcs_ch !FromGCS !User2 !MEMBERSARE(Insert(User3, Empty)) !Group4;
    success; stop

    []

    (* Member in administered group, by admin *)
    mgcs_ch !ToMGCS !User4 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             Administered, User4, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User4 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !REGISTER !Encode(User2, Chan4);
    gcs_ch !FromGCS !User4 !REGISTERED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !MEMBERS !NoMsg;
    gcs_ch !FromGCS !User4 !MEMBERSARE(Insert(User2, Insert(User4, Empty)))
                           !Group4;
    gcs_ch !ToGCS !User4 !Group4 !DEREGISTER !Encode(User2 of MID);
    gcs_ch !FromGCS !User4 !DEREGISTERED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User4 !Group4 !MEMBERS !NoMsg;
    gcs_ch !FromGCS !User4 !MEMBERSARE(Insert(User4, Empty)) !Group4;
    success; stop

    []

    (* Unknown member in public group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !DEREGISTER !NoMsg;
    gcs_ch !FromGCS !User4 !MEMBERNOTINGROUP !Group4;
    success; stop

    []

    (* Unknown member in administered group, by admin *)
    mgcs_ch !ToMGCS !User4 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             Administered, User4, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User4 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !DEREGISTER !Encode(User2 of MID);
    gcs_ch !FromGCS !User4 !MEMBERNOTINGROUP !Group4;
    success; stop

endproc (* Test_11: TestUCMderegA *)


(* Rejection test : Checks member deregistration within a group (5 tests) *)
process Test_12 [mgcs_ch, gcs_ch, reject]:noexit :=

    (* Member in a group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !REGISTER !Encode(Chan1 of CID);
    gcs_ch !FromGCS !User4 !REGISTERED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !DEREGISTER !NoMsg;
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4 [reqack ne DEREGISTERED];
    reject; stop

    []

    (* Last member in group. Group should be automatically deleted. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !DEREGISTER !NoMsg;
    gcs_ch !FromGCS !User3 !DEREGISTERED !Group4;
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4 [reqack ne GROUPDELETED];
    reject; stop

    []

    (* Member in administered group, by admin *)
    mgcs_ch !ToMGCS !User4 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             Administered, User4, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User4 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !REGISTER !Encode(User1 of MID, Chan2 of CID);
    gcs_ch !FromGCS !User4 !REGISTERED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !MEMBERS !NoMsg;
    gcs_ch !FromGCS !User4 !MEMBERSARE(Insert(User1, Insert(User4, Empty)))
                           !Group4;
    gcs_ch !ToGCS !User4 !Group4 !DEREGISTER !Encode(User1 of MID);
    gcs_ch !FromGCS !User4 ?reqack:AckError !Group4 [reqack ne DEREGISTERED];
    reject; stop

    []

    (* Unknown member in public group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !DEREGISTER !NoMsg;
    gcs_ch !FromGCS !User4 ?reqack:AckError !Group4
                            [reqack ne MEMBERNOTINGROUP];
    reject; stop

    []

    (* Unknown member in administered group, by admin *)
    mgcs_ch !ToMGCS !User4 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             Administered, User4, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User4 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !DEREGISTER !Encode(User1 of MID);
    gcs_ch !FromGCS !User4 ?reqack:AckError !Group4
                            [reqack ne MEMBERNOTINGROUP];
    reject; stop

endproc (* Test_12: TestUCMderegR *)


(***************************************************************************)
(*                                                                         *)
(*      Multicast                                                          *)
(*                                                                         *)
(***************************************************************************)

(* Assumes that Creation and Registration requests are operational. *)

(* Acceptance test : Checks group multicast (6 tests) *)
process Test_13 [mgcs_ch, gcs_ch, out_ch, success]:noexit :=

    (* 3 members in public, non-moderated group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !REGISTER !Encode(Chan1);
    gcs_ch !FromGCS !User2 !REGISTERED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !REGISTER !Encode(Chan2);
    gcs_ch !FromGCS !User4 !REGISTERED !Group4;
    gcs_ch !ToGCS !User1 !Group4 !MULTICAST !Encode(Hello);
    out_ch !User2.Chan1 !User1 !Encode(Hello);     (* any order! *)
    out_ch !User3.Chan4 !User1 !Encode(Hello);
    out_ch !User4.Chan2 !User1 !Encode(Hello);
    gcs_ch !FromGCS !User1 !MESSAGESENT !Group4;
    success; stop

    []

    (* 3 members in public, non-moderated group. Different order *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !REGISTER !Encode(Chan1);
    gcs_ch !FromGCS !User2 !REGISTERED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !REGISTER !Encode(Chan2);
    gcs_ch !FromGCS !User4 !REGISTERED !Group4;
    gcs_ch !ToGCS !User1 !Group4 !MULTICAST !Encode(Hello);
    out_ch !User3.Chan4 !User1 !Encode(Hello);
    out_ch !User2.Chan1 !User1 !Encode(Hello);     (* any order! *)
    out_ch !User4.Chan2 !User1 !Encode(Hello);
    gcs_ch !FromGCS !User1 !MESSAGESENT !Group4;
    success; stop

    []

    (* Sender is a member of closed group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan4,
             Administered, User3, Closed, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !REGISTER !Encode(Chan1);
    gcs_ch !FromGCS !User2 !REGISTERED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !MULTICAST !Encode(Hello);
    out_ch !User2.Chan1 !User2 !Encode(Hello);
    out_ch !User3.Chan4 !User2 !Encode(Hello);     (* any order! *)
    gcs_ch !FromGCS !User2 !MESSAGESENT !Group4;
    success; stop

    []

    (* Sender is not member of close group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Closed, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User1 !Group4 !MULTICAST !Encode(Hello);
    gcs_ch !FromGCS !User1 !MEMBERNOTINGROUP !Group4;
    success; stop

    []

    (* Sender is moderator of moderated group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan1,
             Administered, User3, Opened, Public, Moderated , User2);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !MULTICAST !Encode(Hello);
    out_ch !User3.Chan1 !User2 !Encode(Hello);
    gcs_ch !FromGCS !User2 !MESSAGESENT !Group4;
    success; stop

    []

    (* Sender is not moderator of moderated group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan1,
             Administered, User3, Opened, Public, Moderated , User2);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User1 !Group4 !MULTICAST !Encode(Hello);
    gcs_ch !FromGCS !User2 !ToApprove(User1, Encode(Hello)) !Group4 ;
    gcs_ch !FromGCS !User1 !SENTTOMODERATOR !Group4;
    success; stop

endproc (* Test_13: TestUCMmultA *)


(* Rejection test : Checks group multicast (6 tests) *)
process Test_14 [mgcs_ch, gcs_ch, out_ch, reject]:noexit :=

    (* 3 members in public, non-moderated group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !REGISTER !Encode(Chan1);
    gcs_ch !FromGCS !User2 !REGISTERED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !REGISTER !Encode(Chan2);
    gcs_ch !FromGCS !User4 !REGISTERED !Group4;
    gcs_ch !ToGCS !User1 !Group4 !MULTICAST !Encode(Hello);
    out_ch !User3.Chan3 !User1 !Encode(Hello);     (* any order! *)
    out_ch !User2.Chan1 !User1 !Encode(Hello);
    out_ch !User4.Chan2 !User1 !Encode(Hello);
    gcs_ch !FromGCS !User1 ?reqack:AckError !Group4 [reqack ne MESSAGESENT];
    reject; stop

    []

    (* MESSAGESENT ack before messages are sent (or lost of a message). *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User1 !Group4 !MULTICAST !Encode(Hello);
    gcs_ch !FromGCS !User1 !MESSAGESENT !Group4;
    reject; stop

    []

    (* Sender is a member of closed group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan1,
             Administered, User3, Closed, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !REGISTER !Encode(Chan1);
    gcs_ch !FromGCS !User2 !REGISTERED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !MULTICAST !Encode(Hello);
    gcs_ch !FromGCS !User2 !MEMBERNOTINGROUP !Group4;
    reject; stop

    []

    (* Sender is not member of closed group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Closed, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User1 !Group4 !MULTICAST !Encode(Hello);
    out_ch !User3.Chan3 !User1 !Encode(Hello);     (* any order! *)
    gcs_ch !FromGCS !User1 !MESSAGESENT !Group4;
    reject; stop

    []

    (* Sender is moderator of moderated group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan1,
             Administered, User3, Opened, Public, Moderated, User2);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !MULTICAST !Encode(Hello);
    gcs_ch !FromGCS !User2 !ToApprove(User2, Encode(Hello)) !Group4 ;
    gcs_ch !FromGCS !User2 !SENTTOMODERATOR !Group4;
    reject; stop

    []

    (* Sender is not moderator of moderated group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan1,
             Administered, User3, Opened, Public, Moderated , User2);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User1 !Group4 !MULTICAST !Encode(Hello);
    out_ch !User3.Chan1 !User1 !Encode(Hello);
    gcs_ch !FromGCS !User1 !MESSAGESENT !Group4;
    reject; stop

endproc (* Test_14: TestUCMmultR *)



(***************************************************************************)
(*                                                                         *)
(*      Group Deletion                                                     *)
(*                                                                         *)
(***************************************************************************)

(* Assumes that Creation, List (of groups), Registration, and *)
(* Multicast requests are operational. *)

(* Acceptance test : Checks deletion of groups (6 tests) *)
process Test_15 [mgcs_ch, gcs_ch, success]:noexit :=

    (* Deletes last group in a list of groups *)
    mgcs_ch !ToMGCS !User2 !CREATEGROUP !Group2 !Encode(Video, Chan3,
             Administered, User2, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User2 !GROUPCREATED !Group2;
    gcs_ch !ToGCS !User2 !Group2 !DELETEGROUP !NoMsg;
    gcs_ch !FromGCS !User2 !GROUPDELETED !Group2;
    (* Verification *)
    mgcs_ch !ToMGCS !User3 !GROUPS;
    mgcs_ch !FromMGCS !User3 !GROUPSARE(NoGCS);
    success; stop

    []

    (* Admin deletes first group in a list of two administered groups *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan3,
             Administered, User1, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    mgcs_ch !ToMGCS !User2 !CREATEGROUP !Group2 !Encode(Video, Chan3,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User2 !GROUPCREATED !Group2;
    gcs_ch !ToGCS !User1 !Group1 !DELETEGROUP !NoMsg;
    gcs_ch !FromGCS !User1 !GROUPDELETED !Group1;
    (* Verification *)
    mgcs_ch !ToMGCS !User3 !GROUPS;
    mgcs_ch !FromMGCS !User3 !GROUPSARE(Insert(Group2, NoGCS));
    success; stop

    []

    (* Admin deletes second group in a list of two administered groups *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan3,
             Administered, User1, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    mgcs_ch !ToMGCS !User2 !CREATEGROUP !Group2 !Encode(Video, Chan3,
             Administered, User2, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User2 !GROUPCREATED !Group2;
    gcs_ch !ToGCS !User2 !Group2 !DELETEGROUP !NoMsg;
    gcs_ch !FromGCS !User2 !GROUPDELETED !Group2;
    (* Verification *)
    mgcs_ch !ToMGCS !User3 !GROUPS;
    mgcs_ch !FromMGCS !User3 !GROUPSARE(Insert(Group1, NoGCS));
    success; stop

    []

    (* Non-admin tries to delete an administered group *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan3,
             Administered, User1, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User2 !Group1 !DELETEGROUP !NoMsg;
    gcs_ch !FromGCS !User2 !NOTADMIN !Group1;
    (* Verification *)
    mgcs_ch !ToMGCS !User3 !GROUPS;
    mgcs_ch !FromMGCS !User3 !GROUPSARE(Insert(Group1, NoGCS));
    success; stop

    []

    (* Someone tries to delete a non-administered group *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User2 !Group1 !DELETEGROUP !NoMsg;
    gcs_ch !FromGCS !User2 !NOADMINGROUP !Group1;
    (* Verification *)
    mgcs_ch !ToMGCS !User3 !GROUPS;
    mgcs_ch !FromMGCS !User3 !GROUPSARE(Insert(Group1, NoGCS));
    success; stop

    []

    (* Indicates to all members that their group was deleted *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Video, Chan1,
             Administered, User1, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !REGISTER !Encode(Chan1);
    gcs_ch !FromGCS !User2 !REGISTERED !Group4;
    gcs_ch !ToGCS !User4 !Group4 !REGISTER !Encode(Chan2);
    gcs_ch !FromGCS !User4 !REGISTERED !Group4;
    gcs_ch !ToGCS !User1 !Group4 !DELETEGROUP !NoMsg;
    (* LIFO order here... Clients should however run in parallel, thus *)
    (* fixing part of this testing problem. *)
    gcs_ch !FromGCS !User4 !GROUPWASDELETED !Group4;
    gcs_ch !FromGCS !User2 !GROUPWASDELETED !Group4;
    gcs_ch !FromGCS !User3 !GROUPWASDELETED !Group4;
    gcs_ch !FromGCS !User1 !GROUPDELETED !Group4;
    (* Verification *)
    mgcs_ch !ToMGCS !User3 !GROUPS;
    mgcs_ch !FromMGCS !User3 !GROUPSARE(NoGCS);
    success; stop

endproc (* Test_15: TestUCMdeletionA *)


(* Rejection test : Checks deletion of groups (5 tests) *)
process Test_16 [mgcs_ch, gcs_ch, reject]:noexit :=

    (* Deletes non-existing group *)
    gcs_ch !ToGCS !User1 ?anyGroup:GID !DELETEGROUP !NoMsg;
    gcs_ch !FromGCS !User1 !GROUPDELETED ?anyGroup:GID;
    reject; stop

    []

    (* Deletes a non-administered group *)
    mgcs_ch !ToMGCS !User2 !CREATEGROUP !Group2 !Encode(Video, Chan3,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User2 !GROUPCREATED !Group2;
    gcs_ch !ToGCS !User2 !Group2 !DELETEGROUP !NoMsg;
    gcs_ch !FromGCS !User2 ?reqack:AckError !Group2 [reqack ne NOADMINGROUP];
    reject; stop

    []

    (* Admin deletes an administered group *)
    mgcs_ch !ToMGCS !User2 !CREATEGROUP !Group2 !Encode(Video, Chan3,
             Administered, User2, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User2 !GROUPCREATED !Group2;
    gcs_ch !ToGCS !User2 !Group2 !DELETEGROUP !NoMsg;
    gcs_ch !FromGCS !User2 ?reqack:AckError !Group2 [reqack ne GROUPDELETED];
    reject; stop

    []

    (* Non-admin tries to delete an administered group *)
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan3,
             Administered, User1, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User2 !Group1 !DELETEGROUP !NoMsg;
    gcs_ch !FromGCS !User2 ?reqack:AckError !Group1 [reqack ne NOTADMIN];
    reject; stop

    []

    (* Member not advised that his group was deleted *)
    mgcs_ch !ToMGCS !User2 !CREATEGROUP !Group4 !Encode(Video, Chan3,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User2 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User1 !Group4 !DELETEGROUP !NoMsg;
    gcs_ch !FromGCS !User1 !GROUPDELETED !Group4;
    reject; stop

endproc (* Test_16: TestUCMdeletionR *)


(***************************************************************************)
(*                                                                         *)
(*      Administrator Changing                                             *)
(*                                                                         *)
(***************************************************************************)

(* Assumes that Creation and Registration requests are operational. *)

(* Acceptance test : Check the change of admin properties (5 tests) *)
process Test_17 [mgcs_ch, gcs_ch, success]:noexit :=

    (* Non-administered group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEADMIN !Encode(User2);
    gcs_ch !FromGCS !User3 !NOADMINGROUP !Group4;
    success; stop

    []

    (* Administered group, not by admin *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !CHANGEADMIN !Encode(User2);
    gcs_ch !FromGCS !User2 !NOTADMIN !Group4;
    success; stop

    []

    (* Administered group, by admin, with new admin not in group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEADMIN !Encode(User2);
    gcs_ch !FromGCS !User3 !MEMBERNOTINGROUP !Group4;
    success; stop

    []

    (* Administered group, by admin, with new admin in group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !REGISTER !Encode(Chan1);
    gcs_ch !FromGCS !User2 !REGISTERED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEADMIN !Encode(User2);
    gcs_ch !FromGCS !User3 !ADMINCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User2 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User2 !ATTRIBUTESARE(Encode(Mail, Chan3,Administered,
                      User2, Opened, Public, NonModerated, Nobody)) !Group4;
    success; stop

    []

    (* Change from administered group to non-administered, by admin. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEADMIN !Encode(Nobody);
    gcs_ch !FromGCS !User3 !ADMINCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User3 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User3 !ATTRIBUTESARE(Encode(Mail, Chan3,NonAdministered,
                      Nobody, Opened, Public, NonModerated, Nobody)) !Group4;
    success; stop

endproc (* Test_17: TestUCMadminA *)


(* Rejection test : Checks the change of admin properties (6 tests) *)
process Test_18 [mgcs_ch, gcs_ch, reject]:noexit :=

    (* Non administered group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEADMIN !Encode(User2);
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4 [reqack ne NOADMINGROUP];
    reject; stop

    []

    (* Administered group, not by admin *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !CHANGEADMIN !Encode(User2);
    gcs_ch !FromGCS !User2 ?reqack:AckError !Group4 [reqack ne NOTADMIN];
    reject; stop

    []

    (* Administered group, by admin, with new admin not in group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEADMIN !Encode(User2);
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4
                            [reqack ne MEMBERNOTINGROUP];
    reject; stop

    []

    (* Administered group, by admin, with new admin in group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !REGISTER !Encode(Chan1);
    gcs_ch !FromGCS !User2 !REGISTERED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEADMIN !Encode(User2);
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4 [reqack ne ADMINCHANGED];
    reject; stop

    []

    (* Administered group, by admin, with new admin in group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !REGISTER !Encode(Chan1);
    gcs_ch !FromGCS !User2 !REGISTERED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEADMIN !Encode(User2);
    gcs_ch !FromGCS !User3 !ADMINCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User2 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User2 ?reqack:AckError !Group4
           [reqack ne ATTRIBUTESARE(Encode(Mail, Chan3, Administered, User2,
                                     Opened, Public, NonModerated, Nobody))];
    reject; stop

    []

    (* Change from administered group no non-administered, by admin. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEADMIN !Encode(Nobody);
    gcs_ch !FromGCS !User3 !ADMINCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User3 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4
           [reqack ne ATTRIBUTESARE(Encode(Mail, Chan3, NonAdministered,
                              Nobody, Opened, Public, NonModerated, Nobody))];
    reject; stop

endproc (* Test_18: TestUCMadminR *)


(***************************************************************************)
(*                                                                         *)
(*      Moderator Changing                                                 *)
(*                                                                         *)
(***************************************************************************)

(* Assumes that Creation, Registration and Multicast requests are *)
(* operational. *)

(* Acceptance test : Checks the change of moderator properties (9 tests) *)
process Test_19 [mgcs_ch, gcs_ch, success]:noexit :=

    (* Non-moderated and group, not by admin. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User3 !NOMODERGROUP !Group4;
    success; stop

    []

    (* Moderated group, not by moderator (nor admin) *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, Moderated, User1);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User2 !NOTMODER !Group4;
    success; stop

    []

    (* Closed moderated group, by moderator, with new moderator not in group*)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Closed, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User3 !MEMBERNOTINGROUP !Group4;
    success; stop

    []

    (* Closed administered and moderated group, by admin, with new *)
    (* moderator not in group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Closed, Public, Moderated, User1);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User3 !MEMBERNOTINGROUP !Group4;
    success; stop

    []

    (* Closed moderated group, by moderator, with new moderator in group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Video, Chan3,
             NonAdministered, Nobody, Closed, Public, Moderated, User1);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !REGISTER !Encode(Chan1);
    gcs_ch !FromGCS !User2 !REGISTERED !Group4;
    gcs_ch !ToGCS !User1 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User1 !MODERCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User2 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User2 !ATTRIBUTESARE(Encode(Video, Chan3, NonAdministered,
                      Nobody, Closed, Public, Moderated, User2)) !Group4;
    success; stop

    []

    (* Opened moderated group, by moderator, with new moderator not in *)
    (* group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, Moderated, User1);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User1 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User1 !MODERCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User2 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User2 !ATTRIBUTESARE(Encode(Mail, Chan3, NonAdministered,
                      Nobody, Opened, Public, Moderated, User2)) !Group4;
    success; stop

    []

    (* Change from non-moderated (opened and administered) group to *)
    (* moderated group, by admin *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User3 !MODERCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User3 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User3 !ATTRIBUTESARE(Encode(Mail, Chan3, Administered,
                      User3, Opened, Public, Moderated, User2)) !Group4;
    success; stop

    []

    (* Change from moderated group to non-moderated, by admin. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan1,
             Administered, User3, Opened, Public, Moderated, User2);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEMODER !Encode(Nobody, NonModerated);
    gcs_ch !FromGCS !User3 !MODERCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User3 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User3 !ATTRIBUTESARE(Encode(Mail, Chan1, Administered,
                      User3, Opened, Public, NonModerated, Nobody)) !Group4;
    success; stop

    []

    (* If the group becomes Non-moderated, insert Nobody as new moderator. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan1,
             Administered, User3, Opened, Public, Moderated, User2);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEMODER !Encode(User3, NonModerated);
    gcs_ch !FromGCS !User3 !MODERCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User3 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User3 !ATTRIBUTESARE(Encode(Mail, Chan1, Administered,
                      User3, Opened, Public, NonModerated, Nobody)) !Group4;
    success; stop

endproc (* Test_19: TestUCMmoderA *)


(* Rejection test : Checks the change of admin properties (7 tests) *)
process Test_20 [mgcs_ch, gcs_ch, reject]:noexit :=

    (* Non-moderated and group, not by admin. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4 [reqack ne NOMODERGROUP];
    reject; stop

    []

    (* Moderated group, not by moderator (nor admin) *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User2 ?reqack:AckError !Group4 [reqack ne NOTMODER];
    reject; stop

    []

    (* Closed moderated group, by moderator, with new moderator not in group*)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Closed, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4
                            [reqack ne MEMBERNOTINGROUP];
    reject; stop

    []

    (* Closed administered and moderated group, by admin, with new *)
    (* moderator not in group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Closed, Public, Moderated, User1);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4
                            [reqack ne MEMBERNOTINGROUP];
    reject; stop

    []

    (* Closed moderated group, by moderator, with new moderator in group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Closed, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !REGISTER !Encode(Chan1);
    gcs_ch !FromGCS !User2 !REGISTERED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4 [reqack ne MODERCHANGED];
    reject; stop

    []

    (* Opened moderated group, by moderator, with new moderator not in *)
    (* group *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4 [reqack ne MODERCHANGED];
    reject; stop

    []

    (* Change from non-moderated (opened and administered) group to *)
    (* moderated group, by admin *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan2,
             Administered, User3, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEMODER !Encode(User2, Moderated);
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4 [reqack ne MODERCHANGED];
    reject; stop

endproc (* Test_20: TestUCMmoderR *)


(***************************************************************************)
(*                                                                         *)
(*      Opened Attribute Changing                                          *)
(*                                                                         *)
(***************************************************************************)

(* Assumes that Creation and GetAttributes are operational. *)

(* Acceptance test : Checks the change of the Opened attribute (4 tests) *)
process Test_21 [mgcs_ch, gcs_ch, success]:noexit :=

    (* Administered group, request by admin. From Closed to Opened *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Closed, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEOPENATTR !Encode(Opened);
    gcs_ch !FromGCS !User3 !OPENATTRCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User3 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User3 !ATTRIBUTESARE(Encode(Mail, Chan3, Administered,
                       User3, Opened, Private, NonModerated, Nobody)) !Group4;
    success; stop

    []

    (* Administered group, request by admin. From Opened to Closed *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEOPENATTR !Encode(Closed);
    gcs_ch !FromGCS !User3 !OPENATTRCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User3 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User3 !ATTRIBUTESARE(Encode(Mail, Chan3, Administered,
                       User3, Closed, Private, NonModerated, Nobody)) !Group4;
    success; stop

    []

    (* Non-administered group, we cannot change this attribute *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEOPENATTR !Encode(Closed);
    gcs_ch !FromGCS !User3 !NOADMINGROUP !Group4;
    success; stop

    []

    (* Administered, not by admin. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !CHANGEOPENATTR !Encode(Closed);
    gcs_ch !FromGCS !User2 !NOTADMIN !Group4;
    success; stop

endproc (* Test_21: TestUCMopenA *)


(* Rejection test : Checks the change of the Opened attribute (3 tests) *)
process Test_22 [mgcs_ch, gcs_ch, reject]:noexit :=

    (* Administered group, request by admin *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Closed, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEOPENATTR !Encode(Opened);
    gcs_ch !FromGCS !User3 !OPENATTRCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User3 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4
            [reqack ne ATTRIBUTESARE(Encode(Mail, Chan3, Administered, User3,
                                    Opened, Private, NonModerated, Nobody))];
    reject; stop

    []

    (* Non-administered group, we cannot change this attribute *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEOPENATTR !Encode(Closed);
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4 [reqack ne NOADMINGROUP];
    reject; stop

    []

    (* Administered, not by admin. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !CHANGEOPENATTR !Encode(Closed);
    gcs_ch !FromGCS !User2 ?reqack:AckError !Group4 [reqack ne NOTADMIN];
    reject; stop

endproc (* Test_22: TestUCMopenR *)


(***************************************************************************)
(*                                                                         *)
(*      Private Attribute Changing                                         *)
(*                                                                         *)
(***************************************************************************)

(* Assumes that Creation and GetAttributes are operational. *)

(* Acceptance test : Checks the change of the Private attribute (4 tests) *)
process Test_23 [mgcs_ch, gcs_ch, success]:noexit :=

    (* Administered group, request by admin. From Private to Public. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Closed, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEPRIVATTR !Encode(Public);
    gcs_ch !FromGCS !User3 !PRIVATTRCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User3 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User3 !ATTRIBUTESARE(Encode(Mail, Chan3, Administered,
                        User3, Closed, Public, NonModerated, Nobody)) !Group4;
    success; stop

    []

    (* Administered group, request by admin. From Public to Private. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Closed, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEPRIVATTR !Encode(Private);
    gcs_ch !FromGCS !User3 !PRIVATTRCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User3 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User3 !ATTRIBUTESARE(Encode(Mail, Chan3, Administered,
                        User3, Closed, Private, NonModerated, Nobody)) !Group4;
    success; stop

    []

    (* Non-administered group, we cannot change this attribute *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEPRIVATTR !Encode(Private);
    gcs_ch !FromGCS !User3 !NOADMINGROUP !Group4;
    success; stop

    []

    (* Administered, not by admin. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !CHANGEPRIVATTR !Encode(Private);
    gcs_ch !FromGCS !User2 !NOTADMIN !Group4;
    success; stop

endproc (* Test_23: TestUCMprivA *)


(* Rejection test : Checks the change of the Opened attribute (3 tests) *)
process Test_24 [mgcs_ch, gcs_ch, reject]:noexit :=

    (* Administered group, request by admin *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Closed, Private, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEPRIVATTR !Encode(Public);
    gcs_ch !FromGCS !User3 !PRIVATTRCHANGED !Group4;
    (* Verification *)
    gcs_ch !ToGCS !User3 !Group4 !GETATTRIBUTES !NoMsg;
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4
            [reqack ne ATTRIBUTESARE(Encode(Mail, Chan3, Administered, User3,
                                      Closed, Public, NonModerated, Nobody))];
    reject; stop

    []

    (* Non-administered group, we cannot change this attribute *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User3 !Group4 !CHANGEPRIVATTR !Encode(Private);
    gcs_ch !FromGCS !User3 ?reqack:AckError !Group4 [reqack ne NOADMINGROUP];
    reject; stop

    []

    (* Administered, not by admin. *)
    mgcs_ch !ToMGCS !User3 !CREATEGROUP !Group4 !Encode(Mail, Chan3,
             Administered, User3, Opened, Public, Moderated, User3);
    mgcs_ch !FromMGCS !User3 !GROUPCREATED !Group4;
    gcs_ch !ToGCS !User2 !Group4 !CHANGEPRIVATTR !Encode(Private);
    gcs_ch !FromGCS !User2 ?reqack:AckError !Group4 [reqack ne NOTADMIN];
    reject; stop

endproc (* Test_24: TestUCMprivR *)


(*============================================*)
(*          Simple Client Test Case           *)
(*============================================*)

(* Test case from the client viewpoint. *)
(* Tests the refusal of requests to unknown groups by the server *)
(* The client needs a timer to detect such problems and react *)
(* accordingly. *)

process Test_25[gcs_ch, success] : exit :=
    hide reject, timeout in
    (* Any request to Group4, which does not exist *)
        gcs_ch !ToGCS !User2 !Group4 ?anyreq:Request !NoMsg;
        reject; exit (* We should not be able to get here *)
        [>
        timeout;     (* timeout should be the only action possible *)
        success; stop
endproc (* Test_25: TestClientA *)


(*============================================*)
(* Complex Test Case with Pre/Post Conditions *)
(*============================================*)

(* This is a more generic format for test processes. We first bring the *)
(* system from the initial state to a specific state that satisfies a *)
(* pre-condition. Then, we execute the scenario, and finally we check *)
(* the scenario post-condition. In this example, the scenario tests *)
(* that we can register a second member to a group that contains already *)
(* one member. *)


process Test_26[mgcs_ch, gcs_ch, out_ch, success] : noexit :=

  hide reject in
  (* Preamble *)
  (* Gets the system to a state where a group contains only its creator *)
  (
    mgcs_ch !ToMGCS !User1 !CREATEGROUP !Group1 !Encode(Mail, Chan3,
             NonAdministered, Nobody, Opened, Public, NonModerated, Nobody);
    mgcs_ch !FromMGCS !User1 !GROUPCREATED !Group1;
    gcs_ch !ToGCS !User1 !Group1 !REGISTER !Encode(Chan2);
    gcs_ch !FromGCS !User1 !REGISTERED !Group1;
    exit
  )
  >>
  (* Check pre-condition : *)
  (* (Group1 IsIn GroupList) AND (MemberList(Group1)={User1}) *)
  (
    gcs_ch !ToGCS !User2 !Group1 !MEMBERS !NoMsg;
    (
        gcs_ch !FromGCS !User2 !MEMBERSARE(Insert(User1, Empty)) !Group1;
        exit
        []
        gcs_ch !FromGCS !User2 ?reqack:AckError !Group1
                                [reqack ne MEMBERSARE(Insert(User1, Empty))];
        reject; stop (* Pre-condition not satisfied *)
    )
  )
  >>
  (* Check scenario: Register of a second user in a group (User3 in Group1) *)
  (
    gcs_ch !ToGCS !User3 !Group1 !REGISTER !Encode(Chan2);
    gcs_ch !FromGCS !User3 !REGISTERED !Group1;
    exit
  )
  >>
  (* Check post-condition: *)
  (* (Group1 IsIn GroupList) AND (MemberList(Group1)={User1, User3}) *)
  (
    gcs_ch !ToGCS !User2 !Group1 !MEMBERS !NoMsg;
    (
        gcs_ch !FromGCS !User2 !MEMBERSARE(Insert(User3, Insert(User1, Empty)))
                               !Group1;
        success; stop
        []
        gcs_ch !FromGCS !User2 ?reqack:AckError !Group1
                   [reqack ne MEMBERSARE(Insert(User3,Insert(User1, Empty)))];
        reject; stop (* Post-condition not satisfied *)
    )
  )

endproc (* Test_26: Test_Complex *)

endspec (* GCS, Group Communication Server *)