From 94b25c02cadde6fac5e89238f0ad0d1da24eb5b8 Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 16 Apr 2014 21:18:12 +0200 Subject: [PATCH] Fixed bugs in some files. Made LTL a little better to compile under WIN32. Former-commit-id: 71377f0672171b8dd8dbd9eb34425cc1de46ab4a --- CMakeLists.txt | 3 +++ .../ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp | 2 +- .../ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp | 2 +- src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h | 2 +- src/modelchecker/prctl/SparseMdpPrctlModelChecker.h | 2 +- src/parser/PrctlParser.cpp | 2 +- src/parser/PrismParser.h | 2 +- src/storage/expressions/SimpleValuation.h | 5 ++++- src/storage/prism/LocatedInformation.h | 1 + test/functional/solver/GmmxxLinearEquationSolverTest.cpp | 2 +- test/functional/storage/ExpressionTest.cpp | 1 + 11 files changed, 16 insertions(+), 8 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 77b5c64a0..c6d62bdde 100644 --- a/CMakeLists.txt +++ b/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() diff --git a/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp b/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp index f20e1eedb..55e55fbd2 100644 --- a/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp +++ b/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp @@ -31,7 +31,7 @@ /* C99 systems have . Non-C99 systems may or may not. */ -#if defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L +#if (defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L) || defined _WIN32 #include typedef int8_t flex_int8_t; typedef uint8_t flex_uint8_t; diff --git a/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp b/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp index 82812c039..9be4a847a 100644 --- a/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp +++ b/resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp @@ -31,7 +31,7 @@ /* C99 systems have . Non-C99 systems may or may not. */ -#if defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L +#if (defined __STDC_VERSION__ && __STDC_VERSION__ >= 199901L) || defined _WIN32 #include typedef int8_t flex_int8_t; typedef uint8_t flex_uint8_t; diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 2f03603d8..9d43dfb52 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/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(formula.getBound())); } else { throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; } diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 868f78722..c3e2aec58 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/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(formula.getBound())); return result; } diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index fb58d7ee9..d929c5ac7 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -140,7 +140,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar stateFormula)[qi::_val = phoenix::new_>(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_>(qi::_1)]; instantaneousReward.name("path formula (for reward operator)"); steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_>()]; diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 3f8f17b65..db0ae9696 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -85,7 +85,7 @@ namespace storm { } }; - struct keywordsStruct : qi::symbols { + struct keywordsStruct : qi::symbols { keywordsStruct() { add ("dtmc", 1) diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h index 35b74291b..a196921a6 100644 --- a/src/storage/expressions/SimpleValuation.h +++ b/src/storage/expressions/SimpleValuation.h @@ -7,6 +7,7 @@ #include #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; /*! diff --git a/src/storage/prism/LocatedInformation.h b/src/storage/prism/LocatedInformation.h index 8aa4d301e..81f5334b5 100644 --- a/src/storage/prism/LocatedInformation.h +++ b/src/storage/prism/LocatedInformation.h @@ -2,6 +2,7 @@ #define STORM_STORAGE_PRISM_LOCATEDINFORMATION_H_ #include +#include #include "src/utility/OsDetection.h" diff --git a/test/functional/solver/GmmxxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxLinearEquationSolverTest.cpp index 077920f13..0381be434 100644 --- a/test/functional/solver/GmmxxLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxLinearEquationSolverTest.cpp @@ -81,7 +81,7 @@ TEST(GmmxxLinearEquationSolver, qmr) { ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver solver(storm::solver::GmmxxLinearEquationSolver::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::NONE)); - storm::solver::GmmxxLinearEquationSolver solver(storm::solver::GmmxxLinearEquationSolver::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::NONE, 50); + storm::solver::GmmxxLinearEquationSolver solver(storm::solver::GmmxxLinearEquationSolver::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver::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()); diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp index 0c19c5bfb..41556f6d6 100644 --- a/test/functional/storage/ExpressionTest.cpp +++ b/test/functional/storage/ExpressionTest.cpp @@ -1,4 +1,5 @@ #include +#include #include "gtest/gtest.h" #include "src/storage/expressions/Expression.h"