this repo has no description
dekker.one
1include "fzn_regular_nfa.mzn";
2include "fzn_regular_nfa_reif.mzn";
3include "fzn_regular_nfa_set.mzn";
4include "fzn_regular_nfa_set_reif.mzn";
5
6/** @group globals.extensional
7 The sequence of values in array \a x (which must all be in the range 1..\a S)
8 is accepted by the NFA of \a Q states with input 1..\a S and transition
9 function \a d (which maps (1..\a Q, 1..\a S) -> set of 1..\a Q)) and initial state \a q0
10 (which must be in 1..\a Q) and accepting states \a F (which all must be in
11 1..\a Q).
12*/
13predicate regular_nfa(array[int] of var int: x, int: Q, int: S,
14 array[int,int] of set of int: d, int: q0, set of int: F) =
15 assert(Q > 0,
16 "regular_nfa: 'Q' must be greater than zero",
17
18 assert(S > 0,
19 "regular_nfa: 'S' must be greater than zero",
20
21 assert(index_set_1of2(d) = 1..Q /\ index_set_2of2(d) == 1..S,
22 "regular_nfa: the transition function 'd' must be [1..Q,1..S]",
23
24 assert(forall([d[i, j] subset 1..Q | i in 1..Q, j in 1..S]),
25 "regular_nfa: transition function 'd' points to states outside 1..Q",
26
27 % Nb: we need the parentheses around the expression otherwise the
28 % parser thinks it's a generator call!
29 assert((q0 in 1..Q),
30 "regular: start state 'q0' not in 1..Q",
31
32 assert(F subset 1..Q,
33 "regular: final states in 'F' contain states outside 1..Q",
34
35 fzn_regular_nfa(x,Q,S,d,q0,F)
36
37 ))))));
38
39/** @group globals.extensional
40 The sequence of values in array \a x (which must all be in the range \a S)
41 is accepted by the NFA of \a Q states with input \a S and transition
42 function \a d (which maps (1..\a Q, \a S) -> set of 1..\a Q)) and initial state \a q0
43 (which must be in 1..\a Q) and accepting states \a F (which all must be in
44 1..\a Q).
45*/
46predicate regular_nfa(array[int] of var int: x, int: Q, set of int: S,
47 array[int,int] of set of int: d, int: q0, set of int: F) =
48 assert(Q > 0,
49 "regular_nfa: 'Q' must be greater than zero",
50
51 assert(card(S) > 0,
52 "regular_nfa: 'S' must be non empty",
53
54 assert(S = min(S)..max(S),
55 "regular_nfa: 'S' must be a range",
56
57 assert(index_set_1of2(d) = 1..Q /\ index_set_2of2(d) == S,
58 "regular_nfa: the transition function 'd' must be [1..Q,S]",
59
60 assert(forall([d[i, j] subset 1..Q | i in 1..Q, j in S]),
61 "regular_nfa: transition function 'd' points to states outside 1..Q",
62
63 % Nb: we need the parentheses around the expression otherwise the
64 % parser thinks it's a generator call!
65 assert((q0 in 1..Q),
66 "regular: start state 'q0' not in 1..Q",
67
68 assert(F subset 1..Q,
69 "regular: final states in 'F' contain states outside 1..Q",
70
71 fzn_regular_nfa(x,Q,S,d,q0,F)
72
73 )))))));