|
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
|
|
|
10 $Header$
|
|
|
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_length(I,empty):-I=<0,!.
|
|
|
36 def_length(I,@ X):-I1 is I-1,def_length(I1,X).
|
|
|
37 def(less(I), X):- I>=0 ,def_less(I,X). % less than N length
|
|
|
38 def_less(I,false):-I=<0,!.
|
|
|
39 def_less(I,next(X)):-I1 is I-1,def_less(I1,X).
|
|
|
40 def(next(P),(empty; @(P))).
|
|
|
41 % temporal assignments
|
|
|
42 def(gets(A,B),keep(@A<->B)).
|
|
|
43 def(stable(A),keep(@A<->A)).
|
|
|
44 def(state(A),(share(A),'[]'(L))):- def_state(A,L).
|
|
|
45 def_state([H],H):-!.
|
|
|
46 def_state([H|L],(H;L1)):-def_state(L,L1).
|
|
|
47 % def(Q=>P,exists(R,(Q = R,stable(R),fin(P = R)))).
|
|
|
48 % easier one
|
|
|
49 % def(Q=>P,(Q & (empty,P); ~Q & (empty, ~P))).
|
|
|
50 % def(P<=Q,Q=>P).
|
|
|
51 % loop stuff and quantifiers
|
|
|
52 def(+A ,(A & *((empty;A)))). % weak closure
|
|
|
53 def(while(Cond,Do), *(((Cond->Do) , (~Cond->empty)))).
|
|
|
54 def(repeat(Do,until,Cond), (*((Do;empty)) ,@ halt(Cond))).
|
|
|
55 def(all(P,Q),not(exists(P,not(Q)))):-!,
|
|
|
56 atomic(P). % more check is necessary
|
|
|
57 def(local(P), (P = (P&true))):- !.
|
|
|
58 % test predicates
|
|
|
59 def(trace(X,List),L) :- !,make_trace(List,X,L).
|
|
|
60 make_trace([],_,true):-!.
|
|
|
61 make_trace([1|T],X,(X,@L)):-!, make_trace(T,X,L).
|
|
|
62 make_trace([true|T],X,(X,@L)):-!, make_trace(T,X,L).
|
|
|
63 make_trace([0|T],X,(not(X),@L)):-!, make_trace(T,X,L).
|
|
|
64 make_trace([_|T],X,(not(X),@L)):-!, make_trace(T,X,L).
|
|
|
65 def(even(P),
|
|
|
66 exists(Q,(Q, keep( @Q = ~Q),'[]'((Q->P))))).
|
|
|
67 def(evenp(P),(
|
|
|
68 *(((P,skip) & skip;empty,P)) & (empty;skip)
|
|
|
69 )).
|
|
|
70 def(phil(L,R),
|
|
|
71 +('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) )).
|
|
|
72 def(X,Y) :- define(X,Y).
|
|
|
73
|
|
|
74 :-dynamic variable/1.
|
|
|
75
|
|
|
76 expand(X,Y) :- init_variable,expand1(X,Y).
|
|
|
77
|
|
|
78 expand1(V,V) :- var(V),!.
|
|
|
79 expand1((P,Q),R) :- !,expand1(P,P1),expand1(Q,Q1),and(P1,Q1,R).
|
|
|
80 expand1(st(R),st(R)) :- !,
|
|
|
81 st_variables(In,Out),add_variable(In),add_variable(Out).
|
|
|
82 % expand1([P|Q],R) :- !,expand1(P,P1),expand1(Q,Q1),and(P1,Q1,R).
|
|
|
83 expand1((P;Q),R) :- !,expand1(P,P1),expand1(Q,Q1),or(P1,Q1,R).
|
|
|
84 expand1((P&Q),R) :- !,expand1(P,P1),expand1(Q,Q1),chop_expand1(P1,Q1,R).
|
|
|
85 chop_expand1(false,_,false):-!.
|
|
|
86 % chop_expand1(_,false,false):-!.
|
|
|
87 chop_expand1(true,true,true):-!.
|
|
|
88 chop_expand1(P,Q,(P&Q)):-!.
|
|
|
89 expand1(not(Q),NQ):-!,expand1(Q,Q1),negate(Q1,NQ).
|
|
|
90 expand1(exists(P,Q),exists(P,Q1)):-
|
|
|
91 nonvar(P),name(P,[X|_]),X = 95,!, % "_" % reuse it...
|
|
|
92 expand1(Q,Q1).
|
|
|
93 expand1(exists(P,Q),exists(P,Q1)):-var(P),!,
|
|
|
94 new_var(P),
|
|
|
95 expand1(Q,Q1).
|
|
|
96 expand1(exists(P,Q),exists(P,Q1)):-!,
|
|
|
97 expand1(Q,Q1).
|
|
|
98 expand1([],[]):-!.
|
|
|
99 expand1([H|L],?(And,true,?(NAnd,false,true_false))):-!,
|
|
|
100 % non-deterministic selection
|
|
|
101 expand_list([H|L],L1),
|
|
|
102 all_and(L1,And),
|
|
|
103 all_not(L1,NAnd).
|
|
|
104 expand_list([],[]) :-!.
|
|
|
105 expand_list([H|L],[H1|L1]) :-
|
|
|
106 expand1(H,H1), expand_list(L,L1).
|
|
|
107 all_and([],true):-!.
|
|
|
108 all_and([H|L],F):- all_and(L,F1),and(H,F1,F).
|
|
|
109 all_not([],true):-!.
|
|
|
110 all_not([H|L],F):- all_not(L,F1),negate(H,H1),and(H1,F1,F).
|
|
|
111 expand1(^(R),^(R)):-!, % 2nd order variable
|
|
|
112 add_2var(R).
|
|
|
113 expand1(P,R) :- def(P,Q),!,expand1(Q,R).
|
|
|
114 expand1(P,P) :- atomic(P),!, % for empty or skip
|
|
|
115 check_atomic(P).
|
|
|
116 check_atomic(empty):-!.
|
|
|
117 check_atomic(more):-!.
|
|
|
118 check_atomic(true):-!.
|
|
|
119 check_atomic(false):-!.
|
|
|
120 check_atomic(true_false):-!.
|
|
|
121 check_atomic(P) :- name(P,PL),PL=[95|_],!.
|
|
|
122 check_atomic(P) :- add_variable(P). % "_"
|
|
|
123 expand1(P,R) :- functor(P,H,N),functor(R,H,N),
|
|
|
124 expand_arg(N,P,R).
|
|
|
125 expand_arg(0,_P,_R):-!.
|
|
|
126 expand_arg(N,P,R):-arg(N,P,PA),arg(N,R,RA),
|
|
|
127 N1 is N-1,expand1(PA,RA),expand_arg(N1,P,R).
|
|
|
128
|
|
|
129 % do not use abolish here to avoid erase dynamic property of variable/1
|
|
|
130 init_variable :- retract(variable(_)),fail;true.
|
|
|
131 add_variable([]):-!.
|
|
|
132 add_variable([X|T]) :- !,add_variable(X),add_variable(T).
|
|
|
133 add_variable(X) :- variable(X),!.
|
|
|
134 add_variable(X) :- assertz(variable(X)),!.
|
|
|
135 variable_list(L) :- setof(X,variable(X),L).
|
|
|
136
|
|
|
137 new_var(P) :-
|
|
|
138 (retract(sbn(N));N=1),N1 is N+1,asserta(sbn(N1)),!,
|
|
|
139 name(N1,X),S = 95,name(P,[S|X]). % "_"
|
|
|
140
|
|
|
141 add_2var(R) :- length_limit(N),!,
|
|
|
142 add_variable(over(R,N)),
|
|
|
143 add_2var(N,R).
|
|
|
144 add_2var(R) :-
|
|
|
145 add_variable(^(R)).
|
|
|
146 add_2var(0,R):-!,
|
|
|
147 add_variable(^(R,0)).
|
|
|
148 add_2var(N,R):- N1 is N-1,
|
|
|
149 add_variable(^(R,N)),
|
|
|
150 add_2var(N1,R).
|
|
|
151
|
|
|
152 and(false,_,false):-!.
|
|
|
153 and(_,false,false):-!.
|
|
|
154 and(true,T,T):-!.
|
|
|
155 and(T,true,T):-!.
|
|
|
156 and(T,T,T):-!.
|
|
|
157 and(A,B,(A,B)):-!.
|
|
|
158
|
|
|
159 or(true,_,true):-!.
|
|
|
160 or(_,true,true):-!.
|
|
|
161 or(false,T,T):-!.
|
|
|
162 or(T,false,T):-!.
|
|
|
163 or(T,T,T):-!.
|
|
|
164 or(A,B,(A;B)):-!.
|
|
|
165
|
|
|
166 negate(true,false):-!.
|
|
|
167 negate(false,true):-!.
|
|
|
168 negate(true_false,true_false):-!.
|
|
|
169 negate(not(N),N):-!.
|
|
|
170 negate(N,not(N)):-!.
|
|
|
171
|
|
|
172 /* */
|
