diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp index 3e4dfaa69..2b76f9eee 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp @@ -2,9 +2,6 @@ #include "storm/modelchecker/helper/infinitehorizon/internal/ComponentUtility.h" -#include "storm/solver/LinearEquationSolver.h" -#include "storm/solver/MinMaxLinearEquationSolver.h" -#include "storm/solver/Multiplier.h" #include "storm/storage/MaximalEndComponent.h" #include "storm/storage/StronglyConnectedComponent.h" @@ -97,7 +94,7 @@ namespace storm { } ValueType selfLoopProb = storm::utility::one() - uniformizationFactor; uint64_t selfLoopColumn = toSubModelStateMapping[componentState]; - for (auto componentChoiceIt = getComponentChoicesBegin(element); componentChoiceIt != getComponentChoicesEnd(element); ++componentChoiceIt) { + for (auto componentChoiceIt = getComponentElementChoicesBegin(element); componentChoiceIt != getComponentElementChoicesEnd(element); ++componentChoiceIt) { bool insertedDiagElement = false; for (auto const& entry : this->_transitionMatrix.getRow(*componentChoiceIt)) { uint64_t subModelColumn = toSubModelStateMapping[entry.getColumn()]; @@ -135,7 +132,7 @@ namespace storm { isTransitionsBuilder.newRowGroup(currIsRow); isToTsTransitionsBuilder.newRowGroup(currIsRow); } - for (auto componentChoiceIt = getComponentChoicesBegin(element); componentChoiceIt != getComponentChoicesEnd(element); ++componentChoiceIt) { + for (auto componentChoiceIt = getComponentElementChoicesBegin(element); componentChoiceIt != getComponentElementChoicesEnd(element); ++componentChoiceIt) { for (auto const& entry : this->_transitionMatrix.getRow(*componentChoiceIt)) { uint64_t subModelColumn = toSubModelStateMapping[entry.getColumn()]; if (isTimedState(entry.getColumn())) { @@ -226,12 +223,12 @@ namespace storm { if (exitRates) { actionRewardScalingFactor = (*exitRates)[componentState] / _uniformizationRate; } - for (auto componentChoiceIt = getComponentChoicesBegin(element); componentChoiceIt != getComponentChoicesEnd(element); ++componentChoiceIt) { + for (auto componentChoiceIt = getComponentElementChoicesBegin(element); componentChoiceIt != getComponentElementChoicesEnd(element); ++componentChoiceIt) { // Compute the values obtained for this choice. _TsChoiceValues.push_back(stateValueGetter(componentState) / _uniformizationRate + actionValueGetter(*componentChoiceIt) * actionRewardScalingFactor); } } else { - for (auto componentChoiceIt = getComponentChoicesBegin(element); componentChoiceIt != getComponentChoicesEnd(element); ++componentChoiceIt) { + for (auto componentChoiceIt = getComponentElementChoicesBegin(element); componentChoiceIt != getComponentElementChoicesEnd(element); ++componentChoiceIt) { // Compute the values obtained for this choice. // State values do not count here since no time passes in instant states. _IsChoiceValues.push_back(actionValueGetter(*componentChoiceIt)); @@ -329,7 +326,7 @@ namespace storm { } else { uint64_t choice = localMecChoices[localState]; STORM_LOG_ASSERT(choice < getComponentElementChoiceCount(element), "The selected choice does not seem to exist."); - uint64_t globalChoiceIndex = *(getComponentChoicesBegin(element) + choice); + uint64_t globalChoiceIndex = *(getComponentElementChoicesBegin(element) + choice); choices[elementState] = globalChoiceIndex - _transitionMatrix.getRowGroupIndices()[elementState]; ++localState; } diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h index 3fb5066c4..7cb62e9a6 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h @@ -2,15 +2,13 @@ #include "storm/storage/SparseMatrix.h" +#include "storm/solver/LinearEquationSolver.h" +#include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/Multiplier.h" namespace storm { class Environment; - namespace solver { - template class LinearEquationSolver; - template class MinMaxLinearEquationSolver; - template class Multiplier; - } namespace modelchecker { namespace helper {