Fixed bugs in some files.

Made LTL a little better to compile under WIN32.


Former-commit-id: 71377f0672

CMakeLists.txt

@@ -122,6 +122,9 @@ elseif(MSVC)
 	# Windows.h breaks GMM in gmm_except.h because of its macro definition for min and max
 	add_definitions(/DNOMINMAX)
 	
+	# since nobody cares at the moment
+	add_definitions(/wd4250)
+	
 	if(ENABLE_Z3)
 		set(Z3_LIB_NAME "libz3")
 	endif()

resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp

@@ -31,7 +31,7 @@
 
 /* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */
 
-#if defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L
+#if (defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L) || defined _WIN32
 #include <inttypes.h>
 typedef int8_t flex_int8_t;
 typedef uint8_t flex_uint8_t;

resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp

@@ -31,7 +31,7 @@
 
 /* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */
 
-#if defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L
+#if (defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L) || defined _WIN32
 #include <inttypes.h>
 typedef int8_t flex_int8_t;
 typedef uint8_t flex_uint8_t;

src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h

@@ -393,7 +393,7 @@ public:
 
 		// Perform the actual matrix-vector multiplication as long as the bound of the formula is met.
         if (linearEquationSolver != nullptr) {
-            this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result, &totalRewardVector, formula.getBound());
+			this->linearEquationSolver->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), result, &totalRewardVector, static_cast<uint_fast64_t>(formula.getBound()));
         } else {
             throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
         }

src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -410,7 +410,7 @@ namespace storm {
                         result.resize(this->getModel().getNumberOfStates());
                     }
                     
-                    this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, &totalRewardVector, formula.getBound());
+					this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, &totalRewardVector, static_cast<uint_fast64_t>(formula.getBound()));
                     
                     return result;
                 }

src/parser/PrctlParser.cpp

@@ -140,7 +140,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 		reachabilityReward = (qi::lit("F") > stateFormula)[qi::_val =
 				phoenix::new_<storm::property::prctl::ReachabilityReward<double>>(qi::_1)];
 		reachabilityReward.name("path formula (for reward operator)");
-		instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::double_)
+		instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::uint_)
 						[qi::_val = phoenix::new_<storm::property::prctl::InstantaneousReward<double>>(qi::_1)];
 		instantaneousReward.name("path formula (for reward operator)");
 		steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_<storm::property::prctl::SteadyStateReward<double>>()];

src/parser/PrismParser.h

@@ -85,7 +85,7 @@ namespace storm {
                 }
             };
             
-            struct keywordsStruct : qi::symbols<char, bool> {
+            struct keywordsStruct : qi::symbols<char, uint_fast64_t> {
                 keywordsStruct() {
                     add
                     ("dtmc", 1)

src/storage/expressions/SimpleValuation.h

@@ -7,6 +7,7 @@
 #include <iostream>
 
 #include "src/storage/expressions/Valuation.h"
+#include "src/utility/OsDetection.h"
 
 namespace storm {
     namespace expressions {
@@ -23,8 +24,10 @@ namespace storm {
             // Instantiate some constructors and assignments with their default implementations.
             SimpleValuation(SimpleValuation const&) = default;
             SimpleValuation& operator=(SimpleValuation const&) = default;
-            SimpleValuation(SimpleValuation&&) = default;
+#ifndef WINDOWS            
+			SimpleValuation(SimpleValuation&&) = default;
             SimpleValuation& operator=(SimpleValuation&&) = default;
+#endif
             virtual ~SimpleValuation() = default;
 
             /*!

src/storage/prism/LocatedInformation.h

@@ -2,6 +2,7 @@
 #define STORM_STORAGE_PRISM_LOCATEDINFORMATION_H_
 
 #include <string>
+#include <cstdint>
 
 #include "src/utility/OsDetection.h"
 

test/functional/solver/GmmxxLinearEquationSolverTest.cpp

@@ -81,7 +81,7 @@ TEST(GmmxxLinearEquationSolver, qmr) {
     
     ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE));
     
-    storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, 50);
+    storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, true, 50);
     ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
     ASSERT_LT(std::abs(x[0] - 1), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
     ASSERT_LT(std::abs(x[1] - 3), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());

test/functional/storage/ExpressionTest.cpp

@@ -1,4 +1,5 @@
 #include <map>
+#include <string>
 
 #include "gtest/gtest.h"
 #include "src/storage/expressions/Expression.h"