%
% 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.
%
% Please, send your comments to kono@csl.sony.co.jp
% $Id$
%
% Display Interface for ITL Verifier
%    Using SICStus Prolog's Graphic Manager ( InterViews Package)
%

:- use_module(library(gmlib)).

:-dynamic font/2.

small :- (retract(font(_,_));true),assert(font("7x14",14)).
large :- (retract(font(_,_));true),assert(font("12x24",24)).

:-small.
% font("7x14",14).

width(W,H):-
   font(_,Fs),
   W is integer(1000/24*Fs), H is integer(500/24*Fs).

display:-
   tell(tmp),told,see(tmp),seen,
   font(Font,_),width(W,H),
   View <= view(W,H),
   View=>setfont(Font),
   In <= input("",Font),In => enable,
   Execute <= button("Execute",exe,font(Font)),Execute=>disable,
   Counter <= button("Counter Example",diag,font(Font)), Counter=>disable,
   Map     <= button("Map",map,font(Font)), Map=>disable,
   ST      <= output("State: Edge:",Font),
   K <= window("ITL Verifier",vbox([scroller(View),
	    space(
	    hbox([output("Enter temporal logic formula:",Font),space,ST])),
	    space(frame(In)),
	    border,
	    space(
	    hbox([space,
		  button("Verify",verify,font(Font)),
		  space,Execute, space,Counter, space,
		  vbox([
		  button("Verbose on",verbose(on),
		    [style(radio),font(Font)]),
		  button("        off",verbose(off),
		    [style(radio),font(Font)])
		  ]),
		  Map,
		  space,
		  button("Quit",quit,font(Font)),
		  space]))
	    ])),
     verbose(off),
   _ <= buttonstate(verbose(_),off),
   K => open,
   handle(In,View,K,[Execute,Counter,Map,ST]).

handle(In,View,K,N):-
   K => waitevent(E),
   handle(E,In,View,K,N).
handle(E,In,View,K,N):-
   (E=button(_,verify);E=menu(_,verify);E=return(_,_)) ->
	handle_verify(In,View,K,N), !,handle(In,View,K,N)
	;
   E=button(_,map) -> 
        clear_event(K), View=>update, width(_,H),
        view_state(View,H),!,handle(In,View,K,N)
	;
   E=button(_,exe) ->
	[Mb,Eb|_]=N, (Mb=>enable,Eb=>enable,
	display_exe(View),
	K=>waitevent(E1), handle_more(E1,In,View,K,N,exe),!;
	Mb=>disable,Eb=>enable,
	!, handle(In,View,K,N))
	;
   E=button(_,diag) ->
	[Mb,Eb|_]=N, (Mb=>enable,Eb=>enable,
	display_diag(View),
	K=>waitevent(E1),handle_more(E1,In,View,K,N,diag),!;
	Mb=>enable,Eb=>disable,
	!, handle(In,View,K,N))
	;
   E=button(_,verbose(on)) -> verbose(on),!, handle(In,View,K,N)
	;
   E=button(_,verbose(off)) -> verbose(off),!, handle(In,View,K,N)
	;
   E=button(_,noevent) ->!, handle(In,View,K,N) 
	;
   K => close.           % all end

clear_event(W) :- repeat,W=>nextevent(E),E=noevent.

handle_verify(In,_,_,N) :-
	[Mb,Eb,Map,ST|_]=N,Mb=>disable,Eb=>disable,Map=>disable,
	In => in(Text),s2term(Text,Term),
	command(Term,Term1),!,
	t2string(Term1,Text0), In => out(Text0),
	(Term1=prolog(_); ex(Term1)),!,
	Mb=>enable,Eb=>enable,Map=>enable,
	(verbose ; display_statistics(ST)),!.

display_statistics(ST) :-
	itl_state_number(S), % number of state
        itl_transition(L),   % number of transition
        name(S,Ss),name(L,Ls),
        append("State: ",Ss,S0),append(S0," Edge:",S1),append(S1,Ls,S2),
        ST=>out(S2),!.

% 
handle_more(Ev,_,_,_,_,E) :-
   Ev=button(_,E),
   !,fail.        % find another solution
handle_more(Ev,In,View,K,N,_) :-
   Ev=button(_,Label),button_event(Label),!,
   handle(Ev,In,View,K,N).
handle_more(Ev,In,View,K,N,_) :-
   Ev=return(_,_),!,
   handle(Ev,In,View,K,N).
handle_more(_,In,View,K,N,E) :-!,
   View=>getevent(Ev),
   handle_more(Ev,In,View,K,N,E).

button_event(verify).
button_event(diag).
button_event(exe).
button_event(quit).
button_event(map).
button_event(verbose(on)).
button_event(verbose(off)).
%%---------------------------------------------------------------------
% display_diagnosis
display_diag(View) :- diag(X),
	write_display_diag(X,View).

% display_execution exapmle.
display_exe(View) :- exe(Z),
	write_display_diag(Z,View).

write_display_diag(counter_example(Hist),View) :-!,display_ce(Hist,View).
write_display_diag(execution(Hist),View) :-!,display_ce(Hist,View).
write_display_diag(R,View):-!,
	atomic(R),name(R,Text),
	View=>clear,View=>string(0,0,Text).

