Mercurial > hg > Applications > Lite

comparison disp.pl @ 2:1c57a78f1d98

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial revision
author kono
date Thu, 18 Jan 2001 23:27:24 +0900
parents
children e1d3145cff7a
comparison
equal deleted inserted replaced
1:683efd6f9a81 2:1c57a78f1d98
1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2 %%
3 %% LITE Tcl/Tk interface
4 %%
5 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6
7 % :- ensure_loaded('../tableau/lite').
8 :- module(lite).
9 :- use_module(library(tcltk)).
10 :- verbose(off).
11
12 :- dynamic r_event/2.
13
14 :- abolish(show_state,2).
15 % Next command keep check event during verification
16 show_state(S,ITL) :-!,
17 (tcl_eval(update);true),!,
18 bdt2itl(ITL,ITL1),
19 nl,write('state('),write(S), % (
20 (verbose,write(' , '), write(ITL1),write(')'),nl;write(')')),!.
21
22 event(verbose,'1') :- verbose(on).
23 event(verbose,'0') :- verbose(off).
24 event(X,Y) :- assertz(r_event(X,Y)). % ,write((X,Y)),nl.
25 event(X) :- assertz(r_event(X,[])). % ,write((X)),nl.
26
27 next(X,Y) :- r_event(_,_),retract(r_event(X,Y)),!.
28 next(X,Y) :- tk_do_one_event(0),!,
29 next(X,Y).
30
31 display :-
32 init_display,!,
33 event_loop(run).
34
35 init_display :-
36 (retract(r_event(_,_)),fail;true),
37 tk_init('lite',[]),
38 % tcl_eval('source disp.tcl'),
39 tcl_eval('source xf-disp'),
40 all_disable.
41 canvas_origin(20,20).
42
43 event_loop(quit):-!.
44 event_loop(_) :-
45 next(X,Y),execute(X,Y),!,event_loop(X).
46
47 execute(verify,X) :- !,
48 verify(X).
49
50 % !,X=1 -> verbose(on); verbose(off). causes error
51 execute(verbose,X) :- X='1' -> verbose(on); verbose(off).
52 execute(map,X) :- !,name(X,L),name(X1,L),view_state(a,X1).
53 execute(execute,_) :- !,do_execute,!.
54 execute(generate,_) :- !,
55 generate.
56 execute(counter,_) :- !,do_diagnosis,!.
57 execute(quit,_) :- !. % ,tcl_eval('destroy .').
58 execute(prolog_call,X) :- !,prolog_call(X).
59 execute(tokio_call,X) :- !,tokio_call(X).
60 execute(X,_) :- !,write(event(X)),nl,ttyflush.
61
62 generate :-
63 TOKIO = 'tmp.tokio',
64 tell(TOKIO),tgen,told,
65 user:com(TOKIO,'tmp.out').
66 gen(X) :- consult(X),specification(Y),ex(Y),generate.
67 gen(X) :-
68 name(X,XL),append(XL,".lite",YL),name(X1,YL),
69 consult(X1),specification(Y),ex(Y),generate.
70
71 verify(X) :-
72 all_disable,
73 abolish(st,3),abolish(specification,1),abolish(st_variables,2),
74 t2string(X,X0),s2terms(X0,X1),command(X1,X2,X3),
75 display_contents(X3),
76 ex(X2),!,
77 ttyflush, display_statistics,
78 all_enable.
79 verify(_) :-
80 all_disable.
81 display_contents(X) :-
82 ttyflush,t2strings(X,XS0),easy_pp(XS0,XS),
83 tcl_eval('$symbolicName(entry) delete 0.0 end'),
84 tcl_eval(['$symbolicName(entry) insert 0.0 {',XS,'}']),
85 display_update.
86
87 all_disable :-
88 tcl_eval('$symbolicName(map) configure -state disabled'),
89 tcl_eval('$symbolicName(execute) configure -state disabled'),
90 tcl_eval('$symbolicName(diag) configure -state disabled'),
91 display_update.
92 all_enable :-
93 tcl_eval('$symbolicName(map) configure -state normal'),
94 tcl_eval('$symbolicName(execute) configure -state normal'),
95 tcl_eval('$symbolicName(diag) configure -state normal'),
96 display_update.
97
98 % Backtrack Control of example/counter example
99
100 do_execute :- display_exe('.'),next(X,Y),do_execute(X,Y),!.
101 do_execute.
102
103 do_execute(execute,_) :-!,
104 fail.
105 do_execute(X,Y) :- execute(X,Y),!.
106
107 do_diagnosis :- display_diag(','),next(X,Y),do_diagnosis(X,Y),!.
108 do_diagnosis.
109
110 do_diagnosis(diag,_) :-!,
111 fail.
112 do_diagnosis(X,Y) :- execute(X,Y),!.
113
114 % :- dynamic specification/1.
115
116 % Text Based Commnad
117
118 command([st(X,Y,Z)|T],Term,[st(X,Y,Z)|T1]):-!,
119 assertz(st(X,Y,Z)),!,
120 command(T,Term,T1).
121 command([specification(X)|T],X,[specification(X)|T1]):-!,
122 command(T,X,T1).
123 command([st_variables(X,Y)|T],Term,[st_variables(X,Y)|T1]):-!,
124 assertz(st_variables(X,Y)),
125 command(T,Term,T1).
126 command([],true,[]) :-!.
127 command([],_,[]) :-!.
128 command([H],Term,[Term1]) :-!,
129 command(H,Term),!,Term=Term1.
130 command([H|T],(Term1,Terms),[Term1|T1]) :-
131 command(H,Term1),!,command(T,Terms,T1).
132
133 command(demo(X),Term):-!,lite:demo(X,Term). % predefined examples
134 command(ex(X),Term):-!,ex(X,Term).
135 command(prolog(X,P),X):-!,safe_call(P).
136 command(prolog(P),true):-!,safe_call(P).
137 command(tokio(P),true):-!,safe_call(tokio(P)).
138 command(consult(P),Term):-!,
139 command(file(P),Term).
140 command(file(P),Term):-
141 on_exception(Er,(consult(P),specification(Term)),
142 read_error(Term,Er,user,user)).
143 command(A,A) :- atomic(A),!.
144 command(P,R) :- functor(P,H,N),functor(R,H,N),
145 command_arg(N,P,R).
146 command_arg(0,_P,_R):-!.
147 command_arg(N,P,R):-arg(N,P,PA),arg(N,R,RA),
148 N1 is N-1,command(PA,RA),command_arg(N1,P,R).
149
150 prolog_call(X) :-
151 t2string(X,X0),s2terms(X0,[X1|_]),safe_call(X1).
152 tokio_call(X) :-
153 t2string(X,X0),s2terms(X0,[X1|_]),safe_call(tokio(X1)).
154
155 safe_call(X) :-
156 on_exception(Er,user:call(X),
157 read_error(X,Er,user,user)),!.
158 safe_call(_).
159
160 :-dynamic font/2.
161
162 small :- (retract(font(_,_));true),assert(font("7x14",14)).
163 large :- (retract(font(_,_));true),assert(font("12x24",24)).
164
165 :-small.
166 % font("7x14",14).
167
168 width(W,H):-
169 font(_,Fs),
170 W is integer(1000/24*Fs), H is integer(500/24*Fs).
171
172 display_statistics :-
173 itl_state_number(S), % number of state
174 itl_transition(L), % number of transition
175 name(S,Ss),name(L,Ls),
176 append("State: ",Ss,S0),append(S0," Edge:",S1),append(S1,Ls,S2),
177 tcl_eval(["$symbolicName(states) configure -text {",S2,"}"]),!.
178
179 %%---------------------------------------------------------------------
180 % display_diagnosis
181 display_diag(View) :- diag(X),
182 write_display_diag(X,View).
183
184 % display_execution exapmle.
185 display_exe(View) :- exe(Z),
186 write_display_diag(Z,View).
187
188 write_display_diag(counter_example(Hist),View) :-!,display_ce(Hist,View).
189 write_display_diag(execution(Hist),View) :-!,display_ce(Hist,View).
190 write_display_diag(R,_View):-!,
191 atomic(R),name(R,Text),
192 clear_display,
193 tcl_eval(['$symbolicName(canvas) create text 0 0 -text "',Text,'"']).
194
195 % append([],X,X):-!.
196 % append([H|X],Y,[H|Z]) :- append(X,Y,Z).
197
198 clear_display :-
199 tcl_eval('$symbolicName(canvas) delete all').
200 display_ce(Hist,View) :-
201 canvas_origin(OX,OY),
202 font(_,Fs),
203 clear_display,
204 X is OX+Fs/2,Y=OY,W is integer(60/24*Fs),H is integer(60/24*Fs),
205 (variable_list(L);L=[]),append(L,['Time'],L1),!,
206 display_var(['State'|L1],View,X,Y,H,X,X1),
207 X2 is X1+X,
208 display_ce(Hist,L,View,X2,Y,W,H,0). % ,View=>batchmodeoff.
209 display_var([],_,_,_,_,X,X):-!.
210 display_var([Var|L],View,X,Y,H,X1,X2):- atomic(Var),!,
211 Y1 is Y+H, font(_Fn,Fs),
212 name(Var,VarText),length(VarText,Len0),Len is Len0*Fs,
213 % View=>stringlength(VarText,Len),
214 (X1>X+Len,X3=X1;X3 is X+Len),!,
215 display_string(X,Y,VarText),
216 display_var(L,View,X,Y1,H,X3,X2).
217 display_var([Var|L],View,X,Y,H,X1,X2):-
218 functor(Var,VarH,2),member(VarH,[(^)]),!,
219 arg(1,Var,VarA),arg(2,Var,VarB),
220 % infix operator
221 Y1 is Y+H, font(_Fn,Fs),
222 name(VarH,VarTextH),name(VarA,VarTextA),name(VarB,VarTextB),
223 append(VarTextA,VarTextH,VarText0),
224 append(VarText0,VarTextB,VarText),
225 length(VarText,Len0),Len is Len0*Fs,
226 % View=>stringlength(VarText,Len),
227 (X1>X+Len,X3=X1;X3 is X+Len),!,
228 display_string(X,Y,VarText),
229 display_var(L,View,X,Y1,H,X3,X2).
230 display_var([Var|L],View,X,Y,H,X1,X2):-
231 functor(Var,VarH,2),
232 arg(1,Var,VarA),arg(2,Var,VarB),
233 Y1 is Y+H, font(_Fn,Fs),
234 name(VarH,VarTextH),name(VarA,VarTextA),name(VarB,VarTextB),
235 CB is "(",CE is ")",CC is ",",
236 append(VarTextH,[CB|VarTextA],VarText0),
237 append(VarText0,[CC|VarTextB],VarText1),
238 append(VarText1,[CE],VarText),
239 length(VarText,Len0),Len is Len0*Fs,
240 % View=>stringlength(VarText,Len),
241 (X1>X+Len,X3=X1;X3 is X+Len),!,
242 display_string(X,Y,VarText),
243 display_var(L,View,X,Y1,H,X3,X2).
244
245 display_string(X,Y,Text) :-
246 font(Fn,_),
247 name(X,XL),name(Y,YL),
248 tcl_eval(['$symbolicName(canvas) create text ',XL,' ',YL,' -font ',Fn,
249 ' -text "', Text,'"'
250 ]).
251 display_ce([],_,_,_,_,_,_,_):-!.
252 display_ce([(S->[_|Cond])|Hist],L,View,X,Y,W,H,T) :-
253 X1 is X+W,Y1 is Y+H,T1 is T+1,
254 name(S,SText),display_string(X1,Y,SText),
255 display_now(L,Cond,View,X1,Y1,W,H,T),
256 display_ce(Hist,L,View,X1,Y,W,H,T1).
257
258 display_now([],_,_View,X,Y,_,_,T):-!,
259 name(T,SText),display_string(X,Y,SText).
260 display_now([V|Vr],Cond,View,X,Y,W,H,T):-
261 XS is X-H/2,YS is Y-H/2,
262 display_state(Cond,V,View,XS,YS,W,H),
263 Y1 is Y+H,
264 display_now(Vr,Cond,View,X,Y1,W,H,T).
265
266 rectangle(1,X,Y,X2,Y2) :-!,
267 name(X,XL),name(Y,YL), name(X2,XL2),name(Y2,YL2),
268 tcl_eval(['$symbolicName(canvas) create rectangle ',
269 XL,' ',YL,' ', XL2,' ',YL2,' ',
270 '-stipple gray50 -fill black'
271 ]).
272 rectangle(0,X,Y,X2,Y2) :-
273 name(X,XL),name(Y,YL), name(X2,XL2),name(Y2,YL2),
274 tcl_eval(['$symbolicName(canvas) create rectangle ',
275 XL,' ',YL,' ', XL2,' ',YL2
276 ]).
277 display_state([V|_],V,_View,X,Y,W,H) :-!, % true
278 X2 is X+W,Y2 is Y+H,
279 rectangle(1,X,Y,X2,Y2).
280 display_state([not(V)|_],V,_View,X,Y,W,H) :-!, % false
281 X2 is X+W,Y2 is Y+H,
282 rectangle(0,X,Y,X2,Y2).
283 display_state([_|T],V,View,X,Y,W,H) :-!,
284 display_state(T,V,View,X,Y,W,H).
285 display_state([],_,_View,X,Y,W,H) :-!, % unknown
286 X2 is X+W,Y2 is Y+H/2,Y3 is Y2+3,
287 rectangle(0,X,Y2,X2,Y3).
288
289 display_update :- tcl_eval('update').
290
291 view_state(View,W) :-
292 itl_state_number(S),
293 clear_display,
294 canvas_origin(OX,OY),
295 calc_view_size(W,S,D,W0),
296 % write(calc_view_size(W,S,D,W0)),nl,
297 W1 is OX + W0 + D, H1 is OY + W0 + D,
298 rectangle(0,OX,OY,W1,H1),
299 view_state_write(View,W0,S,D).
300
301 calc_view_size(W,S,D,W1) :-
302 D0 is integer(W/(S+1)),(D0<2,D=2;D=D0),!,
303 W0 is D*(S+1),(W0=<W,!,W1 = W0; W1 is integer(W)),!.
304
305 view_state_write(_View,W,S,D) :-
306 canvas_origin(OX,OY),
307 links(X,Y), link_translate(X,Y,X1,Y1,W,S),
308 X2 is OX+X1+D,Y2 is OY+Y1+D,
309 X11 is OX+X1,Y11 is OY+Y1,
310 rectangle(1,X11,Y11,X2,Y2),
311 display_update,
312 fail.
313 view_state_write(_View,_,_,_):-true.
314
315 link_translate(false,Y,X1,Y1,W,S) :- !,
316 link_translate(S,Y,X1,Y1,W,S).
317 link_translate(X,false,X1,Y1,W,S) :- !,
318 link_translate(X,S,X1,Y1,W,S).
319 link_translate(X,Y,X1,Y1,W,S) :- number(X),number(Y),!,
320 X1 is integer(X*W/(S+1))+1, Y1 is integer(Y*W/(S+1)).
321 link_translate(X,_,X1,0,W,S) :- number(X),!,
322 X1 is integer(X*W/(S+1)).
323 link_translate(_,Y,0,Y1,W,S) :- number(Y),!,
324 Y1 is integer(Y*W/(S+1)).
325 link_translate(_,_,0,0,_,_).
326
327 %%
328
329 s2term("",true):-!.
330 s2term(Text,Term) :-
331 telling(O),
332 tell(tmp),format("~s.~n",[Text]),told,tell(O),
333 seeing(I),
334 see(tmp),on_exception(Er,read(Term),read_error(Term,Er,I,O)),
335 see(tmp),seen,see(I),!.
336 s2term(_,true):-tell(tmp),told,see(tmp),seen.
337
338 s2terms("",true):-!.
339 s2terms(Text,Terms) :-
340 check_period(Text,0,Text1),
341 telling(O),
342 tell(tmp),format("~s~n",[Text1]),told,tell(O),
343 seeing(I),
344 see(tmp),on_exception(Er,s2terms0(Terms),read_error(Terms,Er,I,O)),
345 see(tmp),seen,see(I),!.
346 s2terms(_,true):-tell(tmp),told,see(tmp),seen.
347
348 s2terms0(Terms) :-read(X),s2terms0(X,Terms).
349 s2terms0(end_of_file,[]):-!.
350 s2terms0(H,[H|T]):-read(X),s2terms0(X,T).
351
352 read_error(true,Er,I,O) :-
353 tell(tmp),told,see(tmp),seen,
354 see(I),tell(O), % unix(system('rm tmp')),
355 write('read error:'),write(Er),nl.
356
357 t2string(Term,Text) :-
358 telling(O),
359 tell(tmp),write(Term),told,tell(O),
360 seeing(I),
361 see(tmp),get0(C),read_string(C,Text),see(tmp),seen,see(I),!.
362 t2string(_,true):-tell(tmp),told,see(tmp),seen.
363
364 t2strings(Terms,Text):-!,
365 telling(O),
366 t2strings(Terms),
367 told,tell(O),
368 seeing(I),
369 see(tmp),get0(C),read_string(C,Text),see(tmp),seen,see(I),!.
370 t2strings(_,true):-tell(tmp),told,see(tmp),seen.
371
372 t2strings([]):-!.
373 t2strings([Term|T]):-!,
374 tell(tmp),write(Term),put("."),put(10),t2strings(T).
375
376 read_string(-1,[]) :- !.
377 read_string(C,[C|T]) :-
378 get0(C1),read_string(C1,T).
379
380 check_period([],0,[32,46]):-!.
381 check_period([],1,[]):-!.
382 check_period([46],_,[46]):-!.
383 check_period([46,X|T],_,[46,X|T1]):-(X=32;X=10;X=37),!,
384 check_period(T,1,T1).
385 check_period([37|T],X,[37|T1]):-
386 skip_line(T,X,T1).
387 check_period([X|T],P,[X|T1]):-(X=32;X=10),!,
388 check_period(T,P,T1).
389 check_period([X|T],_,[X|T1]):-
390 check_period(T,0,T1).
391
392 skip_line([],X,[]):-!,
393 check_period([],X,_).
394 skip_line([10|T],X,[10|T1]):-!,
395 check_period(T,X,T1).
396 skip_line([_|T],X,T1):-skip_line(T,X,T1).
397
398 % sicstus dependent
399 easy_pp(X,X1) :- easy_pp(X,X1,0).
400 easy_pp([],[10],_) :- !.
401 easy_pp([C|T],[C1,10|T0],_) :- C is ".",!,C1 = C,
402 easy_pp(T,T0,0).
403 easy_pp([C|T],[C1,10|T0],N) :- C is ",",!,C1 = C,
404 easy_tab(N,T0,T1),easy_pp(T,T1,N).
405 easy_pp([C|T],[C1,10|T0],N) :- C is ";",!,C1 = C,
406 easy_tab(N,T0,T1),easy_pp(T,T1,N).
407 easy_pp([C,C|T],[C1,C1,10|T0],N) :- C is "&",!,C1 = C, % &&
408 easy_tab(N,T0,T1),easy_pp(T,T1,N).
409 easy_pp([C|T],[C1,10|T0],N) :- C is "&",!,C1 = C, % &
410 easy_tab(N,T0,T1),easy_pp(T,T1,N).
411 easy_pp([C,C1,C2,CB|T],C3,N) :- [C,_,C2,CB]="[a](",!, % quote '[a]'
412 CQ is "'", C3 = [CQ,C,C1,C2,CQ,CB|T1],
413 easy_pp(T,T1,N).
414 easy_pp([10|T],[10|T0],N) :- !,
415 easy_tab(N,T0,T1),easy_pp(T,T1,N).
416 easy_pp([Par|T],[Par1|T0],N) :- Par is "(",!,Par1 = Par,
417 N1 is N+1,easy_pp(T,T0,N1).
418 easy_pp([Par|T],[Par1|T0],N) :- Par is ")",!,Par1 = Par,
419 N1 is N-1,easy_pp(T,T0,N1).
420 easy_pp([H|T],[H|T0],N) :-
421 easy_pp(T,T0,N).
422
423 easy_tab(N,T,T1):-N =< 0,!,T=T1.
424 easy_tab(N,[32,32|T],T1) :-
425 N1 is N-1,easy_tab(N1,T,T1).
426
427 % end %