diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 069ed1936..f0eb0fc39 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -157,7 +157,7 @@ namespace storm { template <typename ValueType, typename RewardModelType> void MarkovAutomaton<ValueType, RewardModelType>::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector<ValueType> const* firstValue, std::vector<ValueType> const* secondValue, std::vector<uint_fast64_t> const* stateColoring, std::vector<std::string> const* colors, std::vector<uint_fast64_t>* scheduler, bool finalizeOutput) const { - NondeterministicModel<ValueType, RewardModelType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); + Model<ValueType, RewardModelType>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); // Write the probability distributions for all the states. for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { @@ -166,7 +166,8 @@ namespace storm { // For this, we need to iterate over all available nondeterministic choices in the current state. for (uint_fast64_t choice = 0; choice < rowCount; ++choice) { - typename storm::storage::SparseMatrix<ValueType>::const_rows row = this->getTransitionMatrix().getRow(this->getTransitionMatrix().getRowGroupIndices()[state] + choice); + uint_fast64_t rowIndex = this->getTransitionMatrix().getRowGroupIndices()[state] + choice; + typename storm::storage::SparseMatrix<ValueType>::const_rows row = this->getTransitionMatrix().getRow(rowIndex); if (scheduler != nullptr) { // If the scheduler picked the current choice, we will not make it dotted, but highlight it. @@ -192,17 +193,17 @@ namespace storm { } outStream << "];" << std::endl; - outStream << "\t" << state << " -> \"" << state << "c" << choice << "\""; + outStream << "\t" << state << " -> \"" << state << "c" << choice << "\" [ label= \"" << rowIndex << "\""; // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { if (highlightChoice) { - outStream << " [color=\"red\", penwidth = 2]"; + outStream << ", color=\"red\", penwidth = 2"; } else { - outStream << " [style = \"dotted\"]"; + outStream << ", style = \"dotted\""; } } - outStream << ";" << std::endl; + outStream << "];" << std::endl; // Now draw all probabilitic arcs that belong to this nondeterminstic choice. for (auto const& transition : row) { diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 8a7a82485..7f221cabe 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -108,7 +108,8 @@ namespace storm { // For this, we need to iterate over all available nondeterministic choices in the current state. for (uint_fast64_t choice = 0; choice < rowCount; ++choice) { - typename storm::storage::SparseMatrix<ValueType>::const_rows row = this->getTransitionMatrix().getRow(this->getNondeterministicChoiceIndices()[state] + choice); + uint_fast64_t rowIndex = this->getNondeterministicChoiceIndices()[state] + choice; + typename storm::storage::SparseMatrix<ValueType>::const_rows row = this->getTransitionMatrix().getRow(rowIndex); if (scheduler != nullptr) { // If the scheduler picked the current choice, we will not make it dotted, but highlight it. @@ -131,17 +132,17 @@ namespace storm { } outStream << "];" << std::endl; - outStream << "\t" << state << " -> \"" << state << "c" << choice << "\""; + outStream << "\t" << state << " -> \"" << state << "c" << choice << "\" [ label= \"" << rowIndex << "\""; // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { if (highlightChoice) { - outStream << " [color=\"red\", penwidth = 2]"; + outStream << ", color=\"red\", penwidth = 2"; } else { - outStream << " [style = \"dotted\"]"; + outStream << ", style = \"dotted\""; } } - outStream << ";" << std::endl; + outStream << "];" << std::endl; // Now draw all probabilitic arcs that belong to this nondeterminstic choice. for (auto const& transition : row) {