# 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

- ECT contains a Graphical automata editor?, a plugin for converting Reo connectors to CAs, and a plugin for generating propositional formulas with linear arithmetic from TCAs.
- The Vereofy model checker also uses CAs internally.
- How to use the extensible automata model describes the underlying Extendible automata model for creating constraint automata programatically.

## References

- Modeling Component Connectors in Reo by Constraint Automata.

F. Arbab, C. Baier, M. Sirjani, and J.J.M.M. Rutten

Science of Computer Programming, Elsevier, Vol. 61, Issue 2, pp. 75-113, July 2006

- Models and Temporal Logical Specifications for Timed Component Connectors.

F. Arbab, C. Baier, F.S. de Boer, and J.J.M.M. Rutten

International Journal on Software and Systems Modeling, pp. 59-82, Vol. 6, No. 1, March 2007, Springer.

- SAT-based Verification for Timed Component Connectors.

Stephanie Kemper.

Proceedings of the 8th International Workshop on the Foundations of Coordination Languages and Software Architectures, FOCLASA'09,

Electronic Notes in Theoretical Computer Science, Volume 255