### view infinite.pl @ 10:f2aa38ce0787

author kono Fri, 19 Jan 2001 23:14:00 +0900 95897517e464 30c6f64102fa
line wrap: on
line source
```
/*
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.

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:'),nl,
make_hist(L,L1),
write_ce(L1,0),nl.

retract_all(X) :-
retract(X),fail.
retract_all(_).

infinite(L) :-
more_only_node(1,Children,L,[],[1]).
infinite([]) :-
found_infinite.

more_only(S) :-
state(S,[empty|_],true),!,fail.
more_only(S) :- number(S).

more_only_node(S,[S1|Children],[S|L],L1,Hist) :-
more_only(S),!,
% starting false loop
more_only_loop(S1,Children,L,L1,[S|Hist],[S]).
more_only_node(_,Children,L,L1,Hist) :- % goto one depth deeper
more_only_node1(Children,L,L1,Hist).

more_only_node1([H|_],L,L1,Hist) :-
more_only_node(H,Children,L,L1,Hist).
more_only_node1([_|T],L,L1,Hist) :-
more_only_node(T,L,L1,Hist).

more_only_loop(S,_,L,L,_Hist,Seq) :-
member(S,Seq),!,
assert(found_infinite).
% we find the one
more_only_loop(S,_,L,L,Hist,_Seq) :-
member(S,Hist),!,
fail.
% end of this branch
more_only_loop(H,_,[H|L],L1,Hist,Seq) :-
more_only(H),!,
% still in the false interval
more_only_loop1(Children,L,L1,[H|Hist],[H|Seq]).
more_only_loop(H,[S|_],[H|L],L1,Hist,_) :-
% false interval ends, start new search in depth first way