|
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
|
|
|
13 A set of non-empty-exit looping states represents infinite
|
|
|
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) :-
|
|
|
34 write('satisfiable in infinite interval: '),
|
|
|
35 write(L),nl.
|
|
|
36
|
|
|
37 retract_all(X) :-
|
|
|
38 retract(X),fail.
|
|
|
39 retract_all(_).
|
|
|
40
|
|
9
|
41 infinite(L) :-
|
|
|
42 setof(S,(links(S,1),integer(S)),Children),
|
|
|
43 more_only_node(1,Children,L,[],[1]).
|
|
6
|
44 infinite([]) :-
|
|
|
45 found_infinite.
|
|
|
46
|
|
|
47 more_only(S) :-
|
|
|
48 state(S,[empty|_],true),!,fail.
|
|
|
49 more_only(S) :- number(S).
|
|
|
50
|
|
9
|
51 more_only_node(S,[S1|Children],[S|L],L1,Hist) :-
|
|
8
|
52 more_only(S),!,
|
|
9
|
53 more_only_loop(S1,Children,L,L1,[S|Hist],[S]).
|
|
8
|
54 more_only_node(_,Children,L,L1,Hist) :- % goto one depth deeper
|
|
|
55 more_only_node1(Children,L,L1,Hist).
|
|
|
56
|
|
9
|
57 more_only_node1([H|_],L,L1,Hist) :-
|
|
8
|
58 setof(S,(links(S,H),integer(S)),Children),
|
|
|
59 more_only_node(H,Children,L,L1,Hist).
|
|
|
60 more_only_node1([_|T],L,L1,Hist) :-
|
|
|
61 more_only_node(T,L,L1,Hist).
|
|
|
62
|
|
6
|
63
|
|
9
|
64 more_only_loop(S,_,L,L,_Hist,Seq) :-
|
|
|
65 member(S,Seq),!,
|
|
|
66 assert(found_infinite).
|
|
8
|
67 % we find the one
|
|
9
|
68 more_only_loop(S,_,L,L,Hist,_Seq) :-
|
|
8
|
69 member(S,Hist),!,
|
|
|
70 fail.
|
|
|
71 % end of this branch
|
|
9
|
72 more_only_loop(H,_,[H|L],L1,Hist,Seq) :-
|
|
8
|
73 more_only(H),!,
|
|
|
74 % still in the false interval
|
|
9
|
75 setof(S,(links(S,H),integer(S)),Children),
|
|
|
76 more_only_loop1(Children,L,L1,[H|Hist],[H|Seq]).
|
|
|
77 more_only_loop(H,[S|_],[H|L],L1,Hist,_) :-
|
|
|
78 % false interval ends, start new search in depth first way
|
|
8
|
79 setof(S,(links(S,H),integer(S)),Children),
|
|
|
80 % we already know S i not more_only
|
|
9
|
81 more_only_node1(Children,L,L1,[H|Hist]).
|
|
8
|
82
|
|
9
|
83 more_only_loop1([H|_],L,L1,Hist,Seq) :-
|
|
8
|
84 setof(S,(links(S,H),integer(S)),Children),
|
|
|
85 more_only_loop(H,Children,L,L1,Hist,Seq).
|
|
|
86 more_only_loop1([_|T],L,L1,Hist,Seq) :-
|
|
|
87 more_only_loop(T,L,L1,Hist,Seq).
|
|
6
|
88
|
|
|
89 /* end */
|
