(* * LOTOS spec of the conference protocol entity * * $Id: cf-pe.lot,v 1.9 1998/12/15 16:46:00 belinfan Exp $ *) specification ConferenceProtocolEntitySpecification[CFSAP_in, CFSAP_out, udp_in, udp_out] : noexit library Element, SetElement, Set, Boolean, FBoolean, NaturalNumber endlib (***************************************************************************************) (****************** standard definitions ***********************************************) (***************************************************************************************) (* definition of queue and operations on queues *) type Queue is SetElement sorts Queue opns empty: -> Queue (* the empty queue *) add: Element, Queue -> Queue (* add element on top of queue *) dda: Element, Queue -> Queue (* add element on bottom of queue *) concat: Queue, Queue -> Queue (* concatenates two queues *) head: Queue -> Element (* gets first element of a queue *) tail: Queue -> Queue (* removes first element of a queue *) last: Queue -> Element (* gets last element of a queue *) init: Queue -> Queue (* removes last element of a queue *) IsEmpty: Queue -> FBool (* receives TRUE when queue is empty *) NotEmpty: Queue -> FBool (* receives TRUE when queue is not empty *) eqns forall x,y,z: Element, q, q1, q2: Queue ofsort Element last(add(x, empty)) = x; last(add(x, add(y, q))) = last(add(y, q)); ofsort Element head(add(x, empty)) = x; head(add(x, add(y, q))) = x; ofsort Queue dda(y, empty) = add(y, empty); dda(y, add(x, empty)) = add(x, add(y, empty)); dda(y, add(x, add(z,q))) = add(x, dda(y, add(z,q))); ofsort Queue tail(empty) = empty; tail(add(x, empty)) = empty; tail(add(x, add(y, q))) = add(y, q); ofsort Queue init(empty) = empty; init(add(x, empty)) = empty; init(add(x, add(y, q))) = add(x, init(add(y, q))); ofsort Queue concat(empty, q) = q; concat(add(y, empty), q) = add(y, q); concat(add(y, add(z,q1)), q2) = add(y, add(z, concat(q1, q2))); ofsort FBool IsEmpty(empty) = true; IsEmpty(add(x, q)) = not(true); NotEmpty(q) = not(IsEmpty(q)); endtype (* definition of the second element for use in the definition of pair *) type SndElement is SetElement renamedby sortnames SndElement for Element endtype (* definition of a pair (2-tuple) and operations on pairs *) type Pair is SetElement, SndElement, NaturalNumber sorts Pair opns fst : Pair -> Element snd : Pair -> SndElement _eq_ : Pair, Pair -> FBool _ne_ : Pair, Pair -> FBool _lt_ : Pair, Pair -> FBool Pair : Element, SndElement -> Pair eqns forall e1 : Element, e2 : SndElement, p1, p2 : Pair ofsort Element fst(Pair(e1, e2)) = e1; ofsort SndElement snd(Pair(e1, e2)) = e2; ofsort FBool fst(p1) ne fst(p2) => p1 ne p2 = true; not(fst(p1) ne fst(p2)) => p1 ne p2 = snd(p1) ne snd(p2); p1 eq p2 = not(p1 ne p2); fst(p1) ne fst(p2) => p1 lt p2 = fst(p1) lt fst(p2); fst(p1) eq fst(p2) => p1 lt p2 = snd(p1) lt snd(p2); endtype (***************************************************************************************) (******************* type definitions **************************************************) (***************************************************************************************) (* definition of PDU field: PDU-type *) type PduType is NaturalNumber, Boolean sorts PduType opns J, A, L, D : -> PduType (* the PDU types *) _eq_, _ne_, _lt_ : PduType, PduType -> Bool NatNum : PduType -> Nat eqns forall x, y : PduType ofsort Nat NatNum(J) = 0; NatNum(L) = succ(NatNum(J)); NatNum(A) = succ(NatNum(L)); NatNum(D) = succ(NatNum(A)); ofsort Bool x eq y = NatNum(x) eq NatNum(y); x ne y = NatNum(x) ne NatNum(y); x lt y = NatNum(x) lt NatNum(y); endtype (* type definition of CF-SAP addresses *) type CFAddress is NaturalNumber, Boolean sorts CFAddress opns _eq_, _ne_, _lt_ : CFAddress, CFAddress -> Bool NatNum : CFAddress -> Nat eqns forall x,y : CFAddress ofsort Bool x eq y = NatNum(x) eq NatNum(y); x ne y = NatNum(x) ne NatNum(y); x lt y = NatNum(x) lt NatNum(y); endtype (* type definition of UDP-SAP addresses *) type UDPAddress is NaturalNumber, Boolean sorts UDPAddress opns _eq_, _ne_, _lt_ : UDPAddress, UDPAddress -> Bool NatNum : UDPAddress -> Nat eqns forall x,y : UDPAddress ofsort Bool x eq y = NatNum(x) eq NatNum(y); x ne y = NatNum(x) ne NatNum(y); x lt y = NatNum(x) lt NatNum(y); endtype (* type definition of SP parameter: User Title *) type UserTitle is NaturalNumber, Boolean sorts UserTitle opns _eq_, _ne_, _lt_ : UserTitle, UserTitle -> Bool NatNum : UserTitle -> Nat eqns forall x, y : UserTitle ofsort Bool x eq y = NatNum(x) eq NatNum(y); x ne y = NatNum(x) ne NatNum(y); x lt y = NatNum(x) lt NatNum(y); endtype (* type definition of locally stored SP parameter: User Title *) type UserTitleOpt is NaturalNumber, Boolean, UserTitle sorts UserTitleOpt opns _eq_, _ne_, _lt_ : UserTitleOpt, UserTitleOpt -> Bool NatNum : UserTitleOpt -> Nat noUt : -> UserTitleOpt yesUt : UserTitle -> UserTitleOpt UtOf : UserTitleOpt -> UserTitle eqns forall x, y : UserTitleOpt, z : UserTitle ofsort Bool x eq y = NatNum(x) eq NatNum(y); x ne y = NatNum(x) ne NatNum(y); x lt y = NatNum(x) lt NatNum(y); ofsort Nat NatNum(noUt) = 0; NatNum(yesUt(z)) = Succ(0); ofsort UserTitle UtOf(yesUt(z)) = z; endtype (* type definition of SP parameter: Conference Identifier *) type ConfIdent is NaturalNumber, Boolean sorts ConfIdent opns _eq_, _ne_, _lt_ : ConfIdent, ConfIdent -> Bool NatNum : ConfIdent -> Nat eqns forall x, y : ConfIdent ofsort Bool x eq y = NatNum(x) eq NatNum(y); x ne y = NatNum(x) ne NatNum(y); x lt y = NatNum(x) lt NatNum(y); endtype (* type definition of locally stored SP parameter: Conference Identifier *) type ConfIdentOpt is NaturalNumber, Boolean, ConfIdent sorts ConfIdentOpt opns _eq_, _ne_, _lt_ : ConfIdentOpt, ConfIdentOpt -> Bool NatNum : ConfIdentOpt -> Nat noCi : -> ConfIdentOpt yesCi : ConfIdent -> ConfIdentOpt CiOf : ConfIdentOpt -> ConfIdent eqns forall x, y : ConfIdentOpt, z : ConfIdent ofsort Bool x eq y = NatNum(x) eq NatNum(y); x ne y = NatNum(x) ne NatNum(y); x lt y = NatNum(x) lt NatNum(y); ofsort Nat NatNum(noCi) = 0; NatNum(yesCi(z)) = Succ(0); ofsort ConfIdent CiOf(yesCi(z)) = z; endtype (* type definition of SP parameter: Data Field Length *) type DataFieldLen is NaturalNumber, Boolean sorts DataFieldLen opns _eq_, _ne_, _lt_ : DataFieldLen, DataFieldLen -> Bool NatNum : DataFieldLen -> Nat eqns forall x, y : DataFieldLen ofsort Bool x eq y = NatNum(x) eq NatNum(y); x ne y = NatNum(x) ne NatNum(y); x lt y = NatNum(x) lt NatNum(y); endtype (* type definition of SP parameter: Data Field *) type DataField is NaturalNumber, Boolean sorts DataField opns _eq_, _ne_, _lt_ : DataField, DataField -> Bool NatNum : DataField -> Nat eqns forall x, y : DataField ofsort Bool x eq y = NatNum(x) eq NatNum(y); x ne y = NatNum(x) ne NatNum(y); x lt y = NatNum(x) lt NatNum(y); endtype (* type definition of SP parameter: Message *) (* type Message is NaturalNumber, Boolean sorts Message opns _eq_, _ne_, _lt_ : Message, Message -> Bool NatNum : Message -> Nat eqns forall x, y : Message ofsort Bool x eq y = NatNum(x) eq NatNum(y); x ne y = NatNum(x) ne NatNum(y); x lt y = NatNum(x) lt NatNum(y); endtype *) (********************************************************************************************) (****************** Definition of Service Primitives and PDUs *******************************) (********************************************************************************************) (* definition of conference service SPs and operations on these SPs *) type ConfServPrim is (* Message, *) UserTitle, ConfIdent, DataField, NaturalNumber, Boolean sorts CFsp opns (* datareq : Message -> CFsp *) datareq : DataField -> CFsp (* datareq(message) *) dataind : UserTitle, DataField -> CFsp (* dataind(user title, message) *) (* dataind : UserTitle, Message -> CFsp *) join : UserTitle, ConfIdent -> CFsp (* join(user title, conference identifier) *) leave : -> CFsp (* leave() *) IsDataReq : CFsp -> Bool (* discriminate datareq SP *) IsDataInd : CFsp -> Bool (* discriminate dataind SP *) IsJoin : CFsp -> Bool (* discriminate join SP *) IsLeave : CFsp -> Bool (* discriminate leave SP *) MsgOf : CFsp -> DataField (* get message from datareq and dataind SPs *) (* MsgOf : CFsp -> Message *) UtOf : CFsp -> UserTitle (* get user title from join and dataind SPs *) CiOf : CFsp -> ConfIdent (* get conference identifier from join SP *) _eq_, _ne_, _lt_ : CFsp, CFsp -> Bool (* NatNum : CFsp -> Nat *) eqns forall (* m:Message, *) u, v:UserTitle, c, d:ConfIdent, m, n :DataField, sp1, sp2:CFsp ofsort Bool IsDataReq(datareq(m)) = true; IsDataReq(dataind(u, m)) = false; IsDataReq(join(u, c)) = false; IsDataReq(leave) = false; IsDataInd(datareq(m)) = false; IsDataInd(dataind(u, m)) = true; IsDataInd(join(u, c)) = false; IsDataInd(leave) = false; IsJoin(datareq(m)) = false; IsJoin(dataind(u, m)) = false; IsJoin(join(u, c)) = true; IsJoin(leave) = false; IsLeave(datareq(m)) = false; IsLeave(dataind(u, m)) = false; IsLeave(join(u, c)) = false; IsLeave(leave) = true; ofsort (* Message *) DataField MsgOf(datareq(m)) = m; MsgOf(dataind(u, m)) = m; ofsort UserTitle UtOf(dataind(u, m)) = u; UtOf(join(u, c)) = u; ofsort ConfIdent CiOf(join(u, c)) = c; ofsort Bool (* sp1 eq sp2 = NatNum(sp1) eq NatNum(sp2); sp1 ne sp2 = NatNum(sp1) ne NatNum(sp2); sp1 lt sp2 = NatNum(sp1) lt NatNum(sp2); *) datareq(m) eq datareq(n) = m eq n; dataind(u,m) eq dataind(v,n) = (m eq n) and (u eq v); join(u,c) eq join(v,d) = (c eq d) and (u eq v); leave eq leave = True; datareq(m) eq dataind(v,n) = False; datareq(m) eq join(v,d) = False; datareq(m) eq leave = False; dataind(u,m) eq datareq(n) = False; dataind(u,m) eq join(v,d) = False; dataind(u,m) eq leave = False; join(u,c) eq datareq(n) = False; join(u,c) eq dataind(v,n) = False; join(u,c) eq leave = False; leave eq datareq(n) = False; leave eq dataind(v,n) = False; leave eq join(v,d) = False; datareq(m) lt datareq(n) = m lt n; dataind(u,m) lt dataind(v,n) = (m lt n) and (u lt v); join(u,c) lt join(v,d) = (c lt d) and (u lt v); leave lt leave = False; datareq(m) lt dataind(v,n) = True; datareq(m) lt join(v,d) = True; datareq(m) lt leave = True; dataind(u,m) lt datareq(n) = False; dataind(u,m) lt join(v,d) = True; dataind(u,m) lt leave = True; join(u,c) lt datareq(n) = False; join(u,c) lt dataind(v,n) = False; join(u,c) lt leave = True; leave lt datareq(n) = False; leave lt dataind(v,n) = False; leave lt join(v,d) = False; sp1 ne sp2 = not ( sp1 eq sp2 ); endtype (* ConfServPrim *) (* definition of PDUs and operations on these PDUs *) type PDU is PduType, UserTitle, ConfIdent, DataField, DataFieldLen, Boolean sorts PDU opns PDU_J : UserTitle, ConfIdent -> PDU PDU_A : UserTitle, ConfIdent -> PDU PDU_L : UserTitle, ConfIdent -> PDU PDU_D : DataFieldLen, DataField -> PDU TypeOf : PDU -> PduType UtOf : PDU -> UserTitle CiOf : PDU -> ConfIdent DataFieldOf : PDU -> DataField DataFieldLenOf : PDU -> DataFieldLen _eq_, _ne_, _lt_ : PDU, PDU -> Bool eqns forall t:PduType, u,v:UserTitle, c,cc:ConfIdent, df,df1,df2:DataField, dl,dl1,dl2:DataFieldLen, p1, p2 : PDU ofsort PduType TypeOf(PDU_J(u, c)) = J; TypeOf(PDU_L(u, c)) = L; TypeOf(PDU_A(u, c)) = A; TypeOf(PDU_D(dl, df)) = D; ofsort UserTitle UtOf(PDU_J(u, c)) = u; UtOf(PDU_L(u, c)) = u; UtOf(PDU_A(u, c)) = u; ofsort ConfIdent CiOf(PDU_J(u, c)) = c; CiOf(PDU_L(u, c)) = c; CiOf(PDU_A(u, c)) = c; ofsort DataField DataFieldOf(PDU_D(dl, df)) = df; ofsort DataFieldLen DataFieldLenOf(PDU_D(dl, df)) = dl; ofsort Bool (* p1 eq p2 = TypeOf(p1) eq TypeOf(p2); p1 ne p2 = TypeOf(p1) ne TypeOf(p2); p1 lt p2 = TypeOf(p1) lt TypeOf(p2); *) PDU_J(u,c) eq PDU_J(v,cc) = (c eq cc) and (u eq v); PDU_A(u,c) eq PDU_A(v,cc) = (c eq cc) and (u eq v); PDU_L(u,c) eq PDU_L(v,cc) = (c eq cc) and (u eq v); PDU_D(dl1,df1) eq PDU_D(dl2,df2) = (dl1 eq dl2) and (df1 eq df2); PDU_J(u,c) eq PDU_A(v,cc) = False; PDU_J(u,c) eq PDU_L(v,cc) = False; PDU_J(u,c) eq PDU_D(dl2,df2) = False; PDU_A(u,c) eq PDU_J(v,cc) = False; PDU_A(u,c) eq PDU_L(v,cc) = False; PDU_A(u,c) eq PDU_D(dl2,df2) = False; PDU_L(u,c) eq PDU_J(v,cc) = False; PDU_L(u,c) eq PDU_A(v,cc) = False; PDU_L(u,c) eq PDU_D(dl2,df2) = False; PDU_D(dl1,df1) eq PDU_J(v,cc) = False; PDU_D(dl1,df1) eq PDU_A(v,cc) = False; PDU_D(dl1,df1) eq PDU_L(v,cc) = False; PDU_J(u,c) lt PDU_J(v,cc) = (u lt v) and (c lt cc); PDU_A(u,c) lt PDU_A(v,cc) = (u lt v) and (c lt cc); PDU_L(u,c) lt PDU_L(v,cc) = (u lt v) and (c lt cc); PDU_D(dl1,df1) lt PDU_D(dl2,df2) = (dl1 lt dl2) and (df1 lt df2); PDU_J(u,c) lt PDU_A(u,cc) = True; PDU_J(u,c) lt PDU_L(v,cc) = True; PDU_J(u,c) lt PDU_D(dl2,df2) = True; PDU_A(u,c) lt PDU_J(v,cc) = False; PDU_A(u,c) lt PDU_L(v,cc) = True; PDU_A(u,c) lt PDU_D(dl2,df2) = True; PDU_L(u,c) lt PDU_J(v,cc) = False; PDU_L(u,c) lt PDU_A(v,cc) = False; PDU_L(u,c) lt PDU_D(dl2,df2) = True; PDU_D(dl1,df1) lt PDU_J(v,cc) = False; PDU_D(dl1,df1) lt PDU_A(v,cc) = False; PDU_D(dl1,df1) lt PDU_L(v,cc) = False; p1 ne p2 = not ( p1 eq p2 ); endtype (* PDU *) (* definition of conference service SPs and operations on these SPs *) type UdpServPrim is PDU, UDPAddress, Boolean, NaturalNumber sorts UDPsp opns udp_datareq : UDPAddress, PDU -> UDPsp udp_dataind : UDPAddress, PDU -> UDPsp IsDataReq : UDPsp -> Bool IsDataInd : UDPsp -> Bool PduOf : UDPsp -> PDU SrcOf : UDPsp -> UDPAddress DestOf : UDPsp -> UDPAddress _eq_, _ne_, _lt_ : UDPsp, UDPsp -> Bool (* NatNum : UDPsp -> Nat *) eqns forall sp, sp1, sp2:UDPsp, a:UDPAddress, p:PDU, b:UDPAddress, q:PDU ofsort Bool IsDataReq(udp_datareq(a,p)) = true; IsDataReq(udp_dataind(a,p)) = false; IsDataInd(sp) = not(IsDataReq(sp)); ofsort PDU PduOf(udp_datareq(a,p)) = p; PduOf(udp_dataind(a,p)) = p; ofsort UDPAddress DestOf(udp_datareq(a,p)) = a; DestOf(udp_dataind(a,p)) = a; SrcOf(udp_datareq(a,p)) = a; SrcOf(udp_dataind(a,p)) = a; ofsort Bool (* sp1 eq sp2 = NatNum(sp1) eq NatNum(sp2); sp1 ne sp2 = NatNum(sp1) ne NatNum(sp2); sp1 lt sp2 = NatNum(sp1) lt NatNum(sp2); *) udp_datareq(a,p) eq udp_datareq(b,q) = (a eq b) and (p eq q); udp_dataind(a,p) eq udp_dataind(b,q) = (a eq b) and (p eq q); udp_datareq(a,p) eq udp_dataind(b,q) = False; udp_dataind(a,p) eq udp_datareq(b,q) = False; udp_datareq(a,p) ne udp_datareq(b,q) = (a ne b) or (p ne q); udp_dataind(a,p) ne udp_dataind(b,q) = (a ne b) or (p ne q); udp_datareq(a,p) ne udp_dataind(b,q) = True; udp_dataind(a,p) ne udp_datareq(b,q) = True; udp_datareq(a,p) lt udp_datareq(b,q) = (a lt b) and (p lt q); udp_dataind(a,p) lt udp_dataind(b,q) = (a lt b) and (p lt q); udp_datareq(a,p) lt udp_dataind(b,q) = True; udp_dataind(a,p) lt udp_datareq(b,q) = False; endtype (* UdpServPrim *) (********************************************************************************************) (***************************** Sets and Queues **********************************************) (********************************************************************************************) (* definition of an address-pair; consists of a CFAddress and a UDPAddress *) type AddressPair is Pair actualizedby CFAddress, UDPAddress using sortnames AddressPair for Pair CFAddress for Element UDPAddress for SndElement Bool for FBool opnnames CFaddrOf for fst UDPaddrOf for snd endtype (* definition of an address-pair-set; used for configuration set *) type AddressPairSet is Set actualizedby AddressPair using sortnames AddressPairSet for Set AddressPair for Element Bool for FBool endtype (* extending the defintion of an address-pair-set *) type ExtAddressPairSet is AddressPairSet, AddressPair, Boolean opns NotEmpty : AddressPairSet -> Bool IsEmpty : AddressPairSet -> Bool eqns forall x:AddressPair, xs:AddressPairSet ofsort Bool NotEmpty(xs) = xs ne {}; IsEmpty(xs) = xs eq {}; endtype (* definition of a conference partner set item: pair of UDPAddress and user title *) type CFPartner is Pair actualizedby UDPAddress, UserTitle using sortnames CFPartner for Pair UDPAddress for Element UserTitle for SndElement Bool for FBool opnnames AddrOf for fst UtOf for snd endtype (* type definition of a conference partners set *) type CFPartnerSet is Set actualizedby CFPartner using sortnames CFPartnerSet for Set CFPartner for Element Bool for FBool opnnames emptyCPS for {} endtype (* extending the defintion of a conference partners set *) type ExtCFPartnerSet is CFPartnerSet, Boolean opns NotEmpty : CFPartnerSet -> Bool IsEmpty : CFPartnerSet -> Bool eqns forall xs:CFPartnerSet ofsort Bool NotEmpty(xs) = xs ne emptyCPS; IsEmpty(xs) = xs eq emptyCPS; endtype (* definition of an operation to check the existence of an UDP address in a *) (* conference partners set *) type IsConferencePartner is CFPartnerSet, CFPartner, UserTitle, UDPAddress, Boolean opns _ IsUDPaddrIn _ : UDPAddress, CFPartnerSet -> Bool eqns forall a, b : UDPAddress, xs:CFPartnerSet, u:UserTitle ofsort Bool a eq b => a IsUDPaddrIn Insert_1(Pair(b, u), xs) = true; a ne b => a IsUDPaddrIn Insert_1(Pair(b, u), xs) = a IsUDPaddrIn xs; a IsUDPaddrIn emptyCPs = false; endtype (* definition of an operation to remove the element in a * conference partner set with a given UDP address. * NOTE: we could have defined a GetPartnerByUDPaddr to get the * conference partner with the given UDPaddr, and then removed it * using the usual Remove on CFPartnerSet, except for the problem * that we then would need a 'null' or 'bottom' CFPartner, that can * be the result of * GetPartnerByUDPaddr(anyUDPaddr, emptyCPs) * For this RemovePartnerByUDPaddr operation we do not need this * 'bottom' element. *) type RemoveConferencePartner is CFPartnerSet, CFPartner, UserTitle, UDPAddress opns RemovePartnerByUDPaddr : UDPAddress, CFPartnerSet -> CFPartnerSet eqns forall a, b : UDPAddress, xs:CFPartnerSet, u:UserTitle ofsort CFPartnerSet a eq b => RemovePartnerByUDPaddr(a, Insert_1(Pair(b, u), xs)) = xs; a ne b => RemovePartnerByUDPaddr(a, Insert_1(Pair(b, u), xs)) = RemovePartnerByUDPaddr(a, xs); RemovePartnerByUDPaddr(a, emptyCPs) = emptyCPs; endtype (***************************************************************************************) (* definition of a queue for UDP SPs *) type UDPspQueue is Queue actualizedby UdpServPrim using sortnames UDPspQ for Queue UDPsp for Element Bool for FBool opnnames emptyUDPspQ for empty endtype (* definition of a queue for output (i.e. CF SPs) at the upper SAP *) type UpperOutQueue is Queue actualizedby ConfServPrim using sortnames UOQ for Queue CFsp for Element Bool for FBool opnnames emptyUOQ for empty endtype (* definition of a queue for output at the lower SAP *) type LowerOutQueue is Queue actualizedby LowerOutQueueItem using sortnames LOQ for Queue LOQItem for Element Bool for FBool opnnames emptyLOQ for empty endtype (* definition of an output-item of the queue for output at the lower SAP *) type LowerOutQueueItem is Pair actualizedby UDPaddrSet, PDU using sortnames LOQItem for Pair UDPaddrSet for Element PDU for SndElement Bool for FBool opnnames AddrSetOf for fst PduOf for snd endtype (* type definition of a set of UDP addresses; used to contain the destination *) (* addresses for PDUs to be send, which is an element of the output-item of a *) (* queue for output at the lower SAP. *) type UDPaddrSet is Set actualizedby UDPAddress using sortnames UDPaddrSet for Set UDPAddress for Element Bool for FBool opnnames noUDPaddr for {} endtype (* extending the defintion of a UDP addresses set *) type ExtUDPaddrSet is UDPaddrSet, Boolean opns NotEmpty : UDPaddrSet -> Bool IsEmpty : UDPaddrSet -> Bool eqns forall xs:UDPaddrSet ofsort Bool NotEmpty(xs) = xs ne noUDPaddr; IsEmpty(xs) = xs eq noUDPaddr; endtype (* definition of operations to derive remote UDP addresses from the conference *) (* partners set and from the configuration set. *) type MakeRemoteAddrSet is ExtCFPartnerSet, UDPaddrSet, ExtAddressPairSet, AddressPair opns MakeRemoteAddrSet : CFPartnerSet -> UDPaddrSet MakeRemoteAddrSet2 : UDPAddress, AddressPairSet -> UDPaddrSet eqns forall u:UDPAddress, x:CFPartner, xs:CFPartnerSet, y:AddressPair, ys:AddressPairSet ofsort UDPaddrSet MakeRemoteAddrSet(Insert_1(x, xs)) = Insert_1(AddrOf(x), MakeRemoteAddrSet(xs)); MakeRemoteAddrSet(emptyCPS) = noUDPaddr; ofsort UDPaddrSet MakeRemoteAddrSet2(u, {}) = noUDPaddr; u ne UDPaddrOf(y) => MakeRemoteAddrSet2(u, Insert_1(y, ys)) = Insert_1(UDPaddrOf(y), MakeRemoteAddrSet2(u, ys)); u eq UDPaddrOf(y) => MakeRemoteAddrSet2(u, Insert_1(y, ys)) = MakeRemoteAddrSet2(u, ys); endtype (****************************************************************************************) (******************** constant definitions for simulation only **************************) (****************************************************************************************) type Data is DataField opns m1 : -> DataField m2 : -> DataField m3 : -> DataField m4 : -> DataField eqns ofsort Nat NatNum(m1) = 0; NatNum(m2) = succ(NatNum(m1)); NatNum(m3) = succ(NatNum(m2)); NatNum(m4) = succ(NatNum(m3)); endtype type UserTitleInst is UserTitle, NaturalNumber opns ut_A : -> UserTitle ut_B : -> UserTitle ut_C : -> UserTitle ut_D : -> UserTitle eqns ofsort Nat NatNum(ut_A) = 0; NatNum(ut_B) = succ(NatNum(ut_A)); NatNum(ut_C) = succ(NatNum(ut_B)); NatNum(ut_D) = succ(NatNum(ut_C)); endtype type ConferenceIdentifiers is ConfIdent, NaturalNumber opns ci_one : -> ConfIdent ci_two : -> ConfIdent eqns ofsort Nat NatNum(ci_one) = 0; NatNum(ci_two) = succ(NatNum(ci_one)); endtype type DataFieldLenInst is DataFieldLen, NaturalNumber opns l : -> DataFieldLen eqns ofsort Nat NatNum(l) = 0; endtype type CFAddressInst is CFAddress, NaturalNumber, Boolean opns cf4, cf2, cf3, cf1 : -> CFAddress eqns forall x,y : CFAddress ofsort Nat NatNum(cf1) = 0; NatNum(cf2) = succ(NatNum(cf1)); NatNum(cf3) = succ(NatNum(cf2)); NatNum(cf4) = succ(NatNum(cf3)); endtype type UDPAddressInst is UDPAddress, NaturalNumber, Boolean opns udp1, udp2, udp3, udp4 : -> UDPAddress eqns forall x,y : UDPAddress ofsort Nat NatNum(udp1) = 0; NatNum(udp2) = succ(NatNum(udp1)); NatNum(udp3) = succ(NatNum(udp2)); NatNum(udp4) = succ(NatNum(udp3)); endtype type ConfigurationSet is AddressPairSet, ExtAddressPairSet, AddressPair, CFAddressInst, UDPAddressInst opns Configurationset : -> AddressPairSet ChooseConfig : AddressPairSet -> AddressPair eqns ofsort AddressPairSet ConfigurationSet = Insert(Pair(cf1, udp1) of AddressPair, Insert(Pair(cf2, udp2) of AddressPair, Insert(Pair(cf3, udp3) of AddressPair, Insert(Pair(cf4, udp4) of AddressPair, {})))); ofsort AddressPair forall r : AddressPairSet, ap:AddressPair ChooseConfig(Insert_1( ap, r)) = ap; endtype (*** type UDPaddrSetInst is UDPaddrSet, UDPAddressInst opns TestSet : -> UDPaddrSet eqns ofsort UDPaddrSet TestSet = Insert(udp1, Insert(udp2, Insert(udp3, noUDPaddr))); endtype type CFPartnerSetInst is CFPartnerSet, CFPartner, UDPAddressInst, UserTitleInst opns ConferencePartners : -> CFPartnerSet eqns ofsort CFPartnerSet ConferencePartners = Insert(Pair(udp1, A), Insert(Pair(udp2, B), Insert(Pair(udp3, C), emptyCPS))); endtype ***) (***************************************************************************************) (******************* End of Abstract Data Type Part ************************************) (***************************************************************************************) behaviour InstallConferenceProtocolEntity[CFSAP_in, CFSAP_out, udp_in, udp_out](ConfigurationSet) where process InstallConferenceProtocolEntity[CFSAP_in, CFSAP_out, udp_in, udp_out](Cfg:AddressPairSet) : noexit := [NotEmpty(Cfg)] -> (* (choice p:AddressPair [] [p IsIn Cfg] -> *) (let p:AddressPair = ChooseConfig(Cfg) in i; (ConferenceProtocolEntity[CFSAP_in, CFSAP_out, udp_in, udp_out](CFaddrOf(p), UDPaddrOf(p)) ) ) where process ConferenceProtocolEntity[CFSAP_in, CFSAP_out, udp_in, udp_out](myCFaddr:CFAddress, myUDPaddr:UDPAddress) : noexit := ( UpperLSI[CFSAP_in, CFSAP_out](myCFaddr) ||| LowerLSI[udp_in, udp_out](myUDPaddr) ) || ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](emptyLOQ of LOQ, emptyUOQ of UOQ, emptyCPS, noUt, noCi, myCFaddr, myUDPaddr) where process UpperLSI[CFSAP_in, CFSAP_out](myCFaddr:CFAddress) : noexit := CFSAP_in ?addr:CFAddress ?sp:CFsp [IsJoin(sp) and (myCFaddr eq addr)]; NextUpperLSI[CFSAP_in, CFSAP_out](myCFaddr) where process NextUpperLSI[CFSAP_in, CFSAP_out](myCFaddr:CFAddress) : noexit := CFSAP_in ?addr:CFAddress ?sp:CFsp [IsDataReq(sp) and (myCFaddr eq addr)]; NextUpperLSI[CFSAP_in, CFSAP_out](myCFaddr) [] CFSAP_out ?addr:CFAddress ?sp:CFsp [IsDataInd(sp) and (myCFaddr eq addr)]; NextUpperLSI[CFSAP_in, CFSAP_out](myCFaddr) [] CFSAP_in ?addr:CFAddress ?sp:CFsp [IsLeave(sp) and (myCFaddr eq addr)]; CFSAP_in ?addr:CFAddress ?sp:CFsp [IsJoin(sp) and (myCFaddr eq addr)]; NextUpperLSI[CFSAP_in, CFSAP_out](myCFaddr) endproc (* NextUpperLSI *) endproc (* UpperLSI *) process LowerLSI[udp_in, udp_out](myUDPaddr:UDPAddress) : noexit := udp_in ?addr:UDPAddress ?sp:UDPsp [IsDataInd(sp) and (myUDPaddr eq addr)]; LowerLSI[udp_in, udp_out](myUDPaddr) [] udp_out ?addr:UDPAddress ?sp:UDPsp [IsDataReq(sp) and (myUDPaddr eq addr)]; LowerLSI[udp_in, udp_out](myUDPaddr) endproc (* LowerLSI *) process ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](Qyo:LOQ, Qxo:UOQ, CPs:CFPartnerSet, myUt:UserTitleOpt, myCi:ConfIdentOpt, myCFaddr:CFAddress, myUDPaddr:UDPAddress) : noexit := CFSAP_in ?addr:CFAddress ?sp:CFsp [addr eq myCFaddr and not(IsDataInd(sp))]; ( [IsJoin(sp)] -> (let myUt:UserTitleOpt = yesUt(UtOf(sp)), myCi:ConfIdentOpt = yesCi(CiOf(sp)), newQyo:LOQ = add(Pair(MakeRemoteAddrSet2(myUDPaddr, ConfigurationSet), PDU_J(UtOf(sp), CiOf(sp))), Qyo) in ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](newQyo, Qxo, CPs, myUt, myCi, myCFaddr, myUDPaddr)) [] [IsLeave(sp)] -> (let newQyo:LOQ = add(Pair(MakeRemoteAddrSet(CPs), PDU_L(UtOf(myUt), CiOf(myCi))), Qyo) in ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](newQyo, Qxo, emptyCPs, noUt, noCi, myCFaddr, myUDPaddr)) [] [IsDataReq(sp)] -> (let newQyo:LOQ = add(Pair(MakeRemoteAddrSet(CPs), PDU_D(l, MsgOf(sp))), Qyo) in ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](newQyo, Qxo, CPs, myUt, myCi, myCFaddr, myUDPaddr)) ) [] udp_in ?addr:UDPAddress ?sp:UDPsp [IsDataInd(sp) and (addr eq myUDPaddr)]; ( [myCi eq noCi] -> ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](Qyo, Qxo, CPs, myUt, myCi, myCFaddr, myUDPaddr) [] [(TypeOf(PduOf(sp)) eq J) and (myCi ne noCi)] -> ( [CiOf(PduOf(sp)) eq CiOf(myCi)] -> ( [not(SrcOf(sp) IsUDPaddrIn CPs)] -> (let newCPs:CFPartnerSet = Insert(Pair(SrcOf(sp), UtOf(PduOf(sp))), CPs), newQyo:LOQ = add(Pair(Insert(SrcOf(sp), noUDPaddr), PDU_A(UtOf(myUt), CiOf(myCi))), Qyo) in ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](newQyo, Qxo, newCPs, myUt, myCi, myCFaddr, myUDPaddr) ) [] [SrcOf(sp) IsUDPaddrIn CPs] -> (let newQyo:LOQ = add(Pair(Insert(SrcOf(sp), noUDPaddr), PDU_A(UtOf(myUt), CiOf(myCi))), Qyo) in ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](newQyo, Qxo, CPs, myUt, myCi, myCFaddr, myUDPaddr) ) ) [] [not(CiOf(PduOf(sp)) eq CiOf(myCi))] -> ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](Qyo, Qxo, CPs, myUt, myCi, myCFaddr, myUDPaddr) ) [] [(TypeOf(PduOf(sp)) eq L) and (myCi ne noCi)] -> ( [CiOf(PduOf(sp)) eq CiOf(myCi)] -> (let newCPs:CFPartnerSet = RemovePartnerByUDPaddr(SrcOf(sp), CPs) in ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](Qyo, Qxo, newCPs, myUt, myCi, myCFaddr, myUDPaddr) ) [] [not(CiOf(PduOf(sp)) eq CiOf(myCi))] -> ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](Qyo, Qxo, CPs, myUt, myCi, myCFaddr, myUDPaddr) ) [] [(TypeOf(PduOf(sp)) eq A) and (myCi ne noCi)] -> ( [CiOf(PduOf(sp)) eq CiOf(myCi)] -> ( [not(SrcOf(sp) IsUDPaddrIn CPs)] -> (let newCPs:CFPartnerSet = Insert(Pair(SrcOf(sp), UtOf(PduOf(sp))), CPs) in ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](Qyo, Qxo, newCPs, myUt, myCi, myCFaddr, myUDPaddr) ) [] [SrcOf(sp) IsUDPaddrIn CPs] -> ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](Qyo, Qxo, CPs, myUt, myCi, myCFaddr, myUDPaddr) ) [] [not(CiOf(PduOf(sp)) eq CiOf(myCi))] -> ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](Qyo, Qxo, CPs, myUt, myCi, myCFaddr, myUDPaddr) ) [] [(TypeOf(PduOf(sp)) eq D) and (myCi ne noCi)] -> ( [SrcOf(sp) IsUDPaddrIn CPs] -> (* receive from a conference partner *) ( choice p:CFPartner [] [(p IsIn CPs) and (AddrOf(p) eq SrcOf(sp))] -> (let newQxo:UOQ = add(dataind(UtOf(p), DataFieldOf(PduOf(sp))), Qxo) in ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](Qyo, newQxo, CPs, myUt, myCi, myCFaddr, myUDPaddr) ) ) [] [not(SrcOf(sp) IsUDPaddrIn CPs)] -> (let newQyo:LOQ = add(Pair(Insert(SrcOf(sp), noUDPaddr), PDU_J(UtOf(myUt), CiOf(myCi))), Qyo) in ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](newQyo, Qxo, CPs, myUt, myCi, myCFaddr, myUDPaddr) ) ) ) [] [NotEmpty(Qxo)] -> (let sp:CFsp = last(Qxo), newQxo:UOQ = init(Qxo) in CFSAP_out !myCFaddr !sp; ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](Qyo, newQxo, CPs, myUt, myCi, myCFaddr, myUDPaddr) ) [] [NotEmpty(Qyo)] -> (let as:UDPaddrSet = AddrSetOf(last(Qyo)), p:PDU = PduOf(last(Qyo)) in (choice dest:UDPAddress [] [dest IsIn as] -> (let newas:UDPaddrSet = Remove(dest, as) in udp_out !myUDPaddr !udp_datareq(dest, p); ( [IsEmpty(newas)] -> ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](init(Qyo), Qxo, CPs, myUt, myCi, myCFaddr, myUDPaddr) [] [NotEmpty(newas)] -> (let newQyo:LOQ = dda(Pair(newas, p), init(Qyo)) in ProtocolFunctions[CFSAP_in, CFSAP_out, udp_in, udp_out](newQyo, Qxo, CPs, myUt, myCi, myCFaddr, myUDPaddr) ) ) ) ) ) endproc (* CFProtocolFunctions *) endproc (* ConferenceProtocolEntity *) endproc (* InstallProtocolEntity *) endspec (* ConferenceProtocolEntitySpecification *)