From c4dffe9a8b14aeb7c2d87e27eba66ac68f792ac0 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 15 Mar 2017 18:48:36 +0100 Subject: [PATCH] tests for step bounded properties --- .../examples/testfiles/prctl/two_dice.prctl | 4 -- .../SparseDtmcParameterLiftingTest.cpp | 62 +++++++++++++++++++ .../SparseMdpParameterLiftingTest.cpp | 62 ++++++++++++++++++- 3 files changed, 123 insertions(+), 5 deletions(-) delete mode 100644 resources/examples/testfiles/prctl/two_dice.prctl diff --git a/resources/examples/testfiles/prctl/two_dice.prctl b/resources/examples/testfiles/prctl/two_dice.prctl deleted file mode 100644 index 3368d9651..000000000 --- a/resources/examples/testfiles/prctl/two_dice.prctl +++ /dev/null @@ -1,4 +0,0 @@ -P<=0.17 [ F "doubles" ] - - - diff --git a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp index a7adb5d22..dd8fd422d 100644 --- a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -68,7 +68,36 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew) { EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); carl::VariablePool::getInstance().clear(); +} +TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm"; + std::string formulaAsString = "R>2.5 [ C<=300]"; + std::string constantsAsString = "pL=0.9,TOAck=0.5"; + carl::VariablePool::getInstance().clear(); + + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + storm::modelchecker::parametric::ParameterLifting, double> parameterLiftingContext(*model); + parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); + + //start testing + auto allSatRegion=storm::storage::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); + auto exBothRegion=storm::storage::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); + auto allVioRegion=storm::storage::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); + + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + + carl::VariablePool::getInstance().clear(); } TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) { @@ -160,6 +189,39 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) { carl::VariablePool::getInstance().clear(); } +TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm"; + std::string formulaAsString = "P<0.5 [F<=300 \"observe0Greater1\" ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + carl::VariablePool::getInstance().clear(); + + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + storm::modelchecker::parametric::ParameterLifting, double> parameterLiftingContext(*model); + parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); + + //start testing + auto allSatRegion=storm::storage::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters); + auto exBothRegion=storm::storage::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters); + auto allVioRegion=storm::storage::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters); + auto allVioHardRegion=storm::storage::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters); + + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::CenterViolated, parameterLiftingContext.analyzeRegion(allVioHardRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + + carl::VariablePool::getInstance().clear(); +} + TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) { std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm"; diff --git a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp index cda3867bd..c31dbf66d 100644 --- a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp +++ b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp @@ -12,7 +12,37 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob) { std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm"; - std::string formulaFile = STORM_TEST_RESOURCES_DIR "/prctl/two_dice.prctl"; //P<=0.17 [F \"doubles\" ]"; + std::string formulaFile = "P<=0.17 [ F \"doubles\" ]"; + + carl::VariablePool::getInstance().clear(); + + storm::prism::Program program = storm::parseProgram(programFile); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaFile, program)); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + storm::modelchecker::parametric::ParameterLifting, double> parameterLiftingContext(*model); + parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); + + auto allSatRegion = storm::storage::ParameterRegion::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters); + auto exBothRegion = storm::storage::ParameterRegion::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters); + auto allVioRegion = storm::storage::ParameterRegion::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters); + + + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + + carl::VariablePool::getInstance().clear(); +} + +TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm"; + std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]"; carl::VariablePool::getInstance().clear(); @@ -128,6 +158,36 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew) { carl::VariablePool::getInstance().clear(); } +TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm"; + std::string formulaAsString = "R>2.5 [ C<=300 ]"; + std::string constantsAsString = "pL=0.9,TOAck=0.5"; + + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + + auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); + auto rewParameters = storm::models::sparse::getRewardParameters(*model); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + + storm::modelchecker::parametric::ParameterLifting, double> parameterLiftingContext(*model); + parameterLiftingContext.specifyFormula(storm::modelchecker::CheckTask(*formulas[0], true)); + + //start testing + auto allSatRegion=storm::storage::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters); + auto exBothRegion=storm::storage::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); + auto allVioRegion=storm::storage::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); + + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); + + carl::VariablePool::getInstance().clear(); +} + TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) {