/*
 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:'),nl,
    write_infinite_seq1(L).
write_infinite_seq1([L]) :-!, % odd case.
    make_hist([L,L],L1),
    write_ce(L1,0),nl.
write_infinite_seq1(L) :-
    make_hist(L,L1),
    write_ce(L1,0),nl.

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

infinite(L) :-
    % 1 seems like original ITL formula that is root.
    setof(S,(links(S,1),integer(S)),Children),
    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) :-
%    write('checking '),write(S),nl,
    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) :-
    setof(S,(links(S,H),integer(S)),Children),
    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,_,[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
    setof(S,(links(S,H),integer(S)),Children),
    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
    setof(S,(links(S,H),integer(S)),Children),
    % we already know S i not more_only
    more_only_node1(Children,L,L1,[H|Hist]).

more_only_loop1([H|_],L,L1,Hist,Seq) :-
    setof(S,(links(S,H),integer(S)),Children),
    more_only_loop(H,Children,L,L1,Hist,Seq).
more_only_loop1([_|T],L,L1,Hist,Seq) :-
    more_only_loop1(T,L,L1,Hist,Seq).

/* end */