fixed bug in detection whether parameters are only used in probabilities/rewards

Former-commit-id: 1929f5e079

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

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;

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.