### 2.4.2. Defining an automaton

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

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

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

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}$ $\left(0\le i is done by writing down the signature constraint ${\Psi }_{𝒞}\left({S}_{i},{𝒮}_{i}\right)$.

• 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}\left(\mathrm{𝐶𝑜𝑢𝑛𝑡𝑒𝑟},$ $\mathrm{𝐼𝑛𝑖𝑡𝑖𝑎𝑙𝑉𝑎𝑙𝑢𝑒},$ $\mathrm{𝐹𝑖𝑛𝑎𝑙𝑉𝑎𝑟𝑖𝑎𝑏𝑙𝑒}\right)$ 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}\left(\mathrm{𝐴𝑟𝑟𝑎𝑦},$ $\mathrm{𝐼𝑛𝑖𝑡𝑖𝑎𝑙𝑉𝑎𝑙𝑢𝑒},$ $\mathrm{𝐹𝑖𝑛𝑎𝑙𝐶𝑜𝑛𝑠𝑡𝑟𝑎𝑖𝑛𝑡}\right)$ 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}\left({\mathrm{𝑖𝑑}}_{1},$ $\mathrm{𝑙𝑎𝑏𝑒𝑙},$ ${\mathrm{𝑖𝑑}}_{2}\right)$ or $\mathrm{arc}\left({\mathrm{𝑖𝑑}}_{1},$ $\mathrm{𝑙𝑎𝑏𝑒𝑙},$ ${\mathrm{𝑖𝑑}}_{2},$ $\mathrm{𝑐𝑜𝑢𝑛𝑡𝑒𝑟𝑠}\right)$. ${\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{𝑜𝑢𝑛𝑡𝑒𝑟𝑠}$.

EXAMPLE: As an illustrative example we give the description of the automaton associated with the $\mathrm{𝚒𝚗𝚏𝚕𝚎𝚡𝚒𝚘𝚗}$$\left(\mathrm{𝑛𝑖𝑛𝑓},\mathrm{𝑣𝑎𝑟𝑠}\right)$ constraint. We have:

• $𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}={S}_{0},{S}_{1},\cdots ,{S}_{n-2}$,

• $𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}𝒟\mathrm{𝑜𝑚𝑎𝑖𝑛}=0..2$,

• $𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}𝒜\mathrm{𝑟𝑔}$ = $〈\mathrm{𝑣𝑎𝑟𝑠}\left[0\right],\mathrm{𝑣𝑎𝑟𝑠}\left[1\right]〉,\cdots ,〈\mathrm{𝑣𝑎𝑟𝑠}\left[n-2\right],\mathrm{𝑣𝑎𝑟𝑠}\left[n-1\right]〉$,

• $𝒮\mathrm{𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒}𝒜\mathrm{𝑟𝑔}𝒫\mathrm{𝑎𝑡𝑡𝑒𝑟𝑛}$ is not used,

• $𝒞\mathrm{𝑜𝑢𝑛𝑡𝑒𝑟𝑠}=\mathrm{t}\left(c,0,\mathrm{𝑛𝑖𝑛𝑓}\right)$,

• $𝒮\mathrm{𝑡𝑎𝑡𝑒𝑠}=\left[\mathrm{𝑠𝑜𝑢𝑟𝑐𝑒}\left(s\right),\mathrm{𝑠𝑖𝑛𝑘}\left(s\right),\mathrm{𝑠𝑖𝑛𝑘}\left(i\right),\mathrm{𝑠𝑖𝑛𝑘}\left(j\right)\right]$,

• $𝒯\mathrm{𝑟𝑎𝑛𝑠𝑖𝑡𝑖𝑜𝑛𝑠}=\left[\mathrm{arc}\left(s,1,s\right)$, $\mathrm{arc}\left(s,2,i\right)$, $\mathrm{arc}\left(s,0,j\right)$, $\mathrm{arc}\left(i,1,i\right)$, $\mathrm{arc}\left(i,2,i\right)$, $\mathrm{arc}\left(i,0,j,\left[c+1\right]\right)$, $\mathrm{arc}\left(j,1,j\right)$, $\mathrm{arc}\left(j,0,j\right)$, $\mathrm{arc}\left(j,2,i,\left[c+1\right]\right)$.

The signature constraint relating each pair of variables $〈\mathrm{𝑣𝑎𝑟𝑠}\left[i\right],\mathrm{𝑣𝑎𝑟𝑠}\left[i+1\right]〉$ to the signature variable ${S}_{i}$ is defined as follows: ${\Psi }_{\mathrm{𝚒𝚗𝚏𝚕𝚎𝚡𝚒𝚘𝚗}}\left({S}_{i},\mathrm{𝑣𝑎𝑟𝑠}\left[i\right],\mathrm{𝑣𝑎𝑟𝑠}\left[i+1\right]\right)\equiv \mathrm{𝑣𝑎𝑟𝑠}\left[i\right]>\mathrm{𝑣𝑎𝑟𝑠}\left[i+1\right]⇔{S}_{i}=0\wedge \mathrm{𝑣𝑎𝑟𝑠}\left[i\right]=\mathrm{𝑣𝑎𝑟𝑠}\left[i+1\right]⇔{S}_{i}=1\wedge \mathrm{𝑣𝑎𝑟𝑠}\left[i\right]<\mathrm{𝑣𝑎𝑟𝑠}\left[i+1\right]⇔{S}_{i}=2$. The sequence of transitions triggered on the ground instance $\mathrm{𝚒𝚗𝚏𝚕𝚎𝚡𝚒𝚘𝚗}$$\left(4$, $\left[3,3,1,4,5,5,6,5,5,6,3\right]\right)$ is $\frac{s}{c=0}\stackrel{3=3⇔{S}_{0}=1}{\to }s\stackrel{3>1⇔{S}_{1}=0}{\to }j\underset{c=1}{\overset{1<4⇔{S}_{2}=2}{\to }}i\stackrel{4<5⇔{S}_{3}=2}{\to }i\stackrel{5=5⇔{S}_{4}=1}{\to }i\stackrel{5<6⇔{S}_{5}=2}{\to }i\underset{c=2}{\overset{6>5⇔{S}_{6}=0}{\to }}j\stackrel{5=5⇔{S}_{7}=1}{\to }j\underset{c=3}{\overset{5<6⇔{S}_{8}=2}{\to }}i\underset{c=4}{\overset{6>3⇔{S}_{9}=0}{\to }}j$. Each transition gives the corresponding condition and, possibly, the value of the counter $c$ just after firing that transition. After the last encountered state $j$ the first argument $\mathrm{𝑛𝑖𝑛𝑓}$ of the $\mathrm{𝚒𝚗𝚏𝚕𝚎𝚡𝚒𝚘𝚗}$ constraint is fixed to the current value of the counter $c$, i.e. $\mathrm{𝑛𝑖𝑛𝑓}=4$.