From 2884b8b1434761d64ddbf05b9d61866037bd6c43 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 16 Dec 2012 22:43:10 +0000 Subject: [PATCH] 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 --- prism/src/explicit/ProbModelChecker.java | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index d0d1cea7..6e06c300 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/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;