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);