Mercurial > hg > Applications > JavaLite
view src/lite/ITLNodeParser.java @ 67:4ced2af1ff09 bdd-order
BDD Order fix
author | kono |
---|---|
date | Sun, 13 Jan 2008 19:48:42 +0900 |
parents | 96b1c8c2f9b9 |
children | 5fd456b0a073 |
line wrap: on
line source
package lite; import java.util.LinkedList; import sbdd.SBDDFactory; import logicNode.parser.Command; import logicNode.parser.Dictionary; import logicNode.parser.LogicNodeScope; import logicNode.parser.MacroNodeParser; import logicNode.parser.Token; import logicNode.parser.TokenID; public class ITLNodeParser<Node extends ITLSolver> extends MacroNodeParser<Node> { public ITLNodeFactoryInterface<Node> logicNodeFactory; public ITLNodeScanner<Node> scanner; public ITLCommander<Node> parseCommand; public Node emptyNode; private Node periodNode; public ITLNodeParser(ITLNodeFactoryInterface<Node> lf) { super(lf); logicNodeFactory = lf; initialize(); Token<Node> emptyToken = dict.reserve("empty",TokenID.Empty); emptyNode = emptyToken.value = logicNodeFactory.emptyNode(); parseCommand = new ITLCommander<Node>(lf,this); define("not(P)","~P"); // not define("P->Q","(not(P);Q))"); // imply define("P<->Q","((not(P);Q),(P; not(Q)))"); // equiv define("P=Q","((not(P);Q),(P; not(Q)))"); // equiv define("P && Q","((not(empty),P) & Q))"); // strong chop define("'<>'(Q)","(true & Q))"); // sometime define("'#'(Q)"," not(true & not(Q)))"); // always define("'[]'(Q)"," not(true & not(Q)))"); // always define("'[a]'(Q)"," not(true & not(Q) & true))"); // always with arbitary fin define("'<a>'(Q)"," (true & Q & true))"); // sometime with arbitary fin define("fin(Q)","(true & (empty,Q)))"); // final state in the interval define("keep(Q)"," not(true & not((empty ; Q))))"); // except final state define("halt(Q)"," '[]'(empty=Q))"); define("more"," not(empty))"); // non empty interval // discrete stuff define("skip"," @(empty))"); // 1 length interval define("infinite"," (true & false))"); // define("finite"," ~((true & false)))"); // // define("length(I)", "true",50,command); // length operator define("length(I)", "empty",50, // length operator new Command<Node>() { public Node exec(Node predicate, Node value, LinkedList<Node> args) { Node n = value; int length = Integer.parseInt(args.get(0).toString()); for(int i =0;i<length;i++) { n = logicNodeFactory.nextNode(n); } return n; } }); define("less(I)","false",50,parseCommand); // less than N length define("next(P)","(empty; @(P)))"); // temporal assignments define("gets(A,B)","keep(@A<->B))"); define("stable(A)","keep(@A<->A))"); // define("state(A)","(share(A),'[]'(L))):- def_state(A,L)"); // def(Q=>P,exists(R,(Q = R,stable(R),fin(P = R))))"); // easier one define("Q=>P","(Q & (empty,P); ~Q & (empty, ~P)))"); // def(P<=Q,Q=>P)"); // loop stuff and quantifiers define("*(A) ","proj(A,true),fin(A)"); // weak closure define("+(A) ","A& *(empty;A)"); // strong closure //define("+(A) ","A & proj(A,true)"); // strong closure define("while(Cond,Do)"," *(((Cond->Do) , (~Cond->empty))))"); define("repeat(Do,until,Cond)"," (*((Do;empty)) ,@ halt(Cond)))"); define("all(P,Q)","not(exists(P,not(Q)))"); define("local(P)"," (P = (P&true))"); // test predicates // define("trace(X,List),L) :- !,make_trace(List,X,L)"); define("even(P)","exists(Q,(Q, keep( @Q = ~Q),'[]'((Q->P)))))"); define("evenp(P)","(*(((P,skip) & skip;empty,P)) & (empty;skip)))"); define("phil(L,R)","+('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) ))"); define("ex(N,Exp)","true",50,parseCommand); define("def(Head,Body,Order)","true",50,parseCommand); define("include(path)","true",50,parseCommand); define("ex0(N,Exp)","skipped"); define("verbose(I)", "true",50,parseCommand); define("^(r)","r"); // interval variable (we cannot handle now) periodNode = logicNodeFactory.variableNode(".", true); // only one of the is true (should allow all false case?) define("share(L)","[](share0(L))"); define("share0(L)","true",50, new Command<Node>() { @SuppressWarnings({ "unchecked", "unchecked" }) public Node exec(Node predicate, Node value, LinkedList<Node> args) { Node allFalse = (Node)SBDDFactory.trueSolver; value= (Node)SBDDFactory.falseSolver; LinkedList<ITLSolver> list = args.get(0).arguments(); if (list.isEmpty()) return value; for(ITLSolver n: list) { Node n1 = (Node)n; value = logicNodeFactory.bddNode(n1, allFalse, value); allFalse = logicNodeFactory.bddNode(n1, (Node)SBDDFactory.falseSolver,allFalse); } return value; } }); } public ITLNodeParser() { super(); } @Override public void initialize() { dict = new Dictionary<Node>(); scope = new LogicNodeScope<Node>(null,dict); initReservedWord(); scanner = new ITLNodeScanner<Node>(dict); super.scanner = scanner; dict.reserve("&",TokenID.Chop); dict.reserve("@",TokenID.Next); dict.reserve("proj",TokenID.Projection); // parseCommand requires reserved word for string comparison dict.reserve("less"); dict.reserve("ex"); dict.reserve("include"); dict.reserve("def"); dict.reserve("verbose"); } @Override public Node expr2() { Node n = exprI2(); while(nextToken.type==TokenID.And) { nextToken(); n = logicNodeFactory.andNode(n, exprI2()) ; } return n; } @Override public Node expr3() { Node n = super.expr3(); while(nextToken.type==TokenID.Question) { nextToken(); Node cond = n; Node high = expr3(); if (nextToken.type!=TokenID.Colon) { error(": expected"); return logicNodeFactory.trueNode(); } nextToken(); Node low = expr3(); n = logicNodeFactory.orNode( logicNodeFactory.andNode(cond, high), logicNodeFactory.andNode(logicNodeFactory.notNode(cond), low)); } return n; } @Override public Node expr4() { if (nextToken.type == TokenID.Next) { nextToken(); return logicNodeFactory.nextNode(expr4()); } return super.expr4(); } @Override public Node term() { if (nextToken.type==TokenID.BParen) { Node predicate = periodNode; nextToken(); LinkedList<Node> arg = arguments(); return logicNodeFactory.predicateNode(predicate, arg); } return super.term(); } public Node exprI2() { Node n = exprM1(); while(nextToken.type == TokenID.Chop) { nextToken(); n = logicNodeFactory.chopNode(n, exprM1()); } return n; } @Override protected LinkedList<Node> arguments() { Node n; LinkedList<Node> arg = new LinkedList<Node>(); while(nextToken.type!=TokenID.CloseParen&&nextToken.type!=TokenID.CloseBParen) { if (nextToken.type==TokenID.NULL) break; n = exprI2(); arg.add(n); if (nextToken.type == TokenID.And) nextToken(); } if (nextToken.type==TokenID.CloseParen|| nextToken.type==TokenID.CloseBParen) nextToken(); else { scanner.error(") expected"); } return arg; } /* @Override protected Node term() { Node n; switch (nextToken.type) { case Next: case Empty: case Chop: case Length: case Less: case Exec: case Define: case Include: case Closure: case Projection: n = makeVariable(nextToken); break; default: return super.term(); } nextToken(); return n; } */ public ITLSolver emptyNode() { return emptyNode; } }