Specification Library

The specifications in this library are described in the indicated sections of the TIOA User Guide.

As noted below, some of these specification were formulated incorrectly in the first draft of the user guide. This shows how easy it is to make subtle errors when formulating a specification (and also the value of a static checker that catches many of these errors). Other examples call attention to the fact that the current version of the TIOA Checker is incomplete and at times fails to accept specifications that are in fact correct. In particular, the checker should, but at times does not, recognize that all natural numbers are also integers, which are also real numbers, etc. As illustrated below, it is usually possible to work around these deficiencies by choosing slightly different representations for state variables.

Built-in vocabulary definitions

Primitive data types

Booleans (Section 7.1.1)

Logical operators for the datatype Bool of boolean values

Natural numbers (Section 7.1.2)

Arithmetical operators for the datatype Nat of non-negative integers

Integers (Section 7.1.3)

Arithmetical operators for the datatype Int of all integers

Real numbers (Section 7.1.4)

Arithmetical operators for the datatype Real of real numbers

Real numbers plus infinity (Section 7.1.4)

Arithmetical operators for the datatype AugmentedReal of real numbers extended by plus and minus infinity

Characters (Section 7.1.5)

Alphabetic ordering operators for the datatype Char of letters and digits

Strings (Section 7.1.6)

Operators for the datatype String of strings of characters

Type constructors

Arrays (Section 7.2.1)

Operators for the datatype Array[I1, ..., In, E] of n-dimensional arrays of elements (illustrated here n = 1)

Finite sets (Section 7.2.2)

Operators for the datatype Set[E] of finite sets of elements of type E (the same notations are used in mathematics for arbitrary sets, but TIOA by convention uses them only for finite sets)

Finite mappings (Section 7.2.3)

Operators for the datatype Map[I1, ..., In, E] of finite partial mappings with n-dimensional domains (illustrated here n = 1)

Finite multisets (Section 7.2.4)

Operators for the datatype Mset[E] of finite multisets of elements of type E (as for sets, TIOA by convention uses these notations only for finite multisets)

Sequences (Section 7.2.5)

Operators for the datatype Seq[E] of finite sequences of elements of type E

Extensions by nil (Section 7.2.6)

Operators for the datatype Null[E], which consists of copies of the elements of datatype E plus one additional element nil

Sample specifications

Alarm (Figure 3.3, page 9)

Component of the AlarmClock automaton

AlarmClock (Figure 3.5, page 10)

Illustrates the composition of two automata

Arrange (Page 14)

Illustrates use of local variable

ArrangeV (Page 17)

Variant of Arrange mentioned to illustrate use of ensuring clause

Channel (Figure 3.1, page 7)

Description of untimed FIFO communication channel

Clock (Figure 3.4, page 10)

Faulty specification for component of the AlarmClock automaton. The assignment whenToShow := floor(now) is invalid, because whenToShow has type Nat and floor(now) has type Int. Of course, we "know" that floor(now) >= 0 is an invariant of the automaton (because time never decreases), but static checking does not attempt to discover and use invariants.

ClockV1 (Variant of Figure 3.4, page 10)

This variant provides a workaround for the faulty specification of the Clock automaton. The workaround is not recommended, because it employs a seemingly superfluous use of the abs function to fix the type error.

ClockSync (Figure 4.4, page 19)

Illustrates constraints on derivatives in an evolve clause. Pending a more complete implementation in the TIOA checker of invariants for trajectories of timed automata, we use a vocabulary to introduce a notation for asserting that a trajectory is continuous (and not just piecewise continuous).

ClockV2 (Variant of Figure 3.4, page 10)

This variant fixes the type error by using a more fortuitous representation of the state instead of by using a trick. However, it still uses the trick to work around a bug in the current version of the TIOA Checker, which should allow the expression whenToShow = floor(now), because every natural number is also an integer, and the value of the expression is simply false if the integer floor(now) is negative.

Draw (Page 27)

Illustrates the use of a union type

IndexedChannel (Figure 4.1, page 11)

Illustrates an internal action

LossyChannel (Variant of Figure 3.2, page 8)

Illustrates automaton and const parameters (as for Figure 3.2, this specification fails to check just yet)

Multicast (Figure 4.2, page 16)

Illustrates for statement

PitchTwo (Page 13)

Illustrates use of a local parameter

PitchTwoA (Page 13)

Illustrates elimination of local parameters

Thermostat (Figure 4.3, page 18)

TimedChannel (Figure 3.2, page 8)

Illustrates a timed input/output automaton (this specification fails to check, because the TIOA Checker does not recognize yet that Real and DiscreteReal datatypes have the same elements)

Illustrates timed automaton with two trajectories

TrafficLight (Page 26)

Illustrates the use of an enumeration type

sampleVocab (Page 26)

Illustrates the definition enumeration, tuple, and union types