refactored shield export

src/storm-cli-utilities/model-handling.h

@@ -49,6 +49,11 @@
 #include "storm/settings/modules/HintSettings.h"
 #include "storm/storage/Qvbs.h"
 
+#include "storm/shields/AbstractShield.h"
+#include "storm/shields/PreShield.h"
+#include "storm/shields/PostShield.h"
+#include "storm/shields/OptimalShield.h"
+
 #include "storm/utility/Stopwatch.h"
 
 namespace storm {
@@ -1047,9 +1052,18 @@ namespace storm {
                                                 if (result->isExplicitQuantitativeCheckResult()) {
                                                     if (result-> template asExplicitQuantitativeCheckResult<ValueType>().hasShield()) {
                                                         auto shield = result->template asExplicitQuantitativeCheckResult<ValueType>().getShield();
+                                                        if(shield->isPreShield()) {
+                                                            shield->asPreShield().construct();
+                                                        } else if(shield->isPostShield()) {
+                                                            shield->asPostShield().construct();
+                                                        } else if(shield->isOptimalShield()) {
+                                                            shield->asOptimalShield().construct();
+                                                        }
+
                                                         STORM_PRINT_AND_LOG("Exporting shield ... ");
 
-                                                        storm::api::exportShield(sparseModel, shield, ioSettings.getExportShieldFilename());
+                                                        STORM_LOG_WARN_COND(exportCount == 0, "Prepending " << exportCount << " to file name for this property because there are multiple properties.");
+                                                        storm::api::exportShield(sparseModel, shield, (exportCount == 0 ? std::string("") : std::to_string(exportCount)) + ioSettings.getExportShieldFilename());
                                                     }
                                                 }
                                             }

src/storm/api/verification.h

@@ -458,7 +458,7 @@ namespace storm {
 
         template<storm::dd::DdType DdType, typename ValueType>
         typename std::enable_if<std::is_same<ValueType, storm::RationalFunction>::value, std::unique_ptr<storm::modelchecker::CheckResult>>::type verifyWithDdEngine(storm::Environment const&, std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>> const&, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const&) {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Dd engine cannot verify MDPs with this data type.");
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "");
         }
 
         template<storm::dd::DdType DdType, typename ValueType>

src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp

@@ -141,6 +141,7 @@ namespace storm {
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
 
+
             auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint());
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
             if(checkTask.isShieldingTask()) {

src/storm/shields/AbstractShield.cpp

@@ -1,4 +1,7 @@
 #include "storm/shields/AbstractShield.h"
+#include "storm/shields/PreShield.h"
+#include "storm/shields/PostShield.h"
+#include "storm/shields/OptimalShield.h"
 
 #include <boost/core/typeinfo.hpp>
 
@@ -29,6 +32,57 @@ namespace tempest {
             return optimizationDirection;
         }
 
+        template<typename ValueType, typename IndexType>
+        void AbstractShield<ValueType, IndexType>::setShieldingExpression(std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression) {
+            this->shieldingExpression = shieldingExpression;
+        }
+
+        template<typename ValueType, typename IndexType>
+        bool AbstractShield<ValueType, IndexType>::isPreShield() const {
+            return false;
+        }
+
+        template<typename ValueType, typename IndexType>
+        bool AbstractShield<ValueType, IndexType>::isPostShield() const {
+            return false;
+        }
+
+        template<typename ValueType, typename IndexType>
+        bool AbstractShield<ValueType, IndexType>::isOptimalShield() const {
+            return false;
+        }
+
+        template<typename ValueType, typename IndexType>
+        PreShield<ValueType, IndexType>& AbstractShield<ValueType, IndexType>::asPreShield() {
+            return dynamic_cast<PreShield<ValueType, IndexType>&>(*this);
+        }
+
+        template<typename ValueType, typename IndexType>
+        PreShield<ValueType, IndexType> const& AbstractShield<ValueType, IndexType>::asPreShield() const {
+            return dynamic_cast<PreShield<ValueType, IndexType> const&>(*this);
+        }
+
+        template<typename ValueType, typename IndexType>
+        PostShield<ValueType, IndexType>& AbstractShield<ValueType, IndexType>::asPostShield() {
+            return dynamic_cast<PostShield<ValueType, IndexType>&>(*this);
+        }
+
+        template<typename ValueType, typename IndexType>
+        PostShield<ValueType, IndexType> const& AbstractShield<ValueType, IndexType>::asPostShield() const {
+            return dynamic_cast<PostShield<ValueType, IndexType> const&>(*this);
+        }
+
+        template<typename ValueType, typename IndexType>
+        OptimalShield<ValueType, IndexType>& AbstractShield<ValueType, IndexType>::asOptimalShield() {
+            return dynamic_cast<OptimalShield<ValueType, IndexType>&>(*this);
+        }
+
+        template<typename ValueType, typename IndexType>
+        OptimalShield<ValueType, IndexType> const& AbstractShield<ValueType, IndexType>::asOptimalShield() const {
+            return dynamic_cast<OptimalShield<ValueType, IndexType> const&>(*this);
+        }
+
+
         template<typename ValueType, typename IndexType>
         std::string AbstractShield<ValueType, IndexType>::getClassName() const {
             return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*this)));

