2.4.2. Defining an automaton

An automaton $𝒜$ of a global constraint $𝒞$ is defined by

$\langle 𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}$, $𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}𝒟\mathrm{𝑜𝑚𝑎𝑖𝑛}$, $𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}𝒜\mathrm{𝑟𝑔}$, $𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}𝒜\mathrm{𝑟𝑔}𝒫\mathrm{𝑎𝑡𝑡𝑒𝑟𝑛}$,

$𝒞\mathrm{𝑜𝑢𝑛𝑡𝑒𝑟𝑠}$, $𝒜\mathrm{𝑟𝑟𝑎𝑦𝑠}$, $𝒮\mathrm{𝑡𝑎𝑡𝑒𝑠}$, $𝒯\mathrm{𝑟𝑎𝑛𝑠𝑖𝑡𝑖𝑜𝑛𝑠}\rangle$

where:

• $𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}$ is the sequence of variables $S_0,\cdots ,S_{m-1}$ corresponding to the signature of the constraint $𝒞$.

• $𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}𝒟\mathrm{𝑜𝑚𝑎𝑖𝑛}$ is an interval that defines the range of possible values of the variables of $𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}$.

• $𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}𝒜\mathrm{𝑟𝑔}$ is the signature argument ${𝒮}_0,\cdots ,{𝒮}_{m-1}$ of the constraint $𝒞$. The link between the variables of ${𝒮}_i$ and the variable $S_i$ $(0\le i<m)$ is done by writing down the signature constraint ${\Psi }_{𝒞}(S_i,{𝒮}_i)$.

• When used, $𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}𝒜\mathrm{𝑟𝑔}𝒫\mathrm{𝑎𝑡𝑡𝑒𝑟𝑛}$ defines a symbolic name for each term of $𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}𝒜\mathrm{𝑟𝑔}$. These names can be used within the description of a transition for expressing an additional condition for triggering the corresponding transition.

• $𝒞\mathrm{𝑜𝑢𝑛𝑡𝑒𝑟𝑠}$ is the, possibly empty, list of all counters used in the automaton $𝒜$. Each counter is described by a term $\mathrm{t}(\mathrm{𝐶𝑜𝑢𝑛𝑡𝑒𝑟},$ $\mathrm{𝐼𝑛𝑖𝑡𝑖𝑎𝑙𝑉𝑎𝑙𝑢𝑒},$ $\mathrm{𝐹𝑖𝑛𝑎𝑙𝑉𝑎𝑟𝑖𝑎𝑏𝑙𝑒})$ where $\mathrm{𝐶𝑜𝑢𝑛𝑡𝑒𝑟}$ is a symbolic name representing the counter, $\mathrm{𝐼𝑛𝑖𝑡𝑖𝑎𝑙𝑉𝑎𝑙𝑢𝑒}$ is an integer giving the value of the counter in the initial state of $𝒜$, and $\mathrm{𝐹𝑖𝑛𝑎𝑙𝑉𝑎𝑟𝑖𝑎𝑏𝑙𝑒}$ gives the variable that should be unified with the value of the counter in the accepting state of $𝒜$.

• $𝒜\mathrm{𝑟𝑟𝑎𝑦𝑠}$ is the, possibly empty, list of all arrays used in the automaton $𝒜$. Each array is described by a term $\mathrm{t}(\mathrm{𝐴𝑟𝑟𝑎𝑦},$ $\mathrm{𝐼𝑛𝑖𝑡𝑖𝑎𝑙𝑉𝑎𝑙𝑢𝑒},$ $\mathrm{𝐹𝑖𝑛𝑎𝑙𝐶𝑜𝑛𝑠𝑡𝑟𝑎𝑖𝑛𝑡})$ where $\mathrm{𝐴𝑟𝑟𝑎𝑦}$ is a symbolic name representing the array, $\mathrm{𝐼𝑛𝑖𝑡𝑖𝑎𝑙𝑉𝑎𝑙𝑢𝑒}$ is an integer giving the value of all the entries of the array in the initial state of $𝒜$. $\mathrm{𝐹𝑖𝑛𝑎𝑙𝐶𝑜𝑛𝑠𝑡𝑟𝑎𝑖𝑛𝑡}$ denotes an existing constraint of the catalogue that should hold in the accepting state of $𝒜$. Arguments of this constraint correspond to collections of variables that are bound to array of counters, or to variables that are bound to counters declared in $𝒞\mathrm{𝑜𝑢𝑛𝑡𝑒𝑟𝑠}$. For an array of counters we only consider those entries that are located between the first and the last entries that were modified while triggering a transition of $𝒜$.

• $𝒮\mathrm{𝑡𝑎𝑡𝑒𝑠}$ is the list of states of $𝒜$, where each state has the form $\mathrm{source}\left(\mathrm{𝑖𝑑}\right)$, $\mathrm{sink}\left(\mathrm{𝑖𝑑}\right)$ or $\mathrm{node}\left(\mathrm{𝑖𝑑}\right)$. $\mathrm{𝑖𝑑}$ is a unique identifier associated with each state. Finally, $\mathrm{source}\left(\mathrm{𝑖𝑑}\right)$ and $\mathrm{sink}\left(\mathrm{𝑖𝑑}\right)$ respectively denote the initial and the accepting state of $𝒜$. An automaton has a single initial state and at least one accepting state. The initial and accepting states may coincide.

• $𝒯\mathrm{𝑟𝑎𝑛𝑠𝑖𝑡𝑖𝑜𝑛𝑠}$ is the list of transitions of $𝒜$. Each transition $t$ has the form $\mathrm{arc}({\mathrm{𝑖𝑑}}_1,$ $\mathrm{𝑙𝑎𝑏𝑒𝑙},$ ${\mathrm{𝑖𝑑}}_2)$ or $\mathrm{arc}({\mathrm{𝑖𝑑}}_1,$ $\mathrm{𝑙𝑎𝑏𝑒𝑙},$ ${\mathrm{𝑖𝑑}}_2,$ $\mathrm{𝑐𝑜𝑢𝑛𝑡𝑒𝑟𝑠})$. ${\mathrm{𝑖𝑑}}_1$ and ${\mathrm{𝑖𝑑}}_2$ respectively correspond to the state just before and just after $t$, while $\mathrm{𝑙𝑎𝑏𝑒𝑙}$ denotes the value that the signature variable should have in order to trigger $t$. When used, $\mathrm{𝑐𝑜𝑢𝑛𝑡𝑒𝑟𝑠}$ gives for each counter of $𝒞\mathrm{𝑜𝑢𝑛𝑡𝑒𝑟𝑠}$ its value after firing the corresponding transition. This value is specified by an arithmetic expression involving counters, constants, as well as usual arithmetic functions, such as $+$, $-$, $min$, or $max$. The order used in the $\mathrm{𝑐𝑜𝑢𝑛𝑡𝑒𝑟𝑠}$ list is identical to the order used in $𝒞\mathrm{𝑜𝑢𝑛𝑡𝑒𝑟𝑠}$.