updated ltl tests

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

@@ -718,6 +718,7 @@ namespace {
     }
 
     TYPED_TEST(DtmcPrctlModelCheckerTest, LtlProbabilitiesDie) {
+#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
         std::string formulasString = "P=? [(X s>0) U (s=7 & d=2)]";
         formulasString += "; P=? [  X (((s=1) U (s=3)) U (s=7))]";
         formulasString += "; P=? [ (F (X (s=6 & (XX s=5)))) & (F G (d!=5))]";
@@ -760,9 +761,13 @@ namespace {
         } else {
             EXPECT_FALSE(checker->canHandle(tasks[0]));
         }
+#else
+        GTEST_SKIP();
+#endif
     }
 
     TYPED_TEST(DtmcPrctlModelCheckerTest, LtlProbabilitiesSynchronousLeader) {
+#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
         std::string formulasString = "P=? [X (u1=true U \"elected\")]";
         formulasString += "; P=? [X !(u1=true U \"elected\")]";
         formulasString += "; P=? [X v1=2 & X v1=1]";
@@ -798,6 +803,9 @@ namespace {
         } else {
             EXPECT_FALSE(checker->canHandle(tasks[0]));
         }
+#else
+        GTEST_SKIP();
+#endif
     }
 
 }

src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp

@@ -700,6 +700,8 @@ namespace {
 #ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
         std::string formulasString = "Pmin=? [!(GF \"all_coins_equal_1\")]";
         formulasString += "; Pmax=? [F \"all_coins_equal_1\" U \"finished\"]";
+        // The following example results in an automaton with acceptance condition not in DNF (using spot)
+        formulasString += "; Pmax=?[ (GF !\"all_coins_equal_1\") & ((GF \"all_coins_equal_1\") | (FG \"finished\"))]";
 
         auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", formulasString);
         auto model = std::move(modelFormulas.first);
@@ -718,13 +720,18 @@ namespace {
             result = checker->check(this->env(), tasks[1]);
             EXPECT_NEAR(this->parseNumber("5/9"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
 
+            result = checker->check(this->env(), tasks[2]);
+            EXPECT_NEAR(this->parseNumber("79/128"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+
+
         } else {
             EXPECT_FALSE(checker->canHandle(tasks[0]));
         }
-    }
 #else
         GTEST_SKIP();
 #endif
+    }
+
 
 
 }