|
@ -12,6 +12,27 @@ namespace tempest { |
|
|
|
|
|
|
|
|
template<typename ValueType, typename IndexType> |
|
|
template<typename ValueType, typename IndexType> |
|
|
storm::storage::Scheduler<ValueType> PreSafetyShield<ValueType, IndexType>::construct() { |
|
|
storm::storage::Scheduler<ValueType> PreSafetyShield<ValueType, IndexType>::construct() { |
|
|
|
|
|
STORM_LOG_DEBUG("PreSafetyShield::construct called"); |
|
|
|
|
|
if (this->getOptimizationDirection() == storm::OptimizationDirection::Minimize) { |
|
|
|
|
|
if(this->shieldingExpression->isRelative()) { |
|
|
|
|
|
return constructWithCompareType<tempest::shields::utility::ChoiceFilter<ValueType, storm::utility::ElementLessEqual<ValueType>, true>>(); |
|
|
|
|
|
} else { |
|
|
|
|
|
return constructWithCompareType<tempest::shields::utility::ChoiceFilter<ValueType, storm::utility::ElementLessEqual<ValueType>, false>>(); |
|
|
|
|
|
} |
|
|
|
|
|
} else { |
|
|
|
|
|
if(this->shieldingExpression->isRelative()) { |
|
|
|
|
|
return constructWithCompareType<tempest::shields::utility::ChoiceFilter<ValueType, storm::utility::ElementGreaterEqual<ValueType>, true>>(); |
|
|
|
|
|
} else { |
|
|
|
|
|
return constructWithCompareType<tempest::shields::utility::ChoiceFilter<ValueType, storm::utility::ElementGreaterEqual<ValueType>, false>>(); |
|
|
|
|
|
} |
|
|
|
|
|
} |
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
template<typename ValueType, typename IndexType> |
|
|
|
|
|
template<typename ChoiceFilter> |
|
|
|
|
|
storm::storage::Scheduler<ValueType> PreSafetyShield<ValueType, IndexType>::constructWithCompareType() { |
|
|
|
|
|
STORM_LOG_DEBUG("PreSafetyShield::constructWithCompareType called"); |
|
|
|
|
|
ChoiceFilter choiceFilter; |
|
|
storm::storage::Scheduler<ValueType> shield(this->rowGroupIndices.size() - 1); |
|
|
storm::storage::Scheduler<ValueType> shield(this->rowGroupIndices.size() - 1); |
|
|
auto choice_it = this->choiceValues.begin(); |
|
|
auto choice_it = this->choiceValues.begin(); |
|
|
if(this->coalitionStates.is_initialized()) { |
|
|
if(this->coalitionStates.is_initialized()) { |
|
@ -22,13 +43,13 @@ namespace tempest { |
|
|
uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; |
|
|
uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; |
|
|
storm::storage::Distribution<ValueType, IndexType> actionDistribution; |
|
|
storm::storage::Distribution<ValueType, IndexType> actionDistribution; |
|
|
ValueType maxProbability = *std::max_element(choice_it, choice_it + rowGroupSize); |
|
|
ValueType maxProbability = *std::max_element(choice_it, choice_it + rowGroupSize); |
|
|
if(!this->allowedValue(maxProbability, maxProbability, this->shieldingExpression)) { |
|
|
|
|
|
|
|
|
if(!choiceFilter(maxProbability, maxProbability, this->shieldingExpression->getValue())) { |
|
|
STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); |
|
|
STORM_LOG_WARN("No shielding action possible with absolute comparison for state with index " << state); |
|
|
shield.setChoice(storm::storage::Distribution<ValueType, IndexType>(), state); |
|
|
shield.setChoice(storm::storage::Distribution<ValueType, IndexType>(), state); |
|
|
continue; |
|
|
continue; |
|
|
} |
|
|
} |
|
|
for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { |
|
|
for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { |
|
|
if(this->allowedValue(maxProbability, *choice_it, this->shieldingExpression)) { |
|
|
|
|
|
|
|
|
if(choiceFilter(*choice_it, maxProbability, this->shieldingExpression->getValue())) { |
|
|
actionDistribution.addProbability(choice, *choice_it); |
|
|
actionDistribution.addProbability(choice, *choice_it); |
|
|
} |
|
|
} |
|
|
} |
|
|
} |
|
@ -39,6 +60,7 @@ namespace tempest { |
|
|
shield.setChoice(storm::storage::Distribution<ValueType, IndexType>(), state); |
|
|
shield.setChoice(storm::storage::Distribution<ValueType, IndexType>(), state); |
|
|
} |
|
|
} |
|
|
} |
|
|
} |
|
|
|
|
|
STORM_LOG_DEBUG("PreSafetyShield::constructWithCompareType done"); |
|
|
return shield; |
|
|
return shield; |
|
|
} |
|
|
} |
|
|
// Explicitly instantiate appropriate
|
|
|
// Explicitly instantiate appropriate
|
|
|