diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp
index 454c29ac1..9771e0ae1 100644
--- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp
@@ -146,6 +146,7 @@ namespace storm {
                     }
                 }
                 
+                
                 // At this point, we can be sure that the state was expanded and that we can sample according to the probabilities.
                 // TODO: set action of topmost stack element
             }
diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
index b2a39f5dd..4284ab85c 100644
--- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
+++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
@@ -8,6 +8,7 @@
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "src/utility/solver.h"
 #include "src/parser/AutoParser.h"
+#include "src/parser/FormulaParser.h"
 #include "src/models/sparse/StandardRewardModel.h"
 
 TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
@@ -22,26 +23,26 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
 
     storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
 
-	auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
-    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
 
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
     EXPECT_NEAR(0.2296800237, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeIGreater1");
-    eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
 
-    result = checker.check(*eventuallyFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
     
 	EXPECT_NEAR(0.05073232193, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeOnlyTrueSender");
-    eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
 
-    result = checker.check(*eventuallyFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
     
 	EXPECT_NEAR(0.22742171078, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
@@ -60,27 +61,26 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
 
 	storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
 
-    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
 
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
     
 	EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-    auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
-    auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 20);
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
 
-    result = checker.check(*boundedUntilFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
     
 	EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-    auto reachabilityRewardFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula, storm::logic::FormulaContext::Reward);
+    formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
 
-    result = checker.check(*reachabilityRewardFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
     
 	EXPECT_NEAR(1.025106273, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
diff --git a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
index 23949131a..85d6399c9 100644
--- a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
@@ -2,13 +2,13 @@
 #include "storm-config.h"
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/GmmxxEquationSolverSettings.h"
-
 #include "src/settings/modules/NativeEquationSolverSettings.h"
 #include "src/settings/SettingMemento.h"
 #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "src/utility/solver.h"
 #include "src/parser/AutoParser.h"
+#include "src/parser/FormulaParser.h"
 #include "src/models/sparse/StandardRewardModel.h"
 
 TEST(NativeDtmcPrctlModelCheckerTest, Crowds) {
@@ -23,26 +23,26 @@ TEST(NativeDtmcPrctlModelCheckerTest, Crowds) {
     
     storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
     
-    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
-    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
     
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(0.22968140721646868, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
     
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeIGreater1");
-    eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
     
-    result = checker.check(*eventuallyFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(0.05073232193, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
     
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeOnlyTrueSender");
-    eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
     
-    result = checker.check(*eventuallyFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(0.22742305378217331, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
@@ -60,28 +60,27 @@ TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) {
     ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions());
     
     storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
+
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
     
-    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
     
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
     
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-    auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
-    auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 20);
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
     
-    result = checker.check(*boundedUntilFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
     
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-    auto reachabilityRewardFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula, storm::logic::FormulaContext::Reward);
+    formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
     
-    result = checker.check(*reachabilityRewardFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(1.0252174454896057, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());