diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp index 3e34f6139..b1403f9a0 100755 --- a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp @@ -235,6 +235,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, simple_lra) { formulasAsString += "multi(R{\"first\"}min=? [ C ], R{\"first\"}max=? [ LRA ]);\n"; // pareto formulasAsString += "multi(R{\"first\"}min=? [ C ], R{\"second\"}max=? [ LRA ], R{\"third\"}max=? [ C ]);\n"; // pareto formulasAsString += "multi(R{\"first\"}min=? [ LRA ], R{\"second\"}max=? [ LRA ], R{\"third\"}min=? [ C ]);\n"; // pareto + formulasAsString += "multi(LRAmax=? [ x=1 ], R{\"second\"}max=? [ LRA ]);\n"; // pareto // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); @@ -309,6 +310,16 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, simple_lra) { EXPECT_TRUE(expectSubset(result->asExplicitParetoCurveCheckResult().getPoints(), convertPointset(expectedPoints), eps)) << "Non-Pareto point found."; EXPECT_TRUE(expectSubset(convertPointset(expectedPoints), result->asExplicitParetoCurveCheckResult().getPoints(), eps)) << "Pareto point missing."; } + { + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[7]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"1","0"})); + expectedPoints.emplace_back(std::vector({"0","16"})); + double eps = 1e-4; + EXPECT_TRUE(expectSubset(result->asExplicitParetoCurveCheckResult().getPoints(), convertPointset(expectedPoints), eps)) << "Non-Pareto point found."; + EXPECT_TRUE(expectSubset(convertPointset(expectedPoints), result->asExplicitParetoCurveCheckResult().getPoints(), eps)) << "Pareto point missing."; + } } #endif /* STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE */