changed print to stream to be pure virtual

src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h

@@ -14,6 +14,8 @@
 #include "storm/utility/OsDetection.h"
 #include "storm/adapters/JsonAdapter.h"
 
+#include "storm/shields/AbstractShield.h"
+
 namespace storm {
     namespace modelchecker {
         // fwd
@@ -24,6 +26,7 @@ namespace storm {
         public:
             typedef std::vector<ValueType> vector_type;
             typedef std::map<storm::storage::sparse::state_type, ValueType> map_type;
+            typedef typename storm::storage::SparseMatrix<ValueType>::index_type IndexType;  
 
             ExplicitQuantitativeCheckResult();
             ExplicitQuantitativeCheckResult(map_type const& values);
@@ -74,10 +77,15 @@ namespace storm {
             virtual ValueType sum() const override;
             
             virtual bool hasScheduler() const override;
+            virtual bool hasShield() const override;
+
             void setScheduler(std::unique_ptr<storm::storage::Scheduler<ValueType>>&& scheduler);
             storm::storage::Scheduler<ValueType> const& getScheduler() const;
             storm::storage::Scheduler<ValueType>& getScheduler();
             
+            void setShield(std::unique_ptr<tempest::shields::AbstractShield<ValueType, IndexType>> shield);
+            std::shared_ptr<tempest::shields::AbstractShield<ValueType, IndexType>> const& getShield() const;
+
             storm::json<ValueType> toJson(boost::optional<storm::storage::sparse::StateValuations> const& stateValuations = boost::none) const;
             
         private:
@@ -86,6 +94,8 @@ namespace storm {
             
             // An optional scheduler that accompanies the values.
             boost::optional<std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler;
+            boost::optional<std::shared_ptr<tempest::shields::AbstractShield<ValueType, IndexType>>> shield;
+
         };
     }
 }

src/storm/shields/AbstractShield.cpp

@@ -39,10 +39,7 @@ namespace tempest {
             return shieldingExpression->getFilename() + ".shield";
         }
 
-        template<typename ValueType, typename IndexType>
-        void AbstractShield<ValueType, IndexType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) const {
-          //  construct().printToStream(out, shieldingExpression, model)
-        }
+        
         // Explicitly instantiate appropriate
         template class AbstractShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
 #ifdef STORM_HAVE_CARL

src/storm/shields/AbstractShield.h

@@ -51,7 +51,7 @@ namespace tempest {
             std::string getClassName() const;
             std::string getShieldFileName() const;
 
-            void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) const;
+            virtual void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) = 0;
 
         protected:
             AbstractShield(std::vector<IndexType> const& rowGroupIndices, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);

src/storm/shields/OptimalShield.cpp

@@ -64,10 +64,16 @@ 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);
+        }
+
         // 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>;
 
 #endif
     }

src/storm/shields/OptimalShield.h

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

src/storm/shields/PostShield.cpp

@@ -67,10 +67,18 @@ namespace tempest {
             return shield;
         }
 
+
+        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);
+        }
+
+
         // 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>;
 
 #endif
     }

src/storm/shields/PostShield.h

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

src/storm/shields/PreShield.cpp

@@ -67,10 +67,19 @@ namespace tempest {
             }
             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);
+        }
+
+
         // 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>;
 
 #endif
     }

src/storm/shields/PreShield.h

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