From 509c1a2b4782babd3bff8099c8f79e5801c4bd17 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 9 Apr 2013 15:25:16 +0200 Subject: [PATCH] Added support for SteadyStateNoBoundOperator into the CSL parser. --- src/formula/StateNoBoundOperator.h | 6 ++--- src/formula/SteadyStateNoBoundOperator.h | 7 +++--- src/parser/CslParser.cpp | 29 ++++++------------------ 3 files changed, 14 insertions(+), 28 deletions(-) diff --git a/src/formula/StateNoBoundOperator.h b/src/formula/StateNoBoundOperator.h index 853e1e0d3..c58e76b13 100644 --- a/src/formula/StateNoBoundOperator.h +++ b/src/formula/StateNoBoundOperator.h @@ -2,7 +2,7 @@ * StateNoBoundOperator.h * * Created on: 09.04.2013 - * Author: thomas + * Author: Thomas Heinemann */ #ifndef STATENOBOUNDOPERATOR_H_ @@ -95,8 +95,8 @@ public: } } - const AbstractStateFormula& getStateFormula() { - return *stateFormula; + const AbstractStateFormula& getStateFormula() const { + return *(this->stateFormula); } void setStateFormula(AbstractStateFormula* stateFormula) { diff --git a/src/formula/SteadyStateNoBoundOperator.h b/src/formula/SteadyStateNoBoundOperator.h index 2297ebfcd..7344e2a5a 100644 --- a/src/formula/SteadyStateNoBoundOperator.h +++ b/src/formula/SteadyStateNoBoundOperator.h @@ -30,7 +30,7 @@ class ISteadyStateNoBoundOperatorModelChecker { * @param obj Formula object with subformulas. * @return Result of the formula for every node. */ - virtual storm::storage::BitVector* checkSteadyStateNoBoundOperator(const SteadyStateNoBoundOperator& obj) const = 0; + virtual std::vector* checkSteadyStateNoBoundOperator(const SteadyStateNoBoundOperator& obj) const = 0; }; template @@ -71,11 +71,12 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ + /* TODO: Add clone method to StateNoBoundOperator and use matching return type virtual AbstractStateFormula* clone() const { SteadyStateNoBoundOperator* result = new SteadyStateNoBoundOperator(); result->setStateFormula(this->getStateFormula().clone()); return result; - } + }*/ /*! * Calls the model checker to check this formula. @@ -86,7 +87,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 { + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkSteadyStateNoBoundOperator(*this); } diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp index cd7efc53d..02edb2743 100644 --- a/src/parser/CslParser.cpp +++ b/src/parser/CslParser.cpp @@ -88,14 +88,14 @@ struct CslParser::CslGrammar : qi::grammar> 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"); + steadyStateNoBoundOperator = (qi::lit("S") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> stateFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1)]; + steadyStateNoBoundOperator.name("no bound operator"); //This block defines rules for parsing probabilistic path formulas pathFormula = (boundedEventually | eventually | globally | boundedUntil | until); @@ -116,23 +116,8 @@ struct CslParser::CslGrammar : qi::grammar>(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"); + start.name("CSL formula"); } qi::rule*(), Skipper> start; @@ -148,9 +133,9 @@ struct CslParser::CslGrammar : qi::grammar*(), Skipper> steadyStateBoundOperator; qi::rule*(), Skipper> rewardBoundOperator; - qi::rule*(), Skipper> noBoundOperator; + qi::rule*(), Skipper> noBoundOperator; qi::rule*(), Skipper> probabilisticNoBoundOperator; - qi::rule*(), Skipper> rewardNoBoundOperator; + qi::rule*(), Skipper> steadyStateNoBoundOperator; qi::rule*(), Skipper> pathFormula; qi::rule*(), Skipper> boundedEventually;