Mercurial > hg > Applications > Lite

comparison dvcomp.pl @ 1:683efd6f9a81

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Sun, 22 Mar 1998 12:22:28 +0900
parents b35e4dc6ec23
children e1d3145cff7a
comparison
equal deleted inserted replaced
0:b35e4dc6ec23 1:683efd6f9a81
10 $Id$ 10 $Id$
11 */ 11 */
12 12
13 % itl decomposition for DST 13 % itl decomposition for DST
14 14
15 :- dynamic regular_limit/1. 15 :- dynamic length_limit/1,renaming/0.
16
16 % requires [chop] 17 % requires [chop]
17 % itl(Predicate,Next,Empty,ConditionLists) 18 % itl(Predicate,Next,Empty,ConditionLists)
18 19
19 itl(P) :- expand(P,P0), 20 itl(P) :- expand(P,P0),
20 moref(Ev),itl(P0,Next,Ev,[],C), 21 moref(Ev),itl(P0,Next,Ev,[],C),
29 30
30 itl(N,F,E,C,C1):-number(N),!, 31 itl(N,F,E,C,C1):-number(N),!,
31 sb(Subterm,N),!,itl(Subterm,F,E,C,C1). 32 sb(Subterm,N),!,itl(Subterm,F,E,C,C1).
32 itl(true,true,_,C,C):-!. 33 itl(true,true,_,C,C):-!.
33 itl(false,false,_,C,C):-!. 34 itl(false,false,_,C,C):-!.
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.
34 itl(more,false,empty,C,C). 38 itl(more,false,empty,C,C).
35 itl(more,true,E,C,C):-!,E = more. 39 itl(more,true,E,C,C):-!,E = more.
36 % next two rule determines descrete time 40 % next two rule determines descrete time
37 itl(empty,true,empty,C,C). 41 itl(empty,true,empty,C,C).
38 itl(empty,false,E,C,C):-!,E = more. % no succeeding more interval 42 itl(empty,false,E,C,C):-!,E = more. % no succeeding more interval
58 itl(F,N,E,C,C1). 62 itl(F,N,E,C,C1).
59 itl_cond(CN,T,F,N,E,C,C1) :-!, 63 itl_cond(CN,T,F,N,E,C,C1) :-!,
60 itl(T,TN,E,C,C0), 64 itl(T,TN,E,C,C0),
61 itl(F,FN,E,C0,C1), negate(CN,NCN), 65 itl(F,FN,E,C0,C1), negate(CN,NCN),
62 and(TN,CN,N1),and(FN,NCN,N2), or(N1,N2,N). 66 and(TN,CN,N1),and(FN,NCN,N2), or(N1,N2,N).
67 % Non deterministic selection (singleton 2nd order variable)
68 itl([],true,_,C,C):-!.
69 itl([H|L],F,empty,C,C1):-!,
70 empty_choice([H|L],0,F,C,C1).
71 empty_choice([H|_],N,F,C,[choice(N)|C1]) :-
72 itl(H,F,empty,C,C1).
73 empty_choice([_|L],N,F,C,C1) :-
74 N1 is N+1,
75 empty_choice(L,N1,F,C,C1).
76 itl([H|L],F,E,C,C1):-!,E=more,
77 choice([H|L],F,C,C1).
78 choice([],[],C,C) :-!.
79 choice([H|L],[H1|L1],C,C2) :-
80 itl(H,H1,more,C,C1),
81 choice(L,L1,C1,C2).
63 % Regular Variable 82 % Regular Variable
64 itl(^(R),F,empty,C,C1):- 83 itl(^(R),F,empty,C,C1):-
65 local(F0,up(R),C,C0), 84 local(F,^(R,0),C,C1).
66 local(F1,down(R,0),C0,C1),and(F0,F1,F). 85 itl(^(R),^(R,1),E,C,C):-!, E=more.
67 itl(^(R),F1,E,C,[^(R,0)|C1]):-!, E=more,
68 local(F,up(R),C,C1),and(F,^(R,0),F1).
69 86
70 itl(^(R,S),F,empty,C,C1):- 87 itl(^(R,S),F,empty,C,C1):-
71 local(F,down(R,S),C,C1). 88 local(F,^(R,S),C,C1).
72 itl(^(R,S),F,E,C,C1):- E = more, 89 %itl(^(R,S),F,E,C,C1):- E = more,
73 regular_limit(X),S>=X,!, 90 % length_limit(X),S>=X,inc_var(over,_),!,
74 local(F,over(R,S),C,C1). 91 % S1 is S+1,local(F,over(R,S1),C,C1).
75 itl(^(R,S),^(R,S1),E,C,[^(R,S1)|C]):-!, 92 itl(^(R,S),^(R,S1),E,C,C):-!,
76 % increment regular variable rength 93 % increment regular variable length
77 % mark reference to detect singleton
78 E=more, S1 is S+1. 94 E=more, S1 is S+1.
79 95
80 % Quantifier 96 % Quantifier
81 itl(exists(P,Q),F,E,C,C0) :-!, 97 itl(exists(P,Q),F,E,C,C0) :-!,
82 itl(Q,QT,E,[P|C],C1),itl_ex(QT,Q,E,P,F,C1,C0). 98 itl(Q,QT,E,[P|C],C1),itl_ex(QT,Q,E,P,F,C1,C0).
167 write('next empty conflict:'),write((PM,PE,F,Q,C)),nl,!, 183 write('next empty conflict:'),write((PM,PE,F,Q,C)),nl,!,
168 fail. 184 fail.
169 185
170 chop1(false,QF,_,QF):-!. 186 chop1(false,QF,_,QF):-!.
171 chop1(false,false,_,false):-!. 187 chop1(false,false,_,false):-!.
188 chop1(true,false,true,true):-!.
189 chop1(true,_,true,true):-!.
172 chop1(PM,false,Q,(PM&Q)):-!. 190 chop1(PM,false,Q,(PM&Q)):-!.
173 chop1(_,true,_,true):-!. 191 chop1(_,true,_,true):-!.
174 chop1(PM,QF,Q,(QF;(PM&Q))):-!. 192 chop1(PM,QF,Q,(QF;(PM&Q))):-!.
175 193
176 itl(proj(_,Q),F,empty,C,C1) :-!, 194 itl(proj(_,Q),F,empty,C,C1) :-!,
181 prj(PM,QM,P,F). 199 prj(PM,QM,P,F).
182 prj(false,_,_,false):-!. 200 prj(false,_,_,false):-!.
183 prj(_,false,_,false):-!. 201 prj(_,false,_,false):-!.
184 prj(PM,QM,P,(PM&proj(P,QM))). 202 prj(PM,QM,P,(PM&proj(P,QM))).
185 203
204 % prefix is not consistently defined
205 % prefix(fin(false)) = true ? funny...
186 itl(prefix(P),F,empty,C,C1) :-!, 206 itl(prefix(P),F,empty,C,C1) :-!,
187 itl(P,PE,empty,C,C0), 207 itl(P,PE,empty,C,C0),
188 itl(P,PM,more,C0,C1), 208 itl(P,PM,more,C0,C1),
189 prefix(PM,PE,F). 209 prefix(PM,PE,F).
190 itl(prefix(P),F,more,C,C1) :-!, 210 itl(prefix(P),F,more,C,C1) :-!,
201 prefix(_,false,true):-!. 221 prefix(_,false,true):-!.
202 222
203 itl(Def,_,_,_,_) :- 223 itl(Def,_,_,_,_) :-
204 write('error: '),write(Def),nl,!,fail. 224 write('error: '),write(Def),nl,!,fail.
205 225
206 % detect regular variable singleton
207 % we can do renumbering here
208 % what do we do for permutation?
209
210 itl_singleton([empty|L],[empty|L],[]) :- !.
211 itl_singleton(Cond,Cond1,Singleton) :- singleton,!,
212 select_singleton(Cond,Cond0,V),
213 split_singleton_case(V,Cond0,Cond1,Singleton).
214 itl_singleton(Cond,Cond1,[]) :-
215 select_singleton(Cond,Cond1,_).
216
217 select_singleton([],[],[]):-!.
218 select_singleton([^(R,S)|L],L1,V):-!,
219 check_singleton(L,^(R,S),L0,single,F),
220 (F==single -> V = [^(R,S)|V0],select_singleton(L0,L1,V0)
221 ; select_singleton(L0,L1,V)).
222 select_singleton([H|L],[H|L1],V):-!,
223 select_singleton(L,L1,V).
224
225 check_singleton([],_,[],F,F):-!.
226 check_singleton([H|T],H,T1,_,multi):-!,
227 check_singleton(T,H,T1,_,_).
228 check_singleton([H|T],H1,[H|T1],F,F1):-!,
229 check_singleton(T,H1,T1,F,F1).
230
231 % choose singleton's truth value
232 % split_singleton_case(_,Cond,Cond,[]) :- !.
233 split_singleton_case([],Cond,Cond,[]).
234 split_singleton_case([^(R,S)|T],Cond,Cond1,[(^(R,S),true)|T1]):-
235 split_singleton_case(T,[ev(^(R,S))|Cond],Cond1,T1).
236 split_singleton_case([^(R,S)|T],Cond,Cond1,[(^(R,S),false)|T1]):-
237 split_singleton_case(T,[not(ev(^(R,S)))|Cond],Cond1,T1).
238 226
239 % develop Local ITL formula into state diagram 227 % develop Local ITL formula into state diagram
240 % 228 %
241 % Mon May 20 17:24:23 BST 1991 229 % Mon May 20 17:24:23 BST 1991
242 % require([chop]). 230 % require([chop]).
243 231
244 :-dynamic verbose/0,state/2,links/2. 232 :-dynamic verbose/0,state/2,links/2.
245 :-dynamic stay/3,lazy/0,singleton/0. 233 :-dynamic stay/3,lazy/0,singleton/0,detailed/0.
246 234
247 :-assert(verbose).
248 verbose(off) :- retract(verbose),fail;true. 235 verbose(off) :- retract(verbose),fail;true.
249 verbose(on) :- asserta(verbose). 236 verbose(on) :- asserta(verbose).
237 :-verbose(on).
250 238
251 lazy(off) :- retract(lazy),fail;true. 239 lazy(off) :- retract(lazy),fail;true.
252 lazy(on) :- asserta(lazy). 240 lazy(on) :- asserta(lazy).
253 241
242 :-lazy(on).
243
254 singleton(off) :- retract(singleton),fail;true. 244 singleton(off) :- retract(singleton),fail;true.
255 singleton(on) :- asserta(singleton). 245 singleton(on) :- asserta(singleton).
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).
256 255
257 set_limit(X) :- 256 set_limit(X) :-
258 set_var(regular_limit,X,_). 257 set_var(length_limit,X,_).
258 no_limit :-
259 retract(length_limit),fail.
260 no_limit.
261
262 :-assert(length_limit(5)).
259 263
260 deve(ITL) :- 264 deve(ITL) :-
261 init,!, 265 init,!,
262 expand(ITL,ITL0), % chop standard form 266 expand(ITL,ITL0), % chop standard form
263 itlstd(ITL0,StdNOW), % BDT 267 itlstd(ITL0,StdNOW,_), % BDT
264 assert(itl_state(StdNOW,1)),!, % Initial State 268 assert(itl_state(StdNOW,1)),!, % Initial State
265 deve0((1,StdNOW)). 269 deve0((1,StdNOW)).
266 270
267 deve0((S,ITL)) :- 271 deve0((S,ITL)) :-
268 show_state(S,ITL), 272 show_state(S,ITL),
275 deve1([H|T]) :- deve0(H),deve1(T). 279 deve1([H|T]) :- deve0(H),deve1(T).
276 280
277 itldecomp(ITL,(NextS,StdNext),From) :- 281 itldecomp(ITL,(NextS,StdNext),From) :-
278 init_var(current,From), 282 init_var(current,From),
279 itl(ITL,Next,Cond), 283 itl(ITL,Next,Cond),
280 itl_singleton(Cond,Cond1,Singleton),
281 %% showing 284 %% showing
282 itlshow(Next,NextS,Cond1,From,StdNext,Singleton). 285 itlshow(Next,NextS,Cond,From,StdNext).
283 286
284 itlshow(Next,S,Cond,From,StdNext,Singleton):- 287 itlshow(Next,S,Cond,From,StdNext):-
285 itlstd(Next,StdNext,Singleton), 288 itlstd(Next,StdNext,Rename),
286
287 itlstd(Next,StdNext1,[]),
288 bdt2itl(StdNext,ItlNext),
289 bdt2itl(StdNext1,ItlNext1),
290 (ItlNext \== ItlNext1 -> write('>>'),
291 write(ItlNext),nl,write(' '),
292 write(ItlNext1),nl; true),
293
294 check_state(StdNext,Cond,New,S), 289 check_state(StdNext,Cond,New,S),
295 (lazy,!;assertz(state(From,Cond,S))), 290 (verbose,!,write(Rename);true),
296 (links(S,From),!;assertz(links(S,From))), 291 (links(S,From),!;
292 assertz(links(S,From)),inc_var(itl_transition_count,_)),
293 inc_var(itl_transition,_),
297 itlshow0(S,Cond,StdNext,New), 294 itlshow0(S,Cond,StdNext,New),
298 !. 295 !.
299 296
300 itlshow0(S,Cond,Next,New) :- verbose,!, 297 itlshow0(S,Cond,Next,New) :- verbose,!,
301 itlshow1(S,Cond,Next,New),nl,!,New=1. 298 itlshow1(S,Cond,Next,New),nl,!,New=1.
314 write(Cond),write('->'),write(S). 311 write(Cond),write('->'),write(S).
315 itlshow1(S,Cond,Org,1):- 312 itlshow1(S,Cond,Org,1):-
316 write(Cond),write('->'),write(S), 313 write(Cond),write('->'),write(S),
317 put(9),bdt2itl(Org,Org0),write(Org0),!. 314 put(9),bdt2itl(Org,Org0),write(Org0),!.
318 315
319 lazy_state(From,Cond,S) :- 316 % lazy transition condition generator
320 links(S,From), 317
318 state(From,Cond,Next) :-
319 links(Next,From),
321 itl_state(ITL,From), 320 itl_state(ITL,From),
322 itl(ITL,Next,Cond), 321 itl(ITL,Next0,Cond),
323 itlstd(Next,StdNext), 322 itlstd(Next0,StdNext,_),
324 check_state(StdNext,Cond,_,S). 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.
325 334
326 init :- 335 init :-
327 subterm_init, 336 subterm_init,
328 abolish(state,3),
329 asserta((state(true,[more],true):-!)),
330 asserta((state(true,[empty],0):-!)),
331 (lazy,assertz((state(A,B,C) :- lazy_state(A,B,C))),!;true),
332 abolish(itl_state,2), 337 abolish(itl_state,2),
333 abolish(stay,3),asserta(stay(0,0,0)), 338 abolish(stay,3),asserta(stay(0,0,0)),
334 asserta(itl_state(false,false)), 339 asserta(itl_state(false,false)),
335 asserta(itl_state(empty,0)), 340 asserta(itl_state(empty,0)),
336 asserta(itl_state(true,true)), 341 asserta(itl_state(true,true)),
337 abolish(links,2),asserta(links(true,true)), 342 abolish(links,2),asserta(links(true,true)),
338 init_var(current,0), 343 init_var(current,0),
339 init_var(regular_limit,5), 344 init_var(over,0),
345 init_var(itl_transition,0),
346 init_var(itl_transition_count,0),
340 init_var(itl_state_number,1),!. 347 init_var(itl_state_number,1),!.
341 348
342 show_state(S,ITL) :- 349 show_state(S,ITL) :-
343 bdt2itl(ITL,ITL0), 350 bdt2itl(ITL,ITL0),
344 nl,write('state('),write(S), % ( 351 nl,write('state('),write(S), % (
351 itl_state(STD,S),!. 358 itl_state(STD,S),!.
352 check_state(STD,_,1,S):- 359 check_state(STD,_,1,S):-
353 inc_var(itl_state_number,S), 360 inc_var(itl_state_number,S),
354 assert(itl_state(STD,S)),!. 361 assert(itl_state(STD,S)),!.
355 362
356 init_var(X,_) :- functor(F,X,1),assert(F),fail. 363 init_var(X,V) :- abolish(X,1),functor(F,X,1),arg(1,F,V),assert(F),!.
357 init_var(X,_) :- functor(F,X,1),retract(F),fail.
358 init_var(X,V) :- functor(F,X,1),arg(1,F,V),assert(F),!.
359 inc_var(Name,X1) :- 364 inc_var(Name,X1) :-
360 functor(F,Name,1),retract(F),arg(1,F,X), 365 functor(F,Name,1),retract(F),arg(1,F,X),
361 X1 is X+1,functor(F1,Name,1),arg(1,F1,X1), 366 X1 is X+1,functor(F1,Name,1),arg(1,F1,X1),
362 asserta(F1),!. 367 asserta(F1),!.
363 set_var(Name,X,X1) :- 368 set_var(Name,X,X1) :-
364 functor(F,Name,1),retract(F),!,arg(1,F,X), 369 functor(F,Name,1),retract(F),!,arg(1,F,X),
365 functor(F1,Name,1),arg(1,F1,X1),asserta(F1),!. 370 functor(F1,Name,1),arg(1,F1,X1),asserta(F1),!.
366 set_var(Name,X,_) :- init_var(Name,X). 371 set_var(Name,X,_) :- init_var(Name,X).
367 372
368 %init_var(X,_) :- recorded(X,_,Ref),erase(Ref),fail.
369 %init_var(X,V) :- recorda(X,V,_).
370 %inc_var(Name,X1) :-
371 % recorded(Name,X,Ref),X1 is X+1,
372 % erase(Ref),recorda(Name,X1,_).
373 %set_var(Name,X,X1) :-
374 % recorded(Name,X1,_),!,init_var(Name,X).
375 %set_var(Name,X,_) :- init_var(Name,X).
376 373
377 itl_statistics :- nl, 374 itl_statistics :- nl,
378 itl_state_number(X),write(X),write(' states'),nl,fail. 375 itl_state_number(X),write(X),write(' states'),nl,fail.
379 itl_statistics :- 376 itl_statistics :-
380 sbn(X),write(X),write(' subterms'),nl,fail. 377 sbn(X),write(X),write(' subterms'),nl,fail.
381 itl_statistics :- 378 itl_statistics :-
382 init_var(tmp,0), 379 itl_transition_count(X),
383 ((links(_,_),inc_var(tmp,_),fail);true), 380 write(X),write(' state transions'),nl,fail.
384 tmp(N), 381 itl_statistics :-
385 write(N),write(' state transions'),nl,fail. 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.
386 itl_statistics. 393 itl_statistics.
387 394
388 %% end %% 395 %% end %%