From 1c2f120a7668aacb92f2444aa470150c0f78deb5 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Mon, 15 Mar 2021 23:46:23 +0100 Subject: [PATCH] added optimization direction to shields --- .../modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp | 2 +- src/storm/shields/AbstractShield.cpp | 7 ++++++- src/storm/shields/AbstractShield.h | 6 +++++- src/storm/shields/PostSafetyShield.cpp | 2 +- src/storm/shields/PostSafetyShield.h | 2 +- src/storm/shields/PreSafetyShield.cpp | 2 +- src/storm/shields/shield-handling.h | 6 +++--- 7 files changed, 18 insertions(+), 9 deletions(-) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 7ff4d500d..d8d36d20b 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -153,7 +153,7 @@ namespace storm { STORM_LOG_DEBUG(ret.values); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), std::move(ret.relevantStates), statesOfCoalition); + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), statesOfCoalition); } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } diff --git a/src/storm/shields/AbstractShield.cpp b/src/storm/shields/AbstractShield.cpp index f24189bf5..7653b0006 100644 --- a/src/storm/shields/AbstractShield.cpp +++ b/src/storm/shields/AbstractShield.cpp @@ -6,7 +6,7 @@ namespace tempest { namespace shields { template - AbstractShield::AbstractShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : rowGroupIndices(rowGroupIndices), choiceValues(choiceValues), shieldingExpression(shieldingExpression), relevantStates(relevantStates), coalitionStates(coalitionStates) { + AbstractShield::AbstractShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : rowGroupIndices(rowGroupIndices), choiceValues(choiceValues), shieldingExpression(shieldingExpression), optimizationDirection(optimizationDirection), relevantStates(relevantStates), coalitionStates(coalitionStates) { // Intentionally left empty. } @@ -29,6 +29,11 @@ namespace tempest { return shieldExpression->isRelative() ? v >= shieldExpression->getValue() * max : v >= shieldExpression->getValue(); } + template + storm::OptimizationDirection AbstractShield::getOptimizationDirection() { + return optimizationDirection; + } + template std::string AbstractShield::getClassName() const { return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*this))); diff --git a/src/storm/shields/AbstractShield.h b/src/storm/shields/AbstractShield.h index 3a8706157..a9191f213 100644 --- a/src/storm/shields/AbstractShield.h +++ b/src/storm/shields/AbstractShield.h @@ -10,6 +10,7 @@ #include "storm/storage/BitVector.h" #include "storm/storage/Distribution.h" +#include "storm/solver/OptimizationDirection.h" #include "storm/logic/ShieldExpression.h" namespace tempest { @@ -33,18 +34,21 @@ namespace tempest { */ bool allowedValue(ValueType const& max, ValueType const& v, std::shared_ptr const shieldExpression); + storm::OptimizationDirection getOptimizationDirection(); + /*! * TODO */ std::string getClassName() const; protected: - AbstractShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + AbstractShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); std::vector rowGroupIndices; std::vector choiceValues; std::shared_ptr shieldingExpression; + storm::OptimizationDirection optimizationDirection; storm::storage::BitVector relevantStates; diff --git a/src/storm/shields/PostSafetyShield.cpp b/src/storm/shields/PostSafetyShield.cpp index 26494ff29..cf76550d5 100644 --- a/src/storm/shields/PostSafetyShield.cpp +++ b/src/storm/shields/PostSafetyShield.cpp @@ -6,7 +6,7 @@ namespace tempest { namespace shields { template - PostSafetyShield::PostSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, choiceValues, shieldingExpression, relevantStates, coalitionStates) { + PostSafetyShield::PostSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates) { // Intentionally left empty. } diff --git a/src/storm/shields/PostSafetyShield.h b/src/storm/shields/PostSafetyShield.h index 7e077a940..ea6eab497 100644 --- a/src/storm/shields/PostSafetyShield.h +++ b/src/storm/shields/PostSafetyShield.h @@ -9,7 +9,7 @@ namespace tempest { template class PostSafetyShield : public AbstractShield { public: - PostSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::storage::BitVector relevantStates, boost::optional coalitionStates); + PostSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); storm::storage::PostScheduler construct(); }; } diff --git a/src/storm/shields/PreSafetyShield.cpp b/src/storm/shields/PreSafetyShield.cpp index 694362d2d..9d0e24b43 100644 --- a/src/storm/shields/PreSafetyShield.cpp +++ b/src/storm/shields/PreSafetyShield.cpp @@ -6,7 +6,7 @@ namespace tempest { namespace shields { template - PreSafetyShield::PreSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, choiceValues, shieldingExpression, relevantStates, coalitionStates) { + PreSafetyShield::PreSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates) { // Intentionally left empty. } diff --git a/src/storm/shields/shield-handling.h b/src/storm/shields/shield-handling.h index bd38fedc2..7e74ebcf2 100644 --- a/src/storm/shields/shield-handling.h +++ b/src/storm/shields/shield-handling.h @@ -30,14 +30,14 @@ namespace tempest { } template - void createShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { + void createShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { std::ofstream stream; storm::utility::openFile(shieldFilename(shieldingExpression), stream); if(shieldingExpression->isPreSafetyShield()) { - PreSafetyShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, relevantStates, coalitionStates); + PreSafetyShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); shield.construct().printToStream(stream, model); } else if(shieldingExpression->isPostSafetyShield()) { - PostSafetyShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, relevantStates, coalitionStates); + PostSafetyShield shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, optimizationDirection, relevantStates, coalitionStates); shield.construct().printToStream(stream, model); } else if(shieldingExpression->isOptimalShield()) { storm::utility::closeFile(stream);