sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Fixed Windows build 

Former-commit-id: 53c99736de
tempestpy_adaptions
David_Korzeniewski 10 years ago
parent
e4968b1dde
commit
d4f051c4f0
4 changed files with 45 additions and 12 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddApply.c
  2. 21
      test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  3. 12
      test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
  4. 18
      test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp

6
resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddApply.c
View File

@ -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

21
test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
View File

@ -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());

12
test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
View File

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

18
test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp
View File

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

Write Preview
Loading…
Cancel
Save