diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h index 4fe38b0f0..5375a7902 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/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,7 +26,8 @@ namespace storm { public: typedef std::vector vector_type; typedef std::map map_type; - + typedef typename storm::storage::SparseMatrix::index_type IndexType; + ExplicitQuantitativeCheckResult(); ExplicitQuantitativeCheckResult(map_type const& values); ExplicitQuantitativeCheckResult(map_type&& 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>&& scheduler); storm::storage::Scheduler const& getScheduler() const; storm::storage::Scheduler& getScheduler(); + void setShield(std::unique_ptr> shield); + std::shared_ptr> const& getShield() const; + storm::json toJson(boost::optional const& stateValuations = boost::none) const; private: @@ -86,6 +94,8 @@ namespace storm { // An optional scheduler that accompanies the values. boost::optional>> scheduler; + boost::optional>> shield; + }; } } diff --git a/src/storm/shields/AbstractShield.cpp b/src/storm/shields/AbstractShield.cpp index c81ac2ecc..abb57f57e 100644 --- a/src/storm/shields/AbstractShield.cpp +++ b/src/storm/shields/AbstractShield.cpp @@ -39,10 +39,7 @@ namespace tempest { return shieldingExpression->getFilename() + ".shield"; } - template - void AbstractShield::printToStream(std::ostream& out, std::shared_ptr> const& model) const { - // construct().printToStream(out, shieldingExpression, model) - } + // Explicitly instantiate appropriate template class AbstractShield::index_type>; #ifdef STORM_HAVE_CARL diff --git a/src/storm/shields/AbstractShield.h b/src/storm/shields/AbstractShield.h index 3a0ee4dd4..26c2e1c63 100644 --- a/src/storm/shields/AbstractShield.h +++ b/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> const& model) const; + virtual void printToStream(std::ostream& out, std::shared_ptr> const& model) = 0; protected: AbstractShield(std::vector const& rowGroupIndices, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates); diff --git a/src/storm/shields/OptimalShield.cpp b/src/storm/shields/OptimalShield.cpp index b1e35a5c1..d1b5daadb 100644 --- a/src/storm/shields/OptimalShield.cpp +++ b/src/storm/shields/OptimalShield.cpp @@ -64,11 +64,17 @@ namespace tempest { return shield; } + template + void OptimalShield::printToStream(std::ostream& out, std::shared_ptr> const& model) { + this->construct().printToStream(out, this->shieldingExpression, model); + } + // Explicitly instantiate appropriate classes template class OptimalShield::index_type>; #ifdef STORM_HAVE_CARL template class OptimalShield::index_type>; - + // template class OptimalShield::index_type>; + #endif } } diff --git a/src/storm/shields/OptimalShield.h b/src/storm/shields/OptimalShield.h index b7c55712e..bae16d8af 100644 --- a/src/storm/shields/OptimalShield.h +++ b/src/storm/shields/OptimalShield.h @@ -14,6 +14,8 @@ namespace tempest { storm::storage::PostScheduler construct(); template storm::storage::PostScheduler constructWithCompareType(); + virtual void printToStream(std::ostream& out, std::shared_ptr> const& model) override; + private: std::vector choiceValues; }; diff --git a/src/storm/shields/PostShield.cpp b/src/storm/shields/PostShield.cpp index 63eb452d8..150ea94f6 100644 --- a/src/storm/shields/PostShield.cpp +++ b/src/storm/shields/PostShield.cpp @@ -67,11 +67,19 @@ namespace tempest { return shield; } + + template + void PostShield::printToStream(std::ostream& out, std::shared_ptr> const& model) { + this->construct().printToStream(out, this->shieldingExpression, model); + } + + // Explicitly instantiate appropriate classes template class PostShield::index_type>; #ifdef STORM_HAVE_CARL template class PostShield::index_type>; - + // template class PostShield::index_type>; + #endif } } diff --git a/src/storm/shields/PostShield.h b/src/storm/shields/PostShield.h index f2a43905f..85a325f93 100644 --- a/src/storm/shields/PostShield.h +++ b/src/storm/shields/PostShield.h @@ -14,6 +14,9 @@ namespace tempest { storm::storage::PostScheduler construct(); template storm::storage::PostScheduler constructWithCompareType(); + + virtual void printToStream(std::ostream& out, std::shared_ptr> const& model) override; + private: std::vector choiceValues; }; diff --git a/src/storm/shields/PreShield.cpp b/src/storm/shields/PreShield.cpp index 3fad08b82..a4437f3f3 100644 --- a/src/storm/shields/PreShield.cpp +++ b/src/storm/shields/PreShield.cpp @@ -67,11 +67,20 @@ namespace tempest { } return shield; } + + + template + void PreShield::printToStream(std::ostream& out, std::shared_ptr> const& model) { + this->construct().printToStream(out, this->shieldingExpression, model); + } + + // Explicitly instantiate appropriate classes template class PreShield::index_type>; #ifdef STORM_HAVE_CARL template class PreShield::index_type>; - + //template class PreShield::index_type>; + #endif } } diff --git a/src/storm/shields/PreShield.h b/src/storm/shields/PreShield.h index 6e98dd7e8..cdaee54f3 100644 --- a/src/storm/shields/PreShield.h +++ b/src/storm/shields/PreShield.h @@ -14,6 +14,9 @@ namespace tempest { storm::storage::PreScheduler construct(); template storm::storage::PreScheduler constructWithCompareType(); + + virtual void printToStream(std::ostream& out, std::shared_ptr> const& model) override; + private: std::vector choiceValues; };