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

avoid exportlabels if simulating -sim + -exportlabels -> NullPointerException 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1071 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Mark Kattenbelt 17 years ago
parent
86df494672
commit
c219d996e6
2 changed files with 52 additions and 18 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. 35
      prism/src/prism/PrismCL.java
  2. 35
      prism/src/prism/StateModelChecker.java

35
prism/src/prism/PrismCL.java
View File

@ -255,27 +255,28 @@ public class PrismCL
error(e.getMessage());
}
}
}
// export labels/states
if (exportlabels) {
try {
if (propertiesFile != null) {
definedPFConstants = undefinedConstants.getPFConstantValues();
propertiesFile.setUndefinedConstants(definedPFConstants);
// export labels/states
if (exportlabels) {
try {
if (propertiesFile != null) {
definedPFConstants = undefinedConstants.getPFConstantValues();
propertiesFile.setUndefinedConstants(definedPFConstants);
}
File f = (exportLabelsFilename.equals("stdout")) ? null : new File(exportLabelsFilename);
prism.exportLabelsToFile(model, modulesFile, propertiesFile, exportType, f);
}
// in case of error, report it and proceed
catch (FileNotFoundException e) {
mainLog.println("Couldn't open file \"" + exportLabelsFilename + "\" for output");
}
catch (PrismException e) {
mainLog.println("\nError: " + e.getMessage() + ".");
}
File f = (exportLabelsFilename.equals("stdout")) ? null : new File(exportLabelsFilename);
prism.exportLabelsToFile(model, modulesFile, propertiesFile, exportType, f);
}
// in case of error, report it and proceed
catch (FileNotFoundException e) {
mainLog.println("Couldn't open file \"" + exportLabelsFilename + "\" for output");
}
catch (PrismException e) {
mainLog.println("\nError: " + e.getMessage() + ".");
}
}
// work through list of properties to be checked
for (j = 0; j < numPropertiesToCheck; j++) {

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

@ -768,10 +768,14 @@ public class StateModelChecker implements ModelChecker
return checkExpressionFuncNary(expr);
case ExpressionFunc.FLOOR:
case ExpressionFunc.CEIL:
case ExpressionFunc.BIT_INV:
return checkExpressionFuncUnary(expr);
case ExpressionFunc.POW:
case ExpressionFunc.MOD:
case ExpressionFunc.LOG:
case ExpressionFunc.BIT_AND:
case ExpressionFunc.BIT_OR:
case ExpressionFunc.BIT_XOR:
return checkExpressionFuncBinary(expr);
default:
throw new PrismException("Unrecognised function \"" + expr.getName() + "\"");
@ -803,6 +807,9 @@ public class StateModelChecker implements ModelChecker
case ExpressionFunc.CEIL:
dd1 = JDD.MonadicApply(JDD.CEIL, dd1);
break;
case ExpressionFunc.BIT_INV:
dd1 = JDD.MonadicApply(JDD.BIT_INV, dd1);
break;
}
return new StateProbsMTBDD(dd1, model);
}
@ -819,6 +826,10 @@ public class StateModelChecker implements ModelChecker
for (i = 0; i < n; i++)
dv1.setElement(i, Math.ceil(dv1.getElement(i)));
break;
case ExpressionFunc.BIT_INV:
for (i = 0; i < n; i++)
dv1.setElement(i, ~((int)dv1.getElement(i)));
break;
}
return new StateProbsDV(dv1, model);
}
@ -844,7 +855,8 @@ public class StateModelChecker implements ModelChecker
throw e;
}
// If both operands are symbolic, result will be symbolic
if (res1 instanceof StateProbsMTBDD && res2 instanceof StateProbsMTBDD) {
if (res1 instanceof StateProbsMTBDD && res2 instanceof StateProbsMTBDD)
{
dd1 = ((StateProbsMTBDD) res1).getJDDNode();
dd2 = ((StateProbsMTBDD) res2).getJDDNode();
switch (op) {
@ -857,6 +869,15 @@ public class StateModelChecker implements ModelChecker
case ExpressionFunc.LOG:
dd = JDD.Apply(JDD.LOGXY, dd1, dd2);
break;
case ExpressionFunc.BIT_AND:
dd = JDD.Apply(JDD.BIT_AND, dd1, dd2);
break;
case ExpressionFunc.BIT_OR:
dd = JDD.Apply(JDD.BIT_OR, dd1, dd2);
break;
case ExpressionFunc.BIT_XOR:
dd = JDD.Apply(JDD.BIT_XOR, dd1, dd2);
break;
}
return new StateProbsMTBDD(dd, model);
}
@ -881,6 +902,18 @@ public class StateModelChecker implements ModelChecker
for (i = 0; i < n; i++)
dv1.setElement(i, PrismUtils.log(dv1.getElement(i), dv2.getElement(i)));
break;
case ExpressionFunc.BIT_AND:
for (i = 0; i < n; i++)
dv1.setElement(i, ((int)dv1.getElement(i)) & ((int)dv2.getElement(i)));
break;
case ExpressionFunc.BIT_OR:
for (i = 0; i < n; i++)
dv1.setElement(i, ((int)dv1.getElement(i)) | ((int)dv2.getElement(i)));
break;
case ExpressionFunc.BIT_XOR:
for (i = 0; i < n; i++)
dv1.setElement(i, ((int)dv1.getElement(i)) ^ ((int)dv2.getElement(i)));
break;
}
dv2.clear();
return new StateProbsDV(dv1, model);

Write Preview
Loading…
Cancel
Save