From 2ea728c681bd000f3072f2340b51dfc97947813a Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 10 Feb 2016 10:27:47 +0000 Subject: [PATCH] explicit.LTLModelChecker: accept any StateModelChecker (preparation for upcoming CTMC PCTL*-fix) git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11166 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/LTLModelChecker.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) {