diff --git a/src/storm/shields/AbstractShield.cpp b/src/storm/shields/AbstractShield.cpp new file mode 100644 index 000000000..41322b837 --- /dev/null +++ b/src/storm/shields/AbstractShield.cpp @@ -0,0 +1,31 @@ +#include "storm/shields/AbstractShield.h" + +#include +namespace tempest { + namespace shields { + + template + AbstractShield::AbstractShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, boost::optional coalitionStates) : rowGroupIndices(rowGroupIndices), choiceValues(choiceValues), shieldingExpression(shieldingExpression), coalitionStates(coalitionStates) { + // Intentionally left empty. + } + + template + AbstractShield::~AbstractShield() { + // Intentionally left empty. + } + + template + std::string AbstractShield::getClassName() const { + return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*this))); + } + + // Explicitly instantiate appropriate + template class AbstractShield::index_type>; + template class AbstractShield::index_type>; + template class AbstractShield::index_type>; + template class AbstractShield::index_type>; +#ifdef STORM_HAVE_CARL + template class AbstractShield::index_type>; +#endif + } +} diff --git a/src/storm/shields/AbstractShield.h b/src/storm/shields/AbstractShield.h new file mode 100644 index 000000000..cc7fe9ca6 --- /dev/null +++ b/src/storm/shields/AbstractShield.h @@ -0,0 +1,44 @@ +#pragma once + +#include +#include +#include + +#include "storm/storage/Scheduler.h" +#include "storm/storage/BitVector.h" + +#include "storm/logic/ShieldExpression.h" + +namespace tempest { + namespace shields { + + template + class AbstractShield { + public: + typedef IndexType index_type; + typedef ValueType value_type; + + virtual ~AbstractShield() = 0; + + /*! + * TODO + */ + virtual storm::storage::Scheduler construct() = 0; + + /*! + * TODO + */ + std::string getClassName() const; + + protected: + AbstractShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, boost::optional coalitionStates); + + std::vector rowGroupIndices; + std::vector choiceValues; + + std::shared_ptr shieldingExpression; + + boost::optional coalitionStates; + }; + } +} diff --git a/src/storm/shields/PreSafetyShield.cpp b/src/storm/shields/PreSafetyShield.cpp new file mode 100644 index 000000000..5b45e8b7f --- /dev/null +++ b/src/storm/shields/PreSafetyShield.cpp @@ -0,0 +1,30 @@ +#include "storm/shields/PreSafetyShield.h" + +namespace tempest { + namespace shields { + + template + PreSafetyShield::PreSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, choiceValues, shieldingExpression, coalitionStates) { + // Intentionally left empty. + } + + template + storm::storage::Scheduler PreSafetyShield::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::index_type>; + template class PreSafetyShield::index_type>; + template class PreSafetyShield::index_type>; + template class PreSafetyShield::index_type>; +#ifdef STORM_HAVE_CARL + template class PreSafetyShield::index_type>; +#endif + } +} diff --git a/src/storm/shields/PreSafetyShield.h b/src/storm/shields/PreSafetyShield.h new file mode 100644 index 000000000..0dbcb6906 --- /dev/null +++ b/src/storm/shields/PreSafetyShield.h @@ -0,0 +1,15 @@ +#pragma once + +#include "storm/shields/AbstractShield.h" + +namespace tempest { + namespace shields { + + template + class PreSafetyShield : public AbstractShield { + public: + PreSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, boost::optional coalitionStates); + storm::storage::Scheduler construct(); + }; + } +}