You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

133 lines
11 KiB

  1. #include "gtest/gtest.h"
  2. #include "storm-config.h"
  3. #ifdef STORM_HAVE_CARL
  4. #include "src/adapters/CarlAdapter.h"
  5. #include "src/settings/SettingsManager.h"
  6. #include "src/settings/modules/GeneralSettings.h"
  7. #include "src/settings/modules/RegionSettings.h"
  8. #include "utility/storm.h"
  9. #include "src/models/sparse/Model.h"
  10. #include "modelchecker/region/SparseRegionModelChecker.h"
  11. #include "modelchecker/region/ParameterRegion.h"
  12. TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) {
  13. std::string programFile = STORM_CPP_BASE_PATH "/examples/pmdp/two_dice/two_dice.nm";
  14. std::string formulaFile = STORM_CPP_BASE_PATH "/examples/pmdp/two_dice/two_dice.prctl"; //P<=0.17 [F \"doubles\" ]";
  15. std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
  16. carl::VariablePool::getInstance().clear();
  17. storm::prism::Program program = storm::parseProgram(programFile);
  18. std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaFile, program);
  19. std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
  20. auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
  21. storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
  22. auto mdpModelchecker = std::make_shared<storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(model, settings);
  23. mdpModelchecker->specifyFormula(formulas[0]);
  24. auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505");
  25. auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55");
  26. auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6");
  27. EXPECT_TRUE(mdpModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint()));
  28. EXPECT_FALSE(mdpModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
  29. //Test the methods provided in storm.h
  30. EXPECT_TRUE(storm::checkSamplingPoint(mdpModelchecker,allSatRegion.getLowerBoundaries()));
  31. EXPECT_TRUE(storm::checkSamplingPoint(mdpModelchecker,allSatRegion.getUpperBoundaries()));
  32. EXPECT_FALSE(storm::checkSamplingPoint(mdpModelchecker,exBothRegion.getLowerBoundaries()));
  33. EXPECT_FALSE(storm::checkSamplingPoint(mdpModelchecker,exBothRegion.getUpperBoundaries()));
  34. EXPECT_TRUE(storm::checkSamplingPoint(mdpModelchecker,exBothRegion.getVerticesOfRegion(exBothRegion.getVariables())[1]));
  35. EXPECT_TRUE(storm::checkSamplingPoint(mdpModelchecker,exBothRegion.getVerticesOfRegion(exBothRegion.getVariables())[2]));
  36. EXPECT_FALSE(storm::checkSamplingPoint(mdpModelchecker,exBothRegion.getUpperBoundaries()));
  37. EXPECT_FALSE(storm::checkSamplingPoint(mdpModelchecker,allVioRegion.getLowerBoundaries()));
  38. EXPECT_FALSE(storm::checkSamplingPoint(mdpModelchecker,allVioRegion.getUpperBoundaries()));
  39. EXPECT_TRUE(storm::checkRegionApproximation(mdpModelchecker, allSatRegion.getLowerBoundaries(), allSatRegion.getUpperBoundaries(), true));
  40. EXPECT_FALSE(storm::checkRegionApproximation(mdpModelchecker, allSatRegion.getLowerBoundaries(), allSatRegion.getUpperBoundaries(), false));
  41. EXPECT_FALSE(storm::checkRegionApproximation(mdpModelchecker, exBothRegion.getLowerBoundaries(), exBothRegion.getUpperBoundaries(), true));
  42. EXPECT_FALSE(storm::checkRegionApproximation(mdpModelchecker, exBothRegion.getLowerBoundaries(), exBothRegion.getUpperBoundaries(), false));
  43. EXPECT_FALSE(storm::checkRegionApproximation(mdpModelchecker, allVioRegion.getLowerBoundaries(), allVioRegion.getUpperBoundaries(), true));
  44. EXPECT_TRUE(storm::checkRegionApproximation(mdpModelchecker, allVioRegion.getLowerBoundaries(), allVioRegion.getUpperBoundaries(), false));
  45. //Remaining tests..
  46. EXPECT_NEAR(0.1666665285, mdpModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
  47. EXPECT_NEAR(0.1666665529, mdpModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
  48. EXPECT_NEAR(0.1716553235, mdpModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
  49. EXPECT_NEAR(0.1709666953, mdpModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
  50. EXPECT_NEAR(0.1826972576, mdpModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
  51. EXPECT_NEAR(0.1964429282, mdpModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
  52. //test approximative method
  53. settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
  54. mdpModelchecker = std::make_shared<storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(model, settings);
  55. mdpModelchecker->specifyFormula(formulas[0]);
  56. ASSERT_TRUE(mdpModelchecker->getSettings().doApprox());
  57. ASSERT_TRUE(mdpModelchecker->getSettings().doSample());
  58. ASSERT_FALSE(mdpModelchecker->getSettings().doSmt());
  59. mdpModelchecker->checkRegion(allSatRegion);
  60. EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
  61. mdpModelchecker->checkRegion(exBothRegion);
  62. EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
  63. mdpModelchecker->checkRegion(allVioRegion);
  64. EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
  65. carl::VariablePool::getInstance().clear();
  66. }
  67. TEST(SparseMdpRegionModelCheckerTest, coin_Prob) {
  68. std::string programFile = STORM_CPP_BASE_PATH "/examples/pmdp/coin2/coin2_2.pm";
  69. std::string formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]";
  70. std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
  71. carl::VariablePool::getInstance().clear();
  72. storm::prism::Program program = storm::parseProgram(programFile);
  73. std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);
  74. std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
  75. auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
  76. storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
  77. auto mdpModelchecker = std::make_shared<storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(model, settings);
  78. mdpModelchecker->specifyFormula(formulas[0]);
  79. //start testing
  80. auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.3<=p1<=0.45,0.2<=p2<=0.54");
  81. auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p1<=0.65,0.5<=p2<=0.7");
  82. auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p1<=0.7,0.55<=p2<=0.6");
  83. EXPECT_TRUE(mdpModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint()));
  84. EXPECT_FALSE(mdpModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
  85. EXPECT_NEAR(0.95128124239, mdpModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
  86. EXPECT_NEAR(0.26787251126, mdpModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
  87. EXPECT_NEAR(0.41880006098, mdpModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
  88. EXPECT_NEAR(0.01535089684, mdpModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
  89. EXPECT_NEAR(0.24952791523, mdpModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
  90. EXPECT_NEAR(0.01711494956, mdpModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
  91. //test approximative method
  92. settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
  93. mdpModelchecker = std::make_shared<storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(model, settings);
  94. mdpModelchecker->specifyFormula(formulas[0]);
  95. ASSERT_TRUE(mdpModelchecker->getSettings().doApprox());
  96. ASSERT_TRUE(mdpModelchecker->getSettings().doSample());
  97. ASSERT_FALSE(mdpModelchecker->getSettings().doSmt());
  98. mdpModelchecker->checkRegion(allSatRegion);
  99. EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
  100. mdpModelchecker->checkRegion(exBothRegion);
  101. EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
  102. mdpModelchecker->checkRegion(allVioRegion);
  103. EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
  104. carl::VariablePool::getInstance().clear();
  105. }
  106. #endif