Mercurial > hg > Applications > JavaLite
changeset 79:c263dc76d1a7
comments
author | kono |
---|---|
date | Thu, 17 Jan 2008 11:09:19 +0900 |
parents | 70cc3ff5c73b |
children | fb6eee69a232 |
files | src/sbdd/BDDSatisfier.java src/sbdd/SBDDEntry.java src/sbdd/SBDDFactory.java src/sbdd/SBDDSet.java |
diffstat | 4 files changed, 25 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- a/src/sbdd/BDDSatisfier.java Thu Jan 17 11:09:15 2008 +0900 +++ b/src/sbdd/BDDSatisfier.java Thu Jan 17 11:09:19 2008 +0900 @@ -31,6 +31,15 @@ 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; @@ -39,10 +48,7 @@ public void init() { lf = new ITLNodeFactory(); p = new ITLNodeParser<ITLSolver>((ITLNodeFactoryInterface<ITLSolver>) lf); - // p.setExecutor(this); sf = new SBDDFactory(); - // empty = ITLNodeFactory.emptySolver; - // empty = SBDDFactory.emptySolver; empty = lf.emptyNode(); }
--- a/src/sbdd/SBDDEntry.java Thu Jan 17 11:09:15 2008 +0900 +++ b/src/sbdd/SBDDEntry.java Thu Jan 17 11:09:19 2008 +0900 @@ -16,6 +16,21 @@ public boolean falsifiable; public boolean satisfiable; + /* + * Hash Table Entry for Subterm BDD + * subterm? high : low + * + * Subterm BDD represents a state in ITL, which is an ITL + * formula. It is ordered, so if it is the same it has same + * tree and the same hash entry. + * + * All subterm is ITLSolver now. getValue() returns itself. + * key subterm has sequence number (order field), it is used + * as variable order in BDDSolver. + * + * nexts contains possible next states. used in BDDDiagnosis. + */ + public SBDDEntry(ITLSolver now) { this.key = now; nexts = new LinkedList<SBDDEntry>();
--- a/src/sbdd/SBDDFactory.java Thu Jan 17 11:09:15 2008 +0900 +++ b/src/sbdd/SBDDFactory.java Thu Jan 17 11:09:19 2008 +0900 @@ -12,10 +12,6 @@ public static final ITLSolver trueSolver = new BDDSolver(ITLNodeFactory.trueSolver,BDDID.True,TokenID.True.hash); public static final ITLSolver falseSolver = new BDDSolver(ITLNodeFactory.falseSolver,BDDID.False,TokenID.False.hash); - //public static final ITLSolver chopSolver = new BDDSolver(BDDID.Chop,TokenID.Chop.hash); - //public static final ITLSolver existsSolver = new BDDSolver(BDDID.Exists,TokenID.Exists.hash); - //public static final ITLSolver nextSolver = new BDDSolver(BDDID.Next,TokenID.Next.hash); - //public static final ITLSolver projSolver = new BDDSolver(BDDID.Projection,TokenID.Projection.hash); public static final ITLSolver emptySolver = new BDDSolver(ITLNodeFactory.emptySolver,trueSolver,falseSolver,BDDID.BDD); public SBDDSet hash; ITLNodeFactory itlf; @@ -27,22 +23,14 @@ void init() { hash = new SBDDSet(this); itlf = new ITLNodeFactory(); - // emptySolver = new BDDSolver(ITLNodeFactory.emptySolver,BDDID.Empty,TokenID.Empty.hash); - + hash.put(falseSolver); hash.put(trueSolver); - //hash.put(existsSolver); - //hash.put(nextSolver); - //hash.put(chopSolver); hash.put(emptySolver); - //hash.put(projSolver); } public ITLSolver bddNode(ITLSolver lvar, ITLSolver solver, ITLSolver solver2) { - // too slow and we don't need it (?) - //solver = hash.put(solver); - //solver2 = hash.put(solver2); if (solver==solver2) return solver; ITLSolver v = new BDDSolver(lvar,solver,solver2,BDDID.BDD); return hash.put(v);
--- a/src/sbdd/SBDDSet.java Thu Jan 17 11:09:15 2008 +0900 +++ b/src/sbdd/SBDDSet.java Thu Jan 17 11:09:19 2008 +0900 @@ -110,10 +110,6 @@ public String toString() { String s = "SBDDSet[\n"; - /* - for(Entry<ITLSolver, BDDInterface>e : sbddset) { - s += e.getValue().hashCode()+":"+e.getValue()+"\n"; - } */ for(int i = 0;i<sbddArray.length;i++) { if (sbddArray[i]!=null) { SBDDEntry e = sbddArray[i];