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: 08f82f2ed2

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

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.";
                     }
                 }

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(""));
 }
 
 /*!