From 5bfb3b132e13c542b4768246307dee82faa8ceec Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 29 Sep 2020 11:42:17 +0200 Subject: [PATCH] New MDP LRA Test case + fix --- .../pcaa/StandardPcaaWeightVectorChecker.cpp | 4 +- ...eMdpPcaaMultiObjectiveModelCheckerTest.cpp | 97 +++++++++++++++++++ 2 files changed, 99 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index c001ca1ca..97e7522c5 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -93,7 +93,7 @@ namespace storm { // Set data for LRA objectives (if available) if (!lraObjectives.empty()) { lraMecDecomposition = LraMecDecomposition(); - lraMecDecomposition->mecs = storm::storage::MaximalEndComponentDecomposition(transitionMatrix, transitionMatrix.transpose(true), totalReward0EStates, actionsWithoutRewardInUnboundedPhase); + lraMecDecomposition->mecs = storm::storage::MaximalEndComponentDecomposition(transitionMatrix, transitionMatrix.transpose(true), storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), actionsWithoutRewardInUnboundedPhase); lraMecDecomposition->auxMecValues.resize(lraMecDecomposition->mecs.size()); } @@ -710,7 +710,7 @@ namespace storm { } } else { // LRA mec is proper subset of eliminated ec. There are also other states for which we have to set choices leading to the LRA MEC inside. - STORM_LOG_ASSERT(lraMec.size() < origStates.size(), "Lra Mec should be a proper subset of the eliminated ec."); + STORM_LOG_ASSERT(lraMec.size() < origStates.size(), "Lra Mec (" << lraMec.size() << " states) should be a proper subset of the eliminated ec (" << origStates.size() << " states)."); for (auto const& state : origStates) { if (lraMec.containsState(state)) { ecStatesToReach.set(state, true); diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp index b1403f9a0..c8769c7a0 100755 --- a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp @@ -322,4 +322,101 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, simple_lra) { } } +TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, resource_gathering) { + 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/resource-gathering.nm"; + std::string constantsDef = "GOLD_TO_COLLECT=0,GEM_TO_COLLECT=0,B=0"; + std::string formulasAsString = "multi(R{\"rew_gold\"}max=? [LRA], R{\"rew_gem\"}max=? [LRA]);\n"; // pareto + formulasAsString += "multi(R{\"rew_gold\"}min=? [LRA], R{\"rew_gem\"}max=? [LRA]);\n"; // pareto + formulasAsString += "multi(R{\"rew_gold\"}max=? [LRA], R{\"rew_gem\"}min=? [LRA]);\n"; // pareto + formulasAsString += "multi(R{\"rew_gold\"}min=? [LRA], R{\"rew_gem\"}min=? [LRA]);\n"; // pareto + formulasAsString += "multi(R{\"rew_gold\"}max=? [LRA], R{\"attacks\"}min=? [LRA]);\n"; // pareto + formulasAsString += "multi(R{\"rew_gold\"}max=? [LRA], R{\"attacks\"}min=? [C]);\n"; // pareto + formulasAsString += "multi(R{\"rew_gold\"}max=? [LRA], R{\"rew_gem\"}max=? [LRA], R{\"attacks\"}min=? [C]);\n"; // pareto + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsDef); + 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({"27/241","0"})); + expectedPoints.emplace_back(std::vector({"0","1/10"})); + expectedPoints.emplace_back(std::vector({"27/349","27/349"})); + 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","1/10"})); + 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({"27/241","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({"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[4]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"27/241","19/723"})); + expectedPoints.emplace_back(std::vector({"3/31","1/93"})); + expectedPoints.emplace_back(std::vector({"1/12","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({"1/12","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[6]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"1/12","0","0"})); + expectedPoints.emplace_back(std::vector({"0","1/10","0"})); + expectedPoints.emplace_back(std::vector({"1/18","1/18","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."; + } +} + #endif /* STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE */