From 3789fbb3e921636181b6adfd3d1f8e58f2d25c19 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 28 Sep 2020 19:22:48 +0200 Subject: [PATCH] Test case for multi-objective lra --- .../testfiles/mdp/multiobj_simple_lra.nm | 2 +- ...eMdpPcaaMultiObjectiveModelCheckerTest.cpp | 168 ++++++++++++++++++ 2 files changed, 169 insertions(+), 1 deletion(-) diff --git a/resources/examples/testfiles/mdp/multiobj_simple_lra.nm b/resources/examples/testfiles/mdp/multiobj_simple_lra.nm index 800c3e35a..d6f9d7e16 100644 --- a/resources/examples/testfiles/mdp/multiobj_simple_lra.nm +++ b/resources/examples/testfiles/mdp/multiobj_simple_lra.nm @@ -1,7 +1,7 @@ mdp module main - x : [0..8]; + x : [0..3]; [a] x=0 -> 0.5 : (x'=1) + 0.5 : (x'=0); [a] x=0 -> 0.2 : (x'=0) + 0.8 : (x'=3); [b] x=1 -> (x'=1); diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp index bed96b7b1..3e34f6139 100755 --- a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp @@ -8,10 +8,13 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" #include "storm/models/sparse/Mdp.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/storage/jani/Property.h" +#include "storm/storage/geometry/Polytope.h" +#include "storm/storage/geometry/Hyperrectangle.h" #include "storm/api/storm.h" #include "storm-parsers/api/storm-parsers.h" #include "storm/environment/Environment.h" @@ -141,6 +144,171 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, dpm) { } +template +bool expectPointConained(std::vector> const& pointset, std::vector const& point, ValueType precision) { + for (auto const& p : pointset) { + EXPECT_EQ(p.size(), point.size()) << "Missmatch in point dimension."; + bool found = true; + for (uint64_t i = 0; i < p.size(); ++i) { + if (storm::utility::abs(p[i] - point[i]) > precision) { + found = false; + break; + } + } + if (found) { + return true; + } + } + // prepare failure message: + std::stringstream errstr; + errstr << "Point ["; + bool firstPi = true; + for (auto const& pi : point) { + if (firstPi) { + firstPi = false; + } else { + errstr << ", "; + } + errstr << pi; + } + errstr << "] is not contained in point set {"; + bool firstP = true; + for (auto const& p : pointset) { + if (firstP) { + firstP = false; + } else { + errstr << ", \t"; + } + errstr << "["; + firstPi = true; + for (auto const& pi : p) { + if (firstPi) { + firstPi = false; + } else { + errstr << ", "; + } + errstr << pi; + } + errstr << "]"; + } + errstr << "}."; + ADD_FAILURE() << errstr.str(); + return false; +} + + +template +bool expectSubset(std::vector> const& lhs, std::vector> const& rhs, ValueType precision) { + for (auto const& p : lhs) { + if (!expectPointConained(rhs, p, precision)) { + return false; + } + } + return true; +} +template +std::vector> convertPointset(std::vector> const& in) { + std::vector> out; + for (auto const& point_str : in) { + out.emplace_back(); + for (auto const& pi_str : point_str) { + out.back().push_back(storm::utility::convertNumber(pi_str)); + } + } + return out; +} + +TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, simple_lra) { + if (!storm::test::z3AtLeastVersion(4,8,5)) { + GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3."; + } + storm::Environment env; + env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa); + + + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_simple_lra.nm"; + std::string formulasAsString = "multi(R{\"first\"}max=? [ LRA ], R{\"second\"}max=? [ LRA ]);\n"; // pareto + formulasAsString += "multi(R{\"first\"}min=? [ LRA ], R{\"second\"}max=? [ LRA ]);\n"; // pareto + formulasAsString += "multi(R{\"first\"}min=? [ LRA ], R{\"second\"}min=? [ LRA ]);\n"; // pareto + formulasAsString += "multi(R{\"first\"}min=? [ C ], R{\"second\"}min=? [ LRA ]);\n"; // pareto + 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 + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program.checkValidity(); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + storm::generator::NextStateGeneratorOptions options(formulas); + auto mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); + + { + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"5","80/11"})); + 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."; + } + { + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + 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."; + } + { + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"0","0"})); + 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."; + } + { + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[3]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"10/8","0"})); + 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."; + } + { + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[4]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"10/8","0"})); + 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."; + } + { + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[5]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"10/8", "0", "10/8"})); + expectedPoints.emplace_back(std::vector({"7", "16", "2"})); + 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."; + } + { + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[6]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"0","0", "10/8"})); + expectedPoints.emplace_back(std::vector({"0","16", "2"})); + 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 */