dehnert
10 years ago
31 changed files with 1120 additions and 121 deletions
-
73src/builder/DdPrismModelBuilder.cpp
-
11src/builder/DdPrismModelBuilder.h
-
2src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
-
91src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
-
38src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h
-
4src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
-
11src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
-
44src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
-
49src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
-
201src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
-
40src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h
-
16src/models/symbolic/StandardRewardModel.cpp
-
12src/models/symbolic/StandardRewardModel.h
-
10src/parser/DeterministicModelParser.cpp
-
3src/settings/modules/GmmxxEquationSolverSettings.cpp
-
3src/settings/modules/NativeEquationSolverSettings.cpp
-
2src/solver/SymbolicLinearEquationSolver.h
-
96src/solver/SymbolicMinMaxLinearEquationSolver.cpp
-
126src/solver/SymbolicMinMaxLinearEquationSolver.h
-
3src/storage/dd/CuddAdd.cpp
-
67src/storage/dd/CuddOdd.cpp
-
22src/storage/dd/CuddOdd.h
-
2src/storage/prism/RewardModel.cpp
-
2src/storage/prism/Update.cpp
-
47src/utility/cli.h
-
26src/utility/graph.h
-
6src/utility/solver.cpp
-
8src/utility/solver.h
-
16test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
-
18test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
-
192test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
@ -0,0 +1,91 @@ |
|||
#include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
|
|||
|
|||
#include "src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h"
|
|||
|
|||
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
|
|||
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/utility/graph.h"
|
|||
|
|||
#include "src/settings/modules/GeneralSettings.h"
|
|||
|
|||
#include "src/exceptions/InvalidStateException.h"
|
|||
#include "src/exceptions/InvalidPropertyException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
SymbolicMdpPrctlModelChecker<DdType, ValueType>::SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType> const& model, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker<DdType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
SymbolicMdpPrctlModelChecker<DdType, ValueType>::SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType> const& model) : SymbolicPropositionalModelChecker<DdType>(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>()) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
bool SymbolicMdpPrctlModelChecker<DdType, ValueType>::canHandle(storm::logic::Formula const& formula) const { |
|||
return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula(); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); |
|||
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); |
|||
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); |
|||
SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>(); |
|||
SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>(); |
|||
return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); |
|||
std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula()); |
|||
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); |
|||
return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeNextProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); |
|||
STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); |
|||
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula()); |
|||
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); |
|||
SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>(); |
|||
SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>(); |
|||
return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional<std::string> const& rewardModelName, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); |
|||
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); |
|||
return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeCumulativeRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional<std::string> const& rewardModelName, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); |
|||
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); |
|||
return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeInstantaneousRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional<std::string> const& rewardModelName, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) { |
|||
STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); |
|||
std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula()); |
|||
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>(); |
|||
return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
storm::models::symbolic::Mdp<DdType> const& SymbolicMdpPrctlModelChecker<DdType, ValueType>::getModel() const { |
|||
return this->template getModelAs<storm::models::symbolic::Mdp<DdType>>(); |
|||
} |
|||
|
|||
template class SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double>; |
|||
} |
|||
} |
|||
@ -0,0 +1,38 @@ |
|||
#ifndef STORM_MODELCHECKER_SYMBOLICMDPPRCTLMODELCHECKER_H_ |
|||
#define STORM_MODELCHECKER_SYMBOLICMDPPRCTLMODELCHECKER_H_ |
|||
|
|||
#include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h" |
|||
|
|||
#include "src/models/symbolic/Mdp.h" |
|||
|
|||
#include "src/utility/solver.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
class SymbolicMdpPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType> { |
|||
public: |
|||
explicit SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType> const& model); |
|||
explicit SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp<DdType> const& model, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory); |
|||
|
|||
// 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, boost::optional<std::string> const& rewardModelName = boost::optional<std::string>(), 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, boost::optional<std::string> const& rewardModelName = boost::optional<std::string>(), 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, boost::optional<std::string> const& rewardModelName = boost::optional<std::string>(), bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override; |
|||
|
|||
protected: |
|||
storm::models::symbolic::Mdp<DdType> const& getModel() const override; |
|||
|
|||
private: |
|||
// An object that is used for retrieving linear equation solvers. |
|||
std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>> linearEquationSolverFactory; |
|||
}; |
|||
|
|||
} // namespace modelchecker |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_SYMBOLICMDPPRCTLMODELCHECKER_H_ */ |
|||
@ -0,0 +1,201 @@ |
|||
#include "src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h"
|
|||
|
|||
#include "src/storage/dd/CuddDdManager.h"
|
|||
#include "src/storage/dd/CuddAdd.h"
|
|||
#include "src/storage/dd/CuddBdd.h"
|
|||
#include "src/storage/dd/CuddOdd.h"
|
|||
|
|||
#include "src/utility/graph.h"
|
|||
|
|||
#include "src/models/symbolic/StandardRewardModel.h"
|
|||
|
|||
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
|
|||
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
|
|||
|
|||
#include "src/exceptions/InvalidPropertyException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) { |
|||
// 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::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01; |
|||
if (minimize) { |
|||
statesWithProbability01 = storm::utility::graph::performProb01Min(model, phiStates, psiStates); |
|||
} else { |
|||
statesWithProbability01 = storm::utility::graph::performProb01Max(model, phiStates, psiStates); |
|||
} |
|||
|
|||
storm::dd::Bdd<DdType> maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates(); |
|||
|
|||
// Perform some logging.
|
|||
STORM_LOG_INFO("Found " << statesWithProbability01.first.getNonZeroCount() << " 'no' states."); |
|||
STORM_LOG_INFO("Found " << statesWithProbability01.second.getNonZeroCount() << " 'yes' states."); |
|||
STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states."); |
|||
|
|||
// 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.
|
|||
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), statesWithProbability01.second.toAdd() + maybeStates.toAdd() * model.getManager().getConstant(0.5))); |
|||
} else { |
|||
// If there are maybe states, we need to solve an equation system.
|
|||
if (!maybeStates.isZero()) { |
|||
// Create the matrix and the vector for the equation system.
|
|||
storm::dd::Add<DdType> maybeStatesAdd = maybeStates.toAdd(); |
|||
|
|||
// Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
|
|||
// non-maybe states in the matrix.
|
|||
storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd; |
|||
|
|||
// Then compute the vector that contains the one-step probabilities to a state with probability 1 for all
|
|||
// maybe states.
|
|||
storm::dd::Add<DdType> prob1StatesAsColumn = statesWithProbability01.second.toAdd(); |
|||
prob1StatesAsColumn = prob1StatesAsColumn.swapVariables(model.getRowColumnMetaVariablePairs()); |
|||
storm::dd::Add<DdType> subvector = submatrix * prob1StatesAsColumn; |
|||
subvector = subvector.sumAbstract(model.getColumnVariables()); |
|||
|
|||
// Finally cut away all columns targeting non-maybe states.
|
|||
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); |
|||
|
|||
// Now solve the resulting equation system.
|
|||
std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); |
|||
storm::dd::Add<DdType> result = solver->solveEquationSystem(minimize, model.getManager().getAddZero(), subvector); |
|||
|
|||
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), statesWithProbability01.second.toAdd() + result)); |
|||
} else { |
|||
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), statesWithProbability01.second.toAdd())); |
|||
} |
|||
} |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeNextProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates) { |
|||
storm::dd::Add<DdType> result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd(); |
|||
return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), result.sumAbstract(model.getColumnVariables()))); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) { |
|||
// We need to identify the states which have to be taken out of the matrix, i.e. all states that have
|
|||
// probability 0 or 1 of satisfying the until-formula.
|
|||
storm::dd::Bdd<DdType> statesWithProbabilityGreater0; |
|||
if (minimize) { |
|||
statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(model, transitionMatrix.notZero(), phiStates, psiStates); |
|||
} else { |
|||
statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(model, transitionMatrix.notZero(), phiStates, psiStates); |
|||
} |
|||
storm::dd::Bdd<DdType> maybeStates = statesWithProbabilityGreater0 && !psiStates && model.getReachableStates(); |
|||
|
|||
// If there are maybe states, we need to perform matrix-vector multiplications.
|
|||
if (!maybeStates.isZero()) { |
|||
// Create the matrix and the vector for the equation system.
|
|||
storm::dd::Add<DdType> maybeStatesAdd = maybeStates.toAdd(); |
|||
|
|||
// Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
|
|||
// non-maybe states in the matrix.
|
|||
storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd; |
|||
|
|||
// Then compute the vector that contains the one-step probabilities to a state with probability 1 for all
|
|||
// maybe states.
|
|||
storm::dd::Add<DdType> prob1StatesAsColumn = psiStates.toAdd().swapVariables(model.getRowColumnMetaVariablePairs()); |
|||
storm::dd::Add<DdType> subvector = (submatrix * prob1StatesAsColumn).sumAbstract(model.getColumnVariables()); |
|||
|
|||
// Finally cut away all columns targeting non-maybe states.
|
|||
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); |
|||
|
|||
std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); |
|||
storm::dd::Add<DdType> result = solver->performMatrixVectorMultiplication(minimize, model.getManager().getAddZero(), &subvector, stepBound); |
|||
|
|||
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), psiStates.toAdd() + result)); |
|||
} else { |
|||
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), psiStates.toAdd())); |
|||
} |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeInstantaneousRewards(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) { |
|||
// Only compute the result if the model has at least one reward this->getModel().
|
|||
STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Perform the matrix-vector multiplication.
|
|||
std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(model.getTransitionMatrix(), model.getReachableStates(), model.getIllegalMask(), model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); |
|||
storm::dd::Add<DdType> result = solver->performMatrixVectorMultiplication(minimize, rewardModel.getStateRewardVector(), nullptr, stepBound); |
|||
|
|||
return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), result)); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeCumulativeRewards(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) { |
|||
// Only compute the result if the model has at least one reward this->getModel().
|
|||
STORM_LOG_THROW(!rewardModel.empty(), 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.
|
|||
storm::dd::Add<DdType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix, model.getColumnVariables()); |
|||
|
|||
// Perform the matrix-vector multiplication.
|
|||
std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(model.getTransitionMatrix(), model.getReachableStates(), model.getIllegalMask(), model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); |
|||
storm::dd::Add<DdType> result = solver->performMatrixVectorMultiplication(minimize, model.getManager().getAddZero(), &totalRewardVector, stepBound); |
|||
|
|||
return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), result)); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) { |
|||
|
|||
// Only compute the result if there is at least one reward model.
|
|||
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Determine which states have a reward of infinity by definition.
|
|||
storm::dd::Bdd<DdType> infinityStates; |
|||
storm::dd::Bdd<DdType> transitionMatrixBdd = transitionMatrix.notZero(); |
|||
if (minimize) { |
|||
infinityStates = storm::utility::graph::performProb1E(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0E(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); |
|||
} else { |
|||
infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); |
|||
} |
|||
infinityStates = !infinityStates && model.getReachableStates(); |
|||
|
|||
storm::dd::Bdd<DdType> maybeStates = (!targetStates && !infinityStates) && model.getReachableStates(); |
|||
STORM_LOG_INFO("Found " << infinityStates.getNonZeroCount() << " 'infinity' states."); |
|||
STORM_LOG_INFO("Found " << targetStates.getNonZeroCount() << " 'target' states."); |
|||
STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states."); |
|||
|
|||
// 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.
|
|||
return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity<ValueType>()) + maybeStates.toAdd() * model.getManager().getConstant(storm::utility::one<ValueType>()))); |
|||
} else { |
|||
// If there are maybe states, we need to solve an equation system.
|
|||
if (!maybeStates.isZero()) { |
|||
// Create the matrix and the vector for the equation system.
|
|||
storm::dd::Add<DdType> maybeStatesAdd = maybeStates.toAdd(); |
|||
|
|||
// Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
|
|||
// non-maybe states in the matrix.
|
|||
storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd; |
|||
|
|||
// Then compute the state reward vector to use in the computation.
|
|||
storm::dd::Add<DdType> subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables()); |
|||
|
|||
// Finally cut away all columns targeting non-maybe states.
|
|||
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); |
|||
|
|||
// Now solve the resulting equation system.
|
|||
std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); |
|||
storm::dd::Add<DdType> result = solver->solveEquationSystem(minimize, model.getManager().getAddZero(), subvector); |
|||
|
|||
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity<ValueType>()) + result)); |
|||
} else { |
|||
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity<ValueType>()))); |
|||
} |
|||
} |
|||
} |
|||
|
|||
template class SymbolicMdpPrctlHelper<storm::dd::DdType::CUDD, double>; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,40 @@ |
|||
#ifndef STORM_MODELCHECKER_SYMBOLIC_MDP_PRCTL_MODELCHECKER_HELPER_H_ |
|||
#define STORM_MODELCHECKER_SYMBOLIC_MDP_PRCTL_MODELCHECKER_HELPER_H_ |
|||
|
|||
#include "src/models/symbolic/NondeterministicModel.h" |
|||
|
|||
#include "src/storage/dd/Add.h" |
|||
#include "src/storage/dd/Bdd.h" |
|||
|
|||
#include "src/utility/solver.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
// Forward-declare result class. |
|||
class CheckResult; |
|||
|
|||
namespace helper { |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
class SymbolicMdpPrctlHelper { |
|||
public: |
|||
typedef typename storm::models::symbolic::NondeterministicModel<DdType>::RewardModelType RewardModelType; |
|||
|
|||
static std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static std::unique_ptr<CheckResult> computeNextProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates); |
|||
|
|||
static std::unique_ptr<CheckResult> computeUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static std::unique_ptr<CheckResult> computeCumulativeRewards(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static std::unique_ptr<CheckResult> computeInstantaneousRewards(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static std::unique_ptr<CheckResult> computeReachabilityRewards(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory); |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_SYMBOLIC_MDP_PRCTL_MODELCHECKER_HELPER_H_ */ |
|||
@ -0,0 +1,96 @@ |
|||
#include "src/solver/SymbolicMinMaxLinearEquationSolver.h"
|
|||
|
|||
#include "src/storage/dd/CuddDdManager.h"
|
|||
#include "src/storage/dd/CuddAdd.h"
|
|||
|
|||
#include "src/storage/dd/Add.h"
|
|||
|
|||
#include "src/utility/constants.h"
|
|||
|
|||
#include "src/settings/SettingsManager.h"
|
|||
#include "src/settings/modules/NativeEquationSolverSettings.h"
|
|||
|
|||
namespace storm { |
|||
namespace solver { |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.toAdd() * A.getDdManager()->getConstant(storm::utility::infinity<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.toAdd() * A.getDdManager()->getConstant(storm::utility::infinity<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs) { |
|||
// Get the settings object to customize solving.
|
|||
storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); |
|||
|
|||
// Get appropriate settings.
|
|||
maximalNumberOfIterations = settings.getMaximalIterationCount(); |
|||
precision = settings.getPrecision(); |
|||
relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
storm::dd::Add<DdType> SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationSystem(bool minimize, storm::dd::Add<DdType> const& x, storm::dd::Add<DdType> const& b) const { |
|||
// Set up the environment.
|
|||
storm::dd::Add<DdType> xCopy = x; |
|||
uint_fast64_t iterations = 0; |
|||
bool converged = false; |
|||
|
|||
while (!converged && iterations < maximalNumberOfIterations) { |
|||
// Compute tmp = A * x + b
|
|||
storm::dd::Add<DdType> xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); |
|||
storm::dd::Add<DdType> tmp = this->A.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); |
|||
tmp += b; |
|||
|
|||
if (minimize) { |
|||
// This is a hack and only here because of the lack of a suitable minAbstract/maxAbstract function
|
|||
// that can properly deal with a restriction of the choices.
|
|||
tmp += illegalMaskAdd; |
|||
tmp = tmp.minAbstract(this->choiceVariables); |
|||
} else { |
|||
tmp = tmp.maxAbstract(this->choiceVariables); |
|||
} |
|||
|
|||
// Now check if the process already converged within our precision.
|
|||
converged = xCopy.equalModuloPrecision(tmp, precision, relative); |
|||
|
|||
// If the method did not converge yet, we prepare the x vector for the next iteration.
|
|||
if (!converged) { |
|||
xCopy = tmp; |
|||
} |
|||
|
|||
++iterations; |
|||
} |
|||
|
|||
return xCopy; |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
storm::dd::Add<DdType> SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::performMatrixVectorMultiplication(bool minimize, storm::dd::Add<DdType> const& x, storm::dd::Add<DdType> const* b, uint_fast64_t n) const { |
|||
storm::dd::Add<DdType> xCopy = x; |
|||
|
|||
// Perform matrix-vector multiplication while the bound is met.
|
|||
for (uint_fast64_t i = 0; i < n; ++i) { |
|||
xCopy = xCopy.swapVariables(this->rowColumnMetaVariablePairs); |
|||
xCopy = this->A.multiplyMatrix(xCopy, this->columnMetaVariables); |
|||
if (b != nullptr) { |
|||
xCopy += *b; |
|||
} |
|||
|
|||
if (minimize) { |
|||
// This is a hack and only here because of the lack of a suitable minAbstract/maxAbstract function
|
|||
// that can properly deal with a restriction of the choices.
|
|||
xCopy += illegalMaskAdd; |
|||
xCopy = xCopy.minAbstract(this->choiceVariables); |
|||
} else { |
|||
xCopy = xCopy.maxAbstract(this->choiceVariables); |
|||
} |
|||
} |
|||
|
|||
return xCopy; |
|||
} |
|||
|
|||
template class SymbolicMinMaxLinearEquationSolver<storm::dd::DdType::CUDD, double>; |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,126 @@ |
|||
#ifndef STORM_SOLVER_SYMBOLICMINMAXLINEAREQUATIONSOLVER_H_ |
|||
#define STORM_SOLVER_SYMBOLICMINMAXLINEAREQUATIONSOLVER_H_ |
|||
|
|||
#include <memory> |
|||
#include <set> |
|||
#include <vector> |
|||
#include <boost/variant.hpp> |
|||
|
|||
#include "src/storage/expressions/Variable.h" |
|||
#include "src/storage/dd/DdType.h" |
|||
|
|||
#include "src/storage/dd/CuddAdd.h" |
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
template<storm::dd::DdType T> class Add; |
|||
template<storm::dd::DdType T> class Bdd; |
|||
} |
|||
|
|||
namespace solver { |
|||
/*! |
|||
* An interface that represents an abstract symbolic linear equation solver. In addition to solving a system of |
|||
* linear equations, the functionality to repeatedly multiply a matrix with a given vector is provided. |
|||
*/ |
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
class SymbolicMinMaxLinearEquationSolver { |
|||
public: |
|||
/*! |
|||
* Constructs a symbolic min/max linear equation solver with the given meta variable sets and pairs. |
|||
* |
|||
* @param A The matrix defining the coefficients of the linear equation system. |
|||
* @param diagonal An ADD characterizing the elements on the diagonal of the matrix. |
|||
* @param allRows A BDD characterizing all rows of the equation system. |
|||
* @param illegalMask A mask that characterizes all illegal choices (that are therefore not to be taken). |
|||
* @param rowMetaVariables The meta variables used to encode the rows of the matrix. |
|||
* @param columnMetaVariables The meta variables used to encode the columns of the matrix. |
|||
* @param choiceVariables The variables encoding the choices of each row group. |
|||
* @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta |
|||
* variables. |
|||
*/ |
|||
SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs); |
|||
|
|||
/*! |
|||
* Constructs a symbolic linear equation solver with the given meta variable sets and pairs. |
|||
* |
|||
* @param A The matrix defining the coefficients of the linear equation system. |
|||
* @param allRows A BDD characterizing all rows of the equation system. |
|||
* @param illegalMask A mask that characterizes all illegal choices (that are therefore not to be taken). |
|||
* @param rowMetaVariables The meta variables used to encode the rows of the matrix. |
|||
* @param columnMetaVariables The meta variables used to encode the columns of the matrix. |
|||
* @param choiceVariables The variables encoding the choices of each row group. |
|||
* @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta |
|||
* variables. |
|||
* @param precision The precision to achieve. |
|||
* @param maximalNumberOfIterations The maximal number of iterations to perform when solving a linear |
|||
* equation system iteratively. |
|||
* @param relative Sets whether or not to use a relativ stopping criterion rather than an absolute one. |
|||
*/ |
|||
SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative); |
|||
|
|||
/*! |
|||
* Solves the equation system A*x = b. The matrix A is required to be square and have a unique solution. |
|||
* The solution of the set of linear equations will be written to the vector x. Note that the matrix A has |
|||
* to be given upon construction time of the solver object. |
|||
* |
|||
* @param minimize If set, all the value of a group of rows is the taken as the minimum over all rows and as |
|||
* the maximum otherwise. |
|||
* @param x The initual guess for the solution vector. Its length must be equal to the number of row |
|||
* groups of A. |
|||
* @param b The right-hand side of the equation system. Its length must be equal to the number of row groups |
|||
* of A. |
|||
* @return The solution of the equation system. |
|||
*/ |
|||
virtual storm::dd::Add<DdType> solveEquationSystem(bool minimize, storm::dd::Add<DdType> const& x, storm::dd::Add<DdType> const& b) const; |
|||
|
|||
/*! |
|||
* Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After |
|||
* performing the necessary multiplications, the result is written to the input vector x. Note that the |
|||
* matrix A has to be given upon construction time of the solver object. |
|||
* |
|||
* @param minimize If set, all the value of a group of rows is the taken as the minimum over all rows and as |
|||
* the maximum otherwise. |
|||
* @param x The initial vector with which to perform matrix-vector multiplication. Its length must be equal |
|||
* to the number of row groups of A. |
|||
* @param b If non-null, this vector is added after each multiplication. If given, its length must be equal |
|||
* to the number of row groups of A. |
|||
* @return The solution of the equation system. |
|||
*/ |
|||
virtual storm::dd::Add<DdType> performMatrixVectorMultiplication(bool minimize, storm::dd::Add<DdType> const& x, storm::dd::Add<DdType> const* b = nullptr, uint_fast64_t n = 1) const; |
|||
|
|||
protected: |
|||
// The matrix defining the coefficients of the linear equation system. |
|||
storm::dd::Add<DdType> const& A; |
|||
|
|||
// A BDD characterizing all rows of the equation system. |
|||
storm::dd::Bdd<DdType> const& allRows; |
|||
|
|||
// An ADD characterizing the illegal choices. |
|||
storm::dd::Add<DdType> illegalMaskAdd; |
|||
|
|||
// The row variables. |
|||
std::set<storm::expressions::Variable> rowMetaVariables; |
|||
|
|||
// The column variables. |
|||
std::set<storm::expressions::Variable> columnMetaVariables; |
|||
|
|||
// The choice variables |
|||
std::set<storm::expressions::Variable> const& choiceVariables; |
|||
|
|||
// The pairs of meta variables used for renaming. |
|||
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs; |
|||
|
|||
// The precision to achive. |
|||
double precision; |
|||
|
|||
// The maximal number of iterations to perform. |
|||
uint_fast64_t maximalNumberOfIterations; |
|||
|
|||
// A flag indicating whether a relative or an absolute stopping criterion is to be used. |
|||
bool relative; |
|||
}; |
|||
|
|||
} // namespace solver |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_SOLVER_SYMBOLICMINMAXLINEAREQUATIONSOLVER_H_ */ |
|||
@ -0,0 +1,192 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include "src/logic/Formulas.h"
|
|||
#include "src/utility/solver.h"
|
|||
#include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
|
|||
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
|
|||
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
|
|||
#include "src/parser/FormulaParser.h"
|
|||
#include "src/parser/PrismParser.h"
|
|||
#include "src/builder/DdPrismModelBuilder.h"
|
|||
#include "src/models/symbolic/Dtmc.h"
|
|||
#include "src/models/symbolic/StandardRewardModel.h"
|
|||
#include "src/settings/SettingsManager.h"
|
|||
|
|||
#include "src/settings/modules/GeneralSettings.h"
|
|||
|
|||
TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { |
|||
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser parser; |
|||
|
|||
// Build the die model with its reward model.
|
|||
#ifdef WINDOWS
|
|||
storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("coinflips"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options); |
|||
EXPECT_EQ(169ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(436ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(); |
|||
|
|||
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>())); |
|||
|
|||
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"two\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
|
|||
formula = parser.parseFromString("Pmax=? [F \"two\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
|
|||
formula = parser.parseFromString("Pmin=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
|
|||
formula = parser.parseFromString("Pmax=? [F \"three\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
|
|||
formula = parser.parseFromString("Pmin=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
|
|||
formula = parser.parseFromString("Pmax=? [F \"four\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
|
|||
formula = parser.parseFromString("Rmin=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
|
|||
formula = parser.parseFromString("Rmax=? [F \"done\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult8 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
} |
|||
|
|||
TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { |
|||
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); |
|||
|
|||
// A parser that we use for conveniently constructing the formulas.
|
|||
storm::parser::FormulaParser parser; |
|||
|
|||
// Build the die model with its reward model.
|
|||
#ifdef WINDOWS
|
|||
storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options; |
|||
#else
|
|||
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options; |
|||
#endif
|
|||
options.buildAllRewardModels = false; |
|||
options.rewardModelsToBuild.insert("rounds"); |
|||
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options); |
|||
EXPECT_EQ(3172ul, model->getNumberOfStates()); |
|||
EXPECT_EQ(7144ul, model->getNumberOfTransitions()); |
|||
|
|||
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); |
|||
|
|||
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(); |
|||
|
|||
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>())); |
|||
|
|||
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]"); |
|||
|
|||
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
|
|||
formula = parser.parseFromString("Pmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
|
|||
formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
|
|||
formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
|
|||
formula = parser.parseFromString("Rmin=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(4.2856890848060498, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(4.2856890848060498, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
|
|||
formula = parser.parseFromString("Rmax=? [F \"elected\"]"); |
|||
|
|||
result = checker.check(*formula); |
|||
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); |
|||
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>(); |
|||
|
|||
EXPECT_NEAR(4.2856890848060498, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
EXPECT_NEAR(4.2856890848060498, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue