|
6
|
1 /*
|
|
|
2 Copyright (C) 2001, Shinji Kono, University of the Ryukyus
|
|
|
3
|
|
|
4 Everyone is permitted to copy and distribute verbatim copies
|
|
|
5 of this license, but changing it is not allowed. You can also
|
|
|
6 use this wording to make the terms for other programs.
|
|
|
7
|
|
|
8 send your comments to kono@ie.u-ryukyu.ac.jp
|
|
|
9 $Header$
|
|
|
10
|
|
|
11 Infinite satisfiability/validity checker
|
|
|
12
|
|
15
|
13 A set of `more' looping states represents infinite
|
|
6
|
14 interval in ITL. The loop can contains deterministic state
|
|
|
15 choice. This should correspond Rabin/Strreet Automaton
|
|
|
16 that is non-deterministic Buchi automaton.
|
|
|
17
|
|
|
18 The algorith works in depth first way.
|
|
|
19
|
|
|
20 */
|
|
|
21
|
|
|
22 :-dynamic found_infinite/0.
|
|
|
23
|
|
|
24 infinite:-
|
|
|
25 retract_all(found_infinite),
|
|
|
26 infinite(L),
|
|
|
27 write_infinite_seq(L).
|
|
|
28 infinite:-
|
|
|
29 found_infinite,!.
|
|
|
30 infinite:-
|
|
|
31 write('unsatisfiable in infinite interval.'),nl.
|
|
|
32
|
|
|
33 write_infinite_seq(L) :-
|
|
10
|
34 write('satisfiable in infinite interval:'),nl,
|
|
12
|
35 write_infinite_seq1(L).
|
|
|
36 write_infinite_seq1([L]) :-!, % odd case.
|
|
|
37 make_hist([L,L],L1),
|
|
|
38 write_ce(L1,0),nl.
|
|
|
39 write_infinite_seq1(L) :-
|
|
16
|
40 insert_loop_mark(L,L1),
|
|
|
41 make_hist(L1,L2),
|
|
|
42 write_ce(L2,0),nl.
|
|
|
43
|
|
|
44 insert_loop_mark(L,L1) :-
|
|
|
45 last(L,Last),
|
|
|
46 insert_loop_mark(L,Last,L1).
|
|
|
47
|
|
|
48 last([Last],Last) :-!.
|
|
|
49 last([_|T],Last) :-
|
|
|
50 last(T,Last).
|
|
|
51
|
|
|
52 insert_loop_mark([Last|T],Last,[(*),Last|T]):-!.
|
|
|
53 insert_loop_mark([H|T],Last,[H|T1]):-
|
|
|
54 insert_loop_mark(T,Last,T1).
|
|
6
|
55
|
|
|
56 retract_all(X) :-
|
|
|
57 retract(X),fail.
|
|
|
58 retract_all(_).
|
|
|
59
|
|
9
|
60 infinite(L) :-
|
|
11
|
61 % 1 seems like original ITL formula that is root.
|
|
15
|
62 setof(S,links(S,1),Children),
|
|
16
|
63 more_node(1,Children,L,[],[1]).
|
|
6
|
64 infinite([]) :-
|
|
|
65 found_infinite.
|
|
|
66
|
|
16
|
67 infinite_node(S) :-
|
|
|
68 state(S,[empty|_],true),!,fail.
|
|
|
69 infinite_node(S) :- number(S).
|
|
13
|
70
|
|
16
|
71 %infinite_node(true) :- !.
|
|
|
72 %infinite_node(S) :-
|
|
|
73 % number(S),
|
|
|
74 % state(S,[more|_],_).
|
|
6
|
75
|
|
16
|
76 more_node(S,[S1|Children],[S|L],L1,Hist) :-
|
|
11
|
77 % write('checking '),write(S),nl,
|
|
16
|
78 infinite_node(S),
|
|
10
|
79 % starting false loop
|
|
16
|
80 more_loop(S1,Children,L,L1,[S|Hist],[S]).
|
|
|
81 more_node(S,Children,L,L1,Hist) :-
|
|
|
82 % goto one depth deeper
|
|
|
83 more_node1(Children,L,L1,[S|Hist]).
|
|
8
|
84
|
|
16
|
85 more_node1([H|_],L,L1,Hist) :-
|
|
|
86 not_member(H,Hist),
|
|
15
|
87 setof(S,links(S,H),Children),
|
|
16
|
88 more_node(H,Children,L,L1,Hist).
|
|
|
89 more_node1([_|T],L,L1,Hist) :-
|
|
|
90 more_node1(T,L,L1,Hist).
|
|
8
|
91
|
|
16
|
92 more_loop(true,_,[true|L],L,_Hist,_Seq) :-
|
|
15
|
93 assert(found_infinite).
|
|
16
|
94 more_loop(S,_,[S|L],L,_Hist,Seq) :-
|
|
9
|
95 member(S,Seq),!,
|
|
|
96 assert(found_infinite).
|
|
8
|
97 % we find the one
|
|
16
|
98 more_loop(S,_,L,L,Hist,_Seq) :-
|
|
8
|
99 member(S,Hist),!,
|
|
|
100 fail.
|
|
|
101 % end of this branch
|
|
16
|
102 more_loop(H,_,[H|L],L1,Hist,Seq) :-
|
|
|
103 infinite_node(H),!,
|
|
8
|
104 % still in the false interval
|
|
15
|
105 setof(S,links(S,H),Children),
|
|
16
|
106 more_loop1(Children,L,L1,[H|Hist],[H|Seq]).
|
|
|
107 more_loop(_,[S|T],L,L1,Hist,Seq) :-!,
|
|
|
108 % try another child
|
|
|
109 more_loop(S,T,L,L1,Hist,Seq).
|
|
|
110 % more_loop(H,[],L,L1,Hist,Seq) :-!,fail.
|
|
|
111 % empty case. fail and try another branch
|
|
|
112
|
|
|
113
|
|
|
114 more_loop1([H|_],L,L1,Hist,Seq) :-
|
|
15
|
115 setof(S,links(S,H),Children),
|
|
16
|
116 more_loop(H,Children,L,L1,Hist,Seq).
|
|
|
117 more_loop1([_|T],L,L1,Hist,Seq) :-
|
|
|
118 more_loop1(T,L,L1,Hist,Seq).
|
|
6
|
119
|
|
|
120 /* end */
|
