Browse Source

introduced choiceFilter for PostSafetyShields

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
commit
1c3e669efa
  1. 23
      src/storm/shields/PostSafetyShield.cpp
  2. 3
      src/storm/shields/PostSafetyShield.h

23
src/storm/shields/PostSafetyShield.cpp

@ -12,6 +12,25 @@ namespace tempest {
template<typename ValueType, typename IndexType> template<typename ValueType, typename IndexType>
storm::storage::PostScheduler<ValueType> PostSafetyShield<ValueType, IndexType>::construct() { storm::storage::PostScheduler<ValueType> PostSafetyShield<ValueType, IndexType>::construct() {
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::PostScheduler<ValueType> PostSafetyShield<ValueType, IndexType>::constructWithCompareType() {
ChoiceFilter choiceFilter;
storm::storage::PostScheduler<ValueType> shield(this->rowGroupIndices.size() - 1, this->computeRowGroupSizes()); storm::storage::PostScheduler<ValueType> shield(this->rowGroupIndices.size() - 1, this->computeRowGroupSizes());
auto choice_it = this->choiceValues.begin(); auto choice_it = this->choiceValues.begin();
if(this->coalitionStates.is_initialized()) { if(this->coalitionStates.is_initialized()) {
@ -22,14 +41,14 @@ namespace tempest {
uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state]; uint rowGroupSize = this->rowGroupIndices[state + 1] - this->rowGroupIndices[state];
auto maxProbabilityIndex = std::max_element(choice_it, choice_it + rowGroupSize) - choice_it; auto maxProbabilityIndex = std::max_element(choice_it, choice_it + rowGroupSize) - choice_it;
ValueType maxProbability = *(choice_it + maxProbabilityIndex); ValueType maxProbability = *(choice_it + maxProbabilityIndex);
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(0, storm::storage::Distribution<ValueType, IndexType>(), state); shield.setChoice(0, 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++) {
storm::storage::Distribution<ValueType, IndexType> actionDistribution; storm::storage::Distribution<ValueType, IndexType> actionDistribution;
if(this->allowedValue(maxProbability, *choice_it, this->shieldingExpression)) {
if(choiceFilter(*choice_it, maxProbability, this->shieldingExpression->getValue())) {
actionDistribution.addProbability(choice, 1); actionDistribution.addProbability(choice, 1);
} else { } else {
actionDistribution.addProbability(maxProbabilityIndex, 1); actionDistribution.addProbability(maxProbabilityIndex, 1);

3
src/storm/shields/PostSafetyShield.h

@ -10,7 +10,10 @@ namespace tempest {
class PostSafetyShield : public AbstractShield<ValueType, IndexType> { class PostSafetyShield : public AbstractShield<ValueType, IndexType> {
public: public:
PostSafetyShield(std::vector<IndexType> const& rowGroupIndices, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates); PostSafetyShield(std::vector<IndexType> const& rowGroupIndices, std::vector<ValueType> const& choiceValues, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional<storm::storage::BitVector> coalitionStates);
storm::storage::PostScheduler<ValueType> construct(); storm::storage::PostScheduler<ValueType> construct();
template<typename ChoiceFilter>
storm::storage::PostScheduler<ValueType> constructWithCompareType();
}; };
} }
} }
Loading…
Cancel
Save