diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 277366bd5..aa34218ce 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -99,6 +99,7 @@ class AbstractDeterministicModel: public AbstractModel { virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override { AbstractModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); + // Simply iterate over all transitions and draw the arrows with probability information attached. for (auto const& transition : this->transitionMatrix) { if (transition.value() != storm::utility::constGetZero()) { if (subsystem == nullptr || subsystem->get(transition.column())) { diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 3821fe185..52d481a90 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -408,11 +408,14 @@ protected: virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const { outStream << "digraph deterministicModel {" << std::endl; + // Write all states to the stream. for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { if (subsystem == nullptr || subsystem->get(state)) { outStream << "\t" << state; if (includeLabeling || firstValue != nullptr || secondValue != nullptr || stateColoring != nullptr) { outStream << " [ "; + + // If we need to print some extra information, do so now. if (includeLabeling || firstValue != nullptr || secondValue != nullptr) { outStream << "label = \"" << state << ": "; @@ -459,6 +462,7 @@ protected: } } + // If this methods has not been called from a derived class, we want to close the digraph here. if (finalizeOutput) { outStream << "}" << std::endl; } diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 4515a7a2c..10ab8bfdd 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -149,9 +149,12 @@ class AbstractNondeterministicModel: public AbstractModel { typename storm::storage::SparseMatrix::ConstRowsIterator transitionIt = this->getTransitionMatrix().begin(); typename storm::storage::SparseMatrix::ConstRowsIterator transitionIte = this->getTransitionMatrix().begin(); + // Write the probability distributions for all the states. for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { uint_fast64_t rowCount = nondeterministicChoiceIndices[state + 1] - nondeterministicChoiceIndices[state]; bool highlightChoice = true; + + // For this, we need to iterate over all available nondeterministic choices in the current state. for (uint_fast64_t row = 0; row < rowCount; ++row) { if (scheduler != nullptr) { // If the scheduler picked the current choice, we will not make it dotted, but highlight it.