From 5310793653a683e8929bdfb3c0f2e9cda460f243 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@rwth-aachen.de>
Date: Thu, 9 Jun 2016 00:48:02 +0200
Subject: [PATCH] minor fixes and debug output

Former-commit-id: 67c7c6b362f1c450275b9ec1fe9b0fb7fba7b093
---
 src/logic/FragmentSpecification.cpp                        | 3 ++-
 .../helper/SparseMultiObjectiveModelCheckerHelper.cpp      | 3 ++-
 src/storage/geometry/Halfspace.h                           | 7 ++++++-
 3 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp
index c9dd90e24..bf63e5019 100644
--- a/src/logic/FragmentSpecification.cpp
+++ b/src/logic/FragmentSpecification.cpp
@@ -89,6 +89,7 @@ namespace storm {
             multiObjective.setMultiObjectiveFormulasAllowed(true);
             multiObjective.setProbabilityOperatorsAllowed(true);
             multiObjective.setUntilFormulasAllowed(true);
+            multiObjective.setGloballyFormulasAllowed(true);
             multiObjective.setReachabilityProbabilityFormulasAllowed(true);
             multiObjective.setRewardOperatorsAllowed(true);
             multiObjective.setReachabilityRewardFormulasAllowed(true);
@@ -466,4 +467,4 @@ namespace storm {
         }
         
     }
-}
\ No newline at end of file
+}
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp
index c57b41215..c29e112c0 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp
@@ -94,7 +94,7 @@ namespace storm {
                 }
                 STORM_LOG_ASSERT(optimizingObjIndex < info.objectives.size(), "Numerical Query invoked but there are no objectives without threshold");
                 auto thresholdsAsPolytope = storm::storage::geometry::Polytope<RationalNumberType>::create(thresholdConstraints);
-                WeightVector directionOfOptimizingObjective(info.objectives.size());
+                WeightVector directionOfOptimizingObjective(info.objectives.size(), storm::utility::zero<RationalNumberType>());
                 directionOfOptimizingObjective[optimizingObjIndex] = storm::utility::one<RationalNumberType>();
                 
                 // Try to find one valid solution
@@ -187,6 +187,7 @@ namespace storm {
             
                 storm::storage::TotalScheduler scheduler = weightedObjectivesChecker.getScheduler();
                 Point weightedObjectivesResult = storm::utility::vector::convertNumericVector<RationalNumberType>(weightedObjectivesChecker.getInitialStateResultOfObjectives());
+                STORM_LOG_DEBUG("Result with weighted objectives is " << storm::utility::vector::toString(weightedObjectivesResult));
                 
                 // Insert the computed scheduler and check whether we have already seen it before
                 auto schedulerInsertRes = schedulers.insert(std::make_pair(std::move(scheduler), paretoOptimalPoints.end()));
diff --git a/src/storage/geometry/Halfspace.h b/src/storage/geometry/Halfspace.h
index eb2bdbdcb..64c0cd8a0 100644
--- a/src/storage/geometry/Halfspace.h
+++ b/src/storage/geometry/Halfspace.h
@@ -73,7 +73,12 @@ namespace storm {
                         }
                         stream << std::setw(10) << numberStream.str();
                     }
-                    stream << ") * x <= " << offset();
+                    stream << ") * x <= ";
+                    if(numbersAsDouble) {
+                        stream << storm::utility::convertNumber<double>(offset());
+                    } else {
+                        stream << offset();
+                    }
                     return stream.str();
                 }