ISO/IEC TR 9572:1989
(Main)Information technology — Open Systems Interconnection — LOTOS description of the session protocol
Information technology — Open Systems Interconnection — LOTOS description of the session protocol
Traitement de l'information — Interconnexion de systèmes ouverts — Description en LOTOS du protocole de session
General Information
Standards Content (Sample)
TECHNICAL ISO/IEC
REPORT TR 9572
First edition
1989-09-1 5
Information technology - Open Systems
Interconnection - LOTOS description of the
session pro tocol
Traitement de l'information - Interconnexion de systèmes ouverts - Description
en LOTOS du protocole de session
Reference number
ISO/IEC/TR 9572 : 1989 (E)
---------------------- Page: 1 ----------------------
ISO/IECTTR 9572: 1989 (E)
Contents
Foreword iii
Introduction iv
1 Scope 1
2 Normative references 1
3 Definitions 2
4 Symbols and abbreviations 2
5 Conventions 2
6 Introduction to the formal description 3
7 Overall constraints of the session protocol 6
8 Constraints for a single session protocol machine 7
9 Session protocol data types 8
8
9.1 Session protocol data unit
9.2 Session variables 35
9.3 Additional functions on session and transport service primitives 36
9.4 Auxiliary data types 36
39
9.5 Types for components of the internal event structure
Processes for the SPM session to transport service boundary relation 41
10
10.1 First decomposition of the session to transport boundary relation 42
44
10.2 Direct mapping between SSPs and TSPs
45
10.3 Relation between SSPs and SPDUs
50
10.4 Relation between SPDUs and TSPs
10.5 SPDU constraints 63
O ISO/IEC 1989
All rights reserved. No part of this publication may be reproduced or utilized in any form or by any
means, electronic or mechanical, including photocopying and microfilm, without permission in
writing from the publisher.
ISO/IEC Copyright Office Case postale 56 CH-1211 Genève 20 Switzerland
Printed in Switzerland
ii
---------------------- Page: 2 ----------------------
ISOiIECRR 9572: 1989 (E)
\
I Foreword
IS0 (the International Organization for Standardization) and IEC (the
International Electrotechnical Commission) together form a system for worldwide
standardization as a whole. National bodies that are members of IS0 or IEC
participate in the development of International Standards through technical
committees established by the respective organization to deal with particular
fields of technical activity. IS0 and IEC technical committees collaborate in
fields of mutual interest. Other international organizations, governmental and
non-governmental, in liaison with IS0 and IEC, also take part in the work.
In the field of information technology, IS0 and IEC have established a joint
technical committee, ISO/IEC JTC 1.
The main task of a technical committee is to prepare International Standards but
in exceptional circumstances, the publication of a technical report of one of the
following types may be proposed:
- type 1, when the necessary support within the technical committee cannot
be obtained for the publication of an International Standard, despite
repeated efforts;
- type 2, when the subject is still under technical development requiring
wider exposure;
- type 3, when a technical committee has collectcd data of a different kind
from that which is normally published as an International Standard ("state
of the art", for example).
Technical reports of types 1 and 2 are subject to review within three years of
publication, to decide whether they can be transformed into International
Standards. Technical reports of type 3 do not necessarily have to be reviewed
until the data they provide are considered to be no longer valid or useful.
ISO/iEC/TR 9572, which is a technical report of type 2, was prepared by ISO/iEC
JTC 1, Information technology.
iii
---------------------- Page: 3 ----------------------
ISO/IECflR 9572: 1989 (E)
Introduction
In view of the complexity and widespread use of Open Systems Interconnection
standards it is imperative to have precise and unambiguous definitions of these
standards. Formal Description Techniques form an important approach for
providing such definitions. The use of Formai Description Techniques in this area
is however relatively new and their application on a wide scale cannot be
expected overnight. Formal descriptions should be introduced gradually in
standards if initially the number of Member Bodies that are able to contribute to
their development is too small, thus allowing time to gain experience and to
develop educational material.
An ad-hoc group for the formai description of the Session Layer, i.e. of the
Session Service IS0 8326 and the Session Protocol IS0 8327, was established in
November 1985. This group applied the Formal Description Technique LOTOS,
defined in IS0 8807, which at that time was still under development. In
September 1986 two Working Documents were produced which contained the
LOTOS draft specifications of IS0 8326 and IS0 8327 respectively. As a
byproduct, the group also produced a number of Defect Reports on the standards,
most of which have been accepted and incorporated in the standards.
A Ballot was then issued requesting Member Bodies to state their position
concerning the progression of the formal descriptions, Based on this Ballot, SC21
decided in June 1987 to progress both formal descriptions as Type 2 Technical
Reports. The main reason for not incorporating them into the standards was that
Member Bodies expressed their current lack of expertise on the subject. It seemed
therefore appropriate that a period of time passed, during which the formal
decriptions can be read and compared with the standards, and after which the
status and progression of the formal descriptions can be re-evaluated.
The purpose of this Technical Report is to provide a complete, consistent and
unambiguous description of IS0 8327. It forms therefore a companion document
to IS0 8327. It takes account of the Defect Reports incorporated in the standard
(annex D of IS0 8327), however, it does not necessarily take account of
subsequent amendments or addenda to the standard.
iv
---------------------- Page: 4 ----------------------
TECHNICAL REPORT ISO/IEC/TR 9572: 1989 (E)
Information technology - Open Systems Interconnection -
LOTOS description of the session protocol
1 Scope
This Technical Report contains a formal description of the OS1 Basic Connection Oriented Session Protocol
0
defined in IS0 8327. The formal definitions presented in this Technical Report are expressed in the formal
description technique LOTOS, which is defined in IS0 8807.
These foimal definitions are related to the formal descriptions in LOTOS of the OS1 Connection Oriented
Session Service, IS0 8326, and of the OS1 Transport Service, IS0 8072. Moreover, formal definitions of
these services, contained in ISOIIECJTR 9571 and ISO/IEC/TR 10023, respectively, are used and
rcferenced in this Technical Report.
The formal description is not limited to a single session protocol machine, but also describes multiple
session protocol machines that result from support of multiple session connections either in parallel or in
sequence. Therefore, it also formalizes aspccts of multiplicity which are not presented in IS0 8327 directly,
but by way of reference to the OS1 Basic Reference Model, IS0 7498.
2 Normative references
0
The following standards contain provisions which, through reference in this text, constitute provisions of
this Technical Report. At the time of publication, the editions indicated were valid. All standards are
subject to revision, and parties to agreement based on this Technical Report are encouraged to investigate
the possibility of applying the most recent editions of the standards listed below. Members of IS0 and IEC
maintain registers of currently valid International Standards.
IS0 7498: 1984, Information processing systems - Open Systems Interconnection - Basic Reference Model.
IS0 8072: 1986, Information processing systems - Open Systems Interconnection - Transport service
I definition.
IS0 8326: 1987, Information processing systems - Open Systems Interconnection - Basic connection
oriented session service definition.
IS0 8327: 1987, Information processing systems - Open Systems Interconnection - Basic connection
oriented session protocol specification.
---------------------- Page: 5 ----------------------
ISO/IECflR 9572: 1989 (E)
IS0 8807: 1988, Information processing systems - Open Systems Interconnection - LOTOS - A formal
of observational behaviour.
description technique based on the temporal ordering
ISO/IEC/lX 9571: 1989, Information processing systems - Open Systems Interconnection - LOTOS
description of the session service.
ISO/IECPX 10023: - 11, Information processing systems - Open Systems Interconnection - LOTOS
description of the transport service.
3 Definitions
For the purpose of this Technical Report the definitions given in IS0 8327 apply.
4 Symbols and abbreviations
This Technical Report uses the symbols defined in clause 6 (formal syntax) and annex A (data type library)
of IS0 8807, and uses the abbreviations contained in clause 4 of IS0 8327.
The following additional abbreviations are employed in this Techical Report:
sc session connection
SCEP session connection endpoint
SCE1 session connection endpoint identifier
SSP session service primitive
TC transport connection
TS Transport Service
TSDU transport service data unit
5 Conventions
Clauses 6 through 10 of this Technical Report constitute LOTOS text. Ali informal explanations in these
and
clauses form LOTOS comments. They are thus separated from the LOTOS specifications (of data types
dynamic behaviour) according to the rules for comment delimitation. Moreovcr, informal explanations
precede the formal definitions to which they refer and contain a final line of only "-" characters. Informal
explanations following formal definitions contain a first line of only "-" characters.
Formal definitions, as well as formal symbols and identifiers reîerenced in informal explanations, are
printed in italics.
1 ) To be published.
2
---------------------- Page: 6 ----------------------
ISO/IEC/TR 9572: 1989 (E)
(* start of
6 Introduction to the formal description
The formal description relates to the dynamic behaviour of an unbounded number of SPMs, each of which
supports the provision of a single SC or, in case of re-use of the underlying TC, a sequence of SCs. The SS
boundary is formally represented by a single gate s and the TS boundary by a single gate t. Events at these
in the service formal descriptions, ISOIIECJTR 9571 and ISO/IECm
gates are structured as defined
10023. Constraints on connection identification, acceptance of connections and backpressure flowcontrol
(from the TS-provider) apply to the Session Protocol, as well as to the related services, and the processes
representing these constraints are in fact imported from the service formal descriptions. Figure 1 shows the
conjunction of processes resulting from this top level decomposition.
S
9
SCAcceptance
+L
SetOfSPM I
TCElden fification TCAccepfance TBackpressu re
II--
O
t
Figure 1 - (Top level) processes representing separate constraints for a Session Protocol entity
outgoing SSPs incoming SSPs
Session Service
observe gate s
decisions on validity state and decisions on
local
protocol actions variables
I I
observe gate p
build SPDUs
I
receive TSDUs build TSDUs
observe gate t
Transport Service v
Figure 2 - Actions within a SPM
3
---------------------- Page: 7 ----------------------
ISO/IECTTR 9572: 1989 (E)
An internal gate p is introduced to favour separation of concerns based on the concept of SPDU. SPDUs are
transferred via the TS by encoding, and possibly concatenating, them into TS data units. The interactions at
gate p are independent of encoding and concatenation, however, thus only abstract SPDUs are to be
considered at p. The actions of a single SPM are summarized in figure 2.
The behaviour of the SPM is described by specifying the constraints on the behaviour observed at the three
gates s, p and f. This is obtained by a parallel composition of a process, termed STPM, that roughly
corresponds to the state tables protocol machine, together with processes that enforce the local constraints
on service primitives at connection endpoints. Again, the latter constraints can be specified with instances
of processes imported from the SS and TS €ormal descriptions (namely SCEP and TCEP).
The next level of substructuring is found in the decomposition of STPM into processes representing the
following separate constraints:
The relationship between SSPs and TSPs that docs not involve abstract SPDUs (described by
a)
process SSPTSP). This constraint is concerned with "direct mappings" between service
primitives, where no SPM generated information is needed to coordinate the interworking with
the remote SPM. Also the establishment of a TC is attributed to this constraint.
The relationship between SSPs and abstract SPDUs, including segmentation of SSDUs (described
b)
by process SSPSPDU).
The transformation of abstract SPDUs to TSPs, and vice versa, including encoding and
c)
concatenation of SPDUs (describcd by process SPDUTSP).
The constraints on the ordering and contents of abstract SPDUs, corresponding to the state tables
d)
description in annex A of IS0 8327 (described by process SPDüConsfrainfs).
SSPTSP and SSPSPDU synchronize at gate s, SSPTSP and SPDUTSP synchronize at gate f, and, finally,
SSPSPDU, SPDUTSP and SPDUConsfraints synchronize at gate p. This is shown in figure 3. The style of
the formal description, which now also shows a limited internal structure, can be characterized as a mixture
of constraint- and resource-oriented styles.
S
I I SSPSPDU I
'I SPDUConstraints
SSPTSP
SPDUTSP 1
Figure 3 - Conjunction of processes representing the behaviour of a single SPM
Each of the processes that must synchronize at p imposes its own constraints on the exchange of abstract
SPDUs. Because of this, an abstract SPDU exchange only occurs if all processes agree on that particular
4
---------------------- Page: 8 ----------------------
ISO/IECTTR 9572: 1989 (E)
exchange. The event structure of the abstract SPDU exchange is as follows:
p ?pd:ASPDU ?fl:TFlow ?d:Dir ?v:Validiiy ?st:TrState
with components
- pdof sort ASPDU: the abstract SPDU being exchanged;
- fl of sort TFlow: the transport flow, which is either normal or expedited;
- d of sort Dir: the direction of transfer, which is either sending or receiving;
- w of sort Validity: the "status" of the abstract SPDU (only applicable for received SPDUs).
According to the state tables of IS0 8327, processing of a received SPDU, and in particular
determining its validity, depends upon the result of several actions (see figure 2) and/or the values of
certain session variables. Relevant states that involve more than one process can be established
through this component when synchronizing at p; and
- st of sort TrState: the "coarse-grained" state of the SPM (only applicable for received SPDUs and
for sending the DN SPDU). The SPM state, known to process SPDUConstrainfs, is often also
required by other processes upon exchange of a SPDU. However, rather than the fine-grained
division of the data transfer phase into SPM states, certain collections of SPM states are relevant for
the latter processes. Values of this component are used to represent such collections and can be
communicated when synchronizing at p.
NOTES
1 - In order to represent flow control and segmenting, events at gates s and t may represent the exchange of
single data octets instead of just executions of "complete" service primitives. Octet-wise exchange of data is
only modelled for those service primitives whose user data parameter has no length restrictions (i.e., S-DATA,
S-TYPED-DATA and T-DATA). Except for the need of "data octet" events, the characteristics of octet-wise
exchange of data are
- two events, a start and an end event, are significant to delimitate an exchange of data;
- the state transition and predicates that are associated with a SSP request are now associated with the
corresponding start event. If a colliding or overtaking, that is, "intervenient", event occurs before the end
event, then either
a) the (unfinished) request is not disrupted (provided the intervenient event is not destructive),
but will be resumed after the intervenient event, or
b) the (unfinished) request is disrupted, and the corresponding TSP request is cancelled or
terminated;
- the state transition and predicates that are associated with a TSP indication are now associated with the
corresponding end event. If a destructive or overtaking event occurs before the end event, then the
(unfinished) indication is disrupted, and all previous events of the indication are discarded.
2 - The formal description extends beyond the state tables description of IS0 8327 by way of explicitly
describing
- the constraints related to the multiplicity of SPMs;
- concatenation, extended concatenation and segmentation;
- the transfer of expedited data;
- the handling of invalid and unrecognizable events.
Figure 4 gives an overview of the processes used for the formal definition of the Session Protocol and their
relations (a number of the lowest level processes are omitted). It also indicates the clauses where the
definition of these processes can be found ("SS" means: defined in ISOIIECJTR 9571; "TS" means: defined
in ISO/IECKR 10023).
The definition of data types precedes the deîinition of the dynamic behaviour in which these types are used.
A number of standard data types are imported from the LOTOS library of data typcs. Apart from these, and
some "ad-hoc" data types, the types can roughly be divided in types for the representation of abstract
SPDUs, of encoded SPDUs, and of session variables. Additionally, a number of types are related to the
components of an internal event at gate p (besides the abstract SPDU).
---------------------- Page: 9 ----------------------
ISO/IEC/TR 9572: 1989 (E)
tance TBackpressure
SdEP STPM (10.1.1) TCEP
SSPTSP SSPSPDU SPDUConstraints
(10.2) (1 0.3) (1 0.5) (1 0.4)
SSPSP&ûUTran
(10.3.1) (10.3.2) (1 0.4.4) (10.4) (10.4.5)
SendAB d0.5.1) SPDUConstraints 1 RecABnr
ImplCon TwoSPDUs SPDUOrd VarCon
(1 0.5.3) (1 0.5.4) (10.5.5) (10.5.6)
Figure 4 - Processes related by a tree structure: each "father" process contains (or is constructed
0
from) one or more instances of its immediate "descendant" process(es)
7 Overall constraints of the session protocol
A number of standard types are imported from the LOTOS library of data types by means of the library
construct. The specification is parameterized with a protocol implementation parameter, defined in type
SProtocoilmplementationPar. Its value indicates: 1) whether or not use of the transport expedited service is
implemented, 2) what is the maximum TSDU size for both directions of data flow, 3) which functional
units have been implemented and 4) whether or not extended concatenation is implemented.
The top level structure shows a full synchronization of process SetOfSPM with two behaviour expressions
which mutually interleave, viz. SCEldentification synchronized with SCAcceptancs on the one hand, and
TCEldentification synchronized with TCAcceptance and TBackpressure on the other. SetOfSPM defines
the dynamic behaviour of a potentially infinite number of independent SPMs, however
disregarding any concerns related to the limited capacity of the local system and the TS-provider
and the need for unique connection identification, The latter concerns are addressed by the two
behaviour expressions mentioned. They formulate the overall constraints that relate to a single service
---------------------- Page: 10 ----------------------
ISO/IEC/TR 9572: 1989 (E)
boundary; the processes representing these constraints are defined in the Session Service formal
description, IS/IEC/TR 9571, and the Transport Service formal description, ISO/IEC/TR 10023,
respectively.
SetOfSPM represents concurrency by multiple instances of SuccSPMs, where each instance describes a
succession of SPM behaviours. A SPM is represented by a distinct instance of SPM. The behaviour
described by SPM is that of using at most one TC for support of a single SC or multiple successive SCs
(based on the same TC). Termination of a TC enforces successful termination of the associated instance of
SPM.
library Boolean, Element, Set, String, NatRepresentations, Octetstring, NaturalNumber, Bit, FBoolean,
Octet, DecNatRepr, Bitstring, BitNatRePr, DecString , DecDigit
endlib
type SProtocollmplementation Par is SRequirements, TSDUSize
sorts SPElmplementation
@ opns
SPElmpl: Bool, SRqms, TSDUSize, Bool -> SPElmplementation
Max TSize: SPElmplementa tion -> TSDUSize ExtConc: SPElmplementa tion -> Bool
eqns forall tex, ExtConc:Bool, s fus:SRqms, tsduSize:TSDUSize
ofsort TSDUSize Max TSize(SPElmpl(tex, s fus, tsduSize, ExtConc)) = tsduSize;
ofsort Boo1 ExtConc(SPElmpl(tex, sfus, tsduSize, ExtConc)) = ExtConc;
endtype
behaviour
( SCEldentification[s] II SCAcceptance[s] ) 111
(
( TCEldentification[t] /I TCAcceptance[t] /I TBackpressure[t] )
) II SetOfSPM[s,t](.spei)
where
8 Constraints for a single session protocol machine
Three separate constraints are distinguished with respect to the behaviour of a single SPM, namely
constraints that are local to the SS boundary, constraints that are local to the TS boundary, and constraints
that relate the behaviour at one boundary to that at the other. These constraints are represented by SCEPs,
TEPS and STPM, respectively.
SEPS is described as the choice of two instances of SCEP that apply to the interaction with the Calling
SS-user and with the Called SS-user, respectively, followed by either successful termination or another
instance of SCEPs. The recursion applies only when the SPM re-uses the TC. Similarly, TCEPs is
described as the choice of two instances of TCEP that apply to the interaction with the Calling TS-user and
with the Called TS-user, respectively. The definitions of SCEP and TCEP are imported from ISO/IEC/TR
9571 and ISO/IEC/TR 10023 respectively.
STPM defines the mapping of SSPs to TSPs during the provision of one SC, or multiple successive SCs,
supported by a single TC.
7
---------------------- Page: 11 ----------------------
ISO/IEC/TR 9572: 1989 (E)
....................................................................................................................
*>
process SPM[s, fl(spei:SPElmplementation): noexit :=
SCEPs[s]][s]/ STPM[s,t](spei) /[tJ TCEPs[fl
where
process SCEPs[s]: exit := ( SCEP[s](calling) [] SCEP[s](called) ) >> ( exit [] SCEPs[s]) endproc
process TCEPs[t]: exit := TCEP[t](CallingRole) [] TCEP[t](CalledRole) endproc
endproc (* SPM *)
9 Session protocol data types
The Session Protocol data types consist of definitions for the construction of a SPDU (see 9.1), some
session variables (see 9.2) for the introduction of some additional functions related to SSPs and TSPs (see
9.3), and for the construction of components of the internal event structure (see 9.5). A number of auxiliary
definitions of general use are presented in 9.4.
9.1 Session protocol data unit
0
Two sets of definitions are distinguished for the construction of a SPDU: one for an "abstract" SPDU and
the other for an encoded SPDU. This division is consistent with the observation that the elements of
procedure related to SPDUs can be described independently of the encoding of SPDUs (i.e,, the mapping
into TS data units).
9.1.1 Abstract SPDU
The specification of the abstract SPDU type is accomplished by way of a number hierarchical type
definitions. First the basic construction of SPDUs is presented (see 9.1.1. l), then a classification of SPDUs
(see 9.1.1.2), and subsequently a number of additional functions on SPDUs (see 9.1.1.3 through 9.1.1.5)
Concatenation of SPDUs is defined in 9.1.2; (groups of) SPDU parameters are defined in 9.1.3 (in as far as
not defined in ISOflECRR 9571).
9.1.1.1 SPDU basic construction
Type BasicASPDU defines functions, referred to as "constructor" functions, that yield (abstract) SPDU
e
values. For each class, or "type", of SPDU a corresponding constructor function is defined with values of
the parameters of that SPDU as arguments. Additionally, a function DUM is introduced for conveniently
specifying error reporting. Definitions that relate to SPDU parameters are imported by BasicASPDU (most
SessionService Primitive).
of them indirectly, by importing type
...............................................................................................................................
*>
type BasicASPDU is SessionServicePrimitive, SPReference, CAltem, TDISPar, Prepare, Encltem
sorts ASPDU
opns
CN: SPReference, CAItem,SFUs,SAddress,SAddress, SData -> ASPDU
AC: SPRe ference, CAltem, S Tokens,SFUs, SAddress, SAddress,SData -> ASPDU
RF: SPReference,TDISPar,SFUs,Nat (*Version*) , DatOctStr (*Reason Code*) -> ASPDU
FN: TDISPar,SData -> ASPDU DN,NF: SData -> ASPDU
AB: TDISPar,Nat (*Reason Code*),DatOctStr (*Reflect Parameter Values*), SData -> ASPDU
GTC, GTA, AA, AIA, ADA: -> ASPDU DT,TD: Enclt,SData -> ASPDU
CO, EX, CDA: SData -> ASPDU GT: STokens (*Token Item parameter*) -> ASPDU
PT: STokens,SData -> ASPDU MIP: SSyncType,SSPSN,SData -> ASPDU
MIA: SSPSN,SData -> ASPDU MAP,AE, MAA,AEA: SSPSN,SData -> ASPDU
RA: STsAss, SSPSN, S Data -> AS PDU RS : STsAss,SResynType,SSPSN,SData -> ASPDU
AS: SActld,SData -> ASPDU
PR: PrepType -> ASPDU
8
---------------------- Page: 12 ----------------------
ISO/IEC/TR 9572: 1989 (E)
AR: SCRe f, SActld, SSPSN, SActld, SData -> ASPDU
AI,AD: Nat (*Reason Code*) -> ASPDU DUM: DatOctStr -> ASPDU
ER : DatOctStr -> ASPDU ED :Nat (* Reason Code *), SData -> ASPDU
endtype
9.1.1.2 SPDU classification
Type ASPDUConstant defines a classification of SPDUs. Each class of SPDU is represented by a constant
with a name similar to the abbreviated name to denote the SPDU in table 39 of IS0 8327. The auxiliary
function h that maps these constants to natural numbers is defined in order to simplify the definition of
equality on SPDU classes.
Type ASPDUClassifiers is a functional enrichment of BasicASPDU. It defines functions, referred to a
"recognizer" functions, that determine whether a given SPDU is of a certain class.
...............................................................................................................................
*>
type ASPDUConstant is NaturalNumber
sorts ASPDUConstant
opns
cn,ac,rf,fn,dn,nf,ab,aa,dt,ex,td,cd,gt,pt,gtc,gta,n~~,mia,map,maa,rs,pr,ra,er,ed,as,ar,ad,ai,ada,aia,ae,aea,
dum: -> ASPDUConstant
h: ASPDUConstant -> Nat
-eq- , -ne-: ASPDUConstant,ASPDUConstant -> Bool
eqns forall x, y:ASPDUConstant
ofsort Nat
h(cn) = O; h(ac) = Succ(0); h(rf) = Succ(h(ac));
h(fn) = Succ(h(rf)); h(dn) = Succ(h(fn)); h(nf) = Succ(h(dn));
h(ab) = Succ(h(nf)); h(aa) = Succ(h(ab)); h(dt) = Succ(h(aa));
h(ex) = Succ(h(dt)); h(td) = Succ(h(ex)); h(Cd) = SüCC(h(td));
h(cda) = Succ(h(cd)); h(gt) = Succ(h(cda)); h(pt) = SüCC(h(gt));
h(gtC) = SüCC(h(pt)); h(gta) = Succ(h(gtc)); h(mip) = Succ(h(gta));
h(mia) = Succ(h(mip)); h(map) = Succ(h(mia)); h(maa) = Succ(h(map));
h(rs) = Succ(h(maa)); h(pr) = Succ(h(rs)); h(ra) = Succ(h(pr));
h(er) = Succ(h(ra)); h(ed) = Succ(h(er)); h(as) = Succ(h(ed));
h(ar) = Succ(h(as)); h(ad) = Succ(h(ar)); h(a0 = Succ(h(ad));
h(ada) = Succ(h(ai)); h(aia) = Succ(h(ada)); h(ae) = Succ(h(aia));
h(aea) = Succ(h(ae)); h(dum) = Succ(h(aea));
ofsort Bool
x eq Y = h(x) eq h(y); x ne y = h(x) ne h(y);
endtype
type ASPDUClassifiers is BasicASPDU, ASPDUConstant
opns
Is CN, IsAC, Is RF, Is FN, Is DN, IsNF, IsAB, IsG TC, IsG TA, IsAA, Is DT, Is TO, IsCD, Is EX, Is CDA, Is GT, Is PT, IsMlP,
IsMIA,lsMAP, IsMAA, IsA EA, Is RS, Is RA, Is PR, IsAS, IsA R,lsAl, IsAD,lsAIA, IsA DA, IsA E, IsCAT2 7, IsACK, IsPAB,
IS ER,IsED, IS DUM,ls PR- RS,k PR-RA, IsPR-MAA, ISACT: ASPDU -> 6001
k: ASPDU -> ASPDUConstant
eqns forall spr:SPRe ference, sreq:SFUs, cait:CAltem, cg,cd:SAddress, d:SData, tk:STokens,
tdpar:TDISPar, vs,reas:Nat, rcode,rpv,err:DatOctStr, sn:SSPSN, a:STsAss, et:Enclt, sntp:SSyncType,
tt:SResyn Type, pt:Prep Type, aid? ,aid2:SActld, scr:SCRe f, pd:ASPDU
ofsort ASPDUConstant
k(CN(spr,cait,sreq,cg,cd,d)) = cn;
k(AC(spr,cait,tk,sreq,cg,cd,d)) = ac;
k(RF(spr, tdpar,sreq, vs,rcode)) = rf;
k(FN(tdpar,d)) = fn; k(DN(d)) = dn; k(NF(d)) = nf;
= ab; k(GTC) = gtc; k(GTA) = gta;
k(AB(tdpar,reas,rpv,d))
= aa; k(A1A) = aia; k(ADA) = ada;
k(AA)
k(DT(et,d)) = dt; k(TD(et,d)) = td; k(CD(d)) = Cd;
k(EX(d)) = ex; k(CDA(d)) = cda;
k(GT(fk)) = gf;
9
---------------------- Page: 13 ----------------------
ISO/IEC/TR 9572: 1989 (E)
k(PT(tk,d)) = pt; k(MIP(sntp,sn,d)) = mip; k(MIA(sn,d)) = rnia;
k(MAP(sn,d)) = map; k(AE(sn,d)) = ae; k(MAA(sn,d)) = maa;
k(RA(a,sn,d)) = ra; k(RS(a, rt, sn,d)) = rs;
k(AEA(sn,d)) = aea;
= ar;
k(AS(aid1,d)) = as; k(A R(scr, aid I, sn, aid2,d))
k(PR(pt)) = Pr;
= ai; k(AD(reas)) = ad; k(ER(err)) = er;
k(Al(reas))
k(ED(reas,d)) = ed; k(DUM(err)) = dum
ofsotf Boo1
IsRF(pd) = k(pd) eq rf;
IsCN(pd) = k(pd) eq cn; IsAC(pd) = k(pd) eq ac;
IsDN(pd) = k(pd) eq dn;
lsFN(pd) = k(pd) eq fn; IsNF(pd) = k(pd) eq nf;
IsAB(pd) = k(pd) eq ab; IsGTC(pd) = k(pd) eq gtc; IsGTA(pd) = k(pd) eq gta;
IsCDA(pd) = k(pd) eq cda;
IsAA(pd) = k(pd) eq aa; IsDT(pd) = k(pd) eq dt;
IsEX(pd) = k(pd) eq ex;
IsTD(pd) = k(pd) eq td; IsCD(pd) = k(pd) eq cd;
IsMIP(pd) = k(pd) eq me; IsGT(pd) = k(pd) eq gt; IsPT(@) = k(pd) eq pt;
IsMAA(pd) = k(pd) eq maa;
IsMIA(pd) = k(pd) eq rnia; IsMAP(pd) = k(pd) eq map;
IsRA(pd) = k(pd) eq ra;
IsAEA(pd) = k(pd) eq aea; Is RS(pd) = k(pd) eq rs;
IsED(pd) = k(pd) eq ed;
IsPR(pd) = k(pd) eq pr; IsER(pd) = k(pd) eq er;
IsAl(pd) = k(@) eq ai;
IsAS(pd) = k(pd) eq as; IsAR(pd) = k(pd) eq ar;
IsADA(pd) = k(pd) eq ada;
IsAD(pd) = k(pd) eq ad; IsAIA(pd) = k(
...
Questions, Comments and Discussion
Ask us and Technical Secretary will try to provide an answer. You can facilitate discussion about the standard in here.