Browse Source

Refactoring

Former-commit-id: e9af97f7af
tempestpy_adaptions
Mavo 9 years ago
parent
commit
2c172cd082
  1. 9
      src/builder/ExplicitDFTModelBuilder.cpp
  2. 2
      src/models/sparse/MarkovAutomaton.h

9
src/builder/ExplicitDFTModelBuilder.cpp

@ -124,7 +124,7 @@ namespace storm {
} else { } else {
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true); std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true);
if (ma->hasOnlyTrivialNondeterminism()) { if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC
// Markov automaton can be converted into CTMC
model = ma->convertToCTMC(); model = ma->convertToCTMC();
} else { } else {
model = ma; model = ma;
@ -287,8 +287,7 @@ namespace storm {
} else { } else {
// Try to merge pseudo states with their instantiation // Try to merge pseudo states with their instantiation
// TODO Matthias: improve? // 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) { if (it->first >= OFFSET_PSEUDO_STATE) {
uint_fast64_t newId = it->first - OFFSET_PSEUDO_STATE; uint_fast64_t newId = it->first - OFFSET_PSEUDO_STATE;
assert(newId < mPseudoStatesMapping.size()); assert(newId < mPseudoStatesMapping.size());
@ -306,9 +305,7 @@ namespace storm {
STORM_LOG_TRACE("Instantiated pseudo state " << newId << " with rate " << it->second); STORM_LOG_TRACE("Instantiated pseudo state " << newId << " with rate " << it->second);
} }
// Remove pseudo state // Remove pseudo state
auto itErase = it;
++it;
outgoingTransitions.erase(itErase);
it = outgoingTransitions.erase(it);
} else { } else {
++it; ++it;
} }

2
src/models/sparse/MarkovAutomaton.h

@ -56,9 +56,9 @@ namespace storm {
* @param stateLabeling The labeling of the states. * @param stateLabeling The labeling of the states.
* @param markovianStates A bit vector indicating the Markovian states of the automaton. * @param markovianStates A bit vector indicating the Markovian states of the automaton.
* @param exitRates A vector storing the exit rates of the states. * @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 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 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<ValueType>&& transitionMatrix, MarkovAutomaton(storm::storage::SparseMatrix<ValueType>&& transitionMatrix,
storm::models::sparse::StateLabeling&& stateLabeling, storm::models::sparse::StateLabeling&& stateLabeling,

Loading…
Cancel
Save