TimQu
8 years ago
15 changed files with 528 additions and 22 deletions
-
2src/storm/modelchecker/region/ApproximationModel.cpp
-
2src/storm/modelchecker/region/ApproximationModel.h
-
2src/storm/modelchecker/region/SamplingModel.cpp
-
2src/storm/modelchecker/region/SamplingModel.h
-
20src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp
-
2src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h
-
5src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp
-
2src/storm/modelchecker/region/SparseMdpRegionModelChecker.h
-
8src/storm/modelchecker/region/SparseRegionModelChecker.cpp
-
14src/storm/modelchecker/region/SparseRegionModelChecker.h
-
162src/storm/transformer/GoalStateMerger.h
-
72src/storm/transformer/SparseParametricDtmcSimplifier.cpp
-
29src/storm/transformer/SparseParametricDtmcSimplifier.h
-
159src/storm/transformer/SparseParametricModelSimplifier.cpp
-
69src/storm/transformer/SparseParametricModelSimplifier.h
@ -0,0 +1,162 @@ |
|||
#pragma once |
|||
|
|||
#include <limits> |
|||
#include <memory> |
|||
#include <boost/optional.hpp> |
|||
|
|||
#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 <typename SparseModelType> |
|||
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<SparseModelType> 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<typename SparseModelType::ValueType> 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<uint_fast64_t>::max()), sinkState(std::numeric_limits<uint_fast64_t>::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<uint_fast64_t> oldToNewIndexMap(maybeStates.size(), std::numeric_limits<uint_fast64_t>::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<typename SparseModelType::ValueType> builder(resNumActions, resNumStates, resNumTransitions, true, true, resNumStates); |
|||
uint_fast64_t currRow = 0; |
|||
for (auto state : maybeStates) { |
|||
builder.newRowGroup(currRow); |
|||
boost::optional<typename SparseModelType::ValueType> 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<typename SparseModelType::ValueType>()); |
|||
++currRow; |
|||
} |
|||
if(sinkStateRequired) { |
|||
builder.newRowGroup(currRow); |
|||
builder.addNextValue(currRow, sinkState, storm::utility::one<typename SparseModelType::ValueType>()); |
|||
++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<SparseModelType>(builder.build(), std::move(labeling)); |
|||
} |
|||
}; |
|||
} |
|||
} |
|||
@ -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<typename SparseModelType> |
|||
SparseParametricDtmcSimplifier<SparseModelType>::SparseParametricDtmcSimplifier(SparseModelType const& model) : SparseParametricModelSimplifier<SparseModelType>(model) { |
|||
// intentionally left empty
|
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
bool SparseParametricDtmcSimplifier<SparseModelType>::simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { |
|||
// Get the prob0, prob1 and the maybeStates
|
|||
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> 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<storm::storage::BitVector, storm::storage::BitVector> 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<SparseModelType>::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<storm::logic::AtomicLabelFormula const> ("target"); |
|||
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula const>(labelFormula, storm::logic::FormulaContext::Probability); |
|||
this->simplifiedFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(eventuallyFormula, formula.getOperatorInformation()); |
|||
|
|||
// Eliminate all states for which all outgoing transitions are constant
|
|||
this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel); |
|||
|
|||
return true; |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
bool SparseParametricDtmcSimplifier<SparseModelType>::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { |
|||
// If this method was not overriden by any subclass, simplification is not possible
|
|||
return false; |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
bool SparseParametricDtmcSimplifier<SparseModelType>::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) { |
|||
// If this method was not overriden by any subclass, simplification is not possible
|
|||
return false; |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
bool SparseParametricDtmcSimplifier<SparseModelType>::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) { |
|||
// If this method was not overriden by any subclass, simplification is not possible
|
|||
return false; |
|||
} |
|||
|
|||
template class SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>; |
|||
} |
|||
} |
|||
@ -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<typename SparseModelType> |
|||
class SparseParametricDtmcSimplifier : public SparseParametricModelSimplifier<SparseModelType> { |
|||
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; |
|||
|
|||
}; |
|||
} |
|||
} |
|||
@ -0,0 +1,159 @@ |
|||
#include <storm/exceptions/InvalidArgumentException.h>
|
|||
#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<typename SparseModelType> |
|||
SparseParametricModelSimplifier<SparseModelType>::SparseParametricModelSimplifier(SparseModelType const& model) : originalModel(model) { |
|||
// intentionally left empty
|
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
bool SparseParametricModelSimplifier<SparseModelType>::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<typename SparseModelType> |
|||
std::shared_ptr<SparseModelType> SparseParametricModelSimplifier<SparseModelType>::getSimplifiedModel() const { |
|||
STORM_LOG_THROW(simplifiedModel, storm::exceptions::InvalidStateException, "Tried to get the simplified model but simplification was not invoked before."); |
|||
return simplifiedModel; |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
std::shared_ptr<storm::logic::Formula const> SparseParametricModelSimplifier<SparseModelType>::getSimplifiedFormula() const { |
|||
STORM_LOG_THROW(simplifiedFormula, storm::exceptions::InvalidStateException, "Tried to get the simplified formula but simplification was not invoked before."); |
|||
return simplifiedFormula; |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
bool SparseParametricModelSimplifier<SparseModelType>::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<typename SparseModelType> |
|||
bool SparseParametricModelSimplifier<SparseModelType>::simplifyForReachabilityProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { |
|||
// transform to until formula
|
|||
auto untilFormula = std::make_shared<storm::logic::UntilFormula const>(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asEventuallyFormula().getSubformula().asSharedPointer()); |
|||
return simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula(untilFormula,formula.getOperatorInformation())); |
|||
} |
|||
|
|||
template<typename SparseModelType> |
|||
bool SparseParametricModelSimplifier<SparseModelType>::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<typename SparseModelType> |
|||
bool SparseParametricModelSimplifier<SparseModelType>::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<typename SparseModelType> |
|||
bool SparseParametricModelSimplifier<SparseModelType>::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<typename SparseModelType> |
|||
std::shared_ptr<SparseModelType> SparseParametricModelSimplifier<SparseModelType>::eliminateConstantDeterministicStates(SparseModelType const& model) { |
|||
storm::storage::SparseMatrix<typename SparseModelType::ValueType> 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<typename SparseModelType::ValueType> 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<typename SparseModelType::ValueType>(model.getNumberOfStates(), storm::utility::zero<typename SparseModelType::ValueType>()); |
|||
} |
|||
|
|||
// Find the states that are to be eliminated
|
|||
std::vector<uint_fast64_t> 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<typename SparseModelType::ValueType> flexibleMatrix(sparseMatrix); |
|||
storm::storage::FlexibleSparseMatrix<typename SparseModelType::ValueType> flexibleBackwardTransitions(sparseMatrix.transpose(true), true); |
|||
storm::solver::stateelimination::PrioritizedStateEliminator<typename SparseModelType::ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, statesToEliminate, stateValues); |
|||
stateEliminator.eliminateAll(); |
|||
|
|||
flexibleMatrix.createSubmatrix(keptRows, keptStates); |
|||
stateValues = storm::utility::vector::filterVector(stateValues, keptRows); |
|||
|
|||
std::unordered_map<std::string, typename SparseModelType::RewardModelType> rewardModels; |
|||
if(model.hasUniqueRewardModel()) { |
|||
rewardModels.insert(std::make_pair(model.getRewardModels().begin()->first, typename SparseModelType::RewardModelType(boost::none, stateValues))); |
|||
} |
|||
|
|||
return std::make_shared<SparseModelType>(flexibleMatrix.createSparseMatrix(), model.getStateLabeling().getSubLabeling(keptStates), std::move(rewardModels)); |
|||
} |
|||
|
|||
|
|||
template class SparseParametricModelSimplifier<storm::models::sparse::Dtmc<storm::RationalFunction>>; |
|||
template class SparseParametricModelSimplifier<storm::models::sparse::Mdp<storm::RationalFunction>>; |
|||
} |
|||
} |
|||
@ -0,0 +1,69 @@ |
|||
#pragma once |
|||
|
|||
#include <memory> |
|||
#include <boost/optional.hpp> |
|||
#include <string> |
|||
|
|||
#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<typename SparseModelType> |
|||
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<SparseModelType> 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<storm::logic::Formula const> 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<SparseModelType> eliminateConstantDeterministicStates(SparseModelType const& model); |
|||
|
|||
SparseModelType const& originalModel; |
|||
|
|||
std::shared_ptr<SparseModelType> simplifiedModel; |
|||
std::shared_ptr<storm::logic::Formula const> simplifiedFormula; |
|||
|
|||
}; |
|||
} |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue