From 172b17d7ae05ecbc0a2a1d11ea15adefa8c598fc Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 28 Aug 2017 14:59:02 +0200
Subject: [PATCH] simple testcase for the reward unfolding
---
.../examples/testfiles/mdp/one_dim_walk.nm | 21 ++++
...MdpMultiDimensionalRewardUnfoldingTest.cpp | 113 ++++++++++++++++++
2 files changed, 134 insertions(+)
create mode 100644 resources/examples/testfiles/mdp/one_dim_walk.nm
create mode 100644 src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp
diff --git a/resources/examples/testfiles/mdp/one_dim_walk.nm b/resources/examples/testfiles/mdp/one_dim_walk.nm
new file mode 100644
index 000000000..7ad51b3e8
--- /dev/null
+++ b/resources/examples/testfiles/mdp/one_dim_walk.nm
@@ -0,0 +1,21 @@
+mdp
+const int N;
+
+const double p = 0.5;
+
+module main
+ x : [0..N] init N/2;
+
+ [right] x<N -> p : (x'=x+1) + (1-p) : (x'=x);
+ [left] x>0 -> p : (x'=x-1) + (1-p) : (x'=x);
+
+endmodule
+
+rewards "r"
+ [right] true : 1;
+ endrewards
+
+
+ rewards "l"
+ [left] true : 1;
+ endrewards
\ No newline at end of file
diff --git a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp
new file mode 100644
index 000000000..49bd83227
--- /dev/null
+++ b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp
@@ -0,0 +1,113 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.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/utility/constants.h"
+#include "storm/api/storm.h"
+
+
+TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) {
+
+ std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm";
+ std::string constantsDef = "N=2";
+ std::string formulasAsString = "multi(Pmax=? [ F{\"r\"}<=1 x=N ]) ";
+ formulasAsString += "; \n multi(Pmax=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )])";
+ formulasAsString += "; \n multi(Pmin=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )])";
+ formulasAsString += "; \n multi(Pmax=? [ F{\"r\"}<=1 x=N], Pmax=? [ F{\"l\"}<=2 x=0])";
+ formulasAsString += "; \n multi(Pmin=? [ F{\"r\"}<=1 x=N], Pmax=? [ F{\"l\"}<=2 x=0])";
+ formulasAsString += "; \n multi(Pmin=? [ F{\"r\"}<=1 x=N], Pmin=? [ F{\"l\"}<=2 x=0])";
+
+ // programm, model, formula
+ storm::prism::Program program = storm::api::parseProgram(programFile);
+ program = storm::utility::prism::preprocess(program, constantsDef);
+ std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+ std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
+ uint_fast64_t const initState = *mdp->getInitialStates().begin();;
+
+ std::unique_ptr<storm::modelchecker::CheckResult> result;
+
+ result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula());
+ ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+ EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.5), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+ result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula());
+ ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+ EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.125), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+ result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula());
+ ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+ EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+ result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[3]->asMultiObjectiveFormula());
+ ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
+ std::vector<storm::RationalNumber> p1 = {storm::utility::convertNumber<storm::RationalNumber>(0.5), storm::utility::convertNumber<storm::RationalNumber>(0.5)};
+ std::vector<storm::RationalNumber> q1 = {storm::utility::convertNumber<storm::RationalNumber>(0.125), storm::utility::convertNumber<storm::RationalNumber>(0.75)};
+ auto expectedAchievableValues = storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p1, q1}));
+
+ EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
+ EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
+
+ result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[4]->asMultiObjectiveFormula());
+ ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
+ std::vector<storm::RationalNumber> p2 = {storm::utility::convertNumber<storm::RationalNumber>(0.0), storm::utility::convertNumber<storm::RationalNumber>(0.75)};
+ expectedAchievableValues = storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p2}));
+ std::vector<std::vector<storm::RationalNumber>> transformationMatrix(2, std::vector<storm::RationalNumber>(2, storm::utility::zero<storm::RationalNumber>()));
+ transformationMatrix[0][0] = -storm::utility::one<storm::RationalNumber>();
+ transformationMatrix[1][1] = storm::utility::one<storm::RationalNumber>();
+ expectedAchievableValues = expectedAchievableValues->affineTransformation(transformationMatrix, std::vector<storm::RationalNumber>(2, storm::utility::zero<storm::RationalNumber>()));
+ EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
+ EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
+
+ result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[5]->asMultiObjectiveFormula());
+ ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
+ std::vector<storm::RationalNumber> p3 = {storm::utility::convertNumber<storm::RationalNumber>(0.0), storm::utility::convertNumber<storm::RationalNumber>(-0.75)};
+ std::vector<storm::RationalNumber> q3 = {storm::utility::convertNumber<storm::RationalNumber>(-0.5), storm::utility::convertNumber<storm::RationalNumber>(0.0)};
+ expectedAchievableValues = storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p3 ,q3}));
+ transformationMatrix[1][1] = -storm::utility::one<storm::RationalNumber>();
+ expectedAchievableValues = expectedAchievableValues->affineTransformation(transformationMatrix, std::vector<storm::RationalNumber>(2, storm::utility::zero<storm::RationalNumber>()));
+ EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
+ EXPECT_TRUE(result->asExplicitParetoCurveCheckResult<storm::RationalNumber>().getOverApproximation()->contains(expectedAchievableValues));
+
+}
+
+TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_large) {
+
+ std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm";
+ std::string constantsDef = "N=10";
+ std::string formulasAsString = "multi(Pmax=? [ F{\"r\"}<=5 x=N ]) ";
+ formulasAsString += "; \n multi(Pmax=? [ multi( F{\"r\"}<=5 x=N, F{\"l\"}<=10 x=0 )])";
+ formulasAsString += "; \n multi(P>=1/512 [ F{\"r\"}<=5 x=N], Pmax=? [ F{\"l\"}<=10 x=0])";
+
+ // programm, model, formula
+ storm::prism::Program program = storm::api::parseProgram(programFile);
+ program = storm::utility::prism::preprocess(program, constantsDef);
+ std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
+ std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
+ uint_fast64_t const initState = *mdp->getInitialStates().begin();;
+
+ std::unique_ptr<storm::modelchecker::CheckResult> result;
+
+ result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula());
+ ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+ storm::RationalNumber expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 5);
+ EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+ result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula());
+ ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+ expectedResult = storm::utility::pow(storm::utility::convertNumber<storm::RationalNumber>(0.5), 15);
+ EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+ result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula());
+ ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+ expectedResult = storm::utility::convertNumber<storm::RationalNumber, std::string>("2539/4096");
+ EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
+
+}
+
+