From 97a3fc7fa088717d3a51c2e4f8adfc8669d772fc Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 4 Jun 2013 18:13:37 +0200 Subject: [PATCH] Provided test class for ltl2dstar, to avoid copypasting the code to construct the labeling in each test. --- .../Ltl2dstarFormulaAdapterTest.cpp | 46 +++++++++++-------- 1 file changed, 26 insertions(+), 20 deletions(-) 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(); +}