diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 866e63fb0..056c84a88 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -195,4 +195,14 @@ TEST(FragmentCheckerTest, Rpatl) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2,3>> Pmin=? [F [2,5] \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <<1,2,3,4,5>> Pmax=? [\"label1\" U [0,7] \"label2\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmax=? [G <=5 \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmin=? [G [0,1] \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + }