diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index d035f6fd7..10de545e3 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -80,6 +80,7 @@ namespace storm { storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(this->_transitionMatrix.getRowCount(), true)}; // under approximation + if (!_multiplier) { prepareSolversAndMultipliers(env); } @@ -100,28 +101,26 @@ namespace storm { storage::SparseMatrix restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions); _multiplierRestricted = storm::solver::MultiplierFactory().create(env, restrictedTransMatrix); - // storage::SparseMatrix restrictedBackMatrix = this->_backwardTransitions.restrictRows(reducedMinimizerActions); // STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); // find_MSECs() & deflate() - storm::storage::MaximalEndComponentDecomposition MECD = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, _backwardTransitions); + storm::storage::MaximalEndComponentDecomposition MSEC = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, _backwardTransitions); // STORM_LOG_DEBUG("MECD: \n" << MECD); - deflate(MECD,restrictedTransMatrix, xNewU()); + deflate(MSEC,restrictedTransMatrix, xNewU()); } template - void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU) { + void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MSEC, storage::SparseMatrix const restrictedMatrix, std::vector& xU) { auto rowGroupIndices = restrictedMatrix.getRowGroupIndices(); // iterating over all MSECs - for (auto smec_it : MECD) { + for (auto smec_it : MSEC) { ValueType bestExit = 0; - for (uint state = 0; state < rowGroupIndices.size() - 1; state++) { + auto stateSet = smec_it.getStateSet(); + for (uint state : stateSet) { uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; - if (!_minimizerStates[state] && smec_it.containsState(state)) { // check if current state is maximizer state - // getting the optimal minimizer choice for the given state - + if (!_minimizerStates[state]) { // check if current state is maximizer state for (uint choice = 0; choice < rowGroupSize; choice++) { if (!smec_it.containsChoice(state, choice + rowGroupIndices[state])) { ValueType choiceValue = 0; @@ -132,11 +131,10 @@ namespace storm { } } } - auto stateSet = smec_it.getStateSet(); - for (auto smec_state : stateSet) - { - if (!_psiStates[smec_state]) - xU[smec_state] = std::min(xU[smec_state], bestExit); + // deflating the states of the current MSEC + for (uint state : stateSet) { + if (!_psiStates[state]) + xU[state] = std::min(xU[state], bestExit); } } } @@ -149,10 +147,6 @@ namespace storm { auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); auto choice_it = choiceValues.begin(); - STORM_LOG_DEBUG("MinStates " << _minimizerStates); - STORM_LOG_DEBUG("init choiceVal " << choiceValues); - - for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; ValueType optChoice;