From d4f051c4f0e5e799c9e9090c316f5b7a6f719669 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Fri, 1 May 2015 14:46:26 +0200 Subject: [PATCH] Fixed Windows build Former-commit-id: 53c99736de67fcf7020ec043c2c03dbe87e669b9 --- .../cudd-2.5.0/src/cudd/cuddAddApply.c | 6 +++--- .../GmmxxCtmcCslModelCheckerTest.cpp | 21 +++++++++++++++---- .../GmmxxHybridDtmcPrctlModelCheckerTest.cpp | 12 +++++++++-- .../SparseCtmcCslModelCheckerTest.cpp | 18 +++++++++++++--- 4 files changed, 45 insertions(+), 12 deletions(-) diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddApply.c b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddApply.c index fc1ab8c15..e789bfc73 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddApply.c +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddApply.c @@ -1078,7 +1078,7 @@ Cudd_addMod( F = *f; G = *g; if (cuddIsConstant(F) && cuddIsConstant(G)) { // If g is <=0, then result is NaN - if (cuddV(G) <= 0) value = (0.0/0.0); + if (cuddV(G) <= 0) value = (NAN); // Take care of negative case (% is remainder, not modulo) else { rem = ((int)cuddV(F) % (int)cuddV(G)); @@ -1119,9 +1119,9 @@ Cudd_addLogXY( F = *f; G = *g; if (cuddIsConstant(F) && cuddIsConstant(G)) { // If base is <=0 or ==1 (or +Inf/NaN), then result is NaN - if (cuddV(G) <= 0 || cuddV(G) == 1.0 || G==DD_PLUS_INFINITY(dd) || cuddV(G) != cuddV(G)) value = (0.0/0.0); + if (cuddV(G) <= 0 || cuddV(G) == 1.0 || G==DD_PLUS_INFINITY(dd) || cuddV(G) != cuddV(G)) value = (NAN); // If arg is <0 or NaN, then result is NaN - else if (cuddV(F) < 0 || cuddV(F) != cuddV(F)) value = (0.0/0.0); + else if (cuddV(F) < 0 || cuddV(F) != cuddV(F)) value = (NAN); // If arg is +Inf, then result is +Inf else if (F==DD_PLUS_INFINITY(dd)) return DD_PLUS_INFINITY(dd); // If arg is (positive/negative) 0, then result is -Inf diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index 6a814d63d..5c637afcb 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -22,7 +22,11 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { std::shared_ptr formula(nullptr); // Build the model. - typename storm::builder::ExplicitPrismModelBuilder::Options options; +#ifdef WINDOWS + storm::builder::ExplicitPrismModelBuilder::Options options; +#else + typename storm::builder::ExplicitPrismModelBuilder::Options options; +#endif options.buildRewards = true; options.rewardModelName = "num_repairs"; std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); @@ -80,7 +84,12 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { std::shared_ptr formula(nullptr); // Build the model. - typename storm::builder::ExplicitPrismModelBuilder::Options options; +#ifdef WINDOWS + storm::builder::ExplicitPrismModelBuilder::Options options; +#else + typename storm::builder::ExplicitPrismModelBuilder::Options options; +#endif + options.buildRewards = true; options.rewardModelName = "up"; std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); @@ -172,8 +181,12 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) { std::shared_ptr formula(nullptr); // Build the model. - typename storm::builder::ExplicitPrismModelBuilder::Options options; - options.buildRewards = true; +#ifdef WINDOWS + storm::builder::ExplicitPrismModelBuilder::Options options; +#else + typename storm::builder::ExplicitPrismModelBuilder::Options options; +#endif + options.buildRewards = true; options.rewardModelName = "customers"; std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index cd1a014a9..df17ce336 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -16,7 +16,11 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); // Build the die model with its reward model. - typename storm::builder::DdPrismModelBuilder::Options options; +#ifdef WINDOWS + storm::builder::DdPrismModelBuilder::Options options; +#else + typename storm::builder::DdPrismModelBuilder::Options options; +#endif options.buildRewards = true; options.rewardModelName = "coin_flips"; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); @@ -118,7 +122,11 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); // Build the die model with its reward model. - typename storm::builder::DdPrismModelBuilder::Options options; +#ifdef WINDOWS + storm::builder::DdPrismModelBuilder::Options options; +#else + typename storm::builder::DdPrismModelBuilder::Options options; +#endif options.buildRewards = true; options.rewardModelName = "num_rounds"; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); diff --git a/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp index 3dfa1b6be..9db619115 100644 --- a/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp @@ -22,7 +22,11 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) { std::shared_ptr formula(nullptr); // Build the model. - typename storm::builder::ExplicitPrismModelBuilder::Options options; +#ifdef WINDOWS + storm::builder::ExplicitPrismModelBuilder::Options options; +#else + typename storm::builder::ExplicitPrismModelBuilder::Options options; +#endif options.buildRewards = true; options.rewardModelName = "num_repairs"; std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); @@ -80,7 +84,11 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) { std::shared_ptr formula(nullptr); // Build the model. - typename storm::builder::ExplicitPrismModelBuilder::Options options; +#ifdef WINDOWS + storm::builder::ExplicitPrismModelBuilder::Options options; +#else + typename storm::builder::ExplicitPrismModelBuilder::Options options; +#endif options.buildRewards = true; options.rewardModelName = "up"; std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); @@ -172,7 +180,11 @@ TEST(SparseCtmcCslModelCheckerTest, Tandem) { std::shared_ptr formula(nullptr); // Build the model with the customers reward structure. - typename storm::builder::ExplicitPrismModelBuilder::Options options; +#ifdef WINDOWS + storm::builder::ExplicitPrismModelBuilder::Options options; +#else + typename storm::builder::ExplicitPrismModelBuilder::Options options; +#endif options.buildRewards = true; options.rewardModelName = "customers"; std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options);