--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/infinite.pl	Fri Jan 19 09:16:27 2001 +0900
@@ -0,0 +1,62 @@
+/*
+ Copyright (C) 2001, Shinji Kono, University of the Ryukyus
+
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license, but changing it is not allowed.  You can also
+ use this wording to make the terms for other programs.
+
+ send your comments to kono@ie.u-ryukyu.ac.jp
+ $Header$
+
+ Infinite satisfiability/validity checker
+
+A set of non-empty-exit looping states represents infinite
+interval in ITL. The loop can contains deterministic state
+choice. This should correspond Rabin/Strreet Automaton
+that is non-deterministic Buchi automaton.
+
+The algorith works in depth first way.
+
+ */
+
+:-dynamic found_infinite/0.
+
+infinite:-
+    retract_all(found_infinite),
+    infinite(L),
+    write_infinite_seq(L).
+infinite:-
+    found_infinite,!.
+infinite:-
+    write('unsatisfiable in infinite interval.'),nl.
+
+write_infinite_seq(L) :-
+    write('satisfiable in infinite interval: '),
+    write(L),nl.
+
+retract_all(X) :-
+    retract(X),fail.
+retract_all(_).
+
+infinite([S|L]) :-
+    links(_,S),
+    more_only(S),   % search more only node
+    more_only_loop(S,S,L,[]),
+    assert(found_infinite).
+infinite([]) :-
+    found_infinite.
+
+more_only(S) :- 
+    state(S,[empty|_],true),!,fail.
+more_only(S) :- number(S).
+
+more_only_loop(S,S0,L,L1) :-
+    links(N,S),
+    more_only_loop1(N,S0,L,L1).
+
+more_only_loop1(S,S,L,L) :-!.
+more_only_loop1(N,S,[N|L],L1) :-
+    more_only(N),
+    more_only_loop(N,S,L,L1).
+
+/* end */