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

LTL model checking code: code tidy and clean-up. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1652 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 16 years ago
parent
3e9a240b71
commit
3bdca763eb
3 changed files with 110 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
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 135
      prism/src/prism/LTLModelChecker.java
  2. 13
      prism/src/prism/NondetModelChecker.java
  3. 13
      prism/src/prism/ProbModelChecker.java

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

@ -43,9 +43,6 @@ public class LTLModelChecker
{
protected Prism prism;
protected PrismLog mainLog;
// DRA/product stuff
protected JDDVars draDDRowVars;
protected JDDVars draDDColVars;
public LTLModelChecker(Prism prism) throws PrismException
{
@ -57,7 +54,8 @@ public class LTLModelChecker
* Extract maximal state formula from an LTL path formula, model check them (with passed in model checker) and
* replace them with ExpressionLabel objects L0, L1, etc. Expression passed in is modified directly, but the result
* is also returned. As an optimisation, model checking that results in true/false for all states is converted to an
* actual true/false, and duplicate results are given the same 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.
*/
public Expression checkMaximalStateFormulas(ModelChecker mc, Model model, Expression expr, Vector<JDDNode> labelDDs)
throws PrismException
@ -113,21 +111,37 @@ public class LTLModelChecker
* @param dra: The DRA
* @param model: The DTMC/CTMC
* @param labelDDs: BDDs giving the set of states for each AP in the DRA
* @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) throws PrismException
public ProbModel constructProductMC(DRA dra, ProbModel model, Vector<JDDNode> labelDDs) throws PrismException
{
return constructProductMC(dra, model, labelDDs, true);
return constructProductMC(dra, model, labelDDs, null, null, true);
}
/**
* Construct product of DRA and DTMC/CTMC.
* @param dra: The DRA
* @param model: The DTMC/CTMC
* @param labelDDs: BDDs giving the set of states for each AP in the 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
*/
public ProbModel constructProductMC(DRA dra, ProbModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy,
JDDVars draDDColVarsCopy) throws PrismException
{
return constructProductMC(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true);
}
/**
* Construct product of DRA and DTMC/CTMC.
* @param dra: The DRA
* @param model: The DTMC/CTMC
* @param labelDDs: BDDs giving the set of states for each AP in the DRA
* @param allInit: Do we assume that all states of the original model are initial states (see below)
* @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 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, 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.
JDDVars varDDRowVars[];
@ -143,6 +157,8 @@ public class LTLModelChecker
Vector<String> newDDVarNames;
VarList newVarList;
String draVar;
// DRA stuff
JDDVars draDDRowVars, draDDColVars;
// Misc
int i, j, n;
boolean before;
@ -171,9 +187,11 @@ public class LTLModelChecker
before = false;
}
// If passed in var lists are null, create new lists
// (which won't be accessible later in this case)
draDDRowVars = (draDDRowVarsCopy == null) ? new JDDVars() : draDDRowVarsCopy;
draDDColVars = (draDDColVarsCopy == null) ? new JDDVars() : draDDColVarsCopy;
// Create the new dd variables
draDDRowVars = new JDDVars();
draDDColVars = new JDDVars();
newDDVarNames = new Vector<String>();
newDDVarNames.addAll(ddVarNames);
j = before ? allDDRowVars.getMinVarIndex() - 2 * n : model.getAllDDColVars().getMaxVarIndex() + 1;
@ -214,7 +232,8 @@ public class LTLModelChecker
}
newVarList = (VarList) varList.clone();
// 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());
// Extra references (because will get derefed when new model is done with)
@ -247,7 +266,7 @@ public class LTLModelChecker
// Create a new model model object to store the product model
ProbModel modelProd = new ProbModel(
// New transition matrix/start state
// New transition matrix/start state
newTrans, newStart,
// Don't pass in any rewards info
new JDDNode[0], new JDDNode[0], new String[0],
@ -270,6 +289,12 @@ public class LTLModelChecker
throw new PrismException("Model-DRA product has deadlock states");
}
// Reference DRA DD vars (if being returned)
if (draDDRowVarsCopy != null)
draDDRowVarsCopy.refAll();
if (draDDColVarsCopy != null)
draDDColVarsCopy.refAll();
return modelProd;
}
@ -281,7 +306,21 @@ public class LTLModelChecker
*/
public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector<JDDNode> labelDDs) throws PrismException
{
return constructProductMDP(dra, model, labelDDs, true);
return constructProductMDP(dra, model, labelDDs, null, null, true);
}
/**
* Construct product of DRA and MDP.
* @param dra: The DRA
* @param model: The MDP
* @param labelDDs: BDDs giving the set of states for each AP in the 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
*/
public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector<JDDNode> labelDDs, JDDVars draDDRowVarsCopy,
JDDVars draDDColVarsCopy) throws PrismException
{
return constructProductMDP(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true);
}
/**
@ -289,9 +328,12 @@ public class LTLModelChecker
* @param dra: The DRA
* @param model: The MDP
* @param labelDDs: BDDs giving the set of states for each AP in the DRA
* @param allInit: Do we assume that all states of the original model are initial states (see below)
* @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 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, 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.
JDDVars varDDRowVars[];
@ -307,6 +349,8 @@ public class LTLModelChecker
Vector<String> newDDVarNames;
VarList newVarList;
String draVar;
// DRA stuff
JDDVars draDDRowVars, draDDColVars;
// Misc
int i, j, n;
boolean before;
@ -335,9 +379,11 @@ public class LTLModelChecker
before = false;
}
// If passed in var lists are null, create new lists
// (which won't be accessible later in this case)
draDDRowVars = (draDDRowVarsCopy == null) ? new JDDVars() : draDDRowVarsCopy;
draDDColVars = (draDDColVarsCopy == null) ? new JDDVars() : draDDColVarsCopy;
// Create the new dd variables
draDDRowVars = new JDDVars();
draDDColVars = new JDDVars();
newDDVarNames = new Vector<String>();
newDDVarNames.addAll(ddVarNames);
j = before ? allDDRowVars.getMinVarIndex() - 2 * n : model.getAllDDColVars().getMaxVarIndex() + 1;
@ -378,7 +424,8 @@ public class LTLModelChecker
}
newVarList = (VarList) varList.clone();
// 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());
// Extra references (because will get derefed when new model is done with)
@ -415,14 +462,15 @@ public class LTLModelChecker
// Create a new model model object to store the product model
NondetModel modelProd = new NondetModel(
// New transition matrix/start state
// New transition matrix/start state
newTrans, newStart,
// Don't pass in any rewards info
new JDDNode[0], new JDDNode[0], new String[0],
// New list of all row/col vars
newAllDDRowVars, newAllDDColVars,
// Nondet variables (unchanged)
model.getAllDDSchedVars(), model.getAllDDSynchVars(), model.getAllDDChoiceVars(), model.getAllDDNondetVars(),
model.getAllDDSchedVars(), model.getAllDDSynchVars(), model.getAllDDChoiceVars(), model
.getAllDDNondetVars(),
// New list of var names
newDDVarNames,
// Module info (unchanged)
@ -440,6 +488,12 @@ public class LTLModelChecker
throw new PrismException("Model-DRA product has deadlock states");
}
// Reference DRA DD vars (if being returned)
if (draDDRowVarsCopy != null)
draDDRowVarsCopy.refAll();
if (draDDColVarsCopy != null)
draDDColVarsCopy.refAll();
return modelProd;
}
@ -449,8 +503,8 @@ public class LTLModelChecker
*
* @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;
DA_State state;
@ -479,8 +533,8 @@ public class LTLModelChecker
// Switch label BDD to col vars
label = JDD.PermuteVariables(label, allDDRowVars, allDDColVars);
// 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
transition = JDD.And(transition, label);
// Add edge BDD to the DRA transition mask
@ -534,20 +588,21 @@ public class LTLModelChecker
*
* @returns a referenced BDD of the union of all the accepting sets
*/
public JDDNode findAcceptingBSCCs(DRA dra, ProbModel model) throws PrismException
public JDDNode findAcceptingBSCCs(DRA dra, JDDVars draDDRowVars, JDDVars draDDColVars, ProbModel model)
throws PrismException
{
SCCComputer sccComputer ;
SCCComputer sccComputer;
JDDNode acceptingStates, allAcceptingStates;
Vector<JDDNode> vectBSCCs, newVectBSCCs;
JDDNode tmp, tmp2;
int i, j, n;
// Compute BSCCs for model
sccComputer = prism.getSCCComputer(model);
sccComputer.computeBSCCs();
vectBSCCs = sccComputer.getVectBSCCs();
JDD.Deref(sccComputer.getNotInBSCCs());
allAcceptingStates = JDD.Constant(0);
// for each acceptance pair (H_i, L_i) in the DRA, build H'_i = S x H_i
@ -572,7 +627,7 @@ public class LTLModelChecker
acceptanceVector_L = JDD.SetVectorElement(acceptanceVector_L, draDDRowVars, j, 1.0);
}
}
// Check each BSCC for inclusion in H_i states
// i.e. restrict each BSCC to H_i states and test if unchanged
n = vectBSCCs.size();
@ -591,20 +646,20 @@ public class LTLModelChecker
JDD.Deref(tmp2);
}
JDD.Deref(acceptanceVector_H);
// Compute union of BSCCs which overlap with acceptanceVector_L
acceptingStates = filteredUnion(newVectBSCCs, acceptanceVector_L);
// Add states to our destination BDD
allAcceptingStates = JDD.Or(allAcceptingStates, acceptingStates);
}
// Deref BSCCs
n = vectBSCCs.size();
for (j = 0; j < n; j++) {
JDD.Deref(vectBSCCs.get(j));
}
return allAcceptingStates;
}
@ -613,11 +668,12 @@ public class LTLModelChecker
*
* @returns a referenced BDD of the union of all the accepting sets
*/
public JDDNode findAcceptingStates(DRA dra, NondetModel model, boolean fairness) throws PrismException
public JDDNode findAcceptingStates(DRA dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars,
boolean fairness) throws PrismException
{
JDDNode acceptingStates, allAcceptingStates;
int i, j;
allAcceptingStates = JDD.Constant(0);
// for each acceptance pair (H_i, L_i) in the DRA, build H'_i = S x H_i
@ -673,7 +729,7 @@ public class LTLModelChecker
// Add states to our destination BDD
allAcceptingStates = JDD.Or(allAcceptingStates, acceptingStates);
}
return allAcceptingStates;
}
@ -797,7 +853,8 @@ public class LTLModelChecker
// now find the maximal SCCs in (stableSet, stableSetTrans)
Vector<JDDNode> sccs;
sccComputer = prism.getSCCComputer(stableSet, stableSetTrans, model.getAllDDRowVars(), model.getAllDDColVars());
sccComputer = prism.getSCCComputer(stableSet, stableSetTrans, model.getAllDDRowVars(), model
.getAllDDColVars());
sccComputer.computeSCCs();
JDD.Deref(stableSet);
JDD.Deref(stableSetTrans);

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

