this repo has no description
dekker.one
1predicate fzn_regular(array[int] of var int: x, int: Q, int: S,
2 array[int,int] of int: d, int: q0, set of int: F) =
3 let {
4 % If x has index set m..n-1, then a[m] holds the initial state
5 % (q0), and a[i+1] holds the state we're in after processing
6 % x[i]. If a[n] is in F, then we succeed (ie. accept the string).
7 int: m = min(index_set(x)),
8 int: n = max(index_set(x)) + 1,
9 array[m..n] of var 1..Q: a
10 } in
11 a[m] = q0 /\ % Set a[0].
12 forall(i in index_set(x)) (
13 x[i] in 1..S /\ % Do this in case it's a var.
14 a[i+1] = d[a[i], x[i]] % Determine a[i+1].
15 ) /\
16 a[n] in F; % Check the final state is in F.