diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 7f892a822..018e0eb90 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -124,7 +124,7 @@ namespace storm { } else { std::shared_ptr> ma = std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true); if (ma->hasOnlyTrivialNondeterminism()) { - // Markov automaton can be converted into CTMC + // Markov automaton can be converted into CTMC model = ma->convertToCTMC(); } else { model = ma; @@ -287,8 +287,7 @@ namespace storm { } else { // Try to merge pseudo states with their instantiation // TODO Matthias: improve? - auto it = outgoingTransitions.begin(); - while (it != outgoingTransitions.end()) { + for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ) { if (it->first >= OFFSET_PSEUDO_STATE) { uint_fast64_t newId = it->first - OFFSET_PSEUDO_STATE; assert(newId < mPseudoStatesMapping.size()); @@ -306,9 +305,7 @@ namespace storm { STORM_LOG_TRACE("Instantiated pseudo state " << newId << " with rate " << it->second); } // Remove pseudo state - auto itErase = it; - ++it; - outgoingTransitions.erase(itErase); + it = outgoingTransitions.erase(it); } else { ++it; } diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h index 45c8855d9..4251640fc 100644 --- a/src/models/sparse/MarkovAutomaton.h +++ b/src/models/sparse/MarkovAutomaton.h @@ -56,9 +56,9 @@ namespace storm { * @param stateLabeling The labeling of the states. * @param markovianStates A bit vector indicating the Markovian states of the automaton. * @param exitRates A vector storing the exit rates of the states. + * @param probabilities Flag if transitions matrix contains probabilities or rates * @param rewardModels A mapping of reward model names to reward models. * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. - * @param probabilities Flag if transitions matrix contains probabilities or rates */ MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling,