Fixed permissive scheduler tests (GitHub issue #38).

src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp

@@ -19,13 +19,18 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) {
     
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm");
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
+    std::string formulaString = "";
+    formulaString += "P>=0.10 [ F \"one\"];\n";
+    formulaString += "P>=0.17 [ F \"one\"];\n";
+    formulaString += "P<=0.10 [ F \"one\"];\n";
+    formulaString += "P<=0.17 [ F \"one\"];\n";
+    auto formulas = formulaParser.parseFromString(formulaString);
     
-    auto formula02 = formulaParser.parseSingleFormulaFromString("P>=0.10 [ F \"one\"]")->asProbabilityOperatorFormula();
+    auto const& formula02 = formulas[0].getRawFormula()->asProbabilityOperatorFormula();
     ASSERT_TRUE(storm::logic::isLowerBound(formula02.getComparisonType()));
-    auto formula001 = formulaParser.parseSingleFormulaFromString("P>=0.17 [ F \"one\"]")->asProbabilityOperatorFormula();
-    
-    auto formula02b = formulaParser.parseSingleFormulaFromString("P<=0.10 [ F \"one\"]")->asProbabilityOperatorFormula();
-    auto formula001b = formulaParser.parseSingleFormulaFromString("P<=0.17 [ F \"one\"]")->asProbabilityOperatorFormula();
+    auto const& formula001 = formulas[1].getRawFormula()->asProbabilityOperatorFormula();
+    auto const& formula02b = formulas[2].getRawFormula()->asProbabilityOperatorFormula();
+    auto const& formula001b = formulas[3].getRawFormula()->asProbabilityOperatorFormula();
     
     // Customize and perform model-building.
     storm::generator::NextStateGeneratorOptions options;

src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp

@@ -20,14 +20,18 @@ TEST(SmtPermissiveSchedulerTest, DISABLED_DieSelection) {
     storm::Environment env;
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm");
     storm::parser::FormulaParser formulaParser(program);
+    std::string formulaString = "";
+    formulaString += "P<=0.16 [ F \"one\"];\n";
+    formulaString += "P<=0.05 [ F \"one\"];\n";
+    auto formulas = formulaParser.parseFromString(formulaString);
     
+    auto const& formula02b = formulas[0].getRawFormula()->asProbabilityOperatorFormula();
+    auto const& formula001b = formulas[1].getRawFormula()->asProbabilityOperatorFormula();
+  
 //    auto formula02 = formulaParser.parseSingleFormulaFromString("P>=0.10 [ F \"one\"]")->asProbabilityOperatorFormula();
 //    ASSERT_TRUE(storm::logic::isLowerBound(formula02.getComparisonType()));
 //    auto formula001 = formulaParser.parseSingleFormulaFromString("P>=0.17 [ F \"one\"]")->asProbabilityOperatorFormula();
     
-    auto formula02b = formulaParser.parseSingleFormulaFromString("P<=0.16 [ F \"one\"]")->asProbabilityOperatorFormula();
-    auto formula001b = formulaParser.parseSingleFormulaFromString("P<=0.05 [ F \"one\"]")->asProbabilityOperatorFormula();
-    
     // Customize and perform model-building.
     storm::generator::NextStateGeneratorOptions options(formula02b);