Constraint Automata

Informally, constraint automata (CA) are a type of Finite Automata, similar to I/O automata, whose transitions represent input/output operations on a set of ports N. A transition fires when all its ports are "active", and data flows between the ports as specified by the associated guard condition.

The example shows the CA for an XOR connector, with input port A and output ports B and C. The two transitions correspond to data flowing from A to B or C.

More generally, the intuitive meaning of CA as an operational model for Reo connectors is as follows. The states represent the configurations of the connector, the transitions the possible one-step behaviour. The meaning of q-[N,g]->p is that in configuration q the ports in N have the possibility to perform I/O operations that meet the guard g and that lead to configuration p, while the other ports not in N do not perform any I/O-operation.

Constraint Automata with Memory

The standard CA representation of a stateful connector such as a FIFO requires a unique state for each possible value in the data domain, leading to a possibly infinite state system. To overcome this problem we introduce the notion of state memory.

The example shows the CA for a FIFO where states p and q correspond to the empty and full states of the FIFO respectively. Note memory cell m in state q that stores the value read from input A. In the guards we refer to the memory cell as $s.m or $t.m depending on whether the cell is the source or target of data flow.

Timed Constraint Automata

Timed Constraint Automata (TCA) add the notion of real-time to CA, and can be seen as a combination of CA and timed automata with location invariants.

TCA have two kinds of transitions: invisible transitions, which represent internal changes of the locations caused by some time constraints (without data flow through any of the ports), and visible transitions that represent the synchronised execution of I/O-operations at some of the ports. The major conceptual difference to other timed (coordination) models is that actions which happen at the same time are truly atomic and thus collapse to a single transitions. As a consequence, a positive amount of time has to elapse before every visible transition, i.e., every transition that involves data flow.

The example shows the TCA for 1-bounded FIFO with expiration. The FIFO looses any data item that remains in the buffer for more than 3 time units. If the data item cannot be delivered within this time, the TCA takes the invisible transition back to state p, thereby discarding the data item. Clock x is used to measure the dwell time in state q, the invariant 'x<=3' forces the TCA to leave state q after a maximum of three time units.

Tool support

References