Availability:
:- use_module(library(clpfd)).
automaton(+Sequence,
?Template, +Signature, +Nodes, +Arcs, +Counters, +Initials, ?Finals)source(Node) and sink(Node) terms. Arcs
is a list of
arc(Node,Integer,Node) and arc(Node,Integer,Node,Exprs)
terms that denote the automaton's transitions. Each node is represented
by an arbitrary term. Transitions that are not mentioned go to an
implicit failure node. Exprs is a list of arithmetic
expressions, of the same length as Counters. In each
expression, variables occurring in Counters symbolically
refer to previous counter values, and variables occurring in Template
refer to the current element of Sequence. When a transition
containing arithmetic expressions is taken, each counter is updated
according to the result of the corresponding expression. When a
transition without arithmetic expressions is taken, all counters remain
unchanged.
Counters is a list of variables. Initials is a
list of finite domain variables or integers denoting, in the same order,
the initial value of each counter. These values are related to Finals
according to the arithmetic expressions of the taken transitions.
The following example is taken from Beldiceanu, Carlsson, Debruyne and Petit: "Reformulation of Global Constraints Based on Constraints Checkers", Constraints 10(4), pp 339-362 (2005). It relates a sequence of integers and finite domain variables to its number of inflexions, which are switches between strictly ascending and strictly descending subsequences:
sequence_inflexions(Vs, N) :-
variables_signature(Vs, Sigs),
automaton(Sigs, _, Sigs,
[source(s),sink(i),sink(j),sink(s)],
[arc(s,0,s), arc(s,1,j), arc(s,2,i),
arc(i,0,i), arc(i,1,j,[C+1]), arc(i,2,i),
arc(j,0,j), arc(j,1,j),
arc(j,2,i,[C+1])],
[C], [0], [N]).
variables_signature([], []).
variables_signature([V|Vs], Sigs) :-
variables_signature_(Vs, V, Sigs).
variables_signature_([], _, []).
variables_signature_([V|Vs], Prev, [S|Sigs]) :-
V #= Prev #<==> S #= 0,
Prev #< V #<==> S #= 1,
Prev #> V #<==> S #= 2,
variables_signature_(Vs, V, Sigs).
Example queries:
?- sequence_inflexions([1,2,3,3,2,1,3,0], N). N = 3. ?- length(Ls, 5), Ls ins 0..1, sequence_inflexions(Ls, 3), label(Ls). Ls = [0, 1, 0, 1, 0] ; Ls = [1, 0, 1, 0, 1].