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

Parametric model checking error message. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10208 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
64a0c61fe2
commit
937978da0b
1 changed files with 3 additions and 1 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. 4
      prism/src/param/ParamModelChecker.java

4
prism/src/param/ParamModelChecker.java
View File

@ -895,7 +895,9 @@ final public class ParamModelChecker extends PrismComponent
RegionValues probs = null; RegionValues probs = null;
if (expr instanceof ExpressionTemporal) { if (expr instanceof ExpressionTemporal) {
ExpressionTemporal exprTemp = (ExpressionTemporal) expr; ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
throw new PrismNotSupportedException("Next operator not supported by parametric engine");
} else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
BitSet needStatesInner = new BitSet(model.getNumStates()); BitSet needStatesInner = new BitSet(model.getNumStates());
needStatesInner.set(0, model.getNumStates()); needStatesInner.set(0, model.getNumStates());
RegionValues b1 = checkExpression(model, exprTemp.getOperand1(), needStatesInner); RegionValues b1 = checkExpression(model, exprTemp.getOperand1(), needStatesInner);

Write Preview
Loading…
Cancel
Save