diff --git a/resources/examples/testfiles/mdp/tiny_reward_bounded.nm b/resources/examples/testfiles/mdp/tiny_reward_bounded.nm index 7205d0783..5b895d557 100644 --- a/resources/examples/testfiles/mdp/tiny_reward_bounded.nm +++ b/resources/examples/testfiles/mdp/tiny_reward_bounded.nm @@ -1,7 +1,7 @@ mdp module main - x : [0..4] init 0; + x : [0..5] init 0; [a] x=0 -> (x'=1); [b] x=0 -> (x'=2); diff --git a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp index e523c4812..0e630a3ab 100644 --- a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp @@ -121,9 +121,9 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, tiny_ec) { formulasAsString += "; \n multi(Pmin=? [ F{\"a\"}<1 x=1 ]) "; // 0.0 formulasAsString += "; \n multi(Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )]) "; // 0.02 formulasAsString += "; \n multi(Pmin=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<=12 x=5 )]) "; // 0.0 - formulasAsString += "; \n multi(Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<13 x=5, F{\"c\"}<0.4 x=3 )]) "; // 0.02 - formulasAsString += "; \n multi(Pmax=? [multi( F{\"a\"}<=0 x=3, F{\"b\"}<=17 x=4, F{\"c\"}<0.8 x=5 )]) "; // 0.02 - formulasAsString += "; \n multi(Pmax=? [multi( F{\"a\"}<=0 x=0, F{\"c\"}<0.5 x=5 )], Pmax=? [multi( F{\"b\"}<=0 x=3, F{\"c\"}<=0.8 x=5 )]) "; // (0.1, 0) , (0, 0.19) + formulasAsString += "; \n multi(Pmax=? [multi( F{\"a\"}<=4 x=4, F{\"b\"}<13 x=5, F{\"c\"}<2/5 x=3 )]) "; // 0.02 + formulasAsString += "; \n multi(Pmax=? [multi( F{\"a\"}<=0 x=3, F{\"b\"}<=17 x=4, F{\"c\"}<4/5 x=5 )]) "; // 0.02 + formulasAsString += "; \n multi(Pmax=? [multi( F{\"a\"}<=0 x=3, F{\"c\"}<1/2 x=5 )], Pmax=? [multi( F{\"b\"}<=0 x=3, F{\"c\"}<=4/5 x=5 )]) "; // (0.1, 0) , (0, 0.19) // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); @@ -174,6 +174,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, tiny_ec) { std::vector p = {storm::utility::convertNumber("1/10"), storm::utility::convertNumber("0")}; std::vector q = {storm::utility::convertNumber("0"), storm::utility::convertNumber("19/100")}; auto expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p, q})); + EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues));