From ee06a1f1a6997481331e877b2df5296da42d6921 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 28 Sep 2020 19:29:47 +0200
Subject: [PATCH] Also added test case for lra operator formula.

---
 .../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 3e34f6139..b1403f9a0 100755
--- a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
@@ -235,6 +235,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, simple_lra) {
     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
+    formulasAsString += "multi(LRAmax=? [ x=1 ], R{\"second\"}max=? [ LRA ]);\n"; // pareto
     
     // programm, model,  formula
     storm::prism::Program program = storm::api::parseProgram(programFile);
@@ -309,6 +310,16 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, simple_lra) {
         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>({"1","0"}));
+        expectedPoints.emplace_back(std::vector<std::string>({"0","16"}));
+        double eps = 1e-4;
+        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 */