--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/display.pl	Thu Aug 30 12:44:35 2007 +0900
@@ -0,0 +1,269 @@
+%
+% 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,_,_).
+
+%%