/*
 Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc.
                                  The University, Newcastle upton Tyne

 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@csl.sony.co.jp
 $Id: dvcomp.pl,v 1.4 2007/08/30 05:16:36 kono Exp $
*/

% itl decomposition for DST

:- dynamic length_limit/1,renaming/0.

% requires [chop]
% itl(Predicate,Next,Empty,ConditionLists)

itl(P) :- expand(P,P0),
	moref(Ev),itl(P0,Next,Ev,[],C),
	write(([Ev|C]->Next)),nl,fail.
itl(_).
itl(P,Next,[Ev|C]) :- moref(Ev),itl(P,Next,Ev,[],C).

moref(empty).
moref(more).

% :- table itl/5.

itl(N,F,E,C,C1):-number(N),!,
	sb(Subterm,N),!,itl(Subterm,F,E,C,C1).
itl(true,true,_,C,C):-!.
itl(false,false,_,C,C):-!.
itl(true_false,true_false,more,C,C):-!.
itl(true_false,true,empty,C,[choice(true)|C]).
itl(true_false,false,E,C,[choice(false)|C]):-!,E=empty.
itl(more,false,empty,C,C).
itl(more,true,E,C,C):-!,E = more.
% next two rule determines descrete time
itl(empty,true,empty,C,C).      
itl(empty,false,E,C,C):-!,E = more.  % no succeeding more interval
itl(P,FF,_,C,C1) :- atomic(P),!, local(FF,P,C,C1).
itl(@(P),P,more,C,C).		   % strong next
itl(@(_),false,E,C,C):-!,E=empty.

itl(?(Cond,T,F),N,E,C,C1):-!,
	itl(Cond,CN,E,C,C0),itl_cond(CN,T,F,N,E,C0,C1).
% Non deterministic selection (singleton 2nd order variable)
itl([],true,_,C,C):-!.
itl([H|L],F,empty,C,C1):-!,
	empty_choice([H|L],0,F,C,C1).
itl([H|L],F,E,C,C1):-!,E=more,
	choice([H|L],F,C,C1).
% Regular Variable
itl(^(R),F,empty,C,C1):-
	local(F,^(R,0),C,C1).
itl(^(R),^(R,1),E,C,C):-!, E=more.

itl(^(R,S),F,empty,C,C1):-
	local(F,^(R,S),C,C1).
%itl(^(R,S),F,E,C,C1):- E = more,
%        length_limit(X),S>=X,inc_var(over,_),!,
%	S1 is S+1,local(F,over(R,S1),C,C1).    
itl(^(R,S),^(R,S1),E,C,C):-!, 
	% increment regular variable length
	E=more, S1 is S+1.

% Quantifier
itl(exists(P,Q),F,E,C,C0) :-!,
	itl(Q,QT,E,[P|C],C1),itl_ex(QT,Q,E,P,F,C1,C0).
itl(*(P),F,empty,C,C1):-!,itl(P,F,empty,C,C1).
itl(*(P),F,E,C,C1):-!,E=more,
	itl(P,PX,more,C,C1),
	closure(PX,P,F).
%% external state diagram
itl(st(N),F,E,C,C1):-!,
        setof((Cond=>X),st(N,Cond,X),L),itl_transition(L,F,E,C,C1).
%% ignore last state to check non stop predicate
itl(non_terminate(_),F,empty,C,C):-!,F=true.
itl(non_terminate(L),F,more,C,C1):-!,
    itl(L,F,more,C,C1).
%% shared resources or state
itl(share(L),F,empty,C,C1):-!,
	exclusive(L,C,C1,true,F).
itl(share(L),F,more,C,C1):-!,
	exclusive(L,C,C1,share(L),F).
%%
itl((P,Q),N,E,C,C1) :-!,
	itl(P,PN,E,C,C0),itland(PN,Q,N,E,C0,C1).
itl((P;Q),N,E,C,C1) :-!,
	itl(P,PN,E,C,C0),itlor(PN,Q,N,E,C0,C1).
itl(not(P),NN,E,X,X1) :- !,
	itl(P,N,E,X,X1),
	negate(N,NN).				%% negate/2 in chop.pl
% F = empty?(P,Q):(empty(P)*more(Q)+more(PM)&Q)
itl((P&Q),F,empty,C,C1) :-!,
	itl((P,Q),F,empty,C,C1).
