diff --git a/src/storm/shields/AbstractShield.cpp b/src/storm/shields/AbstractShield.cpp index 2722b1916..f24189bf5 100644 --- a/src/storm/shields/AbstractShield.cpp +++ b/src/storm/shields/AbstractShield.cpp @@ -24,6 +24,11 @@ namespace tempest { return rowGroupSizes; } + template + bool AbstractShield::allowedValue(ValueType const& max, ValueType const& v, std::shared_ptr const shieldExpression) { + return shieldExpression->isRelative() ? v >= shieldExpression->getValue() * max : v >= shieldExpression->getValue(); + } + template std::string AbstractShield::getClassName() const { return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*this))); diff --git a/src/storm/shields/AbstractShield.h b/src/storm/shields/AbstractShield.h index 3dfcc2b1b..3a8706157 100644 --- a/src/storm/shields/AbstractShield.h +++ b/src/storm/shields/AbstractShield.h @@ -26,9 +26,13 @@ namespace tempest { /*! * TODO */ - //virtual storm::storage::Scheduler* construct() = 0; std::vector computeRowGroupSizes(); + /*! + * TODO + */ + bool allowedValue(ValueType const& max, ValueType const& v, std::shared_ptr const shieldExpression); + /*! * TODO */ @@ -46,10 +50,5 @@ namespace tempest { boost::optional coalitionStates; }; - - template - bool allowedValue(ValueType const& max, ValueType const& v, std::shared_ptr const shieldExpression) { - return shieldExpression->isRelative() ? v >= shieldExpression->getValue() * max : v >= shieldExpression->getValue(); - } } } diff --git a/src/storm/shields/PostSafetyShield.cpp b/src/storm/shields/PostSafetyShield.cpp index 6b5773854..26494ff29 100644 --- a/src/storm/shields/PostSafetyShield.cpp +++ b/src/storm/shields/PostSafetyShield.cpp @@ -22,14 +22,14 @@ namespace tempest { uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; auto maxProbabilityIndex = std::max_element(choice_it, choice_it + rowGroupSize) - choice_it; ValueType maxProbability = *(choice_it + maxProbabilityIndex); - if(!allowedValue(maxProbability, maxProbability, this->shieldingExpression)) { + if(!this->allowedValue(maxProbability, maxProbability, this->shieldingExpression)) { STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); shield.setChoice(0, storm::storage::Distribution(), state); continue; } for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { storm::storage::Distribution actionDistribution; - if(allowedValue(maxProbability, *choice_it, this->shieldingExpression)) { + if(this->allowedValue(maxProbability, *choice_it, this->shieldingExpression)) { actionDistribution.addProbability(choice, 1); } else { actionDistribution.addProbability(maxProbabilityIndex, 1); diff --git a/src/storm/shields/PreSafetyShield.cpp b/src/storm/shields/PreSafetyShield.cpp index fb63387d7..694362d2d 100644 --- a/src/storm/shields/PreSafetyShield.cpp +++ b/src/storm/shields/PreSafetyShield.cpp @@ -22,13 +22,13 @@ namespace tempest { uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; storm::storage::Distribution actionDistribution; ValueType maxProbability = *std::max_element(choice_it, choice_it + rowGroupSize); - if(!allowedValue(maxProbability, maxProbability, this->shieldingExpression)) { + if(!this->allowedValue(maxProbability, maxProbability, this->shieldingExpression)) { STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); shield.setChoice(storm::storage::Distribution(), state); continue; } for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { - if(allowedValue(maxProbability, *choice_it, this->shieldingExpression)) { + if(this->allowedValue(maxProbability, *choice_it, this->shieldingExpression)) { actionDistribution.addProbability(choice, *choice_it); } }