From 6ff25321d42be3e4438ada7515719fb40e162c43 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 9 Apr 2013 11:09:14 +0200 Subject: [PATCH] First version of CSL parser TODO: - Correct path formulas - Time bounded until - Steady state operator without bounds --- src/formula/Formulas.h | 2 +- ...eOperator.h => SteadyStateBoundOperator.h} | 18 +- src/parser/CslParser.cpp | 183 ++++++++++++++++++ src/parser/CslParser.h | 53 +++++ 4 files changed, 246 insertions(+), 10 deletions(-) rename src/formula/{SteadyStateOperator.h => SteadyStateBoundOperator.h} (82%) create mode 100644 src/parser/CslParser.cpp create mode 100644 src/parser/CslParser.h diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index 4ad64b1e7..89e3da422 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -32,7 +32,7 @@ #include "RewardNoBoundOperator.h" #include "SteadyStateReward.h" -#include "SteadyStateOperator.h" +#include "SteadyStateBoundOperator.h" #include "AbstractFormula.h" #include "AbstractPathFormula.h" diff --git a/src/formula/SteadyStateOperator.h b/src/formula/SteadyStateBoundOperator.h similarity index 82% rename from src/formula/SteadyStateOperator.h rename to src/formula/SteadyStateBoundOperator.h index 402a33c01..a341e316e 100644 --- a/src/formula/SteadyStateOperator.h +++ b/src/formula/SteadyStateBoundOperator.h @@ -17,7 +17,7 @@ namespace storm { namespace formula { -template class SteadyStateOperator; +template class SteadyStateBoundOperator; /*! * @brief Interface class for model checkers that support SteadyStateOperator. @@ -26,7 +26,7 @@ template class SteadyStateOperator; * this pure virtual class. */ template -class ISteadyStateOperatorModelChecker { +class ISteadyStateBoundOperatorModelChecker { public: /*! * @brief Evaluates SteadyStateOperator formula within a model checker. @@ -34,12 +34,12 @@ class ISteadyStateOperatorModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual storm::storage::BitVector* checkSteadyStateOperator(const SteadyStateOperator& obj) const = 0; + virtual storm::storage::BitVector* checkSteadyStateBoundOperator(const SteadyStateBoundOperator& obj) const = 0; }; /*! * @brief - * Class for a Abstract (path) formula tree with a SteadyStateOperator node as root. + * Class for an Abstract (path) formula tree with a SteadyStateOperator node as root. * * Has two Abstract state formulas as sub formulas/trees. * @@ -53,13 +53,13 @@ class ISteadyStateOperatorModelChecker { * @see AbstractFormula */ template -class SteadyStateOperator : public StateBoundOperator { +class SteadyStateBoundOperator : public StateBoundOperator { public: /*! * Empty constructor */ - SteadyStateOperator() : StateBoundOperator + SteadyStateBoundOperator() : StateBoundOperator (StateBoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { // Intentionally left empty } @@ -69,7 +69,7 @@ public: * * @param stateFormula The child node */ - SteadyStateOperator( + SteadyStateBoundOperator( typename StateBoundOperator::ComparisonType comparisonRelation, T bound, AbstractStateFormula* stateFormula) : StateBoundOperator(comparisonRelation, bound, stateFormula) { } @@ -93,7 +93,7 @@ public: * @returns a new BoundedUntil-object that is identical the called object. */ virtual AbstractStateFormula* clone() const { - SteadyStateOperator* result = new SteadyStateOperator(); + SteadyStateBoundOperator* result = new SteadyStateBoundOperator(); result->setStateFormula(this->getStateFormula().clone()); return result; } @@ -108,7 +108,7 @@ public: * @returns A vector indicating the probability that the formula holds for each state. */ virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { - return modelChecker.template as()->checkSteadyStateOperator(*this); + return modelChecker.template as()->checkSteadyStateOperator(*this); } }; diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp new file mode 100644 index 000000000..3a6c3d5d7 --- /dev/null +++ b/src/parser/CslParser.cpp @@ -0,0 +1,183 @@ +/* + * CslParser.cpp + * + * Created on: 08.04.2013 + * Author: Thomas Heinemann + */ + +#include "src/parser/PrctlParser.h" +#include "src/utility/OsDetection.h" +#include "src/utility/ConstTemplates.h" + +// If the parser fails due to ill-formed data, this exception is thrown. +#include "src/exceptions/WrongFormatException.h" + +// Used for Boost spirit. +#include +#include +#include + +// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. +#include +#include + +// Needed for file IO. +#include +#include +#include + + +// Some typedefs and namespace definitions to reduce code size. +typedef std::string::const_iterator BaseIteratorType; +typedef boost::spirit::classic::position_iterator2 PositionIteratorType; +namespace qi = boost::spirit::qi; +namespace phoenix = boost::phoenix; + +#include "CslParser.h" + + +namespace storm { +namespace parser { + +template +struct CslParser::CslGrammar : qi::grammar*(), Skipper > { + CslGrammar() : CslGrammar::base_type(start) { + freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; + + //This block defines rules for parsing state formulas + stateFormula %= orFormula; + stateFormula.name("state formula"); + orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val = + phoenix::new_>(qi::_val, qi::_1)]; + orFormula.name("state formula"); + andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val = + phoenix::new_>(qi::_val, qi::_1)]; + andFormula.name("state formula"); + notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val = + phoenix::new_>(qi::_1)]; + notFormula.name("state formula"); + + //This block defines rules for "atomic" state formulas + //(Propositions, probabilistic/reward formulas, and state formulas in brackets) + atomicStateFormula %= probabilisticBoundOperator | steadyStateBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")"); + atomicStateFormula.name("state formula"); + atomicProposition = (freeIdentifierName)[qi::_val = + phoenix::new_>(qi::_1)]; + atomicProposition.name("state formula"); + probabilisticBoundOperator = ( + (qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::PathBoundOperator::GREATER, qi::_1, qi::_2)] | + (qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::PathBoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | + (qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::PathBoundOperator::LESS, qi::_1, qi::_2)] | + (qi::lit("P") > qi::lit("<=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::PathBoundOperator::LESS_EQUAL, qi::_1, qi::_2)] + ); + probabilisticBoundOperator.name("state formula"); + steadyStateBoundOperator = ( + (qi::lit("S") >> qi::lit(">") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::PathBoundOperator::GREATER, qi::_1, qi::_2)] | + (qi::lit("S") >> qi::lit(">=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::PathBoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | + (qi::lit("S") >> qi::lit("<") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::PathBoundOperator::LESS, qi::_1, qi::_2)] | + (qi::lit("S") > qi::lit("<=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::PathBoundOperator::LESS_EQUAL, qi::_1, qi::_2)] + ); + steadyStateBoundOperator.name("state formula"); + + //This block defines rules for parsing formulas with noBoundOperators + noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator); + noBoundOperator.name("no bound operator"); + probabilisticNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1)]; + probabilisticNoBoundOperator.name("no bound operator"); + rewardNoBoundOperator = (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1)]; + rewardNoBoundOperator.name("no bound operator"); + + //This block defines rules for parsing probabilistic path formulas + pathFormula = (boundedEventually | eventually | globally | boundedUntil | until); + pathFormula.name("path formula"); + boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val = + phoenix::new_>(qi::_2, qi::_1)]; + boundedEventually.name("path formula (for probablistic operator)"); + eventually = (qi::lit("F") > stateFormula)[qi::_val = + phoenix::new_ >(qi::_1)]; + eventually.name("path formula (for probablistic operator)"); + globally = (qi::lit("G") > stateFormula)[qi::_val = + phoenix::new_ >(qi::_1)]; + globally.name("path formula (for probablistic operator)"); + boundedUntil = (stateFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula) + [qi::_val = phoenix::new_>(phoenix::bind(&storm::formula::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_3, qi::_2)]; + boundedUntil.name("path formula (for probablistic operator)"); + until = (stateFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val = + phoenix::new_>(phoenix::bind(&storm::formula::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_2)]; + until.name("path formula (for probablistic operator)"); + + //This block defines rules for parsing reward path formulas + rewardPathFormula = (cumulativeReward | reachabilityReward | instantaneousReward | steadyStateReward); + rewardPathFormula.name("path formula (for reward operator)"); + cumulativeReward = (qi::lit("C") > qi::lit("<=") > qi::double_) + [qi::_val = phoenix::new_>(qi::_1)]; + cumulativeReward.name("path formula (for reward operator)"); + reachabilityReward = (qi::lit("F") > stateFormula)[qi::_val = + phoenix::new_>(qi::_1)]; + reachabilityReward.name("path formula (for reward operator)"); + instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::double_) + [qi::_val = phoenix::new_>(qi::_1)]; + instantaneousReward.name("path formula (for reward operator)"); + steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_>()]; + + + start = (noBoundOperator | stateFormula); + start.name("PRCTL formula"); + } + + qi::rule*(), Skipper> start; + + qi::rule*(), Skipper> stateFormula; + qi::rule*(), Skipper> atomicStateFormula; + + qi::rule*(), Skipper> andFormula; + qi::rule*(), Skipper> atomicProposition; + qi::rule*(), Skipper> orFormula; + qi::rule*(), Skipper> notFormula; + qi::rule*(), Skipper> probabilisticBoundOperator; + qi::rule*(), Skipper> steadyStateBoundOperator; + qi::rule*(), Skipper> rewardBoundOperator; + + qi::rule*(), Skipper> noBoundOperator; + qi::rule*(), Skipper> probabilisticNoBoundOperator; + qi::rule*(), Skipper> rewardNoBoundOperator; + + qi::rule*(), Skipper> pathFormula; + qi::rule*(), Skipper> boundedEventually; + qi::rule*(), Skipper> eventually; + qi::rule*(), Skipper> globally; + qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> boundedUntil; + qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> until; + + qi::rule*(), Skipper> rewardPathFormula; + qi::rule*(), Skipper> cumulativeReward; + qi::rule*(), Skipper> reachabilityReward; + qi::rule*(), Skipper> instantaneousReward; + qi::rule*(), Skipper> steadyStateReward; + + + qi::rule freeIdentifierName; + +}; + +CslParser::CslParser(std::string formulaString) { + // TODO Auto-generated constructor stub + +} + +CslParser::~CslParser() { + // TODO Auto-generated destructor stub +} + +} /* namespace parser */ +} /* namespace storm */ diff --git a/src/parser/CslParser.h b/src/parser/CslParser.h new file mode 100644 index 000000000..d5c08dfa0 --- /dev/null +++ b/src/parser/CslParser.h @@ -0,0 +1,53 @@ +/* + * CslParser.h + * + * Created on: 08.04.2013 + * Author: Thomas Heinemann + */ + +#ifndef STORM_PARSER_CSLPARSER_H_ +#define STORM_PARSER_CSLPARSER_H_ + +#include "Parser.h" + +#include "src/formula/Formulas.h" +//#include + +namespace storm { +namespace parser { + +class CslParser: public storm::parser::Parser { +public: + /*! + * Reads a CSL formula from its string representation and parses it into a formula tree, consisting of + * classes in the namespace storm::formula. + * + * If the string could not be parsed successfully, it will throw a wrongFormatException. + * + * @param formulaString The string representation of the formula + * @throw wrongFormatException If the input could not be parsed successfully + */ + CslParser(std::string formulaString); + virtual ~CslParser(); + + /*! + * @return a pointer to the parsed formula object + */ + storm::formula::AbstractFormula* getFormula() { + return this->formula; + } + +private: +private: + storm::formula::AbstractFormula* formula; + + /*! + * Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas. + */ + template + struct CslGrammar; +}; + +} /* namespace parser */ +} /* namespace storm */ +#endif /* STORM_PARSER_CSLPARSER_H_ */