From 1e5de29eec42bcc87241e19d3aedcb3d34121675 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 4 Jun 2013 17:46:38 +0200 Subject: [PATCH] Conversion adapter to create LTL2DStar formulas out of "ours" --- src/adapters/Ltl2dstarFormulaAdapter.h | 284 ++++++++++++++++++ src/models/AtomicPropositionsLabeling.h | 19 ++ src/parser/CslParser.cpp | 6 +- src/parser/LtlParser.cpp | 6 +- src/parser/PrctlParser.cpp | 6 +- .../Ltl2dstarFormulaAdapterTest.cpp | 68 +++++ 6 files changed, 386 insertions(+), 3 deletions(-) create mode 100644 src/adapters/Ltl2dstarFormulaAdapter.h create mode 100644 test/functional/ltl2dstarIntegration/Ltl2dstarFormulaAdapterTest.cpp diff --git a/src/adapters/Ltl2dstarFormulaAdapter.h b/src/adapters/Ltl2dstarFormulaAdapter.h new file mode 100644 index 000000000..5596bfbe8 --- /dev/null +++ b/src/adapters/Ltl2dstarFormulaAdapter.h @@ -0,0 +1,284 @@ +/* + * Ltl2dstarFormulaAdapter.h + * + * Created on: 29.05.2013 + * Author: Thomas Heinemann + */ + +#ifndef STORM_ADAPTER_LTL2DSTARFORMULAADAPTER_H_ +#define STORM_ADAPTER_LTL2DSTARFORMULAADAPTER_H_ + +#include "formula/Ltl.h" +#include "models/AtomicPropositionsLabeling.h" + +#include "LTLFormula.hpp" //LTL2Dstar include file + +namespace storm { +namespace adapters { + +/*! + * @brief + * Conversion routines for creating an equivalent formula of the LTL2DStar classes out of storm formula classes. + * + * @note + * Storm allows bounded until and eventually operators, which are not available in LTL2Dstar + * These formulas are unfolded into an equivalent formula using nested next operators. + * + * This class uses the visitor pattern for traversing the LTL formula. + * Due to the limitations of templates in C++ the callback for the visit functions are of type void. As a workaround, + * intermediate result formulas are stored in the field intermediateResult. + * + */ +template +class Ltl2dstarFormulaAdapter : + public storm::property::ltl::visitor::AbstractLtlFormulaVisitor, + public storm::property::ltl::IAndVisitor, + public storm::property::ltl::IApVisitor, + public storm::property::ltl::IBoundedEventuallyVisitor, + public storm::property::ltl::IBoundedUntilVisitor, + public storm::property::ltl::IEventuallyVisitor, + public storm::property::ltl::IGloballyVisitor, + public storm::property::ltl::INextVisitor, + public storm::property::ltl::INotVisitor, + public storm::property::ltl::IOrVisitor, + public storm::property::ltl::IUntilVisitor { +public: + virtual ~Ltl2dstarFormulaAdapter() { + // TODO Auto-generated destructor stub + } + + /*! + * Visit method for an ltl And formula. + * Stores the converted formula (in LTL2Dstar classes) in the field intermediateResult + * + * @param formula Reference to the And formula that is to be visited. + */ + virtual void visitAnd(const storm::property::ltl::And& formula) { + this->visit(formula.getLeft()); + LTLNode_p left = intermediateResult; + this->visit(formula.getRight()); + LTLNode_p right = intermediateResult; + intermediateResult.reset(new LTLNode(LTLNode::T_AND, left, right)); + } + + /*! + * Visit method for an ltl Ap formula. + * Stores the converted formula (in LTL2Dstar classes) in the field intermediateResult + * + * @param formula Reference to the Ap formula that is to be visited. + */ + virtual void visitAp(const storm::property::ltl::Ap& formula) { + intermediateResult.reset(new LTLNode(apset->find(formula.getAp()))); + } + + /*! + * Visit method for an ltl Bounded Eventually formula. + * Stores the converted formula (in LTL2Dstar classes) in the field intermediateResult + * + * As Bounded Eventually is not supported in LTL2Dstar, the formula is unfolded into an equivalent + * formula using nested Next operators. + * + * @param formula Reference to the Bounded Eventually formula that is to be visited. + */ + virtual void visitBoundedEventually(const storm::property::ltl::BoundedEventually& formula) { + this->visit(formula.getChild()); + LTLNode_p child = intermediateResult; + + //As ltl2dstar does not support bounded eventually, we transform it to (phi || X (phi || X ( ... ) ) ) + for (uint_fast64_t i = 0; i < formula.getBound(); i++) { + LTLNode_p nextOp(new LTLNode(LTLNode::T_NEXTSTEP, intermediateResult)); + intermediateResult.reset(new LTLNode(LTLNode::T_OR, child, nextOp)); + } + //TODO: Check if this works, even though the object child is never cloned, but referenced several time in the tree... + } + + /*! + * Visit method for an ltl Bounded Until formula. + * Stores the converted formula (in LTL2Dstar classes) in the field intermediateResult + * + * As Bounded Eventually is not supported in LTL2Dstar, the formula is unfolded into an equivalent + * formula using nested Next operators. + * + * @param formula Reference to the Bounded Until formula that is to be visited. + */ + virtual void visitBoundedUntil(const storm::property::ltl::BoundedUntil& formula) { + this->visit(formula.getLeft()); + LTLNode_p left = intermediateResult; + this->visit(formula.getRight()); + LTLNode_p right = intermediateResult; + + //As ltl2dstar does not support bounded until, we transform it to (phi || psi && X (phi || X ( ... ) ) ) + for (uint_fast64_t i = 0; i < formula.getBound(); i++) { + LTLNode_p nextOp(new LTLNode(LTLNode::T_NEXTSTEP, intermediateResult)); + LTLNode_p andOp(new LTLNode(LTLNode::T_AND, left, nextOp)); + intermediateResult.reset(new LTLNode(LTLNode::T_OR, right, andOp)); + } + //TODO: Check if this works, even though the objects left and right are never cloned, + //but referenced several time in the tree... + } + + /*! + * Visit method for an ltl Eventually formula. + * Stores the converted formula (in LTL2Dstar classes) in the field intermediateResult + * + * In LTL2DStar, the type for this formula is called "Finally". + * + * @param formula Reference to the Eventually formula that is to be visited. + */ + virtual void visitEventually(const storm::property::ltl::Eventually& formula) { + this->visit(formula.getChild()); + LTLNode_p child = intermediateResult; + intermediateResult.reset(new LTLNode(LTLNode::T_FINALLY, child)); + } + + /*! + * Visit method for an ltl Globally formula. + * Stores the converted formula (in LTL2Dstar classes) in the field intermediateResult + * + * @param formula Reference to the Globally formula that is to be visited. + */ + virtual void visitGlobally(const storm::property::ltl::Globally& formula) { + this->visit(formula.getChild()); + LTLNode_p child = intermediateResult; + intermediateResult.reset(new LTLNode(LTLNode::T_GLOBALLY, child)); + } + + /*! + * Visit method for an ltl Next formula. + * Stores the converted formula (in LTL2Dstar classes) in the field intermediateResult + * + * @param formula Reference to the Next formula that is to be visited. + */ + virtual void visitNext(const storm::property::ltl::Next& formula) { + this->visit(formula.getChild()); + LTLNode_p child = intermediateResult; + intermediateResult.reset(new LTLNode(LTLNode::T_NEXTSTEP, child)); + } + + /*! + * Visit method for an ltl Not formula. + * Stores the converted formula (in LTL2Dstar classes) in the field intermediateResult + * + * @param formula Reference to the Not formula that is to be visited. + */ + virtual void visitNot(const storm::property::ltl::Not& formula) { + this->visit(formula.getChild()); + LTLNode_p child = intermediateResult; + intermediateResult.reset(new LTLNode(LTLNode::T_NOT, child)); + } + + /*! + * Visit method for an ltl Or formula. + * Stores the converted formula (in LTL2Dstar classes) in the field intermediateResult + * + * @param formula Reference to the Or formula that is to be visited. + */ + virtual void visitOr(const storm::property::ltl::Or& formula) { + this->visit(formula.getLeft()); + LTLNode_p left = intermediateResult; + this->visit(formula.getRight()); + LTLNode_p right = intermediateResult; + intermediateResult.reset(new LTLNode(LTLNode::T_OR, left, right)); + } + + /*! + * Visit method for an ltl Until formula. + * Stores the converted formula (in LTL2Dstar classes) in the field intermediateResult + * + * @param formula Reference to the Until formula that is to be visited. + */ + virtual void visitUntil(const storm::property::ltl::Until& formula) { + this->visit(formula.getLeft()); + LTLNode_p left = intermediateResult; + this->visit(formula.getRight()); + LTLNode_p right = intermediateResult; + intermediateResult.reset(new LTLNode(LTLNode::T_UNTIL, left, right)); + } + + /*! + * @brief + * Start the conversion of the formula tree + * + * As LTL2DStar uses the shared pointers of the boost library, the converted object is stored in these. + * + * @param formula The LTL formula to be converted + * @return A boost shared pointer to the converted formula. + */ + LTLNode_p convertToLtlNode_p(storm::property::ltl::AbstractLtlFormula const& formula) { + this->visit(formula); + return intermediateResult; + } + + /*! + * Returns an APSet object which contains all atomic propositions of the labeling parameter + * @param labeling The labeling of which the APs are extracted + * @return + */ + static APSet_cp extractAPSetFromLabeling(storm::models::AtomicPropositionsLabeling const& labeling) { + //TODO: Make sure that the index of the AP is the same in the labeling and the APSet. + APSet* apset = new APSet(); + + //Insert each AP of the labeling into the APSet + for (auto it = labeling.getNameToLabelingMap().begin(); + it != labeling.getNameToLabelingMap().end(); + it++) { + apset->addAP(it->first); + } + + //Insert our object into the shared pointer + return APSet_cp(apset); + } + + /*! + * Convert an LTL formula using the storm data structures into an equivalent one for LTL2Dstar. + * + * @note + * Storm allows bounded until and eventually operators, which are not available in LTL2Dstar + * These formulas are unfolded into an equivalent formula using nested next operators. + * + * @param formula The formula object to convert + * @param labeling A labeling that contains (at least) each AP that is used in the formula + * @return + */ + static LTLFormula convert(storm::property::ltl::AbstractLtlFormula const& formula, + storm::models::AtomicPropositionsLabeling const& labeling) { + //First an APSet is extracted out of the labeling + APSet_cp apset = extractAPSetFromLabeling(labeling); + + //The visitor has to be an actual object, which is created here + Ltl2dstarFormulaAdapter adapter(apset); + + //The return value is the result of the visitor object + return LTLFormula(adapter.convertToLtlNode_p(formula), apset); + } + +protected: + /*! + * Constructor is protected, as the object should only be created in the static convert method. + * + * @param apset A set of atomic propositions (of LTL2Dstar) + */ + Ltl2dstarFormulaAdapter(APSet_cp apset) : + apset(apset) { + //Intentionally left empty + } + +private: + /*! + * Used to store the intermediate results of the conversion routine + */ + LTLNode_p intermediateResult; + + /*! + * Stores the apset information... + */ + APSet_cp apset; + + + +}; + +} /* namespace adapters */ +} /* namespace storm */ + +#endif /* STORM_ADAPTER_LTL2DSTARFORMULAADAPTER_H_ */ diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index 81d8ff504..07deef78b 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -161,6 +161,20 @@ public: return apCountMax; } + /*! + * Returns the number of atomic propositions managed by this object (set in the initialization). + * + * @return The number of atomic propositions. + */ + uint_fast64_t getIndexOfProposition(std::string const& ap) const { + if (!this->containsAtomicProposition(ap)) { + LOG4CPLUS_ERROR(logger, "The atomic proposition " << ap << " is invalid for the labeling of the model."); + throw storm::exceptions::InvalidArgumentException() << "The atomic proposition " << ap << " is invalid for the labeling of the model."; + } + auto apIndexPair = nameToLabelingMap.find(ap); + return apIndexPair->second; + } + /*! * Returns the labeling of states associated with the given atomic proposition. * @@ -201,6 +215,11 @@ public: } } + std::unordered_map const& getNameToLabelingMap() const + { + return this->nameToLabelingMap; + } + private: /*! The number of states whose labels are to be stored by this object. */ diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp index 8538c8d3f..8c0457310 100644 --- a/src/parser/CslParser.cpp +++ b/src/parser/CslParser.cpp @@ -92,7 +92,7 @@ struct CslParser::CslGrammar : qi::grammar> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)[qi::_val = @@ -106,6 +106,9 @@ struct CslParser::CslGrammar : qi::grammar stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; eventually.name("path formula (for probabilistic operator)"); + next = (qi::lit("X") > stateFormula)[qi::_val = + phoenix::new_ >(qi::_1)]; + next.name("path formula (for probabilistic operator)"); globally = (qi::lit("G") > stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; globally.name("path formula (for probabilistic operator)"); @@ -152,6 +155,7 @@ struct CslParser::CslGrammar : qi::grammar*(), Skipper> pathFormula; qi::rule*(), Skipper> timeBoundedEventually; qi::rule*(), Skipper> eventually; + qi::rule*(), Skipper> next; qi::rule*(), Skipper> globally; qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> timeBoundedUntil; qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> until; diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp index 6060adedc..3d53e5368 100644 --- a/src/parser/LtlParser.cpp +++ b/src/parser/LtlParser.cpp @@ -75,7 +75,7 @@ struct LtlParser::LtlGrammar : qi::grammar> qi::lit("<=") > qi::int_ > ltlFormula)[qi::_val = phoenix::new_>(qi::_2, qi::_1)]; @@ -86,6 +86,9 @@ struct LtlParser::LtlGrammar : qi::grammar> ltlFormula)[qi::_val = phoenix::new_ >(qi::_1)]; globally.name("LTL formula"); + next = (qi::lit("X") >> ltlFormula)[qi::_val = + phoenix::new_ >(qi::_1)]; + next.name("LTL formula"); start = (((ltlFormula) > (comment | qi::eps))[qi::_val = qi::_1] | comment @@ -113,6 +116,7 @@ struct LtlParser::LtlGrammar : qi::grammar*(), Skipper> boundedEventually; qi::rule*(), Skipper> eventually; qi::rule*(), Skipper> globally; + qi::rule*(), Skipper> next; qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> boundedUntil; qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> until; diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 88098561d..6f7cdf562 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -110,7 +110,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val = phoenix::new_>(qi::_2, qi::_1)]; @@ -118,6 +118,9 @@ struct PrctlParser::PrctlGrammar : qi::grammar stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; eventually.name("path formula (for probabilistic operator)"); + next = (qi::lit("X") > stateFormula)[qi::_val = + phoenix::new_ >(qi::_1)]; + next.name("path formula (for probabilistic operator)"); globally = (qi::lit("G") > stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; globally.name("path formula (for probabilistic operator)"); @@ -172,6 +175,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper> pathFormula; qi::rule*(), Skipper> boundedEventually; qi::rule*(), Skipper> eventually; + qi::rule*(), Skipper> next; qi::rule*(), Skipper> globally; qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> boundedUntil; qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> until; diff --git a/test/functional/ltl2dstarIntegration/Ltl2dstarFormulaAdapterTest.cpp b/test/functional/ltl2dstarIntegration/Ltl2dstarFormulaAdapterTest.cpp new file mode 100644 index 000000000..a12aca14a --- /dev/null +++ b/test/functional/ltl2dstarIntegration/Ltl2dstarFormulaAdapterTest.cpp @@ -0,0 +1,68 @@ +/* + * Ltl2dstarFormulaAdapterTest.cpp + * + * Created on: 01.06.2013 + * Author: thomas + */ + + + +#include "gtest/gtest.h" + +#include "src/formula/Ltl.h" +#include "src/adapters/Ltl2dstarFormulaAdapter.h" +#include "src/parser/LtlParser.h" + +TEST(Ltl2dstarFormulaAdapterTest, ConvertAndFormulaTest) { + storm::parser::LtlParser parser ("a & 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) && (b)"); + + delete parser.getFormula(); +} + +TEST(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) { + 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) { + 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(); +}