diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index bdee4eedc..25daedf7a 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -138,22 +138,13 @@ namespace storm { } std::shared_ptr> model; - + storm::storage::sparse::ModelComponents components(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); + components.exitRates = std::move(modelComponents.exitRates); if (deterministic) { - // Turn the probabilities into rates by multiplying each row with the exit rate of the state. - // TODO Matthias: avoid transforming back and forth - storm::storage::SparseMatrix rateMatrix(modelComponents.transitionMatrix); - for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) { - STORM_LOG_ASSERT(row < modelComponents.markovianStates.size(), "Row exceeds no. of markovian states."); - if (modelComponents.markovianStates.get(row)) { - for (auto& entry : rateMatrix.getRow(row)) { - entry.setValue(entry.getValue() * modelComponents.exitRates[row]); - } - } - } - model = std::make_shared>(std::move(rateMatrix), std::move(modelComponents.exitRates), std::move(modelComponents.stateLabeling)); + model = std::make_shared>(std::move(components)); } 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); + components.markovianStates = std::move(modelComponents.markovianStates); + std::shared_ptr> ma = std::make_shared>(std::move(components)); if (ma->hasOnlyTrivialNondeterminism()) { // Markov automaton can be converted into CTMC model = ma->convertToCTMC(); diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp index 84eaa21a7..0c7d69628 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp @@ -525,7 +525,11 @@ namespace storm { } STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates); - std::shared_ptr> ma = std::make_shared>(std::move(matrix), std::move(labeling), modelComponents.markovianStates, modelComponents.exitRates); + storm::storage::sparse::ModelComponents maComponents(std::move(matrix), std::move(labeling)); + maComponents.rateTransitions = true; + maComponents.markovianStates = modelComponents.markovianStates; + maComponents.exitRates = modelComponents.exitRates; + std::shared_ptr> ma = std::make_shared>(std::move(maComponents)); if (ma->hasOnlyTrivialNondeterminism()) { // Markov automaton can be converted into CTMC // TODO Matthias: change components which were not moved accordingly @@ -573,9 +577,17 @@ namespace storm { std::shared_ptr> ma; if (copy) { - ma = std::make_shared>(modelComponents.transitionMatrix, modelComponents.stateLabeling, modelComponents.markovianStates, modelComponents.exitRates); + storm::storage::sparse::ModelComponents maComponents(modelComponents.transitionMatrix, modelComponents.stateLabeling); + maComponents.rateTransitions = true; + maComponents.markovianStates = modelComponents.markovianStates; + maComponents.exitRates = modelComponents.exitRates; + std::shared_ptr> ma = std::make_shared>(std::move(maComponents)); } else { - ma = std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates)); + storm::storage::sparse::ModelComponents maComponents(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); + maComponents.rateTransitions = true; + maComponents.markovianStates = std::move(modelComponents.markovianStates); + maComponents.exitRates = std::move(modelComponents.exitRates); + std::shared_ptr> ma = std::make_shared>(std::move(maComponents)); } if (ma->hasOnlyTrivialNondeterminism()) { // Markov automaton can be converted into CTMC