From 5987dde29969ea2f2fc774fc6ef80eb19ff3657d Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 21 Apr 2008 10:18:26 +0000 Subject: [PATCH] Bug fixes in DRA libraries (Carlos). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@762 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/jltl2ba/APSet.java | 11 +++++++++++ prism/src/jltl2ba/SimpleLTL.java | 1 + prism/src/jltl2dstar/APMonom2APElements.java | 17 ++++++++++++----- prism/src/jltl2dstar/LTL2DRA.java | 4 ++-- prism/src/jltl2dstar/LTL2Rabin.java | 10 +++++----- prism/src/jltl2dstar/NBAAnalysis.java | 13 ++++++------- prism/src/jltl2dstar/Scheduler.java | 7 +++---- 7 files changed, 40 insertions(+), 23 deletions(-) diff --git a/prism/src/jltl2ba/APSet.java b/prism/src/jltl2ba/APSet.java index 7ae0ba81..fdc8ec68 100644 --- a/prism/src/jltl2ba/APSet.java +++ b/prism/src/jltl2ba/APSet.java @@ -135,4 +135,15 @@ public class APSet implements Iterable { out.println(i + ": " + getAP(i)); } } + + public String toString() { + String rv = "{"; + for (Iterator it = this.iterator(); it.hasNext(); ) { + rv = rv + it.next(); + if (it.hasNext()) { + rv = rv + ","; + } + } + return rv + "}"; + } } diff --git a/prism/src/jltl2ba/SimpleLTL.java b/prism/src/jltl2ba/SimpleLTL.java index e02bea35..92df9438 100644 --- a/prism/src/jltl2ba/SimpleLTL.java +++ b/prism/src/jltl2ba/SimpleLTL.java @@ -146,6 +146,7 @@ public class SimpleLTL { rv = left.getAPs(); for (String s : right.getAPs()) rv.addAP(s); + break; // terminals case FALSE:case TRUE: rv = new APSet(); diff --git a/prism/src/jltl2dstar/APMonom2APElements.java b/prism/src/jltl2dstar/APMonom2APElements.java index 2be78298..37bfcd2f 100644 --- a/prism/src/jltl2dstar/APMonom2APElements.java +++ b/prism/src/jltl2dstar/APMonom2APElements.java @@ -41,7 +41,10 @@ public class APMonom2APElements implements Iterator { private APMonom _m; /** The current APElement. */ - private APElement _cur_e; + private APElement _cur_e; + + /** Bits that are set */ + private MyBitSet set_mask; /** Marker, true if end was reached */ private boolean _end_marker; @@ -52,18 +55,22 @@ public class APMonom2APElements implements Iterator { _ap_set = s; _cur_e = new APElement(m.getValueBits()); _end_marker = m.isFalse(); + + if (m.isTrue()) { + set_mask = new MyBitSet(_ap_set.size()); + } + else { + set_mask = _m.getSetBits(); + } } private void increment() { - MyBitSet set_mask = (MyBitSet) _m.getSetBits(); - int i = set_mask.nextClearBit(0); - while (i < _ap_set.size()) { + for (int i = set_mask.nextClearBit(0); i < _ap_set.size(); i = set_mask.nextClearBit(i+1)) { if (_cur_e.get(i) == false) { _cur_e.set(i, true); return; } else { _cur_e.set(i, false); - i = set_mask.nextClearBit(i+1); } } // overflow -> end diff --git a/prism/src/jltl2dstar/LTL2DRA.java b/prism/src/jltl2dstar/LTL2DRA.java index ae8de010..4fe3f504 100644 --- a/prism/src/jltl2dstar/LTL2DRA.java +++ b/prism/src/jltl2dstar/LTL2DRA.java @@ -90,9 +90,9 @@ public class LTL2DRA { } - public DRA LTLtoDRA(SimpleLTL ltl, Options_LTL2DRA options) throws PrismException { + /* public DRA LTLtoDRA(SimpleLTL ltl, Options_LTL2DRA options) throws PrismException { return LTLtoDRA_rec(ltl, ltl.getAPs(), options); - } + } */ public DRA LTLtoDRA(SimpleLTL ltl, APSet apset, Options_LTL2DRA options) throws PrismException { return LTLtoDRA_rec(ltl, apset, options); diff --git a/prism/src/jltl2dstar/LTL2Rabin.java b/prism/src/jltl2dstar/LTL2Rabin.java index 24a6dc9e..f8296817 100644 --- a/prism/src/jltl2dstar/LTL2Rabin.java +++ b/prism/src/jltl2dstar/LTL2Rabin.java @@ -26,13 +26,13 @@ import prism.PrismException; public class LTL2Rabin { - public static DRA ltl2rabin(SimpleLTL ltlformula) throws PrismException { - return ltl2rabin(ltlformula, new APSet()); + public static DRA ltl2rabin(SimpleLTL ltlFormula) throws PrismException { + SimpleLTL ltl = ltlFormula.simplify(); + return ltl2rabin(ltl, ltl.getAPs()); } - public static DRA ltl2rabin(SimpleLTL ltlformula, APSet apset) throws PrismException { + + private static DRA ltl2rabin(SimpleLTL ltl, APSet apset) throws PrismException { DRA dra = null; - SimpleLTL ltl = ltlformula.clone(); - ltl = ltl.simplify(); Options_LTL2DRA opt_ltl2rabin = new Options_LTL2DRA(); // boolean flag_dra2nba=false; diff --git a/prism/src/jltl2dstar/NBAAnalysis.java b/prism/src/jltl2dstar/NBAAnalysis.java index 26c7504a..24174b58 100644 --- a/prism/src/jltl2dstar/NBAAnalysis.java +++ b/prism/src/jltl2dstar/NBAAnalysis.java @@ -172,15 +172,15 @@ public class NBAAnalysis { MyBitSet scc_all_final = new MyBitSet(sccs.countSCCs()); - for (int i = sccs.countSCCs(); i > 0; --i) { + for (int sccIndex = sccs.countSCCs(); sccIndex > 0; --sccIndex) { // go backward in topological order... - int scc = (sccs.topologicalOrder()).get(i-1); + int scc = sccs.topologicalOrder().get(sccIndex-1); MyBitSet states_in_scc = sccs.get(scc); // check to see if all states in this SCC are final scc_all_final.set(scc); - for (int it = states_in_scc.nextSetBit(0); it >= 0; it = states_in_scc.nextSetBit(i+1)) { + for (int it = states_in_scc.nextSetBit(0); it >= 0; it = states_in_scc.nextSetBit(it+1)) { if (!_nba.get(it).isFinal()) { scc_all_final.clear(scc); break; @@ -189,12 +189,11 @@ public class NBAAnalysis { boolean might_be_final = false; if (!scc_all_final.get(scc)) { - // FIXME: This should be cardinality, bug in ltl2dstar? - if (states_in_scc.length() == 1) { + if (states_in_scc.cardinality() == 1) { // there is only one state in this scc ... int state = states_in_scc.nextSetBit(0); - if (sccs.stateIsReachable(state,state) == false) { + if (!sccs.stateIsReachable(state,state)) { // ... and it doesn't loop to itself might_be_final = true; } @@ -205,7 +204,7 @@ public class NBAAnalysis { // Check to see if all successors are final... boolean all_successors_are_final = true; MyBitSet scc_succ = sccs.successors(scc); - for (int it = scc_succ.nextSetBit(0); it >= 0; it = scc_succ.nextSetBit(i+1)) { + for (int it = scc_succ.nextSetBit(0); it >= 0; it = scc_succ.nextSetBit(it+1)) { if (!scc_all_final.get(it)) { all_successors_are_final = false; break; diff --git a/prism/src/jltl2dstar/Scheduler.java b/prism/src/jltl2dstar/Scheduler.java index e4c12f43..6da05264 100644 --- a/prism/src/jltl2dstar/Scheduler.java +++ b/prism/src/jltl2dstar/Scheduler.java @@ -492,7 +492,7 @@ public class Scheduler { union_trueloop, _options.detailed_states); } else { - */ + */ _automaton = children.get(0)._automaton.calculateUnion(children.get(1)._automaton, union_trueloop, _options.detailed_states); /* _automaton=DRAOperations::dra_union(*children[0]->_automaton, *children[1]->_automaton, @@ -660,13 +660,12 @@ public class Scheduler { * Generate a DRA/DSA for the LTL formula */ public DRA calculate(SimpleLTL ltl, APSet apset, Options_LTL2DRA ltl_opt) throws PrismException { - SimpleLTL ltl_p = ltl.simplify(); if (ltl_opt.verbose_scheduler) { - System.err.println(ltl_p); + System.err.println(ltl); } - Tree root = new Tree_Start(ltl_p, apset, ltl_opt, this); + Tree root = new Tree_Start(ltl, apset, ltl_opt, this); if (ltl_opt.verbose_scheduler) { root.printTree(System.err, 0);