From 748e100aadaaa91d0c0833b8c525754b9715eb33 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 5 May 2017 15:54:04 +0200
Subject: [PATCH] fixed/improved .dot output for MAs and Mdps. We now also
display the index of each choice.
---
src/storm/models/sparse/MarkovAutomaton.cpp | 13 +++++++------
src/storm/models/sparse/NondeterministicModel.cpp | 11 ++++++-----
2 files changed, 13 insertions(+), 11 deletions(-)
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) {