From 9c82fe7b0d1b403d16ee27e71ce72f51a139f69d Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 12 Aug 2020 10:30:45 +0200 Subject: [PATCH] Making hybrid infinite horizon helper ready for deterministic models. --- .../HybridInfiniteHorizonHelper.cpp | 143 ++++++++++++++++++ .../HybridInfiniteHorizonHelper.h | 87 +++++++++++ ...dNondeterministicInfiniteHorizonHelper.cpp | 101 ------------- ...ridNondeterministicInfiniteHorizonHelper.h | 64 -------- 4 files changed, 230 insertions(+), 165 deletions(-) create mode 100644 src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.cpp create mode 100644 src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.h delete mode 100644 src/storm/modelchecker/helper/infinitehorizon/HybridNondeterministicInfiniteHorizonHelper.cpp delete mode 100644 src/storm/modelchecker/helper/infinitehorizon/HybridNondeterministicInfiniteHorizonHelper.h diff --git a/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.cpp new file mode 100644 index 000000000..36231a419 --- /dev/null +++ b/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.cpp @@ -0,0 +1,143 @@ +#include "HybridInfiniteHorizonHelper.h" + +#include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h" +#include "storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.h" +#include "storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h" + +#include "storm/models/symbolic/NondeterministicModel.h" + +#include "storm/storage/SparseMatrix.h" + +#include "storm/utility/macros.h" + +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + template + HybridInfiniteHorizonHelper::HybridInfiniteHorizonHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix) : _model(model), _transitionMatrix(transitionMatrix), _markovianStates(nullptr), _exitRates(nullptr) { + // Intentionally left empty. + } + + template + HybridInfiniteHorizonHelper::HybridInfiniteHorizonHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector) : _model(model), _transitionMatrix(transitionMatrix), _markovianStates(&markovianStates), _exitRates(&exitRateVector) { + // Intentionally left empty. + } + + template + HybridInfiniteHorizonHelper::HybridInfiniteHorizonHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector) : _model(model), _transitionMatrix(transitionMatrix), _markovianStates(nullptr), _exitRates(&exitRateVector) { + // Intentionally left empty. + } + + template + std::unique_ptr> HybridInfiniteHorizonHelper::computeLongRunAverageProbabilities(Environment const& env, storm::dd::Bdd const& psiStates) { + // Convert this query to an instance for the sparse engine. + // Create ODD for the translation. + storm::dd::Odd odd = _model.getReachableStates().createOdd(); + // Translate all required components + storm::storage::SparseMatrix explicitTransitionMatrix; + if (_model.isNondeterministicModel()) { + explicitTransitionMatrix = _transitionMatrix.toMatrix(dynamic_cast const&>(_model).getNondeterminismVariables(), odd, odd); + } else { + explicitTransitionMatrix = _transitionMatrix.toMatrix(odd, odd); + } + std::vector explicitExitRateVector; + storm::storage::BitVector explicitMarkovianStates; + if (isContinuousTime()) { + explicitExitRateVector = _exitRates->toVector(odd); + if (_markovianStates) { + explicitMarkovianStates = _markovianStates->toVector(odd); + } + } + auto sparseHelper = createSparseHelper(explicitTransitionMatrix, explicitMarkovianStates, explicitExitRateVector, odd); + auto explicitResult = sparseHelper->computeLongRunAverageProbabilities(env, psiStates.toVector(odd)); + return std::make_unique>(_model.getReachableStates(), _model.getManager().getBddZero(), _model.getManager().template getAddZero(), _model.getReachableStates(), std::move(odd), std::move(explicitResult)); + } + + template + std::unique_ptr> HybridInfiniteHorizonHelper::computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::StandardRewardModel const& rewardModel) { + // Convert this query to an instance for the sparse engine. + // Create ODD for the translation. + storm::dd::Odd odd = _model.getReachableStates().createOdd(); + + // Translate all required components + // Transitions and rewards + storm::storage::SparseMatrix explicitTransitionMatrix; + std::vector explicitStateRewards, explicitActionRewards; + if (rewardModel.hasStateRewards()) { + explicitStateRewards = rewardModel.getStateRewardVector().toVector(odd); + } + if (_model.isNondeterministicModel() && rewardModel.hasStateActionRewards()) { + // Matrix and action-based vector have to be produced at the same time to guarantee the correct order + auto matrixRewards = _transitionMatrix.toMatrixVector(rewardModel.getStateActionRewardVector(), dynamic_cast const&>(_model).getNondeterminismVariables(), odd, odd); + explicitTransitionMatrix = std::move(matrixRewards.first); + explicitActionRewards = std::move(matrixRewards.second); + } else { + // Translate matrix only + explicitTransitionMatrix = _transitionMatrix.toMatrix(dynamic_cast const&>(_model).getNondeterminismVariables(), odd, odd); + if (rewardModel.hasStateActionRewards()) { + // For deterministic models we can translate the action rewards easily + explicitActionRewards = rewardModel.getStateActionRewardVector().toVector(odd); + } + } + STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are not supported in this engine."); + // Continuous time information + std::vector explicitExitRateVector; + storm::storage::BitVector explicitMarkovianStates; + if (isContinuousTime()) { + explicitExitRateVector = _exitRates->toVector(odd); + if (_markovianStates) { + explicitMarkovianStates = _markovianStates->toVector(odd); + } + } + auto sparseHelper = createSparseHelper(explicitTransitionMatrix, explicitMarkovianStates, explicitExitRateVector, odd); + auto explicitResult = sparseHelper->computeLongRunAverageValues(env, rewardModel.hasStateRewards() ? &explicitStateRewards : nullptr, rewardModel.hasStateActionRewards() ? &explicitActionRewards : nullptr); + return std::make_unique>(_model.getReachableStates(), _model.getManager().getBddZero(), _model.getManager().template getAddZero(), _model.getReachableStates(), std::move(odd), std::move(explicitResult)); + } + + template + bool HybridInfiniteHorizonHelper::isContinuousTime() const { + STORM_LOG_ASSERT((_markovianStates == nullptr) || (_exitRates != nullptr), "Inconsistent information given: Have Markovian states but no exit rates." ); + return _exitRates != nullptr; + } + + template + template > + std::unique_ptr> HybridInfiniteHorizonHelper::createSparseHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, storm::dd::Odd const& odd) const { + std::unique_ptr> result; + if (isContinuousTime()) { + result = std::make_unique>(transitionMatrix, markovianStates, exitRates); + } else { + result = std::make_unique>(transitionMatrix); + } + storm::modelchecker::helper::setInformationFromOtherHelperNondeterministic(*result, *this, [&odd](storm::dd::Bdd const& s){ return s.toVector(odd); }); + STORM_LOG_WARN_COND(!this->isProduceSchedulerSet(), "Scheduler extraction not supported in Hybrid engine."); + return result; + } + + template + template > + std::unique_ptr> HybridInfiniteHorizonHelper::createSparseHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, storm::dd::Odd const& odd) const { + std::unique_ptr> result; + if (isContinuousTime()) { + result = std::make_unique>(transitionMatrix, exitRates); + } else { + result = std::make_unique>(transitionMatrix); + } + storm::modelchecker::helper::setInformationFromOtherHelperDeterministic(*result, *this, [&odd](storm::dd::Bdd const& s){ return s.toVector(odd); }); + return result; + } + + template class HybridInfiniteHorizonHelper; + template class HybridInfiniteHorizonHelper; + template class HybridInfiniteHorizonHelper; + template class HybridInfiniteHorizonHelper; + template class HybridInfiniteHorizonHelper; + template class HybridInfiniteHorizonHelper; + template class HybridInfiniteHorizonHelper; + + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.h new file mode 100644 index 000000000..09035c6f3 --- /dev/null +++ b/src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.h @@ -0,0 +1,87 @@ +#pragma once +#include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h" + +#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" + +#include "storm/models/symbolic/Model.h" +#include "storm/models/symbolic/StandardRewardModel.h" + +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Add.h" +#include "storm/storage/dd/Bdd.h" + +namespace storm { + class Environment; + + namespace storage { + template class SparseMatrix; + class BitVector; + } + + namespace modelchecker { + namespace helper { + + template class SparseInfiniteHorizonHelper; + + /*! + * Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system. + */ + template + class HybridInfiniteHorizonHelper : public SingleValueModelCheckerHelper { + + public: + /*! + * Initializes the helper for a discrete time model (MDP or DTMC) + */ + HybridInfiniteHorizonHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix); + + /*! + * Initializes the helper for a Markov Automaton + */ + HybridInfiniteHorizonHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& _exitRates); + + /*! + * Initializes the helper for a CTMC + * @note The transition matrix must be probabilistic + */ + HybridInfiniteHorizonHelper(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& _exitRates); + + /*! + * Computes the long run average probabilities, i.e., the fraction of the time we are in a psiState + * @return a value for each state + */ + std::unique_ptr> computeLongRunAverageProbabilities(Environment const& env, storm::dd::Bdd const& psiStates); + + /*! + * Computes the long run average rewards, i.e., the average reward collected per time unit + * @return a value for each state + */ + std::unique_ptr> computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::StandardRewardModel const& rewardModel); + + protected: + + /*! + * @return true iff this is a computation on a continuous time model (i.e. MA) + */ + bool isContinuousTime() const; + + /*! + * @return a sparse infinite horizon helper with the provided explicit model information. + * @param exitRates exit rates (ignored for discrete time models) + * @param markovianStates Markovian states or (ignored for non-MA) + */ + template = 0> + std::unique_ptr> createSparseHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, storm::dd::Odd const& odd) const; + template = 0> + std::unique_ptr> createSparseHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, storm::dd::Odd const& odd) const; + + + private: + storm::models::symbolic::Model const& _model; + storm::dd::Add const& _transitionMatrix; + storm::dd::Bdd const* _markovianStates; + storm::dd::Add const* _exitRates; + }; + } + } +} diff --git a/src/storm/modelchecker/helper/infinitehorizon/HybridNondeterministicInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/HybridNondeterministicInfiniteHorizonHelper.cpp deleted file mode 100644 index fa28e486a..000000000 --- a/src/storm/modelchecker/helper/infinitehorizon/HybridNondeterministicInfiniteHorizonHelper.cpp +++ /dev/null @@ -1,101 +0,0 @@ -#include "HybridNondeterministicInfiniteHorizonHelper.h" - -#include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h" -#include "storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h" - -#include "storm/storage/SparseMatrix.h" - -#include "storm/utility/macros.h" - -#include "storm/exceptions/NotSupportedException.h" - -namespace storm { - namespace modelchecker { - namespace helper { - - template - HybridNondeterministicInfiniteHorizonHelper::HybridNondeterministicInfiniteHorizonHelper(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix) : _model(model), _transitionMatrix(transitionMatrix), _markovianStates(nullptr), _exitRates(nullptr) { - // Intentionally left empty. - } - - template - HybridNondeterministicInfiniteHorizonHelper::HybridNondeterministicInfiniteHorizonHelper(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& exitRateVector) : _model(model), _transitionMatrix(transitionMatrix), _markovianStates(&markovianStates), _exitRates(&exitRateVector) { - // Intentionally left empty. - } - - template - std::unique_ptr> HybridNondeterministicInfiniteHorizonHelper::computeLongRunAverageProbabilities(Environment const& env, storm::dd::Bdd const& psiStates) { - // Convert this query to an instance for the sparse engine. - // Create ODD for the translation. - storm::dd::Odd odd = _model.getReachableStates().createOdd(); - storm::storage::SparseMatrix explicitTransitionMatrix = _transitionMatrix.toMatrix(_model.getNondeterminismVariables(), odd, odd); - std::unique_ptr> sparseHelper; - std::vector explicitExitRateVector; - storm::storage::BitVector explicitMarkovianStates; - if (isContinuousTime()) { - explicitExitRateVector = _exitRates->toVector(odd); - explicitMarkovianStates = _markovianStates->toVector(odd); - sparseHelper = std::make_unique>(explicitTransitionMatrix, explicitMarkovianStates, explicitExitRateVector); - } else { - sparseHelper = std::make_unique>(explicitTransitionMatrix); - } - storm::modelchecker::helper::setInformationFromOtherHelperNondeterministic(*sparseHelper, *this, [&odd](storm::dd::Bdd const& s){ return s.toVector(odd); }); - STORM_LOG_WARN_COND(!this->isProduceSchedulerSet(), "Scheduler extraction not supported in Hybrid engine."); - auto explicitResult = sparseHelper->computeLongRunAverageProbabilities(env, psiStates.toVector(odd)); - return std::make_unique>(_model.getReachableStates(), _model.getManager().getBddZero(), _model.getManager().template getAddZero(), _model.getReachableStates(), std::move(odd), std::move(explicitResult)); - } - - template - std::unique_ptr> HybridNondeterministicInfiniteHorizonHelper::computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::StandardRewardModel const& rewardModel) { - // Convert this query to an instance for the sparse engine. - // Create ODD for the translation. - storm::dd::Odd odd = _model.getReachableStates().createOdd(); - - // Create matrix and reward vectors - storm::storage::SparseMatrix explicitTransitionMatrix; - std::vector explicitStateRewards, explicitActionRewards; - if (rewardModel.hasStateRewards()) { - explicitStateRewards = rewardModel.getStateRewardVector().toVector(odd); - } - if (rewardModel.hasStateActionRewards()) { - // Matrix and action-based vector have to be produced at the same time to guarantee the correct order - auto matrixRewards = _transitionMatrix.toMatrixVector(rewardModel.getStateActionRewardVector(), _model.getNondeterminismVariables(), odd, odd); - explicitTransitionMatrix = std::move(matrixRewards.first); - explicitActionRewards = std::move(matrixRewards.second); - } else { - // Translate matrix only - explicitTransitionMatrix = _transitionMatrix.toMatrix(_model.getNondeterminismVariables(), odd, odd); - } - STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are not supported in this engine."); - - // Create remaining components and helper - std::vector explicitExitRateVector; - storm::storage::BitVector explicitMarkovianStates; - std::unique_ptr> sparseHelper; - if (isContinuousTime()) { - explicitExitRateVector = _exitRates->toVector(odd); - explicitMarkovianStates = _markovianStates->toVector(odd); - sparseHelper = std::make_unique>(explicitTransitionMatrix, explicitMarkovianStates, explicitExitRateVector); - } else { - sparseHelper = std::make_unique>(explicitTransitionMatrix); - } - storm::modelchecker::helper::setInformationFromOtherHelperNondeterministic(*sparseHelper, *this, [&odd](storm::dd::Bdd const& s){ return s.toVector(odd); }); - - STORM_LOG_WARN_COND(!this->isProduceSchedulerSet(), "Scheduler extraction not supported in Hybrid engine."); - auto explicitResult = sparseHelper->computeLongRunAverageValues(env, rewardModel.hasStateRewards() ? &explicitStateRewards : nullptr, rewardModel.hasStateActionRewards() ? &explicitActionRewards : nullptr); - return std::make_unique>(_model.getReachableStates(), _model.getManager().getBddZero(), _model.getManager().template getAddZero(), _model.getReachableStates(), std::move(odd), std::move(explicitResult)); - } - - template - bool HybridNondeterministicInfiniteHorizonHelper::isContinuousTime() const { - STORM_LOG_ASSERT((_markovianStates == nullptr) == (_exitRates == nullptr), "Inconsistent information given: Have Markovian states but no exit rates (or vice versa)." ); - return _markovianStates != nullptr; - } - - template class HybridNondeterministicInfiniteHorizonHelper; - template class HybridNondeterministicInfiniteHorizonHelper; - template class HybridNondeterministicInfiniteHorizonHelper; - - } - } -} \ No newline at end of file diff --git a/src/storm/modelchecker/helper/infinitehorizon/HybridNondeterministicInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/HybridNondeterministicInfiniteHorizonHelper.h deleted file mode 100644 index d6a67089b..000000000 --- a/src/storm/modelchecker/helper/infinitehorizon/HybridNondeterministicInfiniteHorizonHelper.h +++ /dev/null @@ -1,64 +0,0 @@ -#pragma once -#include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h" - -#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" - -#include "storm/models/symbolic/NondeterministicModel.h" -#include "storm/models/symbolic/StandardRewardModel.h" - -#include "storm/storage/dd/DdManager.h" -#include "storm/storage/dd/Add.h" -#include "storm/storage/dd/Bdd.h" - -namespace storm { - class Environment; - - namespace modelchecker { - namespace helper { - - /*! - * Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system. - */ - template - class HybridNondeterministicInfiniteHorizonHelper : public SingleValueModelCheckerHelper { - - public: - /*! - * Initializes the helper for a discrete time (i.e. MDP) - */ - HybridNondeterministicInfiniteHorizonHelper(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix); - - /*! - * Initializes the helper for a continuous time (i.e. MA) - */ - HybridNondeterministicInfiniteHorizonHelper(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& markovianStates, storm::dd::Add const& _exitRates); - - /*! - * Computes the long run average probabilities, i.e., the fraction of the time we are in a psiState - * @return a value for each state - */ - std::unique_ptr> computeLongRunAverageProbabilities(Environment const& env, storm::dd::Bdd const& psiStates); - - /*! - * Computes the long run average rewards, i.e., the average reward collected per time unit - * @return a value for each state - */ - std::unique_ptr> computeLongRunAverageRewards(Environment const& env, storm::models::symbolic::StandardRewardModel const& rewardModel); - - protected: - - /*! - * @return true iff this is a computation on a continuous time model (i.e. MA) - */ - bool isContinuousTime() const; - - - private: - storm::models::symbolic::NondeterministicModel const& _model; - storm::dd::Add const& _transitionMatrix; - storm::dd::Bdd const* _markovianStates; - storm::dd::Add const* _exitRates; - }; - } - } -}