diff --git a/test/functional/ltl2dstarIntegration/Ltl2dstarFormulaAdapterTest.cpp b/test/functional/ltl2dstarIntegration/Ltl2dstarFormulaAdapterTest.cpp index a12aca14a..c39d7e672 100644 --- a/test/functional/ltl2dstarIntegration/Ltl2dstarFormulaAdapterTest.cpp +++ b/test/functional/ltl2dstarIntegration/Ltl2dstarFormulaAdapterTest.cpp @@ -13,12 +13,20 @@ #include "src/adapters/Ltl2dstarFormulaAdapter.h" #include "src/parser/LtlParser.h" -TEST(Ltl2dstarFormulaAdapterTest, ConvertAndFormulaTest) { - storm::parser::LtlParser parser ("a & b"); +class Ltl2dstarFormulaAdapterTest : public testing::Test { +protected: + virtual void SetUp() { + labeling.addAtomicProposition("a"); + labeling.addAtomicProposition("b"); + } + + //virtual void TearDown() - storm::models::AtomicPropositionsLabeling labeling(1, 2); - labeling.addAtomicProposition("a"); - labeling.addAtomicProposition("b"); + storm::models::AtomicPropositionsLabeling labeling = storm::models::AtomicPropositionsLabeling(1,2); +}; + +TEST_F(Ltl2dstarFormulaAdapterTest, ConvertAndFormulaTest) { + storm::parser::LtlParser parser ("a & b"); LTLFormula ltlFormula = storm::adapters::Ltl2dstarFormulaAdapter::convert(*parser.getFormula(), labeling); @@ -27,42 +35,40 @@ TEST(Ltl2dstarFormulaAdapterTest, ConvertAndFormulaTest) { delete parser.getFormula(); } -TEST(Ltl2dstarFormulaAdapterTest, ConvertUntilFormulaTest) { +TEST_F(Ltl2dstarFormulaAdapterTest, ConvertUntilFormulaTest) { storm::parser::LtlParser parser ("a U b"); - storm::models::AtomicPropositionsLabeling labeling(1, 2); - labeling.addAtomicProposition("a"); - labeling.addAtomicProposition("b"); - LTLFormula ltlFormula = storm::adapters::Ltl2dstarFormulaAdapter::convert(*parser.getFormula(), labeling); ASSERT_EQ(ltlFormula.toStringInfix(), "(a) U (b)"); delete parser.getFormula(); } -TEST(Ltl2dstarFormulaAdapterTest, ConvertNextEventuallyFormulaTest) { +TEST_F(Ltl2dstarFormulaAdapterTest, ConvertNextEventuallyFormulaTest) { storm::parser::LtlParser parser ("(F a) & X b"); - storm::models::AtomicPropositionsLabeling labeling(1, 2); - labeling.addAtomicProposition("a"); - labeling.addAtomicProposition("b"); - LTLFormula ltlFormula = storm::adapters::Ltl2dstarFormulaAdapter::convert(*parser.getFormula(), labeling); ASSERT_EQ(ltlFormula.toStringInfix(), "(<> (a)) && (X (b))"); delete parser.getFormula(); } -TEST(Ltl2dstarFormulaAdapterTest, ConvertBoundedEventuallyFormulaTest) { +TEST_F(Ltl2dstarFormulaAdapterTest, ConvertBoundedEventuallyFormulaTest) { storm::parser::LtlParser parser ("F <= 3 a"); - storm::models::AtomicPropositionsLabeling labeling(1, 2); - labeling.addAtomicProposition("a"); - labeling.addAtomicProposition("b"); - LTLFormula ltlFormula = storm::adapters::Ltl2dstarFormulaAdapter::convert(*parser.getFormula(), labeling); //Bounded eventually is "unrolled", as Ltl2dstar does not support bounded operators ASSERT_EQ(ltlFormula.toStringInfix(), "(a) || (X ((a) || (X ((a) || (X (a))))))"); delete parser.getFormula(); } + +TEST_F(Ltl2dstarFormulaAdapterTest, ConvertBoundedUntilFormulaTest) { + storm::parser::LtlParser parser ("a U<=3 b"); + + LTLFormula ltlFormula = storm::adapters::Ltl2dstarFormulaAdapter::convert(*parser.getFormula(), labeling); + + //Bounded until is "unrolled", as Ltl2dstar does not support bounded operators + ASSERT_EQ(ltlFormula.toStringInfix(), "(b) || ((a) && (X ((b) || ((a) && (X ((b) || ((a) && (X (b)))))))))"); + delete parser.getFormula(); +}