From 6d5f4dc9c924985e7e0879a480750c1b8e4f70a9 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 19 Aug 2016 08:56:59 +0200
Subject: [PATCH] fixed bug in detection whether parameters are only used in
 probabilities/rewards

Former-commit-id: 1929f5e079a03863d9b838043070be4ffe640314
---
 src/storage/prism/Constant.cpp | 7 ++++++-
 src/storage/prism/Module.cpp   | 4 +++-
 src/storage/prism/Program.cpp  | 6 ++++--
 3 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp
index 0416dc4b9..1c3b07057 100644
--- a/src/storage/prism/Constant.cpp
+++ b/src/storage/prism/Constant.cpp
@@ -42,7 +42,12 @@ namespace storm {
         }
         
         std::ostream& operator<<(std::ostream& stream, Constant const& constant) {
-            stream << "const " << constant.getExpressionVariable().getType() << " ";
+            stream << "const ";
+            if (constant.getType().isRationalType()) {
+                stream << "double" << " ";
+            } else {
+                stream << constant.getType() << " ";
+            }
             stream << constant.getName();
             if (constant.isDefined()) {
                 stream << " = " << constant.getExpression();
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index d4168196d..7b929edfc 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -216,7 +216,9 @@ namespace storm {
             }
             
             for (auto const& command : this->getCommands()) {
-                command.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables);
+                if (!command.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables)) {
+                    return false;
+                }
             }
             
             return true;
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index c1a1e4cf0..4962157eb 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -230,7 +230,7 @@ namespace storm {
             // constants' variables is empty (except for the update probabilities).
             
             // Start by checking the defining expressions of all defined constants. If it contains a currently undefined
-            //constant, we need to mark the target constant as undefined as well.
+            // constant, we need to mark the target constant as undefined as well.
             for (auto const& constant : this->getConstants()) {
                 if (constant.isDefined()) {
                     if (constant.getExpression().containsVariable(undefinedConstantVariables)) {
@@ -266,7 +266,9 @@ namespace storm {
             
             // Proceed by checking each of the modules.
             for (auto const& module : this->getModules()) {
-                module.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables);
+                if (!module.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables)) {
+                    return false;
+                }
             }
             
             // Check the reward models.