(****************************************************************************) (* *) (* 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 *)