From 2c172cd0827e33609cb7209a3e88b6ffac5abec8 Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 17 Mar 2016 11:55:40 +0100 Subject: [PATCH] Refactoring Former-commit-id: e9af97f7afd148d23f1667ce82f12cfba63d4881 --- src/builder/ExplicitDFTModelBuilder.cpp | 9 +++------ src/models/sparse/MarkovAutomaton.h | 2 +- 2 files changed, 4 insertions(+), 7 deletions(-) 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,