From 3decad58b93433ce7fb440b6ab8de872d0878d7c Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Mon, 15 Mar 2021 09:20:10 +0100
Subject: [PATCH] introduced shield export

Still needs a proper naming convention for the shields to be unique
---
 src/storm/shields/shield-handling.h | 25 +++++++++++++++++++++----
 1 file changed, 21 insertions(+), 4 deletions(-)

diff --git a/src/storm/shields/shield-handling.h b/src/storm/shields/shield-handling.h
index be3b1ce88..bd38fedc2 100644
--- a/src/storm/shields/shield-handling.h
+++ b/src/storm/shields/shield-handling.h
@@ -11,22 +11,39 @@
 
 #include "storm/shields/AbstractShield.h"
 #include "storm/shields/PreSafetyShield.h"
+#include "storm/shields/PostSafetyShield.h"
+
+#include "storm/io/file.h"
+#include "storm/utility/macros.h"
 
 #include "storm/exceptions/InvalidArgumentException.h"
 
 
 namespace tempest {
     namespace shields {
+        std::string shieldFilename(std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression) {
+            std::stringstream filename;
+            filename << shieldingExpression->typeToString() << "_";
+            filename << shieldingExpression->comparisonToString();
+            filename << shieldingExpression->getValue() << ".shield";
+            return filename.str();
+        }
+
         template<typename ValueType, typename IndexType = storm::storage::sparse::state_type>
-        storm::storage::Scheduler<ValueType> createShield(std::vector<IndexType> const& rowGroupIndices, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates) {
+        void createShield(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates) {
+            std::ofstream stream;
+            storm::utility::openFile(shieldFilename(shieldingExpression), stream);
             if(shieldingExpression->isPreSafetyShield()) {
-                PreSafetyShield<ValueType, IndexType> shield(rowGroupIndices, choiceValues, shieldingExpression, relevantStates, coalitionStates);
-                return shield.construct();
+                PreSafetyShield<ValueType, IndexType> shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, relevantStates, coalitionStates);
+                shield.construct().printToStream(stream, model);
             } else if(shieldingExpression->isPostSafetyShield()) {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot create post safety shields yet");
+                PostSafetyShield<ValueType, IndexType> shield(model->getTransitionMatrix().getRowGroupIndices(), choiceValues, shieldingExpression, relevantStates, coalitionStates);
+                shield.construct().printToStream(stream, model);
             } else if(shieldingExpression->isOptimalShield()) {
+                storm::utility::closeFile(stream);
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot create optimal shields yet");
             }
+            storm::utility::closeFile(stream);
         }
     }
 }