2
|
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 %
|