Mercurial > hg > Applications > Lite
view bddcomp.pl @ 22:29cf617f49db default tip
newer CVS version
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 22 Apr 2016 16:47:13 +0900 |
parents | 07d6c4c5654b |
children |
line wrap: on
line source
/* Copyright (C) 1991, Shinji Kono, Sony Computer Science Laboratory, Inc. The University, Newcastle upton Tyne Everyone is permitted to copy and distribute verbatim copies of this license, but changing it is not allowed. You can also use this wording to make the terms for other programs. send your comments to kono@csl.sony.co.jp $Id: bddcomp.pl,v 1.2 2007/08/30 05:16:36 kono Exp $ */ % itl decomposition for DST :- use_module('~/ITL/bdd/sicstus/bdd'). % requires [chop] % itl(Predicate,Next,Empty,ConditionLists) itl(P) :- expand(P,P0), moref(Ev),itl(P0,Next,Ev,[],C), write(([Ev|C]->Next)),nl,fail. itl(_). itl(P,Next,[Ev|C]) :- moref(Ev),itl(P,Next,Ev,[],C). moref(empty). moref(more). itl(N,F,E,C,C1):-integer(N),!, bdd2itl1(N,Term),!,itl(Term,F,E,C,C1). itl(true,true,_,C,C):-!. itl(false,false,_,C,C):-!. itl(more,false,empty,C,C). itl(more,true,E,C,C):-!,E = more. % next two rule determines descrete time itl(empty,true,empty,C,C). itl(empty,false,E,C,C):-!,E = more. % no succeeding more interval itl(P,FF,_,C,C1) :- atomic(P),!, local(FF,P,C,C1). local(true,P,C,C1):- true(C,P,C,C1). true([],P,C,[P|C]):-!. true([P|_],P,C,C):-!. true([not(P)|_],P,_,_):-!,fail. true([_|T],P,C,C1):-true(T,P,C,C1). local(false,P,C,C1):- false(C,P,C,C1). false([],P,C,[not(P)|C]):-!. false([P|_],P,_,_):-!,fail. false([not(P)|_],P,C,C):-!. false([_|T],P,C,C1):-false(T,P,C,C1). itl(@(P),P,more,C,C). % strong next itl(@(_),false,E,C,C):-!,E=empty. itl(?(Cond,T,F),N,E,C,C1):-!, itl(Cond,CN,E,C,C0),itl_cond(CN,T,F,N,E,C0,C1). itl_cond(true,T,_,N,E,C,C1) :-!, itl(T,N,E,C,C1). itl_cond(false,_,F,N,E,C,C1) :-!, itl(F,N,E,C,C1). itl_cond(CN,T,F,N,E,C,C1) :-!, itl(T,TN,E,C,C0), itl(F,FN,E,C0,C1), negate(CN,NCN), and(TN,CN,N1),and(FN,NCN,N2), or(N1,N2,N). % Quantifier itl(exists(P,Q),F,E,C,C0) :-!, itl(Q,QT,E,[P|C],C1),itl_ex(QT,Q,E,P,F,C1,C0). itl_ex(true,_,_,P,true,C,C1):-!,remove_p(C,P,C1). itl_ex(false,Q,E,P,F,C,C0):- !,remove_p(C,P,C1), itl(Q,QF,E,[not(P)|C1],C2),remove_p(C2,P,C0), exists(QF,P,F). itl_ex(QT,Q,E,P,F,C,C0):- remove_p(C,P,C1), itl(Q,QF,E,[not(P)|C1],C2), remove_p(C2,P,C0), or(QT,QF,TF),exists(TF,P,F). % constant order optimzation for quantifier exists(P,P,true):-!. exists(P,_,P):-atomic(P),!. exists(Q,P,exists(P,Q)). remove_p([],_,[]):-!. remove_p([not(P)|T],P,T):-!. remove_p([P|T],P,T):-!. remove_p([H|T],P,[H|T1]):-!,remove_p(T,P,T1). itl(*(P),F,empty,C,C1):-!,itl(P,F,empty,C,C1). itl(*(P),F,E,C,C1):-!,E=more, itl(P,PX,more,C,C1), closure(PX,P,F). closure(false,_,false):-!. closure(PX,P,(PX & *(P))). %% infinite clousre (strong) %% closure(PX,P,(PX & (*(P);empty))). %% finite closure (weak) %% external state diagram itl(st(N),F,E,C,C1):-!, setof((Cond=>X),st(N,Cond,X),L),itl_transition(L,F,E,C,C1). itl_transition([],false,_,C,C):-!. itl_transition([(Cond=>empty)|T],F,E,C,C1):-!, itl((empty,Cond),F0,E,C,C0), itl_transition(T,F1,E,C0,C1),or(F0,F1,F). itl_transition([(Cond=>X)|T],F,E,C,C1):- itl((more,Cond),F0,E,C,C0), itl_transition1(F0,X,T,F,E,C0,C1). itl_transition1(false,_,T,F,E,C,C1):- itl_transition(T,F,E,C,C1). itl_transition1(true,X,T,(st(X);F),E,C,C1):- itl_transition(T,F,E,C,C1). %% shared resources or state itl(share(L),F,empty,C,C1):-!, exclusive(L,C,C1,true,F). itl(share(L),F,more,C,C1):-!, exclusive(L,C,C1,share(L),F). exclusive([],C,C,F,F):-!. exclusive([A|L],C,C1,F,F1):- true(C,A,C,C0),exclusive1(L,C0,C1,F,F1). exclusive([N|L],C,C1,F,F1):- false(C,N,C,C0), !,exclusive(L,C0,C1,F,F1). % exclusive(_,C,C,_,false). % eliminate this brach exclusive1([],C,C,F,F):-!. exclusive1([H|L],C,C1,F,F1):- false(C,H,C,C0), !,exclusive1(L,C0,C1,F,F1). % exclusive1(_,C,C,_,false). %% itl((P,Q),N,E,C,C1) :-!, itl(P,PN,E,C,C0),itland(PN,Q,N,E,C0,C1). itland(false,_,false,_,C0,C0):-!. itland(true,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1). itland(PN,Q,N,E,C0,C1):- itl(Q,QN,E,C0,C1),and(PN,QN,N). %% and/3 in chop.pl itl((P;Q),N,E,C,C1) :-!, itl(P,PN,E,C,C0),itlor(PN,Q,N,E,C0,C1). itlor(true,_,true,_,C0,C0):-!. itlor(false,Q,QN,E,C0,C1):-!,itl(Q,QN,E,C0,C1). itlor(PN,Q,N,E,C0,C1):- itl(Q,QN,E,C0,C1),or(PN,QN,N). %% or/3 in chop.pl itl(not(P),NN,E,X,X1) :- !, itl(P,N,E,X,X1), negate(N,NN). %% negate/2 in chop.pl % F = empty?(P,Q):(empty(P)*more(Q)+more(PM)&Q) itl((P&Q),F,empty,C,C1) :-!, itl((P,Q),F,empty,C,C1). itl((P&Q),F,more,C,C2) :-!, itl(P,PE,empty,C,C0), itl(P,PM,more,C0,C1), chop(PM,PE,F,Q,C1,C2). chop(false,false,false,_,C,C):-!. chop(PM,false,(PM & Q),Q,C,C):-!. chop(PM,true,F,Q,C,C1):-!, itl(Q,QF,more,C,C1), chop1(PM,QF,Q,F). chop(PM,PE,F,Q,C,C):-!, write('next empty conflict:'),write((PM,PE,F,Q,C)),nl,!, fail. chop1(false,QF,_,QF):-!. chop1(false,false,_,false):-!. chop1(PM,false,Q,(PM&Q)):-!. chop1(_,true,_,true):-!. chop1(PM,QF,Q,(QF;(PM&Q))):-!. itl(proj(_,Q),F,empty,C,C1) :-!, itl(Q,F,empty,C,C1). itl(proj(P,Q),F,more,C,C1) :-!, itl(P,PM,more,C,C0), itl(Q,QM,more,C0,C1), prj(PM,QM,P,F). prj(false,_,_,false):-!. prj(_,false,_,false):-!. prj(PM,QM,P,(PM&proj(P,QM))). itl(prefix(P),F,empty,C,C1) :-!, itl(P,PE,empty,C,C0), itl(P,PM,more,C0,C1), prefix(PM,PE,F). itl(prefix(P),F,more,C,C1) :-!, itl(P,PM,more,C,C1), prefix(PM,F). prefix(true,true):-!. prefix(false,false):-!. prefix(PM,prefix(PM)):-!. prefix(true,_,true):-!. prefix(_,true,true):-!. prefix(false,false,false):-!. prefix(_,false,true):-!. itl(Def,_,_,_,_) :- write('error: '),write(Def),nl,!,fail. % develop Local ITL formula into state diagram % % Mon May 20 17:24:23 BST 1991 % require([chop]). :-dynamic verbose/0,state/2,links/2. :-dynamic stay/3,lazy/0. :-assert(verbose). verbose(off) :- retract(verbose),fail;true. verbose(on) :- asserta(verbose). lazy(off) :- retract(lazy),fail;true. lazy(on) :- asserta(lazy). % A \= A :-!,fail. % _ \= _. deve(ITL) :- init,!, expand(ITL,ITL0), % chop standard form itl2bdd(ITL0,StdNOW), % BDD assert(itl_state(StdNOW,1)),!, % Initial State deve0((1,StdNOW)). deve0((S,ITL)) :- show_state(S,ITL), setof(Next,itldecomp(ITL,Next,S), Nexts),!, deve1(Nexts). deve0(_). deve1([]). deve1([H|T]) :- deve0(H),deve1(T). itldecomp(ITL,(NextS,StdNext),From) :- init_var(current,From), itl(ITL,Next,Cond), %% showing itlshow(Next,NextS,Cond,From,StdNext). itlshow(Next,S,Cond,From,StdNext):- itl2bdd(Next,StdNext), check_state(StdNext,Cond,New,S), (lazy,!;assertz(state(From,Cond,S))), (links(S,From),!;assertz(links(S,From))), !, itlshow0(S,Cond,StdNext,New). itlshow0(S,Cond,Next,New) :- verbose,!, itlshow1(S,Cond,Next,New),nl,!,New=1. itlshow0(0,_,_,0):- !,put("e"),!,fail. itlshow0(false,_,_,0):- !,put("f"),!,fail. itlshow0(true,_,_,0):- !,put("t"),!,fail. itlshow0(_,_,_,0):- !,put("."),!,fail. itlshow0(S,_,_,1):- !,write(S),put("."),ttyflush,!. itlshow1(0,Cond,_,_):-!, write(Cond),write('->'),write(empty). itlshow1(true,Cond,_,_):-!, write(Cond),write('->'),write(true). itlshow1(false,Cond,_,_):-!, write(Cond),write('->'),write(false). itlshow1(S,Cond,_,0):-!, write(Cond),write('->'),write(S). itlshow1(S,Cond,Org,1):- write(Cond),write('->'),write(S), bdd2itl(Org,S1),put(9),write(S1),!. lazy_state(From,Cond,S) :- links(S,From), itl_state(ITL,From), itl(ITL,Next,Cond), itl2bdd(Next,StdNext), check_state(StdNext,Cond,_,S). init :- subterm_init, r_abolish(state,3), asserta((state(true,[more],true):-!)), asserta((state(true,[empty],0):-!)), (lazy,assertz((state(A,B,C) :- lazy_state(A,B,C))),!;true), r_abolish(itl_state,2), r_abolish(stay,3),asserta(stay(0,0,0)), bdd:zero(F), bdd:one(T), asserta(itl_state(F,false)), asserta(itl_state(empty,0)), asserta(itl_state(T,true)), r_abolish(links,2),asserta(links(true,true)), init_var(itl_state_number,1),!. show_state(S,ITL) :- bdd2itl(ITL,ITL0), nl,write('state('),write(S), % ( (verbose,write(' , '), write(ITL0),write(')'),nl;write(')')),!. check_state(true,[more |_],0,true):-!. check_state(true,[empty|_],0,0):-!. check_state(false,_,0,-2):-!. check_state(STD,_,0,S):- itl_state(STD,S),!. check_state(STD,_,1,S):- inc_var(itl_state_number,S), assert(itl_state(STD,S)),!. init_var(X,_) :- functor(F,X,1),assert(F),fail. init_var(X,_) :- functor(F,X,1),retract(F),fail. init_var(X,V) :- functor(F,X,1),arg(1,F,V),assert(F),!. inc_var(Name,X1) :- functor(F,Name,1),retract(F),arg(1,F,X), X1 is X+1,functor(F1,Name,1),arg(1,F1,X1), asserta(F1),!. increment_state(stay(P,now),stay(P,S),S) :- !, (stay(P,F,S);assertz(stay(P,F,S))),!. increment_state(N,N,_) :- atomic(N),!. increment_state(P,R,S) :- functor(P,H,N),functor(R,H,N), increment_state_arg(N,P,R,S). increment_state_arg(0,_P,_R,_):-!. increment_state_arg(N,P,R,S):-arg(N,P,PA),arg(N,R,RA), N1 is N-1,increment_state(PA,RA,S), increment_state_arg(N1,P,R,S). itl_statistics :- nl, itl_state_number(X),write(X),write(' states'),nl,fail. itl_statistics :- sbn(X),write(X),write(' subterms'),nl,fail. itl_statistics :- init_var(tmp,0), ((links(_,_),inc_var(tmp,_),fail);true), tmp(N), write(N),write(' state transitions'),nl,fail. itl_statistics. %% end %%