From c990d27c500537901d18d789ce9ec5ed7e7311b7 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 29 Sep 2020 13:22:48 +0200 Subject: [PATCH] Added MA test case + fixes --- .../testfiles/ma/multiobj_simple_lra.ma | 22 +++ .../StandardMaPcaaWeightVectorChecker.cpp | 4 +- .../pcaa/StandardPcaaWeightVectorChecker.cpp | 4 +- ...seMaPcaaMultiObjectiveModelCheckerTest.cpp | 148 ++++++++++++++++++ 4 files changed, 176 insertions(+), 2 deletions(-) create mode 100644 resources/examples/testfiles/ma/multiobj_simple_lra.ma diff --git a/resources/examples/testfiles/ma/multiobj_simple_lra.ma b/resources/examples/testfiles/ma/multiobj_simple_lra.ma new file mode 100644 index 000000000..045c86563 --- /dev/null +++ b/resources/examples/testfiles/ma/multiobj_simple_lra.ma @@ -0,0 +1,22 @@ +ma +module main + + x : [0..4]; + [a] x=0 -> 0.5 : (x'=1) + 0.5 : (x'=0); + [b] x=0 -> (x'=2); + <> x=1 -> 6 : (x'=2) + 4 : (x'=4); + <> x=2 -> 5 : (x'=2) + 5 : (x'=3); + [c] x=3 -> 0.3 : (x'=2) + 0.7 : (x'=4); + [d] x=3 -> 0.3 : (x'=4) + 0.7 : (x'=2); + <> x=4 -> 5 : (x'=3); +endmodule + +rewards "first" + true : 3; + [] x=2 : 10; + [d] true : 5; +endrewards + +rewards "second" + x<2 : 42; +endrewards diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp index 628862cca..64641b3a8 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp @@ -73,7 +73,9 @@ namespace storm { storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper StandardMaPcaaWeightVectorChecker::createDetInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitions) const { STORM_LOG_ASSERT(transitions.getRowGroupCount() == this->transitionMatrix.getRowGroupCount(), "Unexpected size of given matrix."); // TODO: Right now, there is no dedicated support for "deterministic" Markov automata so we have to pick the nondeterministic one. - return storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper(transitions, this->markovianStates, this->exitRates); + auto result = storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper(transitions, this->markovianStates, this->exitRates); + result.setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); + return result; } template diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 97e7522c5..42c8f5ff8 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -118,7 +118,9 @@ namespace storm { ValueType weight = storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex]; storm::utility::vector::addScaledVector(weightedRewardVector, actionRewards[objIndex], weight); if (!stateRewards.empty() && !stateRewards[objIndex].empty()) { - weightedStateRewardVector->resize(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + if (!weightedStateRewardVector) { + weightedStateRewardVector = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + } storm::utility::vector::addScaledVector(weightedStateRewardVector.get(), stateRewards[objIndex], weight); } } diff --git a/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp index 1fcd25efa..80bbd3752 100755 --- a/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp @@ -213,4 +213,152 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_2Obj) { } +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(SparseMaPcaaMultiObjectiveModelCheckerTest, 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 "/ma/multiobj_simple_lra.ma"; + std::string formulasAsString = "multi(R{\"first\"}max=? [LRA], LRAmax=? [ x=4 ] );\n"; // pareto + formulasAsString += "multi(R{\"first\"}max=? [LRA], LRAmin=? [ x=4] );\n"; // pareto + formulasAsString += "multi(R{\"first\"}max=? [LRA], LRAmin=? [ x=4] , R{\"second\"}max=? [LRA]);\n"; // pareto + formulasAsString += "multi(R{\"first\"}max=? [LRA], LRAmax=? [ x=4] , R{\"second\"}max=? [C]);\n"; // pareto + formulasAsString += "multi(R{\"first\"}max=? [LRA], LRAmax=? [ x=4] , R{\"second\"}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 ma = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); + + { + std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"98","3/10"})); + expectedPoints.emplace_back(std::vector({"33","7/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, *ma, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"98","3/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, *ma, formulas[2]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"98","3/10", "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, *ma, formulas[3]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"98", "3/10", "42/10"})); + expectedPoints.emplace_back(std::vector({"33", "7/10", "42/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, *ma, formulas[4]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector> expectedPoints; + expectedPoints.emplace_back(std::vector({"98", "3/10", "0"})); + expectedPoints.emplace_back(std::vector({"33", "7/10", "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 /* defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE */