Mercurial > hg > Applications > JavaLite
view src/sbdd/BDDSatisfier.java @ 88:6b3535ea6958
*** empty log message ***
author | kono |
---|---|
date | Fri, 18 Jan 2008 16:00:37 +0900 |
parents | e70b8c36ec0a |
children | 5bd5c58edfd0 |
line wrap: on
line source
package sbdd; import java.util.Date; import java.util.LinkedList; import parser.ExecutorInterface; import verifier.Backtrack; import verifier.ChoicePointList; import lite.BDDSolver; import lite.Continuation; import lite.ITLNodeFactory; import lite.ITLNodeParser; import lite.ITLSatisfier; import lite.ITLSolver; import lite.Next; public class BDDSatisfier extends ITLSatisfier implements ExecutorInterface<ITLSolver> { public ITLNodeParser<ITLSolver> p; public SBDDFactory sf; public LinkedList<SBDDEntry> queue; public SBDDSet state; public SBDDEntry currentState; public SBDDEntry last; boolean falsifiable,satisfiable; int edge; /** * Tableau expansion verifier for ITL with Subterm BDD. * * develop() try to find satisfiable choice point list for the ITL * formula. allNext() stores generated next time ITL formula in * a queue and SBDD Hash table ( SBDDEntry ). verify() repeats * develop() over the queue, until no more new states are generated. * * If we have no true in SBDD Hash, the formula is unsatisfiable. * These are checked by BDDDiagnosis. * */ private static final long serialVersionUID = 1L; public void init() { p = new ITLNodeParser<ITLSolver>(new ITLNodeFactory()); sf = new SBDDFactory(); edge = 0; } public BDDSatisfier() { init(); lf = sf; // this is strage. // the parser uses ITLNodeFactory for syntax tree, but in Satisfier, // SBDDFactory have be used. true_ = SBDDFactory.trueSolver; false_ = SBDDFactory.falseSolver; state = sf.set(); state.getEntry(SBDDFactory.trueSolver).expanded = true; state.getEntry(SBDDFactory.falseSolver).expanded = true; state.getEntry((empty=SBDDFactory.emptySolver)).expanded = true; } public void showAllNext(String s) { ITLSolver n = p.parse(s); BDDSolver b = n.toSBDD(sf); System.out.println(b); develop(b, new Print()); // System.out.println(sf.hash); System.out.println(); } class Print implements Next { public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { System.out.println(" "+sat.choicePoint()+" -> "+value); throw sat.backtrack; } } public void showVerify(String s) { ITLSolver n = p.parse(s); BDDSolver b = n.toSBDD(sf); System.out.println(s); verify(b); System.out.println(); } class AllNext implements Next { public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { edge++; if (value!=null) { if (value==true_) satisfiable = true; SBDDEntry e = state.getEntry(value); currentState.addNext(e); if (e.expanded) { System.out.print((e.key==sat.true_)?"t":"."); } else { queue.add(e); e.expanded = true; System.out.print(e.id+" "); } } else { System.out.print("f"); falsifiable = true; } throw sat.backtrack; } } class AllNextVerbose implements Next { public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { String s = "null"; System.out.print(" "+sat.choicePoint()+" -> "); edge++; if (value!=null) { if (value==true_) { s="true";satisfiable = true; } else { SBDDEntry e = state.getEntry(value); currentState.addNext(e); s = value.toString(); s = Integer.toString(e.id)+":"+s; if (e.expanded) { // skip } else { queue.add(e); e.expanded = true; s = "!"+s; } } } else { falsifiable = true; } System.out.println(s); throw sat.backtrack; } } /* * Do tableau expansion on an ITL formula * use develop to find out all possible next * store them in SBDDSet. If no more new next * states, all done. */ public void verify(ITLSolver n) { Date start = new Date(); queue = new LinkedList<SBDDEntry>(); Next allNext = verbose? new AllNextVerbose() : new AllNext(); SBDDEntry b = state.getEntry(n); last = b; if (b.expanded) { // already checked System.out.println(" already checked."); return; } queue.add(b); b.expanded = true; for(SBDDEntry e;(e = queue.poll())!=null; ) { System.out.println(e.id+":"+(verbose?e.key+"->":"")); currentState = e; falsifiable=false; satisfiable = false; cp.clear(); // all choice point is searched and removed develop(e.key, allNext); // this flag is work on current state // to check validity/unsatisfiability, full check is required. e.falsifiable = falsifiable; e.satisfiable = satisfiable; if (!verbose) System.out.println(); } Date end = new Date(); String time = Long.toString(end.getTime()-start.getTime()); if (!verbose) System.out.println("done in "+time+"msec"); } public SBDDEntry getEntry(ITLSolver key) { return sf.hash.getEntry(key); } /* SBDDEntry does not contains choice point set * i.e. transition condition represented by true/false combination of * variables. Choice point have to be generated on the fly. Condition * Edge is 2^(number of variable), so it is not good to have all in * memory. findNext generate choice point on the fly. */ class FindOne implements Next { SBDDEntry dest; public ChoicePointList<ITLSolver> cp; public FindOne(SBDDEntry next) { this.dest = next; } public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { if (value!=null && state.getEntry(value)==dest) { cp = sat.cp; return null; } throw sat.backtrack; } } public ChoicePointList<ITLSolver> findNext(SBDDEntry now, SBDDEntry next) { FindOne findOne = new FindOne(next); cp.clear(); develop(now.key, findOne); return findOne.cp; } // Find all possible choice points // // public ChoicePointList<ITLSolver> copy(ChoicePointList<ITLSolver> cplist) { // ChoicePointList<ITLSolver> newcp = new ChoicePointList<ITLSolver>(); // for(ITLSolver cp : cplist) { // newcp.add(new VariableSolver(cp.toString(),cp.value)); // } // return newcp; //// } // // class FindNext extends LinkedList<ChoicePointList<ITLSolver>> implements Next { // private static final long serialVersionUID = 1L; // public SBDDEntry dest; // FindNext(SBDDEntry dest) { this.dest = dest; } // public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { // if (value!=null&&value!=true_) { // SBDDEntry e = state.getEntry(value); // if (e.expanded) { // add(copy(sat.cp)); // } // } // throw sat.backtrack; // } // } }