|
0
|
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 $Id$
|
|
|
11 */
|
|
|
12
|
|
|
13 % itl decomposition for DST
|
|
|
14
|
|
1
|
15 :- dynamic length_limit/1,renaming/0.
|
|
|
16
|
|
0
|
17 % requires [chop]
|
|
|
18 % itl(Predicate,Next,Empty,ConditionLists)
|
|
|
19
|
|
|
20 itl(P) :- expand(P,P0),
|
|
|
21 moref(Ev),itl(P0,Next,Ev,[],C),
|
|
|
22 write(([Ev|C]->Next)),nl,fail.
|
|
|
23 itl(_).
|
|
|
24 itl(P,Next,[Ev|C]) :- moref(Ev),itl(P,Next,Ev,[],C).
|
|
|
25
|
|
|
26 moref(empty).
|
|
|
27 moref(more).
|
|
|
28
|
|
|
29 % :- table itl/5.
|
|
|
30
|
|
|
31 itl(N,F,E,C,C1):-number(N),!,
|
|
|
32 sb(Subterm,N),!,itl(Subterm,F,E,C,C1).
|
|
|
33 itl(true,true,_,C,C):-!.
|
|
|
34 itl(false,false,_,C,C):-!.
|
|
1
|
35 itl(true_false,true_false,more,C,C):-!.
|
|
|
36 itl(true_false,true,empty,C,[choice(true)|C]).
|
|
|
37 itl(true_false,false,E,C,[choice(false)|C]):-!,E=empty.
|
|
0
|
38 itl(more,false,empty,C,C).
|
|
|
39 itl(more,true,E,C,C):-!,E = more.
|
|
|
40 % next two rule determines descrete time
|
|
|
41 itl(empty,true,empty,C,C).
|
|
|
42 itl(empty,false,E,C,C):-!,E = more. % no succeeding more interval
|
|
|
43 itl(P,FF,_,C,C1) :- atomic(P),!, local(FF,P,C,C1).
|
|
|
44 itl(@(P),P,more,C,C). % strong next
|
|
|
45 itl(@(_),false,E,C,C):-!,E=empty.
|
|
|
46
|
|
|
47 itl(?(Cond,T,F),N,E,C,C1):-!,
|
|
|
48 itl(Cond,CN,E,C,C0),itl_cond(CN,T,F,N,E,C0,C1).
|
|
1
|
49 % Non deterministic selection (singleton 2nd order variable)
|
|
|
50 itl([],true,_,C,C):-!.
|
|
|
51 itl([H|L],F,empty,C,C1):-!,
|
|
|
52 empty_choice([H|L],0,F,C,C1).
|
|
|
53 itl([H|L],F,E,C,C1):-!,E=more,
|
|
|
54 choice([H|L],F,C,C1).
|
|
0
|
55 % Regular Variable
|
|
|
56 itl(^(R),F,empty,C,C1):-
|
|
1
|
57 local(F,^(R,0),C,C1).
|
|
|
58 itl(^(R),^(R,1),E,C,C):-!, E=more.
|
|
0
|
59
|
|
|
60 itl(^(R,S),F,empty,C,C1):-
|
|
1
|
61 local(F,^(R,S),C,C1).
|
|
|
62 %itl(^(R,S),F,E,C,C1):- E = more,
|
|
|
63 % length_limit(X),S>=X,inc_var(over,_),!,
|
|
|
64 % S1 is S+1,local(F,over(R,S1),C,C1).
|
|
|
65 itl(^(R,S),^(R,S1),E,C,C):-!,
|
|
|
66 % increment regular variable length
|
|
0
|
67 E=more, S1 is S+1.
|
|
|
68
|
|
|
69 % Quantifier
|
|
|
70 itl(exists(P,Q),F,E,C,C0) :-!,
|
|
|
71 itl(Q,QT,E,[P|C],C1),itl_ex(QT,Q,E,P,F,C1,C0).
|
|
|
72 itl(*(P),F,empty,C,C1):-!,itl(P,F,empty,C,C1).
|
|
|
73 itl(*(P),F,E,C,C1):-!,E=more,
|
|
|
74 itl(P,PX,more,C,C1),
|
|
|
75 closure(PX,P,F).
|
|
|
76 %% external state diagram
|
|
|
77 itl(st(N),F,E,C,C1):-!,
|
|
|
78 setof((Cond=>X),st(N,Cond,X),L),itl_transition(L,F,E,C,C1).
|
|
|
79 %% ignore last state to check non stop predicate
|
|
|
80 itl(non_terminate(_),F,empty,C,C):-!,F=true.
|
|
|
81 itl(non_terminate(L),F,more,C,C1):-!,
|
|
|
82 itl(L,F,more,C,C1).
|
|
|
83 %% shared resources or state
|
|
|
84 itl(share(L),F,empty,C,C1):-!,
|
|
|
85 exclusive(L,C,C1,true,F).
|
|
|
86 itl(share(L),F,more,C,C1):-!,
|
|
|
87 exclusive(L,C,C1,share(L),F).
|
|
|
88 %%
|
|
|
89 itl((P,Q),N,E,C,C1) :-!,
|
|
|
90 itl(P,PN,E,C,C0),itland(PN,Q,N,E,C0,C1).
|
|
|
91 itl((P;Q),N,E,C,C1) :-!,
|
|
|
92 itl(P,PN,E,C,C0),itlor(PN,Q,N,E,C0,C1).
|
|
|
93 itl(not(P),NN,E,X,X1) :- !,
|
|
|
94 itl(P,N,E,X,X1),
|
|
|
95 negate(N,NN). %% negate/2 in chop.pl
|
|
|
96 % F = empty?(P,Q):(empty(P)*more(Q)+more(PM)&Q)
|
|
|
97 itl((P&Q),F,empty,C,C1) :-!,
|
|
|
98 itl((P,Q),F,empty,C,C1).
|
|
|
99 itl((P&Q),F,more,C,C2) :-!,
|
|
|
100 itl(P,PE,empty,C,C0),
|
|
|
101 itl(P,PM,more,C0,C1),
|
|
|
102 chop(PM,PE,F,Q,C1,C2).
|
|
19
|
103 itl(proj(_,Q),F,empty,C,C1) :-!,
|
|
|
104 itl(Q,F,empty,C,C1).
|
|
|
105 itl(proj(P,Q),F,more,C,C1) :-!,
|
|
|
106 itl(P,PM,more,C,C0),
|
|
|
107 itl(Q,QM,more,C0,C1),
|
|
|
108 prj(PM,QM,P,F).
|
|
|
109 % prefix is not consistently defined
|
|
|
110 % prefix(fin(false)) = true ? funny...
|
|
|
111 itl(prefix(P),F,empty,C,C1) :-!,
|
|
|
112 itl(P,PE,empty,C,C0),
|
|
|
113 itl(P,PM,more,C0,C1),
|
|
|
114 prefix(PM,PE,F).
|
|
|
115 itl(prefix(P),F,more,C,C1) :-!,
|
|
|
116 itl(P,PM,more,C,C1),
|
|
|
117 prefix(PM,F).
|
|
|
118 itl(Def,_,_,_,_) :-
|
|
|
119 write('error: '),write(Def),nl,!,fail.
|
|
0
|
120
|
|
19
|
121
|
|
|
122 local(true,P,C,C1):- true(C,P,C,C1).
|
|
|
123 local(false,P,C,C1):- false(C,P,C,C1).
|
|
|
124 true([],P,C,[P|C]):-!.
|
|
|
125 true([P|_],P,C,C):-!.
|
|
|
126 true([not(P)|_],P,_,_):-!,fail.
|
|
|
127 true([_|T],P,C,C1):-true(T,P,C,C1).
|
|
|
128 false([],P,C,[not(P)|C]):-!.
|
|
|
129 false([P|_],P,_,_):-!,fail.
|
|
|
130 false([not(P)|_],P,C,C):-!.
|
|
|
131 false([_|T],P,C,C1):-false(T,P,C,C1).
|
|
|
132 empty_choice([H|_],N,F,C,[choice(N)|C1]) :-
|
|
|
133 itl(H,F,empty,C,C1).
|
|
|
134 empty_choice([_|L],N,F,C,C1) :-
|
|
|
135 N1 is N+1,
|
|
|
136 empty_choice(L,N1,F,C,C1).
|
|
|
137 choice([],[],C,C) :-!.
|
|
|
138 choice([H|L],[H1|L1],C,C2) :-
|
|
|
139 itl(H,H1,more,C,C1),
|
|
|
140 choice(L,L1,C1,C2).
|
|
|
141 itl_cond(true,T,_,N,E,C,C1) :-!,
|
|
|
142 itl(T,N,E,C,C1).
|
|
|
143 itl_cond(false,_,F,N,E,C,C1) :-!,
|
|
|
144 itl(F,N,E,C,C1).
|
|
|
145 itl_cond(CN,T,F,N,E,C,C1) :-!,
|
|
|
146 itl(T,TN,E,C,C0),
|
|
|
147 itl(F,FN,E,C0,C1), negate(CN,NCN),
|
|
|
148 and(TN,CN,N1),and(FN,NCN,N2), or(N1,N2,N).
|
|
|
149 itl_ex(true,_,_,P,true,C,C1):-!,remove_p(C,P,C1).
|
|
|
150 itl_ex(false,Q,E,P,F,C,C0):- !,remove_p(C,P,C1),
|
|
|
151 itl(Q,QF,E,[not(P)|C1],C2),remove_p(C2,P,C0), exists(QF,P,F).
|
|
|
152 itl_ex(QT,Q,E,P,F,C,C0):- remove_p(C,P,C1),
|
|
|
153 itl(Q,QF,E,[not(P)|C1],C2), remove_p(C2,P,C0),
|
|
|
154 or(QT,QF,TF),exists(TF,P,F).
|
|
|
155 % constant order optimzation for quantifier
|
|
|
156 exists(P,P,true):-!.
|
|
|
157 exists(P,_,P):-atomic(P),!.
|
|
|
158 exists(Q,P,exists(P,Q)).
|
|
|
159 remove_p([],_,[]):-!.
|
|
|
160 remove_p([not(P)|T],P,T):-!.
|
|
|
161 remove_p([P|T],P,T):-!.
|
|
|
162 remove_p([H|T],P,[H|T1]):-!,remove_p(T,P,T1).
|
|
|
163 closure(false,_,false):-!.
|
|
|
164 closure(PX,P,(PX & *(P))). %% infinite clousre (strong)
|
|
|
165 %% closure(PX,P,(PX & (*(P);empty))). %% finite closure (weak)
|
|
|
166 itl_transition([],false,_,C,C):-!.
|
|
|
167 itl_transition([(Cond=>empty)|T],F,E,C,C1):-!,
|
|
|
168 itl((empty,Cond),F0,E,C,C0),
|
|
|
169 itl_transition(T,F1,E,C0,C1),or(F0,F1,F).
|
|
|
170 itl_transition([(Cond=>X)|T],F,E,C,C1):-
|
|
|
171 itl((more,Cond),F0,E,C,C0),
|
|
|
172 itl_transition1(F0,X,T,F,E,C0,C1).
|
|
|
173 itl_transition1(false,_,T,F,E,C,C1):-
|
|
|
174 itl_transition(T,F,E,C,C1).
|
|
|
175 itl_transition1(true,X,T,(st(X);F),E,C,C1):-
|
|
|
176 itl_transition(T,F,E,C,C1).
|
|
|
177 exclusive([],C,C,F,F):-!.
|
|
|
178 exclusive([A|L],C,C1,F,F1):-
|
|
|
179 true(C,A,C,C0),exclusive1(L,C0,C1,F,F1).
|
|
|
180 exclusive([N|L],C,C1,F,F1):-
|
|
|
181 false(C,N,C,C0), !,exclusive(L,C0,C1,F,F1).
|
|
|
182 % exclusive(_,C,C,_,false). % eliminate this brach
|
|
|
183 exclusive1([],C,C,F,F):-!.
|
|
|
184 exclusive1([H|L],C,C1,F,F1):-
|
|
|
185 false(C,H,C,C0), !,exclusive1(L,C0,C1,F,F1).
|
|
|
186 % exclusive1(_,C,C,_,false).
|
|
|
187 itland(false,_,false,_,C0,C0):-!.
|
|
|
188 itland(true,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1).
|
|
|
189 itland(PN,Q,N,E,C0,C1):-
|
|
|
190 itl(Q,QN,E,C0,C1),and(PN,QN,N). %% and/3 in chop.pl
|
|
|
191 itlor(true,_,true,_,C0,C0):-!.
|
|
|
192 itlor(false,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1).
|
|
|
193 itlor(PN,Q,N,E,C0,C1):-
|
|
|
194 itl(Q,QN,E,C0,C1),or(PN,QN,N). %% or/3 in chop.pl
|
|
0
|
195 chop(false,false,false,_,C,C):-!.
|
|
|
196 chop(PM,false,(PM & Q),Q,C,C):-!.
|
|
|
197 chop(PM,true,F,Q,C,C1):-!,
|
|
|
198 itl(Q,QF,more,C,C1),
|
|
|
199 chop1(PM,QF,Q,F).
|
|
|
200 chop(PM,PE,F,Q,C,C):-!,
|
|
|
201 write('next empty conflict:'),write((PM,PE,F,Q,C)),nl,!,
|
|
|
202 fail.
|
|
|
203
|
|
|
204 chop1(false,QF,_,QF):-!.
|
|
|
205 chop1(false,false,_,false):-!.
|
|
1
|
206 chop1(true,false,true,true):-!.
|
|
|
207 chop1(true,_,true,true):-!.
|
|
0
|
208 chop1(PM,false,Q,(PM&Q)):-!.
|
|
|
209 chop1(_,true,_,true):-!.
|
|
|
210 chop1(PM,QF,Q,(QF;(PM&Q))):-!.
|
|
|
211
|
|
|
212 prj(false,_,_,false):-!.
|
|
|
213 prj(_,false,_,false):-!.
|
|
|
214 prj(PM,QM,P,(PM&proj(P,QM))).
|
|
|
215
|
|
|
216
|
|
|
217 prefix(true,true):-!.
|
|
|
218 prefix(false,false):-!.
|
|
|
219 prefix(PM,prefix(PM)):-!.
|
|
|
220
|
|
|
221 prefix(true,_,true):-!.
|
|
|
222 prefix(_,true,true):-!.
|
|
|
223 prefix(false,false,false):-!.
|
|
|
224 prefix(_,false,true):-!.
|
|
|
225
|
|
|
226
|
|
|
227 % develop Local ITL formula into state diagram
|
|
|
228 %
|
|
|
229 % Mon May 20 17:24:23 BST 1991
|
|
|
230 % require([chop]).
|
|
|
231
|
|
|
232 :-dynamic verbose/0,state/2,links/2.
|
|
1
|
233 :-dynamic stay/3,lazy/0,singleton/0,detailed/0.
|
|
0
|
234
|
|
|
235 verbose(off) :- retract(verbose),fail;true.
|
|
|
236 verbose(on) :- asserta(verbose).
|
|
1
|
237 :-verbose(on).
|
|
0
|
238
|
|
|
239 lazy(off) :- retract(lazy),fail;true.
|
|
|
240 lazy(on) :- asserta(lazy).
|
|
|
241
|
|
1
|
242 :-lazy(on).
|
|
|
243
|
|
0
|
244 singleton(off) :- retract(singleton),fail;true.
|
|
|
245 singleton(on) :- asserta(singleton).
|
|
1
|
246 :-singleton(on).
|
|
|
247
|
|
|
248 renaming(off) :- retract(renaming),fail;true.
|
|
|
249 renaming(on) :- asserta(renaming).
|
|
|
250 :-renaming(on).
|
|
|
251
|
|
|
252 detail(off) :- retract(detailed),fail;true.
|
|
|
253 detail(on) :- asserta(detailed).
|
|
|
254 % :-detail(on).
|
|
0
|
255
|
|
|
256 set_limit(X) :-
|
|
1
|
257 set_var(length_limit,X,_).
|
|
|
258 no_limit :-
|
|
|
259 retract(length_limit),fail.
|
|
|
260 no_limit.
|
|
|
261
|
|
|
262 :-assert(length_limit(5)).
|
|
0
|
263
|
|
|
264 deve(ITL) :-
|
|
|
265 init,!,
|
|
|
266 expand(ITL,ITL0), % chop standard form
|
|
1
|
267 itlstd(ITL0,StdNOW,_), % BDT
|
|
0
|
268 assert(itl_state(StdNOW,1)),!, % Initial State
|
|
|
269 deve0((1,StdNOW)).
|
|
|
270
|
|
|
271 deve0((S,ITL)) :-
|
|
|
272 show_state(S,ITL),
|
|
|
273 bagof(Next,itldecomp(ITL,Next,S),
|
|
|
274 Nexts),!,
|
|
|
275 deve1(Nexts).
|
|
|
276 deve0(_).
|
|
|
277
|
|
|
278 deve1([]).
|
|
|
279 deve1([H|T]) :- deve0(H),deve1(T).
|
|
|
280
|
|
|
281 itldecomp(ITL,(NextS,StdNext),From) :-
|
|
|
282 init_var(current,From),
|
|
|
283 itl(ITL,Next,Cond),
|
|
|
284 %% showing
|
|
1
|
285 itlshow(Next,NextS,Cond,From,StdNext).
|
|
0
|
286
|
|
1
|
287 itlshow(Next,S,Cond,From,StdNext):-
|
|
|
288 itlstd(Next,StdNext,Rename),
|
|
0
|
289 check_state(StdNext,Cond,New,S),
|
|
1
|
290 (verbose,!,write(Rename);true),
|
|
|
291 (links(S,From),!;
|
|
|
292 assertz(links(S,From)),inc_var(itl_transition_count,_)),
|
|
|
293 inc_var(itl_transition,_),
|
|
0
|
294 itlshow0(S,Cond,StdNext,New),
|
|
|
295 !.
|
|
|
296
|
|
|
297 itlshow0(S,Cond,Next,New) :- verbose,!,
|
|
|
298 itlshow1(S,Cond,Next,New),nl,!,New=1.
|
|
|
299 itlshow0(0,_,_,0):- !,put(101),!,fail. % "e"
|
|
|
300 itlshow0(false,_,_,0):- !,put(102),!,fail. % "f"
|
|
|
301 itlshow0(true,_,_,0):- !,put(116),!,fail. % "t"
|
|
|
302 itlshow0(_,_,_,0):- !,put(46),!,fail. % "."
|
|
|
303 itlshow0(S,_,_,1):- !,write(S),put(46),ttyflush,!.
|
|
|
304
|
|
|
305 itlshow1(0,Cond,_,_):-!,
|
|
|
306 write(Cond),write('->'),write(empty). itlshow1(true,Cond,_,_):-!,
|
|
|
307 write(Cond),write('->'),write(true).
|
|
|
308 itlshow1(false,Cond,_,_):-!,
|
|
|
309 write(Cond),write('->'),write(false).
|
|
|
310 itlshow1(S,Cond,_,0):-!,
|
|
|
311 write(Cond),write('->'),write(S).
|
|
|
312 itlshow1(S,Cond,Org,1):-
|
|
|
313 write(Cond),write('->'),write(S),
|
|
|
314 put(9),bdt2itl(Org,Org0),write(Org0),!.
|
|
|
315
|
|
1
|
316 % lazy transition condition generator
|
|
|
317
|
|
|
318 state(From,Cond,Next) :-
|
|
|
319 links(Next,From),
|
|
0
|
320 itl_state(ITL,From),
|
|
1
|
321 itl(ITL,Next0,Cond),
|
|
|
322 itlstd(Next0,StdNext,_),
|
|
|
323 check_state(StdNext,Cond,_,Next1), % Next1 has not to be instantiated
|
|
|
324 Next1=Next.
|
|
|
325
|
|
|
326 % detailed state transition including 2var renamings
|
|
|
327
|
|
|
328 state(From,Cond,Next,FromFull,NextFull,Rename,Rename1) :-
|
|
|
329 links(Next,From),
|
|
|
330 itl(FromFull,PNext,Cond),
|
|
|
331 itlstd(PNext,StdNext,NextFull,Rename,Rename1),
|
|
|
332 check_state(StdNext,Cond,_,Next1), % S1 has not to be instantiated
|
|
|
333 Next = Next1.
|
|
0
|
334
|
|
|
335 init :-
|
|
|
336 subterm_init,
|
|
20
|
337 r_abolish(itl_state,2),
|
|
|
338 r_abolish(stay,3),asserta(stay(0,0,0)),
|
|
0
|
339 asserta(itl_state(false,false)),
|
|
|
340 asserta(itl_state(empty,0)),
|
|
|
341 asserta(itl_state(true,true)),
|
|
20
|
342 r_abolish(links,2),asserta(links(true,true)),
|
|
0
|
343 init_var(current,0),
|
|
1
|
344 init_var(over,0),
|
|
|
345 init_var(itl_transition,0),
|
|
|
346 init_var(itl_transition_count,0),
|
|
0
|
347 init_var(itl_state_number,1),!.
|
|
|
348
|
|
|
349 show_state(S,ITL) :-
|
|
|
350 bdt2itl(ITL,ITL0),
|
|
|
351 nl,write('state('),write(S), % (
|
|
|
352 (verbose,write(' , '), write(ITL0),write(')'),nl;write(')')),!.
|
|
|
353
|
|
|
354 check_state(true,[more |_],0,true):-!.
|
|
|
355 check_state(true,[empty|_],0,0):-!.
|
|
|
356 check_state(false,_,0,false):-!.
|
|
|
357 check_state(STD,_,0,S):-
|
|
|
358 itl_state(STD,S),!.
|
|
|
359 check_state(STD,_,1,S):-
|
|
|
360 inc_var(itl_state_number,S),
|
|
|
361 assert(itl_state(STD,S)),!.
|
|
|
362
|
|
20
|
363 init_var(X,V) :- r_abolish(X,1),functor(F,X,1),arg(1,F,V),assert(F),!.
|
|
0
|
364 inc_var(Name,X1) :-
|
|
|
365 functor(F,Name,1),retract(F),arg(1,F,X),
|
|
|
366 X1 is X+1,functor(F1,Name,1),arg(1,F1,X1),
|
|
|
367 asserta(F1),!.
|
|
|
368 set_var(Name,X,X1) :-
|
|
|
369 functor(F,Name,1),retract(F),!,arg(1,F,X),
|
|
|
370 functor(F1,Name,1),arg(1,F1,X1),asserta(F1),!.
|
|
|
371 set_var(Name,X,_) :- init_var(Name,X).
|
|
|
372
|
|
|
373
|
|
|
374 itl_statistics :- nl,
|
|
|
375 itl_state_number(X),write(X),write(' states'),nl,fail.
|
|
|
376 itl_statistics :-
|
|
|
377 sbn(X),write(X),write(' subterms'),nl,fail.
|
|
|
378 itl_statistics :-
|
|
1
|
379 itl_transition_count(X),
|
|
|
380 write(X),write(' state transions'),nl,fail.
|
|
|
381 itl_statistics :-
|
|
|
382 over(X),X=\=0,write(X),write(' interval overflows'),nl,fail.
|
|
|
383 itl_statistics :-
|
|
|
384 verbose,write('verbose,'),fail.
|
|
|
385 itl_statistics :-
|
|
|
386 renaming,write('renaming,'),fail.
|
|
|
387 itl_statistics :-
|
|
|
388 singleton,write('singleton,'),fail.
|
|
|
389 itl_statistics :-
|
|
|
390 detailed,write('detailed,'),fail.
|
|
|
391 itl_statistics :-
|
|
|
392 length_limit(X),X=\=0,write('length limit '),write(X),nl,fail.
|
|
0
|
393 itl_statistics.
|
|
|
394
|
|
|
395 %% end %%
|
