From 0e7d9bd5b2e6eadeb9598f0c110b1215cf3d20bb Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 10 Jul 2008 12:58:38 +0000 Subject: [PATCH] Carlos' latest updates to LTL code. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@802 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/jdd/JDDNode.java | 5 + prism/src/jltl2ba/SimpleLTL.java | 44 ++-- prism/src/jltl2dstar/DA.java | 7 +- prism/src/jltl2dstar/SafraTreeNode.java | 3 +- prism/src/prism/LTLModelChecker.java | 278 +++++++++++++++--------- prism/src/prism/Modules2MTBDD.java | 7 +- prism/src/prism/NondetModelChecker.java | 29 +-- prism/src/prism/Prism.java | 9 + prism/src/prism/PrismSettings.java | 4 +- 9 files changed, 242 insertions(+), 144 deletions(-) diff --git a/prism/src/jdd/JDDNode.java b/prism/src/jdd/JDDNode.java index 1df3ab25..050e9d7e 100644 --- a/prism/src/jdd/JDDNode.java +++ b/prism/src/jdd/JDDNode.java @@ -93,6 +93,11 @@ public class JDDNode return (o instanceof JDDNode) && (((JDDNode) o).ptr == ptr); } + public int hashCode() + { + return (int)ptr; + } + public String toString() { return "" + ptr; diff --git a/prism/src/jltl2ba/SimpleLTL.java b/prism/src/jltl2ba/SimpleLTL.java index 92df9438..00fb29a6 100644 --- a/prism/src/jltl2ba/SimpleLTL.java +++ b/prism/src/jltl2ba/SimpleLTL.java @@ -194,6 +194,13 @@ public class SimpleLTL { { SimpleLTL tmp, tmp2, a, b; SimpleLTL rv = this; + + switch (kind) { + case AND: case OR: case IMPLIES: case EQUIV: case UNTIL: case RELEASE: + right = right.simplify(); + case NOT: case NEXT: case FINALLY: case GLOBALLY: + left = left.simplify(); + } switch (kind) { case NOT: @@ -202,8 +209,8 @@ public class SimpleLTL { rv = tmp.simplify(); else rv = tmp; break; + case FINALLY: - left = left.simplify(); if (left.kind == LTLType.TRUE || left.kind == LTLType.FALSE) { rv = left; break; @@ -221,7 +228,6 @@ public class SimpleLTL { break; case GLOBALLY: - left = left.simplify(); if (left.kind == LTLType.FALSE || left.kind == LTLType.TRUE) { rv = left; break; @@ -239,9 +245,6 @@ public class SimpleLTL { break; case UNTIL: - left = left.simplify(); - right = right.simplify(); - if (right.kind == LTLType.TRUE || right.kind == LTLType.FALSE || left.kind == LTLType.FALSE) { @@ -294,9 +297,6 @@ public class SimpleLTL { break; case RELEASE: - left = left.simplify(); - right = right.simplify(); - if (right.kind == LTLType.FALSE || right.kind == LTLType.TRUE || left.kind == LTLType.TRUE) { @@ -346,8 +346,6 @@ public class SimpleLTL { break; case NEXT: - left = left.simplify(); - if (left.kind == LTLType.TRUE || left.kind == LTLType.FALSE) { rv = left; break; @@ -371,9 +369,6 @@ public class SimpleLTL { } break; case IMPLIES: - left = left.simplify(); - right = right.simplify(); - if (left.implies(right)) { rv = new SimpleLTL(true); break; @@ -385,9 +380,6 @@ public class SimpleLTL { break; case EQUIV: - left = left.simplify(); - right = right.simplify(); - if (left.implies(right) && right.implies(left)) { rv = new SimpleLTL(true); @@ -403,9 +395,6 @@ public class SimpleLTL { break; case AND: - left = left.simplify(); - right = right.simplify(); - /* p && (q U p) = p */ if (right.kind == LTLType.UNTIL && right.right.equals(left)) { @@ -511,9 +500,6 @@ public class SimpleLTL { break; case OR: - left = left.simplify(); - right = right.simplify(); - /* p || (q U p) == q U p */ if (right.kind == LTLType.UNTIL && right.right.equals(left)) { @@ -652,6 +638,20 @@ public class SimpleLTL { kind = LTLType.AND; pushBothOperands = true; break; + case IMPLIES: + kind = LTLType.AND; + m = new SimpleLTL(LTLType.NOT, left.right); + right = m.pushNegation(); + left = left.left; + break; + case EQUIV: + kind = LTLType.OR; + m = new SimpleLTL(LTLType.NOT, left.left.clone()); + right = new SimpleLTL(LTLType.AND, m.pushNegation(), left.right.clone()); + left.kind = LTLType.AND; + m = new SimpleLTL(LTLType.NOT, left.right); + left.right = m.pushNegation(); + break; case FINALLY: kind = LTLType.GLOBALLY; left.kind = LTLType.NOT; diff --git a/prism/src/jltl2dstar/DA.java b/prism/src/jltl2dstar/DA.java index 661242a7..981fd659 100644 --- a/prism/src/jltl2dstar/DA.java +++ b/prism/src/jltl2dstar/DA.java @@ -287,9 +287,10 @@ public class DA { out.println(); _acceptance.outputAcceptanceForState(out, i_state); - - for (DA_State to_state : cur_state.edges().values()) { - out.println(to_state.getName()); + + // the entry set isn't sorted so we need to print the transition label too + for (Map.Entry transition : cur_state.edges().entrySet()) { + out.println(transition.getKey().toString(_ap_set, true) + " -> " + transition.getValue().getName()); } } } diff --git a/prism/src/jltl2dstar/SafraTreeNode.java b/prism/src/jltl2dstar/SafraTreeNode.java index 44a050fd..5dea5b80 100644 --- a/prism/src/jltl2dstar/SafraTreeNode.java +++ b/prism/src/jltl2dstar/SafraTreeNode.java @@ -481,7 +481,8 @@ public class SafraTreeNode implements Iterable { * Print node to output stream */ public void print(PrintStream out) { - out.print(_id + " " + _labeling); + out.print(_id + " "); + _labeling.print(out); if (_final_flag) {out.print(" !");} } diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index a545072e..521cc4d7 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -334,19 +334,18 @@ public class LTLModelChecker return startMask; } - + /** - * computes maximal accepting SCSSs for each Rabin acceptance pair + * computes sets of accepting states for each Rabin acceptance pair * - * @returns a referenced BDD of the union of all the accepting SCSSs - */ - public JDDNode findAcceptingSCSSs(DRA dra, NondetModel model) throws PrismException - { + * @returns a referenced BDD of the union of all the accepting sets + */ + public JDDNode findAcceptingStates(DRA dra, NondetModel model, boolean fairness) throws PrismException { - JDDNode allAcceptingSCSSs = JDD.Constant(0); + JDDNode allAcceptingStates = JDD.Constant(0); // for each acceptance pair (H_i, L_i) in the DRA, build H'_i = S x H_i - // and compute the SCSS maximals in H'_i + // and compute the maximal ECs in H'_i for (int i = 0; i < dra.acceptance().size(); i++) { // build the acceptance vectors H_i and L_i @@ -368,60 +367,159 @@ public class LTLModelChecker acceptanceVector_L = JDD.SetVectorElement(acceptanceVector_L, draDDRowVars, j, 1.0); } } - + // build bdd of accepting states (under H_i) in the product model JDD.Ref(model.getTrans01()); JDD.Ref(acceptanceVector_H); - JDDNode acceptingStates = JDD.Apply(JDD.TIMES, model.getTrans01(), acceptanceVector_H); + JDDNode candidateStates = JDD.Apply(JDD.TIMES, model.getTrans01(), acceptanceVector_H); acceptanceVector_H = JDD.PermuteVariables(acceptanceVector_H, draDDRowVars, draDDColVars); - acceptingStates = JDD.Apply(JDD.TIMES, acceptingStates, acceptanceVector_H); - acceptingStates = JDD.ThereExists(acceptingStates, model.getAllDDColVars()); - acceptingStates = JDD.ThereExists(acceptingStates, model.getAllDDNondetVars()); - - // find SCSSs in acceptingStates that are accepting under L_i - JDDNode acceptingSCSSs = filteredUnion(findMaximalSCSSs(model, acceptingStates), acceptanceVector_L); - - // Add SCSSs to our destination bdd - allAcceptingSCSSs = JDD.Or(allAcceptingSCSSs, acceptingSCSSs); + candidateStates = JDD.Apply(JDD.TIMES, candidateStates, acceptanceVector_H); + candidateStates = JDD.ThereExists(candidateStates, model.getAllDDColVars()); + candidateStates = JDD.ThereExists(candidateStates, model.getAllDDNondetVars()); + + JDDNode acceptingStates; + if (fairness) { + // compute the backward set of S x L_i + JDD.Ref(candidateStates); + JDDNode tmp = JDD.And(candidateStates, acceptanceVector_L); + JDD.Ref(model.getTrans01()); + JDDNode edges = JDD.ThereExists(model.getTrans01(), model.getAllDDNondetVars()); + JDDNode filterStates = backwardSet(model, tmp, edges); + + // Filter out states that can't reach a state in L'_i + candidateStates = JDD.And(candidateStates, filterStates); + + // Find accepting states in S x H_i + acceptingStates = findFairECs(model, candidateStates); + } + else { + // find ECs in acceptingStates that are accepting under L_i + acceptingStates = filteredUnion(findEndComponents(model, candidateStates), acceptanceVector_L); + } + + // Add states to our destination BDD + allAcceptingStates = JDD.Or(allAcceptingStates, acceptingStates); } - return allAcceptingSCSSs; + return allAcceptingStates; } - + + /** + * Returns all end components in candidateStates under fairness assumptions + * @param candidateStates set of candidate states S x H_i + * (dereferenced after calling this function) + * @return a referenced BDD with the maximal stable set in c + */ + private JDDNode findFairECs(NondetModel model, JDDNode candidateStates) { + + JDDNode old = JDD.Constant(0); + JDDNode current = candidateStates; + + while (!current.equals(old)) { + JDD.Deref(old); + JDD.Ref(current); + old = current; + + JDD.Ref(current); + JDD.Ref(model.getTrans01()); + // Select transitions starting in current + JDDNode currTrans01 = JDD.And(model.getTrans01(), current); + JDD.Ref(current); + // mask of transitions that end outside current + JDDNode mask = JDD.Not(JDD.PermuteVariables(current, model.getAllDDRowVars(), model.getAllDDColVars())); + mask = JDD.And(currTrans01, mask); + // mask of states that have bad transitions + mask = JDD.ThereExists(mask, model.getAllDDColVars()); + mask = JDD.ThereExists(mask, model.getAllDDNondetVars()); + // Filter states with bad transitions + current = JDD.And(current, JDD.Not(mask)); + } + JDD.Deref(old); + return current; + } + + /** + * Return the set of states that reach nodes through edges + * Refs: result + * Derefs: nodes, edges + */ + private JDDNode backwardSet(NondetModel model, JDDNode nodes, JDDNode edges) + { + JDDNode old = JDD.Constant(0); + JDDNode current = nodes; + while (!current.equals(old)) { + JDD.Deref(old); + JDD.Ref(current); + old = current; + JDD.Ref(current); + JDD.Ref(edges); + current = JDD.Or(current, preimage(model, current, edges)); + } + JDD.Deref(edges); + JDD.Deref(old); + return current; + } + + /** + * Return the preimage of nodes in edges + * Refs: result + * Derefs: edges, nodes + */ + // FIXME: Refactor this out (duplicated in SCCComputers) + private JDDNode preimage(NondetModel model, JDDNode nodes, JDDNode edges) + { + JDDNode tmp; + + // Get transitions that end at nodes + tmp = JDD.PermuteVariables(nodes, model.getAllDDRowVars(), model.getAllDDColVars()); + tmp = JDD.And(edges, tmp); + // Get pre(nodes) + tmp = JDD.ThereExists(tmp, model.getAllDDColVars()); + return tmp; + } + /** - * Computes maximal accepting SCSSs in states + * Computes maximal accepting end components in states * @param states BDD of a set of states (dereferenced after calling this function) - * @return a vector of referenced BDDs containing all the maximal SCSSs in states + * @return a vector of referenced BDDs containing all the ECs in states */ - private Vector findMaximalSCSSs(NondetModel model, JDDNode states) throws PrismException - { - + private Vector findEndComponents(NondetModel model, JDDNode states) throws PrismException { + boolean initialCandidate = true; Stack candidates = new Stack(); candidates.push(states); - Vector scsss = new Vector(); - + Vector ecs = new Vector(); + while (!candidates.isEmpty()) { JDDNode candidate = candidates.pop(); - + // Compute the stable set JDD.Ref(candidate); - JDDNode stableSet = findMaxStableSet(model, candidate); - + JDDNode stableSet = findMaximalStableSet(model, candidate); + + // Drop empty sets + if (stableSet.equals(JDD.ZERO)) { + JDD.Deref(stableSet); + JDD.Deref(candidate); + continue; + } + if (!initialCandidate) { // candidate is an SCC, check if it's stable if (stableSet.equals(candidate)) { - scsss.add(candidate); + ecs.add(candidate); JDD.Deref(stableSet); continue; } - } else + } + else { initialCandidate = false; + } JDD.Deref(candidate); - + // Filter bad transitions JDD.Ref(stableSet); JDDNode stableSetTrans = maxStableSetTrans(model, stableSet); - + // now find the maximal SCCs in (stableSet, stableSetTrans) Vector sccs; SCCComputer sccComputer; @@ -449,84 +547,68 @@ public class LTLModelChecker JDD.Deref(sccComputer.getNotInBSCCs()); candidates.addAll(sccs); } - return scsss; + return ecs; } - + /** - * Returns the maximal stable set in c - * @param c a set of nodes where we want to find a stable set - * (dereferenced after calling this function) + * Returns a stable set of states contained in candidateStates + * @param candidateStates set of candidate states S x H_i + * (dereferenced after calling this function) * @return a referenced BDD with the maximal stable set in c */ - private JDDNode findMaxStableSet(NondetModel model, JDDNode c) - { - JDDNode old; - JDDNode current; - JDDNode mask; - - JDD.Ref(c); - current = c; - - do { - /* if (verbose) { - mainLog.println("Stable set pass " + i + ":"); - } */ + private JDDNode findMaximalStableSet(NondetModel model, JDDNode candidateStates) { + + JDDNode old = JDD.Constant(0); + JDDNode current = candidateStates; + + while (!current.equals(old)) { + JDD.Deref(old); + JDD.Ref(current); old = current; - // states that aren't in B (column vector) + JDD.Ref(current); - mask = JDD.Not(JDD.PermuteVariables(current, model.getAllDDRowVars(), model.getAllDDColVars())); - JDD.Ref(model.getTrans01()); - // transitions that end outside of B - mask = JDD.Apply(JDD.TIMES, model.getTrans01(), mask); - // mask of transitions that end in B - mask = JDD.Not(mask); - // mask of states that always transition to other states in B through a certain action - mask = JDD.ForAll(mask, model.getAllDDColVars()); - // mask of states that have an action that always transitions to other states in B - mask = JDD.ThereExists(mask, model.getAllDDNondetVars()); - // states in B that have an action that always transitions to other states in B - current = JDD.Apply(JDD.TIMES, current, mask); - /* if (verbose) { - mainLog.println("Stable set search pass " + i); - JDD.PrintVector(current, allDDRowVars); - mainLog.println(); - i++; - } */ - } while (!current.equals(old)); - JDD.Deref(c); + JDD.Ref(model.getTrans()); + // Select transitions starting in current + JDDNode currTrans = JDD.Apply(JDD.TIMES, model.getTrans(), current); + // Select transitions starting in current and ending in current + JDDNode tmp = JDD.PermuteVariables(current, model.getAllDDRowVars(), model.getAllDDColVars()); + tmp = JDD.Apply(JDD.TIMES, currTrans, tmp); + // Sum all successor probabilities for each (state, action) tuple + tmp = JDD.SumAbstract(tmp, model.getAllDDColVars()); + // If the sum for a (state,action) tuple is 1, + // there is an action that remains in the stable set with prob 1 + tmp = JDD.GreaterThan(tmp, 1 - prism.getUpdateSumRoundOff()); + // Without fairness, we just need one action per state + current = JDD.ThereExists(tmp, model.getAllDDNondetVars()); + } + JDD.Deref(old); return current; } - + /** * Returns the transition relation of a stable set * @param b BDD of a stable set (dereferenced after calling this function) * @return referenced BDD of the transition relation restricted to the stable set */ - private JDDNode maxStableSetTrans(NondetModel model, JDDNode b) - { - - JDDNode ssTrans; - JDDNode mask; + private JDDNode maxStableSetTrans(NondetModel model, JDDNode b) { - // Restrict threshold to transitions that start in the stable set - JDD.Ref(model.getTrans01()); JDD.Ref(b); - ssTrans = JDD.Apply(JDD.TIMES, model.getTrans01(), b); - // states that aren't in B (column vector) - mask = JDD.Not(JDD.PermuteVariables(b, model.getAllDDRowVars(), model.getAllDDColVars())); - JDD.Ref(ssTrans); - // transitions that land outside of B - mask = JDD.Apply(JDD.TIMES, ssTrans, mask); - // mask of transitions that land in B - mask = JDD.Not(mask); - // mask of states that always transition to other states in B through a certain action - mask = JDD.ForAll(mask, model.getAllDDColVars()); - // transitions that always land in B through a certain action - ssTrans = JDD.Apply(JDD.TIMES, ssTrans, mask); - // valid transitions in the stable set regardless of action - ssTrans = JDD.ThereExists(ssTrans, model.getAllDDNondetVars()); - - return ssTrans; + JDD.Ref(model.getTrans()); + // Select transitions starting in b + JDDNode currTrans = JDD.Apply(JDD.TIMES, model.getTrans(), b); + JDDNode mask = JDD.PermuteVariables(b, model.getAllDDRowVars(), model.getAllDDColVars()); + // Select transitions starting in current and ending in current + mask = JDD.Apply(JDD.TIMES, currTrans, mask); + // Sum all successor probabilities for each (state, action) tuple + mask = JDD.SumAbstract(mask, model.getAllDDColVars()); + // If the sum for a (state,action) tuple is 1, + // there is an action that remains in the stable set with prob 1 + mask = JDD.GreaterThan(mask, 1 - prism.getUpdateSumRoundOff()); + // select the transitions starting in these tuples + JDD.Ref(model.getTrans01()); + JDDNode stableTrans01 = JDD.And(model.getTrans01(), mask); + // Abstract over actions + return JDD.ThereExists(stableTrans01, model.getAllDDNondetVars()); } /** diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index e7e01c44..1e1547fa 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -38,9 +38,6 @@ import parser.ast.*; public class Modules2MTBDD { - // constants - private static final double ACCEPTABLE_ROUND_OFF = 10e-6; // when checking for sums to 1 - // Prism object private Prism prism; @@ -1383,7 +1380,7 @@ public class Modules2MTBDD throw new PrismLangException(s, command); } // check min sums - 1 (ish) for dtmcs/mdps, 0 for ctmcs - if (type != ModulesFile.STOCHASTIC && dmin < 1-ACCEPTABLE_ROUND_OFF) { + if (type != ModulesFile.STOCHASTIC && dmin < 1-prism.getUpdateSumRoundOff()) { JDD.Deref(tmp); String s = "Probabilities in command " + (l+1) + " of module \"" + module.getName() + "\" sum to less than one"; s += " (e.g. " + dmin + ") for some states. "; @@ -1400,7 +1397,7 @@ public class Modules2MTBDD throw new PrismLangException(s, command); } // check max sums - 1 (ish) for dtmcs/mdps, infinity for ctmcs - if (type != ModulesFile.STOCHASTIC && dmax > 1+ACCEPTABLE_ROUND_OFF) { + if (type != ModulesFile.STOCHASTIC && dmax > 1+prism.getUpdateSumRoundOff()) { JDD.Deref(tmp); String s = "Probabilities in command " + (l+1) + " of module \"" + module.getName() + "\" sum to more than one"; s += " (e.g. " + dmax + ") for some states. "; diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 5934e71f..4920ba0d 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -384,15 +384,6 @@ public class NondetModelChecker extends StateModelChecker int i; long l; - // Can't do LTL and fairness. - // Note: the basic techniques, i.e. DRA product and BSCC reachability work - // (see e.g. Christel's habilitation); the problem is that the current computation - // of satisfying BSCCs is optimised to remove unwanted parts of the product MDP - // which can break fairness (e.g. add new BSCCs). - if (fairness) { - throw new PrismException("Fairness is not supported for LTL properties"); - } - // Can't do LTL with time-bounded variants of the temporal operators try { expr.accept(new ASTTraverse() @@ -417,9 +408,14 @@ public class NondetModelChecker extends StateModelChecker ltl = mcLtl.checkMaximalStateFormulas(model, expr.deepCopy(), labelDDs); // Convert LTL formula to deterministic Rabin automaton (DRA) - mainLog.println("\nBuilding deterministic Rabin automaton (for "+ltl+")..."); + mainLog.println("\nBuilding deterministic Rabin automaton (for "+(min&&!fairness?"!":"")+ltl+")..."); l = System.currentTimeMillis(); - dra = LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba()); + if (min && !fairness) { + dra = LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba().negate()); + } + else { + dra = LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba()); + } mainLog.println("\nDRA has " + dra.size() + " states."); //dra.print(System.out); l = System.currentTimeMillis() - l; @@ -433,12 +429,17 @@ public class NondetModelChecker extends StateModelChecker //prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, null); //prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, null); - mainLog.println("\nFinding accepting SCCs..."); - JDDNode acc = mcLtl.findAcceptingSCSSs(dra, modelProduct); + mainLog.println("\nFinding accepting end components..."); + JDDNode acc = mcLtl.findAcceptingStates(dra, modelProduct, fairness); mainLog.println("\nComputing reachability probabilities..."); mcProduct = new NondetModelChecker(prism, modelProduct, null); - probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual, min); + probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual, min && fairness); + + // subtract from 1 if we're model checking a negated formula for regular Pmin + if (min && !fairness) { + probsProduct.subtractFromOne(); + } // Convert probability vector to original model // First, filter over DRA start states diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index c2a40790..bb2d4b4a 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -309,6 +309,12 @@ public class Prism implements PrismSettingsListener settings.set(PrismSettings.PRISM_SCC_METHOD, i-1); // note index offset correction } + public void setUpdateSumRoundOff(double d) throws PrismException + { + settings.set(PrismSettings.PRISM_UPDATE_SUM_ROUND_OFF, d); + } + + // set methods for miscellaneous options public void setDoReach(boolean b) throws PrismException @@ -408,6 +414,9 @@ public class Prism implements PrismSettingsListener public int getSCCMethod() { return settings.getInteger(PrismSettings.PRISM_SCC_METHOD)+1; } //NOTE THE CORRECTION for the ChoiceSetting index + public double getUpdateSumRoundOff() + { return settings.getDouble(PrismSettings.PRISM_UPDATE_SUM_ROUND_OFF); } + // get methods for miscellaneous options public boolean getDoReach() diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index b37586fc..2c5f97cc 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -89,6 +89,7 @@ public class PrismSettings implements Observer public static final String PRISM_EXTRA_DD_INFO = "prism.extraDDInfo"; public static final String PRISM_EXTRA_REACH_INFO = "prism.extraReachInfo"; public static final String PRISM_SCC_METHOD = "prism.sccMethod"; + public static final String PRISM_UPDATE_SUM_ROUND_OFF = "prism.updateSumRoundOff"; //GUI Model public static final String MODEL_AUTO_PARSE = "model.autoParse"; @@ -185,7 +186,8 @@ public class PrismSettings implements Observer { BOOLEAN_TYPE, PRISM_DO_SS_DETECTION, "Use steady-state detection", "3.0", new Boolean(true), "0,", "Use steady-state detection during CTMC transient probability computation." }, { BOOLEAN_TYPE, PRISM_EXTRA_DD_INFO, "Extra MTBDD information", "3.2", new Boolean(false), "0,", "Display extra information about (MT)BDDs used during and after model construction." }, { BOOLEAN_TYPE, PRISM_EXTRA_REACH_INFO, "Extra reachability information", "3.2", new Boolean(false), "0,", "Display extra information about progress of reachability during model construction." }, - { CHOICE_TYPE, PRISM_SCC_METHOD, "SCC decomposition method", "3.2", "Lockstep", "Xie-Beerel,Lockstep,SCC-Find", "Which algorithm to use for decomposing a graph into strongly connected components (SCCs)." } + { CHOICE_TYPE, PRISM_SCC_METHOD, "SCC decomposition method", "3.2", "Lockstep", "Xie-Beerel,Lockstep,SCC-Find", "Which algorithm to use for decomposing a graph into strongly connected components (SCCs)." }, + { DOUBLE_TYPE, PRISM_UPDATE_SUM_ROUND_OFF, "Update probability sum round off", "3.2.dev", new Double(10e-6), "0.0,", "Epsilon value used by PRISM for update probabilities that should sum to 1" } }, { { BOOLEAN_TYPE, MODEL_AUTO_PARSE, "Auto parse", "3.0", new Boolean(true), "", "Parse PRISM models automatically as they are loaded/edited in the text editor." },