/*
 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 `more' 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) :-
    insert_loop_mark(L,L1),
    make_hist(L1,L2),
    write_ce(L2,0),nl.

insert_loop_mark(L,L1) :-
    last(L,Last),
    insert_loop_mark(L,Last,L1).

last([Last],Last) :-!.
last([_|T],Last) :-
    last(T,Last).

insert_loop_mark([Last|T],Last,[(*),Last|T]):-!.
insert_loop_mark([H|T],Last,[H|T1]):-
    insert_loop_mark(T,Last,T1).

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

infinite(L) :-
    % 1 seems like original ITL formula that is root.
    setof(S,links(S,1),Children),
    more_node(1,Children,L,[],[1]).
infinite([]) :-
    found_infinite.

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

%infinite_node(true) :- !.
%infinite_node(S) :- 
%    number(S),
%    state(S,[more|_],_).

more_node(S,[S1|Children],[S|L],L1,Hist) :-
%    write('checking '),write(S),nl,
    infinite_node(S),
    % starting false loop
    more_loop(S1,Children,L,L1,[S|Hist],[S]).
more_node(S,Children,L,L1,Hist) :- 
    % goto one depth deeper
    more_node1(Children,L,L1,[S|Hist]).

more_node1([H|_],L,L1,Hist) :-
    not_member(H,Hist),
    setof(S,links(S,H),Children),
    more_node(H,Children,L,L1,Hist).
more_node1([_|T],L,L1,Hist) :-
    more_node1(T,L,L1,Hist).

more_loop(true,_,[true|L],L,_Hist,_Seq) :-
    assert(found_infinite).
more_loop(S,_,[S|L],L,_Hist,Seq) :-
    member(S,Seq),!,
    assert(found_infinite).
    % we find the one
more_loop(S,_,L,L,Hist,_Seq) :-
    member(S,Hist),!,
    fail.	
    % end of this branch
more_loop(H,_,[H|L],L1,Hist,Seq) :-
    infinite_node(H),!,		
    % still in the false interval
    setof(S,links(S,H),Children),
    more_loop1(Children,L,L1,[H|Hist],[H|Seq]).
more_loop(_,[S|T],L,L1,Hist,Seq) :-!,
    % try another child
    more_loop(S,T,L,L1,Hist,Seq).
% more_loop(H,[],L,L1,Hist,Seq) :-!,fail.
    % empty case. fail and try another branch


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

/* end */