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

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

ex :- ex1(_).

ex(N) :- number(N),!,ex1(N).
ex(demo(N)) :- number(N),!,ex1(N).
ex(X) :- verbose,!,time(deve(X)),itl_statistics,diag,!.
ex(X) :- time(deve(X)),itl_statistics.

ex1(N) :- ex(N,P),nl,write(P),write('.'),nl,ex(P),fail.
ex1(_) :- told.

exex :- verbose(off),tell(ex),(
	ex(_,P),nl,write(P),write('.'),nl,ex(P),itl_statistics,fail;
	told
	).

% cputime(X):-statistics(runtime,[X1,_]),!,X is X1/1000.
% cputime(X):-X is cputime. % for cprolog
time(X):- r_cputime(T0),call(X),r_cputime(T1),
	T is T1-T0,
	nl,write(T),write(' sec.').

state :- listing(state/3),lising(state/4).

% diagnosis
diag :- diag(X),
	(X = counter_example(_), write('counter example:'),nl; true),!,
	write_diag(X).

diag(X) :- number(X),   % at most X length solution
	links(false,_),    % search false
	diag_l(false,[],H,X),
	make_hist(H,Hist),
	write_diag(counter_example(Hist)).
diag(valid) :- \+(links(false,_)),!.
diag(counter_example(Hist)) :-
	diag_l(false,[],H,0),
	make_hist(H,Hist).

% execution exapmle.
exe :- exe(Z),
	(Z=unsatisfiable, nl,write('unsatisfiable'),nl,!,fail; 
	nl,write('execution:'),nl,write_diag(Z)).

exe(X) :- number(X),   % at most X length solution
	possible_root(R),
	diag_l(R,[],H,X),
	make_hist(H,Hist),
	write_diag(execution(Hist)).
exe(unsatisfiable) :- \+(possible_root(_)),!.
exe(execution(Hist)) :-
	possible_root(R),
	diag_l(R,[],H,0),
	make_hist(H,Hist).

% possible root is non looping true or 0 node.
possible_root(true) :-
	possible_root1(true).
possible_root(0) :-
	possible_root1(0).

possible_root1(R) :- links(R,N),\+(N = true),!.

% Log order search

make_hist(S,C) :- detailed,!,
	S = [P|L],itl_state(P1,P),
	make_hist1(L,P,P1,[],_,C).
make_hist(S,C) :- 
	S = [P|L],
	make_hist0(L,P,C).

make_hist0([],_,[]):-!.
make_hist0([D|L],*,[*|L1]):-!, 
	make_hist0(L,D,L1).
make_hist0([*|L],S,[*|L1]):-!, 
	make_hist0(L,S,L1).
make_hist0([D|L],S,[(D->Cond)|L1]):-!,  % step by step
	state(S,Cond,D),
	!,  				% 
	make_hist0(L,D,L1).

% trace 2variable renamings

make_hist1([],_,_,R,R,[]):-!.
make_hist1([*|L],S,P,R,R1,[*|L1]):-!,  
	make_hist1(L,S,P,R,R1,L1).
make_hist1([SN|L],S,P,R,R1,[(SN->Cond)|L1]):-!,  % step by step
	state(S,Cond,SN,P,P1,R,R0),
	!,
	make_hist1(L,SN,P1,R0,R1,L1).


diag(Hist,P) :-
	diag_l(P,[],Hist,0).

% try to find interesting example
% reverse order back track
diag_ls(Ps,L,L1,D):-member(P,Ps),diag_l(P,L,L1,D).

% one minimum solution
diag_l(1,L,[1|L],D):-!,D=<0.    % Initial State? Enough depth?
diag_l(E,L,L1,D) :-
	setof(P,links(E,P),P1),  % must be minimum first order
	D1 is D-1,
	member(P0,P1),
	diag_l(P0,[E|L],L1,D1).


write_diag(counter_example(Hist)) :-!,write_ce(Hist,0).
write_diag(execution(Hist)) :-!,write_ce(Hist,0).
	write_ce([],_):-!.
	write_ce([(*)|T],I) :- !,
	    write(*),nl,
	    write_ce(T,I).
	write_ce([(S->[E|L])|T],I) :- (E=more,L=L1;E=empty,L=L1;[E|L]=L1),!,
		write(I),write(:),write_cond(L1),put(9),write(S),nl,
		J is I+1,
		write_ce(T,J).
write_diag(R):-!,write(R),nl.

% condition print

write_cond(X) :- sortC(X,Y),write_cond1(Y).
write_cond1([]):-!.
write_cond1([H|T]):-!,write_cond1(H),write_cond1(T).
write_cond1(not(P)):-!,put(45),  % "-"
	write(P).
write_cond1(P):-     !,put(43),  % "+"
	write(P).

% bubble sort
sortC([],[]).
sortC([H|T],[Min|Y]):-
    min(T,H,Min,Rest),
    sortC(Rest,Y).

min([],X,X,[]).
min([H|T],X,Y,[H|S]) :- ord(H,X),!,min(T,X,Y,S).
min([H|T],X,Y,[X|S]) :- min(T,H,Y,S).

ord(not(X),not(Y)) :- !,X @> Y.
ord(X,not(Y))  :- !,X @> Y.
ord(not(X),Y)  :- !,X @> Y.
ord(X,Y)   :- !,X @> Y.

rev([],X,X).
rev([H|T],X,Y) :- rev(T,[H|X],Y).

member(H,[H|_]).
member(H,[_|T]):-member(H,T).

not_member(_,[]):-!.
not_member(H,[H|_]):-!,fail.
not_member(H,[_|T]):-not_member(H,T).

count(A) :- count(A,X),write(X),nl.
count(A, _) :-
        init_var(tmp, 0),
        call(A),
        inc_var(tmp, _),
        fail.
count(_, A) :-
	retract(tmp(A)).

user_help :- write('?-ex(2).'),nl,
write('?-ex( [](p) -> <> p ).'),nl,
write('    Verify numbered examples or ITL formula.'),nl,
write('?-diag.'),nl,
write('    shows a counter example.'),nl,
write('?-exe.'),nl,
write('    This shows an execution of ITL formula.'),nl,
write('?-diag(N) or ?-exe(N) '),nl,
write('    shows at least N length examples.  '),nl,
write('         1: +p-q   means "at clock 1, p is true and q is false". '),nl,
write('?-verbose(off). '),nl,
write('    generates one character per state transition condition.'),nl,
write('     e   empty / t   true / f   false'),nl,
write('     123. newly genrated state number'),nl,
write('     .   transition to a registerd state'),nl,
write('?-verbose(on).'),nl,
write('    show ITL formula for each state. (Can be Very large)'),nl,
write('?-start, display.'),nl,
write('    starts X-Window Interface.'),nl,
write('?-ex. runs all examples in diag.pl. But it takes several hours.'),nl,
write('      Some of the examples are quite large.'),nl,
write('?-kiss.'),nl,
write('    generates KISS2 format for SIS.'),nl,
write('?-tgen.'),nl,
write('    generates Tokio language.'),nl,
write('?-read_kiss(File,In,Out,Empty).'),nl,
write('    reads KISS2 format. In and Out are list of variables in the order'),nl,
write('    of the KISS2 file. '),nl,
write('?-read_kiss(File).'),nl,
write('    =>  read_kiss(File,_,_,empty)'),nl,
write('?-read_kiss(File,Empty).'),nl,
write('    =>  read_kiss(File,_,_,Empty) '),nl,
true.

/* end */