From 816f12f2f6099f1136aba402cb94deec8676366a Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 16 Sep 2013 20:31:48 +0200
Subject: [PATCH] Added global variables to string output of probabilistic
 program. Added number of choices to model information output of
 nondeterministic models.

Former-commit-id: 63f2b9da7ab3b92d5da5b2926fb44845f70af2a3
---
 src/ir/Program.cpp                         |  8 ++++++++
 src/models/AbstractModel.h                 |  2 +-
 src/models/AbstractNondeterministicModel.h | 15 +++++++++++++++
 3 files changed, 24 insertions(+), 1 deletion(-)

diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp
index eb21aa9f2..14a6af59a 100644
--- a/src/ir/Program.cpp
+++ b/src/ir/Program.cpp
@@ -83,6 +83,14 @@ namespace storm {
             }
             result << std::endl;
             
+            for (auto const& element : globalBooleanVariables) {
+                result << "global " << element.toString() << std::endl;
+            }
+            for (auto const& element : globalIntegerVariables) {
+                result << "global " << element.toString() << std::endl;
+            }
+            result << std::endl;
+            
             for (auto const& module : modules) {
                 result << module.toString() << std::endl;
             }
diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h
index 7790bd7b9..760fb6cc5 100644
--- a/src/models/AbstractModel.h
+++ b/src/models/AbstractModel.h
@@ -416,7 +416,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
          * Prints information about the model to the specified stream.
          * @param out The stream the information is to be printed to.
          */
-        void printModelInformationToStream(std::ostream& out) const {
+        virtual void printModelInformationToStream(std::ostream& out) const {
             out << "-------------------------------------------------------------- " << std::endl;
             out << "Model type: \t\t" << this->getType() << std::endl;
             out << "States: \t\t" << this->getNumberOfStates() << std::endl;
diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h
index 013ab5448..516238e14 100644
--- a/src/models/AbstractNondeterministicModel.h
+++ b/src/models/AbstractNondeterministicModel.h
@@ -137,6 +137,21 @@ class AbstractNondeterministicModel: public AbstractModel<T> {
 			return result;
 		}
 
+        /*!
+         * Prints information about the model to the specified stream.
+         * @param out The stream the information is to be printed to.
+         */
+        virtual void printModelInformationToStream(std::ostream& out) const override {
+            out << "-------------------------------------------------------------- " << std::endl;
+            out << "Model type: \t\t" << this->getType() << std::endl;
+            out << "States: \t\t" << this->getNumberOfStates() << std::endl;
+            out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
+            out << "Choices: \t\t" << this->getNumberOfChoices() << std::endl;
+            this->getStateLabeling().printAtomicPropositionsInformationToStream(out);
+            out << "Size in memory: \t" << (this->getSizeInMemory())/1024 << " kbytes" << std::endl;
+            out << "-------------------------------------------------------------- " << std::endl;
+        }
+    
         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);