changeset 19:e1d3145cff7a lite-verifier

*** empty log message ***
author kono
date Thu, 30 Aug 2007 12:44:35 +0900
parents a6adedccd5f6
children 07d6c4c5654b
files chop.pl cp.pl demo.pl diag.pl disp.pl display.pl dvcomp.pl ex.pl gi_ex.pl kiss.pl lite.pl liter.pl problems rstd.pl verilog.pl
diffstat 15 files changed, 837 insertions(+), 340 deletions(-) [+]
line wrap: on
line diff
--- 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([]):-!.
--- 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).
-
-
- 
--- 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.
--- 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).
--- 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.
--- /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,_,_).
+
+%%
--- 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
 %
--- 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 */
--- /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.
--- 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]="-"),!,
--- 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
--- /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
--- 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
 
 あれ? やっぱり、なんか変だな。
--- 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 %
 
--- /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 */