|
|
@ -485,6 +485,8 @@ public class ProbModelChecker extends NonProbModelChecker |
|
|
|
|
|
|
|
|
if (useSimplePathAlgo) { |
|
|
if (useSimplePathAlgo) { |
|
|
return checkProbPathFormulaSimple(expr, qual, statesOfInterest); |
|
|
return checkProbPathFormulaSimple(expr, qual, statesOfInterest); |
|
|
|
|
|
} else if (Expression.containsAccumulationExpression(expr)) { |
|
|
|
|
|
throw new PrismException("Model checking of accumulation expressions not supported for this engine!"); |
|
|
} else { |
|
|
} else { |
|
|
return checkProbPathFormulaLTL(expr, qual, statesOfInterest); |
|
|
return checkProbPathFormulaLTL(expr, qual, statesOfInterest); |
|
|
} |
|
|
} |
|
|
|