diff --git a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp index 0e630a3ab..3675ea1cc 100644 --- a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp @@ -211,7 +211,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, csma) { std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/csma2_2.nm"; std::string constantsDef = ""; std::string formulasAsString = "multi(Pmax=? [ F{\"time\"}<=70 \"all_delivered\" ])"; - formulasAsString += "; \n multi(Pmax=? [ F{\"time\"}<=70 \"all_delivered\" ], P>=0 [ !\"collision_max_backoff\" U \"all_delivered\"] )"; + formulasAsString += "; \n multi(Pmax=? [ F{\"time\"}<=70 \"all_delivered\" ], Pmax=? [ !\"collision_max_backoff\" U \"all_delivered\"] )"; // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); @@ -229,7 +229,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, csma) { result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); - std::vector p = {storm::utility::convertNumber("29487882838281/35184372088832"), storm::utility::convertNumber("6979344855/8589934592")}; + std::vector p = {storm::utility::convertNumber("29487882838281/35184372088832"), storm::utility::convertNumber("7/8")}; auto expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p})); EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues));