Conversion adapter to create LTL2DStar formulas out of "ours"

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 T>
+class Ltl2dstarFormulaAdapter :
+		public storm::property::ltl::visitor::AbstractLtlFormulaVisitor<T>,
+		public storm::property::ltl::IAndVisitor<T>,
+		public storm::property::ltl::IApVisitor<T>,
+		public storm::property::ltl::IBoundedEventuallyVisitor<T>,
+		public storm::property::ltl::IBoundedUntilVisitor<T>,
+		public storm::property::ltl::IEventuallyVisitor<T>,
+		public storm::property::ltl::IGloballyVisitor<T>,
+		public storm::property::ltl::INextVisitor<T>,
+		public storm::property::ltl::INotVisitor<T>,
+		public storm::property::ltl::IOrVisitor<T>,
+		public storm::property::ltl::IUntilVisitor<T> {
+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<T>& 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<T>& 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<T>& 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<T>& 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<T>& 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<T>& 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<T>& 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<T>& 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<T>& 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<T>& 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<T> 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<T> 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_ */

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<std::string, uint_fast64_t> const& getNameToLabelingMap() const
+			{
+		return this->nameToLabelingMap;
+	}
+
 private:
 
 	/*! The number of states whose labels are to be stored by this object. */

src/parser/CslParser.cpp

@@ -92,7 +92,7 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::Abstr
 		steadyStateNoBoundOperator.name("no bound operator");
 
 		//This block defines rules for parsing probabilistic path formulas
-		pathFormula = (timeBoundedEventually | eventually | globally | timeBoundedUntil | until);
+		pathFormula = (timeBoundedEventually | eventually | globally | next | timeBoundedUntil | until);
 		pathFormula.name("path formula");
 		timeBoundedEventually = (
 				(qi::lit("F") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)[qi::_val =
@@ -106,6 +106,9 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::Abstr
 		eventually = (qi::lit("F") > stateFormula)[qi::_val =
 				phoenix::new_<storm::property::csl::Eventually<double> >(qi::_1)];
 		eventually.name("path formula (for probabilistic operator)");
+		next = (qi::lit("X") > stateFormula)[qi::_val =
+				phoenix::new_<storm::property::csl::Next<double> >(qi::_1)];
+		next.name("path formula (for probabilistic operator)");
 		globally = (qi::lit("G") > stateFormula)[qi::_val =
 				phoenix::new_<storm::property::csl::Globally<double> >(qi::_1)];
 		globally.name("path formula (for probabilistic operator)");
@@ -152,6 +155,7 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::Abstr
 	qi::rule<Iterator, storm::property::csl::AbstractPathFormula<double>*(), Skipper> pathFormula;
 	qi::rule<Iterator, storm::property::csl::TimeBoundedEventually<double>*(), Skipper> timeBoundedEventually;
 	qi::rule<Iterator, storm::property::csl::Eventually<double>*(), Skipper> eventually;
+	qi::rule<Iterator, storm::property::csl::Next<double>*(), Skipper> next;
 	qi::rule<Iterator, storm::property::csl::Globally<double>*(), Skipper> globally;
 	qi::rule<Iterator, storm::property::csl::TimeBoundedUntil<double>*(), qi::locals< std::shared_ptr<storm::property::csl::AbstractStateFormula<double>>>, Skipper> timeBoundedUntil;
 	qi::rule<Iterator, storm::property::csl::Until<double>*(), qi::locals< std::shared_ptr<storm::property::csl::AbstractStateFormula<double>>>, Skipper> until;

src/parser/LtlParser.cpp

@@ -75,7 +75,7 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::property::ltl::Abstr
 		atomicProposition.name("LTL formula");
 
 		//This block defines rules for parsing probabilistic path formulas
-		pathFormula = (boundedEventually | eventually | globally);
+		pathFormula = (boundedEventually | eventually | globally | next);
 		pathFormula.name("LTL formula");
 		boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > ltlFormula)[qi::_val =
 				phoenix::new_<storm::property::ltl::BoundedEventually<double>>(qi::_2, qi::_1)];
@@ -86,6 +86,9 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::property::ltl::Abstr
 		globally = (qi::lit("G") >> ltlFormula)[qi::_val =
 				phoenix::new_<storm::property::ltl::Globally<double> >(qi::_1)];
 		globally.name("LTL formula");
+		next = (qi::lit("X") >> ltlFormula)[qi::_val =
+				phoenix::new_<storm::property::ltl::Next<double> >(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<Iterator, storm::property::ltl::Abstr
 	qi::rule<Iterator, storm::property::ltl::BoundedEventually<double>*(), Skipper> boundedEventually;
 	qi::rule<Iterator, storm::property::ltl::Eventually<double>*(), Skipper> eventually;
 	qi::rule<Iterator, storm::property::ltl::Globally<double>*(), Skipper> globally;
+	qi::rule<Iterator, storm::property::ltl::Next<double>*(), Skipper> next;
 	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), qi::locals< std::shared_ptr<storm::property::ltl::AbstractLtlFormula<double>>>, Skipper> boundedUntil;
 	qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), qi::locals< std::shared_ptr<storm::property::ltl::AbstractLtlFormula<double>>>, Skipper> until;
 

src/parser/PrctlParser.cpp

@@ -110,7 +110,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 		rewardNoBoundOperator.name("no bound operator");
 
 		//This block defines rules for parsing probabilistic path formulas
-		pathFormula = (boundedEventually | eventually | globally | boundedUntil | until);
+		pathFormula = (boundedEventually | eventually | next | globally | boundedUntil | until);
 		pathFormula.name("path formula");
 		boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
 				phoenix::new_<storm::property::prctl::BoundedEventually<double>>(qi::_2, qi::_1)];
@@ -118,6 +118,9 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 		eventually = (qi::lit("F") > stateFormula)[qi::_val =
 				phoenix::new_<storm::property::prctl::Eventually<double> >(qi::_1)];
 		eventually.name("path formula (for probabilistic operator)");
+		next = (qi::lit("X") > stateFormula)[qi::_val =
+				phoenix::new_<storm::property::prctl::Next<double> >(qi::_1)];
+		next.name("path formula (for probabilistic operator)");
 		globally = (qi::lit("G") > stateFormula)[qi::_val =
 				phoenix::new_<storm::property::prctl::Globally<double> >(qi::_1)];
 		globally.name("path formula (for probabilistic operator)");
@@ -172,6 +175,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 	qi::rule<Iterator, storm::property::prctl::AbstractPathFormula<double>*(), Skipper> pathFormula;
 	qi::rule<Iterator, storm::property::prctl::BoundedEventually<double>*(), Skipper> boundedEventually;
 	qi::rule<Iterator, storm::property::prctl::Eventually<double>*(), Skipper> eventually;
+	qi::rule<Iterator, storm::property::prctl::Next<double>*(), Skipper> next;
 	qi::rule<Iterator, storm::property::prctl::Globally<double>*(), Skipper> globally;
 	qi::rule<Iterator, storm::property::prctl::BoundedUntil<double>*(), qi::locals< std::shared_ptr<storm::property::prctl::AbstractStateFormula<double>>>, Skipper> boundedUntil;
 	qi::rule<Iterator, storm::property::prctl::Until<double>*(), qi::locals< std::shared_ptr<storm::property::prctl::AbstractStateFormula<double>>>, Skipper> until;

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<double>::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<double>::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<double>::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<double>::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();
+}