src/storm/shields/AbstractShield.h

@@ -16,12 +16,23 @@
 
 #include "storm/logic/ShieldExpression.h"
 
+#include "storm/exceptions/NotSupportedException.h"
+
+
 namespace tempest {
     namespace shields {
+        template<typename ValueType, typename IndexType>
+        class PreShield;
+        template<typename ValueType, typename IndexType>
+        class PostShield;
+        template<typename ValueType, typename IndexType>
+        class OptimalShield;
+
         namespace utility {
             template<typename ValueType, typename Compare, bool relative>
             struct ChoiceFilter {
                 bool operator()(ValueType v, ValueType opt, double shieldValue) {
+                    if constexpr (std::is_same_v<ValueType, storm::RationalNumber> || std::is_same_v<ValueType, double>) {
                         Compare compare;
                         if(relative && std::is_same<Compare, storm::utility::ElementLessEqual<ValueType>>::value) {
                             return compare(v, opt + opt * shieldValue);
@@ -29,6 +40,9 @@ namespace tempest {
                             return compare(v, opt * shieldValue);
                         }
                         else return compare(v, shieldValue);
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot create shields for parametric models");
+                    }
                 }
             };
         }
@@ -47,9 +61,24 @@ namespace tempest {
             std::vector<IndexType> computeRowGroupSizes();
 
             storm::OptimizationDirection getOptimizationDirection();
+            void setShieldingExpression(std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression);
 
             std::string getClassName() const;
 
+            virtual bool isPreShield() const;
+            virtual bool isPostShield() const;
+            virtual bool isOptimalShield() const;
+
+            PreShield<ValueType, IndexType>& asPreShield();
+            PreShield<ValueType, IndexType> const& asPreShield() const;
+
+            PostShield<ValueType, IndexType>& asPostShield();
+            PostShield<ValueType, IndexType> const& asPostShield() const;
+
+            OptimalShield<ValueType, IndexType>& asOptimalShield();
+            OptimalShield<ValueType, IndexType> const& asOptimalShield() const;
+
+
             virtual void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) = 0;
             virtual void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) = 0;
 

src/storm/shields/OptimalShield.cpp

@@ -64,21 +64,40 @@ namespace tempest {
             return shield;
         }
 
+
         template<typename ValueType, typename IndexType>
-        void OptimalShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
-           this->construct().printToStream(out, this->shieldingExpression, model);
+        std::shared_ptr<storm::storage::PostScheduler<ValueType>> OptimalShield<ValueType, IndexType>::getScheduler() const {
+            return optimalScheduler;
+        }
+
+        template<typename ValueType, typename IndexType>
+        bool OptimalShield<ValueType, IndexType>::isOptimalShield() const {
+            return true;
         }
 
         template<typename ValueType, typename IndexType>
         void OptimalShield<ValueType, IndexType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
-            this->construct().printJsonToStream(out, model);
+            optimalScheduler->printJsonToStream(out, model);
+        }
+
+        template<typename ValueType, typename IndexType>
+        void OptimalShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
+            optimalScheduler->printToStream(out, this->shieldingExpression, model);
         }
 
+        //template<typename ValueType, typename IndexType>
+        //template<typename VT>
+        //std::enable_if_t<std::is_same<VT, storm::RationalFunction>::value, storm::storage::PostScheduler<VT>> OptimalShield<ValueType, IndexType>::construct() {
+        //    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "todo");
+        //}
+
+
+
         // Explicitly instantiate appropriate classes
         template class OptimalShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
 #ifdef STORM_HAVE_CARL
         template class OptimalShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
-       // template class OptimalShield<storm::RationalFunction, typename storm::storage::SparseMatrix<storm::RationalFunction>::index_type>;
+        template class OptimalShield<storm::RationalFunction, typename storm::storage::SparseMatrix<storm::RationalFunction>::index_type>;
 
 #endif
     }

src/storm/shields/OptimalShield.h

@@ -14,11 +14,16 @@ namespace tempest {
             storm::storage::PostScheduler<ValueType> construct();
             template<typename Compare, bool relative>
             storm::storage::PostScheduler<ValueType> constructWithCompareType();
+            std::shared_ptr<storm::storage::PostScheduler<ValueType>> getScheduler() const;
+
+            virtual bool isOptimalShield() const override;
+
             virtual void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
             virtual void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
-
         private:
             std::vector<ValueType> choiceValues;
+
+            std::shared_ptr<storm::storage::PostScheduler<ValueType>> optimalScheduler;
         };
     }
 }

src/storm/shields/PostShield.cpp

@@ -45,7 +45,7 @@ namespace tempest {
                     }
                     ValueType optProbability = *(choice_it + optProbabilityIndex);
                     if(!relative && !choiceFilter(optProbability, optProbability, this->shieldingExpression->getValue())) {
-                        STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state);
+                        //STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state);
                         shield.setChoice(storm::storage::PostSchedulerChoice<ValueType>(), state, 0);
                         choice_it += rowGroupSize;
                         continue;
@@ -69,21 +69,37 @@ namespace tempest {
 
 
         template<typename ValueType, typename IndexType>
-        void PostShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
-           this->construct().printToStream(out, this->shieldingExpression, model);
+        std::shared_ptr<storm::storage::PostScheduler<ValueType>> PostShield<ValueType, IndexType>::getScheduler() const {
+            return postScheduler;
+        }
+
+        template<typename ValueType, typename IndexType>
+        bool PostShield<ValueType, IndexType>::isPostShield() const {
+            return true;
         }
 
         template<typename ValueType, typename IndexType>
         void PostShield<ValueType, IndexType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
-            this->construct().printJsonToStream(out, model);
+            postScheduler->printJsonToStream(out, model);
         }
 
+        template<typename ValueType, typename IndexType>
+        void PostShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
+            postScheduler->printToStream(out, this->shieldingExpression, model);
+        }
+
+        //template<typename ValueType, typename IndexType>
+        //template<typename VT>
+        //std::enable_if_t<std::is_same<VT, storm::RationalFunction>::value, storm::storage::PostScheduler<VT>> PostShield<ValueType, IndexType>::construct() {
+        //    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "todo");
+        //}
+
 
         // Explicitly instantiate appropriate classes
         template class PostShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
 #ifdef STORM_HAVE_CARL
         template class PostShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
-       // template class PostShield<storm::RationalFunction, typename storm::storage::SparseMatrix<storm::RationalFunction>::index_type>;
+        template class PostShield<storm::RationalFunction, typename storm::storage::SparseMatrix<storm::RationalFunction>::index_type>;
 
 #endif
     }

src/storm/shields/PostShield.h

@@ -14,12 +14,16 @@ namespace tempest {
             storm::storage::PostScheduler<ValueType> construct();
             template<typename Compare, bool relative>
             storm::storage::PostScheduler<ValueType> constructWithCompareType();
+            std::shared_ptr<storm::storage::PostScheduler<ValueType>> getScheduler() const;
+
+            virtual bool isPostShield() const override;
 
             virtual void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
             virtual void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
-
         private:
             std::vector<ValueType> choiceValues;
+
+            std::shared_ptr<storm::storage::PostScheduler<ValueType>> postScheduler;
         };
     }
 }

src/storm/shields/PreShield.cpp

@@ -10,8 +10,12 @@ namespace tempest {
             // Intentionally left empty.
         }
 
