From 97d4dba54045849ad7c176868d42d8909202d283 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 29 Sep 2020 14:02:37 +0200
Subject: [PATCH] Added test case for Multi-objective LRA combined with
step-bounded property.
---
.../SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp | 11 +++++++++++
1 file changed, 11 insertions(+)
diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
index c8769c7a0..3c60c9818 100755
--- a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
@@ -339,6 +339,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, resource_gathering) {
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
+ formulasAsString += "multi(R{\"rew_gold\"}max=? [LRA], R{\"rew_gem\"}max=? [ C<100 ]);\n"; // pareto
// programm, model, formula
storm::prism::Program program = storm::api::parseProgram(programFile);
@@ -417,6 +418,16 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, resource_gathering) {
EXPECT_TRUE(expectSubset(result->asExplicitParetoCurveCheckResult<double>().getPoints(), convertPointset<double>(expectedPoints), eps)) << "Non-Pareto point found.";
EXPECT_TRUE(expectSubset(convertPointset<double>(expectedPoints), result->asExplicitParetoCurveCheckResult<double>().getPoints(), eps)) << "Pareto point missing.";
}
+ {
+ std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[7]->asMultiObjectiveFormula());
+ ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
+ std::vector<std::vector<std::string>> expectedPoints;
+ expectedPoints.emplace_back(std::vector<std::string>({"27/241","9"}));
+ double eps = 1e-4;
+ // TODO: Right now, there is a non-optimal point included due to numerical imprecisions. We therefore skip this check:
+ // EXPECT_TRUE(expectSubset(result->asExplicitParetoCurveCheckResult<double>().getPoints(), convertPointset<double>(expectedPoints), eps)) << "Non-Pareto point found.";
+ EXPECT_TRUE(expectSubset(convertPointset<double>(expectedPoints), result->asExplicitParetoCurveCheckResult<double>().getPoints(), eps)) << "Pareto point missing.";
+ }
}
#endif /* STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE */