From 4bb4e29e43c0dc866deb1eee32e648d0fb4f47d4 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@web.de>
Date: Fri, 18 Mar 2016 16:47:06 +0100
Subject: [PATCH] Added a test case where model checking expected rewards on
 MDPs currently fails

Former-commit-id: 35dbe908c8c3cc6a59225832200e28c315803434
---
 .../GmmxxMdpPrctlModelCheckerTest.cpp         | 33 +++++++++++++++++++
 test/functional/modelchecker/tiny_rewards.nm  | 17 ++++++++++
 2 files changed, 50 insertions(+)
 create mode 100644 test/functional/modelchecker/tiny_rewards.nm

diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
index 93643fd52..22e7d8464 100644
--- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
@@ -240,3 +240,36 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) {
     EXPECT_EQ(0, scheduler2.getChoice(2));
     EXPECT_EQ(0, scheduler2.getChoice(3));
 }
+
+TEST(GmmxxMdpPrctlModelCheckerTest, tiny_rewards) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/tiny_rewards.nm");
+
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>(program).translate();
+    EXPECT_EQ(3ul, model->getNumberOfStates());
+    EXPECT_EQ(4ul, model->getNumberOfTransitions());
+    
+    ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
+
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>();
+
+    EXPECT_EQ(4ul, mdp->getNumberOfChoices());
+
+    auto solverFactory = std::make_unique<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(storm::solver::EquationSolverTypeSelection::Gmmxx);
+    solverFactory->setPreferredTechnique(storm::solver::MinMaxTechniqueSelection::ValueIteration);
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::move(solverFactory));
+    
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"target\"]");
+    
+    storm::modelchecker::CheckTask<storm::logic::Formula> checkTask(*formula);
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(checkTask);
+    
+    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+    EXPECT_NEAR(1,result->asExplicitQuantitativeCheckResult<double>().getValueVector()[0], storm::settings::nativeEquationSolverSettings().getPrecision());
+    EXPECT_NEAR(1,result->asExplicitQuantitativeCheckResult<double>().getValueVector()[1], storm::settings::nativeEquationSolverSettings().getPrecision());
+    EXPECT_NEAR(0,result->asExplicitQuantitativeCheckResult<double>().getValueVector()[2], storm::settings::nativeEquationSolverSettings().getPrecision());
+    
+}
diff --git a/test/functional/modelchecker/tiny_rewards.nm b/test/functional/modelchecker/tiny_rewards.nm
new file mode 100644
index 000000000..5119f6306
--- /dev/null
+++ b/test/functional/modelchecker/tiny_rewards.nm
@@ -0,0 +1,17 @@
+mdp
+
+module mod1
+
+s : [0..2] init 0;
+[] s=0 -> true;
+[] s=0 -> (s'=1);
+[] s=1 -> (s'=2);
+[] s=2 -> (s'=2);
+
+endmodule
+
+rewards
+ [] s=1 : 1;
+endrewards
+
+label "target" = s=2;