From 3052b19c58bdfd9da7d7b51c50078079f63ec023 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Wed, 12 Feb 2014 02:56:42 +0100
Subject: [PATCH] Created a "real" scc example. Modified the
 TopologicalValueIterationMdpPrctlModelCheckerTest.cpp to show the crash when
 not using TBB.

Former-commit-id: 98b47e957389bbaf164aaede53acc58542b0165c
---
 examples/mdp/scc/scc.pctl                              |  4 ++--
 ...pologicalValueIterationMdpPrctlModelCheckerTest.cpp | 10 +++++-----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/examples/mdp/scc/scc.pctl b/examples/mdp/scc/scc.pctl
index 393670a26..8a853a969 100644
--- a/examples/mdp/scc/scc.pctl
+++ b/examples/mdp/scc/scc.pctl
@@ -1,2 +1,2 @@
-Pmin=? [ F a ]
-Pmax=? [ F a ]
\ No newline at end of file
+Pmin=? [ F end ]
+Pmax=? [ F end ]
\ No newline at end of file
diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
index 114de1b47..874170a4f 100644
--- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
@@ -16,12 +16,12 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
     
 	std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
     
-	ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
-	ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
+	ASSERT_EQ(mdp->getNumberOfStates(), 11ull);
+	ASSERT_EQ(mdp->getNumberOfTransitions(), 17ull);
     
 	storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
     
-	storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
+	storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("end");
 	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
 	storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
     
@@ -30,7 +30,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
 	ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
     
 	delete probFormula;
-    
+	/*
 	apFormula = new storm::property::prctl::Ap<double>("two");
 	eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
 	probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
@@ -149,7 +149,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
 	result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
     
 	ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
-	delete rewardFormula;
+	delete rewardFormula;*/
 }
 
 TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {