| The IOA language provides notations for defining both primitive and composite I/O automata.
This note describes, both formally and with examples, the constraints on these definitions, the
composability requirements for the components of a composite automaton, and the transformation
of a composite automaton into an equivalent primitive automaton.
Section 2 introduces four examples used throughout this note to illustrate new definitions and
operations. Section 3 treats IOA programs for primitive I/O automata: it introduces notations
for describing the syntactic structures that appear in these programs, and it lists syntactic and
semantic conditions that these programs must satisfy to represent valid primitive I/O automata.
Section 4 describes how to reformulate primitive IOA programs into an equivalent but more regular
(desugared) form that is used in later definitions in this note. Section 5 treats IOA programs
for composite I/O automata: it introduces notations for describing the syntactic structures that
appear in these programs, describes resortings induced by them, and lists syntactic and semantic
conditions that these programs must satisfy to represent valid composite I/O automata. Section 6
describes the translation of the name spaces of component automata into a unified name space
for the composite automaton. Section 7 shows how to expand an IOA program for a composite
automaton into an equivalent IOA program for a primitive automaton. The expansion is generated
by combining syntactic structures of the desugared programs for the component automata after
applying appropriate replacements of sorts and variables. Section 8 details the expansion of the
composite automaton introduced in Section 2 using the desugared forms developed throughout
Sections 4–6 and the techniques described in Section 7. Finally, Section 9 gives a precise definition
of the resortings and substitutions used to replace sorts and variables. |