%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% LITE Tcl/Tk interface %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % :- ensure_loaded('../tableau/lite'). :- module(lite). :- use_module(library(tcltk)). :- verbose(off). :- dynamic r_event/2. :- abolish(show_state,2). % Next command keep check event during verification show_state(S,ITL) :-!, (tcl_eval(update);true),!, bdt2itl(ITL,ITL1), nl,write('state('),write(S), % ( (verbose,write(' , '), write(ITL1),write(')'),nl;write(')')),!. event(verbose,'1') :- verbose(on). event(verbose,'0') :- verbose(off). event(X,Y) :- assertz(r_event(X,Y)). % ,write((X,Y)),nl. event(X) :- assertz(r_event(X,[])). % ,write((X)),nl. next(X,Y) :- r_event(_,_),retract(r_event(X,Y)),!. next(X,Y) :- tk_do_one_event(0),!, next(X,Y). display :- init_display,!, event_loop(run), tcl_exit. tcl_exit :- tcl(X),tcl_delete(X),retract(tcl(X)). tcl_name(L,Name) :- concatenate(L,L1), name(Name,L1). concatenate([],[]). concatenate([H|T],X) :- atomic(H),!, name(H,List),concatenate(T,X1),append(List,X1,X). concatenate([H|T],X) :- H=[_|_], concatenate(T,X1),append(H,X1,X). tcl_eval(E) :- atomic(E),!, tcl(Tcl),tcl_eval(Tcl,E,_). tcl_eval(E) :- E=[_|_],tcl_name(E,N), tcl(Tcl),tcl_eval(Tcl,N,_). init_display :- (retract(r_event(_,_)),fail;true), tk_new([name('Lite Verifier')], Tcl), assert(tcl(Tcl)), % tcl_eval('source disp.tcl'), tcl_eval('source xf-disp'), all_disable. canvas_origin(20,20). event_loop(quit):-!. event_loop(_) :- next(X,Y),execute(X,Y),!,event_loop(X). execute(verify,X) :- !, verify(X). % !,X=1 -> verbose(on); verbose(off). causes error execute(verbose,X) :- X='1' -> verbose(on); verbose(off). execute(map,X) :- !,name(X,L),name(X1,L),view_state(a,X1). execute(execute,_) :- !,do_execute,!. execute(generate,_) :- !, generate. execute(counter,_) :- !,do_diagnosis,!. execute(quit,_) :- !. % ,tcl_eval('destroy .'). execute(prolog_call,X) :- !,prolog_call(X). execute(tokio_call,X) :- !,tokio_call(X). execute(X,_) :- !,write(event(X)),nl,ttyflush. generate :- TOKIO = 'tmp.tokio', tell(TOKIO),tgen,told, user:com(TOKIO,'tmp.out'). gen(X) :- consult(X),specification(Y),ex(Y),generate. gen(X) :- name(X,XL),append(XL,".lite",YL),name(X1,YL), consult(X1),specification(Y),ex(Y),generate. verify(X) :- all_disable, abolish(st,3),abolish(specification,1),abolish(st_variables,2), t2string(X,X0),s2terms(X0,X1),command(X1,X2,X3), display_contents(X3), ex(X2),!, ttyflush, display_statistics, all_enable. verify(_) :- all_disable. display_contents(X) :- ttyflush,t2string(X,XS0),easy_pp(XS0,XS), tcl_eval('$symbolicName(entry) delete 0.0 end'), tcl_eval(['$symbolicName(entry) insert 0.0 {',XS,'}']), display_update. all_disable :- tcl_eval('$symbolicName(map) configure -state disabled'), tcl_eval('$symbolicName(execute) configure -state disabled'), tcl_eval('$symbolicName(diag) configure -state disabled'), display_update. all_enable :- tcl_eval('$symbolicName(map) configure -state normal'), tcl_eval('$symbolicName(execute) configure -state normal'), tcl_eval('$symbolicName(diag) configure -state normal'), display_update. % Backtrack Control of example/counter example do_execute :- display_exe('.'),next(X,Y),do_execute(X,Y),!. do_execute. do_execute(execute,_) :-!, fail. do_execute(X,Y) :- execute(X,Y),!. do_diagnosis :- display_diag(','),next(X,Y),do_diagnosis(X,Y),!. do_diagnosis. do_diagnosis(diag,_) :-!, fail. do_diagnosis(X,Y) :- execute(X,Y),!. % :- dynamic specification/1. % Text Based Commnad command([st(X,Y,Z)|T],Term,[st(X,Y,Z)|T1]):-!, assertz(st(X,Y,Z)),!, command(T,Term,T1). command([specification(X)|T],X,[specification(X)|T1]):-!, command(T,X,T1). command([st_variables(X,Y)|T],Term,[st_variables(X,Y)|T1]):-!, assertz(st_variables(X,Y)), command(T,Term,T1). command([],true,[]) :-!. command([],_,[]) :-!. command([H],Term,[Term1]) :-!, command(H,Term),!,Term=Term1. command([H|T],(Term1,Terms),[Term1|T1]) :- command(H,Term1),!,command(T,Terms,T1). command(demo(X),Term):-!,lite:demo(X,Term). % predefined examples command(ex(X),Term):-!,ex(X,Term). command(prolog(X,P),X):-!,safe_call(P). command(prolog(P),true):-!,safe_call(P). command(tokio(P),true):-!,safe_call(tokio(P)). command(consult(P),Term):-!, command(file(P),Term). command(file(P),Term):- on_exception(Er,(consult(P),specification(Term)), read_error(Term,Er,user,user)). command(A,A) :- atomic(A),!. command(P,R) :- functor(P,H,N),functor(R,H,N), command_arg(N,P,R). command_arg(0,_P,_R):-!. command_arg(N,P,R):-arg(N,P,PA),arg(N,R,RA), N1 is N-1,command(PA,RA),command_arg(N1,P,R). prolog_call(X) :- t2string(X,X0),s2terms(X0,[X1|_]),safe_call(X1). tokio_call(X) :- t2string(X,X0),s2terms(X0,[X1|_]),safe_call(tokio(X1)). safe_call(X) :- on_exception(Er,user:call(X), read_error(X,Er,user,user)),!. safe_call(_). :-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_statistics :- 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), tcl_eval(["$symbolicName(states) configure -text {",S2,"}"]),!. %%--------------------------------------------------------------------- % 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), clear_display, tcl_eval(['$symbolicName(canvas) create text 0 0 -text "',Text,'"']). % append([],X,X):-!. % append([H|X],Y,[H|Z]) :- append(X,Y,Z). clear_display :- tcl_eval('$symbolicName(canvas) delete all'). display_ce(Hist,View) :- canvas_origin(OX,OY), font(_,Fs), clear_display, X is OX+Fs/2,Y=OY,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):- atomic(Var),!, Y1 is Y+H, font(_Fn,Fs), name(Var,VarText),length(VarText,Len0),Len is Len0*Fs, % View=>stringlength(VarText,Len), (X1>X+Len,X3=X1;X3 is X+Len),!, display_string(X,Y,VarText), display_var(L,View,X,Y1,H,X3,X2). display_var([Var|L],View,X,Y,H,X1,X2):- functor(Var,VarH,2),member(VarH,[(^)]),!, arg(1,Var,VarA),arg(2,Var,VarB), % infix operator Y1 is Y+H, font(_Fn,Fs), name(VarH,VarTextH),name(VarA,VarTextA),name(VarB,VarTextB), append(VarTextA,VarTextH,VarText0), append(VarText0,VarTextB,VarText), length(VarText,Len0),Len is Len0*Fs, % View=>stringlength(VarText,Len), (X1>X+Len,X3=X1;X3 is X+Len),!, display_string(X,Y,VarText), display_var(L,View,X,Y1,H,X3,X2). display_var([Var|L],View,X,Y,H,X1,X2):- functor(Var,VarH,2), arg(1,Var,VarA),arg(2,Var,VarB), Y1 is Y+H, font(_Fn,Fs), name(VarH,VarTextH),name(VarA,VarTextA),name(VarB,VarTextB), CB is "(",CE is ")",CC is ",", append(VarTextH,[CB|VarTextA],VarText0), append(VarText0,[CC|VarTextB],VarText1), append(VarText1,[CE],VarText), length(VarText,Len0),Len is Len0*Fs, % View=>stringlength(VarText,Len), (X1>X+Len,X3=X1;X3 is X+Len),!, display_string(X,Y,VarText), display_var(L,View,X,Y1,H,X3,X2). display_string(X,Y,Text) :- font(Fn,_), name(X,XL),name(Y,YL), tcl_eval(['$symbolicName(canvas) create text ',XL,' ',YL,' -font ',Fn, ' -text "', Text,'"' ]). 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),display_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),display_string(X,Y,SText). display_now([V|Vr],Cond,View,X,Y,W,H,T):- XS is X-H/2,YS is Y-H/2, display_state(Cond,V,View,XS,YS,W,H), Y1 is Y+H, display_now(Vr,Cond,View,X,Y1,W,H,T). rectangle(1,X,Y,X2,Y2) :-!, name(X,XL),name(Y,YL), name(X2,XL2),name(Y2,YL2), tcl_eval(['$symbolicName(canvas) create rectangle ', XL,' ',YL,' ', XL2,' ',YL2,' ', '-stipple gray50 -fill black' ]). rectangle(0,X,Y,X2,Y2) :- name(X,XL),name(Y,YL), name(X2,XL2),name(Y2,YL2), tcl_eval(['$symbolicName(canvas) create rectangle ', XL,' ',YL,' ', XL2,' ',YL2 ]). display_state([V|_],V,_View,X,Y,W,H) :-!, % true X2 is X+W,Y2 is Y+H, rectangle(1,X,Y,X2,Y2). display_state([not(V)|_],V,_View,X,Y,W,H) :-!, % false X2 is X+W,Y2 is Y+H, rectangle(0,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, rectangle(0,X,Y2,X2,Y3). display_update :- tcl_eval('update'). view_state(View,W) :- itl_state_number(S), clear_display, canvas_origin(OX,OY), calc_view_size(W,S,D,W0), % write(calc_view_size(W,S,D,W0)),nl, W1 is OX + W0 + D, H1 is OY + W0 + D, rectangle(0,OX,OY,W1,H1), view_state_write(View,W0,S,D). calc_view_size(W,S,D,W1) :- D0 is integer(W/(S+1)),(D0<2,D=2;D=D0),!, W0 is D*(S+1),(W0=