display_ce(Hist,View) :-
	font(_,Fs),
	View=>clear,  % View=>batchmode,
        View=>setpattern(4),
	X is Fs/2,Y=0,W is integer(60/24*Fs),H is integer(60/24*Fs),
	(variable_list(L);L=[]),append(L,['Time'],L1),!,
	display_var(['State'|L1],View,X,Y,H,X,X1),
	X2 is X1+X,
	display_ce(Hist,L,View,X2,Y,W,H,0). % ,View=>batchmodeoff.
display_var([],_,_,_,_,X,X):-!.
display_var([Var|L],View,X,Y,H,X1,X2):-
	Y1 is Y+H,
	name(Var,VarText),
	View=>stringlength(VarText,Len),
	(X1>X+Len,X3=X1;X3 is X+Len),!,
	View=>string(X,Y,VarText),
	display_var(L,View,X,Y1,H,X3,X2).

display_ce([],_,_,_,_,_,_,_):-!.
display_ce([(S->[_|Cond])|Hist],L,View,X,Y,W,H,T) :-
	X1 is X+W,Y1 is Y+H,T1 is T+1,
	name(S,SText),View=>string(X1,Y,SText),
	display_now(L,Cond,View,X1,Y1,W,H,T),
	display_ce(Hist,L,View,X1,Y,W,H,T1).

display_now([],_,View,X,Y,_,_,T):-!,
	name(T,SText),View=>string(X,Y,SText).
display_now([V|Vr],Cond,View,X,Y,W,H,T):-
	display_state(Cond,V,View,X,Y,W,H),
	Y1 is Y+H,
	display_now(Vr,Cond,View,X,Y1,W,H,T).

display_state([V|_],V,View,X,Y,W,H) :-!, % true
	X2 is X+W,Y2 is Y+H,
	View=>fillrect(X,Y,X2,Y2).
display_state([not(V)|_],V,View,X,Y,W,H) :-!, % false
	X2 is X+W,Y2 is Y+H,
	View=>rect(X,Y,X2,Y2).
display_state([_|T],V,View,X,Y,W,H) :-!,
	display_state(T,V,View,X,Y,W,H).
display_state([],_,View,X,Y,W,H) :-!,    % unknown
	X2 is X+W,Y2 is Y+H/2,Y3 is Y2+3,
	View=>rect(X,Y2,X2,Y3).

s2term("",true):-!.
s2term(Text,Term) :-
	telling(O),
	tell(tmp),format("~s.~n",[Text]),told,tell(O),
	seeing(I),
	see(tmp),on_exception(Er,read(Term),read_error(Term,Er,I,O)),
	see(tmp),seen,see(I),!.
s2term(_,true):-tell(tmp),told,see(tmp),seen.

read_error(true,Er,I,O) :- 
	tell(tmp),told,see(tmp),seen,
	see(I),tell(O),unix(system('rm tmp')),
	write('read error:'),write(Er),nl.

t2string(Term,Text) :-
	telling(O),
	tell(tmp),write(Term),told,tell(O),
	seeing(I),
	see(tmp),get0(C),read_string(C,Text),see(tmp),seen,see(I),!.
t2string(_,true):-tell(tmp),told,see(tmp),seen.

read_string(-1,[]) :- !.
read_string(C,[C|T]) :- 
	get0(C1),read_string(C1,T).


command(demo(X),Term):-!,demo(X,Term).   % predefined examples
command(ex(X),Term):-!,ex(X,Term).
command(prolog(X,P),X):-!,call(P).
command(prolog(P),prolog(P)):-!,call(P).
command(X,X).

view_state :-
   make_state_view(View,W,K),
   view_state(View,W),View=>enable,
   repeat,
       K=>waitevent(E),E=down(_,_,_,_),K=>close.

make_state_view(View,W,K) :-
   width(W,_),font(Font,_),
   View <= view(W,W),
   View=>setfont(Font),
   K <= window("State Pattern",vbox([scroller(View) ])),
   K => open.

view_state(View,W) :-
   View=>setpattern(0),
   itl_state_number(S),
   View=>clear,View=>disable,View=>update, % View=>batchmode,
   View=>string(0,W,"T"),                  % This prevents core dump
   D0 is integer(W/(S+1)),(D0=0,D=1;D=D0),!,
   view_state_write(View,W,S,D).
view_state_write(View,W,S,D) :- 
   links(X,Y), link_translate(X,Y,X1,Y1,W,S),
%   View=>fillcircle(X1,Y1,2),fail.
%   View=>circle(X1,Y1,2),
    X2 is X1+D,Y2 is Y1+D,View=>fillrect(X1,Y1,X2,Y2),
    View=>update,
    fail.
view_state_write(_View,_,_,_):-true. % View=>batchmodeoff.

link_translate(false,Y,X1,Y1,W,S) :- !,
    link_translate(S,Y,X1,Y1,W,S).
link_translate(X,false,X1,Y1,W,S) :- !,
    link_translate(X,S,X1,Y1,W,S).
link_translate(X,Y,X1,Y1,W,S) :- number(X),number(Y),!,
    X1 is integer(X*W/(S+1))+1, Y1 is integer(Y*W/(S+1)).
link_translate(X,_,X1,0,W,S) :- number(X),!,
    X1 is integer(X*W/(S+1)).
link_translate(_,Y,0,Y1,W,S) :- number(Y),!,
    Y1 is integer(Y*W/(S+1)).
link_translate(_,_,0,0,_,_).

%%