Mercurial > hg > Applications > Lite

comparison display.pl @ 19:e1d3145cff7a lite-verifier

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Thu, 30 Aug 2007 12:44:35 +0900
parents
children 29cf617f49db
comparison
equal deleted inserted replaced
18:a6adedccd5f6 19:e1d3145cff7a
1 %
2 % Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc.
3 % The University, Newcastle upton Tyne
4 %
5 % Everyone is permitted to copy and distribute verbatim copies
6 % of this license, but changing it is not allowed. You can also
7 % use this wording to make the terms for other programs.
8 %
9 % Please, send your comments to kono@csl.sony.co.jp
10 % $Id$
11 %
12 % Display Interface for ITL Verifier
13 % Using SICStus Prolog's Graphic Manager ( InterViews Package)
14 %
15
16 :- use_module(library(gmlib)).
17
18 :-dynamic font/2.
19
20 small :- (retract(font(_,_));true),assert(font("7x14",14)).
21 large :- (retract(font(_,_));true),assert(font("12x24",24)).
22
23 :-small.
24 % font("7x14",14).
25
26 width(W,H):-
27 font(_,Fs),
28 W is integer(1000/24*Fs), H is integer(500/24*Fs).
29
30 display:-
31 tell(tmp),told,see(tmp),seen,
32 font(Font,_),width(W,H),
33 View <= view(W,H),
34 View=>setfont(Font),
35 In <= input("",Font),In => enable,
36 Execute <= button("Execute",exe,font(Font)),Execute=>disable,
37 Counter <= button("Counter Example",diag,font(Font)), Counter=>disable,
38 Map <= button("Map",map,font(Font)), Map=>disable,
39 ST <= output("State: Edge:",Font),
40 K <= window("ITL Verifier",vbox([scroller(View),
41 space(
42 hbox([output("Enter temporal logic formula:",Font),space,ST])),
43 space(frame(In)),
44 border,
45 space(
46 hbox([space,
47 button("Verify",verify,font(Font)),
48 space,Execute, space,Counter, space,
49 vbox([
50 button("Verbose on",verbose(on),
51 [style(radio),font(Font)]),
52 button(" off",verbose(off),
53 [style(radio),font(Font)])
54 ]),
55 Map,
56 space,
57 button("Quit",quit,font(Font)),
58 space]))
59 ])),
60 verbose(off),
61 _ <= buttonstate(verbose(_),off),
62 K => open,
63 handle(In,View,K,[Execute,Counter,Map,ST]).
64
65 handle(In,View,K,N):-
66 K => waitevent(E),
67 handle(E,In,View,K,N).
68 handle(E,In,View,K,N):-
69 (E=button(_,verify);E=menu(_,verify);E=return(_,_)) ->
70 handle_verify(In,View,K,N), !,handle(In,View,K,N)
71 ;
72 E=button(_,map) ->
73 clear_event(K), View=>update, width(_,H),
74 view_state(View,H),!,handle(In,View,K,N)
75 ;
76 E=button(_,exe) ->
77 [Mb,Eb|_]=N, (Mb=>enable,Eb=>enable,
78 display_exe(View),
79 K=>waitevent(E1), handle_more(E1,In,View,K,N,exe),!;
80 Mb=>disable,Eb=>enable,
81 !, handle(In,View,K,N))
82 ;
83 E=button(_,diag) ->
84 [Mb,Eb|_]=N, (Mb=>enable,Eb=>enable,
85 display_diag(View),
86 K=>waitevent(E1),handle_more(E1,In,View,K,N,diag),!;
87 Mb=>enable,Eb=>disable,
88 !, handle(In,View,K,N))
89 ;
90 E=button(_,verbose(on)) -> verbose(on),!, handle(In,View,K,N)
91 ;
92 E=button(_,verbose(off)) -> verbose(off),!, handle(In,View,K,N)
93 ;
94 E=button(_,noevent) ->!, handle(In,View,K,N)
95 ;
96 K => close. % all end
97
98 clear_event(W) :- repeat,W=>nextevent(E),E=noevent.
99
100 handle_verify(In,_,_,N) :-
101 [Mb,Eb,Map,ST|_]=N,Mb=>disable,Eb=>disable,Map=>disable,
102 In => in(Text),s2term(Text,Term),
103 command(Term,Term1),!,
104 t2string(Term1,Text0), In => out(Text0),
105 (Term1=prolog(_); ex(Term1)),!,
106 Mb=>enable,Eb=>enable,Map=>enable,
107 (verbose ; display_statistics(ST)),!.
108
109 display_statistics(ST) :-
110 itl_state_number(S), % number of state
111 itl_transition(L), % number of transition
112 name(S,Ss),name(L,Ls),
113 append("State: ",Ss,S0),append(S0," Edge:",S1),append(S1,Ls,S2),
114 ST=>out(S2),!.
115
116 %
117 handle_more(Ev,_,_,_,_,E) :-
118 Ev=button(_,E),
119 !,fail. % find another solution
120 handle_more(Ev,In,View,K,N,_) :-
121 Ev=button(_,Label),button_event(Label),!,
122 handle(Ev,In,View,K,N).
123 handle_more(Ev,In,View,K,N,_) :-
124 Ev=return(_,_),!,
125 handle(Ev,In,View,K,N).
126 handle_more(_,In,View,K,N,E) :-!,
127 View=>getevent(Ev),
128 handle_more(Ev,In,View,K,N,E).
129
130 button_event(verify).
131 button_event(diag).
132 button_event(exe).
133 button_event(quit).
134 button_event(map).
135 button_event(verbose(on)).
136 button_event(verbose(off)).
137 %%---------------------------------------------------------------------
138 % display_diagnosis
139 display_diag(View) :- diag(X),
140 write_display_diag(X,View).
141
142 % display_execution exapmle.
143 display_exe(View) :- exe(Z),
144 write_display_diag(Z,View).
145
146 write_display_diag(counter_example(Hist),View) :-!,display_ce(Hist,View).
147 write_display_diag(execution(Hist),View) :-!,display_ce(Hist,View).
148 write_display_diag(R,View):-!,
149 atomic(R),name(R,Text),
150 View=>clear,View=>string(0,0,Text).
151
152 display_ce(Hist,View) :-
153 font(_,Fs),
154 View=>clear, % View=>batchmode,
155 View=>setpattern(4),
156 X is Fs/2,Y=0,W is integer(60/24*Fs),H is integer(60/24*Fs),
157 (variable_list(L);L=[]),append(L,['Time'],L1),!,
158 display_var(['State'|L1],View,X,Y,H,X,X1),
159 X2 is X1+X,
160 display_ce(Hist,L,View,X2,Y,W,H,0). % ,View=>batchmodeoff.
161 display_var([],_,_,_,_,X,X):-!.
162 display_var([Var|L],View,X,Y,H,X1,X2):-
163 Y1 is Y+H,
164 name(Var,VarText),
165 View=>stringlength(VarText,Len),
166 (X1>X+Len,X3=X1;X3 is X+Len),!,
167 View=>string(X,Y,VarText),
168 display_var(L,View,X,Y1,H,X3,X2).
169
170 display_ce([],_,_,_,_,_,_,_):-!.
171 display_ce([(S->[_|Cond])|Hist],L,View,X,Y,W,H,T) :-
172 X1 is X+W,Y1 is Y+H,T1 is T+1,
173 name(S,SText),View=>string(X1,Y,SText),
174 display_now(L,Cond,View,X1,Y1,W,H,T),
175 display_ce(Hist,L,View,X1,Y,W,H,T1).
176
177 display_now([],_,View,X,Y,_,_,T):-!,
178 name(T,SText),View=>string(X,Y,SText).
179 display_now([V|Vr],Cond,View,X,Y,W,H,T):-
180 display_state(Cond,V,View,X,Y,W,H),
181 Y1 is Y+H,
182 display_now(Vr,Cond,View,X,Y1,W,H,T).
183
184 display_state([V|_],V,View,X,Y,W,H) :-!, % true
185 X2 is X+W,Y2 is Y+H,
186 View=>fillrect(X,Y,X2,Y2).
187 display_state([not(V)|_],V,View,X,Y,W,H) :-!, % false
188 X2 is X+W,Y2 is Y+H,
189 View=>rect(X,Y,X2,Y2).
190 display_state([_|T],V,View,X,Y,W,H) :-!,
191 display_state(T,V,View,X,Y,W,H).
192 display_state([],_,View,X,Y,W,H) :-!, % unknown
193 X2 is X+W,Y2 is Y+H/2,Y3 is Y2+3,
194 View=>rect(X,Y2,X2,Y3).
195
196 s2term("",true):-!.
197 s2term(Text,Term) :-
198 telling(O),
199 tell(tmp),format("~s.~n",[Text]),told,tell(O),
200 seeing(I),
201 see(tmp),on_exception(Er,read(Term),read_error(Term,Er,I,O)),
202 see(tmp),seen,see(I),!.
203 s2term(_,true):-tell(tmp),told,see(tmp),seen.
204
205 read_error(true,Er,I,O) :-
206 tell(tmp),told,see(tmp),seen,
207 see(I),tell(O),unix(system('rm tmp')),
208 write('read error:'),write(Er),nl.
209
210 t2string(Term,Text) :-
211 telling(O),
212 tell(tmp),write(Term),told,tell(O),
213 seeing(I),
214 see(tmp),get0(C),read_string(C,Text),see(tmp),seen,see(I),!.
215 t2string(_,true):-tell(tmp),told,see(tmp),seen.
216
217 read_string(-1,[]) :- !.
218 read_string(C,[C|T]) :-
219 get0(C1),read_string(C1,T).
220
221
222 command(demo(X),Term):-!,demo(X,Term). % predefined examples
223 command(ex(X),Term):-!,ex(X,Term).
224 command(prolog(X,P),X):-!,call(P).
225 command(prolog(P),prolog(P)):-!,call(P).
226 command(X,X).
227
228 view_state :-
229 make_state_view(View,W,K),
230 view_state(View,W),View=>enable,
231 repeat,
232 K=>waitevent(E),E=down(_,_,_,_),K=>close.
233
234 make_state_view(View,W,K) :-
235 width(W,_),font(Font,_),
236 View <= view(W,W),
237 View=>setfont(Font),
238 K <= window("State Pattern",vbox([scroller(View) ])),
239 K => open.
240
241 view_state(View,W) :-
242 View=>setpattern(0),
243 itl_state_number(S),
244 View=>clear,View=>disable,View=>update, % View=>batchmode,
245 View=>string(0,W,"T"), % This prevents core dump
246 D0 is integer(W/(S+1)),(D0=0,D=1;D=D0),!,
247 view_state_write(View,W,S,D).
248 view_state_write(View,W,S,D) :-
249 links(X,Y), link_translate(X,Y,X1,Y1,W,S),
250 % View=>fillcircle(X1,Y1,2),fail.
251 % View=>circle(X1,Y1,2),
252 X2 is X1+D,Y2 is Y1+D,View=>fillrect(X1,Y1,X2,Y2),
253 View=>update,
254 fail.
255 view_state_write(_View,_,_,_):-true. % View=>batchmodeoff.
256
257 link_translate(false,Y,X1,Y1,W,S) :- !,
258 link_translate(S,Y,X1,Y1,W,S).
259 link_translate(X,false,X1,Y1,W,S) :- !,
260 link_translate(X,S,X1,Y1,W,S).
261 link_translate(X,Y,X1,Y1,W,S) :- number(X),number(Y),!,
262 X1 is integer(X*W/(S+1))+1, Y1 is integer(Y*W/(S+1)).
263 link_translate(X,_,X1,0,W,S) :- number(X),!,
264 X1 is integer(X*W/(S+1)).
265 link_translate(_,Y,0,Y1,W,S) :- number(Y),!,
266 Y1 is integer(Y*W/(S+1)).
267 link_translate(_,_,0,0,_,_).
268
269 %%