diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index eac2e12a8..f68db3db2 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -1,6 +1,8 @@ #include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h" +#include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h" +#include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" @@ -140,8 +142,15 @@ namespace storm { std::unique_ptr subResultPointer = this->check(env, stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getMarkovianStates(), this->getModel().getExitRates()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector()); + + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); + if (checkTask.isProduceSchedulersSet()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); + } + return result; } template @@ -149,8 +158,16 @@ namespace storm { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute long run average rewards in non-closed Markov automaton."); auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rewardModel.get()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); + + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getMarkovianStates(), this->getModel().getExitRates()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); + + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); + if (checkTask.isProduceSchedulersSet()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); + } + return result; } template