From df6ba12c74de5eb20ca99992c693604c512de3a3 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 15 Aug 2017 17:38:58 +0200 Subject: [PATCH] enabled handling of reward bounded formulas within multi-objective formulas --- src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 6b9026ff0..02a91f496 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -50,7 +50,7 @@ namespace storm { // For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude multiple initial states. if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; if (!checkTask.isOnlyInitialStatesRelevantSet()) return false; - return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true)); + return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true)); } }