dehnert
12 years ago
76 changed files with 1183 additions and 1921 deletions
-
6CMakeLists.txt
-
2src/logic/BinaryBooleanStateFormula.cpp
-
2src/logic/BinaryBooleanStateFormula.h
-
12src/logic/BinaryPathFormula.cpp
-
9src/logic/BinaryPathFormula.h
-
11src/logic/BinaryStateFormula.cpp
-
9src/logic/BinaryStateFormula.h
-
8src/logic/BooleanLiteralFormula.cpp
-
5src/logic/BooleanLiteralFormula.h
-
4src/logic/BoundedUntilFormula.cpp
-
4src/logic/BoundedUntilFormula.h
-
2src/logic/ConditionalPathFormula.cpp
-
2src/logic/ConditionalPathFormula.h
-
4src/logic/CumulativeRewardFormula.cpp
-
6src/logic/CumulativeRewardFormula.h
-
2src/logic/EventuallyFormula.cpp
-
2src/logic/EventuallyFormula.h
-
34src/logic/Formula.cpp
-
27src/logic/Formula.h
-
1src/logic/Formulas.h
-
2src/logic/GloballyFormula.cpp
-
2src/logic/GloballyFormula.h
-
4src/logic/InstantaneousRewardFormula.cpp
-
6src/logic/InstantaneousRewardFormula.h
-
2src/logic/NextFormula.cpp
-
2src/logic/NextFormula.h
-
2src/logic/OperatorFormula.cpp
-
2src/logic/OperatorFormula.h
-
9src/logic/PathRewardFormula.cpp
-
12src/logic/ProbabilityOperatorFormula.cpp
-
12src/logic/ProbabilityOperatorFormula.h
-
6src/logic/ReachabilityRewardFormula.cpp
-
9src/logic/ReachabilityRewardFormula.h
-
12src/logic/RewardOperatorFormula.cpp
-
12src/logic/RewardOperatorFormula.h
-
9src/logic/RewardPathFormula.cpp
-
6src/logic/RewardPathFormula.h
-
10src/logic/SteadyStateOperatorFormula.cpp
-
10src/logic/SteadyStateOperatorFormula.h
-
2src/logic/UnaryBooleanStateFormula.cpp
-
2src/logic/UnaryBooleanStateFormula.h
-
8src/logic/UnaryPathFormula.cpp
-
5src/logic/UnaryPathFormula.h
-
6src/logic/UnaryStateFormula.cpp
-
5src/logic/UnaryStateFormula.h
-
2src/logic/UntilFormula.cpp
-
2src/logic/UntilFormula.h
-
171src/modelchecker/AbstractModelChecker.cpp
-
62src/modelchecker/AbstractModelChecker.h
-
74src/modelchecker/CheckResult.cpp
-
35src/modelchecker/CheckResult.h
-
51src/modelchecker/ExplicitQualitativeCheckResult.cpp
-
60src/modelchecker/ExplicitQualitativeCheckResult.h
-
47src/modelchecker/ExplicitQuantitativeCheckResult.cpp
-
58src/modelchecker/ExplicitQuantitativeCheckResult.h
-
9src/modelchecker/QualitativeCheckResult.cpp
-
15src/modelchecker/QualitativeCheckResult.h
-
12src/modelchecker/QuantitativeCheckResult.cpp
-
16src/modelchecker/QuantitativeCheckResult.h
-
35src/modelchecker/SparseAllStatesQualitativeCheckResult.h
-
37src/modelchecker/SparseAllStatesQuantitativeCheckResult.h
-
244src/modelchecker/csl/AbstractModelChecker.h
-
24src/modelchecker/csl/ForwardDeclarations.h
-
154src/modelchecker/ltl/AbstractModelChecker.h
-
24src/modelchecker/ltl/ForwardDeclarations.h
-
297src/modelchecker/prctl/AbstractModelChecker.h
-
31src/modelchecker/prctl/CreatePrctlModelChecker.h
-
143src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h
-
24src/modelchecker/prctl/ForwardDeclarations.h
-
314src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
-
563src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
-
5src/parser/FormulaParser.cpp
-
1src/parser/FormulaParser.h
-
167test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
-
106test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
-
12test/functional/parser/FormulaParserTest.cpp
@ -1,9 +0,0 @@ |
|||
#include "src/logic/PathRewardFormula.h"
|
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
bool PathRewardFormula::isPathRewardFormula() const { |
|||
return true; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,9 @@ |
|||
#include "src/logic/RewardPathFormula.h"
|
|||
|
|||
namespace storm { |
|||
namespace logic { |
|||
bool RewardPathFormula::isRewardPathFormula() const { |
|||
return true; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,171 @@ |
|||
#include "src/modelchecker/AbstractModelChecker.h"
|
|||
|
|||
#include "src/utility/ConstantsComparator.h"
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/exceptions/NotImplementedException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
std::unique_ptr<CheckResult> AbstractModelChecker::check(storm::logic::Formula const& formula) { |
|||
STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check this formula."); |
|||
if (formula.isStateFormula()) { |
|||
return this->checkStateFormula(formula.asStateFormula()); |
|||
} else if (formula.isPathFormula()) { |
|||
return this->computeProbabilities(formula.asPathFormula()); |
|||
} else if (formula.isRewardPathFormula()) { |
|||
return this->computeRewards(formula.asRewardPathFormula()); |
|||
} |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::computeProbabilities(storm::logic::PathFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
if (pathFormula.isBoundedUntilFormula()) { |
|||
return this->computeBoundedUntilProbabilities(pathFormula.asBoundedUntilFormula()); |
|||
} else if (pathFormula.isConditionalPathFormula()) { |
|||
return this->computeConditionalProbabilities(pathFormula.asConditionalPathFormula()); |
|||
} else if (pathFormula.isEventuallyFormula()) { |
|||
return this->computeEventuallyProbabilities(pathFormula.asEventuallyFormula()); |
|||
} else if (pathFormula.isGloballyFormula()) { |
|||
return this->computeGloballyProbabilities(pathFormula.asGloballyFormula()); |
|||
} else if (pathFormula.isUntilFormula()) { |
|||
return this->computeUntilProbabilities(pathFormula.asUntilFormula()); |
|||
} |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer()); |
|||
return this->check(newFormula); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << pathFormula << "."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
if (rewardPathFormula.isCumulativeRewardFormula()) { |
|||
return this->computeCumulativeRewards(rewardPathFormula.asCumulativeRewardFormula()); |
|||
} else if (rewardPathFormula.isInstantaneousRewardFormula()) { |
|||
return this->computeInstantaneousRewards(rewardPathFormula.asInstantaneousRewardFormula()); |
|||
} else if (rewardPathFormula.isReachabilityRewardFormula()) { |
|||
return this->computeReachabilityRewards(rewardPathFormula.asReachabilityRewardFormula()); |
|||
} |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << "."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::checkStateFormula(storm::logic::StateFormula const& stateFormula) { |
|||
if (stateFormula.isBinaryBooleanStateFormula()) { |
|||
return this->checkBinaryBooleanStateFormula(stateFormula.asBinaryBooleanStateFormula()); |
|||
} else if (stateFormula.isBooleanLiteralFormula()) { |
|||
return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula()); |
|||
} else if (stateFormula.isProbabilityOperatorFormula()) { |
|||
return this->checkProbabilityOperatorFormula(stateFormula.asProbabilityOperatorFormula()); |
|||
} else if (stateFormula.isRewardOperatorFormula()) { |
|||
return this->checkRewardOperatorFormula(stateFormula.asRewardOperatorFormula()); |
|||
} else if (stateFormula.isSteadyStateOperatorFormula()) { |
|||
return this->checkSteadyStateOperatorFormula(stateFormula.asSteadyStateOperatorFormula()); |
|||
} else if (stateFormula.isAtomicExpressionFormula()) { |
|||
return this->checkAtomicExpressionFormula(stateFormula.asAtomicExpressionFormula()); |
|||
} else if (stateFormula.isAtomicLabelFormula()) { |
|||
return this->checkAtomicLabelFormula(stateFormula.asAtomicLabelFormula()); |
|||
} else if (stateFormula.isBooleanLiteralFormula()) { |
|||
return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula()); |
|||
} |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << "."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << "."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula) { |
|||
STORM_LOG_THROW(stateFormula.getLeftSubformula().isStateFormula() && stateFormula.getRightSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); |
|||
|
|||
std::unique_ptr<CheckResult> leftResult = this->check(stateFormula.getLeftSubformula().asStateFormula()); |
|||
std::unique_ptr<CheckResult> rightResult = this->check(stateFormula.getRightSubformula().asStateFormula()); |
|||
|
|||
*leftResult &= *rightResult; |
|||
return leftResult; |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << "."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula) { |
|||
STORM_LOG_THROW(stateFormula.getSubformula().isPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); |
|||
|
|||
// If the probability bound is 0 or 1, is suffices to do qualitative model checking.
|
|||
bool qualitative = false; |
|||
if (stateFormula.hasBound()) { |
|||
if (stateFormula.getBound() == storm::utility::zero<double>() || stateFormula.getBound() == storm::utility::one<double>()) { |
|||
qualitative = true; |
|||
} |
|||
} |
|||
if (stateFormula.hasOptimalityType()) { |
|||
return this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, stateFormula.getOptimalityType()); |
|||
} else { |
|||
return this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative); |
|||
} |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula) { |
|||
STORM_LOG_THROW(stateFormula.getSubformula().isRewardOperatorFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid."); |
|||
|
|||
// If the probability bound is 0, is suffices to do qualitative model checking.
|
|||
bool qualitative = false; |
|||
if (stateFormula.hasBound()) { |
|||
if (stateFormula.getBound() == storm::utility::zero<double>() || stateFormula.getBound() == storm::utility::one<double>()) { |
|||
qualitative = true; |
|||
} |
|||
} |
|||
if (stateFormula.hasOptimalityType()) { |
|||
return this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative, stateFormula.getOptimalityType()); |
|||
} else { |
|||
return this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative); |
|||
} |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::checkSteadyStateOperatorFormula(storm::logic::SteadyStateOperatorFormula const& stateFormula) { |
|||
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << "."); |
|||
} |
|||
|
|||
std::unique_ptr<CheckResult> AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula) { |
|||
std::unique_ptr<CheckResult> subResult = this->check(stateFormula.getSubformula()); |
|||
subResult->complement(); |
|||
return subResult; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,62 @@ |
|||
#ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ |
|||
#define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ |
|||
|
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "src/logic/Formulas.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
class AbstractModelChecker { |
|||
public: |
|||
virtual ~AbstractModelChecker() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Determines whether the model checker can handle the formula. If this method returns false, the formula |
|||
* must not be checked using the model checker. |
|||
* |
|||
* @param formula The formula for which to check whether the model checker can handle it. |
|||
* @return True iff the model checker can check the given formula. |
|||
*/ |
|||
virtual bool canHandle(storm::logic::Formula const& formula) const = 0; |
|||
|
|||
/*! |
|||
* Checks the provided formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @return The verification result. |
|||
*/ |
|||
virtual std::unique_ptr<CheckResult> check(storm::logic::Formula const& formula); |
|||
|
|||
// The methods to compute probabilities for path formulas. |
|||
virtual std::unique_ptr<CheckResult> computeProbabilities(storm::logic::PathFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()); |
|||
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()); |
|||
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>()); |
|||
virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()); |
|||
virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()); |
|||
virtual std::unique_ptr<CheckResult> computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()); |
|||
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>()); |
|||
|
|||
// The methods to compute the rewards for path formulas. |
|||
virtual std::unique_ptr<CheckResult> computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()); |
|||
virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()); |
|||
virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()); |
|||
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>()); |
|||
|
|||
// The methods to check state formulas. |
|||
virtual std::unique_ptr<CheckResult> checkStateFormula(storm::logic::StateFormula const& stateFormula); |
|||
virtual std::unique_ptr<CheckResult> checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula); |
|||
virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula); |
|||
virtual std::unique_ptr<CheckResult> checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula); |
|||
virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula); |
|||
virtual std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula); |
|||
virtual std::unique_ptr<CheckResult> checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula); |
|||
virtual std::unique_ptr<CheckResult> checkSteadyStateOperatorFormula(storm::logic::SteadyStateOperatorFormula const& stateFormula); |
|||
virtual std::unique_ptr<CheckResult> checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula); |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ */ |
|||
@ -0,0 +1,74 @@ |
|||
#include "src/modelchecker/CheckResult.h"
|
|||
|
|||
#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
|
|||
#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/exceptions/InvalidOperationException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
CheckResult& CheckResult::operator&=(CheckResult const& other) { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'and' on the two check results."); |
|||
} |
|||
|
|||
CheckResult& CheckResult::operator|=(CheckResult const& other) { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'or' on the two check results."); |
|||
} |
|||
|
|||
void CheckResult::complement() { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'not' on the check result."); |
|||
} |
|||
|
|||
bool CheckResult::isExplicit() const { |
|||
return false; |
|||
} |
|||
|
|||
bool CheckResult::isQuantitative() const { |
|||
return false; |
|||
} |
|||
|
|||
bool CheckResult::isQualitative() const { |
|||
return false; |
|||
} |
|||
|
|||
bool CheckResult::isResultForAllStates() const { |
|||
return false; |
|||
} |
|||
|
|||
std::ostream& operator<<(std::ostream& out, CheckResult& checkResult) { |
|||
checkResult.writeToStream(out); |
|||
return out; |
|||
} |
|||
|
|||
bool CheckResult::isExplicitQualitativeCheckResult() const { |
|||
return false; |
|||
} |
|||
|
|||
bool CheckResult::isExplicitQuantitativeCheckResult() const { |
|||
return false; |
|||
} |
|||
|
|||
ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult() { |
|||
return dynamic_cast<ExplicitQualitativeCheckResult&>(*this); |
|||
} |
|||
|
|||
ExplicitQualitativeCheckResult const& CheckResult::asExplicitQualitativeCheckResult() const { |
|||
return dynamic_cast<ExplicitQualitativeCheckResult const&>(*this); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
ExplicitQuantitativeCheckResult<ValueType>& CheckResult::asExplicitQuantitativeCheckResult() { |
|||
return dynamic_cast<ExplicitQuantitativeCheckResult<ValueType>&>(*this); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
ExplicitQuantitativeCheckResult<ValueType> const& CheckResult::asExplicitQuantitativeCheckResult() const { |
|||
return dynamic_cast<ExplicitQuantitativeCheckResult<ValueType> const&>(*this); |
|||
} |
|||
|
|||
// Explicitly instantiate the template functions.
|
|||
template ExplicitQuantitativeCheckResult<double>& CheckResult::asExplicitQuantitativeCheckResult(); |
|||
template ExplicitQuantitativeCheckResult<double> const& CheckResult::asExplicitQuantitativeCheckResult() const; |
|||
} |
|||
} |
|||
@ -1,12 +1,47 @@ |
|||
#ifndef STORM_MODELCHECKER_CHECKRESULT_H_ |
|||
#define STORM_MODELCHECKER_CHECKRESULT_H_ |
|||
|
|||
#include <iostream> |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
// Forward-declare the existing subclasses. |
|||
class QualitativeCheckResult; |
|||
template <typename ValueType> class QuantitativeCheckResult; |
|||
class ExplicitQualitativeCheckResult; |
|||
template <typename ValueType> class ExplicitQuantitativeCheckResult; |
|||
|
|||
// The base class of all check results. |
|||
class CheckResult { |
|||
public: |
|||
virtual CheckResult& operator&=(CheckResult const& other); |
|||
virtual CheckResult& operator|=(CheckResult const& other); |
|||
virtual void complement(); |
|||
|
|||
friend std::ostream& operator<<(std::ostream& out, CheckResult& checkResult); |
|||
|
|||
virtual bool isExplicit() const; |
|||
virtual bool isQuantitative() const; |
|||
virtual bool isQualitative() const; |
|||
virtual bool isResultForAllStates() const; |
|||
|
|||
virtual bool isExplicitQualitativeCheckResult() const; |
|||
virtual bool isExplicitQuantitativeCheckResult() const; |
|||
|
|||
ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult(); |
|||
ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const; |
|||
|
|||
template<typename ValueType> |
|||
ExplicitQuantitativeCheckResult<ValueType>& asExplicitQuantitativeCheckResult(); |
|||
|
|||
template<typename ValueType> |
|||
ExplicitQuantitativeCheckResult<ValueType> const& asExplicitQuantitativeCheckResult() const; |
|||
|
|||
protected: |
|||
virtual std::ostream& writeToStream(std::ostream& out) const = 0; |
|||
}; |
|||
|
|||
std::ostream& operator<<(std::ostream& out, CheckResult& checkResult); |
|||
} |
|||
} |
|||
|
|||
@ -0,0 +1,51 @@ |
|||
#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/exceptions/InvalidOperationException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
CheckResult& ExplicitQualitativeCheckResult::operator&=(CheckResult const& other) { |
|||
STORM_LOG_THROW(typeid(other) == typeid(ExplicitQualitativeCheckResult), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type."); |
|||
ExplicitQualitativeCheckResult const& otherCheckResult = static_cast<ExplicitQualitativeCheckResult const&>(other); |
|||
this->truthValues &= otherCheckResult.truthValues; |
|||
return *this; |
|||
} |
|||
|
|||
CheckResult& ExplicitQualitativeCheckResult::operator|=(CheckResult const& other) { |
|||
STORM_LOG_THROW(typeid(other) == typeid(ExplicitQualitativeCheckResult), storm::exceptions::InvalidOperationException, "Cannot perform logical 'or' on check results of incompatible type."); |
|||
ExplicitQualitativeCheckResult const& otherCheckResult = static_cast<ExplicitQualitativeCheckResult const&>(other); |
|||
this->truthValues |= otherCheckResult.truthValues; |
|||
return *this; |
|||
} |
|||
|
|||
bool ExplicitQualitativeCheckResult::operator[](uint_fast64_t index) const { |
|||
return truthValues.get(index); |
|||
} |
|||
|
|||
storm::storage::BitVector const& ExplicitQualitativeCheckResult::getTruthValues() const { |
|||
return truthValues; |
|||
} |
|||
|
|||
void ExplicitQualitativeCheckResult::complement() { |
|||
truthValues.complement(); |
|||
} |
|||
|
|||
bool ExplicitQualitativeCheckResult::isExplicit() const { |
|||
return true; |
|||
} |
|||
|
|||
bool ExplicitQualitativeCheckResult::isResultForAllStates() const { |
|||
return true; |
|||
} |
|||
|
|||
bool ExplicitQualitativeCheckResult::isExplicitQualitativeCheckResult() const { |
|||
return true; |
|||
} |
|||
|
|||
std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out) const { |
|||
out << truthValues; |
|||
return out; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,60 @@ |
|||
#ifndef STORM_MODELCHECKER_EXPLICITQUALITATIVECHECKRESULT_H_ |
|||
#define STORM_MODELCHECKER_EXPLICITQUALITATIVECHECKRESULT_H_ |
|||
|
|||
#include "src/modelchecker/QualitativeCheckResult.h" |
|||
#include "src/storage/BitVector.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
class ExplicitQualitativeCheckResult : public QualitativeCheckResult { |
|||
public: |
|||
/*! |
|||
* Constructs a check result with the provided truth values. |
|||
* |
|||
* @param truthValues The truth values of the result. |
|||
*/ |
|||
ExplicitQualitativeCheckResult(storm::storage::BitVector const& truthValues) : truthValues(truthValues) { |
|||
// Intentionally left empty. |
|||
|
|||
} |
|||
|
|||
/*! |
|||
* Constructs a check result with the provided truth values. |
|||
* |
|||
* @param truthValues The truth values of the result. |
|||
*/ |
|||
ExplicitQualitativeCheckResult(storm::storage::BitVector&& truthValues) : truthValues(std::move(truthValues)) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
ExplicitQualitativeCheckResult(ExplicitQualitativeCheckResult const& other) = default; |
|||
ExplicitQualitativeCheckResult& operator=(ExplicitQualitativeCheckResult const& other) = default; |
|||
#ifndef WINDOWS |
|||
ExplicitQualitativeCheckResult(ExplicitQualitativeCheckResult&& other) = default; |
|||
ExplicitQualitativeCheckResult& operator=(ExplicitQualitativeCheckResult&& other) = default; |
|||
#endif |
|||
|
|||
bool operator[](uint_fast64_t index) const; |
|||
|
|||
virtual bool isExplicit() const override; |
|||
virtual bool isResultForAllStates() const override; |
|||
|
|||
virtual bool isExplicitQualitativeCheckResult() const override; |
|||
|
|||
virtual CheckResult& operator&=(CheckResult const& other) override; |
|||
virtual CheckResult& operator|=(CheckResult const& other) override; |
|||
virtual void complement() override; |
|||
|
|||
storm::storage::BitVector const& getTruthValues() const; |
|||
|
|||
protected: |
|||
virtual std::ostream& writeToStream(std::ostream& out) const override; |
|||
|
|||
private: |
|||
// The values of the quantitative check result. |
|||
storm::storage::BitVector truthValues; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_EXPLICITQUALITATIVECHECKRESULT_H_ */ |
|||
@ -0,0 +1,47 @@ |
|||
#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/exceptions/InvalidOperationException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
template<typename ValueType> |
|||
std::vector<ValueType> const& ExplicitQuantitativeCheckResult<ValueType>::getValues() const { |
|||
return values; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::ostream& ExplicitQuantitativeCheckResult<ValueType>::writeToStream(std::ostream& out) const { |
|||
out << "["; |
|||
if (!values.empty()) { |
|||
for (auto element: values) { |
|||
out << element << " "; |
|||
} |
|||
} |
|||
out << "]"; |
|||
return out; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
ValueType ExplicitQuantitativeCheckResult<ValueType>::operator[](uint_fast64_t index) const { |
|||
return values[index]; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool ExplicitQuantitativeCheckResult<ValueType>::isExplicit() const { |
|||
return true; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool ExplicitQuantitativeCheckResult<ValueType>::isResultForAllStates() const { |
|||
return true; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool ExplicitQuantitativeCheckResult<ValueType>::isExplicitQuantitativeCheckResult() const { |
|||
return true; |
|||
} |
|||
|
|||
template class ExplicitQuantitativeCheckResult<double>; |
|||
} |
|||
} |
|||
@ -0,0 +1,58 @@ |
|||
#ifndef STORM_MODELCHECKER_EXPLICITQUANTITATIVECHECKRESULT_H_ |
|||
#define STORM_MODELCHECKER_EXPLICITQUANTITATIVECHECKRESULT_H_ |
|||
|
|||
#include <vector> |
|||
|
|||
#include "src/modelchecker/QuantitativeCheckResult.h" |
|||
#include "src/utility/OsDetection.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
template<typename ValueType> |
|||
class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult<ValueType> { |
|||
public: |
|||
/*! |
|||
* Constructs a check result with the provided values. |
|||
* |
|||
* @param values The values of the result. |
|||
*/ |
|||
ExplicitQuantitativeCheckResult(std::vector<ValueType> const& values) : values(values) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Constructs a check result with the provided values. |
|||
* |
|||
* @param values The values of the result. |
|||
*/ |
|||
ExplicitQuantitativeCheckResult(std::vector<ValueType>&& values) : values(std::move(values)) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
ExplicitQuantitativeCheckResult(ExplicitQuantitativeCheckResult const& other) = default; |
|||
ExplicitQuantitativeCheckResult& operator=(ExplicitQuantitativeCheckResult const& other) = default; |
|||
#ifndef WINDOWS |
|||
ExplicitQuantitativeCheckResult(ExplicitQuantitativeCheckResult&& other) = default; |
|||
ExplicitQuantitativeCheckResult& operator=(ExplicitQuantitativeCheckResult&& other) = default; |
|||
#endif |
|||
|
|||
ValueType operator[](uint_fast64_t index) const; |
|||
|
|||
virtual bool isExplicit() const override; |
|||
virtual bool isResultForAllStates() const override; |
|||
|
|||
virtual bool isExplicitQuantitativeCheckResult() const override; |
|||
|
|||
std::vector<ValueType> const& getValues() const; |
|||
|
|||
protected: |
|||
virtual std::ostream& writeToStream(std::ostream& out) const override; |
|||
|
|||
private: |
|||
// The values of the quantitative check result. |
|||
std::vector<ValueType> values; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_EXPLICITQUANTITATIVECHECKRESULT_H_ */ |
|||
@ -0,0 +1,9 @@ |
|||
#include "src/modelchecker/QualitativeCheckResult.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
bool QualitativeCheckResult::isQualitative() const { |
|||
return true; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,15 @@ |
|||
#ifndef STORM_MODELCHECKER_QUALITATIVECHECKRESULT_H_ |
|||
#define STORM_MODELCHECKER_QUALITATIVECHECKRESULT_H_ |
|||
|
|||
#include "src/modelchecker/CheckResult.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
class QualitativeCheckResult : public CheckResult { |
|||
public: |
|||
virtual bool isQualitative() const override; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_QUALITATIVECHECKRESULT_H_ */ |
|||
@ -0,0 +1,12 @@ |
|||
#include "src/modelchecker/QuantitativeCheckResult.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
template<typename ValueType> |
|||
bool QuantitativeCheckResult<ValueType>::isQuantitative() const { |
|||
return true; |
|||
} |
|||
|
|||
template class QuantitativeCheckResult<double>; |
|||
} |
|||
} |
|||
@ -0,0 +1,16 @@ |
|||
#ifndef STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ |
|||
#define STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ |
|||
|
|||
#include "src/modelchecker/CheckResult.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
template<typename ValueType> |
|||
class QuantitativeCheckResult : public CheckResult { |
|||
public: |
|||
virtual bool isQuantitative() const override; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ */ |
|||
@ -1,35 +0,0 @@ |
|||
#ifndef STORM_MODELCHECKER_SPARSEALLSTATESQUALITATIVECHECKRESULT_H_ |
|||
#define STORM_MODELCHECKER_SPARSEALLSTATESQUALITATIVECHECKRESULT_H_ |
|||
|
|||
#include "src/modelchecker/CheckResult.h" |
|||
#include "src/storage/BitVector.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
template<typename ValueType> |
|||
class SparseAllStatesQualitativeCheckResult : public CheckResult { |
|||
public: |
|||
/*! |
|||
* Constructs a check result with the provided truth values. |
|||
* |
|||
* @param truthValues The truth values of the result. |
|||
*/ |
|||
SparseAllStatesQualitativeCheckResult(storm::storage::BitVector&& truthValues) : truthValues(std::move(truthValues)) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
SparseAllStatesQualitativeCheckResult(SparseAllStatesQualitativeCheckResult const& other) = default; |
|||
SparseAllStatesQualitativeCheckResult& operator=(SparseAllStatesQualitativeCheckResult const& other) = default; |
|||
#ifndef WINDOWS |
|||
SparseAllStatesQualitativeCheckResult(SparseAllStatesQualitativeCheckResult&& other) = default; |
|||
SparseAllStatesQualitativeCheckResult& operator=(SparseAllStatesQualitativeCheckResult&& other) = default; |
|||
#endif |
|||
|
|||
private: |
|||
// The values of the quantitative check result. |
|||
storm::storage::BitVector truthValues; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_SPARSEALLSTATESQUALITATIVECHECKRESULT_H_ */ |
|||
@ -1,37 +0,0 @@ |
|||
#ifndef STORM_MODELCHECKER_SPARSEALLSTATESQUANTITATIVECHECKRESULT_H_ |
|||
#define STORM_MODELCHECKER_SPARSEALLSTATESQUANTITATIVECHECKRESULT_H_ |
|||
|
|||
#include <vector> |
|||
|
|||
#include "src/modelchecker/CheckResult.h" |
|||
#include "src/utility/OsDetection.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
template<typename ValueType> |
|||
class SparseAllStatesQuantitativeCheckResult : public CheckResult { |
|||
public: |
|||
/*! |
|||
* Constructs a check result with the provided values. |
|||
* |
|||
* @param values The values of the result. |
|||
*/ |
|||
SparseAllStatesQuantitativeCheckResult(std::vector<ValueType>&& values) : values(std::move(values)) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
SparseAllStatesQuantitativeCheckResult(SparseAllStatesQuantitativeCheckResult const& other) = default; |
|||
SparseAllStatesQuantitativeCheckResult& operator=(SparseAllStatesQuantitativeCheckResult const& other) = default; |
|||
#ifndef WINDOWS |
|||
SparseAllStatesQuantitativeCheckResult(SparseAllStatesQuantitativeCheckResult&& other) = default; |
|||
SparseAllStatesQuantitativeCheckResult& operator=(SparseAllStatesQuantitativeCheckResult&& other) = default; |
|||
#endif |
|||
|
|||
private: |
|||
// The values of the quantitative check result. |
|||
std::vector<ValueType> values; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_SPARSEALLSTATESQUANTITATIVECHECKRESULT_H_ */ |
|||
@ -1,244 +0,0 @@ |
|||
/* |
|||
* AbstractModelChecker.h |
|||
* |
|||
* Created on: 22.10.2012 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
#ifndef STORM_MODELCHECKER_CSL_ABSTRACTMODELCHECKER_H_ |
|||
#define STORM_MODELCHECKER_CSL_ABSTRACTMODELCHECKER_H_ |
|||
|
|||
#include <stack> |
|||
#include "src/exceptions/InvalidPropertyException.h" |
|||
#include "src/properties/Csl.h" |
|||
#include "src/storage/BitVector.h" |
|||
#include "src/models/AbstractModel.h" |
|||
|
|||
#include "log4cplus/logger.h" |
|||
#include "log4cplus/loggingmacros.h" |
|||
|
|||
#include <iostream> |
|||
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace csl { |
|||
|
|||
/*! |
|||
* @brief |
|||
* (Abstract) interface for all model checker classes. |
|||
* |
|||
* This class provides basic functions that are common to all model checkers (i.e. subclasses). It mainly declares |
|||
* abstract methods that are implemented in the concrete subclasses, but also covers checking procedures that are common |
|||
* to all model checkers for state-based models. |
|||
*/ |
|||
template<class Type> |
|||
class AbstractModelChecker : |
|||
// A list of interfaces the model checker supports. Typically, for each of the interfaces, a check method needs to |
|||
// be implemented that performs the corresponding check. |
|||
public virtual storm::properties::csl::IApModelChecker<Type>, |
|||
public virtual storm::properties::csl::IAndModelChecker<Type>, |
|||
public virtual storm::properties::csl::IOrModelChecker<Type>, |
|||
public virtual storm::properties::csl::INotModelChecker<Type>, |
|||
public virtual storm::properties::csl::IUntilModelChecker<Type>, |
|||
public virtual storm::properties::csl::IEventuallyModelChecker<Type>, |
|||
public virtual storm::properties::csl::IGloballyModelChecker<Type>, |
|||
public virtual storm::properties::csl::INextModelChecker<Type>, |
|||
public virtual storm::properties::csl::ITimeBoundedUntilModelChecker<Type>, |
|||
public virtual storm::properties::csl::ITimeBoundedEventuallyModelChecker<Type>, |
|||
public virtual storm::properties::csl::IProbabilisticBoundOperatorModelChecker<Type> { |
|||
|
|||
public: |
|||
/*! |
|||
* Constructs an AbstractModelChecker with the given model. |
|||
*/ |
|||
explicit AbstractModelChecker(storm::models::AbstractModel<Type> const& model) : minimumOperatorStack(), model(model) { |
|||
// Intentionally left empty. |
|||
} |
|||
/*! |
|||
* Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly |
|||
* constructed model checker will have the model of the given model checker as its associated model. |
|||
*/ |
|||
explicit AbstractModelChecker(AbstractModelChecker<Type> const& modelchecker) : minimumOperatorStack(), model(modelchecker.model) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Virtual destructor. Needs to be virtual, because this class has virtual methods. |
|||
*/ |
|||
virtual ~AbstractModelChecker() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Returns a pointer to the model checker object that is of the requested type as given by the template parameters. |
|||
* @returns A pointer to the model checker object that is of the requested type as given by the template parameters. |
|||
* If the model checker is not of the requested type, type casting will fail and result in an exception. |
|||
*/ |
|||
template <template <class T> class Target> |
|||
const Target<Type>* as() const { |
|||
try { |
|||
const Target<Type>* target = dynamic_cast<const Target<Type>*>(this); |
|||
return target; |
|||
} catch (std::bad_cast& bc) { |
|||
LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<Type>).name() << "."); |
|||
throw bc; |
|||
} |
|||
return nullptr; |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves the model associated with this model checker as a constant reference to an object of the type given |
|||
* by the template parameter. |
|||
* |
|||
* @returns A constant reference of the specified type to the model associated with this model checker. If the model |
|||
* is not of the requested type, type casting will fail and result in an exception. |
|||
*/ |
|||
template <class Model> |
|||
Model const& getModel() const { |
|||
try { |
|||
Model const& target = dynamic_cast<Model const&>(this->model); |
|||
return target; |
|||
} catch (std::bad_cast& bc) { |
|||
LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(this->model).name() << " to " << typeid(Model).name() << "."); |
|||
throw bc; |
|||
} |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula consisting of a single atomic proposition. |
|||
* |
|||
* @param formula The formula to be checked. |
|||
* @returns The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
storm::storage::BitVector checkAp(storm::properties::csl::Ap<Type> const& formula) const { |
|||
if (formula.getAp() == "true") { |
|||
return storm::storage::BitVector(model.getNumberOfStates(), true); |
|||
} else if (formula.getAp() == "false") { |
|||
return storm::storage::BitVector(model.getNumberOfStates()); |
|||
} |
|||
|
|||
if (!model.hasAtomicProposition(formula.getAp())) { |
|||
LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid."); |
|||
throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; |
|||
} |
|||
|
|||
return storm::storage::BitVector(model.getLabeledStates(formula.getAp())); |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is a logical "and" of two formulae. |
|||
* |
|||
* @param formula The formula to be checked. |
|||
* @returns The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
storm::storage::BitVector checkAnd(storm::properties::csl::And<Type> const& formula) const { |
|||
storm::storage::BitVector result = formula.getLeft()->check(*this); |
|||
storm::storage::BitVector right = formula.getRight()->check(*this); |
|||
result &= right; |
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is a logical "or" of two formulae. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @returns The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
storm::storage::BitVector checkOr(storm::properties::csl::Or<Type> const& formula) const { |
|||
storm::storage::BitVector result = formula.getLeft()->check(*this); |
|||
storm::storage::BitVector right = formula.getRight()->check(*this); |
|||
result |= right; |
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is a logical "not" of a sub-formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @returns The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
storm::storage::BitVector checkNot(const storm::properties::csl::Not<Type>& formula) const { |
|||
storm::storage::BitVector result = formula.getChild()->check(*this); |
|||
result.complement(); |
|||
return result; |
|||
} |
|||
|
|||
|
|||
/*! |
|||
* Checks the given formula that is a P operator over a path formula featuring a value bound. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @returns The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::properties::csl::ProbabilisticBoundOperator<Type> const& formula) const { |
|||
// First, we need to compute the probability for satisfying the path formula for each state. |
|||
std::vector<Type> quantitativeResult = formula.getChild()->check(*this, false); |
|||
|
|||
// Create resulting bit vector that will hold the yes/no-answer for every state. |
|||
storm::storage::BitVector result(quantitativeResult.size()); |
|||
|
|||
// Now, we can compute which states meet the bound specified in this operator and set the |
|||
// corresponding bits to true in the resulting vector. |
|||
for (uint_fast64_t i = 0; i < quantitativeResult.size(); ++i) { |
|||
if (formula.meetsBound(quantitativeResult[i])) { |
|||
result.set(i, true); |
|||
} |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula and determines whether minimum or maximum probabilities or rewards are to be computed for the formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param minimumOperator True iff minimum probabilities/rewards are to be computed. |
|||
* @returns The probabilities to satisfy the formula or the rewards accumulated by it, represented by a vector. |
|||
*/ |
|||
virtual std::vector<Type> checkMinMaxOperator(storm::properties::csl::AbstractPathFormula<Type> const & formula, bool minimumOperator) const { |
|||
minimumOperatorStack.push(minimumOperator); |
|||
std::vector<Type> result = formula.check(*this, false); |
|||
minimumOperatorStack.pop(); |
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula and determines whether minimum or maximum probabilities or rewards are to be computed for the formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param minimumOperator True iff minimum probabilities/rewards are to be computed. |
|||
* @returns The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
virtual storm::storage::BitVector checkMinMaxOperator(storm::properties::csl::AbstractStateFormula<Type> const & formula, bool minimumOperator) const { |
|||
minimumOperatorStack.push(minimumOperator); |
|||
storm::storage::BitVector result = formula.check(*this); |
|||
minimumOperatorStack.pop(); |
|||
return result; |
|||
} |
|||
|
|||
protected: |
|||
|
|||
/*! |
|||
* A stack used for storing whether we are currently computing min or max probabilities or rewards, respectively. |
|||
* The topmost element is true if and only if we are currently computing minimum probabilities or rewards. |
|||
*/ |
|||
mutable std::stack<bool> minimumOperatorStack; |
|||
|
|||
private: |
|||
|
|||
/*! |
|||
* A constant reference to the model associated with this model checker. |
|||
* |
|||
* @note that we do not own this object, but merely have a constant reference to it. That means that using the |
|||
* model checker object is unsafe after the object has been destroyed. |
|||
*/ |
|||
storm::models::AbstractModel<Type> const& model; |
|||
}; |
|||
|
|||
} // namespace csl |
|||
} // namespace modelchecker |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_CSL_ABSTRACTMODELCHECKER_H_ */ |
|||
@ -1,24 +0,0 @@ |
|||
/* |
|||
* ForwardDeclarations.h |
|||
* |
|||
* Created on: 14.01.2013 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
#ifndef STORM_MODELCHECKER_FORWARDDECLARATIONS_H_ |
|||
#define STORM_MODELCHECKER_FORWARDDECLARATIONS_H_ |
|||
|
|||
// Forward declare the abstract model checker. This is used by the formula classes that need this declaration for |
|||
// the callback methods (i.e., the check methods). |
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace csl { |
|||
|
|||
template <class Type> |
|||
class AbstractModelChecker; |
|||
|
|||
} //namespace csl |
|||
} //namespace modelchecker |
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_FORWARDDECLARATIONS_H_ */ |
|||
@ -1,154 +0,0 @@ |
|||
/* |
|||
* AbstractModelChecker.h |
|||
* |
|||
* Created on: 22.10.2012 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
#ifndef STORM_MODELCHECKER_LTL_ABSTRACTMODELCHECKER_H_ |
|||
#define STORM_MODELCHECKER_LTL_ABSTRACTMODELCHECKER_H_ |
|||
|
|||
#include "src/exceptions/InvalidPropertyException.h" |
|||
#include "src/properties/Ltl.h" |
|||
#include "src/storage/BitVector.h" |
|||
#include "src/models/AbstractModel.h" |
|||
|
|||
#include "log4cplus/logger.h" |
|||
#include "log4cplus/loggingmacros.h" |
|||
|
|||
#include <iostream> |
|||
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace ltl { |
|||
|
|||
/*! |
|||
* @brief |
|||
* (Abstract) interface for all model checker classes. |
|||
* |
|||
* This class provides basic functions that are common to all model checkers (i.e. subclasses). It mainly declares |
|||
* abstract methods that are implemented in the concrete subclasses, but also covers checking procedures that are common |
|||
* to all model checkers for state-based models. |
|||
*/ |
|||
template<class Type> |
|||
class AbstractModelChecker : |
|||
// A list of interfaces the model checker supports. Typically, for each of the interfaces, a check method needs to |
|||
// be implemented that performs the corresponding check. |
|||
public virtual storm::properties::ltl::IApModelChecker<Type>, |
|||
public virtual storm::properties::ltl::IAndModelChecker<Type>, |
|||
public virtual storm::properties::ltl::IOrModelChecker<Type>, |
|||
public virtual storm::properties::ltl::INotModelChecker<Type>, |
|||
public virtual storm::properties::ltl::IUntilModelChecker<Type>, |
|||
public virtual storm::properties::ltl::IEventuallyModelChecker<Type>, |
|||
public virtual storm::properties::ltl::IGloballyModelChecker<Type>, |
|||
public virtual storm::properties::ltl::INextModelChecker<Type>, |
|||
public virtual storm::properties::ltl::IBoundedUntilModelChecker<Type>, |
|||
public virtual storm::properties::ltl::IBoundedEventuallyModelChecker<Type> { |
|||
|
|||
public: |
|||
/*! |
|||
* Constructs an AbstractModelChecker with the given model. |
|||
*/ |
|||
explicit AbstractModelChecker(storm::models::AbstractModel<Type> const& model) : model(model) { |
|||
// Intentionally left empty. |
|||
} |
|||
/*! |
|||
* Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly |
|||
* constructed model checker will have the model of the given model checker as its associated model. |
|||
*/ |
|||
explicit AbstractModelChecker(AbstractModelChecker<Type> const& modelchecker) : model(modelchecker.model) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Virtual destructor. Needs to be virtual, because this class has virtual methods. |
|||
*/ |
|||
virtual ~AbstractModelChecker() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Returns a pointer to the model checker object that is of the requested type as given by the template parameters. |
|||
* @returns A pointer to the model checker object that is of the requested type as given by the template parameters. |
|||
* If the model checker is not of the requested type, type casting will fail and result in an exception. |
|||
*/ |
|||
template <template <class T> class Target> |
|||
const Target<Type>* as() const { |
|||
try { |
|||
const Target<Type>* target = dynamic_cast<const Target<Type>*>(this); |
|||
return target; |
|||
} catch (std::bad_cast& bc) { |
|||
LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<Type>).name() << "."); |
|||
throw bc; |
|||
} |
|||
return nullptr; |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves the model associated with this model checker as a constant reference to an object of the type given |
|||
* by the template parameter. |
|||
* |
|||
* @returns A constant reference of the specified type to the model associated with this model checker. If the model |
|||
* is not of the requested type, type casting will fail and result in an exception. |
|||
*/ |
|||
template <class Model> |
|||
Model const& getModel() const { |
|||
try { |
|||
Model const& target = dynamic_cast<Model const&>(this->model); |
|||
return target; |
|||
} catch (std::bad_cast& bc) { |
|||
LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(this->model).name() << " to " << typeid(Model).name() << "."); |
|||
throw bc; |
|||
} |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula consisting of a single atomic proposition. |
|||
* |
|||
* @param formula The formula to be checked. |
|||
* @returns The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
virtual std::vector<Type> checkAp(storm::properties::ltl::Ap<Type> const& formula) const = 0; |
|||
|
|||
/*! |
|||
* Checks the given formula that is a logical "and" of two formulae. |
|||
* |
|||
* @param formula The formula to be checked. |
|||
* @returns The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
virtual std::vector<Type> checkAnd(storm::properties::ltl::And<Type> const& formula) const = 0; |
|||
|
|||
/*! |
|||
* Checks the given formula that is a logical "or" of two formulae. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @returns The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
virtual std::vector<Type> checkOr(storm::properties::ltl::Or<Type> const& formula) const = 0; |
|||
|
|||
/*! |
|||
* Checks the given formula that is a logical "not" of a sub-formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @returns The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
virtual std::vector<Type> checkNot(const storm::properties::ltl::Not<Type>& formula) const = 0; |
|||
|
|||
private: |
|||
|
|||
/*! |
|||
* A constant reference to the model associated with this model checker. |
|||
* |
|||
* @note that we do not own this object, but merely have a constant reference to it. That means that using the |
|||
* model checker object is unsafe after the object has been destroyed. |
|||
*/ |
|||
storm::models::AbstractModel<Type> const& model; |
|||
}; |
|||
|
|||
} // namespace ltl |
|||
} // namespace modelchecker |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_LTL_ABSTRACTMODELCHECKER_H_ */ |
|||
@ -1,24 +0,0 @@ |
|||
/* |
|||
* ForwardDeclarations.h |
|||
* |
|||
* Created on: 14.01.2013 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
#ifndef STORM_MODELCHECKER_LTL_FORWARDDECLARATIONS_H_ |
|||
#define STORM_MODELCHECKER_LTL_FORWARDDECLARATIONS_H_ |
|||
|
|||
// Forward declare the abstract model checker. This is used by the formula classes that need this declaration for |
|||
// the callback methods (i.e., the check methods). |
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace ltl { |
|||
|
|||
template <class Type> |
|||
class AbstractModelChecker; |
|||
|
|||
} //namespace ltl |
|||
} //namespace modelchecker |
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_LTL_FORWARDDECLARATIONS_H_ */ |
|||
@ -1,297 +0,0 @@ |
|||
/* |
|||
* AbstractModelChecker.h |
|||
* |
|||
* Created on: 22.10.2012 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
#ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ |
|||
#define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ |
|||
|
|||
// Forward declaration of abstract model checker class needed by the formula classes. |
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace prctl { |
|||
template <class Type> class AbstractModelChecker; |
|||
} |
|||
} |
|||
} |
|||
|
|||
#include <stack> |
|||
#include "src/exceptions/InvalidPropertyException.h" |
|||
#include "src/properties/Prctl.h" |
|||
#include "src/storage/BitVector.h" |
|||
#include "src/models/AbstractModel.h" |
|||
#include "src/settings/SettingsManager.h" |
|||
|
|||
#include "log4cplus/logger.h" |
|||
#include "log4cplus/loggingmacros.h" |
|||
|
|||
#include <iostream> |
|||
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace prctl { |
|||
|
|||
/*! |
|||
* @brief |
|||
* (Abstract) interface for all model checker classes. |
|||
* |
|||
* This class provides basic functions that are common to all model checkers (i.e. subclasses). It mainly declares |
|||
* abstract methods that are implemented in the concrete subclasses, but also covers checking procedures that are common |
|||
* to all model checkers for state-based models. |
|||
*/ |
|||
template<class Type> |
|||
class AbstractModelChecker : |
|||
// A list of interfaces the model checker supports. Typically, for each of the interfaces, a check method needs to |
|||
// be implemented that performs the corresponding check. |
|||
public virtual storm::properties::prctl::IApModelChecker<Type>, |
|||
public virtual storm::properties::prctl::IAndModelChecker<Type>, |
|||
public virtual storm::properties::prctl::IOrModelChecker<Type>, |
|||
public virtual storm::properties::prctl::INotModelChecker<Type>, |
|||
public virtual storm::properties::prctl::IUntilModelChecker<Type>, |
|||
public virtual storm::properties::prctl::IEventuallyModelChecker<Type>, |
|||
public virtual storm::properties::prctl::IGloballyModelChecker<Type>, |
|||
public virtual storm::properties::prctl::INextModelChecker<Type>, |
|||
public virtual storm::properties::prctl::IBoundedUntilModelChecker<Type>, |
|||
public virtual storm::properties::prctl::IBoundedEventuallyModelChecker<Type>, |
|||
public virtual storm::properties::prctl::IProbabilisticBoundOperatorModelChecker<Type>, |
|||
public virtual storm::properties::prctl::IRewardBoundOperatorModelChecker<Type>, |
|||
public virtual storm::properties::prctl::IReachabilityRewardModelChecker<Type>, |
|||
public virtual storm::properties::prctl::ICumulativeRewardModelChecker<Type>, |
|||
public virtual storm::properties::prctl::IInstantaneousRewardModelChecker<Type> { |
|||
|
|||
public: |
|||
/*! |
|||
* Constructs an AbstractModelChecker with the given model. |
|||
*/ |
|||
explicit AbstractModelChecker(storm::models::AbstractModel<Type> const& model) : minimumOperatorStack(), model(model) { |
|||
// Intentionally left empty. |
|||
} |
|||
/*! |
|||
* Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly |
|||
* constructed model checker will have the model of the given model checker as its associated model. |
|||
*/ |
|||
explicit AbstractModelChecker(AbstractModelChecker<Type> const& modelchecker) : minimumOperatorStack(), model(modelchecker.model) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Virtual destructor. Needs to be virtual, because this class has virtual methods. |
|||
*/ |
|||
virtual ~AbstractModelChecker() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Returns a pointer to the model checker object that is of the requested type as given by the template parameters. |
|||
* |
|||
* @return A pointer to the model checker object that is of the requested type as given by the template parameters. |
|||
* If the model checker is not of the requested type, type casting will fail and result in an exception. |
|||
*/ |
|||
template <template <class T> class Target> |
|||
const Target<Type>* as() const { |
|||
try { |
|||
const Target<Type>* target = dynamic_cast<const Target<Type>*>(this); |
|||
return target; |
|||
} catch (std::bad_cast& bc) { |
|||
LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<Type>).name() << "."); |
|||
throw bc; |
|||
} |
|||
return nullptr; |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves the model associated with this model checker as a constant reference to an object of the type given |
|||
* by the template parameter. |
|||
* |
|||
* @return A constant reference of the specified type to the model associated with this model checker. If the model |
|||
* is not of the requested type, type casting will fail and result in an exception. |
|||
*/ |
|||
template <class Model> |
|||
Model const& getModel() const { |
|||
try { |
|||
Model const& target = dynamic_cast<Model const&>(this->model); |
|||
return target; |
|||
} catch (std::bad_cast& bc) { |
|||
LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(this->model).name() << " to " << typeid(Model).name() << "."); |
|||
throw bc; |
|||
} |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula consisting of a single atomic proposition. |
|||
* |
|||
* @param formula The formula to be checked. |
|||
* @return The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
storm::storage::BitVector checkAp(storm::properties::prctl::Ap<Type> const& formula) const { |
|||
if (formula.getAp() == "true") { |
|||
return storm::storage::BitVector(model.getNumberOfStates(), true); |
|||
} else if (formula.getAp() == "false") { |
|||
return storm::storage::BitVector(model.getNumberOfStates()); |
|||
} |
|||
|
|||
if (!model.hasAtomicProposition(formula.getAp())) { |
|||
LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid."); |
|||
throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; |
|||
} |
|||
|
|||
return storm::storage::BitVector(model.getLabeledStates(formula.getAp())); |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is a logical "and" of two formulae. |
|||
* |
|||
* @param formula The formula to be checked. |
|||
* @return The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
storm::storage::BitVector checkAnd(storm::properties::prctl::And<Type> const& formula) const { |
|||
storm::storage::BitVector result = formula.getLeft()->check(*this); |
|||
storm::storage::BitVector right = formula.getRight()->check(*this); |
|||
result &= right; |
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is a logical "or" of two formulae. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @return The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
storm::storage::BitVector checkOr(storm::properties::prctl::Or<Type> const& formula) const { |
|||
storm::storage::BitVector result = formula.getLeft()->check(*this); |
|||
storm::storage::BitVector right = formula.getRight()->check(*this); |
|||
result |= right; |
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is a logical "not" of a sub-formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @return The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
storm::storage::BitVector checkNot(const storm::properties::prctl::Not<Type>& formula) const { |
|||
storm::storage::BitVector result = formula.getChild()->check(*this); |
|||
result.complement(); |
|||
return result; |
|||
} |
|||
|
|||
|
|||
/*! |
|||
* Checks the given formula that is a P operator over a path formula featuring a value bound. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @return The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::properties::prctl::ProbabilisticBoundOperator<Type> const& formula) const { |
|||
// First, we need to compute the probability for satisfying the path formula for each state. |
|||
std::vector<Type> quantitativeResult = formula.getChild()->check(*this, false); |
|||
|
|||
// Create resulting bit vector that will hold the yes/no-answer for every state. |
|||
storm::storage::BitVector result(quantitativeResult.size()); |
|||
|
|||
// Now, we can compute which states meet the bound specified in this operator and set the |
|||
// corresponding bits to true in the resulting vector. |
|||
for (uint_fast64_t i = 0; i < quantitativeResult.size(); ++i) { |
|||
if (formula.meetsBound(quantitativeResult[i])) { |
|||
result.set(i, true); |
|||
} |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is an R operator over a reward formula featuring a value bound. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @return The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
virtual storm::storage::BitVector checkRewardBoundOperator(const storm::properties::prctl::RewardBoundOperator<Type>& formula) const { |
|||
// First, we need to compute the probability for satisfying the path formula for each state. |
|||
std::vector<Type> quantitativeResult = formula.getChild()->check(*this, false); |
|||
|
|||
// Create resulting bit vector that will hold the yes/no-answer for every state. |
|||
storm::storage::BitVector result(quantitativeResult.size()); |
|||
|
|||
// Now, we can compute which states meet the bound specified in this operator and set the |
|||
// corresponding bits to true in the resulting vector. |
|||
for (uint_fast64_t i = 0; i < quantitativeResult.size(); ++i) { |
|||
if (formula.meetsBound(quantitativeResult[i])) { |
|||
result.set(i, true); |
|||
} |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula and determines whether minimum or maximum probabilities are to be computed for the formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param optOperator True iff minimum probabilities are to be computed. |
|||
* @returns The probabilities to satisfy the formula, represented by a vector. |
|||
*/ |
|||
virtual std::vector<Type> checkOptimizingOperator(storm::properties::prctl::AbstractPathFormula<Type> const & formula, bool optOperator) const { |
|||
minimumOperatorStack.push(optOperator); |
|||
std::vector<Type> result = formula.check(*this, false); |
|||
minimumOperatorStack.pop(); |
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula and determines whether minimum or maximum rewards are to be computed for the formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param optOperator True iff minimum rewards are to be computed. |
|||
* @returns The the rewards accumulated by the formula, represented by a vector. |
|||
*/ |
|||
virtual std::vector<Type> checkOptimizingOperator(storm::properties::prctl::AbstractRewardPathFormula<Type> const & formula, bool optOperator) const { |
|||
minimumOperatorStack.push(optOperator); |
|||
std::vector<Type> result = formula.check(*this, false); |
|||
minimumOperatorStack.pop(); |
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula and determines whether minimum or maximum probabilities or rewards are to be computed for the formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param optOperator True iff minimum probabilities/rewards are to be computed. |
|||
* @returns The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
virtual storm::storage::BitVector checkOptimizingOperator(storm::properties::prctl::AbstractStateFormula<Type> const & formula, bool optOperator) const { |
|||
minimumOperatorStack.push(optOperator); |
|||
storm::storage::BitVector result = formula.check(*this); |
|||
minimumOperatorStack.pop(); |
|||
return result; |
|||
} |
|||
|
|||
protected: |
|||
|
|||
/*! |
|||
* A stack used for storing whether we are currently computing min or max probabilities or rewards, respectively. |
|||
* The topmost element is true if and only if we are currently computing minimum probabilities or rewards. |
|||
*/ |
|||
mutable std::stack<bool> minimumOperatorStack; |
|||
|
|||
private: |
|||
|
|||
/*! |
|||
* A constant reference to the model associated with this model checker. |
|||
* |
|||
* @note that we do not own this object, but merely have a constant reference to it. That means that using the |
|||
* model checker object is unsafe after the object has been destroyed. |
|||
*/ |
|||
storm::models::AbstractModel<Type> const& model; |
|||
}; |
|||
|
|||
} // namespace prctl |
|||
} // namespace modelchecker |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_PRCTL_DTMCPRCTLMODELCHECKER_H_ */ |
|||
@ -1,31 +0,0 @@ |
|||
#ifndef STORM_MODELCHECKER_PRCTL_CREATEPRCTLMODELCHECKER_H_ |
|||
#define STORM_MODELCHECKER_PRCTL_CREATEPRCTLMODELCHECKER_H_ |
|||
|
|||
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" |
|||
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" |
|||
#include "src/solver/GmmxxLinearEquationSolver.h" |
|||
#include "src/solver/NativeLinearEquationSolver.h" |
|||
#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" |
|||
#include "src/solver/GurobiLpSolver.h" |
|||
/*! |
|||
* Creates a model checker for the given DTMC that complies with the given options. |
|||
* |
|||
* @param dtmc A reference to the DTMC for which the model checker is to be created. |
|||
* @return A pointer to the resulting model checker. |
|||
*/ |
|||
storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Dtmc<double> const& dtmc) { |
|||
return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double>(dtmc); |
|||
} |
|||
|
|||
/*! |
|||
* Creates a model checker for the given MDP that complies with the given options. |
|||
* |
|||
* @param mdp The Dtmc that the model checker will check |
|||
* @return |
|||
*/ |
|||
storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Mdp<double> const & mdp) { |
|||
// Create the appropriate model checker. |
|||
return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double>(mdp); |
|||
} |
|||
|
|||
#endif |
|||
@ -1,143 +0,0 @@ |
|||
/* |
|||
* EigenDtmcPrctlModelChecker.h |
|||
* |
|||
* Created on: 07.12.2012 |
|||
* Author: |
|||
*/ |
|||
|
|||
#ifndef STORM_MODELCHECKER_PRCTL_EIGENDTMCPRCTLMODELCHECKER_H_ |
|||
#define STORM_MODELCHECKER_PRCTL_EIGENDTMCPRCTLMODELCHECKER_H_ |
|||
|
|||
#include "src/utility/vector.h" |
|||
|
|||
#include "src/models/Dtmc.h" |
|||
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" |
|||
#include "src/utility/constants.h" |
|||
#include "src/exceptions/NoConvergenceException.h" |
|||
|
|||
#include "Eigen/Sparse" |
|||
#include "Eigen/src/IterativeLinearSolvers/BiCGSTAB.h" |
|||
#include "src/adapters/EigenAdapter.h" |
|||
|
|||
#include "gmm/gmm_matrix.h" |
|||
#include "gmm/gmm_iter_solvers.h" |
|||
|
|||
#include "log4cplus/logger.h" |
|||
#include "log4cplus/loggingmacros.h" |
|||
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace prctl { |
|||
|
|||
/* |
|||
* A model checking engine that makes use of the eigen backend. |
|||
*/ |
|||
template <class Type> |
|||
class EigenDtmcPrctlModelChecker : public SparseDtmcPrctlModelChecker<Type> { |
|||
|
|||
typedef Eigen::Matrix<Type, -1, 1, 0, -1, 1> VectorType; |
|||
typedef Eigen::Map<VectorType> MapType; |
|||
|
|||
public: |
|||
explicit EigenDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : SparseDtmcPrctlModelChecker<Type>(dtmc) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
virtual ~EigenDtmcPrctlModelChecker() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
private: |
|||
virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>** vector, std::vector<Type>* summand, uint_fast64_t repetitions = 1) const { |
|||
// Transform the transition probability matrix to the eigen format to use its arithmetic. |
|||
Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(matrix); |
|||
|
|||
Type* p = &((**vector)[0]); // get the address storing the data for result |
|||
MapType vectorMap(p, (*vector)->size()); // vectorMap shares data |
|||
|
|||
p = &((*summand)[0]); |
|||
MapType summandMap(p, summand->size()); |
|||
|
|||
// Now perform matrix-vector multiplication as long as we meet the bound. |
|||
std::vector<Type>* swap = nullptr; |
|||
std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates()); |
|||
for (uint_fast64_t i = 0; i < repetitions; ++i) { |
|||
vectorMap = (*eigenMatrix) * (vectorMap); |
|||
|
|||
// If requested, add an offset to the current result vector. |
|||
if (summand != nullptr) { |
|||
vectorMap = vectorMap + summandMap; |
|||
} |
|||
} |
|||
delete eigenMatrix; |
|||
} |
|||
|
|||
/*! |
|||
* Solves the linear equation system Ax=b with the given parameters. |
|||
* |
|||
* @param A The matrix A specifying the coefficients of the linear equations. |
|||
* @param x The vector x for which to solve the equations. The initial value of the elements of |
|||
* this vector are used as the initial guess and might thus influence performance and convergence. |
|||
* @param b The vector b specifying the values on the right-hand-sides of the equations. |
|||
* @return The solution of the system of linear equations in form of the elements of the vector |
|||
* x. |
|||
*/ |
|||
virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>** vector, std::vector<Type>& b) const { |
|||
// Get the settings object to customize linear solving. |
|||
storm::settings::Settings* s = storm::settings::Settings::getInstance(); |
|||
|
|||
// Transform the submatric matrix to the eigen format to use its solvers |
|||
Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix<Type>(matrix); |
|||
|
|||
Eigen::BiCGSTAB<Eigen::SparseMatrix<Type, 1, int_fast32_t>> solver; |
|||
solver.compute(*eigenMatrix); |
|||
if(solver.info()!= Eigen::ComputationInfo::Success) { |
|||
// decomposition failed |
|||
LOG4CPLUS_ERROR(logger, "Decomposition of matrix failed!"); |
|||
} |
|||
uint_fast64_t maxIterations = s->getOptionByLongName("maxIterations").getArgument(0).getValueAsUnsignedInteger(); |
|||
solver.setMaxIterations(static_cast<int>(maxIterations)); |
|||
solver.setTolerance(s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); |
|||
|
|||
std::cout << matrix.toString(nullptr) << std::endl; |
|||
std::cout << **vector << std::endl; |
|||
std::cout << b << std::endl; |
|||
|
|||
std::cout << *eigenMatrix << std::endl; |
|||
|
|||
// Map for x |
|||
Type *px = &((**vector)[0]); // get the address storing the data for x |
|||
MapType vectorX(px, (*vector)->size()); // vectorX shares data |
|||
|
|||
Type *pb = &(b[0]); // get the address storing the data for b |
|||
MapType vectorB(pb, b.size()); // vectorB shares data |
|||
|
|||
vectorX = solver.solveWithGuess(vectorB, vectorX); |
|||
|
|||
std::cout << **vector << std::endl; |
|||
|
|||
if(solver.info() == Eigen::ComputationInfo::InvalidInput) { |
|||
// solving failed |
|||
LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: InvalidInput"); |
|||
} else if(solver.info() == Eigen::ComputationInfo::NoConvergence) { |
|||
// NoConvergence |
|||
throw storm::exceptions::NoConvergenceException() << "Failed to converge within " << solver.iterations() << " out of a maximum of " << solver.maxIterations() << " iterations."; |
|||
} else if(solver.info() == Eigen::ComputationInfo::NumericalIssue) { |
|||
// NumericalIssue |
|||
LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: NumericalIssue"); |
|||
} else if(solver.info() == Eigen::ComputationInfo::Success) { |
|||
// solving Success |
|||
LOG4CPLUS_INFO(logger, "Solving of Submatrix succeeded: Success"); |
|||
} |
|||
|
|||
delete eigenMatrix; |
|||
} |
|||
}; |
|||
|
|||
} //namespace prctl |
|||
} //namespace modelchecker |
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_PRCTL_EIGENDTMCPRCTLMODELCHECKER_H_ */ |
|||
@ -1,24 +0,0 @@ |
|||
/* |
|||
* ForwardDeclarations.h |
|||
* |
|||
* Created on: 14.01.2013 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
#ifndef STORM_MODELCHECKER_PRCTL_FORWARDDECLARATIONS_H_ |
|||
#define STORM_MODELCHECKER_PRCTL_FORWARDDECLARATIONS_H_ |
|||
|
|||
// Forward declare the abstract model checker. This is used by the formula classes that need this declaration for |
|||
// the callback methods (i.e., the check methods). |
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace prctl { |
|||
|
|||
template <class Type> |
|||
class AbstractModelChecker; |
|||
|
|||
} //namespace prctl |
|||
} //namespace modelchecker |
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_PRCTL_FORWARDDECLARATIONS_H_ */ |
|||
@ -0,0 +1,314 @@ |
|||
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
|
|||
|
|||
#include <vector>
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/utility/vector.h"
|
|||
#include "src/utility/graph.h"
|
|||
|
|||
#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
|
|||
#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
|
|||
|
|||
#include "src/exceptions/InvalidPropertyException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace prctl { |
|||
template<typename ValueType> |
|||
SparseDtmcPrctlModelChecker<ValueType>::SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model, std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>&& linearEquationSolver) : model(model), linearEquationSolver(std::move(linearEquationSolver)) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
SparseDtmcPrctlModelChecker<ValueType>::SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model) : model(model), linearEquationSolver(storm::utility::solver::getLinearEquationSolver<ValueType>()) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType> |
|||
bool SparseDtmcPrctlModelChecker<ValueType>::canHandle(storm::logic::Formula const& formula) const { |
|||
return formula.isPctlStateFormula() || formula.isPctlPathFormula(); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound) { |
|||
std::vector<ValueType> result(model.getNumberOfStates()); |
|||
|
|||
// If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis.
|
|||
storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(model.getBackwardTransitions(), phiStates, psiStates, true, stepBound); |
|||
STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states.") |
|||
|
|||
if (!statesWithProbabilityGreater0.empty()) { |
|||
// We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
|
|||
storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, true); |
|||
|
|||
// Compute the new set of target states in the reduced system.
|
|||
storm::storage::BitVector rightStatesInReducedSystem = psiStates % statesWithProbabilityGreater0; |
|||
|
|||
// Make all rows absorbing that satisfy the second sub-formula.
|
|||
submatrix.makeRowsAbsorbing(rightStatesInReducedSystem); |
|||
|
|||
// Create the vector with which to multiply.
|
|||
std::vector<ValueType> subresult(statesWithProbabilityGreater0.getNumberOfSetBits()); |
|||
storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::one<ValueType>()); |
|||
|
|||
// Perform the matrix vector multiplication as often as required by the formula bound.
|
|||
STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available."); |
|||
this->linearEquationSolver->performMatrixVectorMultiplication(submatrix, subresult, nullptr, stepBound); |
|||
|
|||
// Set the values of the resulting vector accordingly.
|
|||
storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult); |
|||
} |
|||
storm::utility::vector::setVectorValues<ValueType>(result, ~statesWithProbabilityGreater0, storm::utility::zero<ValueType>()); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); |
|||
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); |
|||
ExplicitQualitativeCheckResult& leftResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*leftResultPointer); |
|||
ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer); |
|||
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValues(), rightResult.getTruthValues(), pathFormula.getUpperBound()))); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeNextProbabilitiesHelper(storm::storage::BitVector const& nextStates) { |
|||
// Create the vector with which to multiply and initialize it correctly.
|
|||
std::vector<ValueType> result(model.getNumberOfStates()); |
|||
storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one<ValueType>()); |
|||
|
|||
// Perform one single matrix-vector multiplication.
|
|||
STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available."); |
|||
this->linearEquationSolver->performMatrixVectorMultiplication(model.getTransitionMatrix(), result); |
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); |
|||
ExplicitQualitativeCheckResult& subResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*subResultPointer); |
|||
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeNextProbabilitiesHelper(subResult.getTruthValues()))); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const { |
|||
// We need to identify the states which have to be taken out of the matrix, i.e.
|
|||
// all states that have probability 0 and 1 of satisfying the until-formula.
|
|||
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(model, phiStates, psiStates); |
|||
storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); |
|||
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); |
|||
|
|||
// Perform some logging.
|
|||
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); |
|||
STORM_LOG_INFO("Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); |
|||
STORM_LOG_INFO("Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); |
|||
STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); |
|||
|
|||
// Create resulting vector.
|
|||
std::vector<ValueType> result(model.getNumberOfStates()); |
|||
|
|||
// Check whether we need to compute exact probabilities for some states.
|
|||
if (qualitative) { |
|||
// Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
|
|||
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, ValueType(0.5)); |
|||
} else { |
|||
// In this case we have have to compute the probabilities.
|
|||
|
|||
// We can eliminate the rows and columns from the original transition probability matrix.
|
|||
storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, true); |
|||
|
|||
// Converting the matrix from the fixpoint notation to the form needed for the equation
|
|||
// system. That is, we go from x = A*x + b to (I-A)x = b.
|
|||
submatrix.convertToEquationSystem(); |
|||
|
|||
// Initialize the x vector with 0.5 for each element. This is the initial guess for
|
|||
// the iterative solvers. It should be safe as for all 'maybe' states we know that the
|
|||
// probability is strictly larger than 0.
|
|||
std::vector<ValueType> x(maybeStates.getNumberOfSetBits(), ValueType(0.5)); |
|||
|
|||
// Prepare the right-hand side of the equation system. For entry i this corresponds to
|
|||
// the accumulated probability of going from state i to some 'yes' state.
|
|||
std::vector<ValueType> b = model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); |
|||
|
|||
// Now solve the created system of linear equations.
|
|||
STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available."); |
|||
this->linearEquationSolver->solveEquationSystem(submatrix, x, b); |
|||
|
|||
// Set values of resulting vector according to result.
|
|||
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x); |
|||
} |
|||
|
|||
// Set values of resulting vector that are known exactly.
|
|||
storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability0, storm::utility::zero<ValueType>()); |
|||
storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability1, storm::utility::one<ValueType>()); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); |
|||
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); |
|||
ExplicitQualitativeCheckResult& leftResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*leftResultPointer); |
|||
ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer); |
|||
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeUntilProbabilitiesHelper(leftResult.getTruthValues(), rightResult.getTruthValues(), qualitative))); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeCumulativeRewardsHelper(uint_fast64_t stepBound) const { |
|||
// Only compute the result if the model has at least one reward model.
|
|||
STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Compute the reward vector to add in each step based on the available reward models.
|
|||
std::vector<ValueType> totalRewardVector; |
|||
if (model.hasTransitionRewards()) { |
|||
totalRewardVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix()); |
|||
if (model.hasStateRewards()) { |
|||
storm::utility::vector::addVectorsInPlace(totalRewardVector, model.getStateRewardVector()); |
|||
} |
|||
} else { |
|||
totalRewardVector = std::vector<ValueType>(model.getStateRewardVector()); |
|||
} |
|||
|
|||
// Initialize result to either the state rewards of the model or the null vector.
|
|||
std::vector<ValueType> result; |
|||
if (model.hasStateRewards()) { |
|||
result = std::vector<ValueType>(model.getStateRewardVector()); |
|||
} else { |
|||
result.resize(model.getNumberOfStates()); |
|||
} |
|||
|
|||
// Perform the matrix vector multiplication as often as required by the formula bound.
|
|||
STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available."); |
|||
this->linearEquationSolver->performMatrixVectorMultiplication(model.getTransitionMatrix(), result, &totalRewardVector, stepBound); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeCumulativeRewardsHelper(rewardPathFormula.getStepBound()))); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeInstantaneousRewardsHelper(uint_fast64_t stepCount) const { |
|||
// Only compute the result if the model has a state-based reward model.
|
|||
STORM_LOG_THROW(model.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Initialize result to state rewards of the model.
|
|||
std::vector<ValueType> result(model.getStateRewardVector()); |
|||
|
|||
// Perform the matrix vector multiplication as often as required by the formula bound.
|
|||
STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available."); |
|||
this->linearEquationSolver->performMatrixVectorMultiplication(model.getTransitionMatrix(), result, nullptr, stepCount); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeInstantaneousRewardsHelper(rewardPathFormula.getStepCount()))); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const { |
|||
// Only compute the result if the model has at least one reward model.
|
|||
STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Determine which states have a reward of infinity by definition.
|
|||
storm::storage::BitVector trueStates(model.getNumberOfStates(), true); |
|||
storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(model.getBackwardTransitions(), trueStates, targetStates); |
|||
infinityStates.complement(); |
|||
storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates; |
|||
STORM_LOG_INFO("Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); |
|||
STORM_LOG_INFO("Found " << targetStates.getNumberOfSetBits() << " 'target' states."); |
|||
STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); |
|||
|
|||
// Create resulting vector.
|
|||
std::vector<ValueType> result(model.getNumberOfStates()); |
|||
|
|||
// Check whether we need to compute exact rewards for some states.
|
|||
if (qualitative) { |
|||
// Set the values for all maybe-states to 1 to indicate that their reward values
|
|||
// are neither 0 nor infinity.
|
|||
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, storm::utility::one<ValueType>()); |
|||
} else { |
|||
// In this case we have to compute the reward values for the remaining states.
|
|||
// We can eliminate the rows and columns from the original transition probability matrix.
|
|||
storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, true); |
|||
|
|||
// Converting the matrix from the fixpoint notation to the form needed for the equation
|
|||
// system. That is, we go from x = A*x + b to (I-A)x = b.
|
|||
submatrix.convertToEquationSystem(); |
|||
|
|||
// Initialize the x vector with 1 for each element. This is the initial guess for
|
|||
// the iterative solvers.
|
|||
std::vector<ValueType> x(submatrix.getColumnCount(), storm::utility::one<ValueType>()); |
|||
|
|||
// Prepare the right-hand side of the equation system.
|
|||
std::vector<ValueType> b(submatrix.getRowCount()); |
|||
if (model.hasTransitionRewards()) { |
|||
// If a transition-based reward model is available, we initialize the right-hand
|
|||
// side to the vector resulting from summing the rows of the pointwise product
|
|||
// of the transition probability matrix and the transition reward matrix.
|
|||
std::vector<ValueType> pointwiseProductRowSumVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix()); |
|||
storm::utility::vector::selectVectorValues(b, maybeStates, pointwiseProductRowSumVector); |
|||
|
|||
if (model.hasStateRewards()) { |
|||
// If a state-based reward model is also available, we need to add this vector
|
|||
// as well. As the state reward vector contains entries not just for the states
|
|||
// that we still consider (i.e. maybeStates), we need to extract these values
|
|||
// first.
|
|||
std::vector<ValueType> subStateRewards(b.size()); |
|||
storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, model.getStateRewardVector()); |
|||
storm::utility::vector::addVectorsInPlace(b, subStateRewards); |
|||
} |
|||
} else { |
|||
// If only a state-based reward model is available, we take this vector as the
|
|||
// right-hand side. As the state reward vector contains entries not just for the
|
|||
// states that we still consider (i.e. maybeStates), we need to extract these values
|
|||
// first.
|
|||
storm::utility::vector::selectVectorValues(b, maybeStates, model.getStateRewardVector()); |
|||
} |
|||
|
|||
// Now solve the resulting equation system.
|
|||
STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available."); |
|||
this->linearEquationSolver->solveEquationSystem(submatrix, x, b); |
|||
|
|||
// Set values of resulting vector according to result.
|
|||
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x); |
|||
} |
|||
|
|||
// Set values of resulting vector that are known exactly.
|
|||
storm::utility::vector::setVectorValues(result, targetStates, storm::utility::zero<ValueType>()); |
|||
storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity<ValueType>()); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula()); |
|||
ExplicitQualitativeCheckResult& subResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*subResultPointer); |
|||
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeReachabilityRewardsHelper(subResult.getTruthValues(), qualitative))); |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<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> SparseDtmcPrctlModelChecker<ValueType>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { |
|||
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel()))); |
|||
} |
|||
|
|||
template class SparseDtmcPrctlModelChecker<double>; |
|||
} |
|||
} |
|||
} |
|||
@ -1,535 +1,50 @@ |
|||
/* |
|||
* SparseDtmcPrctlModelChecker.h |
|||
* |
|||
* Created on: 22.10.2012 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
#ifndef STORM_MODELCHECKER_PRCTL_SPARSEDTMCPRCTLMODELCHECKER_H_ |
|||
#define STORM_MODELCHECKER_PRCTL_SPARSEDTMCPRCTLMODELCHECKER_H_ |
|||
|
|||
#include "src/modelchecker/prctl/AbstractModelChecker.h" |
|||
#include "src/modelchecker/AbstractModelChecker.h" |
|||
#include "src/models/Dtmc.h" |
|||
#include "src/solver/LinearEquationSolver.h" |
|||
#include "src/utility/solver.h" |
|||
#include "src/utility/vector.h" |
|||
#include "src/utility/graph.h" |
|||
|
|||
#include <vector> |
|||
#include "src/solver/LinearEquationSolver.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace prctl { |
|||
|
|||
/*! |
|||
* @brief |
|||
* Interface for all model checkers that can verify PRCTL formulae over DTMCs represented as a sparse matrix. |
|||
*/ |
|||
template<class Type> |
|||
class SparseDtmcPrctlModelChecker : public AbstractModelChecker<Type> { |
|||
|
|||
public: |
|||
/*! |
|||
* Constructs a SparseDtmcPrctlModelChecker with the given model. |
|||
* |
|||
* @param model The DTMC to be checked. |
|||
*/ |
|||
explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<Type> const& model, std::unique_ptr<storm::solver::LinearEquationSolver<Type>>&& linearEquationSolver) : AbstractModelChecker<Type>(model), linearEquationSolver(std::move(linearEquationSolver)) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<Type> const& model) : AbstractModelChecker<Type>(model), linearEquationSolver(storm::utility::solver::getLinearEquationSolver<Type>()) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Copy constructs a SparseDtmcPrctlModelChecker from the given model checker. In particular, this means that the newly |
|||
* constructed model checker will have the model of the given model checker as its associated model. |
|||
*/ |
|||
explicit SparseDtmcPrctlModelChecker(storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<Type> const& modelChecker) : AbstractModelChecker<Type>(modelChecker), linearEquationSolver(modelChecker.linearEquationSolver->clone()) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Virtual destructor. Needs to be virtual, because this class has virtual methods. |
|||
*/ |
|||
virtual ~SparseDtmcPrctlModelChecker() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Returns a constant reference to the DTMC associated with this model checker. |
|||
* @returns A constant reference to the DTMC associated with this model checker. |
|||
*/ |
|||
storm::models::Dtmc<Type> const& getModel() const { |
|||
return AbstractModelChecker<Type>::template getModel<storm::models::Dtmc<Type>>(); |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is a bounded-until formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
|||
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
|||
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
|||
* bounds 0 and 1. |
|||
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
|||
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
|||
*/ |
|||
virtual std::vector<Type> checkBoundedUntil(storm::properties::prctl::BoundedUntil<Type> const& formula, bool qualitative) const { |
|||
return this->checkBoundedUntil(formula.getLeft()->check(*this), formula.getRight()->check(*this), formula.getBound(), qualitative); |
|||
} |
|||
|
|||
/*! |
|||
* Computes the probability to satisfy phi until psi inside a given bound for each state in the model. |
|||
* |
|||
* @param phiStates A bit vector indicating which states satisfy phi. |
|||
* @param psiStates A bit vector indicating which states satisfy psi. |
|||
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
|||
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
|||
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
|||
* bounds 0 and 1. |
|||
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
|||
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
|||
*/ |
|||
virtual std::vector<Type> checkBoundedUntil(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, bool qualitative) const { |
|||
std::vector<Type> result(this->getModel().getNumberOfStates()); |
|||
|
|||
// If we identify the states that have probability 0 of reaching the target states, we can exclude them in the |
|||
// further analysis. |
|||
storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel().getBackwardTransitions(), phiStates, psiStates, true, stepBound); |
|||
LOG4CPLUS_INFO(logger, "Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states."); |
|||
|
|||
// Check if we already know the result (i.e. probability 0) for all initial states and |
|||
// don't compute anything in this case. |
|||
if (this->getModel().getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) { |
|||
LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step." |
|||
<< " No exact probabilities were computed."); |
|||
// Set the values for all maybe-states to 0.5 to indicate that their probability values are not 0 (and |
|||
// not necessarily 1). |
|||
storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, Type(0.5)); |
|||
} else { |
|||
// In this case we have have to compute the probabilities. |
|||
|
|||
// We can eliminate the rows and columns from the original transition probability matrix that have probability 0. |
|||
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, true); |
|||
|
|||
// Compute the new set of target states in the reduced system. |
|||
storm::storage::BitVector rightStatesInReducedSystem = psiStates % statesWithProbabilityGreater0; |
|||
|
|||
// Make all rows absorbing that satisfy the second sub-formula. |
|||
submatrix.makeRowsAbsorbing(rightStatesInReducedSystem); |
|||
|
|||
// Create the vector with which to multiply. |
|||
std::vector<Type> subresult(statesWithProbabilityGreater0.getNumberOfSetBits()); |
|||
storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constantOne<Type>()); |
|||
|
|||
// Perform the matrix vector multiplication as often as required by the formula bound. |
|||
if (linearEquationSolver != nullptr) { |
|||
this->linearEquationSolver->performMatrixVectorMultiplication(submatrix, subresult, nullptr, stepBound); |
|||
} else { |
|||
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; |
|||
} |
|||
|
|||
// Set the values of the resulting vector accordingly. |
|||
storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult); |
|||
storm::utility::vector::setVectorValues<Type>(result, ~statesWithProbabilityGreater0, storm::utility::constantZero<Type>()); |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is a next formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
|||
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
|||
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
|||
* bounds 0 and 1. |
|||
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
|||
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
|||
*/ |
|||
virtual std::vector<Type> checkNext(storm::properties::prctl::Next<Type> const& formula, bool qualitative) const { |
|||
// First, we need to compute the states that satisfy the child formula of the next-formula. |
|||
storm::storage::BitVector nextStates = formula.getChild()->check(*this); |
|||
|
|||
// Create the vector with which to multiply and initialize it correctly. |
|||
std::vector<Type> result(this->getModel().getNumberOfStates()); |
|||
storm::utility::vector::setVectorValues(result, nextStates, storm::utility::constantOne<Type>()); |
|||
|
|||
// Perform one single matrix-vector multiplication. |
|||
if (linearEquationSolver != nullptr) { |
|||
this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result); |
|||
} else { |
|||
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is a bounded-eventually formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
|||
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
|||
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
|||
* bounds 0 and 1. |
|||
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
|||
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
|||
*/ |
|||
virtual std::vector<Type> checkBoundedEventually(storm::properties::prctl::BoundedEventually<Type> const& formula, bool qualitative) const { |
|||
return this->checkBoundedUntil(storm::storage::BitVector(this->getModel().getNumberOfStates(), true), formula.getChild()->check(*this), formula.getBound(), qualitative); |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is an eventually formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
|||
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
|||
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
|||
* bounds 0 and 1. |
|||
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
|||
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
|||
*/ |
|||
virtual std::vector<Type> checkEventually(storm::properties::prctl::Eventually<Type> const& formula, bool qualitative) const { |
|||
// Create equivalent temporary until formula and check it. |
|||
storm::properties::prctl::Until<Type> temporaryUntilFormula(std::shared_ptr<storm::properties::prctl::Ap<Type>>(new storm::properties::prctl::Ap<Type>("true")), formula.getChild()); |
|||
return this->checkUntil(temporaryUntilFormula, qualitative); |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is a globally formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
|||
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
|||
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
|||
* bounds 0 and 1. |
|||
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
|||
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
|||
*/ |
|||
virtual std::vector<Type> checkGlobally(storm::properties::prctl::Globally<Type> const& formula, bool qualitative) const { |
|||
// Create "equivalent" (equivalent up to negation) temporary eventually formula and check it. |
|||
storm::properties::prctl::Eventually<Type> temporaryEventuallyFormula(std::shared_ptr<storm::properties::prctl::Not<Type>>(new storm::properties::prctl::Not<Type>(formula.getChild()))); |
|||
std::vector<Type> result = this->checkEventually(temporaryEventuallyFormula, qualitative); |
|||
|
|||
// Now subtract the resulting vector from the constant one vector to obtain final result. |
|||
storm::utility::vector::subtractFromConstantOneVector(result); |
|||
return result; |
|||
} |
|||
|
|||
|
|||
/*! |
|||
* Check the given formula that is an until formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
|||
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
|||
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
|||
* bounds 0 and 1. |
|||
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
|||
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
|||
*/ |
|||
virtual std::vector<Type> checkUntil(storm::properties::prctl::Until<Type> const& formula, bool qualitative) const { |
|||
return this->checkUntil(formula.getLeft()->check(*this), formula.getRight()->check(*this), qualitative); |
|||
} |
|||
|
|||
/*! |
|||
* Computes the probability to satisfy phi until psi for each state in the model. |
|||
* |
|||
* @param phiStates A bit vector indicating which states satisfy phi. |
|||
* @param psiStates A bit vector indicating which states satisfy psi. |
|||
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
|||
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
|||
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
|||
* bounds 0 and 1. |
|||
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
|||
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
|||
*/ |
|||
virtual std::vector<Type> checkUntil(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const { |
|||
|
|||
// We need to identify the states which have to be taken out of the matrix, i.e. |
|||
// all states that have probability 0 and 1 of satisfying the until-formula. |
|||
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), phiStates, psiStates); |
|||
storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); |
|||
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); |
|||
|
|||
// Perform some logging. |
|||
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); |
|||
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); |
|||
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); |
|||
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); |
|||
|
|||
// Create resulting vector. |
|||
std::vector<Type> result(this->getModel().getNumberOfStates()); |
|||
|
|||
// Check whether we need to compute exact probabilities for some states. |
|||
if (this->getModel().getInitialStates().isDisjointFrom(maybeStates) || qualitative) { |
|||
if (qualitative) { |
|||
LOG4CPLUS_INFO(logger, "The formula was checked qualitatively. No exact probabilities were computed."); |
|||
} else { |
|||
LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step." |
|||
<< " No exact probabilities were computed."); |
|||
} |
|||
// Set the values for all maybe-states to 0.5 to indicate that their probability values |
|||
// are neither 0 nor 1. |
|||
storm::utility::vector::setVectorValues<Type>(result, maybeStates, Type(0.5)); |
|||
} else { |
|||
// In this case we have have to compute the probabilities. |
|||
|
|||
// We can eliminate the rows and columns from the original transition probability matrix. |
|||
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, true); |
|||
// Converting the matrix from the fixpoint notation to the form needed for the equation |
|||
// system. That is, we go from x = A*x + b to (I-A)x = b. |
|||
submatrix.convertToEquationSystem(); |
|||
|
|||
// Initialize the x vector with 0.5 for each element. This is the initial guess for |
|||
// the iterative solvers. It should be safe as for all 'maybe' states we know that the |
|||
// probability is strictly larger than 0. |
|||
std::vector<Type> x(maybeStates.getNumberOfSetBits(), Type(0.5)); |
|||
|
|||
// Prepare the right-hand side of the equation system. For entry i this corresponds to |
|||
// the accumulated probability of going from state i to some 'yes' state. |
|||
std::vector<Type> b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); |
|||
|
|||
// Now solve the created system of linear equations. |
|||
if (linearEquationSolver != nullptr) { |
|||
this->linearEquationSolver->solveEquationSystem(submatrix, x, b); |
|||
} else { |
|||
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; |
|||
} |
|||
|
|||
// Set values of resulting vector according to result. |
|||
storm::utility::vector::setVectorValues<Type>(result, maybeStates, x); |
|||
} |
|||
|
|||
// Set values of resulting vector that are known exactly. |
|||
storm::utility::vector::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constantZero<Type>()); |
|||
storm::utility::vector::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constantOne<Type>()); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is an instantaneous reward formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
|||
* results are only compared against the bound 0. If set to true, this will most likely results that are only |
|||
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
|||
* bound 0. |
|||
* @returns The reward values for the given formula for every state of the model associated with this model |
|||
* checker. If the qualitative flag is set, exact values might not be computed. |
|||
*/ |
|||
virtual std::vector<Type> checkInstantaneousReward(storm::properties::prctl::InstantaneousReward<Type> const& formula, bool qualitative) const { |
|||
// Only compute the result if the model has a state-based reward model. |
|||
if (!this->getModel().hasStateRewards()) { |
|||
LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); |
|||
throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula."; |
|||
} |
|||
|
|||
// Initialize result to state rewards of the model. |
|||
std::vector<Type> result(this->getModel().getStateRewardVector()); |
|||
|
|||
// Perform the actual matrix-vector multiplication as long as the bound of the formula is met. |
|||
if (linearEquationSolver != nullptr) { |
|||
this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result, nullptr, formula.getBound()); |
|||
} else { |
|||
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Check the given formula that is a cumulative reward formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
|||
* results are only compared against the bound 0. If set to true, this will most likely results that are only |
|||
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
|||
* bound 0. |
|||
* @returns The reward values for the given formula for every state of the model associated with this model |
|||
* checker. If the qualitative flag is set, exact values might not be computed. |
|||
*/ |
|||
virtual std::vector<Type> checkCumulativeReward(storm::properties::prctl::CumulativeReward<Type> const& formula, bool qualitative) const { |
|||
// Only compute the result if the model has at least one reward model. |
|||
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { |
|||
LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); |
|||
throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; |
|||
} |
|||
|
|||
// Compute the reward vector to add in each step based on the available reward models. |
|||
std::vector<Type> totalRewardVector; |
|||
if (this->getModel().hasTransitionRewards()) { |
|||
totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix()); |
|||
if (this->getModel().hasStateRewards()) { |
|||
storm::utility::vector::addVectorsInPlace(totalRewardVector, this->getModel().getStateRewardVector()); |
|||
} |
|||
} else { |
|||
totalRewardVector = std::vector<Type>(this->getModel().getStateRewardVector()); |
|||
} |
|||
|
|||
// Initialize result to either the state rewards of the model or the null vector. |
|||
std::vector<Type> result; |
|||
if (this->getModel().hasStateRewards()) { |
|||
result = std::vector<Type>(this->getModel().getStateRewardVector()); |
|||
} else { |
|||
result.resize(this->getModel().getNumberOfStates()); |
|||
} |
|||
|
|||
// Perform the actual matrix-vector multiplication as long as the bound of the formula is met. |
|||
if (linearEquationSolver != nullptr) { |
|||
this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result, &totalRewardVector, static_cast<uint_fast64_t>(formula.getBound())); |
|||
} else { |
|||
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula that is a reachability reward formula. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
|||
* results are only compared against the bound 0. If set to true, this will most likely results that are only |
|||
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
|||
* bound 0. |
|||
* @returns The reward values for the given formula for every state of the model associated with this model |
|||
* checker. If the qualitative flag is set, exact values might not be computed. |
|||
*/ |
|||
virtual std::vector<Type> checkReachabilityReward(storm::properties::prctl::ReachabilityReward<Type> const& formula, bool qualitative) const { |
|||
// Only compute the result if the model has at least one reward model. |
|||
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { |
|||
LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); |
|||
throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; |
|||
} |
|||
|
|||
// Determine the states for which the target predicate holds. |
|||
storm::storage::BitVector targetStates = formula.getChild()->check(*this); |
|||
|
|||
// Determine which states have a reward of infinity by definition. |
|||
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); |
|||
storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel().getBackwardTransitions(), trueStates, targetStates); |
|||
infinityStates.complement(); |
|||
storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates; |
|||
LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); |
|||
LOG4CPLUS_INFO(logger, "Found " << targetStates.getNumberOfSetBits() << " 'target' states."); |
|||
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); |
|||
|
|||
// Create resulting vector. |
|||
std::vector<Type> result(this->getModel().getNumberOfStates()); |
|||
|
|||
// Check whether we need to compute exact rewards for some states. |
|||
if (this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { |
|||
LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step." |
|||
<< " No exact rewards were computed."); |
|||
// Set the values for all maybe-states to 1 to indicate that their reward values |
|||
// are neither 0 nor infinity. |
|||
storm::utility::vector::setVectorValues<Type>(result, maybeStates, storm::utility::constantOne<Type>()); |
|||
} else { |
|||
// In this case we have to compute the reward values for the remaining states. |
|||
// We can eliminate the rows and columns from the original transition probability matrix. |
|||
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, true); |
|||
// Converting the matrix from the fixpoint notation to the form needed for the equation |
|||
// system. That is, we go from x = A*x + b to (I-A)x = b. |
|||
submatrix.convertToEquationSystem(); |
|||
|
|||
// Initialize the x vector with 1 for each element. This is the initial guess for |
|||
// the iterative solvers. |
|||
std::vector<Type> x(submatrix.getColumnCount(), storm::utility::constantOne<Type>()); |
|||
|
|||
// Prepare the right-hand side of the equation system. |
|||
std::vector<Type> b(submatrix.getRowCount()); |
|||
if (this->getModel().hasTransitionRewards()) { |
|||
// If a transition-based reward model is available, we initialize the right-hand |
|||
// side to the vector resulting from summing the rows of the pointwise product |
|||
// of the transition probability matrix and the transition reward matrix. |
|||
std::vector<Type> pointwiseProductRowSumVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix()); |
|||
storm::utility::vector::selectVectorValues(b, maybeStates, pointwiseProductRowSumVector); |
|||
namespace modelchecker { |
|||
namespace prctl { |
|||
|
|||
template<class ValueType> |
|||
class SparseDtmcPrctlModelChecker : public AbstractModelChecker { |
|||
public: |
|||
explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model); |
|||
explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model, std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>&& linearEquationSolver); |
|||
|
|||
if (this->getModel().hasStateRewards()) { |
|||
// If a state-based reward model is also available, we need to add this vector |
|||
// as well. As the state reward vector contains entries not just for the states |
|||
// that we still consider (i.e. maybeStates), we need to extract these values |
|||
// first. |
|||
std::vector<Type> subStateRewards(b.size()); |
|||
storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, this->getModel().getStateRewardVector()); |
|||
storm::utility::vector::addVectorsInPlace(b, subStateRewards); |
|||
} |
|||
} else { |
|||
// If only a state-based reward model is available, we take this vector as the |
|||
// right-hand side. As the state reward vector contains entries not just for the |
|||
// states that we still consider (i.e. maybeStates), we need to extract these values |
|||
// first. |
|||
storm::utility::vector::selectVectorValues(b, maybeStates, this->getModel().getStateRewardVector()); |
|||
} |
|||
|
|||
// Now solve the resulting equation system. |
|||
if (linearEquationSolver != nullptr) { |
|||
this->linearEquationSolver->solveEquationSystem(submatrix, x, b); |
|||
} else { |
|||
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; |
|||
} |
|||
|
|||
// Set values of resulting vector according to result. |
|||
storm::utility::vector::setVectorValues<Type>(result, maybeStates, x); |
|||
} |
|||
|
|||
// Set values of resulting vector that are known exactly. |
|||
storm::utility::vector::setVectorValues(result, targetStates, storm::utility::constantZero<Type>()); |
|||
storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constantInfinity<Type>()); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula. |
|||
* @note This methods overrides the method of the base class to give an additional warning that declaring that minimal or maximal probabilities |
|||
* should be computed for the formula makes no sense in the context of a deterministic model. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param optOperator True iff minimum probabilities/rewards are to be computed. |
|||
* @returns The probabilities to satisfy the formula or the rewards accumulated by it, represented by a vector. |
|||
*/ |
|||
virtual std::vector<Type> checkOptimizingOperator(storm::properties::prctl::AbstractPathFormula<Type> const & formula, bool optOperator) const override { |
|||
|
|||
LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models."); |
|||
|
|||
std::vector<Type> result = formula.check(*this, false); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given formula and determines whether minimum or maximum probabilities or rewards are to be computed for the formula. |
|||
* @note This methods overrides the method of the base class to give an additional warning that declaring that minimal or maximal probabilities |
|||
* should be computed for the formula makes no sense in the context of a deterministic model. |
|||
* |
|||
* @param formula The formula to check. |
|||
* @param optOperator True iff minimum probabilities/rewards are to be computed. |
|||
* @returns The set of states satisfying the formula represented by a bit vector. |
|||
*/ |
|||
virtual storm::storage::BitVector checkOptimizingOperator(storm::properties::prctl::AbstractStateFormula<Type> const & formula, bool optOperator) const override { |
|||
|
|||
LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models."); |
|||
|
|||
storm::storage::BitVector result = formula.check(*this); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
private: |
|||
// An object that is used for solving linear equations and performing matrix-vector multiplication. |
|||
std::unique_ptr<storm::solver::LinearEquationSolver<Type>> linearEquationSolver; |
|||
}; |
|||
|
|||
} // namespace prctl |
|||
} // namespace modelchecker |
|||
// The implemented methods of the AbstractModelChecker interface. |
|||
virtual bool canHandle(storm::logic::Formula const& formula) const override; |
|||
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override; |
|||
virtual std::unique_ptr<CheckResult> computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) 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> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override; |
|||
virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, 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> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override; |
|||
virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override; |
|||
|
|||
// The methods that perform the actual checking. |
|||
std::vector<ValueType> computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound); |
|||
std::vector<ValueType> computeNextProbabilitiesHelper(storm::storage::BitVector const& nextStates); |
|||
std::vector<ValueType> computeUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const; |
|||
std::vector<ValueType> computeInstantaneousRewardsHelper(uint_fast64_t stepCount) const; |
|||
std::vector<ValueType> computeCumulativeRewardsHelper(uint_fast64_t stepBound) const; |
|||
std::vector<ValueType> computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const; |
|||
|
|||
private: |
|||
// The model this model checker is supposed to analyze. |
|||
storm::models::Dtmc<ValueType> const& model; |
|||
|
|||
// An object that is used for solving linear equations and performing matrix-vector multiplication. |
|||
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> linearEquationSolver; |
|||
}; |
|||
|
|||
} // namespace prctl |
|||
} // namespace modelchecker |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_PRCTL_SPARSEDTMCPRCTLMODELCHECKER_H_ */ |
|||
@ -1,167 +0,0 @@ |
|||
/*
|
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "src/settings/SettingsManager.h"
|
|||
#include "src/modelchecker/EigenDtmcPrctlModelChecker.h"
|
|||
#include "src/parser/AutoParser.h"
|
|||
|
|||
TEST(EigenDtmcPrctlModelCheckerTest, Die) { |
|||
storm::settings::Settings* s = storm::settings::Settings::getInstance(); |
|||
storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true); |
|||
ASSERT_TRUE(s->isSet("fixDeadlocks")); |
|||
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/die/die.coin_flips.trans.rew"); |
|||
|
|||
ASSERT_EQ(parser.getType(), storm::models::DTMC); |
|||
|
|||
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 14); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28); |
|||
|
|||
storm::modelChecker::EigenDtmcPrctlModelChecker<double> mc(*dtmc); |
|||
|
|||
storm::properties::Ap<double>* apFormula = new storm::properties::Ap<double>("one"); |
|||
storm::properties::Eventually<double>* eventuallyFormula = new storm::properties::Eventually<double>(apFormula); |
|||
storm::properties::ProbabilisticNoBoundOperator<double>* probFormula = new storm::properties::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
std::vector<double>* result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::properties::Ap<double>("two"); |
|||
eventuallyFormula = new storm::properties::Eventually<double>(apFormula); |
|||
probFormula = new storm::properties::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::properties::Ap<double>("three"); |
|||
eventuallyFormula = new storm::properties::Eventually<double>(apFormula); |
|||
probFormula = new storm::properties::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
storm::properties::Ap<double>* done = new storm::properties::Ap<double>("done"); |
|||
storm::properties::ReachabilityReward<double>* reachabilityRewardFormula = new storm::properties::ReachabilityReward<double>(done); |
|||
storm::properties::RewardNoBoundOperator<double>* rewardFormula = new storm::properties::RewardNoBoundOperator<double>(reachabilityRewardFormula); |
|||
|
|||
result = rewardFormula->check(mc); |
|||
|
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - ((double)11/3)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
} |
|||
|
|||
TEST(EigenDtmcPrctlModelCheckerTest, Crowds) { |
|||
storm::settings::Settings* s = storm::settings::Settings::getInstance(); |
|||
storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true); |
|||
ASSERT_TRUE(s->isSet("fixDeadlocks")); |
|||
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/crowds/crowds5_5.lab", "", ""); |
|||
|
|||
ASSERT_EQ(parser.getType(), storm::models::DTMC); |
|||
|
|||
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 8608); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 22461); |
|||
|
|||
storm::modelChecker::EigenDtmcPrctlModelChecker<double> mc(*dtmc); |
|||
|
|||
storm::properties::Ap<double>* apFormula = new storm::properties::Ap<double>("observe0Greater1"); |
|||
storm::properties::Eventually<double>* eventuallyFormula = new storm::properties::Eventually<double>(apFormula); |
|||
storm::properties::ProbabilisticNoBoundOperator<double>* probFormula = new storm::properties::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
std::vector<double>* result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - 0.3328800375801578281), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::properties::Ap<double>("observeIGreater1"); |
|||
eventuallyFormula = new storm::properties::Eventually<double>(apFormula); |
|||
probFormula = new storm::properties::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - 0.1522173670950556501), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::properties::Ap<double>("observeOnlyTrueSender"); |
|||
eventuallyFormula = new storm::properties::Eventually<double>(apFormula); |
|||
probFormula = new storm::properties::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - 0.32153724292835045), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
} |
|||
|
|||
TEST(EigenDtmcPrctlModelCheckerTest, SynchronousLeader) { |
|||
storm::settings::Settings* s = storm::settings::Settings::getInstance(); |
|||
storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true); |
|||
ASSERT_TRUE(s->isSet("fixDeadlocks")); |
|||
storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/synchronous_leader/leader4_8.pick.trans.rew"); |
|||
|
|||
ASSERT_EQ(parser.getType(), storm::models::DTMC); |
|||
|
|||
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>(); |
|||
|
|||
ASSERT_EQ(dtmc->getNumberOfStates(), 12401); |
|||
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28895); |
|||
|
|||
storm::modelChecker::EigenDtmcPrctlModelChecker<double> mc(*dtmc); |
|||
|
|||
storm::properties::Ap<double>* apFormula = new storm::properties::Ap<double>("elected"); |
|||
storm::properties::Eventually<double>* eventuallyFormula = new storm::properties::Eventually<double>(apFormula); |
|||
storm::properties::ProbabilisticNoBoundOperator<double>* probFormula = new storm::properties::ProbabilisticNoBoundOperator<double>(eventuallyFormula); |
|||
|
|||
std::vector<double>* result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::properties::Ap<double>("elected"); |
|||
storm::properties::BoundedUntil<double>* boundedUntilFormula = new storm::properties::BoundedUntil<double>(new storm::properties::Ap<double>("true"), apFormula, 20); |
|||
probFormula = new storm::properties::ProbabilisticNoBoundOperator<double>(boundedUntilFormula); |
|||
|
|||
result = probFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - 0.9999965911265462636), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); |
|||
|
|||
delete probFormula; |
|||
delete result; |
|||
|
|||
apFormula = new storm::properties::Ap<double>("elected"); |
|||
storm::properties::ReachabilityReward<double>* reachabilityRewardFormula = new storm::properties::ReachabilityReward<double>(apFormula); |
|||
storm::properties::RewardNoBoundOperator<double>* rewardFormula = new storm::properties::RewardNoBoundOperator<double>(reachabilityRewardFormula); |
|||
|
|||
result = rewardFormula->check(mc); |
|||
|
|||
ASSERT_LT(std::abs((*result)[1] - 1.0448979591835938496), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); |
|||
|
|||
delete rewardFormula; |
|||
delete result; |
|||
} |
|||
*/ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue