diff --git a/src/storm/modelchecker/region/ApproximationModel.cpp b/src/storm/modelchecker/region/ApproximationModel.cpp index 9646193f6..b79fee942 100644 --- a/src/storm/modelchecker/region/ApproximationModel.cpp +++ b/src/storm/modelchecker/region/ApproximationModel.cpp @@ -23,7 +23,7 @@ namespace storm { namespace region { template - ApproximationModel::ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula) { + ApproximationModel::ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula) { //First some simple checks and initializations this->typeOfParametricModel = parametricModel.getType(); if(formula->isProbabilityOperatorFormula()){ diff --git a/src/storm/modelchecker/region/ApproximationModel.h b/src/storm/modelchecker/region/ApproximationModel.h index 986c555bd..1984afdf7 100644 --- a/src/storm/modelchecker/region/ApproximationModel.h +++ b/src/storm/modelchecker/region/ApproximationModel.h @@ -40,7 +40,7 @@ namespace storm { * The (single) initial state should be disjoint from these states. (otherwise the result would be independent of the parameters, anyway) * @note This will not check whether approximation is applicable */ - ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula); + ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula); virtual ~ApproximationModel(); /*! diff --git a/src/storm/modelchecker/region/SamplingModel.cpp b/src/storm/modelchecker/region/SamplingModel.cpp index 0aeb8d940..5c312d74d 100644 --- a/src/storm/modelchecker/region/SamplingModel.cpp +++ b/src/storm/modelchecker/region/SamplingModel.cpp @@ -31,7 +31,7 @@ namespace storm { namespace region { template - SamplingModel::SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula) : modelInstantiator(parametricModel){ + SamplingModel::SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula) : modelInstantiator(parametricModel){ //First some simple checks and initializations.. this->typeOfParametricModel = parametricModel.getType(); if(formula->isProbabilityOperatorFormula()){ diff --git a/src/storm/modelchecker/region/SamplingModel.h b/src/storm/modelchecker/region/SamplingModel.h index 1e86b86f9..b0641966c 100644 --- a/src/storm/modelchecker/region/SamplingModel.h +++ b/src/storm/modelchecker/region/SamplingModel.h @@ -40,7 +40,7 @@ namespace storm { * * "sink", labeled on states from which a target state can not be reached. * The (single) initial state should be disjoint from these states. (otherwise the result would be independent of the parameters, anyway) */ - SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula); + SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula); virtual ~SamplingModel(); /*! diff --git a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp index b516515d0..891ff0b53 100644 --- a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -31,6 +31,8 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm/logic/FragmentSpecification.h" +#include "storm/transformer/SparseParametricDtmcSimplifier.h" + namespace storm { namespace modelchecker { namespace region { @@ -72,7 +74,7 @@ namespace storm { template void SparseDtmcRegionModelChecker::preprocess(std::shared_ptr& simpleModel, - std::shared_ptr& simpleFormula, + std::shared_ptr& simpleFormula, bool& isApproximationApplicable, boost::optional& constantResult){ STORM_LOG_DEBUG("Preprocessing for DTMC started."); @@ -95,6 +97,17 @@ namespace storm { //The result is already known. Nothing else to do here return; } + + storm::transformer::SparseParametricDtmcSimplifier 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 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); @@ -241,16 +254,17 @@ namespace storm { std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); if(this->isComputeRewards()){ std::shared_ptr eventuallyFormula(new storm::logic::EventuallyFormula(targetFormulaPtr, storm::logic::FormulaContext::Reward)); - simpleFormula = std::shared_ptr(new storm::logic::RewardOperatorFormula(eventuallyFormula, boost::none, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound()))); + simpleFormula = std::shared_ptr(new storm::logic::RewardOperatorFormula(eventuallyFormula, boost::none, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound()))); } else { 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()))); + simpleFormula = std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(eventuallyFormula, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound()))); } //Check if the reachability function needs to be computed if((this->getSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION) || (this->getSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){ this->computeReachabilityFunction(*(this->getSimpleModel())->template as>()); } + */ } template diff --git a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h index 2cf623802..7fcf92124 100644 --- a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -54,7 +54,7 @@ namespace storm { * * @note this->specifiedFormula and this->computeRewards has to be set accordingly before calling this function */ - virtual void preprocess(std::shared_ptr& simpleModel, std::shared_ptr& simpleFormula, bool& isApproximationApplicable, boost::optional& constantResult); + virtual void preprocess(std::shared_ptr& simpleModel, std::shared_ptr& simpleFormula, bool& isApproximationApplicable, boost::optional& constantResult); private: /*! diff --git a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp index 31d4d5f79..a34b2f2dc 100644 --- a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp @@ -72,7 +72,7 @@ namespace storm { template void SparseMdpRegionModelChecker::preprocess(std::shared_ptr& simpleModel, - std::shared_ptr& simpleFormula, + std::shared_ptr& simpleFormula, bool& isApproximationApplicable, boost::optional& constantResult){ STORM_LOG_DEBUG("Preprocessing for MDPs started."); @@ -104,6 +104,7 @@ namespace storm { //The states that we consider to eliminate storm::storage::BitVector considerToEliminate(submatrix.getRowGroupCount(), true); considerToEliminate.set(initialState, false); + std::vector statesToEliminate; @@ -197,7 +198,7 @@ namespace storm { //Get the simplified formula 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()))); + simpleFormula = std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(eventuallyFormula, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound()))); } template diff --git a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h index 54f63a598..6ceb020b3 100644 --- a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h +++ b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h @@ -40,7 +40,7 @@ namespace storm { * * @note this->specifiedFormula and this->computeRewards has to be set accordingly before calling this function */ - virtual void preprocess(std::shared_ptr& simpleModel, std::shared_ptr& simpleFormula, bool& isApproximationApplicable, boost::optional& constantResult); + virtual void preprocess(std::shared_ptr& simpleModel, std::shared_ptr& simpleFormula, bool& isApproximationApplicable, boost::optional& constantResult); private: /*! diff --git a/src/storm/modelchecker/region/SparseRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseRegionModelChecker.cpp index e98ba6485..1724335cc 100644 --- a/src/storm/modelchecker/region/SparseRegionModelChecker.cpp +++ b/src/storm/modelchecker/region/SparseRegionModelChecker.cpp @@ -73,7 +73,7 @@ namespace storm { } template - std::shared_ptr const& SparseRegionModelChecker::getSpecifiedFormula() const { + std::shared_ptr const& SparseRegionModelChecker::getSpecifiedFormula() const { return this->specifiedFormula; } @@ -103,7 +103,7 @@ namespace storm { } template - std::shared_ptr const& SparseRegionModelChecker::getSimpleFormula() const { + std::shared_ptr const& SparseRegionModelChecker::getSimpleFormula() const { return this->simpleFormula; } @@ -192,7 +192,7 @@ namespace storm { } template - void SparseRegionModelChecker::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula) { + void SparseRegionModelChecker::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula) { std::chrono::high_resolution_clock::time_point timeInitApproxModelStart = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Initializing the Approximation Model..."); STORM_LOG_THROW(this->isApproximationApplicable, storm::exceptions::UnexpectedException, "Approximation model requested but approximation is not applicable"); @@ -203,7 +203,7 @@ namespace storm { } template - void SparseRegionModelChecker::initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula) { + void SparseRegionModelChecker::initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula) { STORM_LOG_DEBUG("Initializing the Sampling Model...."); std::chrono::high_resolution_clock::time_point timeInitSamplingModelStart = std::chrono::high_resolution_clock::now(); this->samplingModel=std::make_shared>(model, formula); diff --git a/src/storm/modelchecker/region/SparseRegionModelChecker.h b/src/storm/modelchecker/region/SparseRegionModelChecker.h index 3fd20be67..4fcf18551 100644 --- a/src/storm/modelchecker/region/SparseRegionModelChecker.h +++ b/src/storm/modelchecker/region/SparseRegionModelChecker.h @@ -150,7 +150,7 @@ namespace storm { /*! * Returns the formula that has been specified upon initialization of this */ - std::shared_ptr const& getSpecifiedFormula() const; + std::shared_ptr const& getSpecifiedFormula() const; //SparseRegionModelCheckerSettings& getSettings(); SparseRegionModelCheckerSettings const& getSettings() const; @@ -165,7 +165,7 @@ namespace storm { bool const& isComputeRewards() const; bool isResultConstant() const; std::shared_ptr const& getSimpleModel() const; - std::shared_ptr const& getSimpleFormula() const; + std::shared_ptr const& getSimpleFormula() const; /*! * Makes the required preprocessing steps for the specified model and formula @@ -174,7 +174,7 @@ namespace storm { * In the latter case, the result is already computed and set to the given parameter. (otherwise the parameter is not touched). * @note this->specifiedFormula and this->computeRewards has to be set accordingly, before calling this function */ - virtual void preprocess(std::shared_ptr& simpleModel, std::shared_ptr& simpleFormula, bool& isApproximationApplicable, boost::optional& constantResult) = 0; + virtual void preprocess(std::shared_ptr& simpleModel, std::shared_ptr& simpleFormula, bool& isApproximationApplicable, boost::optional& constantResult) = 0; /*! * Instantiates the approximation model to compute bounds on the maximal/minimal reachability probability (or reachability reward). @@ -236,23 +236,23 @@ namespace storm { * * @note does not check whether approximation can be applied */ - void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula); + void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula); /*! * initializes the Sampling Model */ - void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula); + void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula); // The model this model checker is supposed to analyze. std::shared_ptr model; //The currently specified formula - std::shared_ptr specifiedFormula; + std::shared_ptr specifiedFormula; //A flag that is true iff we are interested in rewards bool computeRewards; // the original model after states with constant transitions have been eliminated std::shared_ptr simpleModel; // a formula that can be checked on the simplified model - std::shared_ptr simpleFormula; + std::shared_ptr simpleFormula; // a flag that is true if approximation is applicable, i.e., there are only linear functions at transitions of the model bool isApproximationApplicable; // the model that is used to approximate the reachability values diff --git a/src/storm/transformer/GoalStateMerger.h b/src/storm/transformer/GoalStateMerger.h new file mode 100644 index 000000000..08d8cb684 --- /dev/null +++ b/src/storm/transformer/GoalStateMerger.h @@ -0,0 +1,162 @@ +#pragma once + +#include +#include +#include + +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Mdp.h" + +#include "storm/exceptions/InvalidArgumentException.h" + + +namespace storm { + namespace transformer { + + /* + * Merges the given target and sink states into a single state with a selfloop + */ + template + class GoalStateMerger { + public: + + /* Computes a submodel of the specified model that only considers the states given by maybeStates as well as + * * one target state to which all transitions to a state selected by targetStates are redirected and + * * one sink state to which all transitions to a state selected by sinkStates are redirected. + * If there is no transition to either target or sink, the corresponding state will not be created. + * + * The two given bitvectors targetStates and sinkStates are modified such that they represent the corresponding state in the obtained submodel. + * + * Notes: + * * The resulting model will not have any rewardmodels, labels (other then "init") etc. + * * It is assumed that the given set of maybeStates can only be left via either a target or a sink state. Otherwise an exception is thrown. + * * It is assumed that maybeStates, targetStates, and sinkStates are all disjoint. Otherwise an exception is thrown. + */ + static std::shared_ptr mergeTargetAndSinkStates(SparseModelType const& model, storm::storage::BitVector const& maybeStates, storm::storage::BitVector& targetStates, storm::storage::BitVector& sinkStates) { + STORM_LOG_THROW(maybeStates.isDisjointFrom(targetStates) && targetStates.isDisjointFrom(sinkStates) && sinkStates.isDisjointFrom(maybeStates), storm::exceptions::InvalidArgumentException, "maybestates, targetstates, and sinkstates are assumed to be disjoint when creating the submodel. However, this is not the case."); + storm::storage::SparseMatrix const& origMatrix = model.getTransitionMatrix(); + + // Get the number of rows, cols and entries that the resulting transition matrix will have. + uint_fast64_t resNumStates(maybeStates.getNumberOfSetBits()), resNumActions(0), resNumTransitions(0); + bool targetStateRequired = !model.getInitialStates().isDisjointFrom(targetStates); + bool sinkStateRequired = !model.getInitialStates().isDisjointFrom(targetStates); + for( auto state : maybeStates) { + resNumActions += origMatrix.getRowGroupSize(state); + bool hasTransitionToTarget(false), hasTransitionToSink(false); + auto const& endOfRowGroup = origMatrix.getRowGroupIndices()[state+1]; + for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) { + for (auto const& entry : origMatrix.getRow(row)) { + if(maybeStates.get(entry.getColumn())) { + ++resNumTransitions; + } else if (targetStates.get(entry.getColumn())) { + hasTransitionToTarget = true; + } else if (sinkStates.get(entry.getColumn())) { + hasTransitionToSink = true; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "There is a transition originating from a maybestate that does not lead to a maybe-, target-, or sinkstate."); + } + } + if(hasTransitionToTarget) { + ++resNumTransitions; + targetStateRequired = true; + } + if(hasTransitionToSink) { + ++resNumTransitions; + sinkStateRequired = true; + } + } + } + + // Get the index of the target/ sink state in the resulting model (if these states will exist) + uint_fast64_t targetState(std::numeric_limits::max()), sinkState(std::numeric_limits::max()); // init with some invalid state + if(targetStateRequired) { + targetState = resNumStates; + ++resNumStates; + ++resNumActions; + ++resNumTransitions; + } + if(sinkStateRequired) { + sinkState = resNumStates; + ++resNumStates; + ++resNumActions; + ++resNumTransitions; + } + + // Get a Mapping that yields for each column in the old matrix the corresponding column in the new matrix + std::vector oldToNewIndexMap(maybeStates.size(), std::numeric_limits::max()); // init with some invalid state + uint_fast64_t newStateIndex = 0; + for (auto maybeState : maybeStates) { + oldToNewIndexMap[maybeState] = newStateIndex; + ++newStateIndex; + } + + // Build the transition matrix + storm::storage::SparseMatrixBuilder builder(resNumActions, resNumStates, resNumTransitions, true, true, resNumStates); + uint_fast64_t currRow = 0; + for (auto state : maybeStates) { + builder.newRowGroup(currRow); + boost::optional targetProbability, sinkProbability; + auto const& endOfRowGroup = origMatrix.getRowGroupIndices()[state+1]; + for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) { + for (auto const& entry : origMatrix.getRow(row)) { + if(maybeStates.get(entry.getColumn())) { + builder.addNextValue(currRow, oldToNewIndexMap[entry.getColumn()], entry.getValue()); + } else if (targetStates.get(entry.getColumn())) { + targetProbability = targetProbability.is_initialized() ? *targetProbability + entry.getValue() : entry.getValue(); + } else if (sinkStates.get(entry.getColumn())) { + sinkProbability = sinkProbability.is_initialized() ? *sinkProbability + entry.getValue() : entry.getValue(); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "There is a transition originating from a maybestate that does not lead to a maybe-, target-, or sinkstate."); + } + } + if(targetProbability) { + builder.addNextValue(currRow, targetState, storm::utility::simplify(*targetProbability)); + } + if(sinkProbability) { + builder.addNextValue(currRow, sinkState, storm::utility::simplify(*sinkProbability)); + } + ++currRow; + } + } + // Add the selfloops at target and sink + if(targetStateRequired) { + builder.newRowGroup(currRow); + builder.addNextValue(currRow, targetState, storm::utility::one()); + ++currRow; + } + if(sinkStateRequired) { + builder.newRowGroup(currRow); + builder.addNextValue(currRow, sinkState, storm::utility::one()); + ++currRow; + } + + // Get the labeling for the initial states + storm::storage::BitVector initialStates = model.getInitialStates() % maybeStates; + initialStates.resize(resNumStates, false); + if(!model.getInitialStates().isDisjointFrom(targetStates)) { + initialStates.set(targetState, true); + } + if(!model.getInitialStates().isDisjointFrom(sinkStates)) { + initialStates.set(sinkState, true); + } + storm::models::sparse::StateLabeling labeling(resNumStates); + labeling.addLabel("init", std::move(initialStates)); + + // modify the given target and sink states + targetStates = storm::storage::BitVector(resNumStates, false); + if(targetStateRequired) { + targetStates.set(targetState, true); + } + sinkStates = storm::storage::BitVector(resNumStates, false); + if(sinkStateRequired) { + sinkStates.set(sinkState, true); + } + + // Return the result + return std::make_shared(builder.build(), std::move(labeling)); + } + }; + } +} diff --git a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp new file mode 100644 index 000000000..72ef29b61 --- /dev/null +++ b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp @@ -0,0 +1,72 @@ +#include "storm/transformer/SparseParametricDtmcSimplifier.h" + +#include "storm/adapters/CarlAdapter.h" + +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/transformer/GoalStateMerger.h" +#include "storm/utility/graph.h" + + +namespace storm { + namespace transformer { + + template + SparseParametricDtmcSimplifier::SparseParametricDtmcSimplifier(SparseModelType const& model) : SparseParametricModelSimplifier(model) { + // intentionally left empty + } + + template + bool SparseParametricDtmcSimplifier::simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { + // 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 = storm::utility::graph::performProb01(this->originalModel.getBackwardTransitions(), 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.second); + storm::storage::BitVector maybeStates = reachableGreater0States & ~statesWithProbability01.second; + + // obtain the resulting subsystem + this->simplifiedModel = storm::transformer::GoalStateMerger::mergeTargetAndSinkStates(this->originalModel, 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); + + return true; + } + + template + bool SparseParametricDtmcSimplifier::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { + // If this method was not overriden by any subclass, simplification is not possible + return false; + } + + template + bool SparseParametricDtmcSimplifier::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) { + // If this method was not overriden by any subclass, simplification is not possible + return false; + } + + template + bool SparseParametricDtmcSimplifier::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) { + // If this method was not overriden by any subclass, simplification is not possible + return false; + } + + template class SparseParametricDtmcSimplifier>; + } +} \ No newline at end of file diff --git a/src/storm/transformer/SparseParametricDtmcSimplifier.h b/src/storm/transformer/SparseParametricDtmcSimplifier.h new file mode 100644 index 000000000..5f34b483b --- /dev/null +++ b/src/storm/transformer/SparseParametricDtmcSimplifier.h @@ -0,0 +1,29 @@ +#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 SparseParametricDtmcSimplifier : public SparseParametricModelSimplifier { + public: + SparseParametricDtmcSimplifier(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; + + }; + } +} diff --git a/src/storm/transformer/SparseParametricModelSimplifier.cpp b/src/storm/transformer/SparseParametricModelSimplifier.cpp new file mode 100644 index 000000000..b972e20cd --- /dev/null +++ b/src/storm/transformer/SparseParametricModelSimplifier.cpp @@ -0,0 +1,159 @@ +#include +#include "storm/transformer/SparseParametricModelSimplifier.h" + + +#include "storm/adapters/CarlAdapter.h" + +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/solver/stateelimination/PrioritizedStateEliminator.h" +#include "storm/storage/FlexibleSparseMatrix.h" +#include "storm/utility/vector.h" +#include "storm/exceptions/InvalidStateException.h" +#include "storm/exceptions/NotImplementedException.h" + +namespace storm { + namespace transformer { + + template + SparseParametricModelSimplifier::SparseParametricModelSimplifier(SparseModelType const& model) : originalModel(model) { + // intentionally left empty + } + + template + bool SparseParametricModelSimplifier::simplify(storm::logic::Formula const& formula) { + // Make sure that there is no old result from a previous call + simplifiedModel = nullptr; + simplifiedFormula = nullptr; + if (formula.isProbabilityOperatorFormula()) { + storm::logic::ProbabilityOperatorFormula const& probOpForm = formula.asProbabilityOperatorFormula(); + if (probOpForm.getSubformula().isUntilFormula()) { + return simplifyForUntilProbabilities(probOpForm); + } else if (probOpForm.getSubformula().isReachabilityProbabilityFormula()) { + return simplifyForReachabilityProbabilities(probOpForm); + } else if (probOpForm.getSubformula().isBoundedUntilFormula()) { + return simplifyForBoundedUntilProbabilities(probOpForm); + } + } else if (formula.isRewardOperatorFormula()) { + storm::logic::RewardOperatorFormula rewOpForm = formula.asRewardOperatorFormula(); + if (rewOpForm.getSubformula().isReachabilityRewardFormula()) { + return simplifyForReachabilityRewards(rewOpForm); + } else if (rewOpForm.getSubformula().isCumulativeRewardFormula()) { + return simplifyForCumulativeRewards(rewOpForm); + } + } + // reaching this point means that the provided formula is not supported. Thus, no simplification is possible. + STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + return false; + } + + template + std::shared_ptr SparseParametricModelSimplifier::getSimplifiedModel() const { + STORM_LOG_THROW(simplifiedModel, storm::exceptions::InvalidStateException, "Tried to get the simplified model but simplification was not invoked before."); + return simplifiedModel; + } + + template + std::shared_ptr SparseParametricModelSimplifier::getSimplifiedFormula() const { + STORM_LOG_THROW(simplifiedFormula, storm::exceptions::InvalidStateException, "Tried to get the simplified formula but simplification was not invoked before."); + return simplifiedFormula; + } + + template + bool SparseParametricModelSimplifier::simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { + // If this method was not overriden by any subclass, simplification is not possible + STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + return false; + } + + template + 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())); + } + + template + bool SparseParametricModelSimplifier::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { + // If this method was not overriden by any subclass, simplification is not possible + STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + return false; + } + + template + bool SparseParametricModelSimplifier::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) { + // If this method was not overriden by any subclass, simplification is not possible + STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + return false; + } + + template + bool SparseParametricModelSimplifier::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) { + // If this method was not overriden by any subclass, simplification is not possible + STORM_LOG_DEBUG("Simplification not possible because the formula is not suppoerted. Formula: " << formula); + return false; + } + + template + std::shared_ptr SparseParametricModelSimplifier::eliminateConstantDeterministicStates(SparseModelType const& model) { + storm::storage::SparseMatrix const& sparseMatrix = model.getTransitionMatrix(); + + // Get the states without any label + storm::storage::BitVector considerForElimination(model.getNumberOfStates(), false); + for(auto const& label : model.getStateLabeling().getLabels()) { + considerForElimination |= model.getStateLabeling().getStates(label); + } + 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()); + } + + // Find the states that are to be eliminated + std::vector statesToEliminate; + 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])) { + bool hasOnlyConstEntries = true; + for (auto const& entry : sparseMatrix.getRowGroup(state)) { + if(!storm::utility::isConstant(entry.getColumn())) { + hasOnlyConstEntries = false; + break; + } + } + if (hasOnlyConstEntries) { + statesToEliminate.push_back(state); + keptStates.set(state, false); + keptRows.set(sparseMatrix.getRowGroupIndices()[state], false); + } + } + } + + storm::storage::FlexibleSparseMatrix flexibleMatrix(sparseMatrix); + storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(sparseMatrix.transpose(true), true); + storm::solver::stateelimination::PrioritizedStateEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions, statesToEliminate, stateValues); + stateEliminator.eliminateAll(); + + flexibleMatrix.createSubmatrix(keptRows, keptStates); + stateValues = storm::utility::vector::filterVector(stateValues, keptRows); + + std::unordered_map rewardModels; + if(model.hasUniqueRewardModel()) { + rewardModels.insert(std::make_pair(model.getRewardModels().begin()->first, typename SparseModelType::RewardModelType(boost::none, stateValues))); + } + + return std::make_shared(flexibleMatrix.createSparseMatrix(), model.getStateLabeling().getSubLabeling(keptStates), std::move(rewardModels)); + } + + + template class SparseParametricModelSimplifier>; + template class SparseParametricModelSimplifier>; + } +} \ No newline at end of file diff --git a/src/storm/transformer/SparseParametricModelSimplifier.h b/src/storm/transformer/SparseParametricModelSimplifier.h new file mode 100644 index 000000000..323200932 --- /dev/null +++ b/src/storm/transformer/SparseParametricModelSimplifier.h @@ -0,0 +1,69 @@ +#pragma once + +#include +#include +#include + +#include "storm/logic/Formulas.h" +#include "storm/storage/BitVector.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 SparseParametricModelSimplifier { + public: + SparseParametricModelSimplifier(SparseModelType const& model); + + /* + * Invokes the simplification of the model w.r.t. the given formula. + * Returns true, iff simplification was successful + */ + bool simplify( storm::logic::Formula const& formula); + + /* + * Retrieves the simplified model. + * Note that simplify(formula) needs to be called first and has to return true. Otherwise an exception is thrown + */ + std::shared_ptr getSimplifiedModel() const; + + /* + * Retrieves the simplified formula. + * Note that simplify(formula) needs to be called first and has to return true. Otherwise an exception is thrown + */ + std::shared_ptr getSimplifiedFormula() const; + + + protected: + + // Perform the simplification for the corresponding formula type + virtual bool simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula); + virtual bool simplifyForReachabilityProbabilities(storm::logic::ProbabilityOperatorFormula const& formula); + virtual bool simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula); + virtual bool simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula); + virtual bool simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula); + + /*! + * Eliminates all states that satisfy + * * 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. + * + * Assumes that there is at most one reward model defined. Otherwise an exception is thrown. + */ + static std::shared_ptr eliminateConstantDeterministicStates(SparseModelType const& model); + + SparseModelType const& originalModel; + + std::shared_ptr simplifiedModel; + std::shared_ptr simplifiedFormula; + + }; + } +}