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

Two bugs in LTL model checking for MDPs. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2201 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
b6d4a15737
commit
31707a7729
1 changed files with 42 additions and 51 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 73
      prism/src/prism/LTLModelChecker.java

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

@ -57,8 +57,7 @@ public class LTLModelChecker
* actual true/false, and duplicate results are given the same label. BDDs giving the states which satisfy each label * actual true/false, and duplicate results are given the same label. BDDs giving the states which satisfy each label
* are put into the vector labelDDs, which should be empty when this function is called. * are put into the vector labelDDs, which should be empty when this function is called.
*/ */
public Expression checkMaximalStateFormulas(ModelChecker mc, Model model, Expression expr, Vector<JDDNode> labelDDs)
throws PrismException
public Expression checkMaximalStateFormulas(ModelChecker mc, Model model, Expression expr, Vector<JDDNode> labelDDs) throws PrismException
{ {
// A state formula // A state formula
if (expr.getType() instanceof TypeBool) { if (expr.getType() instanceof TypeBool) {
@ -125,8 +124,8 @@ public class LTLModelChecker
* @param draDDRowVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA * @param draDDRowVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA
* @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA * @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA
*/ */
public ProbModel constructProductMC(DRA dra, ProbModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy,
JDDVars draDDColVarsCopy) throws PrismException
public ProbModel constructProductMC(DRA dra, ProbModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy)
throws PrismException
{ {
return constructProductMC(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true); return constructProductMC(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true);
} }
@ -140,8 +139,8 @@ public class LTLModelChecker
* @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA * @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA
* @param allInit: Do we assume that all states of the original model are initial states? (see below) * @param allInit: Do we assume that all states of the original model are initial states? (see below)
*/ */
public ProbModel constructProductMC(DRA dra, ProbModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy,
JDDVars draDDColVarsCopy, boolean allInit) throws PrismException
public ProbModel constructProductMC(DRA dra, ProbModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy, boolean allInit)
throws PrismException
{ {
// Existing model - dds, vars, etc. // Existing model - dds, vars, etc.
JDDVars varDDRowVars[]; JDDVars varDDRowVars[];
@ -232,8 +231,7 @@ public class LTLModelChecker
} }
newVarList = (VarList) varList.clone(); newVarList = (VarList) varList.clone();
// NB: if DRA only has one state, we add an extra dummy state // NB: if DRA only has one state, we add an extra dummy state
Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(dra
.size() - 1, 1))));
Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(dra.size() - 1, 1))));
newVarList.addVar(before ? 0 : varList.getNumVars(), decl, 1, model.getConstantValues()); newVarList.addVar(before ? 0 : varList.getNumVars(), decl, 1, model.getConstantValues());
// Extra references (because will get derefed when new model is done with) // Extra references (because will get derefed when new model is done with)
@ -317,8 +315,8 @@ public class LTLModelChecker
* @param draDDRowVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA * @param draDDRowVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA
* @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA * @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA
*/ */
public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy,
JDDVars draDDColVarsCopy) throws PrismException
public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy)
throws PrismException
{ {
return constructProductMDP(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true); return constructProductMDP(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true);
} }
@ -332,8 +330,8 @@ public class LTLModelChecker
* @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA * @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA
* @param allInit: Do we assume that all states of the original model are initial states? (see below) * @param allInit: Do we assume that all states of the original model are initial states? (see below)
*/ */
public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy,
JDDVars draDDColVarsCopy, boolean allInit) throws PrismException
public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy, JDDVars draDDColVarsCopy,
boolean allInit) throws PrismException
{ {
// Existing model - dds, vars, etc. // Existing model - dds, vars, etc.
JDDVars varDDRowVars[]; JDDVars varDDRowVars[];
@ -424,8 +422,7 @@ public class LTLModelChecker
} }
newVarList = (VarList) varList.clone(); newVarList = (VarList) varList.clone();
// NB: if DRA only has one state, we add an extra dummy state // NB: if DRA only has one state, we add an extra dummy state
Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(dra
.size() - 1, 1))));
Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(dra.size() - 1, 1))));
newVarList.addVar(before ? 0 : varList.getNumVars(), decl, 1, model.getConstantValues()); newVarList.addVar(before ? 0 : varList.getNumVars(), decl, 1, model.getConstantValues());
// Extra references (because will get derefed when new model is done with) // Extra references (because will get derefed when new model is done with)
@ -469,8 +466,7 @@ public class LTLModelChecker
// New list of all row/col vars // New list of all row/col vars
newAllDDRowVars, newAllDDColVars, newAllDDRowVars, newAllDDColVars,
// Nondet variables (unchanged) // Nondet variables (unchanged)
model.getAllDDSchedVars(), model.getAllDDSynchVars(), model.getAllDDChoiceVars(), model
.getAllDDNondetVars(),
model.getAllDDSchedVars(), model.getAllDDSynchVars(), model.getAllDDChoiceVars(), model.getAllDDNondetVars(),
// New list of var names // New list of var names
newDDVarNames, newDDVarNames,
// Module info (unchanged) // Module info (unchanged)
@ -516,8 +512,7 @@ public class LTLModelChecker
* *
* @return a referenced mask BDD over trans * @return a referenced mask BDD over trans
*/ */
public JDDNode buildTransMask(DRA dra, Vector<JDDNode> labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars,
JDDVars draDDRowVars, JDDVars draDDColVars)
public JDDNode buildTransMask(DRA dra, Vector<JDDNode> labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars draDDRowVars, JDDVars draDDColVars)
{ {
Iterator<DA_State> it; Iterator<DA_State> it;
DA_State state; DA_State state;
@ -546,8 +541,7 @@ public class LTLModelChecker
// Switch label BDD to col vars // Switch label BDD to col vars
label = JDD.PermuteVariables(label, allDDRowVars, allDDColVars); label = JDD.PermuteVariables(label, allDDRowVars, allDDColVars);
// Build a BDD for the edge // Build a BDD for the edge
transition = JDD.SetMatrixElement(JDD.Constant(0), draDDRowVars, draDDColVars, state.getName(), edge
.getValue().getName(), 1);
transition = JDD.SetMatrixElement(JDD.Constant(0), draDDRowVars, draDDColVars, state.getName(), edge.getValue().getName(), 1);
// Now get the conjunction of the two // Now get the conjunction of the two
transition = JDD.And(transition, label); transition = JDD.And(transition, label);
// Add edge BDD to the DRA transition mask // Add edge BDD to the DRA transition mask
@ -601,8 +595,7 @@ public class LTLModelChecker
* *
* @returns a referenced BDD of the union of all the accepting sets * @returns a referenced BDD of the union of all the accepting sets
*/ */
public JDDNode findAcceptingBSCCs(DRA dra, JDDVars draDDRowVars, JDDVars draDDColVars, ProbModel model)
throws PrismException
public JDDNode findAcceptingBSCCs(DRA dra, JDDVars draDDRowVars, JDDVars draDDColVars, ProbModel model) throws PrismException
{ {
SCCComputer sccComputer; SCCComputer sccComputer;
JDDNode acceptingStates, allAcceptingStates; JDDNode acceptingStates, allAcceptingStates;
@ -681,8 +674,7 @@ public class LTLModelChecker
* *
* @returns a referenced BDD of the union of all the accepting sets * @returns a referenced BDD of the union of all the accepting sets
*/ */
public JDDNode findAcceptingStates(DRA dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars,
boolean fairness) throws PrismException
public JDDNode findAcceptingStates(DRA dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, boolean fairness) throws PrismException
{ {
JDDNode acceptingStates, allAcceptingStates; JDDNode acceptingStates, allAcceptingStates;
int i, j; int i, j;
@ -825,10 +817,8 @@ public class LTLModelChecker
* BDD of a set of states (dereferenced after calling this function) * BDD of a set of states (dereferenced after calling this function)
* @return a vector of referenced BDDs containing all the ECs in states * @return a vector of referenced BDDs containing all the ECs in states
*/ */
private Vector<JDDNode> findEndComponents(NondetModel model, JDDNode states) throws PrismException
public Vector<JDDNode> findEndComponents(NondetModel model, JDDNode states) throws PrismException
{ {
boolean initialCandidate = true;
Stack<JDDNode> candidates = new Stack<JDDNode>(); Stack<JDDNode> candidates = new Stack<JDDNode>();
candidates.push(states); candidates.push(states);
Vector<JDDNode> ecs = new Vector<JDDNode>(); Vector<JDDNode> ecs = new Vector<JDDNode>();
@ -836,11 +826,9 @@ public class LTLModelChecker
while (!candidates.isEmpty()) { while (!candidates.isEmpty()) {
JDDNode candidate = candidates.pop(); JDDNode candidate = candidates.pop();
// Compute the stable set // Compute the stable set
JDD.Ref(candidate); JDD.Ref(candidate);
JDDNode stableSet = findMaximalStableSet(model, candidate); JDDNode stableSet = findMaximalStableSet(model, candidate);
// Drop empty sets // Drop empty sets
if (stableSet.equals(JDD.ZERO)) { if (stableSet.equals(JDD.ZERO)) {
JDD.Deref(stableSet); JDD.Deref(stableSet);
@ -848,17 +836,11 @@ public class LTLModelChecker
continue; continue;
} }
if (!initialCandidate) {
// candidate is an SCC, check if it's stable
if (stableSet.equals(candidate)) {
if (stableSet.equals(candidate) && JDD.GetNumMinterms(stableSet, model.getNumDDRowVars()) == 1) {
ecs.add(candidate); ecs.add(candidate);
JDD.Deref(stableSet); JDD.Deref(stableSet);
continue; continue;
} }
} else {
initialCandidate = false;
}
JDD.Deref(candidate);
// Filter bad transitions // Filter bad transitions
JDD.Ref(stableSet); JDD.Ref(stableSet);
@ -866,15 +848,22 @@ public class LTLModelChecker
// now find the maximal SCCs in (stableSet, stableSetTrans) // now find the maximal SCCs in (stableSet, stableSetTrans)
Vector<JDDNode> sccs; Vector<JDDNode> sccs;
sccComputer = prism.getSCCComputer(stableSet, stableSetTrans, model.getAllDDRowVars(), model
.getAllDDColVars());
sccComputer = prism.getSCCComputer(stableSet, stableSetTrans, model.getAllDDRowVars(), model.getAllDDColVars());
sccComputer.computeSCCs(); sccComputer.computeSCCs();
JDD.Deref(stableSet); JDD.Deref(stableSet);
JDD.Deref(stableSetTrans); JDD.Deref(stableSetTrans);
sccs = sccComputer.getVectSCCs(); sccs = sccComputer.getVectSCCs();
mainLog.println("SCC computer found " + sccs.size() + " SCCs");
JDD.Deref(sccComputer.getNotInSCCs()); JDD.Deref(sccComputer.getNotInSCCs());
if (sccs.size() > 0) {
if (sccs.size() > 1 || !sccs.get(0).equals(candidate)) {
candidates.addAll(sccs); candidates.addAll(sccs);
JDD.Deref(candidate);
} else {
ecs.add(candidate);
JDD.Deref(sccs.get(0));
}
} else
JDD.Deref(candidate);
} }
return ecs; return ecs;
} }
@ -959,8 +948,10 @@ public class LTLModelChecker
{ {
JDDNode union = JDD.Constant(0); JDDNode union = JDD.Constant(0);
for (JDDNode set : sets) { for (JDDNode set : sets) {
JDD.Ref(filter);
union = JDD.Or(union, JDD.And(set, filter));
if (JDD.AreInterecting(set, filter))
union = JDD.Or(union, set);
else
JDD.Deref(set);
} }
JDD.Deref(filter); JDD.Deref(filter);
return union; return union;

Write Preview
Loading…
Cancel
Save