From 41db9a80926a68ee83a0ab3804833b3734546beb Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 17 Jun 2013 19:24:34 +0200
Subject: [PATCH] Small changes to MDP model checker.

Former-commit-id: df85f5586689a38749c46f2437ae57f07834f0c6
---
 src/models/AbstractDeterministicModel.h    | 1 +
 src/models/AbstractModel.h                 | 4 ++++
 src/models/AbstractNondeterministicModel.h | 3 +++
 3 files changed, 8 insertions(+)

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<T> {
         virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<T> const* firstValue = nullptr, std::vector<T> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const override {
             AbstractModel<T>::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<T>()) {
                     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<T> const* firstValue = nullptr, std::vector<T> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* 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<T> {
             typename storm::storage::SparseMatrix<T>::ConstRowsIterator transitionIt = this->getTransitionMatrix().begin();
             typename storm::storage::SparseMatrix<T>::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.