From f605ec28e3e1f5a4a88205e556a420c098fafe67 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Mon, 1 Mar 2021 19:50:56 +0100 Subject: [PATCH] fixed bug in safety shield creation --- src/storm/shields/PreSafetyShield.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/storm/shields/PreSafetyShield.cpp b/src/storm/shields/PreSafetyShield.cpp index a87aa940b..98d32ded7 100644 --- a/src/storm/shields/PreSafetyShield.cpp +++ b/src/storm/shields/PreSafetyShield.cpp @@ -12,7 +12,7 @@ namespace tempest { template storm::storage::Scheduler PreSafetyShield::construct() { - storm::storage::Scheduler shield(this->rowGroupIndices.size()); + storm::storage::Scheduler 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 actionDistribution; ValueType maxProbability = *std::max_element(this->choiceValues.begin(), this->choiceValues.begin() + rowGroupSize); for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { if(allowedValue(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(actionDistribution), state); - STORM_LOG_DEBUG("SchedulerChoice: " << storm::storage::SchedulerChoice(actionDistribution)); } else { shield.setChoice(storm::storage::Distribution(), state);