itl((P&Q),F,more,C,C2) :-!,
	itl(P,PE,empty,C,C0),
	itl(P,PM,more,C0,C1),
	chop(PM,PE,F,Q,C1,C2).
itl(proj(_,Q),F,empty,C,C1) :-!,
	itl(Q,F,empty,C,C1).
itl(proj(P,Q),F,more,C,C1) :-!,
	itl(P,PM,more,C,C0),
	itl(Q,QM,more,C0,C1),
	prj(PM,QM,P,F).
% prefix is not consistently defined
% prefix(fin(false)) = true ? funny...
itl(prefix(P),F,empty,C,C1) :-!,
	itl(P,PE,empty,C,C0),
	itl(P,PM,more,C0,C1),
	prefix(PM,PE,F).
itl(prefix(P),F,more,C,C1) :-!,
	itl(P,PM,more,C,C1),
	prefix(PM,F).
itl(Def,_,_,_,_) :-
    write('error: '),write(Def),nl,!,fail.


local(true,P,C,C1):- true(C,P,C,C1).
local(false,P,C,C1):- false(C,P,C,C1).
true([],P,C,[P|C]):-!.
true([P|_],P,C,C):-!.
true([not(P)|_],P,_,_):-!,fail.
true([_|T],P,C,C1):-true(T,P,C,C1).
false([],P,C,[not(P)|C]):-!.
false([P|_],P,_,_):-!,fail.
false([not(P)|_],P,C,C):-!.
false([_|T],P,C,C1):-false(T,P,C,C1).
empty_choice([H|_],N,F,C,[choice(N)|C1]) :-
    itl(H,F,empty,C,C1).
empty_choice([_|L],N,F,C,C1) :-
    N1 is N+1,
    empty_choice(L,N1,F,C,C1).
choice([],[],C,C) :-!.
choice([H|L],[H1|L1],C,C2) :-
    itl(H,H1,more,C,C1),
    choice(L,L1,C1,C2).
itl_cond(true,T,_,N,E,C,C1) :-!,
	itl(T,N,E,C,C1).
itl_cond(false,_,F,N,E,C,C1) :-!,
	itl(F,N,E,C,C1).
itl_cond(CN,T,F,N,E,C,C1) :-!,
	itl(T,TN,E,C,C0),
	itl(F,FN,E,C0,C1), negate(CN,NCN),
	and(TN,CN,N1),and(FN,NCN,N2), or(N1,N2,N).
itl_ex(true,_,_,P,true,C,C1):-!,remove_p(C,P,C1).
itl_ex(false,Q,E,P,F,C,C0):-  !,remove_p(C,P,C1),
    itl(Q,QF,E,[not(P)|C1],C2),remove_p(C2,P,C0), exists(QF,P,F).
itl_ex(QT,Q,E,P,F,C,C0):- remove_p(C,P,C1),
    itl(Q,QF,E,[not(P)|C1],C2), remove_p(C2,P,C0),
    or(QT,QF,TF),exists(TF,P,F).
% constant order optimzation for quantifier
exists(P,P,true):-!.
exists(P,_,P):-atomic(P),!.
exists(Q,P,exists(P,Q)).
remove_p([],_,[]):-!.
remove_p([not(P)|T],P,T):-!.
remove_p([P|T],P,T):-!.
remove_p([H|T],P,[H|T1]):-!,remove_p(T,P,T1).
closure(false,_,false):-!.
closure(PX,P,(PX & *(P))).              %% infinite clousre (strong)
%%    closure(PX,P,(PX & (*(P);empty))).    %% finite closure (weak)
itl_transition([],false,_,C,C):-!.
itl_transition([(Cond=>empty)|T],F,E,C,C1):-!,
    itl((empty,Cond),F0,E,C,C0),
    itl_transition(T,F1,E,C0,C1),or(F0,F1,F).
itl_transition([(Cond=>X)|T],F,E,C,C1):-
    itl((more,Cond),F0,E,C,C0),
    itl_transition1(F0,X,T,F,E,C0,C1).
itl_transition1(false,_,T,F,E,C,C1):-
    itl_transition(T,F,E,C,C1).
itl_transition1(true,X,T,(st(X);F),E,C,C1):-
    itl_transition(T,F,E,C,C1).
exclusive([],C,C,F,F):-!.
exclusive([A|L],C,C1,F,F1):-
    true(C,A,C,C0),exclusive1(L,C0,C1,F,F1).
exclusive([N|L],C,C1,F,F1):-
    false(C,N,C,C0), !,exclusive(L,C0,C1,F,F1).
%    exclusive(_,C,C,_,false).   % eliminate this brach
exclusive1([],C,C,F,F):-!.
exclusive1([H|L],C,C1,F,F1):-
    false(C,H,C,C0), !,exclusive1(L,C0,C1,F,F1).
%    exclusive1(_,C,C,_,false).
itland(false,_,false,_,C0,C0):-!.
itland(true,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1).
itland(PN,Q,N,E,C0,C1):-
	itl(Q,QN,E,C0,C1),and(PN,QN,N).		%% and/3 in chop.pl
itlor(true,_,true,_,C0,C0):-!.
itlor(false,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1).
itlor(PN,Q,N,E,C0,C1):-
	itl(Q,QN,E,C0,C1),or(PN,QN,N).		%% or/3 in chop.pl
chop(false,false,false,_,C,C):-!.
chop(PM,false,(PM & Q),Q,C,C):-!.
chop(PM,true,F,Q,C,C1):-!,
    itl(Q,QF,more,C,C1),
    chop1(PM,QF,Q,F).
chop(PM,PE,F,Q,C,C):-!,
	write('next empty conflict:'),write((PM,PE,F,Q,C)),nl,!,
	fail.

chop1(false,QF,_,QF):-!.
chop1(false,false,_,false):-!.
chop1(true,false,true,true):-!.
chop1(true,_,true,true):-!.
chop1(PM,false,Q,(PM&Q)):-!.
chop1(_,true,_,true):-!.
chop1(PM,QF,Q,(QF;(PM&Q))):-!.

prj(false,_,_,false):-!.
prj(_,false,_,false):-!.
prj(PM,QM,P,(PM&proj(P,QM))).


prefix(true,true):-!.
prefix(false,false):-!.
prefix(PM,prefix(PM)):-!.

prefix(true,_,true):-!.
prefix(_,true,true):-!.
prefix(false,false,false):-!.
prefix(_,false,true):-!.


% develop Local ITL formula into state diagram
%
% Mon May 20 17:24:23 BST 1991
% require([chop]).

:-dynamic verbose/0,state/2,links/2.
:-dynamic stay/3,lazy/0,singleton/0,detailed/0.

verbose(off) :- retract(verbose),fail;true.
verbose(on) :- asserta(verbose).
:-verbose(on).

lazy(off) :- retract(lazy),fail;true.
lazy(on) :- asserta(lazy).

:-lazy(on).

singleton(off) :- retract(singleton),fail;true.
singleton(on) :- asserta(singleton).
:-singleton(on).

renaming(off) :- retract(renaming),fail;true.
renaming(on) :- asserta(renaming).
:-renaming(on).

detail(off) :- retract(detailed),fail;true.
detail(on) :- asserta(detailed).
% :-detail(on).

set_limit(X) :-
    set_var(length_limit,X,_).
no_limit :-
    retract(length_limit),fail.
no_limit.

:-assert(length_limit(5)).

deve(ITL) :-
	init,!,
	expand(ITL,ITL0),		% chop standard form
	itlstd(ITL0,StdNOW,_),		% BDT
	assert(itl_state(StdNOW,1)),!,  % Initial State
	deve0((1,StdNOW)).

deve0((S,ITL)) :-
        show_state(S,ITL),
	bagof(Next,itldecomp(ITL,Next,S),
	    Nexts),!,
	deve1(Nexts).
deve0(_).

deve1([]).
deve1([H|T]) :- deve0(H),deve1(T).

itldecomp(ITL,(NextS,StdNext),From) :-
	init_var(current,From),
	itl(ITL,Next,Cond),
	%% showing
	itlshow(Next,NextS,Cond,From,StdNext).

itlshow(Next,S,Cond,From,StdNext):-
	itlstd(Next,StdNext,Rename),
	check_state(StdNext,Cond,New,S),
	(verbose,!,write(Rename);true),
	(links(S,From),!;
             assertz(links(S,From)),inc_var(itl_transition_count,_)),
        inc_var(itl_transition,_),
	itlshow0(S,Cond,StdNext,New),
	!.

