# HG changeset patch # User kono # Date 1188445475 -32400 # Node ID e1d3145cff7a542092a0c44d28fb36fbf1fd3bf5 # Parent a6adedccd5f630940072fe71d96183cd4d8262cc *** empty log message *** diff -r a6adedccd5f6 -r e1d3145cff7a chop.pl --- a/chop.pl Sun Jan 21 10:21:43 2001 +0900 +++ b/chop.pl Thu Aug 30 12:44:35 2007 +0900 @@ -32,18 +32,12 @@ def(infinite, (true & false)). % def(finite, ~((true & false))). % def(length(I), X):- I>=0 ,def_length(I,X). % length operator - def_length(I,empty):-I=<0,!. - def_length(I,@ X):-I1 is I-1,def_length(I1,X). def(less(I), X):- I>=0 ,def_less(I,X). % less than N length - def_less(I,false):-I=<0,!. - def_less(I,next(X)):-I1 is I-1,def_less(I1,X). def(next(P),(empty; @(P))). % temporal assignments def(gets(A,B),keep(@A<->B)). def(stable(A),keep(@A<->A)). def(state(A),(share(A),'[]'(L))):- def_state(A,L). - def_state([H],H):-!. - def_state([H|L],(H;L1)):-def_state(L,L1). % def(Q=>P,exists(R,(Q = R,stable(R),fin(P = R)))). % easier one % def(Q=>P,(Q & (empty,P); ~Q & (empty, ~P))). @@ -57,11 +51,6 @@ def(local(P), (P = (P&true))):- !. % test predicates def(trace(X,List),L) :- !,make_trace(List,X,L). - make_trace([],_,true):-!. - make_trace([1|T],X,(X,@L)):-!, make_trace(T,X,L). - make_trace([true|T],X,(X,@L)):-!, make_trace(T,X,L). - make_trace([0|T],X,(not(X),@L)):-!, make_trace(T,X,L). - make_trace([_|T],X,(not(X),@L)):-!, make_trace(T,X,L). def(even(P), exists(Q,(Q, keep( @Q = ~Q),'[]'((Q->P))))). def(evenp(P),( @@ -71,6 +60,18 @@ +('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) )). def(X,Y) :- define(X,Y). +def_length(I,empty):-I=<0,!. +def_length(I,@ X):-I1 is I-1,def_length(I1,X). +def_less(I,false):-I=<0,!. +def_less(I,next(X)):-I1 is I-1,def_less(I1,X). +def_state([H],H):-!. +def_state([H|L],(H;L1)):-def_state(L,L1). +make_trace([],_,true):-!. +make_trace([1|T],X,(X,@L)):-!, make_trace(T,X,L). +make_trace([true|T],X,(X,@L)):-!, make_trace(T,X,L). +make_trace([0|T],X,(not(X),@L)):-!, make_trace(T,X,L). +make_trace([_|T],X,(not(X),@L)):-!, make_trace(T,X,L). + :-dynamic variable/1. expand(X,Y) :- init_variable,expand1(X,Y). @@ -82,10 +83,6 @@ % expand1([P|Q],R) :- !,expand1(P,P1),expand1(Q,Q1),and(P1,Q1,R). expand1((P;Q),R) :- !,expand1(P,P1),expand1(Q,Q1),or(P1,Q1,R). expand1((P&Q),R) :- !,expand1(P,P1),expand1(Q,Q1),chop_expand1(P1,Q1,R). - chop_expand1(false,_,false):-!. -% chop_expand1(_,false,false):-!. - chop_expand1(true,true,true):-!. - chop_expand1(P,Q,(P&Q)):-!. expand1(not(Q),NQ):-!,expand1(Q,Q1),negate(Q1,NQ). expand1(exists(P,Q),exists(P,Q1)):- nonvar(P),name(P,[X|_]),X = 95,!, % "_" % reuse it... @@ -101,31 +98,36 @@ expand_list([H|L],L1), all_and(L1,And), all_not(L1,NAnd). - expand_list([],[]) :-!. - expand_list([H|L],[H1|L1]) :- - expand1(H,H1), expand_list(L,L1). - all_and([],true):-!. - all_and([H|L],F):- all_and(L,F1),and(H,F1,F). - all_not([],true):-!. - all_not([H|L],F):- all_not(L,F1),negate(H,H1),and(H1,F1,F). expand1(^(R),^(R)):-!, % 2nd order variable add_2var(R). expand1(P,R) :- def(P,Q),!,expand1(Q,R). expand1(P,P) :- atomic(P),!, % for empty or skip check_atomic(P). - check_atomic(empty):-!. - check_atomic(more):-!. - check_atomic(true):-!. - check_atomic(false):-!. - check_atomic(true_false):-!. - check_atomic(P) :- name(P,PL),PL=[95|_],!. - check_atomic(P) :- add_variable(P). % "_" expand1(P,R) :- functor(P,H,N),functor(R,H,N), expand_arg(N,P,R). expand_arg(0,_P,_R):-!. expand_arg(N,P,R):-arg(N,P,PA),arg(N,R,RA), N1 is N-1,expand1(PA,RA),expand_arg(N1,P,R). +chop_expand1(false,_,false):-!. +% chop_expand1(_,false,false):-!. +chop_expand1(true,true,true):-!. +chop_expand1(P,Q,(P&Q)):-!. +expand_list([],[]) :-!. +expand_list([H|L],[H1|L1]) :- + expand1(H,H1), expand_list(L,L1). +all_and([],true):-!. +all_and([H|L],F):- all_and(L,F1),and(H,F1,F). +all_not([],true):-!. +all_not([H|L],F):- all_not(L,F1),negate(H,H1),and(H1,F1,F). +check_atomic(empty):-!. +check_atomic(more):-!. +check_atomic(true):-!. +check_atomic(false):-!. +check_atomic(true_false):-!. +check_atomic(P) :- name(P,PL),PL=[95|_],!. +check_atomic(P) :- add_variable(P). % "_" + % do not use abolish here to avoid erase dynamic property of variable/1 init_variable :- retract(variable(_)),fail;true. add_variable([]):-!. diff -r a6adedccd5f6 -r e1d3145cff7a cp.pl --- a/cp.pl Sun Jan 21 10:21:43 2001 +0900 +++ b/cp.pl Thu Aug 30 12:44:35 2007 +0900 @@ -1,52 +1,5 @@ - - - - - - - - - - - - - - - - - - - - - - -% A '\=' A :-!,fail. -% _ '\=' _. - - - - - - - - - - - - - +A '\=' A :-!,fail. +_ '\=' _. r_cputime(X) :- statistics(runtime,[X1,_]),X is X1/1000. - - - - - - - - - append([],X,X). append([H|X],Y,[H|Z]) :- append(X,Y,Z). - - - diff -r a6adedccd5f6 -r e1d3145cff7a demo.pl --- a/demo.pl Sun Jan 21 10:21:43 2001 +0900 +++ b/demo.pl Thu Aug 30 12:44:35 2007 +0900 @@ -1,4 +1,5 @@ -:-ensure_loaded('../tableau/liter'). +% :-ensure_loaded('../tableau/liter'). +:-ensure_loaded(lite). % :-ensure_loaded('../Tokio/initm'). % :-fcompile(lite:disp). :-ensure_loaded(lite:disp). @@ -8,7 +9,7 @@ % :-com([bou],'tmp.out'). -:-write('To do demonstration, +a :-write('To do demonstration, Start Lite verifier ?- display. Load file gi?.lite. @@ -16,3 +17,7 @@ Generate it. Run Tokio command toy0. '). + +:- display. + +:- halt. diff -r a6adedccd5f6 -r e1d3145cff7a diag.pl --- a/diag.pl Sun Jan 21 10:21:43 2001 +0900 +++ b/diag.pl Thu Aug 30 12:44:35 2007 +0900 @@ -125,16 +125,17 @@ write_diag(counter_example(Hist)) :-!,write_ce(Hist,0). write_diag(execution(Hist)) :-!,write_ce(Hist,0). - write_ce([],_):-!. - write_ce([(*)|T],I) :- !, - write(*),nl, - write_ce(T,I). - write_ce([(S->[E|L])|T],I) :- (E=more,L=L1;E=empty,L=L1;[E|L]=L1),!, - write(I),write(:),write_cond(L1),put(9),write(S),nl, - J is I+1, - write_ce(T,J). write_diag(R):-!,write(R),nl. +write_ce([],_):-!. +write_ce([(*)|T],I) :- !, + write(*),nl, + write_ce(T,I). +write_ce([(S->[E|L])|T],I) :- (E=more,L=L1;E=empty,L=L1;[E|L]=L1),!, + write(I),write(:),write_cond(L1),put(9),write(S),nl, + J is I+1, + write_ce(T,J). + % condition print write_cond(X) :- sortC(X,Y),write_cond1(Y). diff -r a6adedccd5f6 -r e1d3145cff7a disp.pl --- a/disp.pl Sun Jan 21 10:21:43 2001 +0900 +++ b/disp.pl Thu Aug 30 12:44:35 2007 +0900 @@ -30,11 +30,31 @@ display :- init_display,!, - event_loop(run). + 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_init('lite',[]), + tk_new([name('Lite Verifier')], Tcl), + assert(tcl(Tcl)), % tcl_eval('source disp.tcl'), tcl_eval('source xf-disp'), all_disable. @@ -78,8 +98,9 @@ all_enable. verify(_) :- all_disable. + display_contents(X) :- - ttyflush,t2strings(X,XS0),easy_pp(XS0,XS), + 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. diff -r a6adedccd5f6 -r e1d3145cff7a display.pl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/display.pl Thu Aug 30 12:44:35 2007 +0900 @@ -0,0 +1,269 @@ +% +% Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc. +% The University, Newcastle upton Tyne +% +% Everyone is permitted to copy and distribute verbatim copies +% of this license, but changing it is not allowed. You can also +% use this wording to make the terms for other programs. +% +% Please, send your comments to kono@csl.sony.co.jp +% $Id$ +% +% Display Interface for ITL Verifier +% Using SICStus Prolog's Graphic Manager ( InterViews Package) +% + +:- use_module(library(gmlib)). + +:-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:- + tell(tmp),told,see(tmp),seen, + font(Font,_),width(W,H), + View <= view(W,H), + View=>setfont(Font), + In <= input("",Font),In => enable, + Execute <= button("Execute",exe,font(Font)),Execute=>disable, + Counter <= button("Counter Example",diag,font(Font)), Counter=>disable, + Map <= button("Map",map,font(Font)), Map=>disable, + ST <= output("State: Edge:",Font), + K <= window("ITL Verifier",vbox([scroller(View), + space( + hbox([output("Enter temporal logic formula:",Font),space,ST])), + space(frame(In)), + border, + space( + hbox([space, + button("Verify",verify,font(Font)), + space,Execute, space,Counter, space, + vbox([ + button("Verbose on",verbose(on), + [style(radio),font(Font)]), + button(" off",verbose(off), + [style(radio),font(Font)]) + ]), + Map, + space, + button("Quit",quit,font(Font)), + space])) + ])), + verbose(off), + _ <= buttonstate(verbose(_),off), + K => open, + handle(In,View,K,[Execute,Counter,Map,ST]). + +handle(In,View,K,N):- + K => waitevent(E), + handle(E,In,View,K,N). +handle(E,In,View,K,N):- + (E=button(_,verify);E=menu(_,verify);E=return(_,_)) -> + handle_verify(In,View,K,N), !,handle(In,View,K,N) + ; + E=button(_,map) -> + clear_event(K), View=>update, width(_,H), + view_state(View,H),!,handle(In,View,K,N) + ; + E=button(_,exe) -> + [Mb,Eb|_]=N, (Mb=>enable,Eb=>enable, + display_exe(View), + K=>waitevent(E1), handle_more(E1,In,View,K,N,exe),!; + Mb=>disable,Eb=>enable, + !, handle(In,View,K,N)) + ; + E=button(_,diag) -> + [Mb,Eb|_]=N, (Mb=>enable,Eb=>enable, + display_diag(View), + K=>waitevent(E1),handle_more(E1,In,View,K,N,diag),!; + Mb=>enable,Eb=>disable, + !, handle(In,View,K,N)) + ; + E=button(_,verbose(on)) -> verbose(on),!, handle(In,View,K,N) + ; + E=button(_,verbose(off)) -> verbose(off),!, handle(In,View,K,N) + ; + E=button(_,noevent) ->!, handle(In,View,K,N) + ; + K => close. % all end + +clear_event(W) :- repeat,W=>nextevent(E),E=noevent. + +handle_verify(In,_,_,N) :- + [Mb,Eb,Map,ST|_]=N,Mb=>disable,Eb=>disable,Map=>disable, + In => in(Text),s2term(Text,Term), + command(Term,Term1),!, + t2string(Term1,Text0), In => out(Text0), + (Term1=prolog(_); ex(Term1)),!, + Mb=>enable,Eb=>enable,Map=>enable, + (verbose ; display_statistics(ST)),!. + +display_statistics(ST) :- + 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), + ST=>out(S2),!. + +% +handle_more(Ev,_,_,_,_,E) :- + Ev=button(_,E), + !,fail. % find another solution +handle_more(Ev,In,View,K,N,_) :- + Ev=button(_,Label),button_event(Label),!, + handle(Ev,In,View,K,N). +handle_more(Ev,In,View,K,N,_) :- + Ev=return(_,_),!, + handle(Ev,In,View,K,N). +handle_more(_,In,View,K,N,E) :-!, + View=>getevent(Ev), + handle_more(Ev,In,View,K,N,E). + +button_event(verify). +button_event(diag). +button_event(exe). +button_event(quit). +button_event(map). +button_event(verbose(on)). +button_event(verbose(off)). +%%--------------------------------------------------------------------- +% 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), + View=>clear,View=>string(0,0,Text). + +display_ce(Hist,View) :- + font(_,Fs), + View=>clear, % View=>batchmode, + View=>setpattern(4), + X is Fs/2,Y=0,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):- + Y1 is Y+H, + name(Var,VarText), + View=>stringlength(VarText,Len), + (X1>X+Len,X3=X1;X3 is X+Len),!, + View=>string(X,Y,VarText), + display_var(L,View,X,Y1,H,X3,X2). + +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),View=>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),View=>string(X,Y,SText). +display_now([V|Vr],Cond,View,X,Y,W,H,T):- + display_state(Cond,V,View,X,Y,W,H), + Y1 is Y+H, + display_now(Vr,Cond,View,X,Y1,W,H,T). + +display_state([V|_],V,View,X,Y,W,H) :-!, % true + X2 is X+W,Y2 is Y+H, + View=>fillrect(X,Y,X2,Y2). +display_state([not(V)|_],V,View,X,Y,W,H) :-!, % false + X2 is X+W,Y2 is Y+H, + View=>rect(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, + View=>rect(X,Y2,X2,Y3). + +s2term("",true):-!. +s2term(Text,Term) :- + telling(O), + tell(tmp),format("~s.~n",[Text]),told,tell(O), + seeing(I), + see(tmp),on_exception(Er,read(Term),read_error(Term,Er,I,O)), + see(tmp),seen,see(I),!. +s2term(_,true):-tell(tmp),told,see(tmp),seen. + +read_error(true,Er,I,O) :- + tell(tmp),told,see(tmp),seen, + see(I),tell(O),unix(system('rm tmp')), + write('read error:'),write(Er),nl. + +t2string(Term,Text) :- + telling(O), + tell(tmp),write(Term),told,tell(O), + seeing(I), + see(tmp),get0(C),read_string(C,Text),see(tmp),seen,see(I),!. +t2string(_,true):-tell(tmp),told,see(tmp),seen. + +read_string(-1,[]) :- !. +read_string(C,[C|T]) :- + get0(C1),read_string(C1,T). + + +command(demo(X),Term):-!,demo(X,Term). % predefined examples +command(ex(X),Term):-!,ex(X,Term). +command(prolog(X,P),X):-!,call(P). +command(prolog(P),prolog(P)):-!,call(P). +command(X,X). + +view_state :- + make_state_view(View,W,K), + view_state(View,W),View=>enable, + repeat, + K=>waitevent(E),E=down(_,_,_,_),K=>close. + +make_state_view(View,W,K) :- + width(W,_),font(Font,_), + View <= view(W,W), + View=>setfont(Font), + K <= window("State Pattern",vbox([scroller(View) ])), + K => open. + +view_state(View,W) :- + View=>setpattern(0), + itl_state_number(S), + View=>clear,View=>disable,View=>update, % View=>batchmode, + View=>string(0,W,"T"), % This prevents core dump + D0 is integer(W/(S+1)),(D0=0,D=1;D=D0),!, + view_state_write(View,W,S,D). +view_state_write(View,W,S,D) :- + links(X,Y), link_translate(X,Y,X1,Y1,W,S), +% View=>fillcircle(X1,Y1,2),fail. +% View=>circle(X1,Y1,2), + X2 is X1+D,Y2 is Y1+D,View=>fillrect(X1,Y1,X2,Y2), + View=>update, + fail. +view_state_write(_View,_,_,_):-true. % View=>batchmodeoff. + +link_translate(false,Y,X1,Y1,W,S) :- !, + link_translate(S,Y,X1,Y1,W,S). +link_translate(X,false,X1,Y1,W,S) :- !, + link_translate(X,S,X1,Y1,W,S). +link_translate(X,Y,X1,Y1,W,S) :- number(X),number(Y),!, + X1 is integer(X*W/(S+1))+1, Y1 is integer(Y*W/(S+1)). +link_translate(X,_,X1,0,W,S) :- number(X),!, + X1 is integer(X*W/(S+1)). +link_translate(_,Y,0,Y1,W,S) :- number(Y),!, + Y1 is integer(Y*W/(S+1)). +link_translate(_,_,0,0,_,_). + +%% diff -r a6adedccd5f6 -r e1d3145cff7a dvcomp.pl --- a/dvcomp.pl Sun Jan 21 10:21:43 2001 +0900 +++ b/dvcomp.pl Thu Aug 30 12:44:35 2007 +0900 @@ -41,44 +41,17 @@ itl(empty,true,empty,C,C). itl(empty,false,E,C,C):-!,E = more. % no succeeding more interval itl(P,FF,_,C,C1) :- atomic(P),!, local(FF,P,C,C1). - local(true,P,C,C1):- true(C,P,C,C1). - true([],P,C,[P|C]):-!. - true([P|_],P,C,C):-!. - true([not(P)|_],P,_,_):-!,fail. - true([_|T],P,C,C1):-true(T,P,C,C1). - local(false,P,C,C1):- false(C,P,C,C1). - false([],P,C,[not(P)|C]):-!. - false([P|_],P,_,_):-!,fail. - false([not(P)|_],P,C,C):-!. - false([_|T],P,C,C1):-false(T,P,C,C1). itl(@(P),P,more,C,C). % strong next itl(@(_),false,E,C,C):-!,E=empty. itl(?(Cond,T,F),N,E,C,C1):-!, itl(Cond,CN,E,C,C0),itl_cond(CN,T,F,N,E,C0,C1). -itl_cond(true,T,_,N,E,C,C1) :-!, - itl(T,N,E,C,C1). -itl_cond(false,_,F,N,E,C,C1) :-!, - itl(F,N,E,C,C1). -itl_cond(CN,T,F,N,E,C,C1) :-!, - itl(T,TN,E,C,C0), - itl(F,FN,E,C0,C1), negate(CN,NCN), - and(TN,CN,N1),and(FN,NCN,N2), or(N1,N2,N). % Non deterministic selection (singleton 2nd order variable) itl([],true,_,C,C):-!. itl([H|L],F,empty,C,C1):-!, empty_choice([H|L],0,F,C,C1). - empty_choice([H|_],N,F,C,[choice(N)|C1]) :- - itl(H,F,empty,C,C1). - empty_choice([_|L],N,F,C,C1) :- - N1 is N+1, - empty_choice(L,N1,F,C,C1). itl([H|L],F,E,C,C1):-!,E=more, choice([H|L],F,C,C1). - choice([],[],C,C) :-!. - choice([H|L],[H1|L1],C,C2) :- - itl(H,H1,more,C,C1), - choice(L,L1,C1,C2). % Regular Variable itl(^(R),F,empty,C,C1):- local(F,^(R,0),C,C1). @@ -96,41 +69,13 @@ % Quantifier itl(exists(P,Q),F,E,C,C0) :-!, itl(Q,QT,E,[P|C],C1),itl_ex(QT,Q,E,P,F,C1,C0). - itl_ex(true,_,_,P,true,C,C1):-!,remove_p(C,P,C1). - itl_ex(false,Q,E,P,F,C,C0):- !,remove_p(C,P,C1), - itl(Q,QF,E,[not(P)|C1],C2),remove_p(C2,P,C0), exists(QF,P,F). - itl_ex(QT,Q,E,P,F,C,C0):- remove_p(C,P,C1), - itl(Q,QF,E,[not(P)|C1],C2), remove_p(C2,P,C0), - or(QT,QF,TF),exists(TF,P,F). - % constant order optimzation for quantifier - exists(P,P,true):-!. - exists(P,_,P):-atomic(P),!. - exists(Q,P,exists(P,Q)). - remove_p([],_,[]):-!. - remove_p([not(P)|T],P,T):-!. - remove_p([P|T],P,T):-!. - remove_p([H|T],P,[H|T1]):-!,remove_p(T,P,T1). itl(*(P),F,empty,C,C1):-!,itl(P,F,empty,C,C1). itl(*(P),F,E,C,C1):-!,E=more, itl(P,PX,more,C,C1), closure(PX,P,F). - closure(false,_,false):-!. - closure(PX,P,(PX & *(P))). %% infinite clousre (strong) -%% closure(PX,P,(PX & (*(P);empty))). %% finite closure (weak) %% external state diagram itl(st(N),F,E,C,C1):-!, setof((Cond=>X),st(N,Cond,X),L),itl_transition(L,F,E,C,C1). - itl_transition([],false,_,C,C):-!. - itl_transition([(Cond=>empty)|T],F,E,C,C1):-!, - itl((empty,Cond),F0,E,C,C0), - itl_transition(T,F1,E,C0,C1),or(F0,F1,F). - itl_transition([(Cond=>X)|T],F,E,C,C1):- - itl((more,Cond),F0,E,C,C0), - itl_transition1(F0,X,T,F,E,C0,C1). - itl_transition1(false,_,T,F,E,C,C1):- - itl_transition(T,F,E,C,C1). - itl_transition1(true,X,T,(st(X);F),E,C,C1):- - itl_transition(T,F,E,C,C1). %% ignore last state to check non stop predicate itl(non_terminate(_),F,empty,C,C):-!,F=true. itl(non_terminate(L),F,more,C,C1):-!, @@ -140,29 +85,11 @@ exclusive(L,C,C1,true,F). itl(share(L),F,more,C,C1):-!, exclusive(L,C,C1,share(L),F). - exclusive([],C,C,F,F):-!. - exclusive([A|L],C,C1,F,F1):- - true(C,A,C,C0),exclusive1(L,C0,C1,F,F1). - exclusive([N|L],C,C1,F,F1):- - false(C,N,C,C0), !,exclusive(L,C0,C1,F,F1). -% exclusive(_,C,C,_,false). % eliminate this brach - exclusive1([],C,C,F,F):-!. - exclusive1([H|L],C,C1,F,F1):- - false(C,H,C,C0), !,exclusive1(L,C0,C1,F,F1). -% exclusive1(_,C,C,_,false). %% itl((P,Q),N,E,C,C1) :-!, itl(P,PN,E,C,C0),itland(PN,Q,N,E,C0,C1). -itland(false,_,false,_,C0,C0):-!. -itland(true,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1). -itland(PN,Q,N,E,C0,C1):- - itl(Q,QN,E,C0,C1),and(PN,QN,N). %% and/3 in chop.pl itl((P;Q),N,E,C,C1) :-!, itl(P,PN,E,C,C0),itlor(PN,Q,N,E,C0,C1). -itlor(true,_,true,_,C0,C0):-!. -itlor(false,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1). -itlor(PN,Q,N,E,C0,C1):- - itl(Q,QN,E,C0,C1),or(PN,QN,N). %% or/3 in chop.pl itl(not(P),NN,E,X,X1) :- !, itl(P,N,E,X,X1), negate(N,NN). %% negate/2 in chop.pl @@ -173,7 +100,98 @@ itl(P,PE,empty,C,C0), itl(P,PM,more,C0,C1), chop(PM,PE,F,Q,C1,C2). +itl(proj(_,Q),F,empty,C,C1) :-!, + itl(Q,F,empty,C,C1). +itl(proj(P,Q),F,more,C,C1) :-!, + itl(P,PM,more,C,C0), + itl(Q,QM,more,C0,C1), + prj(PM,QM,P,F). +% prefix is not consistently defined +% prefix(fin(false)) = true ? funny... +itl(prefix(P),F,empty,C,C1) :-!, + itl(P,PE,empty,C,C0), + itl(P,PM,more,C0,C1), + prefix(PM,PE,F). +itl(prefix(P),F,more,C,C1) :-!, + itl(P,PM,more,C,C1), + prefix(PM,F). +itl(Def,_,_,_,_) :- + write('error: '),write(Def),nl,!,fail. + +local(true,P,C,C1):- true(C,P,C,C1). +local(false,P,C,C1):- false(C,P,C,C1). +true([],P,C,[P|C]):-!. +true([P|_],P,C,C):-!. +true([not(P)|_],P,_,_):-!,fail. +true([_|T],P,C,C1):-true(T,P,C,C1). +false([],P,C,[not(P)|C]):-!. +false([P|_],P,_,_):-!,fail. +false([not(P)|_],P,C,C):-!. +false([_|T],P,C,C1):-false(T,P,C,C1). +empty_choice([H|_],N,F,C,[choice(N)|C1]) :- + itl(H,F,empty,C,C1). +empty_choice([_|L],N,F,C,C1) :- + N1 is N+1, + empty_choice(L,N1,F,C,C1). +choice([],[],C,C) :-!. +choice([H|L],[H1|L1],C,C2) :- + itl(H,H1,more,C,C1), + choice(L,L1,C1,C2). +itl_cond(true,T,_,N,E,C,C1) :-!, + itl(T,N,E,C,C1). +itl_cond(false,_,F,N,E,C,C1) :-!, + itl(F,N,E,C,C1). +itl_cond(CN,T,F,N,E,C,C1) :-!, + itl(T,TN,E,C,C0), + itl(F,FN,E,C0,C1), negate(CN,NCN), + and(TN,CN,N1),and(FN,NCN,N2), or(N1,N2,N). +itl_ex(true,_,_,P,true,C,C1):-!,remove_p(C,P,C1). +itl_ex(false,Q,E,P,F,C,C0):- !,remove_p(C,P,C1), + itl(Q,QF,E,[not(P)|C1],C2),remove_p(C2,P,C0), exists(QF,P,F). +itl_ex(QT,Q,E,P,F,C,C0):- remove_p(C,P,C1), + itl(Q,QF,E,[not(P)|C1],C2), remove_p(C2,P,C0), + or(QT,QF,TF),exists(TF,P,F). +% constant order optimzation for quantifier +exists(P,P,true):-!. +exists(P,_,P):-atomic(P),!. +exists(Q,P,exists(P,Q)). +remove_p([],_,[]):-!. +remove_p([not(P)|T],P,T):-!. +remove_p([P|T],P,T):-!. +remove_p([H|T],P,[H|T1]):-!,remove_p(T,P,T1). +closure(false,_,false):-!. +closure(PX,P,(PX & *(P))). %% infinite clousre (strong) +%% closure(PX,P,(PX & (*(P);empty))). %% finite closure (weak) +itl_transition([],false,_,C,C):-!. +itl_transition([(Cond=>empty)|T],F,E,C,C1):-!, + itl((empty,Cond),F0,E,C,C0), + itl_transition(T,F1,E,C0,C1),or(F0,F1,F). +itl_transition([(Cond=>X)|T],F,E,C,C1):- + itl((more,Cond),F0,E,C,C0), + itl_transition1(F0,X,T,F,E,C0,C1). +itl_transition1(false,_,T,F,E,C,C1):- + itl_transition(T,F,E,C,C1). +itl_transition1(true,X,T,(st(X);F),E,C,C1):- + itl_transition(T,F,E,C,C1). +exclusive([],C,C,F,F):-!. +exclusive([A|L],C,C1,F,F1):- + true(C,A,C,C0),exclusive1(L,C0,C1,F,F1). +exclusive([N|L],C,C1,F,F1):- + false(C,N,C,C0), !,exclusive(L,C0,C1,F,F1). +% exclusive(_,C,C,_,false). % eliminate this brach +exclusive1([],C,C,F,F):-!. +exclusive1([H|L],C,C1,F,F1):- + false(C,H,C,C0), !,exclusive1(L,C0,C1,F,F1). +% exclusive1(_,C,C,_,false). +itland(false,_,false,_,C0,C0):-!. +itland(true,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1). +itland(PN,Q,N,E,C0,C1):- + itl(Q,QN,E,C0,C1),and(PN,QN,N). %% and/3 in chop.pl +itlor(true,_,true,_,C0,C0):-!. +itlor(false,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1). +itlor(PN,Q,N,E,C0,C1):- + itl(Q,QN,E,C0,C1),or(PN,QN,N). %% or/3 in chop.pl chop(false,false,false,_,C,C):-!. chop(PM,false,(PM & Q),Q,C,C):-!. chop(PM,true,F,Q,C,C1):-!, @@ -191,25 +209,10 @@ chop1(_,true,_,true):-!. chop1(PM,QF,Q,(QF;(PM&Q))):-!. -itl(proj(_,Q),F,empty,C,C1) :-!, - itl(Q,F,empty,C,C1). -itl(proj(P,Q),F,more,C,C1) :-!, - itl(P,PM,more,C,C0), - itl(Q,QM,more,C0,C1), - prj(PM,QM,P,F). prj(false,_,_,false):-!. prj(_,false,_,false):-!. prj(PM,QM,P,(PM&proj(P,QM))). -% prefix is not consistently defined -% prefix(fin(false)) = true ? funny... -itl(prefix(P),F,empty,C,C1) :-!, - itl(P,PE,empty,C,C0), - itl(P,PM,more,C0,C1), - prefix(PM,PE,F). -itl(prefix(P),F,more,C,C1) :-!, - itl(P,PM,more,C,C1), - prefix(PM,F). prefix(true,true):-!. prefix(false,false):-!. @@ -220,9 +223,6 @@ prefix(false,false,false):-!. prefix(_,false,true):-!. -itl(Def,_,_,_,_) :- - write('error: '),write(Def),nl,!,fail. - % develop Local ITL formula into state diagram % diff -r a6adedccd5f6 -r e1d3145cff7a ex.pl --- a/ex.pl Sun Jan 21 10:21:43 2001 +0900 +++ b/ex.pl Thu Aug 30 12:44:35 2007 +0900 @@ -74,7 +74,7 @@ % shared resources '[]'( ~ ( ar, bl)), '[]'( ~ ( br, cl)), '[]'( ~ ( cr, dl)), '[]'( ~ ( dr, el)), '[]'( ~ ( er, al)) -)):-fail. % too big to verify (sigh...) +)). % :-fail. % too big to verify (sigh...) ex(21,(more, share([ar,bl]),share([br,cl]),share([cr,dl]), @@ -84,7 +84,7 @@ *( ((true && '[]'(cl) && '[]'((cl,cr)) && '[]'(cr));empty) ) , *( ((true && '[]'(dl) && '[]'((dl,dr)) && '[]'(dr));empty) ) , *( ((true && '[]'(el) && '[]'((el,er)) && '[]'(er));empty) ) , -true)):-fail. % too big to verify (sigh...) +true)). % :-fail. % too big to verify (sigh...) ex(22,(more, % three philosophers with no iteration @@ -114,6 +114,62 @@ ex(110,(more-> (more&more))). % our dense time ex(demo(X),Y) :- demo(X,Y). +% Regular variable examples ( doesnot work now....) + +ex(200,^r). +ex(201,true & ^r). % will terminate? +ex(202,((^r & ^r),not(^r))). % is non-local? +ex(203,(^r,length(4))). % distinguish different state? +ex(204,('[a]'(^r))). % non-deterministic? +ex(205,('[a]'(^r = length(2)))). % imitate length? +ex(206,('[a]'(^r = length(4)),(^r& ^r))). +ex(207,('[a]'(^r = (length(4);empty)),* ^r)). +ex(208,('[]'(^r = ( + a,@ ^r; + not(a),c,@ @ ^r; + not(a),not(c),b,empty)),^r)). % RE +ex(209,('[a]'(^r = ( + a,@((^r & @((b,empty)))) ; + not(a),b,empty)), + ^r)). % CFG + +% Linear Time Axioms, valid in ITL +ex(210,('[]'((^a-> ^b)) -> ('[]'(^a) -> '[]'(^b)))). % K +ex(211,('[]'(((^a , '[]'(^a))-> ^b));'[]'(((^b , '[]'(^b))-> ^a)))). % 4 +ex(212,('[]'(^a)-> '<>'(^a))). % D +ex(213,('[]'(^a)-> '[]'('[]'(^a)))). % L +ex(214,(('[]'(^a))-> ^a)). % T +% Diodorean discreteness +ex(215,('[]'('[]'((((^a-> '[]'(^a)))-> ^a))) -> ((('<>'('[]'(^a)))-> '[]'(^a))))). +% Linear Time Axioms, not valid in ITL +% Z discreteness +ex(216,('[]'(('[]'(^a)-> ^a))-> ((('<>'('[]'(^a)))-> '[]'(^a))))). +% W weak density +ex(217,('[]'(('[]'(^a)-> ^a))-> ('[]'(^a)))). +% Other Axioms, not v^alid in ITL +ex(218,(^a-> '[]'('<>'(^a)))). % B +ex(219,(('<>' ^a)-> '[]'('<>'(^a)))). % 5 + +% State Diagram Support + +ex(300,(((length(2), @ '<>'(q)) proj true), + st(ns0) + )) :- ensure_loaded(kiss_ex). + +% Infinite Interval + +ex(400,infinite). +ex(401,*infinite). +ex(402,*skip). +ex(403,*length(5)). +ex(404,~('<>'(empty))). +ex(405,('<>'(empty))). % unsatisfiable +ex(406,(infinite-> @infinite)). +ex(407,((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6))))). +ex(408,(infinite -> ~(<>([](p)) = [](<>(p))))). % satisfiable +ex(409,finite). % unsatisfiable + + demo(X) :- number(X),demo(X,ITL),nl,ex(ITL),nl,write(ITL). % length 5 interval @@ -211,61 +267,5 @@ '[]'(not((c,a))) )). -% Regular variable examples ( doesnot work now....) - -ex(200,^r). -ex(201,true & ^r). % will terminate? -ex(202,((^r & ^r),not(^r))). % is non-local? -ex(203,(^r,length(4))). % distinguish different state? -ex(204,('[a]'(^r))). % non-deterministic? -ex(205,('[a]'(^r = length(2)))). % imitate length? -ex(206,('[a]'(^r = length(4)),(^r& ^r))). -ex(207,('[a]'(^r = (length(4);empty)),* ^r)). -ex(208,('[]'(^r = ( - a,@ ^r; - not(a),c,@ @ ^r; - not(a),not(c),b,empty)),^r)). % RE -ex(209,('[a]'(^r = ( - a,@((^r & @((b,empty)))) ; - not(a),b,empty)), - ^r)). % CFG - -% Linear Time Axioms, valid in ITL -ex(210,('[]'((^a-> ^b)) -> ('[]'(^a) -> '[]'(^b)))). % K -ex(211,('[]'(((^a , '[]'(^a))-> ^b));'[]'(((^b , '[]'(^b))-> ^a)))). % 4 -ex(212,('[]'(^a)-> '<>'(^a))). % D -ex(213,('[]'(^a)-> '[]'('[]'(^a)))). % L -ex(214,(('[]'(^a))-> ^a)). % T -% Diodorean discreteness -ex(215,('[]'('[]'((((^a-> '[]'(^a)))-> ^a))) -> ((('<>'('[]'(^a)))-> '[]'(^a))))). -% Linear Time Axioms, not valid in ITL -% Z discreteness -ex(216,('[]'(('[]'(^a)-> ^a))-> ((('<>'('[]'(^a)))-> '[]'(^a))))). -% W weak density -ex(217,('[]'(('[]'(^a)-> ^a))-> ('[]'(^a)))). -% Other Axioms, not v^alid in ITL -ex(218,(^a-> '[]'('<>'(^a)))). % B -ex(219,(('<>' ^a)-> '[]'('<>'(^a)))). % 5 - -% State Diagram Support - -ex(300,(((length(2), @ '<>'(q)) proj true), - st(ns0) - )) :- ensure_loaded(kiss_ex). - -% Infinite Interval - -ex(400,infinite). -ex(401,*infinite). -ex(402,*skip). -ex(403,*length(5)). -ex(404,~('<>'(empty))). -ex(405,('<>'(empty))). % unsatisfiable -ex(406,(infinite-> @infinite)). -ex(407,((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6))))). -ex(408,(infinite -> ~(<>([](p)) = [](<>(p))))). % satisfiable -ex(409,finite). % unsatisfiable - - /* end */ diff -r a6adedccd5f6 -r e1d3145cff7a gi_ex.pl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/gi_ex.pl Thu Aug 30 12:44:35 2007 +0900 @@ -0,0 +1,16 @@ +% +% specification for simple graphics interaction +% + +gi_ex(( ++(((stop,keep((red,not(start)));start,keep((green,not(stop)))))), +[]((red,not(green);not(red),green)), +[]((green->move)), +[]((red->not(move))), +halt(quit) +)) :- + asserta(lite:st_variables([stop,start,quit],[red,gree,move])). + +gi:-gi_ex(X),write(X),nl,lite:ex(X),nl,lite:tgen. + +giout :- gi_ex(X),lite:ex(X),tell('gi.tokio'),lite:tgen,told. diff -r a6adedccd5f6 -r e1d3145cff7a kiss.pl --- a/kiss.pl Sun Jan 21 10:21:43 2001 +0900 +++ b/kiss.pl Thu Aug 30 12:44:35 2007 +0900 @@ -194,21 +194,22 @@ read_kiss_header(C,C2,IL,OL) :-[C]=".",!, get(C0), read_kiss_header1(C0,C1,IL,OL), read_kiss_header(C1,C2,IL,OL). - read_kiss_header1(C,C2,IL,_OL):-[C]="i",!,get(C0), - read_number(C0,C1,IL),skip_line(C1,C2). - read_kiss_header1(C,C2,_IL,OL):-[C]="o",!,get(C0), - read_number(C0,C1,OL),skip_line(C1,C2). - read_kiss_header1(C,C1,_,_):-[C]="p",!, - skip_line(C,C1). - read_kiss_header1(C,C1,_,_):-[C]="s",!, - skip_line(C,C1). - read_kiss_header1(C,C1,_,_):- - skip_line(C,C1). read_kiss_header(C,C,_,_) :-([C]="0";[C]="1";[C]="-"),!. read_kiss_header(C,C1,IL,OL) :- skip_line(C,C0), read_kiss_header(C0,C1,IL,OL). +read_kiss_header1(C,C2,IL,_OL):-[C]="i",!,get(C0), + read_number(C0,C1,IL),skip_line(C1,C2). +read_kiss_header1(C,C2,_IL,OL):-[C]="o",!,get(C0), + read_number(C0,C1,OL),skip_line(C1,C2). +read_kiss_header1(C,C1,_,_):-[C]="p",!, + skip_line(C,C1). +read_kiss_header1(C,C1,_,_):-[C]="s",!, + skip_line(C,C1). +read_kiss_header1(C,C1,_,_):- + skip_line(C,C1). + read_kiss_body(-1,_,_,_) :-!. read_kiss_body(C,In,Out,Emode) :- ([C]="0";[C]="1";[C]="-"),!, diff -r a6adedccd5f6 -r e1d3145cff7a lite.pl --- a/lite.pl Sun Jan 21 10:21:43 2001 +0900 +++ b/lite.pl Thu Aug 30 12:44:35 2007 +0900 @@ -34,7 +34,7 @@ %?-op(60,fy,[*]). ?-[op]. % :- use_module(library(gmlib)). -:- ensure_loaded([dvcomp,rstd,chop,diag,kiss,ex,cp,infinite]). +:- ensure_loaded([dvcomp,rstd,chop,diag,kiss,ex,cp]). % ,display]). % end diff -r a6adedccd5f6 -r e1d3145cff7a liter.pl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/liter.pl Thu Aug 30 12:44:35 2007 +0900 @@ -0,0 +1,39 @@ +% Sat May 22 11:43:11 JST 1993 + +:- module(lite,[ + ex/1, % ex(ITL) verification predicate + ex/2, % ex(No,Example) + diag/1,diag/0, % find counter example + exe/1, exe/0, % find sample execution + verbose/1, % verbose mode (default on) + renaming/1, % 2var renaming mode (default on) + singleton/1, % singleton removal mode (default on) + detail/1, % detailed trace of 2var + set_limit/1, % 2var state limit + lazy/1, % lazy mode (dvcomp only) + kiss/0, % kiss format geneartion + read_kiss/1, % read KISS2 format + read_kiss/4, % read KISS2 format + read_kiss/3, % read KISS2 format + tgen/0, % tokio clause geneartion + itl/1, % one step tableau expansion + itl/3, % " in detail + itl_statistics/0, % show number of state etc. + st/3, % external state machine + st_variables/2, % its variables + sbterm/0, % show sub term/ state database + display/0, large/0, small/0, % show state database + start/0, display_diag/1, display_exe/1, + state/0 % show state database +]). + +%?-op(900,xfy,[(&),('&&')]). +%?-op(700,xfy,['<->','\=',proj]). +%?-op(60,fy,['~','#','<>', '@',^]). +%?-op(60,fy,[*]). +?-[op]. +% :- use_module(library(gmlib)). +:- ensure_loaded([dvcomp,rstd,chop,diag,kiss,ex,cp]). +% ,display]). + +% end diff -r a6adedccd5f6 -r e1d3145cff7a problems --- a/problems Sun Jan 21 10:21:43 2001 +0900 +++ b/problems Thu Aug 30 12:44:35 2007 +0900 @@ -1,3 +1,49 @@ +Sun Feb 10 21:30:04 JST 2002 + +あ、そうだよ。empty は、どうすんだ? kiss の時は、無視したんだが... + +そもそも、2nd order を入れたおかげで、複雑になりすぎ。 + +もう一度 simple なversion を作るべきだよね。 + +状態生成を再利用できる形で。 + +対称性 general abstraction + +Thu Feb 7 12:12:21 JST 2002 + +Verlog output for Prof. Fujita + +switch でもいいんだけど、ちょっと巨大にならない? + +module check001(clk,inputs..,outputs...) +input clk; +input inputs; +output outputs; +reg state; +initial state = 0; + always @(posedge clk) begin + case (state) + 0: if (inputs condtion) begin + outputs set + end else if (inputs condtion) begin + outputs set + ... + end + endcase + end +endmodule + +ってな感じ? + +やっぱり、状態をcubeのような形で生成するのは、良くないよね。 + ?(a,@a,@b) +みたいな形で、生成した方が扱いやすい。ま、それは、Java Version +で。 + +特性方程式を生成する方が良い? BDD の末端が各状態にいくようにする。 +それは、あんまり良くないか... + Sun Jan 21 00:42:39 JST 2001 あれ? やっぱり、なんか変だな。 diff -r a6adedccd5f6 -r e1d3145cff7a rstd.pl --- a/rstd.pl Sun Jan 21 10:21:43 2001 +0900 +++ b/rstd.pl Thu Aug 30 12:44:35 2007 +0900 @@ -135,78 +135,12 @@ sbdt(P,F,L,L) :- atomic(P),!,F= ?(P,true,false). sbdt(?(C,T,F),?(C,T,F),L,L) :- !. % already done. sbdt(not(P),F,L,L1) :- !,sbdt(P,F0,L,L0),sbdt_not(F0,F,L0,L1),!. - sbdt_not(true,false,L,L). - sbdt_not(false,true,L,L). - sbdt_not(true_false,true_false,L,L). - sbdt_not(F,?(H,A1,B1),L,L1):- - arg(1,F,H),arg(2,F,A),arg(3,F,B), - sbdt_not(A,A1,L,L0),sbdt_not(B,B1,L0,L1). sbdt((P,Q),F,L,L2) :- !, sbdt(P,P0,L,L0),sbdt(Q,Q0,L0,L1), sbdt_and(P0,Q0,F,L1,L2),!. - sbdt_and(false,_,false,L,L):-!. - sbdt_and(_,false,false,L,L):-!. - sbdt_and(true,T,T,L,L):-!. - sbdt_and(T,true,T,L,L):-!. - sbdt_and(T,T1,T1,L,L):- atomic(T),T=T1,!. - sbdt_and(?(PF,P0,P1),true_false,F,L,L1):-!, - sbdt_and(P0,true_false,R0,L,L0), - sbdt_and(P1,true_false,R1,L0,L1), - sbdt_opt(PF,R0,R1,F). - sbdt_and(true_false,?(PF,P0,P1),F,L,L1):-!, - sbdt_and(P0,true_false,R0,L,L0), - sbdt_and(P1,true_false,R1,L0,L1), - sbdt_opt(PF,R0,R1,F). - sbdt_and(P,Q,R,L,L1) :-!, - arg(1,P,PF),arg(1,Q,QF), - sbdt_and(PF,QF,P,Q,R,L,L1). - sbdt_and(PF,QF,P,Q,R,L,L1):-PF @< QF,!, - sbdt_and(QF,PF,Q,P,R,L,L1). - sbdt_and(PF,QF,P,Q,F,L,L1):-PF @> QF,!, - arg(2,Q,Q0),arg(3,Q,Q1), - sbdt_and(Q0,P,R0,L,L0), - sbdt_and(Q1,P,R1,L0,L1), - sbdt_opt(QF,R0,R1,F). - sbdt_and(PF,PF,P,Q,F,L,L1):- - arg(2,P,P0),arg(3,P,P1), - arg(2,Q,Q0),arg(3,Q,Q1), - sbdt_and(P0,Q0,R0,L,L0), - sbdt_and(P1,Q1,R1,L0,L1), - sbdt_opt(PF,R0,R1,F). sbdt((P;Q),F,L,L2) :- !, sbdt(P,P0,L,L0),sbdt(Q,Q0,L0,L1), sbdt_or(P0,Q0,F,L1,L2),!. - sbdt_or(true,_,true,L,L):-!. - sbdt_or(_,true,true,L,L):-!. - sbdt_or(false,T,T,L,L):-!. - sbdt_or(T,false,T,L,L):-!. - sbdt_or(T,T1,T1,L,L):- atomic(T),T=T1,!. - sbdt_or(?(PF,P0,P1),true_false,F,L,L1):-!, - sbdt_or(P0,true_false,R0,L,L0), - sbdt_or(P1,true_false,R1,L0,L1), - sbdt_opt(PF,R0,R1,F). - sbdt_or(true_false,?(PF,P0,P1),F,L,L1):-!, - sbdt_or(P0,true_false,R0,L,L0), - sbdt_or(P1,true_false,R1,L0,L1), - sbdt_opt(PF,R0,R1,F). - sbdt_or(P,Q,R,L,L1) :-!, - arg(1,P,PF),arg(1,Q,QF), - sbdt_or(PF,QF,P,Q,R,L,L1). - sbdt_or(PF,QF,P,Q,R,L,L1):-PF @< QF,!, - sbdt_or(QF,PF,Q,P,R,L,L1). - sbdt_or(PF,QF,P,Q,F,L,L1):-PF @> QF,!, - arg(2,Q,Q0),arg(3,Q,Q1), - sbdt_or(Q0,P,R0,L,L0), - sbdt_or(Q1,P,R1,L0,L1), - sbdt_opt(QF,R0,R1,F). - sbdt_or(PF,PF,P,Q,F,L,L1):- - arg(2,P,P0),arg(3,P,P1), - arg(2,Q,Q0),arg(3,Q,Q1), - sbdt_or(P0,Q0,R0,L,L0), - sbdt_or(P1,Q1,R1,L0,L1), - sbdt_opt(PF,R0,R1,F). - sbdt_opt(_IF,THEN,ELSE,THEN) :- THEN==ELSE,!. - sbdt_opt(IF,THEN,ELSE,?(IF,THEN,ELSE)). sbdt((P&Q), N,(U,V,D),(U,V2,D2)) :-!, sbdt(P,P1,([],V,D),(U1,V1,D1)), sbdt(Q,Q1,([],V1,D1),(U2,V2,D2)), @@ -228,11 +162,6 @@ sbdt(^(R), ?(^(R),true,false),L,L) :-!. sbdt(Rg, ?(Rg,true,false),(U,V,D),(U1,V1,D1)) :- Rg = ^(_,_),!, sbdt_r(Rg,U,V,D,U1,V1,D1). - sbdt_r(Rg,U,V,D,U,V,D) :- - member(Rg,U),!. % in the same formula - sbdt_r(Rg,U,V,D,[Rg|U],V,[Rg|D]) :- - member(Rg,V),!. % duplicate - sbdt_r(Rg,U,V,D,[Rg|U],[Rg|V],D). % new % Simple Functor sbdt(Func,N,(U,V,D),(U,V1,D1)) :- functor(Func,H,1),!, arg(1,Func,A), @@ -247,6 +176,78 @@ sbdt(Def,true,L,L) :- write('bdtstd error: '),write(Def),nl. +sbdt_not(true,false,L,L). +sbdt_not(false,true,L,L). +sbdt_not(true_false,true_false,L,L). +sbdt_not(F,?(H,A1,B1),L,L1):- + arg(1,F,H),arg(2,F,A),arg(3,F,B), + sbdt_not(A,A1,L,L0),sbdt_not(B,B1,L0,L1). +sbdt_and(false,_,false,L,L):-!. +sbdt_and(_,false,false,L,L):-!. +sbdt_and(true,T,T,L,L):-!. +sbdt_and(T,true,T,L,L):-!. +sbdt_and(T,T1,T1,L,L):- atomic(T),T=T1,!. +sbdt_and(?(PF,P0,P1),true_false,F,L,L1):-!, + sbdt_and(P0,true_false,R0,L,L0), + sbdt_and(P1,true_false,R1,L0,L1), + sbdt_opt(PF,R0,R1,F). +sbdt_and(true_false,?(PF,P0,P1),F,L,L1):-!, + sbdt_and(P0,true_false,R0,L,L0), + sbdt_and(P1,true_false,R1,L0,L1), + sbdt_opt(PF,R0,R1,F). +sbdt_and(P,Q,R,L,L1) :-!, + arg(1,P,PF),arg(1,Q,QF), + sbdt_and(PF,QF,P,Q,R,L,L1). +sbdt_and(PF,QF,P,Q,R,L,L1):-PF @< QF,!, + sbdt_and(QF,PF,Q,P,R,L,L1). +sbdt_and(PF,QF,P,Q,F,L,L1):-PF @> QF,!, + arg(2,Q,Q0),arg(3,Q,Q1), + sbdt_and(Q0,P,R0,L,L0), + sbdt_and(Q1,P,R1,L0,L1), + sbdt_opt(QF,R0,R1,F). +sbdt_and(PF,PF,P,Q,F,L,L1):- + arg(2,P,P0),arg(3,P,P1), + arg(2,Q,Q0),arg(3,Q,Q1), + sbdt_and(P0,Q0,R0,L,L0), + sbdt_and(P1,Q1,R1,L0,L1), + sbdt_opt(PF,R0,R1,F). +sbdt_or(true,_,true,L,L):-!. +sbdt_or(_,true,true,L,L):-!. +sbdt_or(false,T,T,L,L):-!. +sbdt_or(T,false,T,L,L):-!. +sbdt_or(T,T1,T1,L,L):- atomic(T),T=T1,!. +sbdt_or(?(PF,P0,P1),true_false,F,L,L1):-!, + sbdt_or(P0,true_false,R0,L,L0), + sbdt_or(P1,true_false,R1,L0,L1), + sbdt_opt(PF,R0,R1,F). +sbdt_or(true_false,?(PF,P0,P1),F,L,L1):-!, + sbdt_or(P0,true_false,R0,L,L0), + sbdt_or(P1,true_false,R1,L0,L1), + sbdt_opt(PF,R0,R1,F). +sbdt_or(P,Q,R,L,L1) :-!, + arg(1,P,PF),arg(1,Q,QF), + sbdt_or(PF,QF,P,Q,R,L,L1). +sbdt_or(PF,QF,P,Q,R,L,L1):-PF @< QF,!, + sbdt_or(QF,PF,Q,P,R,L,L1). +sbdt_or(PF,QF,P,Q,F,L,L1):-PF @> QF,!, + arg(2,Q,Q0),arg(3,Q,Q1), + sbdt_or(Q0,P,R0,L,L0), + sbdt_or(Q1,P,R1,L0,L1), + sbdt_opt(QF,R0,R1,F). +sbdt_or(PF,PF,P,Q,F,L,L1):- + arg(2,P,P0),arg(3,P,P1), + arg(2,Q,Q0),arg(3,Q,Q1), + sbdt_or(P0,Q0,R0,L,L0), + sbdt_or(P1,Q1,R1,L0,L1), + sbdt_opt(PF,R0,R1,F). +sbdt_opt(_IF,THEN,ELSE,THEN) :- THEN==ELSE,!. +sbdt_opt(IF,THEN,ELSE,?(IF,THEN,ELSE)). +sbdt_r(Rg,U,V,D,U,V,D) :- + member(Rg,U),!. % in the same formula +sbdt_r(Rg,U,V,D,[Rg|U],V,[Rg|D]) :- + member(Rg,V),!. % duplicate +sbdt_r(Rg,U,V,D,[Rg|U],[Rg|V],D). % new + or_list([],[],[]):-!. or_list(_,_,[a]):-!. @@ -378,11 +379,12 @@ sbdt_unify(F,F1) :- functor(F,H,N),functor(F1,H,N),!, sbdt_unify_arg(N,N,F,F1). - sbdt_unify_arg(0,_,_,_) :- !. - sbdt_unify_arg(N,N1,F,F0) :- - N0 is N-1, - arg(N,F,A),arg(N,F0,A0), - sbdt_unify(A,A0),sbdt_unify_arg(N0,N1,F,F0). + +sbdt_unify_arg(0,_,_,_) :- !. +sbdt_unify_arg(N,N1,F,F0) :- + N0 is N-1, + arg(N,F,A),arg(N,F0,A0), + sbdt_unify(A,A0),sbdt_unify_arg(N0,N1,F,F0). sbterm :- listing(sb/2),listing(itl_state/2). @@ -394,22 +396,22 @@ bdt2itl(?(IF,THEN,ELSE),F) :-!, bdt2itl(IF,IF0),bdt2itl(THEN,THEN0),bdt2itl(ELSE,ELSE0), bdt2itl_opt(IF0,THEN0,ELSE0,F). -% little more readable representation - bdt2itl_opt(IF,true,false,IF) :- !. - bdt2itl_opt(IF,false,true,not(IF)) :- !. - bdt2itl_opt(IF,true,ELSE,(IF;ELSE)) :- !. - bdt2itl_opt(IF,THEN,false,(IF,THEN)) :- !. - bdt2itl_opt(IF,false,ELSE,(not(IF);ELSE)) :- !. - bdt2itl_opt(IF,THEN,true,(not(IF),THEN)) :- !. - bdt2itl_opt(IF,THEN,ELSE,?(IF,THEN,ELSE)) :- !. bdt2itl(B,F) :- atom(B),!,F=B. bdt2itl(B,F) :- functor(B,H,N),functor(F,H,N),bdt2itl_subterm(N,N,B,F). - bdt2itl_subterm(0,_,_,_) :- !. - bdt2itl_subterm(N,N1,F,F0) :- - N0 is N-1, - arg(N,F,A),arg(N,F0,A0), - bdt2itl(A,A0),bdt2itl_subterm(N0,N1,F,F0). +% little more readable representation +bdt2itl_opt(IF,true,false,IF) :- !. +bdt2itl_opt(IF,false,true,not(IF)) :- !. +bdt2itl_opt(IF,true,ELSE,(IF;ELSE)) :- !. +bdt2itl_opt(IF,THEN,false,(IF,THEN)) :- !. +bdt2itl_opt(IF,false,ELSE,(not(IF);ELSE)) :- !. +bdt2itl_opt(IF,THEN,true,(not(IF),THEN)) :- !. +bdt2itl_opt(IF,THEN,ELSE,?(IF,THEN,ELSE)) :- !. +bdt2itl_subterm(0,_,_,_) :- !. +bdt2itl_subterm(N,N1,F,F0) :- + N0 is N-1, + arg(N,F,A),arg(N,F0,A0), + bdt2itl(A,A0),bdt2itl_subterm(N0,N1,F,F0). % BDT end % diff -r a6adedccd5f6 -r e1d3145cff7a verilog.pl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/verilog.pl Thu Aug 30 12:44:35 2007 +0900 @@ -0,0 +1,142 @@ +/* + Copyright (C) 2002, Shinji Kono, University of the Ryukyus + PRESTO21 + + Everyone is permitted to copy and distribute verbatim copies + of this license, but changing it is not allowed. You can also + use this wording to make the terms for other programs. + + send your comments to kono@ie.u-ryukyu.ac.jp + $Id$ +*/ + +:- dynamic st_variables/2. + +% already in kiss.pl +set_verilog_var(In) :- + variable_list(L), + (retract(st_variables(_));true),!, + assert(st_variables(In,L)). + +/* +module check001(clk,inputs..,outputs...) +input clk; +input inputs; +output outputs; +reg outputs; +reg state; +initial state = 0; + always @(posedge clk) begin + case (state) + 0: if (inputs condtion) begin + outputs set + end else if (inputs condtion) begin + outputs set + ... + end + endcase + end +endmodule + */ + +verilog(File) :- + tell(File), + verilog, + told. + +verilog :- + write('module check001(clk,'), + (variable_list(L);L=[]), + (st_variables(In,_);In=[]), + delete(L,In,Out), + write_verilog_var_list(L), + write(')'),nl,write('input clk,'),nl, + write_verilog_var_list(In), + write(';'),nl,write('output '),nl, + write_verilog_var_list(Out), + write(';'),nl,write('reg '),nl, + write_verilog_var_list(Out), + write(';'),nl,write('initial state = 0;'),nl, + write(' always @(posedge clk) begin'),nl, + write(' case (state)'),nl, + verilog(In,Out), + write(' endcase'),nl, + write(' end'),nl, + write('endmodule'),nl. + +verilog(In,Out) :- + bagof((D,Cond),(state(S,Cond,D)),L), + write_verilog(S,L,In,Out),fail. +verilog(_,_) :- nl. + +write_verilog_var_list([]):-!. +write_verilog_var_list([H]):-!,write(H). +write_verilog_var_list([H|L]):-!,write(H),put(","), % " " + write_verilog_var_list(L). + +% 0: if jinputs condtion) begin +% outputs set +write_verilog(S,[(D,Cond)|L],In,Out) :- + put(9), write_verilog_state(S),write(' if ('), + write_verilog_cond(Cond,In),write(') begin'),nl, + put(9),write(' '), + write_verilog_output(Cond,D,Out), + nl, + write_verilog(L,In,Out). +% end +% endcase +write_verilog([],_In,_Out) :- + nl,put(9),write(' end'),nl,put(9),write('endcase'),nl,!. +% end else if (inputs condtion) begin +write_verilog([(D,Cond)|L],In,Out) :- + nl,put(9),write(' end else if ('), + write_verilog_cond(Cond,In),write(') begin'),nl, + put(9),write(' '), + write_verilog_output(Cond,D,Out),write(') begin'),nl, + write_verilog(L,In,Out). + +write_verilog_state(true) :-!,fail. +write_verilog_state(false) :- !,fail. +write_verilog_state(S) :- !, + write(S),write(':'). + +write_verilog_cond([],_In) :-!. +write_verilog_cond([not(H)],In) :-member(H,In),!, + put("!"),write(H). +write_verilog_cond([H],In) :-member(H,In),!, + write(H). +write_verilog_cond([not(H)|L],In) :-member(H,In),!, + put("!"),write(H),write('&&'), + write_verilog_cond(L,In). +write_verilog_cond([H|L],In) :-member(H,In),!, + write(H),write('&&'), + write_verilog_cond(L,In). +write_verilog_cond([_H|L],In) :- + write_verilog_cond(L,In). + +write_verilog_output([],D,_Out) :-!, + write('state='), + write_verilog_state(D),put(";"). +write_verilog_output([not(H)|L],D,Out) :-member(H,Out),!, + write(H),write('=0;'), + write_verilog_output(L,D,Out). +write_verilog_output([H|L],D,Out) :-member(H,Out),!, + write(H),write('=1;'), + write_verilog_output(L,D,Out). +write_verilog_output([_H|L],D,Out) :- + write_verilog_output(L,D,Out). + +% delete([],_,[]) :-!. +% delete([H|X],L,Y) :- member(H,L),!,delete(X,L,Y). +% delete([H|X],L,[H|Y]) :- delete(X,L,Y). + +write_verilog_var([],_):-!. +write_verilog_var([H|L],Cond) :- member(H,Cond),!,write(1), + write_verilog_var(L,Cond). +write_verilog_var([H|L],Cond) :- member(not(H),Cond),!,write(0), + write_verilog_var(L,Cond). +write_verilog_var([_|L],Cond) :- write(-), + write_verilog_var(L,Cond). + + +/* end */