2
|
1 /*
|
|
2 Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc.
|
|
3 The University, Newcastle upton Tyne
|
|
4
|
|
5 Everyone is permitted to copy and distribute verbatim copies
|
|
6 of this license, but changing it is not allowed. You can also
|
|
7 use this wording to make the terms for other programs.
|
|
8
|
|
9 send your comments to kono@csl.sony.co.jp
|
22
|
10 $Header: /Users/kono/src/CVS/Lite/chop.pl,v 1.4 2007/08/30 05:16:36 kono Exp $
|
2
|
11 */
|
|
12 :-dynamic define/2.
|
|
13 % ITL chop standard form
|
|
14 % requires ndcomp
|
|
15
|
|
16 def(~(P),not(P)). % not
|
|
17 def((P->Q),(not(P);Q)). % imply
|
|
18 def(P<->Q,((not(P);Q),(P; not(Q)))). % equiv
|
|
19 def(P=Q,((not(P);Q),(P; not(Q)))). % equiv
|
|
20 def((P && Q),((not(empty),P) & Q)). % strong chop
|
|
21 def('<>'(Q),(true & Q)). % sometime
|
|
22 def('#'(Q), not(true & not(Q))). % always
|
|
23 def('[]'(Q), not(true & not(Q))). % always
|
|
24 def('[a]'(Q), not(true & not(Q) & true)). % always with arbitary fin
|
|
25 def('<a>'(Q), (true & Q & true)). % sometime with arbitary fin
|
|
26 def(fin(Q),(true & (empty,Q))). % final state in the interval
|
|
27 def(keep(Q), not(true & not((empty ; Q)))). % except final state
|
|
28 def(halt(Q), '[]'(empty=Q)).
|
|
29 def(more, not(empty)). % non empty interval
|
|
30 % discrete stuff
|
|
31 def(skip, @(empty)). % 1 length interval
|
|
32 def(infinite, (true & false)). %
|
|
33 def(finite, ~((true & false))). %
|
|
34 def(length(I), X):- I>=0 ,def_length(I,X). % length operator
|
|
35 def(less(I), X):- I>=0 ,def_less(I,X). % less than N length
|
|
36 def(next(P),(empty; @(P))).
|
|
37 % temporal assignments
|
|
38 def(gets(A,B),keep(@A<->B)).
|
|
39 def(stable(A),keep(@A<->A)).
|
|
40 def(state(A),(share(A),'[]'(L))):- def_state(A,L).
|
|
41 % def(Q=>P,exists(R,(Q = R,stable(R),fin(P = R)))).
|
|
42 % easier one
|
|
43 % def(Q=>P,(Q & (empty,P); ~Q & (empty, ~P))).
|
|
44 % def(P<=Q,Q=>P).
|
|
45 % loop stuff and quantifiers
|
|
46 def(+A ,(A & *((empty;A)))). % weak closure
|
|
47 def(while(Cond,Do), *(((Cond->Do) , (~Cond->empty)))).
|
|
48 def(repeat(Do,until,Cond), (*((Do;empty)) ,@ halt(Cond))).
|
|
49 def(all(P,Q),not(exists(P,not(Q)))):-!,
|
|
50 atomic(P). % more check is necessary
|
|
51 def(local(P), (P = (P&true))):- !.
|
|
52 % test predicates
|
|
53 def(trace(X,List),L) :- !,make_trace(List,X,L).
|
|
54 def(even(P),
|
|
55 exists(Q,(Q, keep( @Q = ~Q),'[]'((Q->P))))).
|
|
56 def(evenp(P),(
|
|
57 *(((P,skip) & skip;empty,P)) & (empty;skip)
|
|
58 )).
|
|
59 def(phil(L,R),
|
|
60 +('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) )).
|
|
61 def(X,Y) :- define(X,Y).
|
|
62
|
19
|
63 def_length(I,empty):-I=<0,!.
|
|
64 def_length(I,@ X):-I1 is I-1,def_length(I1,X).
|
|
65 def_less(I,false):-I=<0,!.
|
|
66 def_less(I,next(X)):-I1 is I-1,def_less(I1,X).
|
|
67 def_state([H],H):-!.
|
|
68 def_state([H|L],(H;L1)):-def_state(L,L1).
|
|
69 make_trace([],_,true):-!.
|
|
70 make_trace([1|T],X,(X,@L)):-!, make_trace(T,X,L).
|
|
71 make_trace([true|T],X,(X,@L)):-!, make_trace(T,X,L).
|
|
72 make_trace([0|T],X,(not(X),@L)):-!, make_trace(T,X,L).
|
|
73 make_trace([_|T],X,(not(X),@L)):-!, make_trace(T,X,L).
|
|
74
|
2
|
75 :-dynamic variable/1.
|
|
76
|
|
77 expand(X,Y) :- init_variable,expand1(X,Y).
|
|
78
|
|
79 expand1(V,V) :- var(V),!.
|
|
80 expand1((P,Q),R) :- !,expand1(P,P1),expand1(Q,Q1),and(P1,Q1,R).
|
|
81 expand1(st(R),st(R)) :- !,
|
|
82 st_variables(In,Out),add_variable(In),add_variable(Out).
|
|
83 % expand1([P|Q],R) :- !,expand1(P,P1),expand1(Q,Q1),and(P1,Q1,R).
|
|
84 expand1((P;Q),R) :- !,expand1(P,P1),expand1(Q,Q1),or(P1,Q1,R).
|
|
85 expand1((P&Q),R) :- !,expand1(P,P1),expand1(Q,Q1),chop_expand1(P1,Q1,R).
|
|
86 expand1(not(Q),NQ):-!,expand1(Q,Q1),negate(Q1,NQ).
|
|
87 expand1(exists(P,Q),exists(P,Q1)):-
|
|
88 nonvar(P),name(P,[X|_]),X = 95,!, % "_" % reuse it...
|
|
89 expand1(Q,Q1).
|
|
90 expand1(exists(P,Q),exists(P,Q1)):-var(P),!,
|
|
91 new_var(P),
|
|
92 expand1(Q,Q1).
|
|
93 expand1(exists(P,Q),exists(P,Q1)):-!,
|
|
94 expand1(Q,Q1).
|
|
95 expand1([],[]):-!.
|
|
96 expand1([H|L],?(And,true,?(NAnd,false,true_false))):-!,
|
|
97 % non-deterministic selection
|
|
98 expand_list([H|L],L1),
|
|
99 all_and(L1,And),
|
|
100 all_not(L1,NAnd).
|
|
101 expand1(^(R),^(R)):-!, % 2nd order variable
|
|
102 add_2var(R).
|
|
103 expand1(P,R) :- def(P,Q),!,expand1(Q,R).
|
|
104 expand1(P,P) :- atomic(P),!, % for empty or skip
|
|
105 check_atomic(P).
|
|
106 expand1(P,R) :- functor(P,H,N),functor(R,H,N),
|
|
107 expand_arg(N,P,R).
|
|
108 expand_arg(0,_P,_R):-!.
|
|
109 expand_arg(N,P,R):-arg(N,P,PA),arg(N,R,RA),
|
|
110 N1 is N-1,expand1(PA,RA),expand_arg(N1,P,R).
|
|
111
|
19
|
112 chop_expand1(false,_,false):-!.
|
|
113 % chop_expand1(_,false,false):-!.
|
|
114 chop_expand1(true,true,true):-!.
|
|
115 chop_expand1(P,Q,(P&Q)):-!.
|
|
116 expand_list([],[]) :-!.
|
|
117 expand_list([H|L],[H1|L1]) :-
|
|
118 expand1(H,H1), expand_list(L,L1).
|
|
119 all_and([],true):-!.
|
|
120 all_and([H|L],F):- all_and(L,F1),and(H,F1,F).
|
|
121 all_not([],true):-!.
|
|
122 all_not([H|L],F):- all_not(L,F1),negate(H,H1),and(H1,F1,F).
|
|
123 check_atomic(empty):-!.
|
|
124 check_atomic(more):-!.
|
|
125 check_atomic(true):-!.
|
|
126 check_atomic(false):-!.
|
|
127 check_atomic(true_false):-!.
|
|
128 check_atomic(P) :- name(P,PL),PL=[95|_],!.
|
|
129 check_atomic(P) :- add_variable(P). % "_"
|
|
130
|
20
|
131 % do not use r_abolish here to avoid erase dynamic property of variable/1
|
2
|
132 init_variable :- retract(variable(_)),fail;true.
|
|
133 add_variable([]):-!.
|
|
134 add_variable([X|T]) :- !,add_variable(X),add_variable(T).
|
|
135 add_variable(X) :- variable(X),!.
|
|
136 add_variable(X) :- assertz(variable(X)),!.
|
|
137 variable_list(L) :- setof(X,variable(X),L).
|
|
138
|
|
139 new_var(P) :-
|
|
140 (retract(sbn(N));N=1),N1 is N+1,asserta(sbn(N1)),!,
|
|
141 name(N1,X),S = 95,name(P,[S|X]). % "_"
|
|
142
|
|
143 add_2var(R) :- length_limit(N),!,
|
|
144 add_variable(over(R,N)),
|
|
145 add_2var(N,R).
|
|
146 add_2var(R) :-
|
|
147 add_variable(^(R)).
|
|
148 add_2var(0,R):-!,
|
|
149 add_variable(^(R,0)).
|
|
150 add_2var(N,R):- N1 is N-1,
|
|
151 add_variable(^(R,N)),
|
|
152 add_2var(N1,R).
|
|
153
|
|
154 and(false,_,false):-!.
|
|
155 and(_,false,false):-!.
|
|
156 and(true,T,T):-!.
|
|
157 and(T,true,T):-!.
|
|
158 and(T,T,T):-!.
|
|
159 and(A,B,(A,B)):-!.
|
|
160
|
|
161 or(true,_,true):-!.
|
|
162 or(_,true,true):-!.
|
|
163 or(false,T,T):-!.
|
|
164 or(T,false,T):-!.
|
|
165 or(T,T,T):-!.
|
|
166 or(A,B,(A;B)):-!.
|
|
167
|
|
168 negate(true,false):-!.
|
|
169 negate(false,true):-!.
|
|
170 negate(true_false,true_false):-!.
|
|
171 negate(not(N),N):-!.
|
|
172 negate(N,not(N)):-!.
|
|
173
|
|
174 /* */
|