Browse Source
A lot of work on model checker interfaces. In particular, the SCC elimination model checker is almost integrated.
A lot of work on model checker interfaces. In particular, the SCC elimination model checker is almost integrated.
Former-commit-id: bbf988c943
main
dehnert
10 years ago
36 changed files with 1945 additions and 748 deletions
-
2CMakeLists.txt
-
6src/counterexamples/MILPMinimalLabelSetGenerator.h
-
6src/counterexamples/SMTMinimalCommandSetGenerator.h
-
47src/logic/ExpectedTimeOperatorFormula.cpp
-
31src/logic/ExpectedTimeOperatorFormula.h
-
22src/logic/Formula.cpp
-
13src/logic/Formula.h
-
3src/logic/Formulas.h
-
47src/logic/LongRunAverageOperatorFormula.cpp
-
31src/logic/LongRunAverageOperatorFormula.h
-
47src/logic/SteadyStateOperatorFormula.cpp
-
31src/logic/SteadyStateOperatorFormula.h
-
72src/modelchecker/AbstractModelChecker.cpp
-
9src/modelchecker/AbstractModelChecker.h
-
2src/modelchecker/CheckResult.cpp
-
1src/modelchecker/CheckResult.h
-
130src/modelchecker/ExplicitQualitativeCheckResult.cpp
-
41src/modelchecker/ExplicitQualitativeCheckResult.h
-
199src/modelchecker/ExplicitQuantitativeCheckResult.cpp
-
39src/modelchecker/ExplicitQuantitativeCheckResult.h
-
95src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
-
12src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
-
20src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
-
20src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
-
864src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
-
75src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
-
435src/modelchecker/reachability/SparseSccModelChecker.cpp
-
43src/modelchecker/reachability/SparseSccModelChecker.h
-
15src/parser/FormulaParser.cpp
-
4src/parser/FormulaParser.h
-
5src/settings/SettingsManager.cpp
-
8src/settings/SettingsManager.h
-
64src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp
-
73src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h
-
123src/utility/ConstantsComparator.cpp
-
58src/utility/ConstantsComparator.h
@ -0,0 +1,47 @@ |
|||
#include "src/logic/ExpectedTimeOperatorFormula.h"
|
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
bool ExpectedTimeOperatorFormula::isExpectedTimeOperatorFormula() const { |
|||
return true; |
|||
} |
|||
|
|||
bool ExpectedTimeOperatorFormula::isPctlStateFormula() const { |
|||
return this->getSubformula().isPctlStateFormula(); |
|||
} |
|||
|
|||
bool ExpectedTimeOperatorFormula::hasProbabilityOperator() const { |
|||
return this->getSubformula().hasProbabilityOperator(); |
|||
} |
|||
|
|||
bool ExpectedTimeOperatorFormula::hasNestedProbabilityOperators() const { |
|||
return this->getSubformula().hasNestedProbabilityOperators(); |
|||
} |
|||
|
|||
ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
std::ostream& ExpectedTimeOperatorFormula::writeToStream(std::ostream& out) const { |
|||
out << "ET"; |
|||
OperatorFormula::writeToStream(out); |
|||
return out; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,31 @@ |
|||
#ifndef STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_ |
|||
#define STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_ |
|||
|
|||
#include "src/logic/OperatorFormula.h" |
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
class ExpectedTimeOperatorFormula : public OperatorFormula { |
|||
public: |
|||
ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula); |
|||
ExpectedTimeOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula); |
|||
ExpectedTimeOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula); |
|||
ExpectedTimeOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula const> const& subformula); |
|||
ExpectedTimeOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula); |
|||
|
|||
virtual ~ExpectedTimeOperatorFormula() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
virtual bool isExpectedTimeOperatorFormula() const override; |
|||
|
|||
virtual bool isPctlStateFormula() const override; |
|||
virtual bool hasProbabilityOperator() const override; |
|||
virtual bool hasNestedProbabilityOperators() const override; |
|||
|
|||
virtual std::ostream& writeToStream(std::ostream& out) const override; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_ */ |
|||
@ -0,0 +1,47 @@ |
|||
#include "src/logic/LongRunAverageOperatorFormula.h"
|
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
bool LongRunAverageOperatorFormula::isLongRunAverageOperatorFormula() const { |
|||
return true; |
|||
} |
|||
|
|||
bool LongRunAverageOperatorFormula::isPctlStateFormula() const { |
|||
return this->getSubformula().isPctlStateFormula(); |
|||
} |
|||
|
|||
bool LongRunAverageOperatorFormula::hasProbabilityOperator() const { |
|||
return this->getSubformula().hasProbabilityOperator(); |
|||
} |
|||
|
|||
bool LongRunAverageOperatorFormula::hasNestedProbabilityOperators() const { |
|||
return this->getSubformula().hasNestedProbabilityOperators(); |
|||
} |
|||
|
|||
LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
std::ostream& LongRunAverageOperatorFormula::writeToStream(std::ostream& out) const { |
|||
out << "LRA"; |
|||
OperatorFormula::writeToStream(out); |
|||
return out; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,31 @@ |
|||
#ifndef STORM_LOGIC_LONGRUNAVERAGEOPERATORFORMULA_H_ |
|||
#define STORM_LOGIC_LONGRUNAVERAGEOPERATORFORMULA_H_ |
|||
|
|||
#include "src/logic/OperatorFormula.h" |
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
class LongRunAverageOperatorFormula : public OperatorFormula { |
|||
public: |
|||
LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula); |
|||
LongRunAverageOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula); |
|||
LongRunAverageOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula); |
|||
LongRunAverageOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula const> const& subformula); |
|||
LongRunAverageOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula); |
|||
|
|||
virtual ~LongRunAverageOperatorFormula() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
virtual bool isLongRunAverageOperatorFormula() const override; |
|||
|
|||
virtual bool isPctlStateFormula() const override; |
|||
virtual bool hasProbabilityOperator() const override; |
|||
virtual bool hasNestedProbabilityOperators() const override; |
|||
|
|||
virtual std::ostream& writeToStream(std::ostream& out) const override; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_LOGIC_LONGRUNAVERAGEOPERATORFORMULA_H_ */ |
|||
@ -1,47 +0,0 @@ |
|||
#include "src/logic/SteadyStateOperatorFormula.h"
|
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
SteadyStateOperatorFormula::SteadyStateOperatorFormula(std::shared_ptr<Formula const> const& subformula) : SteadyStateOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
SteadyStateOperatorFormula::SteadyStateOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula) : SteadyStateOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
SteadyStateOperatorFormula::SteadyStateOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula) : SteadyStateOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
SteadyStateOperatorFormula::SteadyStateOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula const> const& subformula) : SteadyStateOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
bool SteadyStateOperatorFormula::isSteadyStateOperatorFormula() const { |
|||
return true; |
|||
} |
|||
|
|||
bool SteadyStateOperatorFormula::isPctlStateFormula() const { |
|||
return this->getSubformula().isPctlStateFormula(); |
|||
} |
|||
|
|||
bool SteadyStateOperatorFormula::hasProbabilityOperator() const { |
|||
return this->getSubformula().hasProbabilityOperator(); |
|||
} |
|||
|
|||
bool SteadyStateOperatorFormula::hasNestedProbabilityOperators() const { |
|||
return this->getSubformula().hasNestedProbabilityOperators(); |
|||
} |
|||
|
|||
SteadyStateOperatorFormula::SteadyStateOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
std::ostream& SteadyStateOperatorFormula::writeToStream(std::ostream& out) const { |
|||
out << "S"; |
|||
OperatorFormula::writeToStream(out); |
|||
return out; |
|||
} |
|||
} |
|||
} |
|||
@ -1,31 +0,0 @@ |
|||
#ifndef STORM_LOGIC_STEADYSTATEFORMULA_H_ |
|||
#define STORM_LOGIC_STEADYSTATEFORMULA_H_ |
|||
|
|||
#include "src/logic/OperatorFormula.h" |
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
class SteadyStateOperatorFormula : public OperatorFormula { |
|||
public: |
|||
SteadyStateOperatorFormula(std::shared_ptr<Formula const> const& subformula); |
|||
SteadyStateOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula); |
|||
SteadyStateOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula); |
|||
SteadyStateOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula const> const& subformula); |
|||
SteadyStateOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula); |
|||
|
|||
virtual ~SteadyStateOperatorFormula() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
virtual bool isSteadyStateOperatorFormula() const override; |
|||
|
|||
virtual bool isPctlStateFormula() const override; |
|||
virtual bool hasProbabilityOperator() const override; |
|||
virtual bool hasNestedProbabilityOperators() const override; |
|||
|
|||
virtual std::ostream& writeToStream(std::ostream& out) const override; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_LOGIC_STEADYSTATEFORMULA_H_ */ |
|||
@ -0,0 +1,864 @@ |
|||
#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
|
|||
|
|||
#include <algorithm>
|
|||
|
|||
#ifdef PARAMETRIC_SYSTEMS
|
|||
#include "src/storage/parameters.h"
|
|||
#endif
|
|||
|
|||
#include "src/storage/StronglyConnectedComponentDecomposition.h"
|
|||
|
|||
#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
|
|||
#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
|
|||
|
|||
#include "src/utility/graph.h"
|
|||
#include "src/utility/vector.h"
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/utility/ConstantsComparator.h"
|
|||
|
|||
#include "src/exceptions/InvalidPropertyException.h"
|
|||
#include "src/exceptions/InvalidStateException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
|
|||
template<typename ValueType> |
|||
SparseDtmcEliminationModelChecker<ValueType>::SparseDtmcEliminationModelChecker(storm::models::Dtmc<ValueType> const& model) : model(model) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool SparseDtmcEliminationModelChecker<ValueType>::canHandle(storm::logic::Formula const& formula) const { |
|||
if (formula.isProbabilityOperatorFormula()) { |
|||
storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); |
|||
// The probability operator must not have a bound.
|
|||
if (!probabilityOperatorFormula.hasBound()) { |
|||
return this->canHandle(probabilityOperatorFormula.getSubformula()); |
|||
} |
|||
} else if (formula.isRewardOperatorFormula()) { |
|||
storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula(); |
|||
// The reward operator must not have a bound.
|
|||
if (!rewardOperatorFormula.hasBound()) { |
|||
return this->canHandle(rewardOperatorFormula.getSubformula()); |
|||
} |
|||
} else if (formula.isUntilFormula() || formula.isEventuallyFormula()) { |
|||
if (formula.isUntilFormula()) { |
|||
storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula(); |
|||
if (untilFormula.getLeftSubformula().isPropositionalFormula() && untilFormula.getRightSubformula().isPropositionalFormula()) { |
|||
return true; |
|||
} |
|||
} else if (formula.isEventuallyFormula()) { |
|||
storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula(); |
|||
if (eventuallyFormula.getSubformula().isPropositionalFormula()) { |
|||
return true; |
|||
} |
|||
} |
|||
} else if (formula.isReachabilityRewardFormula()) { |
|||
storm::logic::ReachabilityRewardFormula reachabilityRewardFormula = formula.asReachabilityRewardFormula(); |
|||
if (reachabilityRewardFormula.getSubformula().isPropositionalFormula()) { |
|||
return true; |
|||
} |
|||
} else if (formula.isConditionalPathFormula()) { |
|||
storm::logic::ConditionalPathFormula conditionalPathFormula = formula.asConditionalPathFormula(); |
|||
if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) { |
|||
return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula()); |
|||
} |
|||
} |
|||
return false; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
// Retrieve the appropriate bitvectors by model checking the subformulas.
|
|||
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); |
|||
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); |
|||
storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
|||
storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
|||
|
|||
// Do some sanity checks to establish some required properties.
|
|||
STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); |
|||
|
|||
// Then, compute the subset of states that has a probability of 0 or 1, respectively.
|
|||
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(model, phiStates, psiStates); |
|||
storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; |
|||
storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; |
|||
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); |
|||
|
|||
// If the initial state is known to have either probability 0 or 1, we can directly return the result.
|
|||
if (model.getInitialStates().isDisjointFrom(maybeStates)) { |
|||
STORM_LOG_DEBUG("The probability of all initial states was found in a preprocessing step."); |
|||
return statesWithProbability0.get(*model.getInitialStates().begin()) ? storm::utility::zero<ValueType>() : storm::utility::one<ValueType>(); |
|||
} |
|||
|
|||
// 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(model.getTransitionMatrix(), model.getInitialStates(), maybeStates, statesWithProbability1); |
|||
|
|||
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
|
|||
maybeStates &= reachableStates; |
|||
|
|||
// Create a vector for the probabilities to go to a state with probability 1 in one step.
|
|||
std::vector<ValueType> oneStepProbabilities = model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); |
|||
|
|||
// Determine the set of initial states of the sub-model.
|
|||
storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates; |
|||
|
|||
// We then build the submatrix that only has the transitions of the maybe states.
|
|||
storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); |
|||
storm::storage::SparseMatrix<ValueType> submatrixTransposed = submatrix.transpose(); |
|||
|
|||
// Before starting the model checking process, we assign priorities to states so we can use them to
|
|||
// impose ordering constraints later.
|
|||
std::vector<std::size_t> statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities); |
|||
|
|||
boost::optional<std::vector<ValueType>> missingStateRewards; |
|||
return computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, missingStateRewards, statePriorities); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
// Retrieve the appropriate bitvectors by model checking the subformulas.
|
|||
std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula()); |
|||
storm::storage::BitVector phiStates(model.getNumberOfStates(), true); |
|||
storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
|||
|
|||
// Do some sanity checks to establish some required properties.
|
|||
STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalArgumentException, "Input model does have transition-based rewards, which are currently unsupported."); |
|||
STORM_LOG_THROW(model.hasStateRewards(), storm::exceptions::IllegalArgumentException, "Input model does not have a state-based reward model."); |
|||
STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); |
|||
|
|||
// Then, compute the subset of states that has a reachability reward less than infinity.
|
|||
storm::storage::BitVector trueStates(model.getNumberOfStates(), true); |
|||
storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(model.getBackwardTransitions(), trueStates, psiStates); |
|||
infinityStates.complement(); |
|||
storm::storage::BitVector maybeStates = ~psiStates & ~infinityStates; |
|||
|
|||
// If the initial state is known to have 0 reward or an infinite reward value, we can directly return the result.
|
|||
STORM_LOG_THROW(model.getInitialStates().isDisjointFrom(infinityStates), storm::exceptions::IllegalArgumentException, "Initial state has infinite reward."); |
|||
if (!model.getInitialStates().isDisjointFrom(psiStates)) { |
|||
STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); |
|||
return storm::utility::zero<ValueType>(); |
|||
} |
|||
|
|||
// 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(model.getTransitionMatrix(), model.getInitialStates(), maybeStates, psiStates); |
|||
|
|||
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
|
|||
maybeStates &= reachableStates; |
|||
|
|||
// Create a vector for the probabilities to go to a state with probability 1 in one step.
|
|||
std::vector<ValueType> oneStepProbabilities = model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates); |
|||
|
|||
// Project the state reward vector to all maybe-states.
|
|||
boost::optional<std::vector<ValueType>> stateRewards(maybeStates.getNumberOfSetBits()); |
|||
storm::utility::vector::selectVectorValues(stateRewards.get(), maybeStates, model.getStateRewardVector()); |
|||
|
|||
// Determine the set of initial states of the sub-model.
|
|||
storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates; |
|||
|
|||
// We then build the submatrix that only has the transitions of the maybe states.
|
|||
storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); |
|||
storm::storage::SparseMatrix<ValueType> submatrixTransposed = submatrix.transpose(); |
|||
|
|||
// Before starting the model checking process, we assign priorities to states so we can use them to
|
|||
// impose ordering constraints later.
|
|||
std::vector<std::size_t> statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities); |
|||
|
|||
return computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, stateRewards, statePriorities); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<ValueType>::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
// Retrieve the appropriate bitvectors by model checking the subformulas.
|
|||
STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula."); |
|||
STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula."); |
|||
|
|||
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula().asEventuallyFormula().getSubformula()); |
|||
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula().asEventuallyFormula().getSubformula()); |
|||
storm::storage::BitVector phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
|||
storm::storage::BitVector psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); |
|||
storm::storage::BitVector trueStates(model.getNumberOfStates(), true); |
|||
|
|||
// Do some sanity checks to establish some required properties.
|
|||
STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); |
|||
STORM_LOG_THROW(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() != storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, storm::exceptions::InvalidArgumentException, "Unsupported elimination method for conditional probabilities."); |
|||
|
|||
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions(); |
|||
|
|||
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, trueStates, psiStates); |
|||
storm::storage::BitVector statesWithProbabilityGreater0 = ~statesWithProbability01.first; |
|||
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); |
|||
|
|||
STORM_LOG_THROW(model.getInitialStates().isSubsetOf(statesWithProbabilityGreater0), storm::exceptions::InvalidPropertyException, "The condition of the conditional probability has zero probability."); |
|||
|
|||
// If the initial state is known to have probability 1 of satisfying the condition, we can apply regular model checking.
|
|||
if (model.getInitialStates().isSubsetOf(statesWithProbability1)) { |
|||
std::shared_ptr<storm::logic::BooleanLiteralFormula> trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true); |
|||
std::shared_ptr<storm::logic::UntilFormula> untilFormula = std::make_shared<storm::logic::UntilFormula>(trueFormula, pathFormula.getLeftSubformula().asSharedPointer()); |
|||
return this->computeUntilProbabilities(untilFormula); |
|||
} |
|||
|
|||
// From now on, we know the condition does not have a trivial probability in the initial state.
|
|||
|
|||
// Compute the states that can be reached on a path that has a psi state in it.
|
|||
storm::storage::BitVector statesWithPsiPredecessor = storm::utility::graph::performProbGreater0(model.getTransitionMatrix(), trueStates, psiStates); |
|||
storm::storage::BitVector statesReachingPhi = storm::utility::graph::performProbGreater0(backwardTransitions, trueStates, phiStates); |
|||
|
|||
// The set of states we need to consider are those that have a non-zero probability to satisfy the condition or are on some path that has a psi state in it.
|
|||
STORM_LOG_DEBUG("Initial state: " << model.getInitialStates()); |
|||
STORM_LOG_DEBUG("Phi states: " << phiStates); |
|||
STORM_LOG_DEBUG("Psi state: " << psiStates); |
|||
STORM_LOG_DEBUG("States with probability greater 0 of satisfying the condition: " << statesWithProbabilityGreater0); |
|||
STORM_LOG_DEBUG("States with psi predecessor: " << statesWithPsiPredecessor); |
|||
STORM_LOG_DEBUG("States reaching phi: " << statesReachingPhi); |
|||
storm::storage::BitVector maybeStates = statesWithProbabilityGreater0 | (statesWithPsiPredecessor & statesReachingPhi); |
|||
STORM_LOG_DEBUG("Found " << maybeStates.getNumberOfSetBits() << " relevant states: " << maybeStates); |
|||
|
|||
// Determine the set of initial states of the sub-DTMC.
|
|||
storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates; |
|||
|
|||
// Create a dummy vector for the one-step probabilities.
|
|||
std::vector<ValueType> oneStepProbabilities(maybeStates.getNumberOfSetBits(), storm::utility::zero<ValueType>()); |
|||
|
|||
// We then build the submatrix that only has the transitions of the maybe states.
|
|||
storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); |
|||
storm::storage::SparseMatrix<ValueType> submatrixTransposed = submatrix.transpose(); |
|||
|
|||
// The states we want to eliminate are those that are tagged with "maybe" but are not a phi or psi state.
|
|||
phiStates = phiStates % maybeStates; |
|||
psiStates = psiStates % maybeStates; |
|||
|
|||
// Keep only the states that we do not eliminate in the maybe states.
|
|||
maybeStates = phiStates | psiStates; |
|||
|
|||
STORM_LOG_DEBUG("Phi states in reduced model " << phiStates); |
|||
STORM_LOG_DEBUG("Psi states in reduced model " << psiStates); |
|||
storm::storage::BitVector statesToEliminate = ~maybeStates & ~newInitialStates; |
|||
STORM_LOG_DEBUG("Eliminating the states " << statesToEliminate); |
|||
|
|||
// Before starting the model checking process, we assign priorities to states so we can use them to
|
|||
// impose ordering constraints later.
|
|||
std::vector<std::size_t> statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities); |
|||
|
|||
std::vector<storm::storage::sparse::state_type> states(statesToEliminate.begin(), statesToEliminate.end()); |
|||
|
|||
// Sort the states according to the priorities.
|
|||
std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities[a] < statePriorities[b]; }); |
|||
|
|||
STORM_PRINT_AND_LOG("Computing conditional probilities." << std::endl); |
|||
STORM_PRINT_AND_LOG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); |
|||
boost::optional<std::vector<ValueType>> missingStateRewards; |
|||
FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(submatrix); |
|||
FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrixTransposed, true); |
|||
for (auto const& state : states) { |
|||
eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, missingStateRewards); |
|||
} |
|||
STORM_PRINT_AND_LOG("Eliminated " << states.size() << " states." << std::endl); |
|||
|
|||
eliminateState(flexibleMatrix, oneStepProbabilities, *newInitialStates.begin(), flexibleBackwardTransitions, missingStateRewards, false); |
|||
|
|||
// Now eliminate all chains of phi or psi states.
|
|||
for (auto phiState : phiStates) { |
|||
// Only eliminate the state if it has a successor that is not itself.
|
|||
auto const& currentRow = flexibleMatrix.getRow(phiState); |
|||
if (currentRow.size() == 1) { |
|||
auto const& firstEntry = currentRow.front(); |
|||
if (firstEntry.getColumn() == phiState) { |
|||
break; |
|||
} |
|||
} |
|||
eliminateState(flexibleMatrix, oneStepProbabilities, phiState, flexibleBackwardTransitions, missingStateRewards, false, true, phiStates); |
|||
} |
|||
for (auto psiState : psiStates) { |
|||
// Only eliminate the state if it has a successor that is not itself.
|
|||
auto const& currentRow = flexibleMatrix.getRow(psiState); |
|||
if (currentRow.size() == 1) { |
|||
auto const& firstEntry = currentRow.front(); |
|||
if (firstEntry.getColumn() == psiState) { |
|||
break; |
|||
} |
|||
} |
|||
eliminateState(flexibleMatrix, oneStepProbabilities, psiState, flexibleBackwardTransitions, missingStateRewards, false, true, psiStates); |
|||
} |
|||
|
|||
ValueType numerator = storm::utility::zero<ValueType>(); |
|||
ValueType denominator = storm::utility::zero<ValueType>(); |
|||
|
|||
for (auto const& trans1 : flexibleMatrix.getRow(*newInitialStates.begin())) { |
|||
auto initialStateSuccessor = trans1.getColumn(); |
|||
if (phiStates.get(initialStateSuccessor)) { |
|||
ValueType additiveTerm = storm::utility::zero<ValueType>(); |
|||
for (auto const& trans2 : flexibleMatrix.getRow(initialStateSuccessor)) { |
|||
STORM_LOG_ASSERT(psiStates.get(trans2.getColumn()), "Expected psi state."); |
|||
additiveTerm += trans2.getValue(); |
|||
} |
|||
additiveTerm *= trans1.getValue(); |
|||
numerator += additiveTerm; |
|||
denominator += additiveTerm; |
|||
} else { |
|||
STORM_LOG_ASSERT(psiStates.get(initialStateSuccessor), "Expected psi state."); |
|||
denominator += trans1.getValue(); |
|||
ValueType additiveTerm = storm::utility::zero<ValueType>(); |
|||
for (auto const& trans2 : flexibleMatrix.getRow(initialStateSuccessor)) { |
|||
STORM_LOG_ASSERT(phiStates.get(trans2.getColumn()), "Expected phi state."); |
|||
additiveTerm += trans2.getValue(); |
|||
} |
|||
numerator += trans1.getValue() * additiveTerm; |
|||
} |
|||
} |
|||
|
|||
return numerator / denominator; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<ValueType>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) { |
|||
if (stateFormula.isTrueFormula()) { |
|||
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true))); |
|||
} else { |
|||
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates()))); |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<ValueType>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { |
|||
STORM_LOG_THROW(model.hasAtomicProposition(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); |
|||
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel()))); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
ValueType SparseDtmcEliminationModelChecker<ValueType>::computeReachabilityValue(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<ValueType>>& stateRewards, boost::optional<std::vector<std::size_t>> const& statePriorities) { |
|||
std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); |
|||
std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); |
|||
|
|||
// Create a bit vector that represents the subsystem of states we still have to eliminate.
|
|||
storm::storage::BitVector subsystem = storm::storage::BitVector(transitionMatrix.getRowCount(), true); |
|||
|
|||
// Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
|
|||
FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(transitionMatrix); |
|||
FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions, true); |
|||
auto conversionEnd = std::chrono::high_resolution_clock::now(); |
|||
|
|||
std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now(); |
|||
uint_fast64_t maximalDepth = 0; |
|||
if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State) { |
|||
// If we are required to do pure state elimination, we simply create a vector of all states to
|
|||
// eliminate and sort it according to the given priorities.
|
|||
|
|||
// Remove the initial state from the states which we need to eliminate.
|
|||
subsystem &= ~initialStates; |
|||
std::vector<storm::storage::sparse::state_type> states(subsystem.begin(), subsystem.end()); |
|||
|
|||
if (statePriorities) { |
|||
std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities.get()[a] < statePriorities.get()[b]; }); |
|||
} |
|||
|
|||
STORM_PRINT_AND_LOG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); |
|||
for (auto const& state : states) { |
|||
eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); |
|||
} |
|||
STORM_PRINT_AND_LOG("Eliminated " << states.size() << " states." << std::endl); |
|||
} else if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) { |
|||
// When using the hybrid technique, we recursively treat the SCCs up to some size.
|
|||
storm::utility::ConstantsComparator<ValueType> comparator; |
|||
std::vector<storm::storage::sparse::state_type> entryStateQueue; |
|||
STORM_PRINT_AND_LOG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl); |
|||
maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::sparseDtmcEliminationModelCheckerSettings().getMaximalSccSize(), entryStateQueue, comparator, stateRewards, statePriorities); |
|||
|
|||
// If the entry states were to be eliminated last, we need to do so now.
|
|||
STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step."); |
|||
if (storm::settings::sparseDtmcEliminationModelCheckerSettings().isEliminateEntryStatesLastSet()) { |
|||
for (auto const& state : entryStateQueue) { |
|||
eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); |
|||
} |
|||
} |
|||
STORM_PRINT_AND_LOG("Eliminated " << subsystem.size() << " states." << std::endl); |
|||
} |
|||
|
|||
// Finally eliminate initial state.
|
|||
if (!stateRewards) { |
|||
// If we are computing probabilities, then we can simply call the state elimination procedure. It
|
|||
// will scale the transition row of the initial state with 1/(1-loopProbability).
|
|||
STORM_PRINT_AND_LOG("Eliminating initial state " << *initialStates.begin() << "." << std::endl); |
|||
eliminateState(flexibleMatrix, oneStepProbabilities, *initialStates.begin(), flexibleBackwardTransitions, stateRewards); |
|||
} else { |
|||
// If we are computing rewards, we cannot call the state elimination procedure for technical reasons.
|
|||
// Instead, we need to get rid of a potential loop in this state explicitly.
|
|||
|
|||
// Start by finding the self-loop element. Since it can only be the only remaining outgoing transition
|
|||
// of the initial state, this amounts to checking whether the outgoing transitions of the initial
|
|||
// state are non-empty.
|
|||
if (!flexibleMatrix.getRow(*initialStates.begin()).empty()) { |
|||
STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).size() == 1, "At most one outgoing transition expected at this point, but found more."); |
|||
STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).front().getColumn() == *initialStates.begin(), "Remaining entry should be a self-loop, but it is not."); |
|||
ValueType loopProbability = flexibleMatrix.getRow(*initialStates.begin()).front().getValue(); |
|||
loopProbability = storm::utility::one<ValueType>() / (storm::utility::one<ValueType>() - loopProbability); |
|||
loopProbability = storm::utility::pow(loopProbability, 2); |
|||
STORM_PRINT_AND_LOG("Scaling the transition reward of the initial state."); |
|||
stateRewards.get()[(*initialStates.begin())] *= loopProbability; |
|||
} |
|||
} |
|||
|
|||
// Make sure that we have eliminated all transitions from the initial state.
|
|||
STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).empty(), "The transitions of the initial states are non-empty."); |
|||
|
|||
std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now(); |
|||
std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); |
|||
|
|||
if (storm::settings::generalSettings().isShowStatisticsSet()) { |
|||
std::chrono::high_resolution_clock::duration conversionTime = conversionEnd - conversionStart; |
|||
std::chrono::milliseconds conversionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(conversionTime); |
|||
std::chrono::high_resolution_clock::duration modelCheckingTime = modelCheckingEnd - modelCheckingStart; |
|||
std::chrono::milliseconds modelCheckingTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(modelCheckingTime); |
|||
std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart; |
|||
std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(totalTime); |
|||
|
|||
STORM_PRINT_AND_LOG(std::endl); |
|||
STORM_PRINT_AND_LOG("Time breakdown:" << std::endl); |
|||
STORM_PRINT_AND_LOG(" * time for conversion: " << conversionTimeInMilliseconds.count() << "ms" << std::endl); |
|||
STORM_PRINT_AND_LOG(" * time for checking: " << modelCheckingTimeInMilliseconds.count() << "ms" << std::endl); |
|||
STORM_PRINT_AND_LOG("------------------------------------------" << std::endl); |
|||
STORM_PRINT_AND_LOG(" * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl); |
|||
STORM_PRINT_AND_LOG(std::endl); |
|||
STORM_PRINT_AND_LOG("Other:" << std::endl); |
|||
STORM_PRINT_AND_LOG(" * number of states eliminated: " << transitionMatrix.getRowCount() << std::endl); |
|||
if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) { |
|||
STORM_PRINT_AND_LOG(" * maximal depth of SCC decomposition: " << maximalDepth << std::endl); |
|||
} |
|||
} |
|||
|
|||
// Now, we return the value for the only initial state.
|
|||
if (stateRewards) { |
|||
return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]); |
|||
} else { |
|||
return storm::utility::simplify(oneStepProbabilities[*initialStates.begin()]); |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::vector<std::size_t> SparseDtmcEliminationModelChecker<ValueType>::getStatePriorities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities) { |
|||
std::vector<std::size_t> statePriorities(transitionMatrix.getRowCount()); |
|||
std::vector<std::size_t> states(transitionMatrix.getRowCount()); |
|||
for (std::size_t index = 0; index < states.size(); ++index) { |
|||
states[index] = index; |
|||
} |
|||
if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Random) { |
|||
std::random_shuffle(states.begin(), states.end()); |
|||
} else { |
|||
std::vector<std::size_t> distances; |
|||
if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed) { |
|||
distances = storm::utility::graph::getDistances(transitionMatrix, initialStates); |
|||
} else if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Backward || storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::BackwardReversed) { |
|||
// Since the target states were eliminated from the matrix already, we construct a replacement by
|
|||
// treating all states that have some non-zero probability to go to a target state in one step.
|
|||
storm::utility::ConstantsComparator<ValueType> comparator; |
|||
storm::storage::BitVector pseudoTargetStates(transitionMatrix.getRowCount()); |
|||
for (std::size_t index = 0; index < oneStepProbabilities.size(); ++index) { |
|||
if (!comparator.isZero(oneStepProbabilities[index])) { |
|||
pseudoTargetStates.set(index); |
|||
} |
|||
} |
|||
|
|||
distances = storm::utility::graph::getDistances(transitionMatrixTransposed, pseudoTargetStates); |
|||
} else { |
|||
STORM_LOG_ASSERT(false, "Illegal sorting order selected."); |
|||
} |
|||
|
|||
// In case of the forward or backward ordering, we can sort the states according to the distances.
|
|||
if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Backward) { |
|||
std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] < distances[state2]; } ); |
|||
} else { |
|||
// Otherwise, we sort them according to descending distances.
|
|||
std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] > distances[state2]; } ); |
|||
} |
|||
} |
|||
|
|||
// Now convert the ordering of the states to priorities.
|
|||
for (std::size_t index = 0; index < states.size(); ++index) { |
|||
statePriorities[states[index]] = index; |
|||
} |
|||
|
|||
return statePriorities; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
uint_fast64_t SparseDtmcEliminationModelChecker<ValueType>::treatScc(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<ValueType>>& stateRewards, boost::optional<std::vector<std::size_t>> const& statePriorities) { |
|||
uint_fast64_t maximalDepth = level; |
|||
|
|||
// If the SCCs are large enough, we try to split them further.
|
|||
if (scc.getNumberOfSetBits() > maximalSccSize) { |
|||
STORM_LOG_DEBUG("SCC is large enough (" << scc.getNumberOfSetBits() << " states) to be decomposed further."); |
|||
|
|||
// Here, we further decompose the SCC into sub-SCCs.
|
|||
storm::storage::StronglyConnectedComponentDecomposition<ValueType> decomposition(forwardTransitions, scc & ~entryStates, false, false); |
|||
STORM_LOG_DEBUG("Decomposed SCC into " << decomposition.size() << " sub-SCCs."); |
|||
|
|||
// Store a bit vector of remaining SCCs so we can be flexible when it comes to the order in which
|
|||
// we eliminate the SCCs.
|
|||
storm::storage::BitVector remainingSccs(decomposition.size(), true); |
|||
|
|||
// First, get rid of the trivial SCCs.
|
|||
std::vector<std::pair<storm::storage::sparse::state_type, uint_fast64_t>> trivialSccs; |
|||
for (uint_fast64_t sccIndex = 0; sccIndex < decomposition.size(); ++sccIndex) { |
|||
storm::storage::StronglyConnectedComponent const& scc = decomposition.getBlock(sccIndex); |
|||
if (scc.isTrivial()) { |
|||
storm::storage::sparse::state_type onlyState = *scc.begin(); |
|||
trivialSccs.emplace_back(onlyState, sccIndex); |
|||
} |
|||
} |
|||
|
|||
// If we are given priorities, sort the trivial SCCs accordingly.
|
|||
if (statePriorities) { |
|||
std::sort(trivialSccs.begin(), trivialSccs.end(), [&statePriorities] (std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& a, std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& b) { return statePriorities.get()[a.first] < statePriorities.get()[b.first]; }); |
|||
} |
|||
|
|||
STORM_LOG_DEBUG("Eliminating " << trivialSccs.size() << " trivial SCCs."); |
|||
for (auto const& stateIndexPair : trivialSccs) { |
|||
eliminateState(matrix, oneStepProbabilities, stateIndexPair.first, backwardTransitions, stateRewards); |
|||
remainingSccs.set(stateIndexPair.second, false); |
|||
} |
|||
STORM_LOG_DEBUG("Eliminated all trivial SCCs."); |
|||
|
|||
// And then recursively treat the remaining sub-SCCs.
|
|||
STORM_LOG_DEBUG("Eliminating " << remainingSccs.getNumberOfSetBits() << " remaining SCCs on level " << level << "."); |
|||
for (auto sccIndex : remainingSccs) { |
|||
storm::storage::StronglyConnectedComponent const& newScc = decomposition.getBlock(sccIndex); |
|||
|
|||
// Rewrite SCC into bit vector and subtract it from the remaining states.
|
|||
storm::storage::BitVector newSccAsBitVector(forwardTransitions.getRowCount(), newScc.begin(), newScc.end()); |
|||
|
|||
// Determine the set of entry states of the SCC.
|
|||
storm::storage::BitVector entryStates(forwardTransitions.getRowCount()); |
|||
for (auto const& state : newScc) { |
|||
for (auto const& predecessor : backwardTransitions.getRow(state)) { |
|||
if (predecessor.getValue() != storm::utility::zero<ValueType>() && !newSccAsBitVector.get(predecessor.getColumn())) { |
|||
entryStates.set(state); |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Recursively descend in SCC-hierarchy.
|
|||
uint_fast64_t depth = treatScc(matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::sparseDtmcEliminationModelCheckerSettings().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, comparator, stateRewards, statePriorities); |
|||
maximalDepth = std::max(maximalDepth, depth); |
|||
} |
|||
|
|||
} else { |
|||
// In this case, we perform simple state elimination in the current SCC.
|
|||
STORM_LOG_DEBUG("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly."); |
|||
storm::storage::BitVector remainingStates = scc & ~entryStates; |
|||
|
|||
std::vector<uint_fast64_t> states(remainingStates.begin(), remainingStates.end()); |
|||
|
|||
// If we are given priorities, sort the trivial SCCs accordingly.
|
|||
if (statePriorities) { |
|||
std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities.get()[a] < statePriorities.get()[b]; }); |
|||
} |
|||
|
|||
// Eliminate the remaining states that do not have a self-loop (in the current, i.e. modified)
|
|||
// transition probability matrix.
|
|||
for (auto const& state : states) { |
|||
eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards); |
|||
} |
|||
|
|||
STORM_LOG_DEBUG("Eliminated all states of SCC."); |
|||
} |
|||
|
|||
// Finally, eliminate the entry states (if we are required to do so).
|
|||
if (eliminateEntryStates) { |
|||
STORM_LOG_DEBUG("Finally, eliminating/adding entry states."); |
|||
for (auto state : entryStates) { |
|||
eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards); |
|||
} |
|||
STORM_LOG_DEBUG("Eliminated/added entry states."); |
|||
} else { |
|||
for (auto state : entryStates) { |
|||
entryStateQueue.push_back(state); |
|||
} |
|||
} |
|||
|
|||
return maximalDepth; |
|||
} |
|||
|
|||
namespace { |
|||
static int chunkCounter = 0; |
|||
static int counter = 0; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void SparseDtmcEliminationModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) { |
|||
auto eliminationStart = std::chrono::high_resolution_clock::now(); |
|||
|
|||
++counter; |
|||
STORM_LOG_DEBUG("Eliminating state " << state << "."); |
|||
if (counter > matrix.getNumberOfRows() / 10) { |
|||
++chunkCounter; |
|||
STORM_PRINT_AND_LOG("Eliminated " << (chunkCounter * 10) << "% of the states." << std::endl); |
|||
counter = 0; |
|||
} |
|||
|
|||
bool hasSelfLoop = false; |
|||
ValueType loopProbability = storm::utility:: <ValueType>(); |
|||
|
|||
// Start by finding loop probability.
|
|||
typename FlexibleSparseMatrix::row_type& currentStateSuccessors = matrix.getRow(state); |
|||
for (auto const& entry : currentStateSuccessors) { |
|||
if (entry.getColumn() >= state) { |
|||
if (entry.getColumn() == state) { |
|||
loopProbability = entry.getValue(); |
|||
hasSelfLoop = true; |
|||
} |
|||
break; |
|||
} |
|||
} |
|||
|
|||
// Scale all entries in this row with (1 / (1 - loopProbability)) only in case there was a self-loop.
|
|||
std::size_t scaledSuccessors = 0; |
|||
if (hasSelfLoop) { |
|||
loopProbability = storm::utility::one<ValueType>() / (storm::utility::one<ValueType>() - loopProbability); |
|||
storm::utility::simplify(loopProbability); |
|||
for (auto& entry : matrix.getRow(state)) { |
|||
// Only scale the non-diagonal entries.
|
|||
if (entry.getColumn() != state) { |
|||
++scaledSuccessors; |
|||
entry.setValue(storm::utility::simplify(entry.getValue() * loopProbability)); |
|||
} |
|||
} |
|||
if (!stateRewards) { |
|||
oneStepProbabilities[state] = oneStepProbabilities[state] * loopProbability; |
|||
} |
|||
} |
|||
|
|||
STORM_LOG_DEBUG((hasSelfLoop ? "State has self-loop." : "State does not have a self-loop.")); |
|||
|
|||
// Now connect the predecessors of the state being eliminated with its successors.
|
|||
typename FlexibleSparseMatrix::row_type& currentStatePredecessors = backwardTransitions.getRow(state); |
|||
std::size_t numberOfPredecessors = currentStatePredecessors.size(); |
|||
std::size_t predecessorForwardTransitionCount = 0; |
|||
for (auto const& predecessorEntry : currentStatePredecessors) { |
|||
uint_fast64_t predecessor = predecessorEntry.getColumn(); |
|||
|
|||
// Skip the state itself as one of its predecessors.
|
|||
if (predecessor == state) { |
|||
assert(hasSelfLoop); |
|||
continue; |
|||
} |
|||
|
|||
// Skip the state if the elimination is constrained, but the predecessor is not in the constraint.
|
|||
if (constrained && !predecessorConstraint.get(predecessor)) { |
|||
continue; |
|||
} |
|||
|
|||
// First, find the probability with which the predecessor can move to the current state, because
|
|||
// the other probabilities need to be scaled with this factor.
|
|||
typename FlexibleSparseMatrix::row_type& predecessorForwardTransitions = matrix.getRow(predecessor); |
|||
predecessorForwardTransitionCount += predecessorForwardTransitions.size(); |
|||
typename FlexibleSparseMatrix::row_type::iterator multiplyElement = std::find_if(predecessorForwardTransitions.begin(), predecessorForwardTransitions.end(), [&](storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() == state; }); |
|||
|
|||
// Make sure we have found the probability and set it to zero.
|
|||
STORM_LOG_THROW(multiplyElement != predecessorForwardTransitions.end(), storm::exceptions::InvalidStateException, "No probability for successor found."); |
|||
ValueType multiplyFactor = multiplyElement->getValue(); |
|||
multiplyElement->setValue(storm::utility::zero<ValueType>()); |
|||
|
|||
// At this point, we need to update the (forward) transitions of the predecessor.
|
|||
typename FlexibleSparseMatrix::row_type::iterator first1 = predecessorForwardTransitions.begin(); |
|||
typename FlexibleSparseMatrix::row_type::iterator last1 = predecessorForwardTransitions.end(); |
|||
typename FlexibleSparseMatrix::row_type::iterator first2 = currentStateSuccessors.begin(); |
|||
typename FlexibleSparseMatrix::row_type::iterator last2 = currentStateSuccessors.end(); |
|||
|
|||
typename FlexibleSparseMatrix::row_type newSuccessors; |
|||
newSuccessors.reserve((last1 - first1) + (last2 - first2)); |
|||
std::insert_iterator<typename FlexibleSparseMatrix::row_type> result(newSuccessors, newSuccessors.end()); |
|||
|
|||
// Now we merge the two successor lists. (Code taken from std::set_union and modified to suit our needs).
|
|||
for (; first1 != last1; ++result) { |
|||
// Skip the transitions to the state that is currently being eliminated.
|
|||
if (first1->getColumn() == state || (first2 != last2 && first2->getColumn() == state)) { |
|||
if (first1->getColumn() == state) { |
|||
++first1; |
|||
} |
|||
if (first2 != last2 && first2->getColumn() == state) { |
|||
++first2; |
|||
} |
|||
continue; |
|||
} |
|||
|
|||
if (first2 == last2) { |
|||
std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state; } ); |
|||
break; |
|||
} |
|||
if (first2->getColumn() < first1->getColumn()) { |
|||
*result = storm::utility::simplify(std::move(*first2 * multiplyFactor)); |
|||
++first2; |
|||
} else if (first1->getColumn() < first2->getColumn()) { |
|||
*result = *first1; |
|||
++first1; |
|||
} else { |
|||
*result = storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type>(first1->getColumn(), storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue()))); |
|||
++first1; |
|||
++first2; |
|||
} |
|||
} |
|||
for (; first2 != last2; ++first2) { |
|||
if (first2->getColumn() != state) { |
|||
*result = storm::utility::simplify(std::move(*first2 * multiplyFactor)); |
|||
} |
|||
} |
|||
|
|||
// Now move the new transitions in place.
|
|||
predecessorForwardTransitions = std::move(newSuccessors); |
|||
|
|||
if (!stateRewards) { |
|||
// Add the probabilities to go to a target state in just one step if we have to compute probabilities.
|
|||
oneStepProbabilities[predecessor] += storm::utility::simplify(multiplyFactor * oneStepProbabilities[state]); |
|||
STORM_LOG_DEBUG("Fixed new next-state probabilities of predecessor states."); |
|||
} else { |
|||
// If we are computing rewards, we basically scale the state reward of the state to eliminate and
|
|||
// add the result to the state reward of the predecessor.
|
|||
if (hasSelfLoop) { |
|||
stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * storm::utility::pow(loopProbability, 2) * stateRewards.get()[state]); |
|||
} else { |
|||
stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * stateRewards.get()[state]); |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Finally, we need to add the predecessor to the set of predecessors of every successor.
|
|||
for (auto const& successorEntry : currentStateSuccessors) { |
|||
typename FlexibleSparseMatrix::row_type& successorBackwardTransitions = backwardTransitions.getRow(successorEntry.getColumn()); |
|||
|
|||
// Delete the current state as a predecessor of the successor state.
|
|||
typename FlexibleSparseMatrix::row_type::iterator elimIt = std::find_if(successorBackwardTransitions.begin(), successorBackwardTransitions.end(), [&](storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() == state; }); |
|||
if (elimIt != successorBackwardTransitions.end()) { |
|||
successorBackwardTransitions.erase(elimIt); |
|||
} |
|||
|
|||
typename FlexibleSparseMatrix::row_type::iterator first1 = successorBackwardTransitions.begin(); |
|||
typename FlexibleSparseMatrix::row_type::iterator last1 = successorBackwardTransitions.end(); |
|||
typename FlexibleSparseMatrix::row_type::iterator first2 = currentStatePredecessors.begin(); |
|||
typename FlexibleSparseMatrix::row_type::iterator last2 = currentStatePredecessors.end(); |
|||
|
|||
typename FlexibleSparseMatrix::row_type newPredecessors; |
|||
newPredecessors.reserve((last1 - first1) + (last2 - first2)); |
|||
std::insert_iterator<typename FlexibleSparseMatrix::row_type> result(newPredecessors, newPredecessors.end()); |
|||
|
|||
|
|||
for (; first1 != last1; ++result) { |
|||
if (first2 == last2) { |
|||
std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state; }); |
|||
break; |
|||
} |
|||
if (first2->getColumn() < first1->getColumn()) { |
|||
if (first2->getColumn() != state) { |
|||
*result = *first2; |
|||
} |
|||
++first2; |
|||
} else { |
|||
if (first1->getColumn() != state) { |
|||
*result = *first1; |
|||
} |
|||
if (first1->getColumn() == first2->getColumn()) { |
|||
++first2; |
|||
} |
|||
++first1; |
|||
} |
|||
} |
|||
std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state; }); |
|||
|
|||
// Now move the new predecessors in place.
|
|||
successorBackwardTransitions = std::move(newPredecessors); |
|||
|
|||
} |
|||
STORM_LOG_DEBUG("Fixed predecessor lists of successor states."); |
|||
|
|||
if (removeForwardTransitions) { |
|||
// Clear the eliminated row to reduce memory consumption.
|
|||
currentStateSuccessors.clear(); |
|||
currentStateSuccessors.shrink_to_fit(); |
|||
} |
|||
if (!constrained) { |
|||
// FIXME: is this safe? If the elimination is constrained, we might have to repair the predecessor
|
|||
// relation.
|
|||
currentStatePredecessors.clear(); |
|||
currentStatePredecessors.shrink_to_fit(); |
|||
} |
|||
|
|||
auto eliminationEnd = std::chrono::high_resolution_clock::now(); |
|||
auto eliminationTime = eliminationEnd - eliminationStart; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::FlexibleSparseMatrix(index_type rows) : data(rows) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::reserveInRow(index_type row, index_type numberOfElements) { |
|||
this->data[row].reserve(numberOfElements); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
typename SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::row_type& SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::getRow(index_type index) { |
|||
return this->data[index]; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
typename SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::row_type const& SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::getRow(index_type index) const { |
|||
return this->data[index]; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
typename SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::index_type SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::getNumberOfRows() const { |
|||
return this->data.size(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::hasSelfLoop(storm::storage::sparse::state_type state) { |
|||
for (auto const& entry : this->getRow(state)) { |
|||
if (entry.getColumn() < state) { |
|||
continue; |
|||
} else if (entry.getColumn() > state) { |
|||
return false; |
|||
} else if (entry.getColumn() == state) { |
|||
return true; |
|||
} |
|||
} |
|||
return false; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::print() const { |
|||
for (uint_fast64_t index = 0; index < this->data.size(); ++index) { |
|||
std::cout << index << " - "; |
|||
for (auto const& element : this->getRow(index)) { |
|||
std::cout << "(" << element.getColumn() << ", " << element.getValue() << ") "; |
|||
} |
|||
std::cout << std::endl; |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
typename SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix SparseDtmcEliminationModelChecker<ValueType>::getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne) { |
|||
FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount()); |
|||
|
|||
for (typename FlexibleSparseMatrix::index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) { |
|||
typename storm::storage::SparseMatrix<ValueType>::const_rows row = matrix.getRow(rowIndex); |
|||
flexibleMatrix.reserveInRow(rowIndex, row.getNumberOfEntries()); |
|||
|
|||
for (auto const& element : row) { |
|||
if (setAllValuesToOne) { |
|||
flexibleMatrix.getRow(rowIndex).emplace_back(element.getColumn(), storm::utility::one<ValueType>()); |
|||
} else { |
|||
flexibleMatrix.getRow(rowIndex).emplace_back(element); |
|||
} |
|||
} |
|||
} |
|||
|
|||
return flexibleMatrix; |
|||
} |
|||
|
|||
template class SparseDtmcEliminationModelChecker<double>; |
|||
|
|||
#ifdef PARAMETRIC_SYSTEMS
|
|||
template class FlexibleSparseMatrix<RationalFunction>; |
|||
template class SparseDtmcEliminationModelChecker<RationalFunction>; |
|||
#endif
|
|||
} // namespace modelchecker
|
|||
} // namespace storm
|
|||
@ -0,0 +1,75 @@ |
|||
#ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCELIMINATIONMODELCHECKER_H_ |
|||
#define STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCELIMINATIONMODELCHECKER_H_ |
|||
|
|||
#include "src/storage/sparse/StateType.h" |
|||
#include "src/models/Dtmc.h" |
|||
#include "src/modelchecker/AbstractModelChecker.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
|
|||
template<typename ValueType> |
|||
class SparseDtmcEliminationModelChecker : public AbstractModelChecker { |
|||
public: |
|||
explicit SparseDtmcEliminationModelChecker(storm::models::Dtmc<ValueType> const& model); |
|||
|
|||
// The implemented methods of the AbstractModelChecker interface. |
|||
virtual bool canHandle(storm::logic::Formula const& formula) const override; |
|||
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override; |
|||
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override; |
|||
virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override; |
|||
virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override; |
|||
virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override; |
|||
|
|||
private: |
|||
class FlexibleSparseMatrix { |
|||
public: |
|||
typedef uint_fast64_t index_type; |
|||
typedef ValueType value_type; |
|||
typedef std::vector<storm::storage::MatrixEntry<index_type, value_type>> row_type; |
|||
typedef typename row_type::iterator iterator; |
|||
typedef typename row_type::const_iterator const_iterator; |
|||
|
|||
FlexibleSparseMatrix() = default; |
|||
FlexibleSparseMatrix(index_type rows); |
|||
|
|||
void reserveInRow(index_type row, index_type numberOfElements); |
|||
|
|||
row_type& getRow(index_type); |
|||
row_type const& getRow(index_type) const; |
|||
|
|||
index_type getNumberOfRows() const; |
|||
|
|||
void print() const; |
|||
|
|||
/*! |
|||
* Checks whether the given state has a self-loop with an arbitrary probability in the given probability matrix. |
|||
* |
|||
* @param state The state for which to check whether it possesses a self-loop. |
|||
* @param matrix The matrix in which to look for the loop. |
|||
* @return True iff the given state has a self-loop with an arbitrary probability in the given probability matrix. |
|||
*/ |
|||
bool hasSelfLoop(storm::storage::sparse::state_type state); |
|||
|
|||
private: |
|||
std::vector<row_type> data; |
|||
}; |
|||
|
|||
static ValueType computeReachabilityValue(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<ValueType>>& stateRewards, boost::optional<std::vector<std::size_t>> const& statePriorities = {}); |
|||
|
|||
static uint_fast64_t treatScc(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<ValueType>>& stateRewards, boost::optional<std::vector<std::size_t>> const& statePriorities = {}); |
|||
|
|||
static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne = false); |
|||
|
|||
static void eliminateState(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards, bool removeForwardTransitions = true, bool constrained = false, storm::storage::BitVector const& predecessorConstraint = storm::storage::BitVector()); |
|||
|
|||
static std::vector<std::size_t> getStatePriorities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities); |
|||
|
|||
// The model this model checker is supposed to analyze. |
|||
storm::models::Dtmc<ValueType> const& model; |
|||
}; |
|||
|
|||
} // namespace modelchecker |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCELIMINATIONMODELCHECKER_H_ */ |
|||
@ -1,435 +0,0 @@ |
|||
#include "src/modelchecker/reachability/SparseSccModelChecker.h"
|
|||
|
|||
#include <algorithm>
|
|||
|
|||
#include "src/storage/StronglyConnectedComponentDecomposition.h"
|
|||
#include "src/utility/graph.h"
|
|||
#include "src/utility/vector.h"
|
|||
#include "src/exceptions/InvalidStateException.h"
|
|||
#include "src/utility/macros.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace reachability { |
|||
|
|||
template<typename ValueType> |
|||
static ValueType&& simplify(ValueType&& value) { |
|||
// In the general case, we don't to anything here, but merely return the value. If something else is
|
|||
// supposed to happen here, the templated function can be specialized for this particular type.
|
|||
return std::forward<ValueType>(value); |
|||
} |
|||
|
|||
template<typename IndexType, typename ValueType> |
|||
static storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry) { |
|||
simplify(matrixEntry.getValue()); |
|||
return std::move(matrixEntry); |
|||
} |
|||
|
|||
template<typename IndexType, typename ValueType> |
|||
static storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) { |
|||
matrixEntry.setValue(simplify(matrixEntry.getValue())); |
|||
return matrixEntry; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
ValueType SparseSccModelChecker<ValueType>::computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|||
// First, do some sanity checks to establish some required properties.
|
|||
STORM_LOG_THROW(dtmc.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); |
|||
typename FlexibleSparseMatrix<ValueType>::index_type initialStateIndex = *dtmc.getInitialStates().begin(); |
|||
|
|||
// Then, compute the subset of states that has a probability of 0 or 1, respectively.
|
|||
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(dtmc, phiStates, psiStates); |
|||
storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; |
|||
storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; |
|||
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); |
|||
|
|||
// If the initial state is known to have either probability 0 or 1, we can directly return the result.
|
|||
if (!maybeStates.get(initialStateIndex)) { |
|||
return statesWithProbability0.get(initialStateIndex) ? 0 : 1; |
|||
} |
|||
|
|||
// 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(dtmc.getTransitionMatrix(), dtmc.getInitialStates(), maybeStates, statesWithProbability1); |
|||
|
|||
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
|
|||
maybeStates &= reachableStates; |
|||
|
|||
// Create a vector for the probabilities to go to a state with probability 1 in one step.
|
|||
std::vector<ValueType> oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); |
|||
|
|||
// Determine the set of initial states of the sub-DTMC.
|
|||
storm::storage::BitVector newInitialStates = dtmc.getInitialStates() % maybeStates; |
|||
|
|||
// We then build the submatrix that only has the transitions of the maybe states.
|
|||
storm::storage::SparseMatrix<ValueType> submatrix = dtmc.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); |
|||
|
|||
// Create a bit vector that represents the subsystem of states we still have to eliminate.
|
|||
storm::storage::BitVector subsystem = storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true); |
|||
|
|||
// Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
|
|||
FlexibleSparseMatrix<ValueType> flexibleMatrix = getFlexibleSparseMatrix(submatrix); |
|||
FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrix.transpose(), true); |
|||
|
|||
// Then, we recursively treat all SCCs.
|
|||
treatScc(dtmc, flexibleMatrix, oneStepProbabilities, newInitialStates, subsystem, submatrix, flexibleBackwardTransitions, false, 0); |
|||
|
|||
// Now, we return the value for the only initial state.
|
|||
return oneStepProbabilities[initialStateIndex]; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void SparseSccModelChecker<ValueType>::treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level) { |
|||
// If the SCCs are large enough, we try to split them further.
|
|||
if (scc.getNumberOfSetBits() > SparseSccModelChecker<ValueType>::maximalSccSize) { |
|||
// Here, we further decompose the SCC into sub-SCCs.
|
|||
storm::storage::StronglyConnectedComponentDecomposition<ValueType> decomposition(forwardTransitions, scc & ~entryStates, false, false); |
|||
|
|||
// To eliminate the remaining one-state SCCs, we need to keep track of them.
|
|||
// storm::storage::BitVector remainingStates(scc);
|
|||
|
|||
// Store a bit vector of remaining SCCs so we can be flexible when it comes to the order in which
|
|||
// we eliminate the SCCs.
|
|||
storm::storage::BitVector remainingSccs(decomposition.size(), true); |
|||
|
|||
// First, get rid of the trivial SCCs.
|
|||
for (uint_fast64_t sccIndex = 0; sccIndex < decomposition.size(); ++sccIndex) { |
|||
storm::storage::StronglyConnectedComponent const& scc = decomposition.getBlock(sccIndex); |
|||
if (scc.isTrivial()) { |
|||
storm::storage::sparse::state_type onlyState = *scc.begin(); |
|||
eliminateState(matrix, oneStepProbabilities, onlyState, backwardTransitions); |
|||
remainingSccs.set(sccIndex, false); |
|||
} |
|||
} |
|||
|
|||
// And then recursively treat the remaining sub-SCCs.
|
|||
for (auto sccIndex : remainingSccs) { |
|||
storm::storage::StronglyConnectedComponent const& newScc = decomposition.getBlock(sccIndex); |
|||
// If the SCC consists of just one state, we do not explore it recursively, but rather eliminate
|
|||
// it directly.
|
|||
if (newScc.size() == 1) { |
|||
continue; |
|||
} |
|||
|
|||
// Rewrite SCC into bit vector and subtract it from the remaining states.
|
|||
storm::storage::BitVector newSccAsBitVector(forwardTransitions.getRowCount(), newScc.begin(), newScc.end()); |
|||
// remainingStates &= ~newSccAsBitVector;
|
|||
|
|||
// Determine the set of entry states of the SCC.
|
|||
storm::storage::BitVector entryStates(dtmc.getNumberOfStates()); |
|||
for (auto const& state : newScc) { |
|||
for (auto const& predecessor : backwardTransitions.getRow(state)) { |
|||
if (predecessor.getValue() > storm::utility::constantZero<ValueType>() && !newSccAsBitVector.get(predecessor.getColumn())) { |
|||
entryStates.set(state); |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Recursively descend in SCC-hierarchy.
|
|||
treatScc(dtmc, matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, true, level + 1); |
|||
} |
|||
|
|||
// If we are not supposed to eliminate the entry states, we need to take them out of the set of
|
|||
// remaining states.
|
|||
// if (!eliminateEntryStates) {
|
|||
// remainingStates &= ~entryStates;
|
|||
// }
|
|||
//
|
|||
// Now that we eliminated all non-trivial sub-SCCs, we need to take care of trivial sub-SCCs.
|
|||
// Therefore, we need to eliminate all states.
|
|||
// for (auto const& state : remainingStates) {
|
|||
// eliminateState(matrix, oneStepProbabilities, state, backwardTransitions);
|
|||
// }
|
|||
} else { |
|||
// In this case, we perform simple state elimination in the current SCC.
|
|||
storm::storage::BitVector remainingStates = scc; |
|||
|
|||
// if (eliminateEntryStates) {
|
|||
remainingStates &= ~entryStates; |
|||
// }
|
|||
|
|||
// Eliminate the remaining states.
|
|||
for (auto const& state : remainingStates) { |
|||
eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); |
|||
} |
|||
|
|||
// Finally, eliminate the entry states (if we are allowed to do so).
|
|||
if (eliminateEntryStates) { |
|||
for (auto state : entryStates) { |
|||
eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void SparseSccModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions) { |
|||
bool hasSelfLoop = false; |
|||
ValueType loopProbability = storm::utility::constantZero<ValueType>(); |
|||
|
|||
// Start by finding loop probability.
|
|||
typename FlexibleSparseMatrix<ValueType>::row_type& currentStateSuccessors = matrix.getRow(state); |
|||
for (auto const& entry : currentStateSuccessors) { |
|||
if (entry.getColumn() >= state) { |
|||
if (entry.getColumn() == state) { |
|||
loopProbability = entry.getValue(); |
|||
hasSelfLoop = true; |
|||
} |
|||
break; |
|||
} |
|||
} |
|||
|
|||
// Scale all entries in this row with (1 / (1 - loopProbability)) only in case there was a self-loop.
|
|||
if (hasSelfLoop) { |
|||
loopProbability = 1 / (1 - loopProbability); |
|||
simplify(loopProbability); |
|||
for (auto& entry : matrix.getRow(state)) { |
|||
entry.setValue(simplify(entry.getValue() * loopProbability)); |
|||
} |
|||
oneStepProbabilities[state] = simplify(oneStepProbabilities[state] * loopProbability); |
|||
} |
|||
|
|||
// Now connect the predecessors of the state being eliminated with its successors.
|
|||
typename FlexibleSparseMatrix<ValueType>::row_type& currentStatePredecessors = backwardTransitions.getRow(state); |
|||
for (auto const& predecessorEntry : currentStatePredecessors) { |
|||
uint_fast64_t predecessor = predecessorEntry.getColumn(); |
|||
|
|||
// Skip the state itself as one of its predecessors.
|
|||
if (predecessor == state) { |
|||
continue; |
|||
} |
|||
|
|||
// First, find the probability with which the predecessor can move to the current state, because
|
|||
// the other probabilities need to be scaled with this factor.
|
|||
typename FlexibleSparseMatrix<ValueType>::row_type& predecessorForwardTransitions = matrix.getRow(predecessor); |
|||
typename FlexibleSparseMatrix<ValueType>::row_type::iterator multiplyElement = std::find_if(predecessorForwardTransitions.begin(), predecessorForwardTransitions.end(), [&](storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; }); |
|||
|
|||
// Make sure we have found the probability and set it to zero.
|
|||
STORM_LOG_THROW(multiplyElement != predecessorForwardTransitions.end(), storm::exceptions::InvalidStateException, "No probability for successor found."); |
|||
ValueType multiplyFactor = multiplyElement->getValue(); |
|||
multiplyElement->setValue(0); |
|||
|
|||
// At this point, we need to update the (forward) transitions of the predecessor.
|
|||
typename FlexibleSparseMatrix<ValueType>::row_type::iterator first1 = predecessorForwardTransitions.begin(); |
|||
typename FlexibleSparseMatrix<ValueType>::row_type::iterator last1 = predecessorForwardTransitions.end(); |
|||
typename FlexibleSparseMatrix<ValueType>::row_type::iterator first2 = currentStateSuccessors.begin(); |
|||
typename FlexibleSparseMatrix<ValueType>::row_type::iterator last2 = currentStateSuccessors.end(); |
|||
|
|||
typename FlexibleSparseMatrix<ValueType>::row_type newSuccessors; |
|||
newSuccessors.reserve((last1 - first1) + (last2 - first2)); |
|||
std::insert_iterator<typename FlexibleSparseMatrix<ValueType>::row_type> result(newSuccessors, newSuccessors.end()); |
|||
|
|||
// Now we merge the two successor lists. (Code taken from std::set_union and modified to suit our needs).
|
|||
for (; first1 != last1; ++result) { |
|||
// Skip the transitions to the state that is currently being eliminated.
|
|||
if (first1->getColumn() == state || (first2 != last2 && first2->getColumn() == state)) { |
|||
if (first1->getColumn() == state) { |
|||
++first1; |
|||
} |
|||
if (first2 != last2 && first2->getColumn() == state) { |
|||
++first2; |
|||
} |
|||
continue; |
|||
} |
|||
|
|||
if (first2 == last2) { |
|||
std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != state; } ); |
|||
break; |
|||
} |
|||
if (first2->getColumn() < first1->getColumn()) { |
|||
*result = simplify(*first2 * multiplyFactor); |
|||
++first2; |
|||
} else if (first1->getColumn() < first2->getColumn()) { |
|||
*result = *first1; |
|||
++first1; |
|||
} else { |
|||
*result = storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type>(first1->getColumn(), simplify(first1->getValue() + simplify(multiplyFactor * first2->getValue()))); |
|||
++first1; |
|||
++first2; |
|||
} |
|||
} |
|||
for (; first2 != last2; ++first2) { |
|||
if (first2->getColumn() != state) { |
|||
*result = simplify(*first2 * multiplyFactor); |
|||
} |
|||
} |
|||
|
|||
// Now move the new transitions in place.
|
|||
predecessorForwardTransitions = std::move(newSuccessors); |
|||
|
|||
// Add the probabilities to go to a target state in just one step.
|
|||
oneStepProbabilities[predecessor] = simplify(oneStepProbabilities[predecessor] + simplify(multiplyFactor * oneStepProbabilities[state])); |
|||
} |
|||
|
|||
// Finally, we need to add the predecessor to the set of predecessors of every successor.
|
|||
for (auto const& successorEntry : currentStateSuccessors) { |
|||
typename FlexibleSparseMatrix<ValueType>::row_type& successorBackwardTransitions = backwardTransitions.getRow(successorEntry.getColumn()); |
|||
|
|||
// Delete the current state as a predecessor of the successor state.
|
|||
typename FlexibleSparseMatrix<ValueType>::row_type::iterator elimIt = std::find_if(successorBackwardTransitions.begin(), successorBackwardTransitions.end(), [&](storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; }); |
|||
if (elimIt != successorBackwardTransitions.end()) { |
|||
successorBackwardTransitions.erase(elimIt); |
|||
} |
|||
|
|||
typename FlexibleSparseMatrix<ValueType>::row_type::iterator first1 = successorBackwardTransitions.begin(); |
|||
typename FlexibleSparseMatrix<ValueType>::row_type::iterator last1 = successorBackwardTransitions.end(); |
|||
typename FlexibleSparseMatrix<ValueType>::row_type::iterator first2 = currentStatePredecessors.begin(); |
|||
typename FlexibleSparseMatrix<ValueType>::row_type::iterator last2 = currentStatePredecessors.end(); |
|||
|
|||
typename FlexibleSparseMatrix<ValueType>::row_type newPredecessors; |
|||
newPredecessors.reserve((last1 - first1) + (last2 - first2)); |
|||
std::insert_iterator<typename FlexibleSparseMatrix<ValueType>::row_type> result(newPredecessors, newPredecessors.end()); |
|||
|
|||
|
|||
for (; first1 != last1; ++result) { |
|||
if (first2 == last2) { |
|||
std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != state; }); |
|||
break; |
|||
} |
|||
if (first2->getColumn() < first1->getColumn()) { |
|||
if (first2->getColumn() != state) { |
|||
*result = *first2; |
|||
} |
|||
++first2; |
|||
} else { |
|||
if (first1->getColumn() != state) { |
|||
*result = *first1; |
|||
} |
|||
if (first1->getColumn() == first2->getColumn()) { |
|||
++first2; |
|||
} |
|||
++first1; |
|||
} |
|||
} |
|||
std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != state; }); |
|||
|
|||
// Now move the new predecessors in place.
|
|||
successorBackwardTransitions = std::move(newPredecessors); |
|||
} |
|||
|
|||
|
|||
// Clear the eliminated row to reduce memory consumption.
|
|||
currentStateSuccessors.clear(); |
|||
currentStateSuccessors.shrink_to_fit(); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
bool SparseSccModelChecker<ValueType>::eliminateStateInPlace(storm::storage::SparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix<ValueType>& backwardTransitions) { |
|||
typename storm::storage::SparseMatrix<ValueType>::iterator forwardElement = matrix.getRow(state).begin(); |
|||
typename storm::storage::SparseMatrix<ValueType>::iterator backwardElement = backwardTransitions.getRow(state).begin(); |
|||
|
|||
if (forwardElement->getValue() != storm::utility::constantOne<ValueType>() || backwardElement->getValue() != storm::utility::constantOne<ValueType>()) { |
|||
return false; |
|||
} |
|||
|
|||
std::cout << "eliminating " << state << std::endl; |
|||
std::cout << "fwd element: " << *forwardElement << " and bwd element: " << *backwardElement << std::endl; |
|||
|
|||
// Find the element of the predecessor that moves to the state that we want to eliminate.
|
|||
typename storm::storage::SparseMatrix<ValueType>::rows forwardRow = matrix.getRow(backwardElement->getColumn()); |
|||
typename storm::storage::SparseMatrix<ValueType>::iterator multiplyElement = std::find_if(forwardRow.begin(), forwardRow.end(), [&](storm::storage::MatrixEntry<typename storm::storage::SparseMatrix<ValueType>::index_type, typename storm::storage::SparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; }); |
|||
|
|||
std::cout << "before fwd: " << std::endl; |
|||
for (auto element : matrix.getRow(backwardElement->getColumn())) { |
|||
std::cout << element << ", " << std::endl; |
|||
} |
|||
|
|||
// Modify the forward probability entry of the predecessor.
|
|||
multiplyElement->setValue(multiplyElement->getValue() * forwardElement->getValue()); |
|||
multiplyElement->setColumn(forwardElement->getColumn()); |
|||
|
|||
// Modify the one-step probability for the predecessor if necessary.
|
|||
if (oneStepProbabilities[state] != storm::utility::constantZero<ValueType>()) { |
|||
oneStepProbabilities[backwardElement->getColumn()] += multiplyElement->getValue() * oneStepProbabilities[state]; |
|||
} |
|||
|
|||
// If the forward entry is not at the right position, we need to move it there.
|
|||
if (multiplyElement != forwardRow.begin() && multiplyElement->getColumn() < (multiplyElement - 1)->getColumn()) { |
|||
while (multiplyElement != forwardRow.begin() && multiplyElement->getColumn() < (multiplyElement - 1)->getColumn()) { |
|||
std::swap(*multiplyElement, *(multiplyElement - 1)); |
|||
--multiplyElement; |
|||
} |
|||
} else if ((multiplyElement + 1) != forwardRow.end() && multiplyElement->getColumn() > (multiplyElement + 1)->getColumn()) { |
|||
while ((multiplyElement + 1) != forwardRow.end() && multiplyElement->getColumn() > (multiplyElement + 1)->getColumn()) { |
|||
std::swap(*multiplyElement, *(multiplyElement + 1)); |
|||
++multiplyElement; |
|||
} |
|||
} |
|||
|
|||
std::cout << "after fwd: " << std::endl; |
|||
for (auto element : matrix.getRow(backwardElement->getColumn())) { |
|||
std::cout << element << ", " << std::endl; |
|||
} |
|||
|
|||
// Find the backward element of the successor that moves to the state that we want to eliminate.
|
|||
typename storm::storage::SparseMatrix<ValueType>::rows backwardRow = backwardTransitions.getRow(forwardElement->getColumn()); |
|||
typename storm::storage::SparseMatrix<ValueType>::iterator backwardEntry = std::find_if(backwardRow.begin(), backwardRow.end(), [&](storm::storage::MatrixEntry<typename storm::storage::SparseMatrix<ValueType>::index_type, typename storm::storage::SparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; }); |
|||
|
|||
std::cout << "before bwd" << std::endl; |
|||
for (auto element : backwardTransitions.getRow(forwardElement->getColumn())) { |
|||
std::cout << element << ", " << std::endl; |
|||
} |
|||
|
|||
// Modify the predecessor list of the successor and add the predecessor of the state we eliminate.
|
|||
backwardEntry->setColumn(backwardElement->getColumn()); |
|||
|
|||
// If the backward entry is not at the right position, we need to move it there.
|
|||
if (backwardEntry != backwardRow.begin() && backwardEntry->getColumn() < (backwardEntry - 1)->getColumn()) { |
|||
while (backwardEntry != backwardRow.begin() && backwardEntry->getColumn() < (backwardEntry - 1)->getColumn()) { |
|||
std::swap(*backwardEntry, *(backwardEntry - 1)); |
|||
--backwardEntry; |
|||
} |
|||
} else if ((backwardEntry + 1) != backwardRow.end() && backwardEntry->getColumn() > (backwardEntry + 1)->getColumn()) { |
|||
while ((backwardEntry + 1) != backwardRow.end() && backwardEntry->getColumn() > (backwardEntry + 1)->getColumn()) { |
|||
std::swap(*backwardEntry, *(backwardEntry + 1)); |
|||
++backwardEntry; |
|||
} |
|||
} |
|||
|
|||
std::cout << "after bwd" << std::endl; |
|||
for (auto element : backwardTransitions.getRow(forwardElement->getColumn())) { |
|||
std::cout << element << ", " << std::endl; |
|||
} |
|||
return true; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
FlexibleSparseMatrix<ValueType>::FlexibleSparseMatrix(index_type rows) : data(rows) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void FlexibleSparseMatrix<ValueType>::reserveInRow(index_type row, index_type numberOfElements) { |
|||
this->data[row].reserve(numberOfElements); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
typename FlexibleSparseMatrix<ValueType>::row_type& FlexibleSparseMatrix<ValueType>::getRow(index_type index) { |
|||
return this->data[index]; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
FlexibleSparseMatrix<ValueType> SparseSccModelChecker<ValueType>::getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne) { |
|||
FlexibleSparseMatrix<ValueType> flexibleMatrix(matrix.getRowCount()); |
|||
|
|||
for (typename FlexibleSparseMatrix<ValueType>::index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) { |
|||
typename storm::storage::SparseMatrix<ValueType>::const_rows row = matrix.getRow(rowIndex); |
|||
flexibleMatrix.reserveInRow(rowIndex, row.getNumberOfEntries()); |
|||
|
|||
for (auto const& element : row) { |
|||
if (setAllValuesToOne) { |
|||
flexibleMatrix.getRow(rowIndex).emplace_back(element.getColumn(), storm::utility::constantOne<ValueType>()); |
|||
} else { |
|||
flexibleMatrix.getRow(rowIndex).emplace_back(element); |
|||
} |
|||
} |
|||
} |
|||
|
|||
return flexibleMatrix; |
|||
} |
|||
|
|||
template class FlexibleSparseMatrix<double>; |
|||
template class SparseSccModelChecker<double>; |
|||
|
|||
} // namespace reachability
|
|||
} // namespace modelchecker
|
|||
} // namespace storm
|
|||
@ -1,43 +0,0 @@ |
|||
#include "src/models/Dtmc.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace reachability { |
|||
|
|||
template<typename ValueType> |
|||
class FlexibleSparseMatrix { |
|||
public: |
|||
typedef uint_fast64_t index_type; |
|||
typedef ValueType value_type; |
|||
typedef std::vector<storm::storage::MatrixEntry<index_type, value_type>> row_type; |
|||
typedef typename row_type::iterator iterator; |
|||
typedef typename row_type::const_iterator const_iterator; |
|||
|
|||
FlexibleSparseMatrix() = default; |
|||
FlexibleSparseMatrix(index_type rows); |
|||
|
|||
void reserveInRow(index_type row, index_type numberOfElements); |
|||
|
|||
row_type& getRow(index_type); |
|||
|
|||
private: |
|||
std::vector<row_type> data; |
|||
}; |
|||
|
|||
template<typename ValueType> |
|||
class SparseSccModelChecker { |
|||
public: |
|||
static ValueType computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); |
|||
|
|||
private: |
|||
static void treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level); |
|||
static FlexibleSparseMatrix<ValueType> getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne = false); |
|||
static void eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions); |
|||
static bool eliminateStateInPlace(storm::storage::SparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix<ValueType>& backwardTransitions); |
|||
|
|||
static const uint_fast64_t maximalSccSize = 1000; |
|||
|
|||
}; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,64 @@ |
|||
#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
|
|||
|
|||
#include "src/settings/SettingsManager.h"
|
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
|
|||
const std::string SparseDtmcEliminationModelCheckerSettings::moduleName = "sparseelim"; |
|||
const std::string SparseDtmcEliminationModelCheckerSettings::eliminationMethodOptionName = "method"; |
|||
const std::string SparseDtmcEliminationModelCheckerSettings::eliminationOrderOptionName = "order"; |
|||
const std::string SparseDtmcEliminationModelCheckerSettings::entryStatesLastOptionName = "entrylast"; |
|||
const std::string SparseDtmcEliminationModelCheckerSettings::maximalSccSizeOptionName = "sccsize"; |
|||
|
|||
SparseDtmcEliminationModelCheckerSettings::SparseDtmcEliminationModelCheckerSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { |
|||
std::vector<std::string> orders = {"fw", "fwrev", "bw", "bwrev", "rand"}; |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(orders)).setDefaultValueString("bw").build()).build()); |
|||
|
|||
std::vector<std::string> methods = {"state", "hybrid"}; |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, eliminationMethodOptionName, true, "The elimination technique to use. Available are {state, hybrid}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the elimination technique to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("hybrid").build()).build()); |
|||
|
|||
this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.") |
|||
.addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxsize", "The maximal size of an SCC on which state elimination is applied.").setDefaultValueUnsignedInteger(20).setIsOptional(true).build()).build()); |
|||
} |
|||
|
|||
SparseDtmcEliminationModelCheckerSettings::EliminationMethod SparseDtmcEliminationModelCheckerSettings::getEliminationMethod() const { |
|||
std::string eliminationMethodAsString = this->getOption(eliminationMethodOptionName).getArgumentByName("name").getValueAsString(); |
|||
if (eliminationMethodAsString == "state") { |
|||
return EliminationMethod::State; |
|||
} else if (eliminationMethodAsString == "hybrid") { |
|||
return EliminationMethod::Hybrid; |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal elimination method selected."); |
|||
} |
|||
} |
|||
|
|||
SparseDtmcEliminationModelCheckerSettings::EliminationOrder SparseDtmcEliminationModelCheckerSettings::getEliminationOrder() const { |
|||
std::string eliminationOrderAsString = this->getOption(eliminationOrderOptionName).getArgumentByName("name").getValueAsString(); |
|||
if (eliminationOrderAsString == "fw") { |
|||
return EliminationOrder::Forward; |
|||
} else if (eliminationOrderAsString == "fwrev") { |
|||
return EliminationOrder::ForwardReversed; |
|||
} else if (eliminationOrderAsString == "bw") { |
|||
return EliminationOrder::Backward; |
|||
} else if (eliminationOrderAsString == "bwrev") { |
|||
return EliminationOrder::BackwardReversed; |
|||
} else if (eliminationOrderAsString == "rand") { |
|||
return EliminationOrder::Random; |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal elimination order selected."); |
|||
} |
|||
} |
|||
|
|||
bool SparseDtmcEliminationModelCheckerSettings::isEliminateEntryStatesLastSet() const { |
|||
return this->getOption(entryStatesLastOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
uint_fast64_t SparseDtmcEliminationModelCheckerSettings::getMaximalSccSize() const { |
|||
return this->getOption(maximalSccSizeOptionName).getArgumentByName("maxsize").getValueAsUnsignedInteger(); |
|||
} |
|||
} // namespace modules
|
|||
} // namespace settings
|
|||
} // namespace storm
|
|||
@ -0,0 +1,73 @@ |
|||
#ifndef STORM_SETTINGS_MODULES_SPARSEDTMCELIMINATIONMODELCHECKERSETTINGS_H_ |
|||
#define STORM_SETTINGS_MODULES_SPARSEDTMCELIMINATIONMODELCHECKERSETTINGS_H_ |
|||
|
|||
#include "src/settings/modules/ModuleSettings.h" |
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
|
|||
/*! |
|||
* This class represents the settings for the elimination-based DTMC model checker. |
|||
*/ |
|||
class SparseDtmcEliminationModelCheckerSettings : public ModuleSettings { |
|||
public: |
|||
/*! |
|||
* An enum that contains all available state elimination orders. |
|||
*/ |
|||
enum class EliminationOrder { Forward, ForwardReversed, Backward, BackwardReversed, Random }; |
|||
|
|||
/*! |
|||
* An enum that contains all available techniques to solve parametric systems. |
|||
*/ |
|||
enum class EliminationMethod { State, Scc, Hybrid}; |
|||
|
|||
/*! |
|||
* Creates a new set of parametric model checking settings that is managed by the given manager. |
|||
* |
|||
* @param settingsManager The responsible manager. |
|||
*/ |
|||
SparseDtmcEliminationModelCheckerSettings(storm::settings::SettingsManager& settingsManager); |
|||
|
|||
/*! |
|||
* Retrieves the selected elimination method. |
|||
* |
|||
* @return The selected elimination method. |
|||
*/ |
|||
EliminationMethod getEliminationMethod() const; |
|||
|
|||
/*! |
|||
* Retrieves the selected elimination order. |
|||
* |
|||
* @return The selected elimination order. |
|||
*/ |
|||
EliminationOrder getEliminationOrder() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the option to eliminate entry states in the very end is set. |
|||
* |
|||
* @return True iff the option is set. |
|||
*/ |
|||
bool isEliminateEntryStatesLastSet() const; |
|||
|
|||
/*! |
|||
* Retrieves the maximal size of an SCC on which state elimination is to be directly applied. |
|||
* |
|||
* @return The maximal size of an SCC on which state elimination is to be directly applied. |
|||
*/ |
|||
uint_fast64_t getMaximalSccSize() const; |
|||
|
|||
const static std::string moduleName; |
|||
|
|||
private: |
|||
const static std::string eliminationMethodOptionName; |
|||
const static std::string eliminationOrderOptionName; |
|||
const static std::string entryStatesLastOptionName; |
|||
const static std::string maximalSccSizeOptionName; |
|||
}; |
|||
|
|||
} // namespace modules |
|||
} // namespace settings |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_SETTINGS_MODULES_SPARSEDTMCELIMINATIONMODELCHECKERSETTINGS_H_ */ |
|||
Reference in new issue
xxxxxxxxxx