--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/chop.pl	Thu Jan 18 23:27:24 2001 +0900
@@ -0,0 +1,172 @@
+/*
+ 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.
+
+ send your comments to kono@csl.sony.co.jp
+ $Header$
+*/
+:-dynamic define/2.
+% ITL chop standard form
+% requires ndcomp
+
+def(~(P),not(P)).				% not
+def((P->Q),(not(P);Q)).				% imply
+def(P<->Q,((not(P);Q),(P; not(Q)))).		% equiv
+def(P=Q,((not(P);Q),(P; not(Q)))).		% equiv 
+def((P && Q),((not(empty),P) & Q)).		% strong chop
+def('<>'(Q),(true & Q)).			% sometime
+def('#'(Q), not(true & not(Q))).		% always
+def('[]'(Q), not(true & not(Q))).		% always
+def('[a]'(Q), not(true & not(Q) & true)).	% always with arbitary fin
+def('<a>'(Q), (true & Q & true)).	% sometime with arbitary fin
+def(fin(Q),(true & (empty,Q))).			% final state in the interval
+def(keep(Q), not(true & not((empty ; Q)))).	% except final state
+def(halt(Q), '[]'(empty=Q)).	
+def(more, not(empty)).				% non empty interval
+% discrete stuff
+def(skip, @(empty)).				% 1 length interval
+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))).
+% def(P<=Q,Q=>P).
+% loop stuff and quantifiers
+def(+A ,(A & *((empty;A)))).  % weak closure
+def(while(Cond,Do), *(((Cond->Do) , (~Cond->empty)))).
+def(repeat(Do,until,Cond), (*((Do;empty)) ,@ halt(Cond))).
+def(all(P,Q),not(exists(P,not(Q)))):-!,
+	atomic(P).  % more check is necessary
+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),(
+	*(((P,skip) & skip;empty,P)) & (empty;skip)
+)). 
+def(phil(L,R),
+       +('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) )).
+def(X,Y) :- define(X,Y).
+
+:-dynamic variable/1.
+
+expand(X,Y) :- init_variable,expand1(X,Y).
+
+expand1(V,V) :- var(V),!.
+expand1((P,Q),R) :- !,expand1(P,P1),expand1(Q,Q1),and(P1,Q1,R).
+expand1(st(R),st(R)) :- !,
+	st_variables(In,Out),add_variable(In),add_variable(Out).
+% 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...
+	expand1(Q,Q1).
+expand1(exists(P,Q),exists(P,Q1)):-var(P),!,
+	new_var(P), 
+	expand1(Q,Q1).
+expand1(exists(P,Q),exists(P,Q1)):-!,
+	expand1(Q,Q1).
+expand1([],[]):-!.
+expand1([H|L],?(And,true,?(NAnd,false,true_false))):-!, 
+        % non-deterministic selection
+	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).
+
+% do not use abolish here to avoid erase dynamic property of variable/1
+init_variable :- retract(variable(_)),fail;true.
+add_variable([]):-!.
+add_variable([X|T]) :- !,add_variable(X),add_variable(T).
+add_variable(X) :- variable(X),!.
+add_variable(X) :- assertz(variable(X)),!.
+variable_list(L) :- setof(X,variable(X),L).
+
+new_var(P) :-
+	(retract(sbn(N));N=1),N1 is N+1,asserta(sbn(N1)),!,
+	name(N1,X),S = 95,name(P,[S|X]). % "_"
+
+add_2var(R) :- length_limit(N),!,
+	add_variable(over(R,N)),
+	add_2var(N,R).
+add_2var(R) :-
+	add_variable(^(R)).
+add_2var(0,R):-!,
+	add_variable(^(R,0)).
+add_2var(N,R):- N1 is N-1,
+	add_variable(^(R,N)),
+	add_2var(N1,R).
+
+and(false,_,false):-!.
+and(_,false,false):-!.
+and(true,T,T):-!.
+and(T,true,T):-!.
+and(T,T,T):-!.
+and(A,B,(A,B)):-!.
+
+or(true,_,true):-!.
+or(_,true,true):-!.
+or(false,T,T):-!.
+or(T,false,T):-!.
+or(T,T,T):-!.
+or(A,B,(A;B)):-!. 
+
+negate(true,false):-!.
+negate(false,true):-!.
+negate(true_false,true_false):-!.
+negate(not(N),N):-!.
+negate(N,not(N)):-!.
+
+/* */