Mercurial > hg > Applications > Lite

comparison infinite.pl @ 15:816425e04ea7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix true - omega interval satisfiability
author kono
date Sat, 20 Jan 2001 21:21:44 +0900
parents d2aa6137e9a9
children 4360c2030303
comparison
equal deleted inserted replaced
14:0d896bcc1061 15:816425e04ea7
8 send your comments to kono@ie.u-ryukyu.ac.jp 8 send your comments to kono@ie.u-ryukyu.ac.jp
9 $Header$ 9 $Header$
10 10
11 Infinite satisfiability/validity checker 11 Infinite satisfiability/validity checker
12 12
13 A set of non-empty-exit looping states represents infinite 13 A set of `more' looping states represents infinite
14 interval in ITL. The loop can contains deterministic state 14 interval in ITL. The loop can contains deterministic state
15 choice. This should correspond Rabin/Strreet Automaton 15 choice. This should correspond Rabin/Strreet Automaton
16 that is non-deterministic Buchi automaton. 16 that is non-deterministic Buchi automaton.
17 17
18 The algorith works in depth first way. 18 The algorith works in depth first way.
44 retract(X),fail. 44 retract(X),fail.
45 retract_all(_). 45 retract_all(_).
46 46
47 infinite(L) :- 47 infinite(L) :-
48 % 1 seems like original ITL formula that is root. 48 % 1 seems like original ITL formula that is root.
49 setof(S,(links(S,1),integer(S)),Children), 49 setof(S,links(S,1),Children),
50 more_only_node(1,Children,L,[],[1]). 50 more_only_node(1,Children,L,[],[1]).
51 infinite([]) :- 51 infinite([]) :-
52 found_infinite. 52 found_infinite.
53 53
54 % more_only(S) :- 54 % more_only(S) :-
55 % state(S,[empty|_],true),!,fail. 55 % state(S,[empty|_],true),!,fail.
56 % more_only(S) :- number(S). 56 % more_only(S) :- number(S).
57 57
58 more_only(true) :- !.
58 more_only(S) :- 59 more_only(S) :-
59 number(S), 60 number(S),
60 state(S,[more|_],_). 61 state(S,[more|_],_).
61 62
62 more_only_node(S,[S1|Children],[S|L],L1,Hist) :- 63 more_only_node(S,[S1|Children],[S|L],L1,Hist) :-
63 % write('checking '),write(S),nl, 64 % write('checking '),write(S),nl,
64 more_only(S),!, 65 more_only(S),
65 % starting false loop 66 % starting false loop
66 more_only_loop(S1,Children,L,L1,[S|Hist],[S]). 67 more_only_loop(S1,Children,L,L1,[S|Hist],[S]).
67 more_only_node(_,Children,L,L1,Hist) :- % goto one depth deeper 68 more_only_node(S,Children,L,L1,Hist) :- % goto one depth deeper
68 more_only_node1(Children,L,L1,Hist). 69 more_only_node1(Children,L,L1,[S|Hist]).
69 70
71 more_only_node1([H|_],_L,_L1,Hist) :-
72 member(H,Hist),
73 !,
74 fail.
70 more_only_node1([H|_],L,L1,Hist) :- 75 more_only_node1([H|_],L,L1,Hist) :-
71 setof(S,(links(S,H),integer(S)),Children), 76 setof(S,links(S,H),Children),
72 more_only_node(H,Children,L,L1,Hist). 77 more_only_node(H,Children,L,L1,Hist).
73 more_only_node1([_|T],L,L1,Hist) :- 78 more_only_node1([_|T],L,L1,Hist) :-
74 more_only_node(T,L,L1,Hist). 79 more_only_node1(T,L,L1,Hist).
75 80
81 more_only_loop(true,_,[true|L],L,_Hist,_Seq) :-
82 assert(found_infinite).
76 more_only_loop(S,_,[S|L],L,_Hist,Seq) :- 83 more_only_loop(S,_,[S|L],L,_Hist,Seq) :-
77 member(S,Seq),!, 84 member(S,Seq),!,
78 assert(found_infinite). 85 assert(found_infinite).
79 % we find the one 86 % we find the one
80 more_only_loop(S,_,L,L,Hist,_Seq) :- 87 more_only_loop(S,_,L,L,Hist,_Seq) :-
82 fail. 89 fail.
83 % end of this branch 90 % end of this branch
84 more_only_loop(H,_,[H|L],L1,Hist,Seq) :- 91 more_only_loop(H,_,[H|L],L1,Hist,Seq) :-
85 more_only(H),!, 92 more_only(H),!,
86 % still in the false interval 93 % still in the false interval
87 setof(S,(links(S,H),integer(S)),Children), 94 setof(S,links(S,H),Children),
88 more_only_loop1(Children,L,L1,[H|Hist],[H|Seq]). 95 more_only_loop1(Children,L,L1,[H|Hist],[H|Seq]).
89 more_only_loop(H,[S|_],[H|L],L1,Hist,_) :- 96 more_only_loop(H,[S|_],[H|L],L1,Hist,_) :-
90 % false interval ends, start new search in depth first way 97 % false interval ends, start new search in depth first way
91 setof(S,(links(S,H),integer(S)),Children), 98 setof(S,links(S,H),Children),
92 % we already know S i not more_only 99 % we already know S i not more_only
93 more_only_node1(Children,L,L1,[H|Hist]). 100 more_only_node1(Children,L,L1,[H|Hist]).
94 101
95 more_only_loop1([H|_],L,L1,Hist,Seq) :- 102 more_only_loop1([H|_],L,L1,Hist,Seq) :-
96 setof(S,(links(S,H),integer(S)),Children), 103 setof(S,links(S,H),Children),
97 more_only_loop(H,Children,L,L1,Hist,Seq). 104 more_only_loop(H,Children,L,L1,Hist,Seq).
98 more_only_loop1([_|T],L,L1,Hist,Seq) :- 105 more_only_loop1([_|T],L,L1,Hist,Seq) :-
99 more_only_loop1(T,L,L1,Hist,Seq). 106 more_only_loop1(T,L,L1,Hist,Seq).
100 107
101 /* end */ 108 /* end */