+
         template<typename ValueType, typename IndexType>
         storm::storage::PreScheduler<ValueType> PreShield<ValueType, IndexType>::construct() {
+            if constexpr (std::is_same_v<ValueType, storm::RationalFunction>) {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "todo");
+            }
             if (this->getOptimizationDirection() == storm::OptimizationDirection::Minimize) {
                 if(this->shieldingExpression->isRelative()) {
                     return constructWithCompareType<storm::utility::ElementLessEqual<ValueType>, true>();
@@ -38,7 +42,7 @@ namespace tempest {
             }
             for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) {
                 uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state];
-                if(this->relevantStates.get(state)) {
+                if(true){ //if(this->relevantStates.get(state)) {
                     storm::storage::PreSchedulerChoice<ValueType> enabledChoices;
                     ValueType optProbability;
                     if(std::is_same<Compare, storm::utility::ElementGreaterEqual<ValueType>>::value) {
@@ -47,7 +51,7 @@ namespace tempest {
                         optProbability = *std::min_element(choice_it, choice_it + rowGroupSize);
                     }
                     if(!relative && !choiceFilter(optProbability, optProbability, this->shieldingExpression->getValue())) {
-                        STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state);
+                        //STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state);
                         shield.setChoice(storm::storage::PreSchedulerChoice<ValueType>(), state, 0);
                         choice_it += rowGroupSize;
                         continue;
@@ -65,27 +69,38 @@ namespace tempest {
                 }
 
             }
+            preScheduler = std::make_shared<storm::storage::PreScheduler<ValueType>>(shield);
             return shield;
         }
 
 
         template<typename ValueType, typename IndexType>
-        void PreShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
-           this->construct().printToStream(out, this->shieldingExpression, model);
+        std::shared_ptr<storm::storage::PreScheduler<ValueType>> PreShield<ValueType, IndexType>::getScheduler() const {
+            return preScheduler;
+        }
+
+        template<typename ValueType, typename IndexType>
+        bool PreShield<ValueType, IndexType>::isPreShield() const {
+            return true;
         }
 
         template<typename ValueType, typename IndexType>
         void PreShield<ValueType, IndexType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
-            this->construct().printJsonToStream(out, model);
+            preScheduler->printJsonToStream(out, model);
         }
 
+        template<typename ValueType, typename IndexType>
+        void PreShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
+            preScheduler->printToStream(out, this->shieldingExpression, model);
+        }
+
+
 
         // Explicitly instantiate appropriate classes
         template class PreShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
 #ifdef STORM_HAVE_CARL
         template class PreShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
-        //template class PreShield<storm::RationalFunction, typename storm::storage::SparseMatrix<storm::RationalFunction>::index_type>;
-
+        template class PreShield<storm::RationalFunction, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
 #endif
     }
 }

src/storm/shields/PreShield.h

@@ -11,15 +11,22 @@ namespace tempest {
         public:
             PreShield(std::vector<IndexType> const& rowGroupIndices, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);
 
+
             storm::storage::PreScheduler<ValueType> construct();
+
             template<typename Compare, bool relative>
             storm::storage::PreScheduler<ValueType> constructWithCompareType();
+            void setShieldingExpression(std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression);
+            std::shared_ptr<storm::storage::PreScheduler<ValueType>> getScheduler() const;
+
+            virtual bool isPreShield() const override;
 
             virtual void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
             virtual void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) override;
-
         private:
             std::vector<ValueType> choiceValues;
+
+            std::shared_ptr<storm::storage::PreScheduler<ValueType>> preScheduler;
         };
     }
 }

src/storm/storage/PostScheduler.cpp

@@ -192,6 +192,7 @@ namespace storm {
         template class PostScheduler<double>;
 #ifdef STORM_HAVE_CARL
         template class PostScheduler<storm::RationalNumber>;
+        template class PostScheduler<storm::RationalFunction>;
 #endif
     }
 }

src/storm/storage/PreScheduler.cpp

@@ -223,6 +223,7 @@ namespace storm {
         template class PreScheduler<double>;
 #ifdef STORM_HAVE_CARL
         template class PreScheduler<storm::RationalNumber>;
+        template class PreScheduler<storm::RationalFunction>;
 #endif
     }
 }

src/storm/storage/PreScheduler.h

@@ -13,6 +13,7 @@ namespace storm {
         /*
          * TODO needs obvious changes in all comment blocks
          */
+        // TODO inherit from Scheduler?
         template <typename ValueType>
         class PreScheduler {
         public: