Created a "real" scc example.

Modified the TopologicalValueIterationMdpPrctlModelCheckerTest.cpp to show the crash when not using TBB.


Former-commit-id: 98b47e9573

examples/mdp/scc/scc.pctl

@@ -1,2 +1,2 @@
-Pmin=? [ F a ]
-Pmax=? [ F a ]
+Pmin=? [ F end ]
+Pmax=? [ F end ]

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) {