|
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 $Id: ndcomp.pl,v 1.2 2007/08/30 05:16:36 kono Exp $
|
|
2
|
11 */
|
|
|
12
|
|
|
13 :-dynamic verbose/0,state/2,links/2.
|
|
|
14 :-dynamic stay/3.
|
|
|
15 :-dynamic regular_limit/1.
|
|
|
16
|
|
|
17 % itl decomposition for DST
|
|
|
18
|
|
|
19 % requires [chop]
|
|
|
20 % itl(Predicate,Next,Empty,ConditionLists)
|
|
|
21
|
|
|
22 itl(P) :- expand(P,P0),
|
|
|
23 moref(Ev),itl(P0,Next,Ev,[],C),
|
|
|
24 write(([Ev|C]->Next)),nl,fail.
|
|
|
25 itl(_).
|
|
|
26 itl(P,Next,[Ev|C]) :- moref(Ev),itl(P,Next,Ev,[],C).
|
|
|
27
|
|
|
28 moref(empty).
|
|
|
29 moref(more).
|
|
|
30
|
|
|
31 itl(true,true,_,C,C):-!.
|
|
|
32 itl(false,false,_,C,C):-!.
|
|
|
33 itl(more,false,empty,C,C).
|
|
|
34 itl(more,true,E,C,C):-!,E = more.
|
|
|
35 % next two rule determines descrete time
|
|
|
36 itl(empty,true,empty,C,C).
|
|
|
37 itl(empty,false,E,C,C):-!,E = more. % no succeeding more interval
|
|
|
38 itl(N,F,E,C,C1):-number(N),!,
|
|
|
39 sb(Subterm,N),!,itl(Subterm,F,E,C,C1).
|
|
|
40 itl(?(Cond,T,F),N,E,C,C1):-!,
|
|
|
41 itl(Cond,CN,E,C,C0),itl_cond(CN,T,F,N,E,C0,C1).
|
|
|
42 itl_cond(true,T,_,N,E,C,C1) :-!,
|
|
|
43 itl(T,N,E,C,C1).
|
|
|
44 itl_cond(false,_,F,N,E,C,C1) :-!,
|
|
|
45 itl(F,N,E,C,C1).
|
|
|
46 itl_cond(CN,T,F,N,E,C,C1) :-!,
|
|
|
47 itl(T,TN,E,C,C0),
|
|
|
48 itl(F,FN,E,C0,C1), negate(CN,NCN),
|
|
|
49 and(TN,CN,N1),and(FN,NCN,N2), or(N1,N2,N).
|
|
|
50
|
|
|
51 itl(P,FF,_,C,C1) :- atomic(P),!, local(FF,P,C,C1).
|
|
|
52 local(true,P,C,C1):- true(C,P,C,C1).
|
|
|
53 true([],P,C,[P|C]):-!.
|
|
|
54 true([P|_],P,C,C):-!.
|
|
|
55 true([not(P)|_],P,_,_):-!,fail.
|
|
|
56 true([_|T],P,C,C1):-true(T,P,C,C1).
|
|
|
57 local(false,P,C,C1):- false(C,P,C,C1).
|
|
|
58 false([],P,C,[not(P)|C]):-!.
|
|
|
59 false([P|_],P,_,_):-!,fail.
|
|
|
60 false([not(P)|_],P,C,C):-!.
|
|
|
61 false([_|T],P,C,C1):-false(T,P,C,C1).
|
|
|
62 itl(@(P),P,more,C,C). % strong next
|
|
|
63 itl(@(_),false,E,C,C):-!,E=empty.
|
|
|
64
|
|
|
65 % Regular Variable
|
|
|
66 itl(^(R),F,empty,C,C1):-
|
|
|
67 local(F0,up(R),C,C0),
|
|
|
68 local(F1,down(R,0),C0,C1),and(F0,F1,F).
|
|
|
69 itl(^(R),F1,E,C,C1):-!, E=more,
|
|
|
70 local(F,up(R),C,C1),and(F,^(R,0),F1).
|
|
|
71
|
|
|
72 itl(^(_R,S),false,_,C,C):-
|
|
|
73 regular_limit(X),S>X,!.
|
|
|
74 itl(^(R,S),F,empty,C,C1):-
|
|
|
75 local(F,down(R,S),C,C1).
|
|
|
76 itl(^(R,S),^(R,S1),E,C,C):-!, E=more, S1 is S+1.
|
|
|
77
|
|
|
78 % Quantifier
|
|
|
79 itl(exists(P,Q),F,E,C,C0) :-!,
|
|
|
80 itl(Q,QT,E,[P|C],C1),itl_ex(QT,Q,E,P,F,C1,C0).
|
|
|
81 itl_ex(true,_,_,P,true,C,C1):-!,remove_p(C,P,C1).
|
|
|
82 itl_ex(false,Q,E,P,F,C,C0):- !,remove_p(C,P,C1),
|
|
|
83 itl(Q,QF,E,[not(P)|C1],C2),remove_p(C2,P,C0), exists(QF,P,F).
|
|
|
84 itl_ex(QT,Q,E,P,F,C,C0):- remove_p(C,P,C1),
|
|
|
85 itl(Q,QF,E,[not(P)|C1],C2), remove_p(C2,P,C0),
|
|
|
86 or(QT,QF,TF),exists(TF,P,F).
|
|
|
87 % constant order optimzation for quantifier
|
|
|
88 exists(P,P,true):-!.
|
|
|
89 exists(P,_,P):-atomic(P),!.
|
|
|
90 exists(Q,P,exists(P,Q)).
|
|
|
91 remove_p([],_,[]):-!.
|
|
|
92 remove_p([not(P)|T],P,T):-!.
|
|
|
93 remove_p([P|T],P,T):-!.
|
|
|
94 remove_p([H|T],P,[H|T1]):-!,remove_p(T,P,T1).
|
|
|
95 itl(*(P),F,empty,C,C1):-!,itl(P,F,empty,C,C1).
|
|
|
96 itl(*(P),F,E,C,C1):-!,E=more,
|
|
|
97 itl(P,PX,more,C,C1),
|
|
|
98 closure(PX,P,F).
|
|
|
99 closure(false,_,false):-!.
|
|
|
100 closure(PX,P,(PX & *(P))). %% infinite clousre (strong)
|
|
|
101 %% closure(PX,P,(PX & (*(P);empty))). %% finite closure (weak)
|
|
|
102 %% external state diagram (determinization)
|
|
|
103 itl(st(N),F,E,C,C1):-!,
|
|
|
104 setof((Cond=>X),st(N,Cond,X),L),
|
|
|
105 itl_transition(L,F,E,C,C1).
|
|
|
106 itl_transition([],false,_,C,C):-!.
|
|
|
107 itl_transition([(Cond=>true)|T],F,E,C,C1):-!,
|
|
|
108 itl((Cond),F0,E,C,C0),
|
|
|
109 itl_transition(T,F1,E,C0,C1),or(F0,F1,F).
|
|
|
110 itl_transition([(Cond=>empty)|T],F,E,C,C1):-!,
|
|
|
111 itl((empty,Cond),F0,E,C,C0),
|
|
|
112 itl_transition(T,F1,E,C0,C1),or(F0,F1,F).
|
|
|
113 itl_transition([(Cond=>X)|T],F,E,C,C1):-
|
|
|
114 itl((more,Cond),F0,E,C,C0),
|
|
|
115 itl_transition1(F0,X,T,F,E,C0,C1).
|
|
|
116 itl_transition1(false,_,T,F,E,C,C1):-!,
|
|
|
117 itl_transition(T,F,E,C,C1).
|
|
|
118 itl_transition1(true,X,T,F1,E,C,C1):-!,
|
|
|
119 itl_transition(T,F,E,C,C1),or(F,st(X),F1).
|
|
|
120 %% ignore last state to check non stop predicate
|
|
|
121 itl(free_fin(_),F,empty,C,C):-!,F=true.
|
|
|
122 itl(free_fin(L),F1,more,C,C1):-!,
|
|
|
123 itl(L,F,more,C,C1),free_fin(F,F1).
|
|
|
124 free_fin(true,true):-!.
|
|
|
125 free_fin(false,false):-!.
|
|
|
126 free_fin(X,free_fin(X)):-!.
|
|
|
127 %%
|
|
|
128 itl((P,Q),N,E,C,C1) :-!,
|
|
|
129 itl(P,PN,E,C,C0),itland(PN,Q,N,E,C0,C1).
|
|
|
130 itland(false,_,false,_,C0,C0):-!.
|
|
|
131 itland(true,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1).
|
|
|
132 itland(PN,Q,N,E,C0,C1):-
|
|
|
133 itl(Q,QN,E,C0,C1),and(PN,QN,N). %% and/3 in chop.pl
|
|
|
134 itl((P;Q),N,E,C,C1) :-!,
|
|
|
135 itl(P,PN,E,C,C0),itlor(PN,Q,N,E,C0,C1).
|
|
|
136 itlor(true,_,true,_,C0,C0):-!.
|
|
|
137 itlor(false,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1).
|
|
|
138 itlor(PN,Q,N,E,C0,C1):-
|
|
|
139 itl(Q,QN,E,C0,C1),or(PN,QN,N). %% or/3 in chop.pl
|
|
|
140 itl(not(P),NN,E,X,X1) :- !,
|
|
|
141 itl(P,N,E,X,X1),
|
|
|
142 negate(N,NN). %% negate/2 in chop.pl
|
|
|
143 % F = empty?(P,Q):(empty(P)*more(Q)+more(PM)&Q)
|
|
|
144 itl((P&Q),F,empty,C,C1) :-!,
|
|
|
145 itl((P,Q),F,empty,C,C1).
|
|
|
146 itl((P&Q),F,more,C,C2) :-!,
|
|
|
147 itl(P,PE,empty,C,C0),
|
|
|
148 C0 = C0R,
|
|
|
149 itl(P,PM,more,C0R,C1),
|
|
|
150 chop(PM,PE,F,Q,C1,C2).
|
|
|
151
|
|
|
152 chop(false,false,false,_,C,C):-!.
|
|
|
153 chop(PM,false,(PM & Q),Q,C,C):-!.
|
|
|
154 chop(PM,true,F,Q,C,C1):-!,
|
|
|
155 itl(Q,QF,more,C,C1),
|
|
|
156 chop1(PM,QF,Q,F).
|
|
|
157 chop(PM,PE,F,Q,C,C):-!,
|
|
|
158 write('next empty conflict:'),write((PM,PE,F,Q,C)),nl,!,
|
|
|
159 fail.
|
|
|
160
|
|
|
161 chop1(false,QF,_,QF):-!.
|
|
|
162 chop1(false,false,_,false):-!.
|
|
|
163 chop1(PM,false,Q,(PM&Q)):-!.
|
|
|
164 chop1(_,true,_,true):-!.
|
|
|
165 chop1(PM,QF,Q,(QF;(PM&Q))):-!.
|
|
|
166
|
|
|
167 itl(proj(_,Q),F,empty,C,C1) :-!,
|
|
|
168 itl(Q,F,empty,C,C1).
|
|
|
169 itl(proj(P,Q),F,more,C,C1) :-!,
|
|
|
170 itl(P,PM,more,C,C0),
|
|
|
171 itl(Q,QM,more,C0,C1),
|
|
|
172 prj(PM,QM,P,F).
|
|
|
173 prj(false,_,_,false):-!.
|
|
|
174 prj(_,false,_,false):-!.
|
|
|
175 prj(PM,QM,P,(PM&proj(P,QM))).
|
|
|
176
|
|
|
177 itl(prefix(P),F,empty,C,C1) :-!,
|
|
|
178 itl(P,PE,empty,C,C0),
|
|
|
179 itl(P,PM,more,C0,C1), % this must be satistifiable
|
|
|
180 prefix(PM,PE,F).
|
|
|
181 itl(prefix(P),F,more,C,C1) :-!,
|
|
|
182 itl(P,PM,more,C,C1),
|
|
|
183 prefix(PM,F).
|
|
|
184
|
|
|
185 prefix(true,true):-!.
|
|
|
186 prefix(false,false):-!.
|
|
|
187 prefix(PM,prefix(PM)):-!.
|
|
|
188
|
|
|
189 prefix(true,_,true):-!.
|
|
|
190 prefix(_,true,true):-!.
|
|
|
191 prefix(false,false,false):-!.
|
|
|
192 prefix(_,false,true):-!.
|
|
|
193
|
|
|
194 itl(Def,_,_,_,_) :-
|
|
|
195 write('error: '),write(Def),nl,!,fail.
|
|
|
196
|
|
|
197 itl_statistics :- nl,
|
|
|
198 itl_state_number(X),write(X),write(' states'),nl,fail.
|
|
|
199 itl_statistics :-
|
|
|
200 sbn(X),write(X),write(' subterms'),nl,fail.
|
|
|
201 itl_statistics :-
|
|
|
202 init_var(tmp,0),
|
|
|
203 ((links(_,_),inc_var(tmp,_),fail);true),
|
|
|
204 tmp(N),
|
|
|
205 % init_var(tmp,0),
|
|
|
206 % ((state(_,_,_),inc_var(tmp,_),fail);true),
|
|
|
207 % recorded(tmp,L,_),
|
|
|
208 itl_transition(L),
|
|
|
209 write(N),put(47), % "/"
|
|
|
210 write(L),write(' state transitions'),nl,fail.
|
|
|
211 itl_statistics.
|
|
|
212
|
|
|
213
|
|
|
214 :-assert(verbose).
|
|
|
215 verbose(off) :- retract(verbose),fail;true.
|
|
|
216 verbose(on) :- asserta(verbose).
|
|
|
217
|
|
|
218 deve(ITL) :-
|
|
|
219 init,!,
|
|
|
220 expand(ITL,ITL0), % chop standard form
|
|
|
221 itlstd(ITL0,StdNOW), % BDT
|
|
|
222 assert(itl_state(StdNOW,1)),!, % Initial State
|
|
|
223 deve0((1,ITL0)).
|
|
|
224
|
|
|
225 deve0((S,ITL)) :-
|
|
|
226 % increment_state(ITL,ITL_1,S),
|
|
|
227 show_state(S,ITL),
|
|
|
228 % setof(Next,itldecomp(ITL,Next,S),
|
|
|
229 bagof(Next,itldecomp(ITL,Next,S),
|
|
|
230 Nexts),!,
|
|
|
231 deve1(Nexts).
|
|
|
232 deve0(_).
|
|
|
233
|
|
|
234 deve1([]).
|
|
|
235 deve1([H|T]) :- deve0(H),deve1(T).
|
|
|
236
|
|
|
237 itldecomp(ITL,(NextS,Next),From) :-
|
|
|
238 init_var(current,From),
|
|
|
239 itl(ITL,Next,Cond),
|
|
|
240 %% showing
|
|
|
241 itlshow(Next,NextS,Cond,From).
|
|
|
242
|
|
|
243 itlshow(Next,S,Cond,From):-
|
|
|
244 itlstd(Next,StdNext),
|
|
|
245 check_state(StdNext,Cond,New,S),
|
|
|
246 inc_var(itl_transition,_),
|
|
|
247 assertz(state(From,Cond,S)),
|
|
|
248 (links(S,From),!;assertz(links(S,From))),
|
|
|
249 !,
|
|
|
250 itlshow0(S,Cond,Next,New).
|
|
|
251
|
|
|
252 itlshow0(S,Cond,Next,New) :- verbose,!,
|
|
|
253 itlshow1(S,Cond,Next,New),nl,!,New=1.
|
|
|
254 itlshow0(0,_,_,0):- !,put(101),!,fail. % "e"
|
|
|
255 itlshow0(false,_,_,0):- !,put(102),!,fail. % "f"
|
|
|
256 itlshow0(true,_,_,0):- !,put(116),!,fail. % "t"
|
|
|
257 itlshow0(_,_,_,0):- !,put(46),!,fail. % "."
|
|
|
258 itlshow0(S,_,_,1):- !,write(S),put(46),ttyflush,!. % "."
|
|
|
259
|
|
|
260 itlshow1(0,Cond,_,_):-!,
|
|
|
261 write(Cond),write('->'),write(empty).
|
|
|
262 itlshow1(true,Cond,_,_):-!,
|
|
|
263 write(Cond),write('->'),write(true).
|
|
|
264 itlshow1(false,Cond,_,_):-!,
|
|
|
265 write(Cond),write('->'),write(false).
|
|
|
266 itlshow1(S,Cond,_,0):-!,
|
|
|
267 write(Cond),write('->'),write(S).
|
|
|
268 itlshow1(S,Cond,Org,1):-
|
|
|
269 write(Cond),write('->'),write(S),
|
|
|
270 put(9),write(Org),!.
|
|
|
271
|
|
|
272 init :-
|
|
|
273 subterm_init,
|
|
20
|
274 r_abolish(state,3),
|
|
2
|
275 asserta(state(true,[more],true)),
|
|
|
276 asserta(state(true,[empty],0)),
|
|
20
|
277 r_abolish(itl_state,2),
|
|
|
278 r_abolish(stay,3),asserta(stay(0,0,0)),
|
|
2
|
279 asserta(itl_state(false,false)),
|
|
|
280 asserta(itl_state(empty,0)),
|
|
|
281 asserta(itl_state(true,true)),
|
|
|
282 init_var(regular_limit,5),
|
|
20
|
283 r_abolish(links,2),asserta(links(true,true)),
|
|
2
|
284 init_var(current,0),
|
|
|
285 init_var(itl_transition,1),
|
|
|
286 init_var(itl_state_number,1),!.
|
|
|
287
|
|
|
288 show_state(S,ITL) :-
|
|
|
289 nl,write('state('),write(S), % (
|
|
|
290 (verbose,write(' , '), write(ITL),write(')'),nl;write(')')),!.
|
|
|
291
|
|
|
292 check_state(true,[more |_],0,true):-!.
|
|
|
293 check_state(true,[empty|_],0,0):-!.
|
|
|
294 check_state(false,_,0,false):-!.
|
|
|
295 check_state(STD,_,0,S):-
|
|
|
296 itl_state(STD,S),!.
|
|
|
297 check_state(STD,_,1,S):-
|
|
|
298 inc_var(itl_state_number,S),
|
|
|
299 assert(itl_state(STD,S)),!.
|
|
|
300
|
|
|
301 init_var(X,_) :- functor(F,X,1),assert(F),fail.
|
|
|
302 init_var(X,_) :- functor(F,X,1),retract(F),fail.
|
|
|
303 init_var(X,V) :- functor(F,X,1),arg(1,F,V),assert(F),!.
|
|
|
304 inc_var(Name,X1) :-
|
|
|
305 functor(F,Name,1),retract(F),arg(1,F,X),
|
|
|
306 X1 is X+1,functor(F1,Name,1),arg(1,F1,X1),
|
|
|
307 asserta(F1),!.
|
|
|
308 set_var(Name,X,X1) :-
|
|
|
309 functor(F,Name,1),retract(F),!,arg(1,F,X),
|
|
|
310 functor(F1,Name,1),arg(1,F1,X1),asserta(F1),!.
|
|
|
311 set_var(Name,X,_) :- init_var(Name,X).
|
|
|
312
|
|
|
313 increment_state(stay(P,now),stay(P,S),S) :- !,
|
|
|
314 (stay(P,F,S);assertz(stay(P,F,S))),!.
|
|
|
315 increment_state(N,N,_) :- atomic(N),!.
|
|
|
316 increment_state(P,R,S) :- functor(P,H,N),functor(R,H,N),
|
|
|
317 increment_state_arg(N,P,R,S).
|
|
|
318 increment_state_arg(0,_P,_R,_):-!.
|
|
|
319 increment_state_arg(N,P,R,S):-arg(N,P,PA),arg(N,R,RA),
|
|
|
320 N1 is N-1,increment_state(PA,RA,S),
|
|
|
321 increment_state_arg(N1,P,R,S).
|
|
|
322
|
|
|
323 %% end %%
|
