(*************************************************************************** * * Group Communication Service, VERSION 1.13 * * Daniel Amyot and Jacques Sincennes * University of Ottawa, August 15, 1996 * * Purpose: Multicast messages to the members of a group. * ======= * * Channels: * ======== * mgcs_ch: Master Group Communication Server Channel * gcs_ch: Group Communication Server Channels * out_ch: mean of distributing messages to group members * * Groups: * ====== * - administered: admin alone creates and destroys group * * - moderated: moderator is the only one allowed to multicast. * All other messages are sent to him for approval. * * - public anyone can register * e.g. mailing lists * - private admin must register another one. Must be member to see list * of group members. * e.g. telephone conference * * - opened anyone can send * e.g. mailing lists * - closed must be member to send * e.g. IRC * ***************************************************************************) 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 member is identified by a hexadecimal digit. *) (* Use hexadecimal digits as Member Identifiers *) type MIDType0 is HexDigit renamedby sortnames MID for HexDigit endtype (* MIDType0 *) type MIDType is MIDType0 opns (* Special MID reserved for admin/moder modification *) Nobody : -> MID eqns ofsort Nat (* For comparisons with other MIDs *) NatNum(NoBody) = Succ(NatNum(F of MID)); 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 use hexadecimal digits as 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 HexDigit renamedby sortnames CID for HexDigit 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 *) (*********************************************) (* Use hexadecimal digits as GCS IDentifiers *) type GIDType is HexDigit renamedby sortnames GID for HexDigit endtype (* GIDType *) (*********************************************) (* List of channel multicasting types available *) type ChanType is sorts Chan opns Mail, Socket, Text, Audio, Video : -> Chan endtype (* ChanType *) (********************************************************** * A group contains characteristics and a list of members. * Characteristics are tuples (records): * (groupID, (of GID) * rationale, (not shown here) * channelType, (of Chan) * administeredBool, (of Bool) * adminID, (of MID) * openedBool, (of Bool) * privateBool, (of Bool) * moderatedBool, (of Bool) * moderID (of MID) ) * * Used in messages and in GCS databases. **********************************************************) type GCSinfoRecordType is GIDType, MemberListType, ChanType sorts GSCinfo opns Info : GID, Chan, Bool, MID, Bool, Bool, Bool, MID -> GSCinfo _eq_, _ne_ : GSCinfo, GSCinfo -> Bool eqns forall gcs1, gcs2 : GSCinfo ofsort Bool gcs1 eq gcs2 = true; (* Needed by ISLA? *) gcs1 ne gcs2 = not(gcs1 eq gcs2); endtype (* GCSinfoRecordType *) (*********************************************) (* List of Groups for Master GCS, implemented as a set. *) (* We avoid the problem with ISLA's renaming in actualization *) type GroupList0 is Set actualizedby GIDType using sortnames GID for Element Bool for FBool endtype (* GroupList0 *) type GroupList is GroupList0 renamedby sortnames GroupList for Set opnnames NoGCS for {} (* Empty list of GCS *) endtype (* GroupList *) (*********************************************) (* Request messages to be sent to the server *) type RequestType is HexDigit renamedby sortnames Request for HexDigit opnnames CREATEGROUP for 1 DELETEGROUP for 2 REGISTER for 3 DEREGISTER for 4 MEMBERS for 5 GROUPS for 6 MULTICAST for 7 CHANGEADMIN for 8 CHANGEMODER for 9 endtype (* RequestType *) (* Resulting acknowledgement messages (OK and Error) from the server *) type AckType0 is HexDigit renamedby sortnames Ack for HexDigit opnnames (* OK *) GROUPCREATED for 1 GROUPDELETED for 2 REGISTERED for 3 DEREGISTERED for 4 MESSAGESENT for 5 ADMINMODERCHANGED for 6 (* Admin or Moderator was changed successfully *) SENTTOMODERATOR for 7 GROUPWASDELETED for 8 (* Multicast when a group is deleted *) (* Errors *) GROUPEXISTS for 9 GROUPDOESNOTEXIST for A MEMBERNOTINGROUP for B NOTADMINMODER for C NOADMINGROUP for D NOMODERGROUP for E UNKNOWNREQUEST for F endtype (* AckType0 *) (* Additional operation to encode lists of members. *) type AckType is AckType0, MIDListType opns MembersAre : MIDList -> Ack eqns forall m: MIDList ofsort Nat (* for comparison with other Acks *) NatNum(MembersAre(m)) = succ(NatNum(UNKNOWNREQUEST)); endtype (* AckType *) (* Instances of messages that can be multicast (for readability). *) (* A message should be, however, a bit string. *) type InfoMsgType is Boolean sorts InfoMsg opns Hi, Hello, Salut, GoodBye, Packet, GroupIsDeleted : -> InfoMsg endtype (* InfoMsgType *) (*********************************************) (* Encoding/Decoding of messages *) (* Several types of packets are needed. *) (* Supplemental packet types are provided for simpler execution *) type MsgType is GCSinfoRecordType, RequestType, AckType, InfoMsgType sorts Msg opns (****************************************************************** * No Message Packet. Used for: * Group deletion * List members * List groups * Deregister ******************************************************************) NoMsg : -> Msg (****************************************************************** * General Packet for Group Creation: * Channel Type (of Chan) * ChanID (od CID) * Administered? (of Bool) * Administrator (of MID) * Opened? (of Bool) * Private? (of Bool) * Moderated? (of Bool) * Moderator (of MID) *******************************************************************) Encode : Chan, CID, Bool, MID, Bool, Bool, Bool, MID -> Msg (* 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 Administrator modification: * Administrator (of MID) * Private? (of Bool) * * Packet for Group Moderator modification: * Moderator (of MID) * Moderated? (of Bool) ******************************************************************) Encode : MID, Bool -> Msg (* Modification Operations *) SetAdmin : MID, Bool, Msg-> Msg SetModer : MID, Bool, Msg-> Msg (****************************************************************** * Packet for moderator approval ******************************************************************) ToApprove : Msg -> Ack (****************************************************************** * Packets for multicasting ******************************************************************) Encode : InfoMsg -> Msg Encode : Ack -> Msg (* Modification Operations *) GetAck : Msg -> Ack 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 eqns forall msg : Msg, info : InfoMsg, CT : Chan, ChID : CID, Adm, NewAdm, Mem, Mod, NewMod : MID, AB, OB, PB, NewPB, MB, NewMB : Bool, ack : Ack 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; IsOpened(Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod)) = OB; IsPrivate(Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod)) = PB; IsPrivate(Encode(Adm, PB)) = PB; IsModerated(Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod)) = MB; IsModerated(Encode(Mod, MB)) = MB; ofsort MID Admin(Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod)) = Adm; Admin(Encode(Adm, PB)) = Adm; Moderator(Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod)) = Mod; Moderator(Encode(Mod, MB)) = Mod; NewMember(Encode(Mem, ChID)) = Mem; ofsort InfoMsg GetInfo(Encode(info)) = info; ofsort Ack GetAck(Encode(ack)) = ack; ofsort Msg (* If the group becomes unadministred (the new admin is Nobody), *) (* then it must be public. *) NewAdm eq Nobody => SetAdmin(NewAdm, NewPB, Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod)) = Encode(CT, ChID, false, NewAdm, OB, false, MB, Mod); NewAdm ne Nobody => SetAdmin(NewAdm, NewPB, Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod)) = Encode(CT, ChID, AB, NewAdm, OB, NewPB, MB, Mod); (* If the new moderator is Nobody, the group becomes unmoderated *) NewMod eq NoBody => SetModer(NewMod, NewMB, Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod)) = Encode(CT, ChID, AB, Adm, OB, PB, false, NewMod); NewMod ne NoBody => SetModer(NewMod, NewMB, Encode(CT, ChID, AB, Adm, OB, PB, MB, Mod)) = Encode(CT, ChID, AB, Adm, OB, PB, NewMB, NewMod); ofsort Nat (* for comparison with other Acks *) NatNum(ToApprove(msg)) = succ(succ(NatNum(UNKNOWNREQUEST))); endtype (* MsgType *) (*********************************************) (********************************************* * * Buffering of requests and acknowledgements * * A generic type is created and actualized as * FIFO buffers for reqs and acks. * *********************************************) (* 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 (* FIFO *) (* Encoding of requests and acknowledgements as Records *) type BufferEncodingType is MIDType, AckType, RequestType, MsgType sorts ReqRecord, AckRecord opns AckElem : MID, Ack -> AckRecord ReqElem : MID, Request, Msg -> ReqRecord S : AckRecord -> MID (* Extract Sender *) A : AckRecord -> Ack (* Extract Ack *) S : ReqRecord -> MID (* Extract Sender *) R : ReqRecord -> Request (* Extract Request *) M : ReqRecord -> Msg (* Extract Message *) eqns forall S1:MID, A1:Ack, R1:Request, M1:Msg ofsort MID S(AckElem(S1, A1)) = S1; S(ReqElem(S1, R1, M1)) = S1; ofsort Ack 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 (* FIFOreqsType *) type FIFOreqsType is FIFOreqsType0 renamedby sortnames FIFOreqs for FIFO opnnames NoReq for Nothing endtype (* FIFOreqsType0 *) (* Actualization (and renaming) of a Buffer type for records of acks *) type FIFOacksType0 is FIFOType actualizedby BufferEncodingType using sortnames AckRecord for Element endtype (* FIFOacksType0 *) type FIFOacksType is FIFOacksType0 renamedby sortnames FIFOacks for FIFO opnnames NoAck for Nothing endtype (* FIFOacksType *) (*============================================*) (* 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 agcs_ch in (* Administrative channel *) ( MGCS[agcs_ch, mgcs_ch](NoGCS) (* Management *) |[agcs_ch]| Spawn_GCS[agcs_ch, gcs_ch, out_ch] (* GCS spawning *) ) endproc (* Control_Team *) (*************************************************************************** * * Master Group Communication Server (MGCS) * * Listens on the MGCS channel for requests for: * - the creation of a new Group Communication Server (GCS) * - the list of existing GCS * ***************************************************************************) process MGCS[agcs_ch, mgcs_ch](GCSlist:GroupList) :noexit:= (* Request for the creation of a new GCS *) (* the ID of the group must not be used by an existing group *) mgcs_ch ?caller:MID !CREATEGROUP ?newgroupid:GID ?infos:msg; ( [newgroupid IsIn GCSlist] -> mgcs_ch !caller! GROUPEXISTS !newgroupid; MGCS[agcs_ch, mgcs_ch](GCSlist) [] [newgroupid NotIn GCSlist] -> agcs_ch !CREATEGROUP !newgroupid !Insert(caller.ChanID(infos), NoMBR) ! infos; mgcs_ch !caller !GROUPCREATED !newgroupid; MGCS[agcs_ch, mgcs_ch](Insert(newgroupid, GCSlist)) ) [] (* Request for the list of existing groups *) mgcs_ch ?caller:MID !GROUPS; mgcs_ch !caller !GCSlist; MGCS[agcs_ch, mgcs_ch](GCSlist) [] (* Process destruction of a GCS. All verifications were done by the GCS. *) (* Used to update the goup list database *) [GCSlist ne NoGCS]-> (* allowed only if there exists at least one group *) agcs_ch !GROUPDELETED ?id:GID; MGCS [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[agcs_ch, gcs_ch, out_ch] :noexit:= agcs_ch !CREATEGROUP ?id:GID ?mbrL:MemberList ?infos: msg; ( GCS_Team[agcs_ch, gcs_ch, out_ch] (id, mbrL, infos) ||| Spawn_GCS[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 DoubleBuffer[agcs_ch, gcs_ch, inter_ch](id, false, NoReq, NoAck) |[inter_ch]| GCS[inter_ch, out_ch] (id, mbrL, infos) endproc (* GCS_Team *) (*************************************************************************** * * DoubleBuffer * * Routes messages for group ID from gcs_ch on 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. * * Requests and acknowledgements are buffered. * We use an infinite, 2-way buffer that holds two ordered lists * (for acks and requests). * ***************************************************************************) process DoubleBuffer[agcs_ch, gcs_ch, inter_ch](id:GID, terminated: Bool, bufreqs:FIFOreqs, bufacks:FIFOacks ) :exit:= (* Buffer requests from senders. *) (* Refuse them if group is deleted (terminated) *) [Not(terminated)] -> ( gcs_ch ?sender:MID !id ?req:Request ?msg:Msg; DoubleBuffer[agcs_ch, gcs_ch, inter_ch](id, terminated, Put(ReqElem(sender, req, msg), bufreqs), bufacks) ) [] (* Forwards buffered requests to GCS *) [Not(IsEmpty(bufreqs))] -> ( inter_ch !S(Get(bufreqs)) !R(Get(bufreqs)) !M(Get(bufreqs)); DoubleBuffer[agcs_ch, gcs_ch, inter_ch](id, terminated, Consume(bufreqs), bufacks) ) [] (* Buffer acks from GCS. *) inter_ch ?sender:MID ?ack:Ack; DoubleBuffer[agcs_ch, gcs_ch, inter_ch](id, terminated, bufreqs, Put(AckElem(sender, ack), bufacks)) [] (* Forwards buffered acks to senders *) [Not(IsEmpty(bufacks))] -> ( [A(Get(bufacks)) eq GROUPDELETED] -> (* Intercept this special case of ack. *) (* Informs MGCS of deletion, for dBase update. *) agcs_ch ! GROUPDELETED ! id; (* Forward ack to sender, empty the request buffer, *) (* and terminate listening *) gcs_ch !S(Get(bufacks)) !A(Get(bufacks)) !id; DoubleBuffer[agcs_ch, gcs_ch, inter_ch](id, true, NoReq, Consume(bufacks)) [] [A(Get(bufacks)) ne GROUPDELETED] -> (* Forward ack to sender *) gcs_ch !S(Get(bufacks)) !A(Get(bufacks)) !id; DoubleBuffer[agcs_ch, gcs_ch, inter_ch](id, terminated, bufreqs, Consume(bufacks)) ) [] (* After everyone has been informed of the group deletion, terminate. *) (* Waits for Req and Ack buffers to be empty *) [IsEmpty(bufreqs) and IsEmpty(bufacks) and terminated] -> inter_ch ! GROUPDELETED; exit endproc (* DoubleBuffer *) (*************************************************************************** * * 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 !Ack * ***************************************************************************) process GCS[inter_ch, out_ch](id:GID, mbrL:MemberList, infos:msg) :exit:= (* gets the request from the sender *) inter_ch ?sender:MID ?req:Request ?msg:Msg; ( [req eq DELETEGROUP] -> Req_DeleteGroup[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) [] (* subscription *) [req eq REGISTER] -> Req_Register[inter_ch, out_ch](sender, msg, id, mbrL, infos) [] (* unsubscription *) [req eq DEREGISTER] -> Req_DeRegister[inter_ch, out_ch](sender, msg, id, mbrL, infos) [] (* destruction of the group by the administrator *) (* change the moderator *) [req eq CHANGEMODER] -> Req_ChangeModer[inter_ch, out_ch](sender, msg, id, mbrL, infos) [] (* change the administrator *) [req eq CHANGEADMIN] -> Req_ChangeAdmin[inter_ch, out_ch](sender, msg, id, mbrL, infos) [] (* multicasting messages; will block until successful *) [req eq MULTICAST] -> Req_Multicast[inter_ch, out_ch](sender, msg, id, mbrL, infos) ) where process Req_DeleteGroup[inter_ch, out_ch](sender: MID, msg: Msg, id:GID, mbrL:MemberList, infos:msg) :exit:= [not(IsAdmin(infos)) or (Admin(infos) eq sender)] -> ( (* Inform members other than sender *) Multicast[inter_ch](sender,Encode(GROUPWASDELETED), RemoveMBR(sender, mbrL), false)>> inter_ch !sender !GROUPDELETED; inter_ch !GROUPDELETED; exit ) [] [IsAdmin(infos) and (Admin(infos) ne sender)] -> inter_ch !sender !NOTADMINMODER; GCS[inter_ch, out_ch](id, mbrL, infos) endproc (* Req_DeleteGroup *) process Req_Members[inter_ch, out_ch](sender: MID, msg: Msg, id:GID, mbrL:MemberList, infos:msg) :exit:= (* Check if group is private *) [not(IsPrivate(infos)) or (IsPrivate(infos) and (sender IsIn MembersOnly(mbrL)))] -> inter_ch !sender !MembersAre(MembersOnly(mbrL)); GCS[inter_ch, out_ch](id, mbrL, infos) [] [IsPrivate(infos) and (sender NotIn MembersOnly(mbrL))] -> inter_ch !sender !MEMBERNOTINGROUP; GCS[inter_ch, out_ch](id, mbrL, infos) endproc (* Req_Members *) 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 !sender !REGISTERED; ( [sender NotIn MembersOnly(mbrl)] -> (* Insert pair MID.CID *) GCS[inter_ch, out_ch] (id, Insert(sender.ChanId(msg), mbrL), infos) [] [sender IsIn MembersOnly(mbrl)] -> (* Modify CID only *) 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 !sender !NOTADMINMODER; GCS[inter_ch, out_ch](id, mbrL, infos) [] [sender eq Admin(infos)] -> (* Admin can register another member in private group *) inter_ch !sender !REGISTERED; ( [NewMember(msg) NotIn MembersOnly(mbrl)] -> (* Insert pair MID.CID *) GCS[inter_ch, out_ch] (id, Insert(NewMember(msg).ChanId(msg), mbrL), infos) [] [NewMember(msg) IsIn MembersOnly(mbrl)] -> (* Modify CID only *) GCS[inter_ch, out_ch] (id, Insert(NewMember(msg).ChanId(msg), RemoveMBR(NewMember(msg),mbrL)), infos) ) ) endproc (* Req_Register *) process Req_DeRegister[inter_ch, out_ch](sender: MID, msg: Msg, id:GID, mbrL:MemberList, infos:msg) :exit:= (* Is sender a member of the group? *) [sender IsIn MembersOnly(mbrL)] -> inter_ch !sender !DEREGISTERED; ( [Card(mbrL) eq succ(0)] -> (* the GCS dies if no member left *) (* We do not need to inform the members... *) inter_ch !sender !GROUPDELETED; inter_ch !GROUPDELETED; exit [] [Card(mbrL) ne succ(0)] -> GCS[inter_ch, out_ch](id, RemoveMBR(sender, mbrL), infos) ) [] [sender NotIn MembersOnly(mbrL)] -> inter_ch !sender !MEMBERNOTINGROUP; GCS[inter_ch, out_ch](id, mbrL, infos) endproc (* Req_DeRegister *) process Req_ChangeModer[inter_ch, out_ch](sender: MID, msg: Msg, id:GID, mbrL:MemberList, infos:msg) :exit:= (* 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 !sender !NOMODERGROUP; GCS[inter_ch, out_ch](id, mbrL, 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 !sender !NOTADMINMODER; GCS[inter_ch, out_ch](id, mbrL, infos) [] (* The sender has the privilege. *) [(IsModerated(infos) and (Moderator(infos) eq sender)) or (IsAdmin(infos) and (Admin(infos) eq sender))] -> ( (* If the group is closed, *) (* then moderator must be a group member *) [not(IsOpened(infos)) and (Moderator(msg) NotIn mbrL)] -> inter_ch !sender !MEMBERNOTINGROUP; GCS[inter_ch, out_ch](id, mbrL, infos) [] [IsOpened(infos) or (Moderator(msg) IsIn mbrL)] -> inter_ch !sender !ADMINMODERCHANGED; GCS[inter_ch, out_ch] (id, mbrL, SetModer(Moderator(msg), IsPrivate(msg), infos)) ) endproc (* Req_ChangeModer *) process Req_ChangeAdmin[inter_ch, out_ch](sender: MID, msg: Msg, id:GID, mbrL:MemberList, infos:msg) :exit:= (* The group does not have an administrator *) [not(IsAdmin(infos))] -> inter_ch !sender !NOADMINGROUP; GCS[inter_ch, out_ch](id, mbrL, infos) [] (* The sender does not have the privilege to change admin *) [IsAdmin(infos) and (Admin(infos) ne sender)] -> inter_ch !sender !NOTADMINMODER; GCS[inter_ch, out_ch](id, mbrL, infos) [] (* The sender has the privilege. *) [IsAdmin(infos) and (Admin(infos) eq sender)] -> ( [Admin(msg) NotIn mbrL] -> inter_ch !sender !MEMBERNOTINGROUP; GCS[inter_ch, out_ch](id, mbrL, infos) [] [Admin(msg) IsIn mbrL] -> inter_ch !sender !ADMINMODERCHANGED; GCS[inter_ch, out_ch] (id, mbrL, SetAdmin(Admin(msg), IsPrivate(msg), infos)) ) endproc (* Req_ChangeAdmin *) 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 (IsModerated(infos) and (sender eq Moderator(infos)))] -> ( Multicast[out_ch](sender, msg, mbrL, true) >> inter_ch !sender !MESSAGESENT; 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 !Moderator(infos) !ToApprove(msg); inter_ch !sender !SENTTOMODERATOR; GCS[inter_ch, out_ch](id, mbrL, infos) ) ) [] [not(IsOpened(infos)) and (sender NotIn MembersOnly(mbrl))]-> ( inter_ch !sender !MEMBERNOTINGROUP; GCS[inter_ch, out_ch](id, mbrL, infos) ) endproc (* Req_Multicast *) endproc (* GCS *) (*************************************************************************** * * Multicast * * Send the message to all subscriber of the group (concurrently). * No other message will be multicast until all members of the group * received it. * ***************************************************************************) process Multicast[out](sender:MID, msg:Msg, mbrL:MemberList, UseChannel: Bool) : exit := [mbrL eq NoMBR] -> exit [] [mbrL ne NoMBR] -> ( ( [UseChannel] -> (* Multicasts message to members on their appropriate data channel *) out !Top(mbrL) !sender !msg; exit [] [Not(UseChannel)] -> (* Use request/ack channel *) out !MID(Top(mbrl)) !GetAck(msg); exit ) ||| Multicast[out](sender, msg, Tail(mbrL), UseChannel) (* loop... *) ) endproc (* Multicast *) (*============================================*) (* Test Cases *) (*============================================*) (* Check group creation and deletion. *) process Test1 [mgcs_ch, gcs_ch, out_ch, success]:noexit := mgcs_ch !0 of MID !CREATEGROUP !a of GID !Encode(Mail, 4, false, Nobody, true, false, false, Nobody); mgcs_ch !0 of MID !GROUPCREATED !a of GID; mgcs_ch !9 of MID !CREATEGROUP !b of GID !Encode(Video, 4, false, Nobody, true, false, false, Nobody); mgcs_ch !9 of MID !GROUPCREATED !b of GID; mgcs_ch !0 of MID !GROUPS; mgcs_ch !0 of MID !Insert(b, Insert(a, NoGCS)); gcs_ch !1 of MID !a of GID !REGISTER !Encode(0 of CID); gcs_ch !1 of MID !REGISTERED !a of GID; mgcs_ch !1 of MID !GROUPS; mgcs_ch !1 of MID !Insert(b, Insert(a, NoGCS)); gcs_ch !1 of MID !a of GID !MEMBERS !NoMsg; gcs_ch !1 of MID !MembersAre(Insert(1, Insert(0, Empty))) !a of GID; gcs_ch !9 of MID !a of GID !DELETEGROUP !NoMsg; ( gcs_ch !0 of MID !GROUPWASDELETED !a of GID; exit ||| gcs_ch !1 of MID !GROUPWASDELETED !a of GID; exit ) >> gcs_ch !9 of MID !GROUPDELETED !a of GID; mgcs_ch !1 of MID !GROUPS; mgcs_ch !1 of MID !Insert(b, NoGCS); success; stop endproc (* Test1 *) (* Check group administration. *) process Test2 [mgcs_ch, gcs_ch, out_ch, success]:noexit := mgcs_ch !0 of MID !CREATEGROUP !a of GID !Encode(Mail, 4, true, 0, true, false, false, Nobody); (* NOTE: We should not have to indicate the admin. *) mgcs_ch !0 of MID !GROUPCREATED !a of GID; mgcs_ch !1 of MID !CREATEGROUP !b of GID !Encode(Text, 4, true, 1, true, false, false, Nobody); mgcs_ch !1 of MID !GROUPCREATED !b of GID; mgcs_ch !9 of MID !CREATEGROUP !c of GID !Encode(Video, 4, false, Nobody, true, false, false, Nobody); mgcs_ch !9 of MID !GROUPCREATED !c of GID; mgcs_ch !0 of MID !GROUPS; mgcs_ch !0 of MID !Insert(c, Insert(b, Insert(a, NoGCS))); gcs_ch !2 of MID !a of GID !REGISTER !Encode(0 of CID); gcs_ch !2 of MID !REGISTERED !a of GID; gcs_ch !9 of MID !a of GID !DELETEGROUP !NoMsg; gcs_ch !9 of MID !NOTADMINMODER !a of GID; gcs_ch !1 of MID !b of GID !DELETEGROUP !NoMsg; gcs_ch !1 of MID !GROUPDELETED !b of GID; gcs_ch !1 of MID !a of GID !CHANGEADMIN !Encode(2 of MID, false); gcs_ch !1 of MID !NOTADMINMODER !a of GID; gcs_ch !2 of MID !a of GID !CHANGEADMIN !Encode(2 of MID, false); gcs_ch !2 of MID !NOTADMINMODER !a of GID; gcs_ch !0 of MID !a of GID !CHANGEADMIN !Encode(1 of MID, false); gcs_ch !0 of MID !MEMBERNOTINGROUP !a of GID; gcs_ch !0 of MID !a of GID !CHANGEADMIN !Encode(2 of MID, false); gcs_ch !0 of MID !ADMINMODERCHANGED !a of GID; mgcs_ch !0 of MID !GROUPS; mgcs_ch !0 of MID !Insert(c, Insert(a, NoGCS)); gcs_ch !2 of MID !a of GID !CHANGEADMIN !Encode(2 of MID, false); gcs_ch !2 of MID !ADMINMODERCHANGED !a of GID; gcs_ch !0 of MID !a of GID !DELETEGROUP !NoMsg; gcs_ch !0 of MID !NOTADMINMODER !a of GID; gcs_ch !2 of MID !a of GID !DELETEGROUP !NoMsg; gcs_ch !0 of MID !GROUPWASDELETED !a of GID; gcs_ch !2 of MID !GROUPDELETED !a of GID; mgcs_ch !0 of MID !GROUPS; mgcs_ch !0 of MID !Insert(c, NoGCS); gcs_ch !9 of MID !c of GID !CHANGEADMIN !Encode(2 of MID, false); gcs_ch !9 of MID !NOADMINGROUP !c of GID; (* Make this group administered and private *) mgcs_ch !5 of MID !CREATEGROUP !d of GID !Encode(Audio, 4, true, 5, true, true, false, Nobody); mgcs_ch !5 of MID !GROUPCREATED !d of GID; gcs_ch !2 of MID !d of GID !REGISTER !Encode(0 of CID); gcs_ch !2 of MID !NOTADMINMODER !d of GID; gcs_ch !5 of MID !d of GID !REGISTER !Encode(6 of MID, 7 of CID); gcs_ch !5 of MID !REGISTERED !d of GID; gcs_ch !9 of MID !d of GID !MEMBERS !NoMsg; gcs_ch !9 of MID !MEMBERNOTINGROUP !d of GID ; gcs_ch !5 of MID !d of GID !MEMBERS !NoMsg; gcs_ch !5 of MID !MembersAre(Insert(6, Insert(5, Empty))) !d of GID; success; stop endproc (* Test2 *) (* Check multicasting *) process Test3 [mgcs_ch, gcs_ch, out_ch, success]:noexit := mgcs_ch !0 of MID !CREATEGROUP !a of GID !Encode(Mail, 0, false, Nobody, true, false, false, Nobody); mgcs_ch !0 of MID !GROUPCREATED !a of GID; gcs_ch !1 of MID !a of GID !REGISTER !Encode(0 of CID); gcs_ch !1 of MID !REGISTERED !a of GID; gcs_ch !2 of MID !a of GID !REGISTER !Encode(0 of CID); gcs_ch !2 of MID !REGISTERED !a of GID; gcs_ch !9 of MID !a of GID !MEMBERS !NoMsg; gcs_ch !9 of MID !MembersAre(Insert(2, Insert(1, Insert(0, Empty)))) !a of GID; gcs_ch !7 of MID !a of GID !MULTICAST !Encode(Hello); (* NOTE: All CIDs are 0 by default for the moment *) out_ch !0.0 !7 of MID !Encode(Hello); (* any order! *) out_ch !2.0 !7 of MID !Encode(Hello); out_ch !1.0 !7 of MID !Encode(Hello); gcs_ch !7 of MID !MESSAGESENT !a of GID; gcs_ch !9 of MID !a of GID !DELETEGROUP !NoMsg; (* Each member is informed *) ( gcs_ch !1 of MID !GROUPWASDELETED !a of GID; exit (* any order! *) ||| gcs_ch !2 of MID !GROUPWASDELETED !a of GID; exit ||| gcs_ch !0 of MID !GROUPWASDELETED !a of GID; exit ) >> gcs_ch !9 of MID !GROUPDELETED !a of GID; mgcs_ch !1 of MID !GROUPS; mgcs_ch !1 of MID !NoGCS; success; stop endproc (* Test3 *) (* More realistic scenario, with all data (even if not used) *) process Test4 [mgcs_ch, gcs_ch, out_ch, success]:noexit := (* Create group A, administered by 0. CID of member 0 is 4. *) mgcs_ch !0 of MID !CREATEGROUP !A of GID !Encode(Mail, 4, true, 0, true, false, false, 0); mgcs_ch !0 of MID !GROUPCREATED !A of GID; (* 1 joins A on its CID 8 *) gcs_ch !1 of MID !a of GID !REGISTER !Encode(8 of CID); gcs_ch !1 of MID !REGISTERED !a of GID; (* 2 joins A on its CID 2 *) gcs_ch !2 of MID !a of GID !REGISTER !Encode(2 of CID); gcs_ch !2 of MID !REGISTERED !a of GID; (* List members of group A *) gcs_ch !9 of MID !a of GID !MEMBERS !NoMsg; gcs_ch !9 of MID !MembersAre(Insert(2, Insert(1, Insert(0, Empty)))) !a of GID; (* 7 multicasts a Hello message on group A *) gcs_ch !7 of MID !a of GID !MULTICAST !Encode(Hello); out_ch !0.4 !7 of MID !Encode(Hello); (* any order! *) out_ch !2.2 !7 of MID !Encode(Hello); out_ch !1.8 !7 of MID !Encode(Hello); gcs_ch !7 of MID !MESSAGESENT !a of GID; (* 2 tries to destroy the administred group A *) gcs_ch !2 of MID !a of GID !DELETEGROUP !NoMsg; gcs_ch !2 of MID !NOTADMINMODER !a of GID; (* 0 decides to destroy the administred group A *) gcs_ch !0 of MID !a of GID !DELETEGROUP !NoMsg; (* Each other member is informed *) ( gcs_ch !2 of MID !GROUPWASDELETED !a of GID; exit (* any order! *) ||| gcs_ch !1 of MID !GROUPWASDELETED !a of GID; exit ) >> gcs_ch !0 of MID !GROUPDELETED !a of GID; (* List the remaining groups *) mgcs_ch !1 of MID !GROUPS; mgcs_ch !1 of MID !NoGCS; success; stop endproc (* Test4 *) (* Check possible deadlocks with DoubleBuffer *) process Test5 [mgcs_ch, gcs_ch, out_ch, success]:noexit := (* Create group A, administered by 0. CID of member 0 is 4. *) mgcs_ch !0 of MID !CREATEGROUP !a of GID !Encode(Mail, 4, true, 0, false, false, false, 0); mgcs_ch !0 of MID !GROUPCREATED !a of GID; (* 9 lists members of group A *) gcs_ch !9 of MID !a of GID !MEMBERS !NoMsg; (* so does 8 right after... *) gcs_ch !8 of MID !a of GID !MEMBERS !NoMsg; (* In theory, we should have this, but Listen will deadlock... *) ( gcs_ch !9 of MID !MembersAre(Insert(0, Empty)) !a of GID; exit ||| gcs_ch !8 of MID !MembersAre(Insert(0, Empty)) !a of GID; exit ) >> success; stop endproc (* Test5 *) (* Test Opened/closed, with all data *) process Test6 [mgcs_ch, gcs_ch, out_ch, success]:noexit := (* Create Closed group A, administered by 0. CID of member 0 is 4. *) mgcs_ch !0 of MID !CREATEGROUP !A of GID !Encode(Mail, 4, true, 0, false, false, false, 0); mgcs_ch !0 of MID !GROUPCREATED !A of GID; (* 1 joins A on its CID 8 *) gcs_ch !1 of MID !a of GID !REGISTER !Encode(8 of CID); gcs_ch !1 of MID !REGISTERED !a of GID; (* Create Opened group B, administered by 2. CID of member 2 is 4. *) mgcs_ch !2 of MID !CREATEGROUP !B of GID !Encode(Mail, 4, true, 0, true, false, false, 0); mgcs_ch !2 of MID !GROUPCREATED !B of GID; (* 3 joins B on its CID 2 *) gcs_ch !3 of MID !b of GID !REGISTER !Encode(2 of CID); gcs_ch !3 of MID !REGISTERED !b of GID; (* 7 multicasts a Hello message on group A (Closed). Should not work. *) gcs_ch !7 of MID !a of GID !MULTICAST !Encode(Hello); gcs_ch !7 of MID !MEMBERNOTINGROUP !a of GID; (* 7 multicasts a Hello message on group B (Opened). Should work. *) gcs_ch !7 of MID !b of GID !MULTICAST !Encode(Hello); out_ch !2.4 !7 of MID !Encode(Hello); (* any order! *) out_ch !3.2 !7 of MID !Encode(Hello); gcs_ch !7 of MID !MESSAGESENT !b of GID; (* 1 multicasts a Hello message on group A (Closed). Should work. *) gcs_ch !1 of MID !a of GID !MULTICAST !Encode(Hello); out_ch !0.4 !1 of MID !Encode(Hello); (* any order! *) out_ch !1.8 !1 of MID !Encode(Hello); gcs_ch !1 of MID !MESSAGESENT !a of GID; (* 2 multicasts a Hello message on group B (Opened). Should work. *) gcs_ch !2 of MID !b of GID !MULTICAST !Encode(Hello); out_ch !3.2 !2 of MID !Encode(Hello); (* any order! *) out_ch !2.4 !2 of MID !Encode(Hello); gcs_ch !2 of MID !MESSAGESENT !b of GID; success; stop endproc (* Test6 *) (* Test Moderator functionalities, with all data *) process Test7 [mgcs_ch, gcs_ch, out_ch, success]:noexit := (* Create Opened/Moderated group A, administered by 0, *) (* moderated by 1. CID of member 0 is 4. *) mgcs_ch !0 of MID !CREATEGROUP !A of GID !Encode(Mail, 4, true, 0, true, false, true, 1); mgcs_ch !0 of MID !GROUPCREATED !A of GID; (* 1 joins A on its CID 8 *) gcs_ch !1 of MID !a of GID !REGISTER !Encode(8 of CID); gcs_ch !1 of MID !REGISTERED !a of GID; (* Create Closed/Unmoderated group B, administered by 2, *) (* CID of member 2 is 4. *) mgcs_ch !2 of MID !CREATEGROUP !B of GID !Encode(Mail, 4, true, 0, false, false, false, Nobody); mgcs_ch !2 of MID !GROUPCREATED !B of GID; (* 3 joins B on its CID 2 *) gcs_ch !3 of MID !b of GID !REGISTER !Encode(2 of CID); gcs_ch !3 of MID !REGISTERED !b of GID; (* 7 multicasts a Hello message on group A (Moderated). *) (* Should be forwarded to Moderator *) gcs_ch !7 of MID !a of GID !MULTICAST !Encode(Hello); gcs_ch !1 of MID !ToApprove(Encode(Hello)) !a of GID; gcs_ch !7 of MID !SENTTOMODERATOR !a of GID; (* 2 multicasts a Hello message on group B (Closed). Should work. *) gcs_ch !2 of MID !b of GID !MULTICAST !Encode(Hello); out_ch !2.4 !2 of MID !Encode(Hello); (* any order! *) out_ch !3.2 !2 of MID !Encode(Hello); gcs_ch !2 of MID !MESSAGESENT !b of GID; (* Moderator (1) multicasts a Hello message on group A (Moderated). *) (* Should work as normal. *) gcs_ch !1 of MID !a of GID !MULTICAST !Encode(Hello); out_ch !0.4 !1 of MID !Encode(Hello); (* any order! *) out_ch !1.8 !1 of MID !Encode(Hello); gcs_ch !1 of MID !MESSAGESENT !a of GID; (* 1 changes moderator to 2 *) gcs_ch !1 of MID !a of GID !CHANGEMODER !Encode(2 of MID, true); gcs_ch !1 of MID !ADMINMODERCHANGED !a of GID; gcs_ch !7 of MID !a of GID !MULTICAST !Encode(Hello); gcs_ch !2 of MID !ToApprove(Encode(Hello)) !a of GID; gcs_ch !7 of MID !SENTTOMODERATOR !a of GID; (* 0 changes moderator to 7 *) gcs_ch !0 of MID !a of GID !CHANGEMODER !Encode(7 of MID, true); gcs_ch !0 of MID !ADMINMODERCHANGED !a of GID; (* 1 tries to change moderator of A to itself, but fails *) gcs_ch !1 of MID !a of GID !CHANGEMODER !Encode(1 of MID, true); gcs_ch !1 of MID !NOTADMINMODER !a of GID; (* 1 tries to change moderator of B to itself, but fails *) gcs_ch !1 of MID !b of GID !CHANGEMODER !Encode(1 of MID, true); gcs_ch !1 of MID !NOMODERGROUP !b of GID; (* Create Closed/Moderated group C, administered by 0, *) (* moderated by 0. CID of member 0 is 4. *) mgcs_ch !0 of MID !CREATEGROUP !C of GID !Encode(Mail, 4, true, 0, false, false, true, 0); mgcs_ch !0 of MID !GROUPCREATED !C of GID; (* Moderator tries to change moderator of C to 1, but fails *) gcs_ch !0 of MID !c of GID !CHANGEMODER !Encode(1 of MID, true); gcs_ch !0 of MID !MEMBERNOTINGROUP !c of GID; (* Admin makes group A moderated *) gcs_ch !0 of MID !a of GID !CHANGEMODER !Encode(1 of MID, true); gcs_ch !0 of MID !ADMINMODERCHANGED !a of GID; gcs_ch !7 of MID !a of GID !MULTICAST !Encode(Hello); gcs_ch !1 of MID !ToApprove(Encode(Hello)) !a of GID; gcs_ch !7 of MID !SENTTOMODERATOR !a of GID; (* Admin makes group A unmoderated again *) gcs_ch !0 of MID !a of GID !CHANGEMODER !Encode(Nobody, false); gcs_ch !0 of MID !ADMINMODERCHANGED !a of GID; gcs_ch !1 of MID !a of GID !CHANGEMODER !Encode(1 of MID, true); gcs_ch !1 of MID !NOMODERGROUP !a of GID; success; stop endproc (* Test7 *) endspec (* GCS, Group Communication Server *)