diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 26235279..5ba0c5b0 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -143,9 +143,9 @@ public class LTLModelChecker extends PrismComponent * replace them with ExpressionLabel objects L0, L1, etc. Expression passed in is modified directly, but the result * is also returned. As an optimisation, expressions that results in true/false for all states are converted to an * actual true/false, and duplicate results (or their negations) reuse the same label. BitSets giving the states which - * satisfy each label are put into the vector labelDDs, which should be empty when this function is called. + * satisfy each label are put into the vector labelBS, which should be empty when this function is called. */ - public Expression checkMaximalStateFormulas(ProbModelChecker mc, Model model, Expression expr, Vector labelBS) throws PrismException + public Expression checkMaximalStateFormulas(StateModelChecker mc, Model model, Expression expr, Vector labelBS) throws PrismException { // A state formula if (expr.getType() instanceof TypeBool) {