|
|
@ -12,7 +12,7 @@ namespace tempest { |
|
|
|
|
|
|
|
template<typename ValueType, typename IndexType> |
|
|
|
storm::storage::Scheduler<ValueType> PreSafetyShield<ValueType, IndexType>::construct() { |
|
|
|
storm::storage::Scheduler<ValueType> shield(this->rowGroupIndices.size()); |
|
|
|
storm::storage::Scheduler<ValueType> shield(this->rowGroupIndices.size() - 1); |
|
|
|
STORM_LOG_DEBUG(this->rowGroupIndices.size()); |
|
|
|
STORM_LOG_DEBUG(this->relevantStates); |
|
|
|
for(auto const& x : this->choiceValues) { |
|
|
@ -22,18 +22,15 @@ namespace tempest { |
|
|
|
for(uint state = 0; state < this->rowGroupIndices.size() - 1; state++) { |
|
|
|
if(this->relevantStates.get(state)) { |
|
|
|
uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; |
|
|
|
STORM_LOG_DEBUG("rowGroupSize: " << rowGroupSize); |
|
|
|
storm::storage::Distribution<ValueType, IndexType> actionDistribution; |
|
|
|
ValueType maxProbability = *std::max_element(this->choiceValues.begin(), this->choiceValues.begin() + rowGroupSize); |
|
|
|
for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { |
|
|
|
if(allowedValue<ValueType, IndexType>(maxProbability, *choice_it, this->shieldingExpression)) { |
|
|
|
actionDistribution.addProbability(choice, *choice_it); |
|
|
|
STORM_LOG_DEBUG("Adding " << *choice_it << " to dist"); |
|
|
|
} |
|
|
|
} |
|
|
|
actionDistribution.normalize(); |
|
|
|
shield.setChoice(storm::storage::SchedulerChoice<ValueType>(actionDistribution), state); |
|
|
|
STORM_LOG_DEBUG("SchedulerChoice: " << storm::storage::SchedulerChoice<ValueType>(actionDistribution)); |
|
|
|
|
|
|
|
} else { |
|
|
|
shield.setChoice(storm::storage::Distribution<ValueType, IndexType>(), state); |
|
|
|