diff --git a/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp index b78eead1b..ad9699e46 100644 --- a/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp @@ -16,23 +16,19 @@ #include "storm/api/storm.h" -/* Rationals for MAs not supported at this point TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto - // formulasAsString += "; \n multi(..)"; // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); program.checkValidity(); - std::vector> formulas = storm::api::extractFormulasFromProperties(parseFormulasForProgram(formulasAsString, program)); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); storm::generator::NextStateGeneratorOptions options(formulas); std::shared_ptr> ma = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); - storm::modelchecker::SparseMarkovAutomatonCslModelChecker> checker(*ma); - - std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); storm::RationalNumber p1 = storm::utility::convertNumber(11.0); p1 /= storm::utility::convertNumber(6.0); @@ -45,7 +41,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) { EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); -}*/ +} TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) {