diff --git a/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp index 18b44c44d..1c27f5055 100644 --- a/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp +++ b/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp @@ -65,5 +65,6 @@ namespace storm { template class SparseMaMultiObjectiveModelChecker>; + // template class SparseMaMultiObjectiveModelChecker>; } } diff --git a/test/functional/modelchecker/SparseMaMultiObjectiveModelCheckerTest.cpp b/test/functional/modelchecker/SparseMaMultiObjectiveModelCheckerTest.cpp index 3b630533e..921795ae1 100644 --- a/test/functional/modelchecker/SparseMaMultiObjectiveModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMaMultiObjectiveModelCheckerTest.cpp @@ -9,13 +9,14 @@ #include "src/modelchecker/results/ParetoCurveCheckResult.h" #include "src/models/sparse/MarkovAutomaton.h" #include "src/storage/geometry/Polytope.h" +#include "src/storage/geometry/Hyperrectangle.h" #include "src/settings/modules/GeneralSettings.h" #include "src/settings/SettingsManager.h" #include "src/utility/storm.h" - -TEST(SparseMdpMultiObjectiveModelCheckerTest, server) { +/* Rationals for MAs not supported at this point +TEST(SparseMaMultiObjectiveModelCheckerTest, serverRationalNumbers) { std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/ma/server/server.ma"; std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto @@ -26,9 +27,9 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, server) { program.checkValidity(); std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); storm::generator::NextStateGeneratorOptions options(formulas); - std::shared_ptr> ma = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); + std::shared_ptr> ma = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); - storm::modelchecker::SparseMaMultiObjectiveModelChecker> checker(*ma); + storm::modelchecker::SparseMaMultiObjectiveModelChecker> checker(*ma); std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); ASSERT_TRUE(result->isParetoCurveCheckResult()); @@ -43,6 +44,38 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, server) { EXPECT_TRUE(expectedAchievableValues->contains(result->asParetoCurveCheckResult().getUnderApproximation())); EXPECT_TRUE(result->asParetoCurveCheckResult().getUnderApproximation()->contains(expectedAchievableValues)); +}*/ + + +TEST(SparseMaMultiObjectiveModelCheckerTest, server) { + + std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/ma/server/server.ma"; + std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto + // formulasAsString += "; \n multi(..)"; + + // programm, model, formula + storm::prism::Program program = storm::parseProgram(programFile); + program.checkValidity(); + std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); + storm::generator::NextStateGeneratorOptions options(formulas); + std::shared_ptr> ma = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); + + storm::modelchecker::SparseMaMultiObjectiveModelChecker> checker(*ma); + + std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); + ASSERT_TRUE(result->isParetoCurveCheckResult()); + + std::vector p = {11.0/6.0, 1.0/2.0}; + std::vector q = {29.0/18.0, 2.0/3.0}; + auto expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p,q})); + // due to precision issues, we enlarge one of the polytopes before checking containement + std::vector lb = {-storm::settings::getModule().getPrecision(), -storm::settings::getModule().getPrecision()}; + std::vector ub = {storm::settings::getModule().getPrecision(), storm::settings::getModule().getPrecision()}; + auto bloatingBox = storm::storage::geometry::Hyperrectangle(lb,ub).asPolytope(); + + EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult().getUnderApproximation())); + EXPECT_TRUE(result->asParetoCurveCheckResult().getUnderApproximation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); + }