itlshow0(S,Cond,Next,New) :- verbose,!,
	itlshow1(S,Cond,Next,New),nl,!,New=1.
itlshow0(0,_,_,0):- !,put(101),!,fail.   % "e"
itlshow0(false,_,_,0):- !,put(102),!,fail.  % "f"
itlshow0(true,_,_,0):- !,put(116),!,fail. % "t"
itlshow0(_,_,_,0):- !,put(46),!,fail.    % "."
itlshow0(S,_,_,1):- !,write(S),put(46),ttyflush,!.

itlshow1(0,Cond,_,_):-!,
	write(Cond),write('->'),write(empty).  itlshow1(true,Cond,_,_):-!,
	write(Cond),write('->'),write(true).
itlshow1(false,Cond,_,_):-!,
	write(Cond),write('->'),write(false).
itlshow1(S,Cond,_,0):-!,
	write(Cond),write('->'),write(S).
itlshow1(S,Cond,Org,1):-
	write(Cond),write('->'),write(S),
	put(9),bdt2itl(Org,Org0),write(Org0),!.

% lazy transition condition generator

state(From,Cond,Next) :-
	links(Next,From),
	itl_state(ITL,From),
	itl(ITL,Next0,Cond),
	itlstd(Next0,StdNext,_),
	check_state(StdNext,Cond,_,Next1),  % Next1 has not to be instantiated
	Next1=Next.

% detailed state transition including 2var renamings

state(From,Cond,Next,FromFull,NextFull,Rename,Rename1) :-
        links(Next,From),
        itl(FromFull,PNext,Cond),
        itlstd(PNext,StdNext,NextFull,Rename,Rename1),
        check_state(StdNext,Cond,_,Next1),  % S1 has not to be instantiated
        Next = Next1.

init :-
	subterm_init,
        r_abolish(itl_state,2),
        r_abolish(stay,3),asserta(stay(0,0,0)),
        asserta(itl_state(false,false)),
        asserta(itl_state(empty,0)),
        asserta(itl_state(true,true)),
	r_abolish(links,2),asserta(links(true,true)),
        init_var(current,0),
        init_var(over,0),
        init_var(itl_transition,0),
        init_var(itl_transition_count,0),
	init_var(itl_state_number,1),!.

show_state(S,ITL) :-
	bdt2itl(ITL,ITL0),
	nl,write('state('),write(S),  % (
	(verbose,write(' , '), write(ITL0),write(')'),nl;write(')')),!.

check_state(true,[more |_],0,true):-!.
check_state(true,[empty|_],0,0):-!.
check_state(false,_,0,false):-!.
check_state(STD,_,0,S):-
	itl_state(STD,S),!.
check_state(STD,_,1,S):-
	inc_var(itl_state_number,S),
	assert(itl_state(STD,S)),!.

init_var(X,V) :- r_abolish(X,1),functor(F,X,1),arg(1,F,V),assert(F),!.
inc_var(Name,X1) :- 
        functor(F,Name,1),retract(F),arg(1,F,X),
        X1 is X+1,functor(F1,Name,1),arg(1,F1,X1),
        asserta(F1),!.
set_var(Name,X,X1) :-
        functor(F,Name,1),retract(F),!,arg(1,F,X),
	functor(F1,Name,1),arg(1,F1,X1),asserta(F1),!.
set_var(Name,X,_) :- init_var(Name,X).


itl_statistics :- nl,
        itl_state_number(X),write(X),write(' states'),nl,fail.
itl_statistics :- 
        sbn(X),write(X),write(' subterms'),nl,fail.
itl_statistics :- 
	itl_transition_count(X),
        write(X),write(' state transions'),nl,fail.
itl_statistics :- 
        over(X),X=\=0,write(X),write(' interval overflows'),nl,fail.
itl_statistics :- 
	verbose,write('verbose,'),fail.
itl_statistics :- 
	renaming,write('renaming,'),fail.
itl_statistics :- 
	singleton,write('singleton,'),fail.
itl_statistics :- 
	detailed,write('detailed,'),fail.
itl_statistics :- 
	length_limit(X),X=\=0,write('length limit '),write(X),nl,fail.
itl_statistics.

%% end %%