system ConferenceProtocol; signal Dataind(Charstring, Charstring), Leave, S_Join(Charstring, Charstring), Datareq(Charstring), Udp_dreq(Charstring, Charstring), Udp_dind(Charstring, Charstring), Udp_dreq2(Charstring, Charstring), Udp_dreq3(Charstring, Charstring); signallist Cout = Dataind; signallist Cin = S_Join, Datareq, Leave; /******************************************************************************* Copyright by Telesoft Europe AB 1990, 1991. Copyright by Telelogic Malmoe AB 1991, 1992, 1993, 1994. Copyright by Telelogic AB 1994 - 1998. This Program is owned by Telelogic and is protected by national copyright laws and international copyright treaties. Telelogic grants you the right to use this Program on one computer or in one local computer network at any one time. Under this License you may only modify the source code for the purpose of adapting it to your environment. You must reproduce and include any copyright and trademark notices on all copies of the source code. You may not use, copy, merge, modify or transfer the Program except as provided in this License. Telelogic does not warrant that the Program will meet your requirements or that the operation of the Program will be uninterrupted and error free. You are solely responsible that the selection of the Program and the modification of the source code will achieve your intended results and that the results are actually obtained. *******************************************************************************/ /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */ /* NOTE the following restictions for this data type when */ /* the SDT Validator is to be used. These restrictions do */ /* not apply to Simulations or Applications. */ /* */ /* 1. The PId_Lit operators may only be applied to process */ /* types with the number of instances (N, N), where N>0. */ /* 2. No process type with the number of instances equal to */ /* (N, N), where N>0, may contain any Stop symbol. */ /* */ /* If you violate any of these rules the behavior of the SDT */ /* Validator is undefined. */ /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */ synonym EnvPId PId = #CODE('xEnv'); newtype xPrsIdNode /*#NAME 'xPrsIdNode'*/ literals Dummy; /*#ADT(TA(S)E(S)R(S)W(S)D(H)) */ endnewtype; newtype PIdList ARRAY( Integer, PId) adding operators PId_Lit /*#NAME 'PId_Lit1'*/ : xPrsIdNode -> PId; PId_Lit /*#NAME 'PId_Lit2'*/ : xPrsIdNode, Integer -> PId; PId_Lit /*#NAME 'PId_Lit3'*/ : xPrsIdNode -> PIdList; /*#ADT(TA(S)E(S)D(H)R(S)W(S)K(H)X(H)M(H)HP) #TYPE typedef SDL_PId * #(PIdList); #HEADING extern SDL_PId PId_Lit1 XPP(( xPrsIdNode PNode )); extern SDL_PId PId_Lit2 XPP(( xPrsIdNode PNode, SDL_Integer InstNr )); extern #(PIdList) PId_Lit3 XPP(( xPrsIdNode PNode )); #define yExtr_#(PIdList)(v,i) v[i] #BODY #ifndef XVALIDATOR #ifdef xFirstActivePrs #undef xFirstActivePrs #endif #define xFirstActivePrs(PNode) (*PNode->ActivePrsList) #ifdef xNextActivePrs #undef xNextActivePrs #endif #define xNextActivePrs(P) P->NextPrs #endif #ifndef XNOPROTO extern SDL_PId PId_Lit1 ( xPrsIdNode PNode ) #else extern SDL_PId PId_Lit1 ( PNode ) xPrsIdNode PNode; #endif { #ifdef XOPERRORF if ( PNode == (xPrsIdNode)0 ) { xSDLOpError("PId_Lit (1) in sort PIdList", "IdNode parameter is 0"); return SDL_NULL; } if ( PNode->EC != xProcessEC ) { xSDLOpError("PId_Lit (1) in sort PIdList", "IdNode parameter does not represent process"); return SDL_NULL; } if ( xFirstActivePrs(PNode) == (xPrsNode)0 ) { xSDLOpError("PId_Lit (1) in sort PIdList", "No active instance of process"); return SDL_NULL; } if ( xNextActivePrs(xFirstActivePrs(PNode)) != (xPrsNode)0 ) { xSDLOpError("PId_Lit (1) in sort PIdList", "Several active instances of process"); } #endif return xFirstActivePrs(PNode)->Self; } #ifndef XNOPROTO extern SDL_PId PId_Lit2 ( xPrsIdNode PNode, SDL_Integer InstNr ) #else extern SDL_PId PId_Lit2 ( PNode, InstNr ) xPrsIdNode PNode; SDL_Integer InstNr; #endif { xPrsNode P; SDL_Integer I; #ifdef XOPERRORF if ( PNode == (xPrsIdNode)0 ) { xSDLOpError("PId_Lit (2) in sort PIdList", "IdNode parameter is 0"); return SDL_NULL; } if ( PNode->EC != xProcessEC ) { xSDLOpError("PId_Lit (2) in sort PIdList", "IdNode parameter does not represent process"); return SDL_NULL; } #endif I = 0; for ( P = xFirstActivePrs(PNode); P != (xPrsNode)0; P = xNextActivePrs(P) ) I++; #ifdef XOPERRORF if ( InstNr > I || InstNr < 1 ) { xSDLOpError("PId_Lit (2) in sort PIdList", "Illegal instance number"); return SDL_NULL; } #endif I = I-InstNr; P = xFirstActivePrs(PNode); while ( I-- > 0 ) P = xNextActivePrs(P); return P->Self; } #ifndef XNOPROTO extern #(PIdList) PId_Lit3 ( xPrsIdNode PNode ) #else extern #(PIdList) PId_Lit3 ( PNode ) xPrsIdNode PNode; #endif { xPrsNode P; SDL_Integer I; #(PIdList) Result; #ifdef XOPERRORF if ( PNode == (xPrsIdNode)0 ) { xSDLOpError("PId_Lit (3) in sort PIdList", "IdNode parameter is 0"); return (#(PIdList))0; } if ( PNode->EC != xProcessEC ) { xSDLOpError("PId_Lit (3) in sort PIdList", "IdNode parameter does not represent process"); return (#(PIdList))0; } if ( xFirstActivePrs(PNode) == (xPrsNode)0 ) { xSDLOpError("PId_Lit (3) in sort PIdList", "No active instance of process"); return (#(PIdList))0; } #endif I = 0; for ( P = xFirstActivePrs(PNode); P != (xPrsNode)0; P = xNextActivePrs(P) ) I++; #ifdef XPIDLIT_FROM_ZERO Result = (#(PIdList))xAlloc((xptrint)(I*sizeof(SDL_PId))); for ( P = xFirstActivePrs(PNode); P != (xPrsNode)0; P = xNextActivePrs(P)) Result[--I] = P->Self; #else Result = (#(PIdList))xAlloc((xptrint)((I+1)*sizeof(SDL_PId))); for ( P = xFirstActivePrs(PNode); P != (xPrsNode)0; P = xNextActivePrs(P) ) Result[I--] = P->Self; #endif return Result; } */ endnewtype PIdList; synonym Adr1 Charstring = '1'; synonym Adr2 Charstring = '2'; synonym Adr3 Charstring = '3'; synonym Join_Pdu Charstring = '1'; synonym Leave_Pdu Charstring = '2'; synonym Answer_Pdu Charstring = '3'; synonym Data_Pdu Charstring = '4'; newtype Element struct Address Charstring; Conf Charstring; Name Charstring; endnewtype Element; newtype ElemArray Array( Integer, Element); endnewtype ElemArray; newtype ConfSet struct pos Integer; Buffer ElemArray; endnewtype ConfSet; newtype AdBuf Array( Integer, Charstring); endnewtype AdBuf; block type CPEntities referenced; block type UDProtocol referenced; channel U_sap nodelay from udp via c to cpe via b with Udp_dind; from cpe via b to udp via c with Udp_dreq; endchannel U_sap; channel C_sap from cpe via a to env with (Cout); from env to cpe via a with (Cin); endchannel C_sap; channel U_sap2 nodelay from udp via d to env with Udp_dind; from env to udp via d with Udp_dreq2; endchannel U_sap2; channel U_sap3 nodelay from udp via e to env with Udp_dind; from env to udp via e with Udp_dreq3; endchannel U_sap3; block cpe : CPEntities; block udp : UDProtocol; /* Structure 'Element' is used for encapsulate the Address ,the Conference and the User for a CPE. Structure 'ElemArray' is used as an intermediary structure for building Conference Set. Structure 'ConfSet' is the Set of Conference Parteners. It contains an array of Elements( one Element contain the Adress,the Conference and the User for a CPE) and the number of all CPE in 'pos'.The default value for 'Conf' and 'Name' is ''. */ /* Structure AdBuf contains the addresses of all CPE. */ endsystem ConferenceProtocol; block type CPEntities; gate a out with (Cout); in with (Cin); gate b out with Udp_dreq; in with Udp_dind; signalroute C_sap from CPE_Process to env via a with (Cout); from env via a to CPE_Process with (Cin); signalroute U_sap from CPE_Process to env via b with Udp_dreq; from env via b to CPE_Process with Udp_dind; process CPE_Process referenced; endblock type CPEntities; process CPE_Process; dcl U, C, d, AO, a Charstring; dcl l Integer; dcl t, lc Charstring; dcl CSP ConfSet; procedure CInitialise referenced; procedure Append referenced; procedure PduCases referenced; procedure TransAll referenced; procedure ClearCSP referenced; procedure Int2CharS referenced; procedure TransMes referenced; start; call CInitialise; nextstate Idle; state Idle; input S_Join(U, C); task t := Join_Pdu; task d := t // U // C; call Append(AO, U, C); call TransAll(d); nextstate Engaged; endstate; state Engaged; input Datareq(d); task t := Data_Pdu; task l := Length(d); call Int2CharS; task d := t // LC // d; call TransMes(d); nextstate Engaged; input Leave; task t := Leave_Pdu; task d := t // U // C; call TransMes(d); call ClearCSP; nextstate Idle; input Udp_dind(a, d); task t := Substring(d, 1, 1); call PduCases; nextstate Engaged; endstate; /* U = User_Name C = Conf_Name CSP = Conference Set Parteners t = Type of Pdu d = Data for Udp_dind or Udp_dreq AO = CPE Own Adress l = Length of message reveived a = Address received lc = Length transforned in CharString */ endprocess CPE_Process; procedure CInitialise; start; task AO := Adr1; task CSP!pos := 3; task CSP!Buffer(0)!Address := Adr1; task CSP!Buffer(1)!Address := Adr2; task CSP!Buffer(2)!Address := Adr3; return; endprocedure CInitialise; procedure Append; fpar in Adr Charstring, in UName Charstring, in CName Charstring; dcl i integer; start; task i := 0; grst7 : decision CSP!buffer(i)!Address = Adr; (False) : task i := i + 1; (True) : task CSP!Buffer(i)!Name := UName; task CSP!Buffer(i)!Conf := CName; return; enddecision; join grst7; endprocedure Append; procedure PduCases; dcl up, cp Charstring; dcl du Charstring; dcl ud, cd, buf Charstring; procedure ClearU referenced; procedure SendDataind referenced; start; decision t = Join_Pdu; (True) : task up := SubString(d, 2, 10); task cp := SubString(d, 12, 10); decision cp = C; (True) : call Append(a, up, cp); task t := Answer_Pdu; task d := t // U // cp; output Udp_dreq(a, d); return; (False) : return; enddecision; (False) : decision t = Answer_Pdu; (True) : task up := SubString(d, 2, 10); task cp := SubString(d, 12, 10); call Append(a, up, cp); return; (False) : decision t = Data_Pdu; (True) : task buf := Substring(d, 2, 1); task l := Num(First(buf)) - 34; task du := SubString(d, 3, l); call SendDataind(a, du); return; (False) : decision t = Leave_Pdu; (True) : task ud := SubString(d, 2, 10); task cd := SubString(d, 12, 10); call ClearU(ud, cd); return; (False) : return; enddecision; enddecision; enddecision; enddecision; /* up = User name of my conference Partener cp = Conference name du = Data which will be sent to User (Dataind) ud = User name which must be Deleted cd = Conference name which must be Deleted buf = is used for decompose the data received */ endprocedure PduCases; procedure ClearU; fpar in U Charstring, C charstring; dcl i integer; start; task i := 0; grst8 : decision i < CSP!pos; (True) : decision (CSP!Buffer(i)!Conf = C) and (CSP!Buffer(i)!Name = U); (True) : task CSP!Buffer(i)!Conf := ''; task CSP!Buffer(i)!Name := ''; (False) : enddecision; task i := i + 1; (False) : return; enddecision; join grst8; /* C = Conference name which must be deteted U = User name which must be deleted */ endprocedure ClearU; procedure SendDataind; fpar in Adr Charstring, in Data Charstring; dcl i integer; dcl name Charstring; start; task i := 0; grst9 : decision CSP!buffer(i)!Address = Adr; (False) : task i := i + 1; (True) : task name := CSP!Buffer(i)!Name; output Dataind(name, data); return; enddecision; join grst9; endprocedure SendDataind; procedure TransAll; fpar in Mes Charstring; dcl i integer; start; decision C = ''; (True) : return; (False) : task i := 0; enddecision; grst10 : decision i >= CSP!pos; (True) : return; (False) : decision CSP!Buffer(i)!Address = Ao; (False) : output Udp_dreq(CSP!Buffer(i)!Address, Mes); (True) : enddecision; task i := i + 1; enddecision; join grst10; endprocedure TransAll; procedure ClearCSP; dcl i integer; start; task C := ''; task U := ''; task i := 0; grst11 : decision i < CSP!pos; (True) : task CSP!Buffer(i)!Conf := ''; task CSP!Buffer(i)!Name := ''; task i := i + 1; (False) : return; enddecision; join grst11; endprocedure ClearCSP; procedure Int2CharS; start; task lc := MkString(Chr(l + 34)); return; endprocedure Int2CharS; procedure TransMes; fpar in Data Charstring; dcl i integer; start; decision C = ''; (False) : task i := 0; (True) : return; enddecision; grst12 : decision i >= CSP!pos; (False) : decision (CSP!Buffer(i)!Conf = C) and (not (CSP!Buffer(i)!Address = Ao)); (True) : output Udp_dreq(CSP!Buffer(i)!Address, Data); (False) : enddecision; task i := i + 1; (True) : return; enddecision; join grst12; endprocedure TransMes; block type UDProtocol; gate c out with Udp_dind; in with Udp_dreq; gate d out with Udp_dind; in with Udp_dreq2; gate e out with Udp_dind; in with Udp_dreq3; signalroute U_sap from Udp_Process to env via c with Udp_dind; from env via c to Udp_Process with Udp_dreq; signalroute U_sap2 from Udp_Process to env via d with Udp_dind; from env via d to Udp_Process with Udp_dreq2; signalroute U_sap3 from Udp_Process to env via e with Udp_dind; from env via e to Udp_Process with Udp_dreq3; process Udp_Process referenced; endblock type UDProtocol; process Udp_Process; dcl adrs, adrd, d Charstring; dcl ba AdBuf; procedure UInitialise referenced; procedure SendMes referenced; start; call UInitialise; nextstate Ready; state Ready; input Udp_dreq(adrd, d); task adrs := ba(0); call SendMes(adrs, adrd, d); nextstate Ready; input Udp_dreq2(adrd, d); task adrs := ba(1); call SendMes(adrs, adrd, d); nextstate Ready; input Udp_dreq3(adrd, d); task adrs := ba(2); call SendMes(adrs, adrd, d); nextstate Ready; endstate; endprocess Udp_Process; procedure UInitialise; start; task ba(0) := Adr1; task ba(1) := Adr2; task ba(2) := Adr3; return; endprocedure UInitialise; procedure SendMes; fpar in SourceAdr Charstring, in DestAdr Charstring, in Data Charstring; dcl i Integer; dcl dest Integer; start; task i := 0; grst13 : decision ba(i) = DestAdr; (False) : task i := i + 1; (True) : task dest := i + 1; decision dest = 1; (True) : output Udp_dind(SourceAdr, Data) via U_sap; return; (False) : decision dest = 2; (False) : decision dest = 3; (True) : output Udp_dind(SourceAdr, Data) via U_sap3; (False) : enddecision; return; (True) : output Udp_dind(SourceAdr, Data) via U_sap2; return; enddecision; enddecision; enddecision; join grst13; endprocedure SendMes;