diff --git a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h new file mode 100644 index 000000000..933e67df0 --- /dev/null +++ b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h @@ -0,0 +1,37 @@ +#pragma once + +#include "storm/logic/Formulas.h" +#include "storm/modelchecker/CheckTask.h" +#include "storm/modelchecker/results/CheckResult.h" +#include "storm/utility/parametric.h" + +namespace storm { + namespace modelchecker { + namespace parametric { + template + + + /*! + * Class to efficiently check a formula on a parametric model on different parameter instantiations + */ + class SparseInstantiationModelChecker { + public: + SparseInstantiationModelChecker(SparseModelType const& parametricModel); + + virtual bool canHandle(CheckTask const& checkTask) = 0; + + virtual void specifyFormula(CheckTask const& checkTask) = 0; + + virtual std::unique_ptr check(storm::utility::parametric::Valuation const& valuation) = 0; + + private: + + SparseModelType const& parametricModel; + + }; + } + } +} + + +#endif //STORM_SPARSEINSTANTIATIONMODELCHECKER_H diff --git a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp new file mode 100644 index 000000000..b4f0a759c --- /dev/null +++ b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp @@ -0,0 +1,5 @@ +// +// Created by Tim Quatmann on 23/02/2017. +// + +#include "SparseInstantiationModelChecker.h" diff --git a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h new file mode 100644 index 000000000..e5559f347 --- /dev/null +++ b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h @@ -0,0 +1,16 @@ +// +// Created by Tim Quatmann on 23/02/2017. +// + +#ifndef STORM_SPARSEINSTANTIATIONMODELCHECKER_H +#define STORM_SPARSEINSTANTIATIONMODELCHECKER_H + + + +class SparseInstantiationModelChecker { + +}; + + + +#endif //STORM_SPARSEINSTANTIATIONMODELCHECKER_H diff --git a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp index a34b2f2dc..7222c866b 100644 --- a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp @@ -31,6 +31,9 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm/logic/FragmentSpecification.h" +#include "storm/transformer/SparseParametricMdpSimplifier.h" + + namespace storm { namespace modelchecker { namespace region { @@ -83,6 +86,17 @@ namespace storm { //The result is already known. Nothing else to do here return; } + + storm::transformer::SparseParametricMdpSimplifier simplifier(*this->getModel()); + if(!simplifier.simplify(*this->getSpecifiedFormula())) { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplification was not possible"); + } + simpleModel = simplifier.getSimplifiedModel(); + STORM_LOG_THROW(simplifier.getSimplifiedFormula()->isOperatorFormula(), storm::exceptions::UnexpectedException, "Expected that the simplified formula is an Operator formula"); + simpleFormula = std::dynamic_pointer_cast(simplifier.getSimplifiedFormula()); + + /* + STORM_LOG_DEBUG("Elimination of deterministic states with constant outgoing transitions is happening now."); // Determine the set of states that is reachable from the initial state without jumping over a target state. storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel()->getTransitionMatrix(), this->getModel()->getInitialStates(), maybeStates, targetStates); @@ -199,6 +213,7 @@ namespace storm { std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); std::shared_ptr eventuallyFormula(new storm::logic::EventuallyFormula(targetFormulaPtr)); simpleFormula = std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(eventuallyFormula, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound()))); + */ } template diff --git a/src/storm/storage/MaximalEndComponentDecomposition.cpp b/src/storm/storage/MaximalEndComponentDecomposition.cpp index d02fd907b..01bb0a1a1 100644 --- a/src/storm/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storm/storage/MaximalEndComponentDecomposition.cpp @@ -196,6 +196,9 @@ namespace storm { #ifdef STORM_HAVE_CARL template class MaximalEndComponentDecomposition; template MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); + + template class MaximalEndComponentDecomposition; + template MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); #endif } } diff --git a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp index 2b24f120f..b251b9043 100644 --- a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp +++ b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp @@ -30,7 +30,7 @@ namespace storm { } storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); - std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->originalModel.getBackwardTransitions(), phiStates, psiStates); + std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->originalModel, phiStates, psiStates); // Only consider the maybestates that are reachable from one initial state without hopping over a target (i.e., prob1) state storm::storage::BitVector reachableGreater0States = storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & ~statesWithProbability01.first, ~statesWithProbability01.first, statesWithProbability01.second); storm::storage::BitVector maybeStates = reachableGreater0States & ~statesWithProbability01.second; @@ -111,7 +111,6 @@ namespace storm { // Only consider the states that are reachable from an initial state without hopping over a target state storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & statesWithProb1, statesWithProb1, targetStates); storm::storage::BitVector maybeStates = reachableStates & ~targetStates; - targetStates = targetStates & reachableStates; // obtain the resulting subsystem std::vector rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); @@ -126,7 +125,7 @@ namespace storm { this->simplifiedFormula = std::make_shared(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation); // Eliminate all states for which all outgoing transitions are constant - this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel); + this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, rewardModelNameAsVector.front()); return true; } diff --git a/src/storm/transformer/SparseParametricMdpSimplifier.cpp b/src/storm/transformer/SparseParametricMdpSimplifier.cpp new file mode 100644 index 000000000..3d978dba2 --- /dev/null +++ b/src/storm/transformer/SparseParametricMdpSimplifier.cpp @@ -0,0 +1,240 @@ +#include "storm/transformer/SparseParametricMdpSimplifier.h" + +#include "storm/adapters/CarlAdapter.h" + +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/transformer/GoalStateMerger.h" +#include "storm/transformer/EndComponentEliminator.h" +#include "storm/utility/graph.h" +#include "storm/utility/vector.h" + +#include +#include + +namespace storm { + namespace transformer { + + template + SparseParametricMdpSimplifier::SparseParametricMdpSimplifier(SparseModelType const& model) : SparseParametricModelSimplifier(model) { + // intentionally left empty + } + + template + bool SparseParametricMdpSimplifier::simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { + bool minimizing = formula.hasOptimalityType() ? storm::solver::minimize(formula.getOptimalityType()) : storm::logic::isLowerBound(formula.getBound().comparisonType); + + // Get the prob0, prob1 and the maybeStates + storm::modelchecker::SparsePropositionalModelChecker propositionalChecker(this->originalModel); + if(!propositionalChecker.canHandle(formula.getSubformula().asUntilFormula().getLeftSubformula()) || !propositionalChecker.canHandle(formula.getSubformula().asUntilFormula().getRightSubformula())) { + STORM_LOG_DEBUG("Can not simplify when Until-formula has non-propositional subformula(s). Formula: " << formula); + return false; + } + storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + std::pair statesWithProbability01 = minimizing ? + storm::utility::graph::performProb01Min(this->originalModel, phiStates, psiStates) : + storm::utility::graph::performProb01Max(this->originalModel, phiStates, psiStates); + + // Only consider the maybestates that are reachable from one initial state without hopping over a target (i.e., prob1) state + storm::storage::BitVector reachableGreater0States = storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & ~statesWithProbability01.first, ~statesWithProbability01.first, statesWithProbability01.second); + storm::storage::BitVector maybeStates = reachableGreater0States & ~statesWithProbability01.second; + + // obtain the resulting subsystem + storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); + this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first); + this->simplifiedModel->getStateLabeling().addLabel("target", statesWithProbability01.second); + this->simplifiedModel->getStateLabeling().addLabel("sink", statesWithProbability01.first); + + // obtain the simplified formula for the simplified model + auto labelFormula = std::make_shared ("target"); + auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Probability); + this->simplifiedFormula = std::make_shared(eventuallyFormula, formula.getOperatorInformation()); + + // Eliminate all states for which all outgoing transitions are constant + this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel); + + // Eliminate the end components that do not contain a target or a sink state (only required if the probability is maximized) + if(!minimizing) { + this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates("target") | this->simplifiedModel->getStates("sink")); + } + + return true; + } + + template + bool SparseParametricMdpSimplifier::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { + STORM_LOG_THROW(!formula.getSubformula().asBoundedUntilFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported."); + STORM_LOG_THROW(formula.getSubformula().asBoundedUntilFormula().hasUpperBound(), storm::exceptions::UnexpectedException, "Expected a bounded until formula with an upper bound."); + STORM_LOG_THROW(formula.getSubformula().asBoundedUntilFormula().isStepBounded(), storm::exceptions::UnexpectedException, "Expected a bounded until formula with step bounds."); + + bool minimizing = formula.hasOptimalityType() ? storm::solver::minimize(formula.getOptimalityType()) : storm::logic::isLowerBound(formula.getBound().comparisonType); + uint_fast64_t upperStepBound = formula.getSubformula().asBoundedUntilFormula().getUpperBound().evaluateAsInt(); + if (formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict()) { + STORM_LOG_THROW(upperStepBound > 0, storm::exceptions::UnexpectedException, "Expected a strict upper bound that is greater than zero."); + --upperStepBound; + } + + // Get the prob0, target, and the maybeStates + storm::modelchecker::SparsePropositionalModelChecker propositionalChecker(this->originalModel); + if(!propositionalChecker.canHandle(formula.getSubformula().asBoundedUntilFormula().getLeftSubformula()) || !propositionalChecker.canHandle(formula.getSubformula().asBoundedUntilFormula().getRightSubformula())) { + STORM_LOG_DEBUG("Can not simplify when Until-formula has non-propositional subformula(s). Formula: " << formula); + return false; + } + storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector probGreater0States = minimizing ? + storm::utility::graph::performProbGreater0A(this->originalModel.getTransitionMatrix(), this->originalModel.getTransitionMatrix().getRowGroupIndices(), this->originalModel.getBackwardTransitions(), phiStates, psiStates, true, upperStepBound) : + storm::utility::graph::performProbGreater0E(this->originalModel.getBackwardTransitions(), phiStates, psiStates, true, upperStepBound); + storm::storage::BitVector prob0States = ~probGreater0States; + + // Only consider the maybestates that are reachable from one initial probGreater0 state within the given amount of steps and without hopping over a target state + storm::storage::BitVector reachableGreater0States = storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & probGreater0States, probGreater0States, psiStates, true, upperStepBound); + storm::storage::BitVector maybeStates = reachableGreater0States & ~psiStates; + + // obtain the resulting subsystem + storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); + this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates); + this->simplifiedModel->getStateLabeling().addLabel("target", psiStates); + this->simplifiedModel->getStateLabeling().addLabel("sink", prob0States); + + // obtain the simplified formula for the simplified model + auto labelFormula = std::make_shared ("target"); + auto boundedUntilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundType::Steps); + this->simplifiedFormula = std::make_shared(boundedUntilFormula, formula.getOperatorInformation()); + + return true; + } + + template + bool SparseParametricMdpSimplifier::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) { + typename SparseModelType::RewardModelType const& originalRewardModel = formula.hasRewardModelName() ? this->originalModel.getRewardModel(formula.getRewardModelName()) : this->originalModel.getUniqueRewardModel(); + + bool minimizing = formula.hasOptimalityType() ? storm::solver::minimize(formula.getOptimalityType()) : storm::logic::isLowerBound(formula.getBound().comparisonType); + + // Get the prob1 and the maybeStates + storm::modelchecker::SparsePropositionalModelChecker propositionalChecker(this->originalModel); + if(!propositionalChecker.canHandle(formula.getSubformula().asEventuallyFormula().getSubformula())) { + STORM_LOG_DEBUG("Can not simplify when reachability reward formula has non-propositional subformula(s). Formula: " << formula); + return false; + } + storm::storage::BitVector targetStates = std::move(propositionalChecker.check(formula.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + // The set of target states can be extended by the states that reach target with probability 1 without collecting any reward + // TODO for the call of Prob1E we could restrict the analysis to actions with zero reward instead of states with zero reward + targetStates = minimizing ? + storm::utility::graph::performProb1E(this->originalModel, this->originalModel.getBackwardTransitions(), originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), targetStates) : + storm::utility::graph::performProb1A(this->originalModel, this->originalModel.getBackwardTransitions(), originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), targetStates); + storm::storage::BitVector statesWithProb1 = minimizing ? + storm::utility::graph::performProb1E(this->originalModel, this->originalModel.getBackwardTransitions(), storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), targetStates) : + storm::utility::graph::performProb1A(this->originalModel, this->originalModel.getBackwardTransitions(), storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), targetStates); + storm::storage::BitVector infinityStates = ~statesWithProb1; + // Only consider the states that are reachable from an initial state without hopping over a target state + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & statesWithProb1, statesWithProb1, targetStates); + storm::storage::BitVector maybeStates = reachableStates & ~targetStates; + + // obtain the resulting subsystem + std::vector rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); + storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); + this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); + this->simplifiedModel->getStateLabeling().addLabel("target", targetStates); + this->simplifiedModel->getStateLabeling().addLabel("sink", infinityStates); + + // obtain the simplified formula for the simplified model + auto labelFormula = std::make_shared ("target"); + auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Reward); + this->simplifiedFormula = std::make_shared(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation); + + // Eliminate all states for which all outgoing transitions are constant + this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, rewardModelNameAsVector.front()); + + // Eliminate the end components in which no reward is collected (only required if rewards are minimized) + this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates("target") | this->simplifiedModel->getStates("sink"), rewardModelNameAsVector.front()); + return true; + } + + template + bool SparseParametricMdpSimplifier::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) { + STORM_LOG_THROW(formula.getSubformula().asCumulativeRewardFormula().isStepBounded(), storm::exceptions::UnexpectedException, "Expected a cumulative reward formula with step bounds."); + + typename SparseModelType::RewardModelType const& originalRewardModel = formula.hasRewardModelName() ? this->originalModel.getRewardModel(formula.getRewardModelName()) : this->originalModel.getUniqueRewardModel(); + + bool minimizing = formula.hasOptimalityType() ? storm::solver::minimize(formula.getOptimalityType()) : storm::logic::isLowerBound(formula.getBound().comparisonType); + uint_fast64_t stepBound = formula.getSubformula().asCumulativeRewardFormula().getBound().evaluateAsInt(); + if (formula.getSubformula().asCumulativeRewardFormula().isBoundStrict()) { + STORM_LOG_THROW(stepBound > 0, storm::exceptions::UnexpectedException, "Expected a strict upper bound that is greater than zero."); + --stepBound; + } + + // Get the states with non-zero reward + storm::storage::BitVector maybeStates = minimizing ? + storm::utility::graph::performProbGreater0A(this->originalModel.getTransitionMatrix(), this->originalModel.getTransitionMatrix().getRowGroupIndices(), this->originalModel.getBackwardTransitions(), storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), ~originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), true, stepBound) : + storm::utility::graph::performProbGreater0E(this->originalModel.getBackwardTransitions(), storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), ~originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), true, stepBound); + storm::storage::BitVector zeroRewardStates = ~maybeStates; + storm::storage::BitVector noStates(this->originalModel.getNumberOfStates(), false); + + // obtain the resulting subsystem + std::vector rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); + storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); + this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector); + + // obtain the simplified formula for the simplified model + this->simplifiedFormula = formula.asSharedPointer(); + + return true; + } + + template + std::shared_ptr SparseParametricMdpSimplifier::eliminateNeutralEndComponents(SparseModelType const& model, storm::storage::BitVector const& ignoredStates, boost::optional const& rewardModelName) { + + // Get the actions that can be part of an EC + storm::storage::BitVector possibleECActions(model.getNumberOfChoices(), true); + for (auto const& state : ignoredStates) { + for(uint_fast64_t actionIndex = model.getTransitionMatrix().getRowGroupIndices()[state]; actionIndex < model.getTransitionMatrix().getRowGroupIndices()[state+1]; ++actionIndex) { + possibleECActions.set(actionIndex, false); + } + } + + // Get the action-based reward values and unselect non-zero reward actions + std::vector actionRewards; + if(rewardModelName) { + actionRewards = model.getRewardModel(*rewardModelName).getTotalRewardVector(model.getTransitionMatrix()); + uint_fast64_t actionIndex = 0; + for (auto const& actionReward : actionRewards) { + if(!storm::utility::isZero(actionReward)) { + possibleECActions.set(actionIndex, false); + } + ++actionIndex; + } + } + + // Invoke EC Elimination + auto ecEliminatorResult = storm::transformer::EndComponentEliminator::transform(model.getTransitionMatrix(), storm::storage::BitVector(model.getNumberOfStates(), true), possibleECActions, storm::storage::BitVector(model.getNumberOfStates(), false)); + + // obtain the reward model for the resulting system + std::unordered_map rewardModels; + if(rewardModelName) { + std::vector newActionRewards(ecEliminatorResult.matrix.getRowCount()); + storm::utility::vector::selectVectorValues(newActionRewards, ecEliminatorResult.newToOldRowMapping, actionRewards); + rewardModels.insert(std::make_pair(*rewardModelName, typename SparseModelType::RewardModelType(boost::none, std::move(actionRewards)))); + } + + // the new labeling + storm::models::sparse::StateLabeling labeling(ecEliminatorResult.matrix.getRowGroupCount()); + for (auto const& label : model.getStateLabeling().getLabels()) { + auto const& origStatesWithLabel = model.getStates(label); + storm::storage::BitVector newStatesWithLabel(ecEliminatorResult.matrix.getRowGroupCount(), false); + for (auto const& origState : origStatesWithLabel) { + newStatesWithLabel.set(ecEliminatorResult.oldToNewStateMapping[origState], true); + } + labeling.addLabel(label, std::move(newStatesWithLabel)); + } + + return std::make_shared(std::move(ecEliminatorResult.matrix), std::move(labeling), std::move(rewardModels)); + } + + + template class SparseParametricMdpSimplifier>; + } +} \ No newline at end of file diff --git a/src/storm/transformer/SparseParametricMdpSimplifier.h b/src/storm/transformer/SparseParametricMdpSimplifier.h new file mode 100644 index 000000000..ebe16f994 --- /dev/null +++ b/src/storm/transformer/SparseParametricMdpSimplifier.h @@ -0,0 +1,41 @@ +#pragma once + + +#include "storm/transformer/SparseParametricModelSimplifier.h" + +namespace storm { + namespace transformer { + + /*! + * This class performs different steps to simplify the given (parametric) model. + * Checking the obtained simplified formula on the simplified model yields the same result as checking the original formula on the original model (wrt. to the initial states of the two models) + * End Components of nondeterministic models are removed whenever this is valid for the corresponding formula. This allows us to apply, e.g., value iteration that does not start from the 0,...,0 vector. + */ + template + class SparseParametricMdpSimplifier : public SparseParametricModelSimplifier { + public: + SparseParametricMdpSimplifier(SparseModelType const& model); + + protected: + + // Perform the simplification for the corresponding formula type + virtual bool simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) override; + virtual bool simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) override; + virtual bool simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) override; + virtual bool simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) override; + + + /*! + * Eliminates all end components of the model satisfying + * * ignoredStates is false for all states of the EC + * * (if rewardModelName is given) there is no reward collected while staying inside the EC. + * + * Eliminating an EC means that it is replaced by a single state whose incoming and outgoing tansitions correspond to the incoming and outgoing transitions of the EC + * + * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given) + */ + static std::shared_ptr eliminateNeutralEndComponents(SparseModelType const& model, storm::storage::BitVector const& ignoredStates, boost::optional const& rewardModelName = boost::none); + + }; + } +} diff --git a/src/storm/transformer/SparseParametricModelSimplifier.cpp b/src/storm/transformer/SparseParametricModelSimplifier.cpp index 96b867aa8..ec35bb45e 100644 --- a/src/storm/transformer/SparseParametricModelSimplifier.cpp +++ b/src/storm/transformer/SparseParametricModelSimplifier.cpp @@ -1,4 +1,5 @@ #include +#include #include "storm/transformer/SparseParametricModelSimplifier.h" @@ -74,7 +75,7 @@ namespace storm { bool SparseParametricModelSimplifier::simplifyForReachabilityProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { // transform to until formula auto untilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asEventuallyFormula().getSubformula().asSharedPointer()); - return simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula(untilFormula,formula.getOperatorInformation())); + return simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula(untilFormula, formula.getOperatorInformation())); } template @@ -99,7 +100,7 @@ namespace storm { } template - std::shared_ptr SparseParametricModelSimplifier::eliminateConstantDeterministicStates(SparseModelType const& model) { + std::shared_ptr SparseParametricModelSimplifier::eliminateConstantDeterministicStates(SparseModelType const& model, boost::optional const& rewardModelName) { storm::storage::SparseMatrix const& sparseMatrix = model.getTransitionMatrix(); // Get the states without any label @@ -109,13 +110,10 @@ namespace storm { } considerForElimination.complement(); - // get the state-based reward values (or the 0..0 vector if there are no rewards) - std::vector stateValues; - if(model.hasUniqueRewardModel()) { - stateValues = model.getUniqueRewardModel().getTotalRewardVector(sparseMatrix); - } else { - STORM_LOG_THROW(!model.hasRewardModel(), storm::exceptions::InvalidArgumentException, "Invoked state elimination but there are multiple reward models defined"); - stateValues = std::vector(model.getNumberOfStates(), storm::utility::zero()); + // get the action-based reward values + std::vector actionRewards; + if(rewardModelName) { + actionRewards = model.getRewardModel(*rewardModelName).getTotalRewardVector(sparseMatrix); } // Find the states that are to be eliminated @@ -123,7 +121,7 @@ namespace storm { storm::storage::BitVector keptStates(sparseMatrix.getRowGroupCount(), true); storm::storage::BitVector keptRows(sparseMatrix.getRowCount(), true); for (auto state : considerForElimination) { - if (sparseMatrix.getRowGroupSize(state) == 1 && storm::utility::isConstant(stateValues[state])) { + if (sparseMatrix.getRowGroupSize(state) == 1 && (!rewardModelName.is_initialized() || storm::utility::isConstant(actionRewards[sparseMatrix.getRowGroupIndices()[state]]))) { bool hasOnlyConstEntries = true; for (auto const& entry : sparseMatrix.getRowGroup(state)) { if(!storm::utility::isConstant(entry.getValue())) { @@ -139,19 +137,40 @@ namespace storm { } } + // only keep the relevant reward values and translate them to state-based rewards + std::vector rewardsOfEliminatedStates; + if(rewardModelName) { + rewardsOfEliminatedStates.reserve(model.getNumberOfStates()); + for(uint_fast64_t state = 0; state < model.getNumberOfStates(); ++state) { + if(keptStates.get(state)) { + // The current state will not be eliminated. Hence we do not need to consider its reward during elimination + rewardsOfEliminatedStates.push_back(storm::utility::zero()); + } else { + // We need to keep track of the reward of this state during elimination + rewardsOfEliminatedStates.push_back(std::move(actionRewards[sparseMatrix.getRowGroupIndices()[state]])); + } + } + } else { + rewardsOfEliminatedStates.resize(model.getNumberOfStates(), storm::utility::zero()); + } + + // invoke elimination and obtain resulting transition matrix storm::storage::FlexibleSparseMatrix flexibleMatrix(sparseMatrix); storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(sparseMatrix.transpose(true), true); - storm::solver::stateelimination::PrioritizedStateEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions, statesToEliminate, stateValues); + storm::solver::stateelimination::PrioritizedStateEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions, statesToEliminate, rewardsOfEliminatedStates); stateEliminator.eliminateAll(); + storm::storage::SparseMatrix newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, keptStates); - stateValues = storm::utility::vector::filterVector(stateValues, keptRows); - + // obtain the reward model for the resulting system std::unordered_map rewardModels; - if(model.hasUniqueRewardModel()) { - rewardModels.insert(std::make_pair(model.getRewardModels().begin()->first, typename SparseModelType::RewardModelType(boost::none, stateValues))); + if(rewardModelName) { + actionRewards = storm::utility::vector::filterVector(actionRewards, keptRows); + rewardsOfEliminatedStates = storm::utility::vector::filterVector(rewardsOfEliminatedStates, keptStates); + storm::utility::vector::addVectorToGroupedVector(actionRewards, rewardsOfEliminatedStates, newTransitionMatrix.getRowGroupIndices()); + rewardModels.insert(std::make_pair(*rewardModelName, typename SparseModelType::RewardModelType(boost::none, std::move(actionRewards)))); } - - return std::make_shared(flexibleMatrix.createSparseMatrix(keptRows, keptStates), model.getStateLabeling().getSubLabeling(keptStates), std::move(rewardModels)); + + return std::make_shared(std::move(newTransitionMatrix), model.getStateLabeling().getSubLabeling(keptStates), std::move(rewardModels)); } diff --git a/src/storm/transformer/SparseParametricModelSimplifier.h b/src/storm/transformer/SparseParametricModelSimplifier.h index 323200932..2f7cedd9d 100644 --- a/src/storm/transformer/SparseParametricModelSimplifier.h +++ b/src/storm/transformer/SparseParametricModelSimplifier.h @@ -53,11 +53,11 @@ namespace storm { * * there is only one enabled action (i.e., there is no nondeterministic choice at the state), * * all outgoing transitions are constant, * * there is no statelabel defined, and - * * (if applicable) the reward collected at the state is constant. + * * (if rewardModelName is given) the reward collected at the state is constant. * - * Assumes that there is at most one reward model defined. Otherwise an exception is thrown. + * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given) */ - static std::shared_ptr eliminateConstantDeterministicStates(SparseModelType const& model); + static std::shared_ptr eliminateConstantDeterministicStates(SparseModelType const& model, boost::optional const& rewardModelName = boost::none); SparseModelType const& originalModel; diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 592167496..bcb530c81 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1352,9 +1352,8 @@ namespace storm { template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - + template std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; @@ -1366,7 +1365,7 @@ namespace storm { template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - + template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;