2.4.2. Defining an automaton

An automaton 𝒜 of a global constraint 𝒞 is defined by

𝒮𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒, 𝒮𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒𝒟𝑜𝑚𝑎𝑖𝑛, 𝒮𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒𝒜𝑟𝑔, 𝒮𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒𝒜𝑟𝑔𝒫𝑎𝑡𝑡𝑒𝑟𝑛,

𝒞𝑜𝑢𝑛𝑡𝑒𝑟𝑠, 𝒜𝑟𝑟𝑎𝑦𝑠, 𝒮𝑡𝑎𝑡𝑒𝑠, 𝒯𝑟𝑎𝑛𝑠𝑖𝑡𝑖𝑜𝑛𝑠

where:

  • 𝒮𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒 is the sequence of variables S 0 ,,S m-1 corresponding to the signature of the constraint 𝒞.

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

  • 𝒮𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒𝒜𝑟𝑔 is the signature argument 𝒮 0 ,,𝒮 m-1 of the constraint 𝒞. The link between the variables of 𝒮 i and the variable S i (0i<m) is done by writing down the signature constraint Ψ 𝒞 (S i ,𝒮 i ).

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

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

  • 𝒜𝑟𝑟𝑎𝑦𝑠 is the, possibly empty, list of all arrays used in the automaton 𝒜. Each array is described by a term t(𝐴𝑟𝑟𝑎𝑦, 𝐼𝑛𝑖𝑡𝑖𝑎𝑙𝑉𝑎𝑙𝑢𝑒, 𝐹𝑖𝑛𝑎𝑙𝐶𝑜𝑛𝑠𝑡𝑟𝑎𝑖𝑛𝑡) where 𝐴𝑟𝑟𝑎𝑦 is a symbolic name representing the array, 𝐼𝑛𝑖𝑡𝑖𝑎𝑙𝑉𝑎𝑙𝑢𝑒 is an integer giving the value of all the entries of the array in the initial state of 𝒜. 𝐹𝑖𝑛𝑎𝑙𝐶𝑜𝑛𝑠𝑡𝑟𝑎𝑖𝑛𝑡 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 𝒞𝑜𝑢𝑛𝑡𝑒𝑟𝑠. 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 𝒜.

  • 𝒮𝑡𝑎𝑡𝑒𝑠 is the list of states of 𝒜, where each state has the form source (𝑖𝑑), sink (𝑖𝑑) or node (𝑖𝑑). 𝑖𝑑 is a unique identifier associated with each state. Finally, source (𝑖𝑑) and sink (𝑖𝑑) 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.

  • 𝒯𝑟𝑎𝑛𝑠𝑖𝑡𝑖𝑜𝑛𝑠 is the list of transitions of 𝒜. Each transition t has the form arc (𝑖𝑑 1 , 𝑙𝑎𝑏𝑒𝑙, 𝑖𝑑 2 ) or arc (𝑖𝑑 1 , 𝑙𝑎𝑏𝑒𝑙, 𝑖𝑑 2 , 𝑐𝑜𝑢𝑛𝑡𝑒𝑟𝑠). 𝑖𝑑 1 and 𝑖𝑑 2 respectively correspond to the state just before and just after t, while 𝑙𝑎𝑏𝑒𝑙 denotes the value that the signature variable should have in order to trigger t. When used, 𝑐𝑜𝑢𝑛𝑡𝑒𝑟𝑠 gives for each counter of 𝒞𝑜𝑢𝑛𝑡𝑒𝑟𝑠 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 𝑐𝑜𝑢𝑛𝑡𝑒𝑟𝑠 list is identical to the order used in 𝒞𝑜𝑢𝑛𝑡𝑒𝑟𝑠.

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

  • 𝒮𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒=S 0 ,S 1 ,,S n-2 ,

  • 𝒮𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒𝒟𝑜𝑚𝑎𝑖𝑛=0..2,

  • 𝒮𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒𝒜𝑟𝑔 = 𝑣𝑎𝑟𝑠[0],𝑣𝑎𝑟𝑠[1],,𝑣𝑎𝑟𝑠[n-2],𝑣𝑎𝑟𝑠[n-1],

  • 𝒮𝑖𝑔𝑛𝑎𝑡𝑢𝑟𝑒𝒜𝑟𝑔𝒫𝑎𝑡𝑡𝑒𝑟𝑛 is not used,

  • 𝒞𝑜𝑢𝑛𝑡𝑒𝑟𝑠=t(c,0,𝑛𝑖𝑛𝑓),

  • 𝒮𝑡𝑎𝑡𝑒𝑠=[𝑠𝑜𝑢𝑟𝑐𝑒(s),𝑠𝑖𝑛𝑘(s),𝑠𝑖𝑛𝑘(i),𝑠𝑖𝑛𝑘(j)],

  • 𝒯𝑟𝑎𝑛𝑠𝑖𝑡𝑖𝑜𝑛𝑠=[ arc (s,1,s), arc (s,2,i), arc (s,0,j), arc (i,1,i), arc (i,2,i), arc (i,0,j,[c+1]), arc (j,1,j), arc (j,0,j), arc (j,2,i,[c+1]).

The signature constraint relating each pair of variables 𝑣𝑎𝑟𝑠[i],𝑣𝑎𝑟𝑠[i+1] to the signature variable S i is defined as follows: Ψ 𝚒𝚗𝚏𝚕𝚎𝚡𝚒𝚘𝚗 (S i ,𝑣𝑎𝑟𝑠[i],𝑣𝑎𝑟𝑠[i+1])𝑣𝑎𝑟𝑠[i]>𝑣𝑎𝑟𝑠[i+1]S i =0 𝑣𝑎𝑟𝑠[i]=𝑣𝑎𝑟𝑠[i+1]S i =1 𝑣𝑎𝑟𝑠[i]<𝑣𝑎𝑟𝑠[i+1]S i =2. The sequence of transitions triggered on the ground instance 𝚒𝚗𝚏𝚕𝚎𝚡𝚒𝚘𝚗(4, [3,3,1,4,5,5,6,5,5,6,3]) is s c=0 3=3S 0 =1s 3>1S 1 =0j c=1 1<4S 2 =2i 4<5S 3 =2i 5=5S 4 =1i 5<6S 5 =2i c=2 6>5S 6 =0j 5=5S 7 =1j c=3 5<6S 8 =2i c=4 6>3S 9 =0j. 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 𝑛𝑖𝑛𝑓 of the 𝚒𝚗𝚏𝚕𝚎𝚡𝚒𝚘𝚗 constraint is fixed to the current value of the counter c, i.e. 𝑛𝑖𝑛𝑓=4.