From 47ab74a16b0eb44aa218206a9687a9c591c4bc45 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 11 Sep 2017 15:32:46 +0200 Subject: [PATCH] implemented single objective queries --- .../SparseMultiObjectivePreprocessor.cpp | 13 +- .../SparseMultiObjectivePreprocessor.h | 1 - .../MultiDimensionalRewardUnfolding.cpp | 105 +++++++---- .../MultiDimensionalRewardUnfolding.h | 19 +- .../prctl/SparseMdpPrctlModelChecker.cpp | 33 +++- .../prctl/helper/SparseMdpPrctlHelper.cpp | 52 ++++- .../prctl/helper/SparseMdpPrctlHelper.h | 7 +- ...MdpMultiDimensionalRewardUnfoldingTest.cpp | 178 ++++++++++++++++++ 8 files changed, 336 insertions(+), 72 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index f541372bc..fb652cd28 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -183,8 +183,6 @@ namespace storm { preprocessUntilFormula(formula.getSubformula().asUntilFormula(), opInfo, data); } else if (formula.getSubformula().isBoundedUntilFormula()){ preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), opInfo, data); - } else if (formula.getSubformula().isMultiObjectiveFormula()){ - preprocessMultiObjectiveSubformula(formula.getSubformula().asMultiObjectiveFormula(), opInfo, data); } else if (formula.getSubformula().isGloballyFormula()){ preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), opInfo, data); } else if (formula.getSubformula().isEventuallyFormula()){ @@ -271,20 +269,11 @@ namespace storm { } - template - void SparseMultiObjectivePreprocessor::preprocessMultiObjectiveSubformula(storm::logic::MultiObjectiveFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { - // Check whether only bounded until formulas are contained - for (auto const& f : formula.getSubformulas()) { - STORM_LOG_THROW(f->isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "MultiObjective subformulas are only allowed if they all contain bounded until formulas"); - } - data.objectives.back()->formula = std::make_shared(formula.asSharedPointer(), opInfo); - } - template void SparseMultiObjectivePreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { // Check how to handle this query - if (formula.getDimension() != 1 || formula.getTimeBoundReference().isRewardBound()) { + if (formula.isMultiDimensional() || formula.getTimeBoundReference().isRewardBound()) { data.objectives.back()->formula = std::make_shared(formula.asSharedPointer(), opInfo); } else if (!formula.hasLowerBound() || (!formula.isLowerBoundStrict() && storm::utility::isZero(formula.template getLowerBound()))) { std::shared_ptr subformula; diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h index 56fb932fb..7def811a1 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h @@ -60,7 +60,6 @@ namespace storm { static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, std::shared_ptr subformula = nullptr); static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); - static void preprocessMultiObjectiveSubformula(storm::logic::MultiObjectiveFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index ccee4a9a7..1e101af6b 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -17,14 +17,38 @@ #include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/IllegalArgumentException.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/InvalidPropertyException.h" namespace storm { namespace modelchecker { namespace multiobjective { template - MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& allowedBottomStates) : model(model), objectives(objectives), possibleECActions(possibleECActions), allowedBottomStates(allowedBottomStates) { + MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::vector> const& objectives) : model(model), objectives(objectives) { + initialize(); + } + template + MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::shared_ptr objectiveFormula) : model(model) { + + STORM_LOG_THROW(objectiveFormula->hasOptimalityType(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + if (objectiveFormula->getSubformula().isMultiObjectiveFormula()) { + for (auto const& subFormula : objectiveFormula->getSubformula().asMultiObjectiveFormula().getSubformulas()) { + STORM_LOG_THROW(subFormula->isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported. Invalid subformula " << *subFormula << "."); + } + } else { + STORM_LOG_THROW(objectiveFormula->getSubformula().isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported. Invalid subformula " << objectiveFormula->getSubformula() << "."); + } + + // Build an objective from the formula. + storm::modelchecker::multiobjective::Objective objective; + objective.formula = objectiveFormula; + objective.originalFormula = objective.formula; + objective.considersComplementaryEvent = false; + objective.lowerResultBound = storm::utility::zero(); + objective.upperResultBound = storm::utility::one(); + objectives.push_back(std::move(objective)); + initialize(); } @@ -46,39 +70,29 @@ namespace storm { for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { auto const& formula = *this->objectives[objIndex].formula; if (formula.isProbabilityOperatorFormula()) { - std::vector> subformulas; - if (formula.getSubformula().isBoundedUntilFormula()) { - subformulas.push_back(formula.getSubformula().asSharedPointer()); - } else if (formula.getSubformula().isMultiObjectiveFormula()) { - subformulas = formula.getSubformula().asMultiObjectiveFormula().getSubformulas(); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unexpected type of subformula for formula " << formula); - } - for (auto const& subformula : subformulas) { - auto const& boundedUntilFormula = subformula->asBoundedUntilFormula(); - for (uint64_t dim = 0; dim < boundedUntilFormula.getDimension(); ++dim) { - subObjectives.push_back(std::make_pair(boundedUntilFormula.restrictToDimension(dim), objIndex)); - std::string memLabel = "dim" + std::to_string(subObjectives.size()) + "_maybe"; - while (model.getStateLabeling().containsLabel(memLabel)) { - memLabel = "_" + memLabel; - } - memoryLabels.push_back(memLabel); - if (boundedUntilFormula.getTimeBoundReference(dim).isTimeBound() || boundedUntilFormula.getTimeBoundReference(dim).isStepBound()) { - dimensionWiseEpochSteps.push_back(std::vector(model.getNumberOfChoices(), 1)); - scalingFactors.push_back(storm::utility::one()); - } else { - STORM_LOG_ASSERT(boundedUntilFormula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound."); - std::string const& rewardName = boundedUntilFormula.getTimeBoundReference(dim).getRewardName(); - STORM_LOG_THROW(this->model.hasRewardModel(rewardName), storm::exceptions::IllegalArgumentException, "No reward model with name '" << rewardName << "' found."); - auto const& rewardModel = this->model.getRewardModel(rewardName); - STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are currently not supported as reward bounds."); - std::vector actionRewards = rewardModel.getTotalRewardVector(this->model.getTransitionMatrix()); - auto discretizedRewardsAndFactor = storm::utility::vector::toIntegralVector(actionRewards); - dimensionWiseEpochSteps.push_back(std::move(discretizedRewardsAndFactor.first)); - scalingFactors.push_back(std::move(discretizedRewardsAndFactor.second)); - } + STORM_LOG_THROW(formula.getSubformula().isBoundedUntilFormula(), storm::exceptions::NotSupportedException, "Unexpected type of subformula for formula " << formula); + auto const& subformula = formula.getSubformula().asBoundedUntilFormula(); + for (uint64_t dim = 0; dim < subformula.getDimension(); ++dim) { + subObjectives.push_back(std::make_pair(subformula.restrictToDimension(dim), objIndex)); + std::string memLabel = "dim" + std::to_string(subObjectives.size()) + "_maybe"; + while (model.getStateLabeling().containsLabel(memLabel)) { + memLabel = "_" + memLabel; + } + memoryLabels.push_back(memLabel); + if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) { + dimensionWiseEpochSteps.push_back(std::vector(model.getNumberOfChoices(), 1)); + scalingFactors.push_back(storm::utility::one()); + } else { + STORM_LOG_ASSERT(subformula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound."); + std::string const& rewardName = subformula.getTimeBoundReference(dim).getRewardName(); + STORM_LOG_THROW(this->model.hasRewardModel(rewardName), storm::exceptions::IllegalArgumentException, "No reward model with name '" << rewardName << "' found."); + auto const& rewardModel = this->model.getRewardModel(rewardName); + STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are currently not supported as reward bounds."); + std::vector actionRewards = rewardModel.getTotalRewardVector(this->model.getTransitionMatrix()); + auto discretizedRewardsAndFactor = storm::utility::vector::toIntegralVector(actionRewards); + dimensionWiseEpochSteps.push_back(std::move(discretizedRewardsAndFactor.first)); + scalingFactors.push_back(std::move(discretizedRewardsAndFactor.second)); } - } } else if (formula.isRewardOperatorFormula() && formula.getSubformula().isCumulativeRewardFormula()) { subObjectives.push_back(std::make_pair(formula.getSubformula().asSharedPointer(), objIndex)); @@ -424,8 +438,7 @@ namespace storm { storm::storage::BitVector MultiDimensionalRewardUnfolding::computeProductInStatesForEpochClass(Epoch const& epoch) { storm::storage::SparseMatrix const& productMatrix = memoryProduct.getProduct().getTransitionMatrix(); - storm::storage::BitVector result(productMatrix.getRowGroupCount(), false); - result.set(*memoryProduct.getProduct().getInitialStates().begin(), true); + storm::storage::BitVector result = memoryProduct.getProduct().getInitialStates(); // Perform DFS storm::storage::BitVector reachableStates = result; std::vector stack(reachableStates.begin(), reachableStates.end()); @@ -588,9 +601,23 @@ namespace storm { template typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getInitialStateResult(Epoch const& epoch) { + STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "The model has multiple initial states."); + STORM_LOG_ASSERT(memoryProduct.getProduct().getInitialStates().getNumberOfSetBits() == 1, "The product has multiple initial states."); return getStateSolution(epoch, *memoryProduct.getProduct().getInitialStates().begin()); } + template + typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getInitialStateResult(Epoch const& epoch, uint64_t initialStateIndex) { + STORM_LOG_ASSERT(model.getInitialStates().get(initialStateIndex), "The given model state is not an initial state."); + for (uint64_t memState = 0; memState < memoryProduct.getNumberOfMemoryState(); ++memState) { + uint64_t productState = memoryProduct.getProductState(initialStateIndex, memState); + if (memoryProduct.getProduct().getInitialStates().get(productState)) { + return getStateSolution(epoch, productState); + } + } + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not find the initial product state corresponding to the given initial model state."); + return getStateSolution(epoch, -1ull); + } template storm::storage::MemoryStructure MultiDimensionalRewardUnfolding::computeMemoryStructure() const { @@ -854,15 +881,23 @@ namespace storm { template storm::storage::BitVector const& MultiDimensionalRewardUnfolding::MemoryProduct::convertMemoryState(uint64_t const& memoryState) const { + STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to convert a memory state, but the memoryStateMap is not yet initialized."); return memoryStateMap[memoryState]; } template uint64_t MultiDimensionalRewardUnfolding::MemoryProduct::convertMemoryState(storm::storage::BitVector const& memoryState) const { + STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to convert a memory state, but the memoryStateMap is not yet initialized."); auto memStateIt = std::find(memoryStateMap.begin(), memoryStateMap.end(), memoryState); return memStateIt - memoryStateMap.begin(); } + template + uint64_t MultiDimensionalRewardUnfolding::MemoryProduct::getNumberOfMemoryState() const { + STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to retrieve the number of memory states but the memoryStateMap is not yet initialized."); + return memoryStateMap.size(); + } + template uint64_t MultiDimensionalRewardUnfolding::MemoryProduct::getProductStateFromChoice(uint64_t const& productChoice) const { return choiceToStateMap[productChoice]; diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index db50bfabf..ed0945337 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -5,12 +5,12 @@ #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" #include "storm/modelchecker/multiobjective/Objective.h" +#include "storm/modelchecker/CheckTask.h" #include "storm/models/sparse/Mdp.h" #include "storm/utility/vector.h" #include "storm/storage/memorystructure/MemoryStructure.h" #include "storm/storage/memorystructure/SparseModelMemoryProduct.h" #include "storm/transformer/EndComponentEliminator.h" - #include "storm/utility/Stopwatch.h" namespace storm { @@ -40,14 +40,10 @@ namespace storm { * * @param model The (preprocessed) model * @param objectives The (preprocessed) objectives - * @param possibleECActions Overapproximation of the actions that are part of an EC - * @param allowedBottomStates The states which are allowed to become a bottom state under a considered scheduler * */ - MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, - std::vector> const& objectives, - storm::storage::BitVector const& possibleECActions, - storm::storage::BitVector const& allowedBottomStates); + MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::vector> const& objectives); + MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::shared_ptr objectiveFormula); ~MultiDimensionalRewardUnfolding() { std::cout << "Unfolding statistics: " << std::endl; @@ -78,7 +74,8 @@ namespace storm { EpochModel& setCurrentEpoch(Epoch const& epoch); void setSolutionForCurrentEpoch(std::vector& inStateSolutions); - SolutionType const& getInitialStateResult(Epoch const& epoch); + SolutionType const& getInitialStateResult(Epoch const& epoch); // Assumes that the initial state is unique + SolutionType const& getInitialStateResult(Epoch const& epoch, uint64_t initialStateIndex); private: @@ -99,6 +96,8 @@ namespace storm { uint64_t convertMemoryState(storm::storage::BitVector const& memoryState) const; storm::storage::BitVector const& convertMemoryState(uint64_t const& memoryState) const; + uint64_t getNumberOfMemoryState() const; + uint64_t getProductStateFromChoice(uint64_t const& productChoice) const; private: @@ -162,9 +161,7 @@ namespace storm { SolutionType const& getStateSolution(Epoch const& epoch, uint64_t const& productState); storm::models::sparse::Mdp const& model; - std::vector> const& objectives; - storm::storage::BitVector possibleECActions; - storm::storage::BitVector allowedBottomStates; + std::vector> objectives; MemoryProduct memoryProduct; diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 02a91f496..3b9806ae3 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -43,14 +43,14 @@ namespace storm { template bool SparseMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true))) { + if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true))) { return true; } else { // Check whether we consider a multi-objective formula // 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).setRewardBoundedUntilFormulasAllowed(true)); + return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true)); } } @@ -58,14 +58,27 @@ namespace storm { std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); 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(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); - STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); - std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); - std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *minMaxLinearEquationSolverFactory, checkTask.getHint()); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + if (pathFormula.isMultiDimensional() || pathFormula.getTimeBoundReference().isRewardBound()) { + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking non-trivial bounded until probabilities can only be computed for the initial states of the model."); + STORM_LOG_WARN_COND(!checkTask.isQualitativeSet(), "Checking non-trivial bounded until formulas is not optimized w.r.t. qualitative queries"); + storm::logic::OperatorInformation opInfo(checkTask.getOptimizationDirection()); + if (checkTask.isBoundSet()) { + opInfo.bound = checkTask.getBound(); + } + auto formula = std::make_shared(checkTask.getFormula().asSharedPointer(), opInfo); + storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding rewardUnfolding(this->getModel(), formula); + auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNonTrivialBoundedUntilProbabilities(checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates(), *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } else { + STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); + std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeStepBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *minMaxLinearEquationSolverFactory, checkTask.getHint()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } } template diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 93c1674b0..ca5ff1cae 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -35,7 +35,7 @@ namespace storm { namespace helper { template - std::vector SparseMdpPrctlHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { + std::vector SparseMdpPrctlHelper::computeStepBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); // Determine the states that have 0 probability of reaching the target states. @@ -71,6 +71,56 @@ namespace storm { return result; } + template + std::map SparseMdpPrctlHelper::computeNonTrivialBoundedUntilProbabilities(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + auto initEpoch = rewardUnfolding.getStartEpoch(); + auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch); + + // initialize data that will be needed for each epoch + std::vector x, b, epochResult; + std::unique_ptr> minMaxSolver; + for (auto const& epoch : epochOrder) { + // Update some data for the case that the Matrix has changed + auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); + if (epochModel.epochMatrixChanged) { + x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero()); + minMaxSolver = minMaxLinearEquationSolverFactory.create(epochModel.epochMatrix); + minMaxSolver->setOptimizationDirection(dir); + minMaxSolver->setCachingEnabled(true); + minMaxSolver->setLowerBound(storm::utility::zero()); + minMaxSolver->setUpperBound(storm::utility::one()); + } + + // Prepare the right hand side of the equation system + b.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero()); + std::vector const& objectiveValues = epochModel.objectiveRewards.front(); + for (auto const& choice : epochModel.objectiveRewardFilter.front()) { + b[choice] = objectiveValues[choice]; + } + auto stepSolutionIt = epochModel.stepSolutions.begin(); + for (auto const& choice : epochModel.stepChoices) { + b[choice] += *stepSolutionIt; + ++stepSolutionIt; + } + assert(stepSolutionIt == epochModel.stepSolutions.end()); + + // Solve the minMax equation system + minMaxSolver->solveEquations(x, b); + + // Plug in the result into the reward unfolding + epochResult.resize(epochModel.epochInStates.getNumberOfSetBits()); + storm::utility::vector::selectVectorValues(epochResult, epochModel.epochInStates, x); + rewardUnfolding.setSolutionForCurrentEpoch(epochResult); + } + + std::map result; + for (auto const& initState : initialStates) { + result[initState] = rewardUnfolding.getInitialStateResult(initEpoch, initState); + } + + return result; + } + template std::vector SparseMdpPrctlHelper::computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index e82c89cc2..89505d192 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -6,6 +6,7 @@ #include "storm/modelchecker/hints/ModelCheckerHint.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/MaximalEndComponent.h" +#include "storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h" #include "MDPModelCheckingHelperReturnType.h" #include "storm/utility/solver.h" @@ -33,8 +34,10 @@ namespace storm { template class SparseMdpPrctlHelper { public: - static std::vector computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); - + static std::vector computeStepBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); + + static std::map computeNonTrivialBoundedUntilProbabilities(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); diff --git a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp index 3675ea1cc..8c878eb53 100644 --- a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp @@ -11,6 +11,184 @@ #include "storm/utility/constants.h" #include "storm/api/storm.h" +TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_small) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm"; + std::string constantsDef = "N=2"; + std::string formulasAsString = "Pmax=? [ F{\"r\"}<=1 x=N ] "; + formulasAsString += "; \n Pmax=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )]"; + formulasAsString += "; \n Pmin=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )]"; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsDef); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin();; + std::unique_ptr result; + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(0.5), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(0.125), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[2], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(0.0), result->asExplicitQuantitativeCheckResult()[initState]); + +} + +TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_large) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm"; + std::string constantsDef = "N=10"; + std::string formulasAsString = "Pmax=? [ F{\"r\"}<=5 x=N ] "; + formulasAsString += "; \n Pmax=? [ multi( F{\"r\"}<=5 x=N, F{\"l\"}<=10 x=0 )]"; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsDef); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin();; + + std::unique_ptr result; + + storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + storm::RationalNumber expectedResult = storm::utility::pow(storm::utility::convertNumber(0.5), 5); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::pow(storm::utility::convertNumber(0.5), 15); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + +} + + +TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_tiny_ec) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_reward_bounded.nm"; + std::string constantsDef = ""; + std::string formulasAsString = "Pmax=? [ F{\"a\"}<=3 x=4 ] "; // 0.2 + formulasAsString += "; \n Pmin=? [ F{\"a\"}<=3 x=4 ] "; // 0.0 + formulasAsString += "; \n Pmin=? [ F{\"a\"}<1 x=1 ] "; // 0.0 + formulasAsString += "; \n Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )] "; // 0.02 + formulasAsString += "; \n Pmin=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )] "; // 0.0 + formulasAsString += "; \n Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<13 x=5, F{\"c\"}<2/5 x=3 )] "; // 0.02 + formulasAsString += "; \n Pmax=? [multi( F{\"a\"}<=0 x=3, F{\"b\"}<=17 x=4, F{\"c\"}<4/5 x=5 )] "; // 0.02 + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsDef); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin();; + + std::unique_ptr result; + + storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + storm::RationalNumber expectedResult = storm::utility::convertNumber("1/5"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::convertNumber("0"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[2], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::convertNumber("0"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[3], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::convertNumber("1/50"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[4], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::convertNumber("0"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[5], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::convertNumber("1/50"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[6], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::convertNumber("1/50"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + +} + +TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_zeroconf_dl) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/zeroconf_dl_not_unfolded.nm"; + std::string constantsDef = "N=1000,K=2,reset=true"; + std::string formulasAsString = "Pmin=? [ F{\"t\"}<50 \"ipfound\" ]"; + formulasAsString += "; \n Pmax=? [multi(F{\"t\"}<50 \"ipfound\", F{\"r\"}<=0 \"ipfound\") ]"; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsDef); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin();; + + std::unique_ptr result; + + storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(0.9989804701, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(0.984621063, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + +} + +TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_csma) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm"; + std::string constantsDef = ""; + std::string formulasAsString = "Pmax=? [ F{\"time\"}<=70 \"all_delivered\" ]"; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsDef); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin();; + + std::unique_ptr result; + + storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + storm::RationalNumber expectedResult = storm::utility::convertNumber("29487882838281/35184372088832"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + +} + + + + #if defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) {