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

Merge branch 'master' into LRA_for_dtmc_mdp 

Former-commit-id: 0f7464cdc0
tempestpy_adaptions
David_Korzeniewski 10 years ago
parent
073ce2ee2c d4f051c4f0
commit
3872e17a4e
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
Unified 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; F = *f; G = *g;
if (cuddIsConstant(F) && cuddIsConstant(G)) { if (cuddIsConstant(F) && cuddIsConstant(G)) {
// If g is <=0, then result is NaN // 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) // Take care of negative case (% is remainder, not modulo)
else { else {
rem = ((int)cuddV(F) % (int)cuddV(G)); rem = ((int)cuddV(F) % (int)cuddV(G));
@ -1119,9 +1119,9 @@ Cudd_addLogXY(
F = *f; G = *g; F = *f; G = *g;
if (cuddIsConstant(F) && cuddIsConstant(G)) { if (cuddIsConstant(F) && cuddIsConstant(G)) {
// If base is <=0 or ==1 (or +Inf/NaN), then result is NaN // 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 // 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 // If arg is +Inf, then result is +Inf
else if (F==DD_PLUS_INFINITY(dd)) return DD_PLUS_INFINITY(dd); else if (F==DD_PLUS_INFINITY(dd)) return DD_PLUS_INFINITY(dd);
// If arg is (positive/negative) 0, then result is -Inf // 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); std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model. // 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.buildRewards = true;
options.rewardModelName = "num_repairs"; options.rewardModelName = "num_repairs";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options); 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); std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model. // 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.buildRewards = true;
options.rewardModelName = "up"; options.rewardModelName = "up";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options); 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); std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model. // 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"; options.rewardModelName = "customers";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options); std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); 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"); 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. // 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.buildRewards = true;
options.rewardModelName = "coin_flips"; 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); 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"); 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. // 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.buildRewards = true;
options.rewardModelName = "num_rounds"; 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); 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); std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model. // 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.buildRewards = true;
options.rewardModelName = "num_repairs"; options.rewardModelName = "num_repairs";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options); 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); std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model. // 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.buildRewards = true;
options.rewardModelName = "up"; options.rewardModelName = "up";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options); 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); std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model with the customers reward structure. // 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.buildRewards = true;
options.rewardModelName = "customers"; options.rewardModelName = "customers";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options); std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);

Write Preview
Loading…
Cancel
Save