Browse Source

Better error message for non-supported S operator in explicit engine.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6206 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
commit
2884b8b143
  1. 7
      prism/src/explicit/ProbModelChecker.java

7
prism/src/explicit/ProbModelChecker.java

@ -635,9 +635,10 @@ public class ProbModelChecker extends StateModelChecker
// Compute probabilities
switch (modelType) {
/*case CTMC:
probs = ((CTMCModelChecker) this).checkSteadyStateFormula(model, expr.getExpression());
break;*/
case CTMC:
//probs = ((CTMCModelChecker) this).checkSteadyStateFormula(model, expr.getExpression());
//break;
throw new PrismException("Explicit engine does not yet support the S operator for CTMCs");
case DTMC:
probs = ((DTMCModelChecker) this).checkSteadyStateFormula(model, expr.getExpression());
break;

Loading…
Cancel
Save