init first shield implementation

4 years ago · 359f20b17d
4 changed files with 120 additions and 0 deletions
--- a/src/storm/shields/AbstractShield.cpp
+++ b/src/storm/shields/AbstractShield.cpp
@ -0,0 +1,31 @@
+#include "storm/shields/AbstractShield.h"
+
+#include <boost/core/typeinfo.hpp>
+namespace tempest {
+    namespace shields {
+
+        template<typename ValueType, typename IndexType>
+        AbstractShield<ValueType, IndexType>::AbstractShield(std::vector<IndexType> const& rowGroupIndices, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, boost::optional<storm::storage::BitVector> coalitionStates) : rowGroupIndices(rowGroupIndices), choiceValues(choiceValues), shieldingExpression(shieldingExpression), coalitionStates(coalitionStates) {
+            // Intentionally left empty.
+        }
+
+        template<typename ValueType, typename IndexType>
+        AbstractShield<ValueType, IndexType>::~AbstractShield() {
+            // Intentionally left empty.
+        }
+
+        template<typename ValueType, typename IndexType>
+        std::string AbstractShield<ValueType, IndexType>::getClassName() const {
+            return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*this)));
+        }
+
+        // Explicitly instantiate appropriate
+        template class AbstractShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
+        template class AbstractShield<float, typename storm::storage::SparseMatrix<float>::index_type>;
+        template class AbstractShield<int, typename storm::storage::SparseMatrix<int>::index_type>;
+        template class AbstractShield<storm::storage::sparse::state_type, typename storm::storage::SparseMatrix<storm::storage::sparse::state_type>::index_type>;
+#ifdef STORM_HAVE_CARL
+        template class AbstractShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
+#endif
+    }
+}
--- a/src/storm/shields/AbstractShield.h
+++ b/src/storm/shields/AbstractShield.h
@ -0,0 +1,44 @@
+#pragma once
+
+#include <boost/optional.hpp>
+#include <iostream>
+#include <string>
+
+#include "storm/storage/Scheduler.h"
+#include "storm/storage/BitVector.h"
+
+#include "storm/logic/ShieldExpression.h"
+
+namespace tempest {
+    namespace shields {
+
+        template<typename ValueType, typename IndexType>
+        class AbstractShield {
+        public:
+            typedef IndexType index_type;
+            typedef ValueType value_type;
+
+            virtual ~AbstractShield() = 0;
+
+            /*!
+             * TODO
+             */
+            virtual storm::storage::Scheduler<ValueType> construct() = 0;
+
+            /*!
+             * TODO
+             */
+            std::string getClassName() const;
+
+        protected:
+            AbstractShield(std::vector<IndexType> const& rowGroupIndices, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, boost::optional<storm::storage::BitVector> coalitionStates);
+
+            std::vector<index_type> rowGroupIndices;
+            std::vector<value_type> choiceValues;
+
+            std::shared_ptr<storm::logic::ShieldExpression const> shieldingExpression;
+
+            boost::optional<storm::storage::BitVector> coalitionStates;
+        };
+    }
+}
--- a/src/storm/shields/PreSafetyShield.cpp
+++ b/src/storm/shields/PreSafetyShield.cpp
@ -0,0 +1,30 @@
+#include "storm/shields/PreSafetyShield.h"
+
+namespace tempest {
+    namespace shields {
+
+        template<typename ValueType, typename IndexType>
+        PreSafetyShield<ValueType, IndexType>::PreSafetyShield(std::vector<IndexType> const& rowGroupIndices, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, boost::optional<storm::storage::BitVector> coalitionStates) : AbstractShield<ValueType, IndexType>(rowGroupIndices, choiceValues, shieldingExpression, coalitionStates) {
+            // Intentionally left empty.
+        }
+
+        template<typename ValueType, typename IndexType>
+        storm::storage::Scheduler<ValueType> PreSafetyShield<ValueType, IndexType>::construct() {
+            for(auto const& x: this->rowGroupIndices) {
+                STORM_LOG_DEBUG(x << ", ");
+            }
+            for(auto const& x: this->choiceValues) {
+                STORM_LOG_DEBUG(x << ", ");
+            }
+            STORM_LOG_ASSERT(false, "construct NYI");
+        }
+        // Explicitly instantiate appropriate
+        template class PreSafetyShield<double, typename storm::storage::SparseMatrix<double>::index_type>;
+        template class PreSafetyShield<float, typename storm::storage::SparseMatrix<float>::index_type>;
+        template class PreSafetyShield<int, typename storm::storage::SparseMatrix<int>::index_type>;
+        template class PreSafetyShield<storm::storage::sparse::state_type, typename storm::storage::SparseMatrix<storm::storage::sparse::state_type>::index_type>;
+#ifdef STORM_HAVE_CARL
+        template class PreSafetyShield<storm::RationalNumber, typename storm::storage::SparseMatrix<storm::RationalNumber>::index_type>;
+#endif
+    }
+}
--- a/src/storm/shields/PreSafetyShield.h
+++ b/src/storm/shields/PreSafetyShield.h
@ -0,0 +1,15 @@
+#pragma once
+
+#include "storm/shields/AbstractShield.h"
+
+namespace tempest {
+    namespace shields {
+
+        template<typename ValueType, typename IndexType>
+        class PreSafetyShield : public AbstractShield<ValueType, IndexType> {
+        public:
+            PreSafetyShield(std::vector<IndexType> const& rowGroupIndices, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, boost::optional<storm::storage::BitVector> coalitionStates);
+            storm::storage::Scheduler<ValueType> construct();
+        };
+    }
+}