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