#include "storm/shields/PostSafetyShield.h" #include namespace tempest { namespace shields { template PostSafetyShield::PostSafetyShield(std::vector const& rowGroupIndices, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::storage::BitVector relevantStates, boost::optional coalitionStates) : AbstractShield(rowGroupIndices, choiceValues, shieldingExpression, relevantStates, coalitionStates) { // Intentionally left empty. } template storm::storage::PostScheduler PostSafetyShield::construct() { storm::storage::PostScheduler shield(this->rowGroupIndices.size() - 1, this->computeRowGroupSizes()); STORM_LOG_DEBUG(this->rowGroupIndices.size()); STORM_LOG_DEBUG(this->relevantStates); STORM_LOG_DEBUG(this->coalitionStates.get()); for(auto const& x : this->choiceValues) { STORM_LOG_DEBUG(x << ","); } auto choice_it = this->choiceValues.begin(); if(this->coalitionStates.is_initialized()) { this->relevantStates &= this->coalitionStates.get(); } STORM_LOG_DEBUG(this->relevantStates); for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) { if(this->relevantStates.get(state)) { 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); for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { STORM_LOG_DEBUG("processing " << state << " with rowGroupSize of " << rowGroupSize << " choice index " << choice << " prob: " << *choice_it << " > " << maxProbability); storm::storage::Distribution actionDistribution; if(allowedValue(maxProbability, *choice_it, this->shieldingExpression)) { actionDistribution.addProbability(choice, 1); } else { actionDistribution.addProbability(maxProbabilityIndex, 1); } actionDistribution.normalize(); STORM_LOG_DEBUG(" dist: " << actionDistribution); shield.setChoice(choice, storm::storage::SchedulerChoice(actionDistribution), state); } } else { shield.setChoice(0, storm::storage::Distribution(), state); } } return shield; } // Explicitly instantiate appropriate template class PostSafetyShield::index_type>; #ifdef STORM_HAVE_CARL template class PostSafetyShield::index_type>; #endif } }