From d4f051c4f0e5e799c9e9090c316f5b7a6f719669 Mon Sep 17 00:00:00 2001
From: David_Korzeniewski <david.korzeniewski@rwth-aachen.de>
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<storm::logic::Formula> formula(nullptr);
// Build the model.
- typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#ifdef WINDOWS
+ storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#else
+ typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#endif
options.buildRewards = true;
options.rewardModelName = "num_repairs";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
@@ -80,7 +84,12 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model.
- typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#ifdef WINDOWS
+ storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#else
+ typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#endif
+
options.buildRewards = true;
options.rewardModelName = "up";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
@@ -172,8 +181,12 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model.
- typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
- options.buildRewards = true;
+#ifdef WINDOWS
+ storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#else
+ typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#endif
+ options.buildRewards = true;
options.rewardModelName = "customers";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::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<storm::dd::DdType::CUDD>::Options options;
+#ifdef WINDOWS
+ storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
+#else
+ typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
+#endif
options.buildRewards = true;
options.rewardModelName = "coin_flips";
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::dd::DdType::CUDD>::Options options;
+#ifdef WINDOWS
+ storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
+#else
+ typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
+#endif
options.buildRewards = true;
options.rewardModelName = "num_rounds";
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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<storm::logic::Formula> formula(nullptr);
// Build the model.
- typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#ifdef WINDOWS
+ storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#else
+ typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#endif
options.buildRewards = true;
options.rewardModelName = "num_repairs";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
@@ -80,7 +84,11 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) {
std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model.
- typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#ifdef WINDOWS
+ storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#else
+ typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#endif
options.buildRewards = true;
options.rewardModelName = "up";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
@@ -172,7 +180,11 @@ TEST(SparseCtmcCslModelCheckerTest, Tandem) {
std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model with the customers reward structure.
- typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#ifdef WINDOWS
+ storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#else
+ typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+#endif
options.buildRewards = true;
options.rewardModelName = "customers";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);