/*
 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$
*/

% itl decomposition for DST

:- use_module('~/ITL/bdd/sicstus/bdd').

% 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).

itl(N,F,E,C,C1):-integer(N),!,
	bdd2itl1(N,Term),!,itl(Term,F,E,C,C1).
itl(true,true,_,C,C):-!.
itl(false,false,_,C,C):-!.
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).
    local(true,P,C,C1):- true(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).
    local(false,P,C,C1):- false(C,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).
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).
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).

% 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_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).
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).
    closure(false,_,false):-!.
    closure(PX,P,(PX & *(P))).              %% infinite clousre (strong)
%%    closure(PX,P,(PX & (*(P);empty))).    %% finite closure (weak)
%% 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).
    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).
%% 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).
    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).
%%
itl((P,Q),N,E,C,C1) :-!,
	itl(P,PN,E,C,C0),itland(PN,Q,N,E,C0,C1).
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
itl((P;Q),N,E,C,C1) :-!,
	itl(P,PN,E,C,C0),itlor(PN,Q,N,E,C0,C1).
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
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).

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(PM,false,Q,(PM&Q)):-!.
chop1(_,true,_,true):-!.
chop1(PM,QF,Q,(QF;(PM&Q))):-!.

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).
prj(false,_,_,false):-!.
prj(_,false,_,false):-!.
prj(PM,QM,P,(PM&proj(P,QM))).

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).

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

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

itl(Def,_,_,_,_) :-
    write('error: '),write(Def),nl,!,fail.

% 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.

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

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

% A \= A :-!,fail.
% _ \= _.

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

deve0((S,ITL)) :-
        show_state(S,ITL),
	setof(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):-
	itl2bdd(Next,StdNext),
	check_state(StdNext,Cond,New,S),
	(lazy,!;assertz(state(From,Cond,S))),
	(links(S,From),!;assertz(links(S,From))),
	!,
	itlshow0(S,Cond,StdNext,New).

itlshow0(S,Cond,Next,New) :- verbose,!,
	itlshow1(S,Cond,Next,New),nl,!,New=1.
itlshow0(0,_,_,0):- !,put("e"),!,fail.
itlshow0(false,_,_,0):- !,put("f"),!,fail.
itlshow0(true,_,_,0):- !,put("t"),!,fail.
itlshow0(_,_,_,0):- !,put("."),!,fail.
itlshow0(S,_,_,1):- !,write(S),put("."),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),
	bdd2itl(Org,S1),put(9),write(S1),!.

lazy_state(From,Cond,S) :-
	links(S,From),
	itl_state(ITL,From),
	itl(ITL,Next,Cond),
	itl2bdd(Next,StdNext),
	check_state(StdNext,Cond,_,S).

init :-
	subterm_init,
	abolish(state,3),
	asserta((state(true,[more],true):-!)),
	asserta((state(true,[empty],0):-!)),
	(lazy,assertz((state(A,B,C) :- lazy_state(A,B,C))),!;true),
        abolish(itl_state,2),
        abolish(stay,3),asserta(stay(0,0,0)),
	bdd:zero(F), bdd:one(T),
        asserta(itl_state(F,false)),
        asserta(itl_state(empty,0)),
        asserta(itl_state(T,true)),
	abolish(links,2),asserta(links(true,true)),
	init_var(itl_state_number,1),!.

show_state(S,ITL) :-
	bdd2itl(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,-2):-!.
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,_) :- functor(F,X,1),assert(F),fail.
init_var(X,_) :- functor(F,X,1),retract(F),fail.
init_var(X,V) :- 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),!.

increment_state(stay(P,now),stay(P,S),S) :- !,
      (stay(P,F,S);assertz(stay(P,F,S))),!.
increment_state(N,N,_) :- atomic(N),!.
increment_state(P,R,S) :- functor(P,H,N),functor(R,H,N),
      increment_state_arg(N,P,R,S).
increment_state_arg(0,_P,_R,_):-!.
increment_state_arg(N,P,R,S):-arg(N,P,PA),arg(N,R,RA),
      N1 is N-1,increment_state(PA,RA,S),
      increment_state_arg(N1,P,R,S).

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 :- 
        init_var(tmp,0),
        ((links(_,_),inc_var(tmp,_),fail);true),
        tmp(N),
        write(N),write(' state transitions'),nl,fail.
itl_statistics.

%% end %%