Merge branch 'master' of https://sselab.de/lab9/private/git/storm

Former-commit-id: 14e58fe6d9

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())) {

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;
             }

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.