s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Carlos' latest updates to LTL code. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@802 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
cf1c9948f0
commit
0e7d9bd5b2
9 changed files with 242 additions and 144 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 5
      prism/src/jdd/JDDNode.java
  2. 44
      prism/src/jltl2ba/SimpleLTL.java
  3. 7
      prism/src/jltl2dstar/DA.java
  4. 3
      prism/src/jltl2dstar/SafraTreeNode.java
  5. 278
      prism/src/prism/LTLModelChecker.java
  6. 7
      prism/src/prism/Modules2MTBDD.java
  7. 29
      prism/src/prism/NondetModelChecker.java
  8. 9
      prism/src/prism/Prism.java
  9. 4
      prism/src/prism/PrismSettings.java

5
prism/src/jdd/JDDNode.java
View File

@ -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;

44
prism/src/jltl2ba/SimpleLTL.java
View File

@ -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;

7
prism/src/jltl2dstar/DA.java
View File

@ -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<APElement, DA_State> transition : cur_state.edges().entrySet()) {
out.println(transition.getKey().toString(_ap_set, true) + " -> " + transition.getValue().getName());
}
}
}

3
prism/src/jltl2dstar/SafraTreeNode.java
View File

@ -481,7 +481,8 @@ public class SafraTreeNode implements Iterable<SafraTreeNode> {
* 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(" !");}
}

278
prism/src/prism/LTLModelChecker.java
View File

@ -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<JDDNode> findMaximalSCSSs(NondetModel model, JDDNode states) throws PrismException
{
private Vector<JDDNode> findEndComponents(NondetModel model, JDDNode states) throws PrismException {
boolean initialCandidate = true;
Stack<JDDNode> candidates = new Stack<JDDNode>();
candidates.push(states);
Vector<JDDNode> scsss = new Vector<JDDNode>();
Vector<JDDNode> ecs = new Vector<JDDNode>();
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<JDDNode> 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());
}
/**

7
prism/src/prism/Modules2MTBDD.java
View File

@ -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. ";

29
prism/src/prism/NondetModelChecker.java
View File

@ -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

9
prism/src/prism/Prism.java
View File

@ -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()

4
prism/src/prism/PrismSettings.java
View File

@ -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." },

Write Preview
Loading…
Cancel
Save