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

Miscellaneous code changes/tidies - trying to align with prism-games a bit. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6871 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
6df7dbf140
commit
4ee9ed825e
3 changed files with 63 additions and 55 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. 82
      prism/src/explicit/StateModelChecker.java
  2. 23
      prism/src/prism/ModelType.java
  3. 13
      prism/src/prism/StateModelChecker.java

82
prism/src/explicit/StateModelChecker.java
View File

@ -80,7 +80,7 @@ public class StateModelChecker
// PRISM settings object // PRISM settings object
//protected PrismSettings settings = new PrismSettings(); //protected PrismSettings settings = new PrismSettings();
// Flags/settings // Flags/settings
// (NB: defaults do not necessarily coincide with PRISM) // (NB: defaults do not necessarily coincide with PRISM)
@ -134,7 +134,7 @@ public class StateModelChecker
// Verbosity level // Verbosity level
protected int verbosity = 0; protected int verbosity = 0;
// Setters/getters // Setters/getters
/** /**
@ -169,7 +169,7 @@ public class StateModelChecker
} }
// Settings methods // Settings methods
/** /**
* Set settings from a PRISMSettings object. * Set settings from a PRISMSettings object.
*/ */
@ -177,7 +177,7 @@ public class StateModelChecker
{ {
if (settings == null) if (settings == null)
return; return;
verbosity = settings.getBoolean(PrismSettings.PRISM_VERBOSE) ? 10 : 1; verbosity = settings.getBoolean(PrismSettings.PRISM_VERBOSE) ? 10 : 1;
} }
@ -230,13 +230,13 @@ public class StateModelChecker
long timer = 0; long timer = 0;
StateValues vals; StateValues vals;
String resultString; String resultString;
// Create storage for result // Create storage for result
result = new Result(); result = new Result();
// Remove any existing filter info // Remove any existing filter info
currentFilter = null; currentFilter = null;
// The final result of model checking will be a single value. If the expression to be checked does not // The final result of model checking will be a single value. If the expression to be checked does not
// already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap // already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap
// a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not // a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not
@ -269,7 +269,7 @@ public class StateModelChecker
// We stop any additional explanation being displayed to avoid confusion. // We stop any additional explanation being displayed to avoid confusion.
exprFilter.setExplanationEnabled(false); exprFilter.setExplanationEnabled(false);
} }
// For any case where a new filter was created above... // For any case where a new filter was created above...
if (exprFilter != null) { if (exprFilter != null) {
// Make it invisible (not that it will be displayed) // Make it invisible (not that it will be displayed)
@ -292,7 +292,7 @@ public class StateModelChecker
resultString += " (" + expr.getResultName().toLowerCase() + ")"; resultString += " (" + expr.getResultName().toLowerCase() + ")";
resultString += ": " + result.getResultString(); resultString += ": " + result.getResultString();
mainLog.print("\n" + resultString + "\n"); mainLog.print("\n" + resultString + "\n");
// Clean up // Clean up
vals.clear(); vals.clear();
@ -378,7 +378,7 @@ public class StateModelChecker
protected StateValues checkExpressionITE(Model model, ExpressionITE expr) throws PrismException protected StateValues checkExpressionITE(Model model, ExpressionITE expr) throws PrismException
{ {
StateValues res1 = null, res2 = null, res3 = null; StateValues res1 = null, res2 = null, res3 = null;
// Check operands recursively // Check operands recursively
try { try {
res1 = checkExpression(model, expr.getOperand1()); res1 = checkExpression(model, expr.getOperand1());
@ -391,12 +391,12 @@ public class StateModelChecker
res2.clear(); res2.clear();
throw e; throw e;
} }
// Apply operation // Apply operation
res3.applyITE(res1, res2); res3.applyITE(res1, res2);
res1.clear(); res1.clear();
res2.clear(); res2.clear();
return res3; return res3;
} }
@ -407,7 +407,7 @@ public class StateModelChecker
{ {
StateValues res1 = null, res2 = null; StateValues res1 = null, res2 = null;
int op = expr.getOperator(); int op = expr.getOperator();
// Check operands recursively // Check operands recursively
try { try {
res1 = checkExpression(model, expr.getOperand1()); res1 = checkExpression(model, expr.getOperand1());
@ -417,11 +417,11 @@ public class StateModelChecker
res1.clear(); res1.clear();
throw e; throw e;
} }
// Apply operation // Apply operation
res1.applyBinaryOp(op, res2); res1.applyBinaryOp(op, res2);
res2.clear(); res2.clear();
return res1; return res1;
} }
@ -432,17 +432,17 @@ public class StateModelChecker
{ {
StateValues res1 = null; StateValues res1 = null;
int op = expr.getOperator(); int op = expr.getOperator();
// Check operand recursively // Check operand recursively
res1 = checkExpression(model, expr.getOperand()); res1 = checkExpression(model, expr.getOperand());
// Parentheses are easy - nothing to do: // Parentheses are easy - nothing to do:
if (op == ExpressionUnaryOp.PARENTH) if (op == ExpressionUnaryOp.PARENTH)
return res1; return res1;
// Apply operation // Apply operation
res1.applyUnaryOp(op); res1.applyUnaryOp(op);
return res1; return res1;
} }
@ -471,10 +471,10 @@ public class StateModelChecker
{ {
StateValues res1 = null; StateValues res1 = null;
int op = expr.getNameCode(); int op = expr.getNameCode();
// Check operand recursively // Check operand recursively
res1 = checkExpression(model, expr.getOperand(0)); res1 = checkExpression(model, expr.getOperand(0));
// Apply operation // Apply operation
try { try {
res1.applyFunctionUnary(op); res1.applyFunctionUnary(op);
@ -485,15 +485,15 @@ public class StateModelChecker
((PrismLangException) e).setASTElement(expr); ((PrismLangException) e).setASTElement(expr);
throw e; throw e;
} }
return res1; return res1;
} }
protected StateValues checkExpressionFuncBinary(Model model, ExpressionFunc expr) throws PrismException protected StateValues checkExpressionFuncBinary(Model model, ExpressionFunc expr) throws PrismException
{ {
StateValues res1 = null, res2 = null; StateValues res1 = null, res2 = null;
int op = expr.getNameCode(); int op = expr.getNameCode();
// Check operands recursively // Check operands recursively
try { try {
res1 = checkExpression(model, expr.getOperand(0)); res1 = checkExpression(model, expr.getOperand(0));
@ -503,7 +503,7 @@ public class StateModelChecker
res1.clear(); res1.clear();
throw e; throw e;
} }
// Apply operation // Apply operation
try { try {
res1.applyFunctionBinary(op, res2); res1.applyFunctionBinary(op, res2);
@ -517,15 +517,15 @@ public class StateModelChecker
((PrismLangException) e).setASTElement(expr); ((PrismLangException) e).setASTElement(expr);
throw e; throw e;
} }
return res1; return res1;
} }
protected StateValues checkExpressionFuncNary(Model model, ExpressionFunc expr) throws PrismException protected StateValues checkExpressionFuncNary(Model model, ExpressionFunc expr) throws PrismException
{ {
StateValues res1 = null, res2 = null; StateValues res1 = null, res2 = null;
int i, n, op = expr.getNameCode(); int i, n, op = expr.getNameCode();
// Check first operand recursively // Check first operand recursively
res1 = checkExpression(model, expr.getOperand(0)); res1 = checkExpression(model, expr.getOperand(0));
// Go through remaining operands // Go through remaining operands
@ -553,10 +553,10 @@ public class StateModelChecker
throw e; throw e;
} }
} }
return res1; return res1;
} }
/** /**
* Model check a literal. * Model check a literal.
*/ */
@ -596,7 +596,7 @@ public class StateModelChecker
} }
return res; return res;
} }
/** /**
* Model check a label. * Model check a label.
*/ */
@ -692,10 +692,10 @@ public class StateModelChecker
} else { } else {
currentFilter = null; currentFilter = null;
} }
// Check operand recursively // Check operand recursively
vals = checkExpression(model, expr.getOperand()); vals = checkExpression(model, expr.getOperand());
// Print out number of states satisfying filter // Print out number of states satisfying filter
if (!filterInit) if (!filterInit)
mainLog.println("\nStates satisfying filter " + filter + ": " + bsFilter.cardinality()); mainLog.println("\nStates satisfying filter " + filter + ": " + bsFilter.cardinality());
@ -729,7 +729,7 @@ public class StateModelChecker
// Compute min // Compute min
// Store as object/vector // Store as object/vector
resObj = vals.minOverBitSet(bsFilter); resObj = vals.minOverBitSet(bsFilter);
resVals = new StateValues(expr.getType(), resObj, model);
resVals = new StateValues(expr.getType(), resObj, model);
// Create explanation of result and print some details to log // Create explanation of result and print some details to log
resultExpl = "Minimum value over " + filterStatesString; resultExpl = "Minimum value over " + filterStatesString;
mainLog.println("\n" + resultExpl + ": " + resObj); mainLog.println("\n" + resultExpl + ": " + resObj);
@ -742,7 +742,7 @@ public class StateModelChecker
// Compute max // Compute max
// Store as object/vector // Store as object/vector
resObj = vals.maxOverBitSet(bsFilter); resObj = vals.maxOverBitSet(bsFilter);
resVals = new StateValues(expr.getType(), resObj, model);
resVals = new StateValues(expr.getType(), resObj, model);
// Create explanation of result and print some details to log // Create explanation of result and print some details to log
resultExpl = "Maximum value over " + filterStatesString; resultExpl = "Maximum value over " + filterStatesString;
mainLog.println("\n" + resultExpl + ": " + resObj); mainLog.println("\n" + resultExpl + ": " + resObj);
@ -786,7 +786,7 @@ public class StateModelChecker
count = vals.countOverBitSet(bsFilter); count = vals.countOverBitSet(bsFilter);
// Store as object/vector // Store as object/vector
resObj = new Integer(count); resObj = new Integer(count);
resVals = new StateValues(expr.getType(), resObj, model);
resVals = new StateValues(expr.getType(), resObj, model);
// Create explanation of result and print some details to log // Create explanation of result and print some details to log
resultExpl = filterTrue ? "Count of satisfying states" : "Count of satisfying states also in filter"; resultExpl = filterTrue ? "Count of satisfying states" : "Count of satisfying states also in filter";
mainLog.println("\n" + resultExpl + ": " + resObj); mainLog.println("\n" + resultExpl + ": " + resObj);
@ -795,7 +795,7 @@ public class StateModelChecker
// Compute sum // Compute sum
// Store as object/vector // Store as object/vector
resObj = vals.sumOverBitSet(bsFilter); resObj = vals.sumOverBitSet(bsFilter);
resVals = new StateValues(expr.getType(), resObj, model);
resVals = new StateValues(expr.getType(), resObj, model);
// Create explanation of result and print some details to log // Create explanation of result and print some details to log
resultExpl = "Sum over " + filterStatesString; resultExpl = "Sum over " + filterStatesString;
mainLog.println("\n" + resultExpl + ": " + resObj); mainLog.println("\n" + resultExpl + ": " + resObj);
@ -804,7 +804,7 @@ public class StateModelChecker
// Compute average // Compute average
// Store as object/vector // Store as object/vector
resObj = vals.averageOverBitSet(bsFilter); resObj = vals.averageOverBitSet(bsFilter);
resVals = new StateValues(expr.getType(), resObj, model);
resVals = new StateValues(expr.getType(), resObj, model);
// Create explanation of result and print some details to log // Create explanation of result and print some details to log
resultExpl = "Average over " + filterStatesString; resultExpl = "Average over " + filterStatesString;
mainLog.println("\n" + resultExpl + ": " + resObj); mainLog.println("\n" + resultExpl + ": " + resObj);
@ -812,7 +812,7 @@ public class StateModelChecker
case FIRST: case FIRST:
// Find first value // Find first value
resObj = vals.firstFromBitSet(bsFilter); resObj = vals.firstFromBitSet(bsFilter);
resVals = new StateValues(expr.getType(), resObj, model);
resVals = new StateValues(expr.getType(), resObj, model);
// Create explanation of result and print some details to log // Create explanation of result and print some details to log
resultExpl = "Value in "; resultExpl = "Value in ";
if (filterInit) { if (filterInit) {
@ -845,7 +845,7 @@ public class StateModelChecker
b = vals.forallOverBitSet(bsFilter); b = vals.forallOverBitSet(bsFilter);
// Store as object/vector // Store as object/vector
resObj = new Boolean(b); resObj = new Boolean(b);
resVals = new StateValues(expr.getType(), resObj, model);
resVals = new StateValues(expr.getType(), resObj, model);
// Create explanation of result and print some details to log // Create explanation of result and print some details to log
resultExpl = "Property " + (b ? "" : "not ") + "satisfied in "; resultExpl = "Property " + (b ? "" : "not ") + "satisfied in ";
mainLog.print("\nProperty satisfied in " + vals.countOverBitSet(bsFilter)); mainLog.print("\nProperty satisfied in " + vals.countOverBitSet(bsFilter));
@ -873,7 +873,7 @@ public class StateModelChecker
b = vals.existsOverBitSet(bsFilter); b = vals.existsOverBitSet(bsFilter);
// Store as object/vector // Store as object/vector
resObj = new Boolean(b); resObj = new Boolean(b);
resVals = new StateValues(expr.getType(), resObj, model);
resVals = new StateValues(expr.getType(), resObj, model);
// Create explanation of result and print some details to log // Create explanation of result and print some details to log
resultExpl = "Property satisfied in "; resultExpl = "Property satisfied in ";
if (filterTrue) { if (filterTrue) {
@ -893,7 +893,7 @@ public class StateModelChecker
// Find first (only) value // Find first (only) value
// Store as object/vector // Store as object/vector
resObj = vals.firstFromBitSet(bsFilter); resObj = vals.firstFromBitSet(bsFilter);
resVals = new StateValues(expr.getType(), resObj, model);
resVals = new StateValues(expr.getType(), resObj, model);
// Create explanation of result and print some details to log // Create explanation of result and print some details to log
resultExpl = "Value in "; resultExpl = "Value in ";
if (filterInit) { if (filterInit) {
@ -937,7 +937,7 @@ public class StateModelChecker
return resVals; return resVals;
} }
/** /**
* Loads labels from a PRISM labels file and stores them in BitSet objects. * Loads labels from a PRISM labels file and stores them in BitSet objects.
* (Actually, it returns a map from label name Strings to BitSets.) * (Actually, it returns a map from label name Strings to BitSets.)

23
prism/src/prism/ModelType.java
View File

@ -29,7 +29,7 @@ package prism;
public enum ModelType { public enum ModelType {
// List of model types (ordered alphabetically) // List of model types (ordered alphabetically)
CTMC, CTMDP, DTMC, MDP, PTA, STPG;
CTMC, CTMDP, DTMC, MDP, PTA, STPG, SMG;
/** /**
* Get the full name, in words, of the this model type. * Get the full name, in words, of the this model type.
@ -49,11 +49,13 @@ public enum ModelType {
return "probabilistic timed automaton"; return "probabilistic timed automaton";
case STPG: case STPG:
return "stochastic two-player game"; return "stochastic two-player game";
case SMG:
return "stochastic multi-player game";
} }
// Should never happen // Should never happen
return ""; return "";
} }
/** /**
* Get the PRISM keyword for this model type. * Get the PRISM keyword for this model type.
*/ */
@ -72,11 +74,13 @@ public enum ModelType {
return "pta"; return "pta";
case STPG: case STPG:
return "stpg"; return "stpg";
case SMG:
return "smg";
} }
// Should never happen // Should never happen
return ""; return "";
} }
/** /**
* Do the transitions in a choice sum to 1 for this model type? * Do the transitions in a choice sum to 1 for this model type?
* Can also use this to test whether models uses rates or probabilities. * Can also use this to test whether models uses rates or probabilities.
@ -88,6 +92,7 @@ public enum ModelType {
case MDP: case MDP:
case PTA: case PTA:
case STPG: case STPG:
case SMG:
return true; return true;
case CTMC: case CTMC:
case CTMDP: case CTMDP:
@ -96,7 +101,7 @@ public enum ModelType {
// Should never happen // Should never happen
return true; return true;
} }
/** /**
* Are time delay continuous for this model type? * Are time delay continuous for this model type?
*/ */
@ -106,6 +111,7 @@ public enum ModelType {
case DTMC: case DTMC:
case MDP: case MDP:
case STPG: case STPG:
case SMG:
return false; return false;
case PTA: case PTA:
case CTMC: case CTMC:
@ -115,7 +121,7 @@ public enum ModelType {
// Should never happen // Should never happen
return true; return true;
} }
/** /**
* Does this model allow nondeterministic choices? * Does this model allow nondeterministic choices?
*/ */
@ -127,6 +133,7 @@ public enum ModelType {
return false; return false;
case MDP: case MDP:
case STPG: case STPG:
case SMG:
case PTA: case PTA:
case CTMDP: case CTMDP:
return true; return true;
@ -134,7 +141,7 @@ public enum ModelType {
// Should never happen // Should never happen
return true; return true;
} }
/** /**
* Does this model have probabilities or rates? * Does this model have probabilities or rates?
* @return "Probability" or "Rate" * @return "Probability" or "Rate"
@ -149,7 +156,7 @@ public enum ModelType {
return "Probability"; return "Probability";
} }
} }
public static ModelType parseName(String name) public static ModelType parseName(String name)
{ {
if ("ctmc".equals(name)) if ("ctmc".equals(name))
@ -164,6 +171,8 @@ public enum ModelType {
return PTA; return PTA;
else if ("stpg".equals(name)) else if ("stpg".equals(name))
return STPG; return STPG;
else if ("smg".equals(name))
return SMG;
else else
return null; return null;
} }

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

@ -150,7 +150,7 @@ public class StateModelChecker implements ModelChecker
} }
return mc; return mc;
} }
/** /**
* Clean up the dummy model created when using the abbreviated constructor * Clean up the dummy model created when using the abbreviated constructor
*/ */
@ -174,7 +174,7 @@ public class StateModelChecker implements ModelChecker
// Remove any existing filter info // Remove any existing filter info
currentFilter = null; currentFilter = null;
// The final result of model checking will be a single value. If the expression to be checked does not // The final result of model checking will be a single value. If the expression to be checked does not
// already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap // already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap
// a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not // a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not
@ -1060,10 +1060,10 @@ public class StateModelChecker implements ModelChecker
} else { } else {
currentFilter = null; currentFilter = null;
} }
// Check operand recursively // Check operand recursively
vals = checkExpression(expr.getOperand());
vals = checkExpression(expr.getOperand());
// Print out number of states satisfying filter // Print out number of states satisfying filter
if (!filterInit) if (!filterInit)
mainLog.println("\nStates satisfying filter " + filter + ": " + statesFilter.sizeString()); mainLog.println("\nStates satisfying filter " + filter + ": " + statesFilter.sizeString());
@ -1308,8 +1308,7 @@ public class StateModelChecker implements ModelChecker
resVals = vals; resVals = vals;
// Set vals to null to stop it being cleared below // Set vals to null to stop it being cleared below
vals = null; vals = null;
}
else {
} else {
// Find first (only) value // Find first (only) value
d = vals.firstFromBDD(ddFilter); d = vals.firstFromBDD(ddFilter);
// Store as object/vector // Store as object/vector

Write Preview
Loading…
Cancel
Save