/* Declare counters. Initially only integers, but other data-types

could be considered as well. All counters start at zero. */

counter int x, y, z, length;

// List automata. Automata transitions are labelled with intervals,

// and can specify counter increments/decrements. A counter can only

// be used in at most one automaton.

synchronised {

automaton A {

init s0;

s0 -> s1 [0, 10] { x += 1};

accepting s1, s2;

};

automaton B {

init t1;

t1 -> t2 [11, 22] { y += 1};

accepting t1, t2;

};

};

automaton C {

init s0;

s0 -> s1 [15] { z += 1 };

s1 -> s1 [15] { z += 1};

accepting s1;

};

// Specify a constraint on the final values of counters; check whether

// there is a word accepted by all automata for which the final counter

// values satisfy this constraints.

constraint z = 2x + 2y && !(x = 0);