@ -382,7 +382,7 @@ public class NondetModelChecker extends NonProbModelChecker
NondetModel modelProduct;
NondetModelChecker mcProduct;
JDDNode startMask;
JDDVars draDDRowVars;
JDDVars draDDRowVars, draDDColVars;
int i;
long l;
@ -430,7 +430,9 @@ public class NondetModelChecker extends NonProbModelChecker
// Build product of MDP and automaton
mainLog.println("\nConstructing MDP-DRA product...");
modelProduct = mcLtl.constructProductMDP(dra, model, labelDDs);
draDDRowVars = new JDDVars();
draDDColVars = new JDDVars();
modelProduct = mcLtl.constructProductMDP(dra, model, labelDDs, draDDRowVars, draDDColVars);
mainLog.println();
modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
// prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, null);
@ -438,7 +440,7 @@ public class NondetModelChecker extends NonProbModelChecker
// Find accepting maximum end components
mainLog.println("\nFinding accepting end components...");
JDDNode acc = mcLtl.findAcceptingStates(dra, modelProduct, fairness);
JDDNode acc = mcLtl.findAcceptingStates(dra, modelProduct, draDDRowVars, draDDColVars, fairness);
// Compute reachability probabilities
mainLog.println("\nComputing reachability probabilities...");
@ -457,9 +459,6 @@ public class NondetModelChecker extends NonProbModelChecker
startMask = modelProduct.getStart();
probsProduct.filter(startMask);
// Then sum over DD vars for the DRA state
draDDRowVars = new JDDVars();
draDDRowVars.addVars(modelProduct.getAllDDRowVars());
draDDRowVars.removeVars(allDDRowVars);
probs = probsProduct.sumOverDDVars(draDDRowVars, model);
// Deref, clean up
@ -469,6 +468,8 @@ public class NondetModelChecker extends NonProbModelChecker
JDD.Deref(labelDDs.get(i));
}
JDD.Deref(acc);
draDDRowVars.derefAll();
draDDColVars.derefAll();
return probs;
}

