Mercurial > hg > Applications > JavaLite
view src/sbdd/BDDSatisfier.java @ 79:c263dc76d1a7
comments
author | kono |
---|---|
date | Thu, 17 Jan 2008 11:09:19 +0900 |
parents | 147864a924cd |
children | 400185be1a60 |
line wrap: on
line source
package sbdd; import java.util.LinkedList; import parser.ExecutorInterface; import verifier.Backtrack; import verifier.ChoicePointList; import lite.BDDSolver; import lite.Continuation; import lite.ITLNodeFactory; import lite.ITLNodeFactoryInterface; import lite.ITLNodeParser; import lite.ITLSatisfier; import lite.ITLSolver; import lite.Next; import lite.VariableSolver; 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; /** * 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() { lf = new ITLNodeFactory(); p = new ITLNodeParser<ITLSolver>((ITLNodeFactoryInterface<ITLSolver>) lf); sf = new SBDDFactory(); empty = lf.emptyNode(); } public BDDSatisfier() { init(); lf = new SBDDFactory(); true_ = SBDDFactory.trueSolver; false_ = SBDDFactory.falseSolver; state = sf.set(); state.getEntry(SBDDFactory.trueSolver).expanded = true; state.getEntry(SBDDFactory.falseSolver).expanded = true; state.getEntry(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(sf.hash); System.out.println(); } class AllNext implements Next { public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { 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; } } 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; } } class AllNextVerbose implements Next { public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { String s = "null"; System.out.print(" "+sat.choicePoint()+" -> "); 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; } } public void verify(ITLSolver n) { 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; 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(); } } public SBDDEntry getEntry(ITLSolver key) { return sf.hash.getEntry(key); } public ChoicePointList<ITLSolver> findNext(SBDDEntry e, SBDDEntry entry) { // TODO Auto-generated method stub return null; } }