From 57882db84ef80109c8991025e325888fc74de0ab Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Wed, 13 Aug 2014 00:28:50 +0200
Subject: [PATCH] Fixed warnings about unused variables in
 PathBasedSubsystemGenerator and SMTMinimalCommandSetGenerator. Also some
 stuff with type conversions.

Fixed the missing include/definition for getcwd


Former-commit-id: 08f82f2ed221357443fff7b34c21e6aefed8f908
---
 src/counterexamples/PathBasedSubsystemGenerator.h   | 7 +++----
 src/counterexamples/SMTMinimalCommandSetGenerator.h | 5 +++--
 src/storm.cpp                                       | 3 ++-
 3 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h
index 2325eebe8..48a175494 100644
--- a/src/counterexamples/PathBasedSubsystemGenerator.h
+++ b/src/counterexamples/PathBasedSubsystemGenerator.h
@@ -588,7 +588,7 @@ public:
 		// estimate the path count using the models state count as well as the probability bound
 		uint_fast8_t const minPrec = 10;
 		uint_fast64_t const stateCount = model.getNumberOfStates();
-		uint_fast64_t const stateEstimate = ((T) stateCount) * bound;
+		uint_fast64_t const stateEstimate = static_cast<uint_fast64_t>(stateCount * bound);
 
 		//since this only has a good effect on big models -> use only if model has at least 10^5 states
 		uint_fast64_t precision = stateEstimate > 100000 ? stateEstimate/1000 : minPrec;
@@ -686,9 +686,8 @@ public:
 				//Are we critical?
 				if(subSysProb >= bound){
 					break;
-				}
-				else if (stateEstimate > 100000){
-					precision = (stateEstimate/1000) - ((stateEstimate/1000) - minPrec)*(subSysProb/bound);
+				} else if (stateEstimate > 100000){
+					precision = static_cast<uint_fast64_t>((stateEstimate / 1000.0) - ((stateEstimate / 1000.0) - minPrec)*(subSysProb/bound));
 				}
 			}
 		}
diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h
index 2a33b50eb..94f550141 100644
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -1809,15 +1809,16 @@ namespace storm {
                     
                     phiStates = untilFormula.getLeft().check(modelchecker);
                     psiStates = untilFormula.getRight().check(modelchecker);
-                } catch (std::bad_cast const& e) {
+                } catch (std::bad_cast const&) {
                     // If the nested formula was not an until formula, it remains to check whether it's an eventually formula.
                     try {
                         storm::property::prctl::Eventually<double> const& eventuallyFormula = dynamic_cast<storm::property::prctl::Eventually<double> const&>(pathFormula);
                         
                         phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true);
                         psiStates = eventuallyFormula.getChild().check(modelchecker);
-                    } catch (std::bad_cast const& e) {
+                    } catch (std::bad_cast const&) {
                         // If the nested formula is neither an until nor a finally formula, we throw an exception.
+						LOG4CPLUS_ERROR(logger, "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation.");
                         throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation.";
                     }
                 }
diff --git a/src/storm.cpp b/src/storm.cpp
index 1a30c2d7a..2287e9b37 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -45,6 +45,7 @@
 #include "src/utility/ErrorHandling.h"
 #include "src/formula/Prctl.h"
 #include "src/utility/vector.h"
+#include "src/utility/OsDetection.h"
 
 #include "src/settings/Settings.h"
 // Registers all standard options
@@ -156,7 +157,7 @@ void setUpFileLogging() {
 */
 std::string getCurrentWorkingDirectory() {
 	char temp[512];
-	return (_getcwd(temp, 512 - 1) ? std::string(temp) : std::string(""));
+	return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string(""));
 }
 
 /*!