|
2
|
1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
2 %%
|
|
|
3 %% LITE Tcl/Tk interface
|
|
|
4 %%
|
|
|
5 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
6
|
|
|
7 :- ensure_loaded('../Lite/lite').
|
|
|
8 :- module(lite).
|
|
|
9 % :- use_module(library(tk)).
|
|
|
10 :- use_module(library(tcltk)).
|
|
|
11 :- verbose(off).
|
|
|
12
|
|
|
13 :- dynamic r_event/2.
|
|
|
14
|
|
|
15 :- abolish(show_state,2).
|
|
|
16 % Next command keep check event during verification
|
|
|
17 show_state(S,ITL) :-!,
|
|
|
18 (tcl_eval(update);true),!,
|
|
|
19 nl,write('state('),write(S), % (
|
|
|
20 (verbose,write(' , '), write(ITL),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 recorded(itl_state_number,S,_), % number of state
|
|
|
174 recorded(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):-
|
|
|
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
|
|
|
218 display_string(X,Y,Text) :-
|
|
|
219 font(Fn,_),
|
|
|
220 name(X,XL),name(Y,YL),
|
|
|
221 tcl_eval(['$symbolicName(canvas) create text ',XL,' ',YL,' -font ',Fn,
|
|
|
222 ' -text "', Text,'"'
|
|
|
223 ]).
|
|
|
224 display_ce([],_,_,_,_,_,_,_):-!.
|
|
|
225 display_ce([(S->[_|Cond])|Hist],L,View,X,Y,W,H,T) :-
|
|
|
226 X1 is X+W,Y1 is Y+H,T1 is T+1,
|
|
|
227 name(S,SText),display_string(X1,Y,SText),
|
|
|
228 display_now(L,Cond,View,X1,Y1,W,H,T),
|
|
|
229 display_ce(Hist,L,View,X1,Y,W,H,T1).
|
|
|
230
|
|
|
231 display_now([],_,_View,X,Y,_,_,T):-!,
|
|
|
232 name(T,SText),display_string(X,Y,SText).
|
|
|
233 display_now([V|Vr],Cond,View,X,Y,W,H,T):-
|
|
|
234 XS is X-H/2,YS is Y-H/2,
|
|
|
235 display_state(Cond,V,View,XS,YS,W,H),
|
|
|
236 Y1 is Y+H,
|
|
|
237 display_now(Vr,Cond,View,X,Y1,W,H,T).
|
|
|
238
|
|
|
239 rectangle(1,X,Y,X2,Y2) :-!,
|
|
|
240 name(X,XL),name(Y,YL), name(X2,XL2),name(Y2,YL2),
|
|
|
241 tcl_eval(['$symbolicName(canvas) create rectangle ',
|
|
|
242 XL,' ',YL,' ', XL2,' ',YL2,' ',
|
|
|
243 '-stipple gray50 -fill black'
|
|
|
244 ]).
|
|
|
245 rectangle(0,X,Y,X2,Y2) :-
|
|
|
246 name(X,XL),name(Y,YL), name(X2,XL2),name(Y2,YL2),
|
|
|
247 tcl_eval(['$symbolicName(canvas) create rectangle ',
|
|
|
248 XL,' ',YL,' ', XL2,' ',YL2
|
|
|
249 ]).
|
|
|
250 display_state([V|_],V,_View,X,Y,W,H) :-!, % true
|
|
|
251 X2 is X+W,Y2 is Y+H,
|
|
|
252 rectangle(1,X,Y,X2,Y2).
|
|
|
253 display_state([not(V)|_],V,_View,X,Y,W,H) :-!, % false
|
|
|
254 X2 is X+W,Y2 is Y+H,
|
|
|
255 rectangle(0,X,Y,X2,Y2).
|
|
|
256 display_state([_|T],V,View,X,Y,W,H) :-!,
|
|
|
257 display_state(T,V,View,X,Y,W,H).
|
|
|
258 display_state([],_,_View,X,Y,W,H) :-!, % unknown
|
|
|
259 X2 is X+W,Y2 is Y+H/2,Y3 is Y2+3,
|
|
|
260 rectangle(0,X,Y2,X2,Y3).
|
|
|
261
|
|
|
262 display_update :- tcl_eval('update').
|
|
|
263
|
|
|
264 view_state(View,W) :-
|
|
|
265 recorded(itl_state_number,S,_),
|
|
|
266 clear_display,
|
|
|
267 canvas_origin(OX,OY),
|
|
|
268 calc_view_size(W,S,D,W0),
|
|
|
269 % write(calc_view_size(W,S,D,W0)),nl,
|
|
|
270 W1 is OX + W0 + D, H1 is OY + W0 + D,
|
|
|
271 rectangle(0,OX,OY,W1,H1),
|
|
|
272 view_state_write(View,W0,S,D).
|
|
|
273
|
|
|
274 calc_view_size(W,S,D,W1) :-
|
|
|
275 D0 is integer(W/(S+1)),(D0<2,D=2;D=D0),!,
|
|
|
276 W0 is D*(S+1),(W0=<W,!,W1 = W0; W1 is integer(W)),!.
|
|
|
277
|
|
|
278 view_state_write(_View,W,S,D) :-
|
|
|
279 canvas_origin(OX,OY),
|
|
|
280 links(X,Y), link_translate(X,Y,X1,Y1,W,S),
|
|
|
281 X2 is OX+X1+D,Y2 is OY+Y1+D,
|
|
|
282 X11 is OX+X1,Y11 is OY+Y1,
|
|
|
283 rectangle(1,X11,Y11,X2,Y2),
|
|
|
284 display_update,
|
|
|
285 fail.
|
|
|
286 view_state_write(_View,_,_,_):-true.
|
|
|
287
|
|
|
288 link_translate(false,Y,X1,Y1,W,S) :- !,
|
|
|
289 link_translate(S,Y,X1,Y1,W,S).
|
|
|
290 link_translate(X,false,X1,Y1,W,S) :- !,
|
|
|
291 link_translate(X,S,X1,Y1,W,S).
|
|
|
292 link_translate(X,Y,X1,Y1,W,S) :- number(X),number(Y),!,
|
|
|
293 X1 is integer(X*W/(S+1))+1, Y1 is integer(Y*W/(S+1)).
|
|
|
294 link_translate(X,_,X1,0,W,S) :- number(X),!,
|
|
|
295 X1 is integer(X*W/(S+1)).
|
|
|
296 link_translate(_,Y,0,Y1,W,S) :- number(Y),!,
|
|
|
297 Y1 is integer(Y*W/(S+1)).
|
|
|
298 link_translate(_,_,0,0,_,_).
|
|
|
299
|
|
|
300 %%
|
|
|
301
|
|
|
302 s2term("",true):-!.
|
|
|
303 s2term(Text,Term) :-
|
|
|
304 telling(O),
|
|
|
305 tell(tmp),format("~s.~n",[Text]),told,tell(O),
|
|
|
306 seeing(I),
|
|
|
307 see(tmp),on_exception(Er,read(Term),read_error(Term,Er,I,O)),
|
|
|
308 see(tmp),seen,see(I),!.
|
|
|
309 s2term(_,true):-tell(tmp),told,see(tmp),seen.
|
|
|
310
|
|
|
311 s2terms("",true):-!.
|
|
|
312 s2terms(Text,Terms) :-
|
|
|
313 check_period(Text,0,Text1),
|
|
|
314 telling(O),
|
|
|
315 tell(tmp),format("~s~n",[Text1]),told,tell(O),
|
|
|
316 seeing(I),
|
|
|
317 see(tmp),on_exception(Er,s2terms0(Terms),read_error(Terms,Er,I,O)),
|
|
|
318 see(tmp),seen,see(I),!.
|
|
|
319 s2terms(_,true):-tell(tmp),told,see(tmp),seen.
|
|
|
320
|
|
|
321 s2terms0(Terms) :-read(X),s2terms0(X,Terms).
|
|
|
322 s2terms0(end_of_file,[]):-!.
|
|
|
323 s2terms0(H,[H|T]):-read(X),s2terms0(X,T).
|
|
|
324
|
|
|
325 read_error(true,Er,I,O) :-
|
|
|
326 tell(tmp),told,see(tmp),seen,
|
|
|
327 see(I),tell(O), % unix(system('rm tmp')),
|
|
|
328 write('read error:'),write(Er),nl.
|
|
|
329
|
|
|
330 t2string(Term,Text) :-
|
|
|
331 telling(O),
|
|
|
332 tell(tmp),write(Term),told,tell(O),
|
|
|
333 seeing(I),
|
|
|
334 see(tmp),get0(C),read_string(C,Text),see(tmp),seen,see(I),!.
|
|
|
335 t2string(_,true):-tell(tmp),told,see(tmp),seen.
|
|
|
336
|
|
|
337 t2strings(Terms,Text):-!,
|
|
|
338 telling(O),
|
|
|
339 t2strings(Terms),
|
|
|
340 told,tell(O),
|
|
|
341 seeing(I),
|
|
|
342 see(tmp),get0(C),read_string(C,Text),see(tmp),seen,see(I),!.
|
|
|
343 t2strings(_,true):-tell(tmp),told,see(tmp),seen.
|
|
|
344
|
|
|
345 t2strings([]):-!.
|
|
|
346 t2strings([Term|T]):-!,
|
|
|
347 tell(tmp),write(Term),put("."),put(10),t2strings(T).
|
|
|
348
|
|
|
349 read_string(-1,[]) :- !.
|
|
|
350 read_string(C,[C|T]) :-
|
|
|
351 get0(C1),read_string(C1,T).
|
|
|
352
|
|
|
353 check_period([],0,[32,46]):-!.
|
|
|
354 check_period([],1,[]):-!.
|
|
|
355 check_period([46],_,[46]):-!.
|
|
|
356 check_period([46,X|T],_,[46,X|T1]):-(X=32;X=10;X=37),!,
|
|
|
357 check_period(T,1,T1).
|
|
|
358 check_period([37|T],X,[37|T1]):-
|
|
|
359 skip_line(T,X,T1).
|
|
|
360 check_period([X|T],P,[X|T1]):-(X=32;X=10),!,
|
|
|
361 check_period(T,P,T1).
|
|
|
362 check_period([X|T],_,[X|T1]):-
|
|
|
363 check_period(T,0,T1).
|
|
|
364
|
|
|
365 skip_line([],X,[]):-!,
|
|
|
366 check_period([],X,_).
|
|
|
367 skip_line([10|T],X,[10|T1]):-!,
|
|
|
368 check_period(T,X,T1).
|
|
|
369 skip_line([_|T],X,T1):-skip_line(T,X,T1).
|
|
|
370
|
|
|
371 easy_pp(X,X1) :- easy_pp(X,X1,0).
|
|
|
372 easy_pp([],[10],_) :- !.
|
|
|
373 easy_pp([C|T],[C1,10|T0],_) :- C is ".",!,C1 = C,
|
|
|
374 easy_pp(T,T0,0).
|
|
|
375 easy_pp([C|T],[C1,10|T0],N) :- C is ",",!,C1 = C,
|
|
|
376 easy_tab(N,T0,T1),easy_pp(T,T1,N).
|
|
|
377 easy_pp([C|T],[C1,10|T0],N) :- C is ";",!,C1 = C,
|
|
|
378 easy_tab(N,T0,T1),easy_pp(T,T1,N).
|
|
|
379 easy_pp([C,C|T],[C1,C1,10|T0],N) :- C is "&",!,C1 = C, % &&
|
|
|
380 easy_tab(N,T0,T1),easy_pp(T,T1,N).
|
|
|
381 easy_pp([C|T],[C1,10|T0],N) :- C is "&",!,C1 = C, % &
|
|
|
382 easy_tab(N,T0,T1),easy_pp(T,T1,N).
|
|
|
383 easy_pp([10|T],[10|T0],N) :- !,
|
|
|
384 easy_tab(N,T0,T1),easy_pp(T,T1,N).
|
|
|
385 easy_pp([Par|T],[Par1|T0],N) :- Par is "(",!,Par1 = Par,
|
|
|
386 N1 is N+1,easy_pp(T,T0,N1).
|
|
|
387 easy_pp([Par|T],[Par1|T0],N) :- Par is ")",!,Par1 = Par,
|
|
|
388 N1 is N-1,easy_pp(T,T0,N1).
|
|
|
389 easy_pp([H|T],[H|T0],N) :-
|
|
|
390 easy_pp(T,T0,N).
|
|
|
391
|
|
|
392 easy_tab(N,T,T1):-N =< 0,!,T=T1.
|
|
|
393 easy_tab(N,[32,32|T],T1) :-
|
|
|
394 N1 is N-1,easy_tab(N1,T,T1).
|
|
|
395
|
|
|
396 % end %
|
