/*
 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]) :-
    setof(S,links(S,0),Depth),
    member(S1,[0|Depth]),
    more_only_loop(S1,L,[],[S1]),
    assert(found_infinite).
infinite([]) :-
    found_infinite.

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

more_only_loop(S,L,L1,Hist) :-
    setof(N,links(N,S),Depth),
    member(S1,Depth),
    more_only_loop1(S1,L,L1,Hist).

more_only_loop1(S,L,L,Hist) :-
    member(S,Hist),
    !.
more_only_loop1(S,[N|L],L1,Hist) :-
    more_only(N),
    more_only_loop(N,S,L,L1,[S|Hist]).

/* end */