modelchecker test update

src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp

@@ -722,10 +722,12 @@ namespace {
         setenv("LTL2DA", "ltl2da-ltl2tgba", true); //todo set PATH variable
 
         std::string formulasString = "P=? [(X s>0) U (s=7 & d=2)]";
-        formulasString += "; P=? [ X (s=1) U (s=3) U (s=7)]";  //  a U b U c  is Treated as: (a U b ) U c
-        formulasString += "; P=? [ G s!=3 U (\"three\") ]";
+        formulasString += "; P=? [  X (((s=1) U (s=3)) U (s=7))]";
         formulasString += "; P=? [ (F (X (s=6 & (XX s=5)))) & (F G (d!=5))]";
-        formulasString += "; P=? [ F ((s=6) & (X \"done\"))]";
+        formulasString += "; P=? [ F (s=3 U (\"three\"))]";
+        formulasString += "; P=? [ F s=3 U (\"three\")]";
+        formulasString += "; P=? [ F (s=6) & (X \"done\")]";  //todo without ()
+        formulasString += "; P=? [ (F s=6) & (X \"done\")]";
 
         storm::prism::Program program = storm::api::parseProgram(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
         auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
@@ -744,20 +746,27 @@ namespace {
         EXPECT_NEAR(1/6, result->asQuantitativeCheckResult<double>().getMin(), 1e-6);
 
         result = checker.check(tasks[2]);
-        EXPECT_NEAR(1/8, result->asQuantitativeCheckResult<double>().getMin(), 1e-6);
+        EXPECT_NEAR(1/24, result->asQuantitativeCheckResult<double>().getMin(), 1e-6);
 
         result = checker.check(tasks[3]);
-        EXPECT_NEAR(1/24, result->asQuantitativeCheckResult<double>().getMin(), 1e-6);
+        EXPECT_NEAR(1/6, result->asQuantitativeCheckResult<double>().getMin(), 1e-6);
 
         result = checker.check(tasks[4]);
+        EXPECT_NEAR(0, result->asQuantitativeCheckResult<double>().getMin(), 1e-6);
+
+        result = checker.check(tasks[5]);
         EXPECT_NEAR(1/2, result->asQuantitativeCheckResult<double>().getMin(), 1e-6);
+
+        result = checker.check(tasks[6]);
+        EXPECT_NEAR(0, result->asQuantitativeCheckResult<double>().getMin(), 1e-6);
     }
 
     TEST(DtmcPrctlModelCheckerTest, LtlProbabilitiesSynchronousLeader) {
         setenv("LTL2DA", "ltl2da-ltl2tgba", true);
         std::string formulasString = "P=? [X (u1=true U \"elected\")]";
-        formulasString += "; P=? [X v1=2 & (X v1=1)]"; // (X v1=2 & (XX v1=1)
+        formulasString += "; P=? [X v1=2 & (X v1=1)]"; // (X v1=2 & (XX v1=1))
         formulasString += "; P=? [(X v1=2) & (X v1=1)]";
+        //todo (X v1=2 & XX v1=1)
 
         storm::prism::Program program = storm::api::parseProgram(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm");
         auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
@@ -777,6 +786,10 @@ namespace {
 
         result = checker.check(tasks[2]);
         EXPECT_NEAR(0, result->asQuantitativeCheckResult<double>().getMin(), 1e-6);
+
+        //  (X v1=2 & XX v1=1)
+        //result = checker.check(tasks[3]);
+        //EXPECT_NEAR(1/25, result->asQuantitativeCheckResult<double>().getMin(), 1e-6);
     }
 
 }