13
prism/src/prism/ProbModelChecker.java
View File

@ -589,7 +589,7 @@ public class ProbModelChecker extends NonProbModelChecker
ProbModel modelProduct;
ProbModelChecker mcProduct;
JDDNode startMask;
JDDVars draDDRowVars;
JDDVars draDDRowVars, draDDColVars;
int i;
long l;
@ -630,7 +630,9 @@ public class ProbModelChecker extends NonProbModelChecker
// Build product of Markov chain and automaton
// (note: might be a CTMC - StochModelChecker extends this class)
mainLog.println("\nConstructing MC-DRA product...");
modelProduct = mcLtl.constructProductMC(dra, model, labelDDs);
draDDRowVars = new JDDVars();
draDDColVars = new JDDVars();
modelProduct = mcLtl.constructProductMC(dra, model, labelDDs, draDDRowVars, draDDColVars);
mainLog.println();
modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
// prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, null);
@ -638,7 +640,7 @@ public class ProbModelChecker extends NonProbModelChecker
// Find accepting maximum end BSCC
mainLog.println("\nFinding accepting BSCCs...");
JDDNode acc = mcLtl.findAcceptingBSCCs(dra, modelProduct);
JDDNode acc = mcLtl.findAcceptingBSCCs(dra, draDDRowVars, draDDColVars, modelProduct);
// Compute reachability probabilities
mainLog.println("\nComputing reachability probabilities...");
@ -652,9 +654,6 @@ public class ProbModelChecker extends NonProbModelChecker
startMask = modelProduct.getStart();
probsProduct.filter(startMask);
// Then sum over DD vars for the DRA state
draDDRowVars = new JDDVars();
draDDRowVars.addVars(modelProduct.getAllDDRowVars());
draDDRowVars.removeVars(allDDRowVars);
probs = probsProduct.sumOverDDVars(draDDRowVars, model);
// Deref, clean up
@ -664,6 +663,8 @@ public class ProbModelChecker extends NonProbModelChecker
JDD.Deref(labelDDs.get(i));
}
JDD.Deref(acc);
draDDRowVars.derefAll();
draDDColVars.derefAll();
return probs;
}

Write Preview
Loading…
Cancel
Save