From ade8078759cb6ab4e09c85fac6b7cf4fead18335 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 15 Sep 2017 12:59:18 +0200 Subject: [PATCH] added test for lower bounded properties --- .../mdp/tiny_lower_reward_bounded.nm | 22 ++++ ...MdpMultiDimensionalRewardUnfoldingTest.cpp | 106 ++++++++++++++++++ 2 files changed, 128 insertions(+) create mode 100644 resources/examples/testfiles/mdp/tiny_lower_reward_bounded.nm diff --git a/resources/examples/testfiles/mdp/tiny_lower_reward_bounded.nm b/resources/examples/testfiles/mdp/tiny_lower_reward_bounded.nm new file mode 100644 index 000000000..dbbf9c582 --- /dev/null +++ b/resources/examples/testfiles/mdp/tiny_lower_reward_bounded.nm @@ -0,0 +1,22 @@ +mdp + +module main + x : [0..4] init 0; + + [a] x=0 -> 1/10 : (x'=1) + 9/10 : (x'=0); + [b] x=0 -> 1/4 : (x'=1) + 3/4 : (x'=2); + [] x=2 -> (x'=3); + [] x=3 -> 1/2 : (x'=2) + 1/2 : (x'=3); + [] x=3 -> 1/3 : (x'=3) + 2/3 : (x'=4); + [] x=4 -> (x'=0); + +endmodule + +rewards "a" + [a] true : 2/5; +endrewards + + +rewards "b" + [b] true : 1; +endrewards diff --git a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp index e0e82903b..ebb126248 100644 --- a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp @@ -206,6 +206,61 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_csma) { } +TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_lower_bounds) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_lower_reward_bounded.nm"; + std::string constantsDef = ""; + std::string formulasAsString = "Pmax=? [ F{\"a\"}>=1.1 x=1 ]"; + formulasAsString += "; \n Pmin=? [ F{\"a\"}>=1.1 x=1 ]"; + formulasAsString += "; \n Pmax=? [ F{\"b\"}>3 x=1 ]"; + formulasAsString += "; \n Pmax=? [ multi(F{\"a\"}<=0.2 x=1, F{\"b\"}>3 x=1) ]"; + formulasAsString += "; \n Pmax=? [ multi(F{\"a\"}>0.2 x=1, F{\"b\"}>3 x=1) ]"; + formulasAsString += "; \n Pmax=? [ multi(F{\"a\"}>=2/5 x=4, F{\"a\"}<=0 x=4) ]"; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsDef); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin();; + + std::unique_ptr result; + + storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + storm::RationalNumber expectedResult = storm::utility::convertNumber("81/100"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::convertNumber("0"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[2], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::convertNumber("27/64"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[3], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::convertNumber("27/64"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[4], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::convertNumber("243/640"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[5], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::convertNumber("81/160"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + +} + @@ -434,5 +489,56 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, csma) { } +TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, lower_bounds) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/tiny_lower_reward_bounded.nm"; + std::string constantsDef = ""; + std::string formulasAsString = "multi(Pmax=? [ F{\"a\"}>=1.1 x=1 ])"; + formulasAsString += "; \n multi(Pmax=? [ F{\"a\"}<=0.2 x=1], Pmax=? [F{\"b\"}>3 x=1 ])"; + formulasAsString += "; \n multi(Pmax=? [ F{\"a\"}>0.2 x=1 ], Pmax=? [F{\"b\"}>3 x=1 ])"; + formulasAsString += "; \n multi(Pmax=? [ multi(F{\"a\"}>=2/5 x=4, F{\"a\"}<=0 x=4)], Pmax=? [F {\"b\"}>3 x = 1])"; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsDef); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin();; + + std::unique_ptr result; + + storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + storm::RationalNumber expectedResult = storm::utility::convertNumber("81/100"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector p1 = {storm::utility::convertNumber("1"), storm::utility::convertNumber("27/64")}; + auto expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p1})); + EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); + EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector p2 = {storm::utility::convertNumber("1"), storm::utility::convertNumber("243/640")}; + std::vector q2 = {storm::utility::convertNumber("81/256"), storm::utility::convertNumber("27/64")}; + expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p2, q2})); + EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); + EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[3]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector p3 = {storm::utility::convertNumber("81/160"), storm::utility::convertNumber("243/640")}; + std::vector q3 = {storm::utility::convertNumber("2187/10240"), storm::utility::convertNumber("27/64")}; + expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p3, q3})); + EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); + EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); + +} + + #endif /* STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE */