ГОСТ Р ИСО’МЭК ТО 10023— 93
h(TCONNECTindication) = Succ(h(TCONNECTrequest));
h(TCONNECTresponi.e) = Succ (h(TCONNECTindication));
h(TCONNECTconfirm) - Succ (h (TCONNECTresponse));
h(TDATArequest) =Succ(h (TCONNECTconfirm));
h(TDATAindication) = Succ (h (TDATArequest));
h (TEXDATArequest) = Succ (li (TDATAindication));
h(TEXDATAindication) = Succ (h (TEXDATArequest)):
Ji(TDISCONNrequest) = Succ(h (TEXDATAindication));
h (TDlSCONNindication) ^ Succ (h (TDISCONNrequest));
ofsort Boo!
Even (0) = true;
Even(Succ(.O)) «false.
Even(Succ(Succ(n))) «Even(n);
Odd(n) «not (F.ven(n));
IsRcquest (s) = Even (h ($));
Islndication(s) = Odd(h(st);
s eq sl = h(s) eq h(sl);
s ne sl = not(s eq si);
endtype (* TSPSubsort *)
type TSPBasicClassifiers
is BasicTSP, TSPSubsort
opns
Subsort: TSP— > TSPSubsort
IsTCON. IsTCONl, lsTCON2. IsTDT, IsTEX, IsTDIS,
IsTCONrcq. IsTCONind.fsTCONresp.IsTCONconf.
IsTDTreq, IsTDISind, IsTReq. IsTInd : TSP — > Bool
cqns
forall
a. a). a2 : TAddress. x : TEXOption. q : TQOS. d :
OctetString. r : TDISReason, t : TSP. clq : CLQOS
oisort TSPSubsort
Subsort(TCONreq(al, a2. x. q. d))-TCONNECTrcqucst;
Subsort (TCONind(al, a2. x. q. d)) «TCONNECT-
indicalion;
Subsorl(TCONresp(a, x. q. d)) =TCONNECTresponse;
Subsort(TCONconf(a, x, q. d) j =TCONNECTconfirm;
Subsort (TDTreq (d)) « TDATArequest;
Subsort (TDTind (d)) *■TDATAindication;
Subsort (TEXreq (d)) = TEXDATArequest;
Subsort (TEXind (d)) =
TEXDATAindication; Subsort (TD1 Srcq (d))
= TDISCONNrequest;
Subsort fiTDISind (r. d)) «TDlSCONNindication;
В