From cc0c3276681fc23daba59f5e6fe215b26aa8ecb3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 8 Apr 2014 16:39:12 +0200 Subject: [PATCH] Removed superfluous grammars and started working on making one PRISM grammar to rule them all. Former-commit-id: 375acb4699e696cb4c88f48fcb53550ddddab680 --- src/parser/PrismParser.h | 60 ++--- src/parser/prismparser/BaseGrammar.h | 253 ------------------ .../prismparser/BooleanExpressionGrammar.cpp | 42 --- .../prismparser/BooleanExpressionGrammar.h | 54 ---- .../ConstBooleanExpressionGrammar.cpp | 38 --- .../ConstBooleanExpressionGrammar.h | 47 ---- .../ConstDoubleExpressionGrammar.cpp | 34 --- .../ConstDoubleExpressionGrammar.h | 41 --- .../ConstIntegerExpressionGrammar.cpp | 41 --- .../ConstIntegerExpressionGrammar.h | 42 --- src/parser/prismparser/IdentifierGrammars.cpp | 23 -- src/parser/prismparser/IdentifierGrammars.h | 42 --- src/parser/prismparser/Includes.h | 39 --- .../prismparser/IntegerExpressionGrammar.cpp | 42 --- .../prismparser/IntegerExpressionGrammar.h | 50 ---- src/parser/prismparser/PrismGrammar.h | 123 +++------ src/parser/prismparser/Tokens.h | 129 +++++---- src/parser/prismparser/VariableState.cpp | 191 ------------- src/parser/prismparser/VariableState.h | 207 -------------- src/storage/prism/Assignment.cpp | 4 +- src/storage/prism/Assignment.h | 19 +- src/storage/prism/BooleanVariable.cpp | 6 +- src/storage/prism/BooleanVariable.h | 26 +- src/storage/prism/Command.cpp | 6 +- src/storage/prism/Command.h | 18 +- src/storage/prism/IntegerVariable.cpp | 6 +- src/storage/prism/IntegerVariable.h | 20 +- src/storage/prism/LocatedInformation.cpp | 17 ++ src/storage/prism/LocatedInformation.h | 48 ++++ src/storage/prism/Module.cpp | 8 +- src/storage/prism/Module.h | 20 +- src/storage/prism/Program.cpp | 16 +- src/storage/prism/Program.h | 53 +++- src/storage/prism/RewardModel.cpp | 2 +- src/storage/prism/RewardModel.h | 14 +- src/storage/prism/StateReward.cpp | 2 +- src/storage/prism/StateReward.h | 15 +- src/storage/prism/TransitionReward.cpp | 2 +- src/storage/prism/TransitionReward.h | 15 +- src/storage/prism/Update.cpp | 12 +- src/storage/prism/Update.h | 21 +- src/storage/prism/Variable.cpp | 4 +- src/storage/prism/Variable.h | 11 +- 43 files changed, 384 insertions(+), 1479 deletions(-) delete mode 100644 src/parser/prismparser/BaseGrammar.h delete mode 100644 src/parser/prismparser/BooleanExpressionGrammar.cpp delete mode 100644 src/parser/prismparser/BooleanExpressionGrammar.h delete mode 100644 src/parser/prismparser/ConstBooleanExpressionGrammar.cpp delete mode 100644 src/parser/prismparser/ConstBooleanExpressionGrammar.h delete mode 100644 src/parser/prismparser/ConstDoubleExpressionGrammar.cpp delete mode 100644 src/parser/prismparser/ConstDoubleExpressionGrammar.h delete mode 100644 src/parser/prismparser/ConstIntegerExpressionGrammar.cpp delete mode 100644 src/parser/prismparser/ConstIntegerExpressionGrammar.h delete mode 100644 src/parser/prismparser/IdentifierGrammars.cpp delete mode 100644 src/parser/prismparser/IdentifierGrammars.h delete mode 100644 src/parser/prismparser/Includes.h delete mode 100644 src/parser/prismparser/IntegerExpressionGrammar.cpp delete mode 100644 src/parser/prismparser/IntegerExpressionGrammar.h delete mode 100644 src/parser/prismparser/VariableState.cpp delete mode 100644 src/parser/prismparser/VariableState.h create mode 100644 src/storage/prism/LocatedInformation.cpp create mode 100644 src/storage/prism/LocatedInformation.h diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index da8ad0941..49bdd20c5 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -1,49 +1,35 @@ -/* * PrismParser.h - * - * Created on: Jan 3, 2013 - * Author: Christian Dehnert - */ - #ifndef STORM_PARSER_PRISMPARSER_H_ #define STORM_PARSER_PRISMPARSER_H_ // All classes of the intermediate representation are used. -#include "src/ir/IR.h" +#include "src/storage/prism/Program.h" // Used for file input. #include -#include namespace storm { - -namespace parser { - -using namespace storm::ir; -using namespace storm::ir::expressions; - -/* - * This functions parse the format of the PRISM model checker into an intermediate representation. - */ - -/*! - * Parses the given file into the intermediate representation assuming it complies with the - * PRISM syntax. - * @param filename the name of the file to parse. - * @return a shared pointer to the intermediate representation of the PRISM file. - */ -storm::ir::Program PrismParserFromFile(std::string const& filename); - -/*! - * Parses the given input stream into the intermediate representation assuming it complies with - * the PRISM syntax. - * @param inputStream the input stream to parse. - * @param filename the name of the file the input stream belongs to. Used for diagnostics. - * @return a shared pointer to the intermediate representation of the PRISM file. - */ -storm::ir::Program PrismParser(std::istream& inputStream, std::string const& filename); - -} // namespace parser - + namespace parser { + using namespace storm::prism; + using namespace storm::expressions; + + /*! + * Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax. + * + * @param filename the name of the file to parse. + * @return The resulting PRISM program. + */ + storm::prism::Program PrismParserFromFile(std::string const& filename); + + /*! + * Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax. + * + * @param inputStream The input stream to parse. + * @param filename The name of the file the input stream belongs to. + * @return The resulting PRISM program. + */ + storm::prism::Program PrismParser(std::istream& inputStream, std::string const& filename); + + } // namespace parser } // namespace storm #endif /* STORM_PARSER_PRISMPARSER_H_ */ diff --git a/src/parser/prismparser/BaseGrammar.h b/src/parser/prismparser/BaseGrammar.h deleted file mode 100644 index 7cac493c3..000000000 --- a/src/parser/prismparser/BaseGrammar.h +++ /dev/null @@ -1,253 +0,0 @@ -/* - * File: Keywords.h - * Author: nafur - * - * Created on April 10, 2013, 6:03 PM - */ - -#ifndef BASEGRAMMAR_H -#define BASEGRAMMAR_H - -#include "Includes.h" - -#include "VariableState.h" - -namespace storm { -namespace parser { -namespace prism { - - /*! - * This is the base class for all expression grammars. - * It takes care of implementing a singleton, stores a VariableState and implements some common helper routines. - */ - template - class BaseGrammar { - public: - /*! - * Constructor. - */ - BaseGrammar(std::shared_ptr const& state) : state(state) {} - - /*! - * Create and return a new instance of class T, usually the subclass. - * @param state VariableState to be given to the constructor. - * @returns Instance of class T. - */ - static T& instance(std::shared_ptr const& state = nullptr) { - if (BaseGrammar::instanceObject == nullptr) { - BaseGrammar::instanceObject = std::shared_ptr(new T(state)); - if (!state->firstRun) BaseGrammar::instanceObject->secondRun(); - } - return *BaseGrammar::instanceObject; - } - - /*! - * Clear the cached instance. - */ - static void resetInstance() { - BaseGrammar::instanceObject = nullptr; - } - - /*! - * Notify the cached object, that we will begin with the second parsing run. - */ - static void secondRun() { - if (BaseGrammar::instanceObject != nullptr) { - BaseGrammar::instanceObject->prepareSecondRun(); - } - } - - /*! - * Create a new boolean literal with the given value. - * @param value Value of the literal. - * @returns Boolean literal. - */ - std::shared_ptr createBoolLiteral(bool value) { - return std::shared_ptr(new BooleanLiteralExpression(value)); - } - /*! - * Create a new double literal with the given value. - * @param value Value of the literal. - * @returns Double literal. - */ - std::shared_ptr createDoubleLiteral(double value) { - return std::shared_ptr(new DoubleLiteralExpression(value)); - } - /*! - * Create a new integer literal with the given value. - * @param value Value of the literal. - * @returns Integer literal. - */ - std::shared_ptr createIntLiteral(int_fast64_t value) { - return std::shared_ptr(new IntegerLiteralExpression(value)); - } - - /*! - * Create a new plus expression. If addition is true, it will be an addition, otherwise a subtraction. - * @param left Left operand. - * @param addition Flag for addition or subtraction. - * @param right Right operand. - * @param type Return type. - * @returns Plus expression. - */ - std::shared_ptr createPlus(std::shared_ptr const& left, bool addition, std::shared_ptr const& right, BaseExpression::ReturnType type) { - if (addition) { - return std::shared_ptr(new BinaryNumericalFunctionExpression(type, left->clone(), right->clone(), BinaryNumericalFunctionExpression::PLUS)); - } else { - return std::shared_ptr(new BinaryNumericalFunctionExpression(type, left->clone(), right->clone(), BinaryNumericalFunctionExpression::MINUS)); - } - } - /*! - * Create a new double plus expression. If addition is true, it will be an addition, otherwise a subtraction. - * @param left Left operand. - * @param addition Flag for addition or subtraction. - * @param right Right operand. - * @returns Double plus expression. - */ - std::shared_ptr createDoublePlus(std::shared_ptr const& left, bool addition, std::shared_ptr const& right) { - return this->createPlus(left, addition, right, BaseExpression::double_); - } - /*! - * Create a new integer plus expression. If addition is true, it will be an addition, otherwise a subtraction. - * @param left Left operand. - * @param addition Flag for addition or subtraction. - * @param right Right operand. - * @returns Integer plus expression. - */ - std::shared_ptr createIntPlus(std::shared_ptr const& left, bool addition, std::shared_ptr const& right) { - return this->createPlus(left, addition, right, BaseExpression::int_); - } - - /*! - * Create a new integer multiplication expression. - * @param left Left operand. - * @param right Right operand. - * @returns Integer multiplication expression. - */ - std::shared_ptr createIntMult(std::shared_ptr const& left, std::shared_ptr const& right) { - return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::int_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::TIMES)); - } - - /*! - * Create a new integer multiplication expression. If multiplication is true, it will be an multiplication, otherwise a division. - * @param left Left operand. - * @param addition Flag for multiplication or division. - * @param right Right operand. - * @returns Integer multiplication expression. - */ - std::shared_ptr createDoubleMult(std::shared_ptr const& left, bool multiplication, std::shared_ptr const& right) { - if (multiplication) { - return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::TIMES)); - } else { - return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::DIVIDE)); - } - } - - /*! - * Creates an integer min/max expression. - * - * @param min Indicates whether the expression is min or max. - * @param left The left operand. - * @param right The right operand. - * @return An integer min/max expression. - */ - std::shared_ptr createIntMinMax(bool min, std::shared_ptr const& left, std::shared_ptr const& right) { - if (min) { - return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::int_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::MIN)); - } else { - return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::int_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::MAX)); - } - } - - /*! - * Creates an integer floor/ceil expression. - * - * @param floor Indicates whether the expression is a floor expression. - * @param operand The argument of the floor/ceil operation. - * @return An integer floor/ceil expression. - */ - std::shared_ptr createIntFloorCeil(bool floor, std::shared_ptr const& operand) { - if (floor) { - return std::shared_ptr(new UnaryNumericalFunctionExpression(BaseExpression::int_, operand->clone(), UnaryNumericalFunctionExpression::FLOOR)); - } else { - return std::shared_ptr(new UnaryNumericalFunctionExpression(BaseExpression::int_, operand->clone(), UnaryNumericalFunctionExpression::CEIL)); - } - } - - /*! - * Create a new binary relation expression. - * @param left Left operand. - * @param relationType Type of binary relation. - * @param right Right operand. - * @returns Binary relation expression. - */ - std::shared_ptr createRelation(std::shared_ptr const& left, BinaryRelationExpression::RelationType relationType, std::shared_ptr const& right) { - return std::shared_ptr(new BinaryRelationExpression(left->clone(), right->clone(), relationType)); - } - /*! - * Create a new negation expression. - * @param child Expression to be negated. - * @returns Negation expression. - */ - std::shared_ptr createNot(std::shared_ptr const& child) { - return std::shared_ptr(new UnaryBooleanFunctionExpression(child->clone(), UnaryBooleanFunctionExpression::NOT)); - } - /*! - * Create a new And expression. - * @param left Left operand. - * @param right Right operand. - * @returns And expression. - */ - std::shared_ptr createAnd(std::shared_ptr const& left, std::shared_ptr const& right) { - return std::shared_ptr(new BinaryBooleanFunctionExpression(left->clone(), right->clone(), BinaryBooleanFunctionExpression::AND)); - } - /*! - * Create a new Or expression. - * @param left Left operand. - * @param right Right operand. - * @returns Or expression. - */ - std::shared_ptr createOr(std::shared_ptr const& left, std::shared_ptr const& right) { - return std::shared_ptr(new BinaryBooleanFunctionExpression(left->clone(), right->clone(), BinaryBooleanFunctionExpression::OR)); - } - /*! - * Retrieve boolean variable by name. - * @param name Variable name. - * @returns Boolean variable. - */ - std::shared_ptr getBoolVariable(std::string const& name) { - return std::shared_ptr(new VariableExpression(*state->getBooleanVariableExpression(name))); - } - /*! - * Retrieve integer variable by name. - * @param name Variable name. - * @returns Integer variable. - */ - std::shared_ptr getIntVariable(std::string const& name) { - return std::shared_ptr(new VariableExpression(*state->getIntegerVariableExpression(name))); - } - - /*! - * Base method to switch to second run. This does nothing. - * Any subclass that needs to do something in order to proceed to the second run should override this method. - */ - virtual void prepareSecondRun() {} - - protected: - /*! - * Pointer to variable state. - */ - std::shared_ptr state; - - private: - static std::shared_ptr instanceObject; - static bool inSecondRun; - }; - - template - std::shared_ptr BaseGrammar::instanceObject; -} -} -} -#endif /* BASEGRAMMAR_H */ - diff --git a/src/parser/prismparser/BooleanExpressionGrammar.cpp b/src/parser/prismparser/BooleanExpressionGrammar.cpp deleted file mode 100644 index a7d9366f8..000000000 --- a/src/parser/prismparser/BooleanExpressionGrammar.cpp +++ /dev/null @@ -1,42 +0,0 @@ -#include "BooleanExpressionGrammar.h" - -#include "IntegerExpressionGrammar.h" -#include "ConstBooleanExpressionGrammar.h" - -namespace storm { - namespace parser { - namespace prism { - - BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr const& state) - : BooleanExpressionGrammar::base_type(booleanExpression), BaseGrammar(state) { - - booleanExpression %= orExpression; - booleanExpression.name("boolean expression"); - - orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&BaseGrammar::createOr, this, qi::_val, qi::_1)]; - orExpression.name("boolean expression"); - - andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::bind(&BaseGrammar::createAnd, this, qi::_val, qi::_1)]; - andExpression.name("boolean expression"); - - notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)]; - notExpression.name("boolean expression"); - - atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | this->state->constantBooleanFormulas_ | this->state->booleanFormulas_ | qi::lit("(") >> booleanExpression >> qi::lit(")") | ConstBooleanExpressionGrammar::instance(this->state)); - atomicBooleanExpression.name("boolean expression"); - - relativeExpression = (IntegerExpressionGrammar::instance(this->state) >> relations_ >> IntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)]; - relativeExpression.name("relative expression"); - - booleanVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getBoolVariable, this, qi::_1)]; - booleanVariableExpression.name("boolean variable"); - } - - void BooleanExpressionGrammar::prepareSecondRun() { - booleanVariableExpression %= this->state->booleanVariables_; - booleanVariableExpression.name("boolean variable"); - } - - } // namespace prism - } // namespace parser -} // namespace storm diff --git a/src/parser/prismparser/BooleanExpressionGrammar.h b/src/parser/prismparser/BooleanExpressionGrammar.h deleted file mode 100644 index 909219fa3..000000000 --- a/src/parser/prismparser/BooleanExpressionGrammar.h +++ /dev/null @@ -1,54 +0,0 @@ -/* - * File: BooleanExpressionGrammar.h - * Author: nafur - * - * Created on April 10, 2013, 6:27 PM - */ - -#ifndef BOOLEANEXPRESSIONGRAMMAR_H -#define BOOLEANEXPRESSIONGRAMMAR_H - -#include "Includes.h" -#include "VariableState.h" -#include "IdentifierGrammars.h" -#include "Tokens.h" - -#include - -namespace storm { -namespace parser { -namespace prism { - -/*! - * This grammar parses (non constant) boolean expressions as used in prism models. - */ -class BooleanExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { -public: - BooleanExpressionGrammar(std::shared_ptr const& state); - /*! - * Switch to second run. - * Variable names may be any valid identifier in the first run, but only defined variables in the second run. - */ - virtual void prepareSecondRun(); - -private: - qi::rule(), Skipper, Unused> booleanExpression; - qi::rule(), Skipper> orExpression; - qi::rule(), Skipper> andExpression; - qi::rule(), Skipper> notExpression; - qi::rule(), Skipper> atomicBooleanExpression; - qi::rule(), Skipper> relativeExpression; - qi::rule(), Skipper> booleanVariableExpression; - - /*! - * Parser relation operators. - */ - storm::parser::prism::relationalOperatorStruct relations_; -}; - - -} -} -} - -#endif /* BOOLEANEXPRESSIONGRAMMAR_H */ diff --git a/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp b/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp deleted file mode 100644 index a5ce0567d..000000000 --- a/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp +++ /dev/null @@ -1,38 +0,0 @@ -#include "ConstBooleanExpressionGrammar.h" - -#include "ConstIntegerExpressionGrammar.h" - -namespace storm { -namespace parser { -namespace prism { - - ConstBooleanExpressionGrammar::ConstBooleanExpressionGrammar(std::shared_ptr const& state) - : ConstBooleanExpressionGrammar::base_type(constantBooleanExpression), BaseGrammar(state) { - - constantBooleanExpression %= constantOrExpression; - constantBooleanExpression.name("constant boolean expression"); - - constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::bind(&BaseGrammar::createOr, this, qi::_val, qi::_1)]; - constantOrExpression.name("constant boolean expression"); - - constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::bind(&BaseGrammar::createAnd, this, qi::_val, qi::_1)]; - constantAndExpression.name("constant boolean expression"); - - constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)]; - constantNotExpression.name("constant boolean expression"); - - constantAtomicBooleanExpression %= (constantRelativeExpression | this->state->constantBooleanFormulas_ | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); - constantAtomicBooleanExpression.name("constant boolean expression"); - - constantRelativeExpression = (ConstIntegerExpressionGrammar::instance(this->state) >> relations_ >> ConstIntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)]; - constantRelativeExpression.name("constant boolean expression"); - - booleanConstantExpression %= (this->state->booleanConstants_ | booleanLiteralExpression); - booleanConstantExpression.name("boolean constant or literal"); - - booleanLiteralExpression = qi::bool_[qi::_val = phoenix::bind(&BaseGrammar::createBoolLiteral, this, qi::_1)]; - booleanLiteralExpression.name("boolean literal"); - } -} -} -} diff --git a/src/parser/prismparser/ConstBooleanExpressionGrammar.h b/src/parser/prismparser/ConstBooleanExpressionGrammar.h deleted file mode 100644 index 8fea3ce95..000000000 --- a/src/parser/prismparser/ConstBooleanExpressionGrammar.h +++ /dev/null @@ -1,47 +0,0 @@ -/* - * File: ConstBooleanExpressionGrammar.h - * Author: nafur - * - * Created on April 10, 2013, 6:34 PM - */ - -#ifndef CONSTBOOLEANEXPRESSIONGRAMMAR_H -#define CONSTBOOLEANEXPRESSIONGRAMMAR_H - -#include "Includes.h" -#include "VariableState.h" -#include "IdentifierGrammars.h" -#include "Tokens.h" - -namespace storm { -namespace parser { -namespace prism { - -/*! - * This grammar parses constant boolean expression as used in prism models. - */ -class ConstBooleanExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { -public: - ConstBooleanExpressionGrammar(std::shared_ptr const& state); - - -private: - qi::rule(), Skipper, Unused> constantBooleanExpression; - qi::rule(), Skipper> constantOrExpression; - qi::rule(), Skipper> constantAndExpression; - qi::rule(), Skipper> constantNotExpression; - qi::rule(), Skipper> constantAtomicBooleanExpression; - qi::rule(), Skipper> constantRelativeExpression; - qi::rule(), Skipper> booleanConstantExpression; - qi::rule(), Skipper> booleanLiteralExpression; - - storm::parser::prism::relationalOperatorStruct relations_; -}; - - -} -} -} - -#endif /* CONSTBOOLEANEXPRESSIONGRAMMAR_H */ - diff --git a/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp b/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp deleted file mode 100644 index 18cd5ae31..000000000 --- a/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp +++ /dev/null @@ -1,34 +0,0 @@ -#include "ConstDoubleExpressionGrammar.h" - -namespace storm { -namespace parser { -namespace prism { - -ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr const& state) - : ConstDoubleExpressionGrammar::base_type(constantDoubleExpression), BaseGrammar(state) { - - constantDoubleExpression %= constantDoublePlusExpression; - constantDoubleExpression.name("constant double expression"); - - constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantDoubleMultExpression) - [qi::_val = phoenix::bind(&BaseGrammar::createDoublePlus, this, qi::_val, qi::_a, qi::_1)]; - constantDoublePlusExpression.name("constant double expression"); - - constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> constantAtomicDoubleExpression) - [qi::_val = phoenix::bind(&BaseGrammar::createDoubleMult, this, qi::_val, qi::_a, qi::_1)]; - constantDoubleMultExpression.name("constant double expression"); - - constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | this->state->constantDoubleFormulas_ | this->state->constantIntegerFormulas_ | doubleConstantExpression); - constantAtomicDoubleExpression.name("constant double expression"); - - doubleConstantExpression %= (this->state->doubleConstants_ | this->state->integerConstants_ | doubleLiteralExpression); - doubleConstantExpression.name("double constant or literal"); - - doubleLiteralExpression = qi::double_[qi::_val = phoenix::bind(&BaseGrammar::createDoubleLiteral, this, qi::_1)]; - doubleLiteralExpression.name("double literal"); -} - - -} -} -} diff --git a/src/parser/prismparser/ConstDoubleExpressionGrammar.h b/src/parser/prismparser/ConstDoubleExpressionGrammar.h deleted file mode 100644 index 41c503731..000000000 --- a/src/parser/prismparser/ConstDoubleExpressionGrammar.h +++ /dev/null @@ -1,41 +0,0 @@ -/* - * File: ConstDoubleExpressionGrammar.h - * Author: nafur - * - * Created on April 10, 2013, 7:04 PM - */ - -#ifndef CONSTDOUBLEEXPRESSIONGRAMMAR_H -#define CONSTDOUBLEEXPRESSIONGRAMMAR_H - -#include "Includes.h" -#include "VariableState.h" -#include "IdentifierGrammars.h" - -namespace storm { - namespace parser { - namespace prism { - - /*! - * This grammar parses constant double expressions as used in prism models. - */ - class ConstDoubleExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { - public: - ConstDoubleExpressionGrammar(std::shared_ptr const& state); - - private: - qi::rule(), Skipper, Unused> constantDoubleExpression; - qi::rule(), qi::locals, Skipper> constantDoublePlusExpression; - qi::rule(), qi::locals, Skipper> constantDoubleMultExpression; - qi::rule(), Skipper> constantAtomicDoubleExpression; - qi::rule(), Skipper> doubleConstantExpression; - qi::rule(), Skipper> doubleLiteralExpression; - }; - - - } - } -} - -#endif /* CONSTDOUBLEEXPRESSIONGRAMMAR_H */ - diff --git a/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp b/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp deleted file mode 100644 index 9ebebebc7..000000000 --- a/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp +++ /dev/null @@ -1,41 +0,0 @@ -#include "ConstIntegerExpressionGrammar.h" - -namespace storm { - namespace parser { - namespace prism { - - - ConstIntegerExpressionGrammar::ConstIntegerExpressionGrammar(std::shared_ptr const& state) - : ConstIntegerExpressionGrammar::base_type(constantIntegerExpression), BaseGrammar(state) { - - constantIntegerExpression %= constantIntegerPlusExpression; - constantIntegerExpression.name("constant integer expression"); - - constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression) - [qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)]; - constantIntegerPlusExpression.name("constant integer expression"); - - constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression) - [qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]; - constantIntegerMultExpression.name("constant integer expression"); - - constantAtomicIntegerExpression %= (constantIntegerMinMaxExpression | constantIntegerFloorCeilExpression | this->state->constantIntegerFormulas_ | qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); - constantAtomicIntegerExpression.name("constant integer expression"); - - constantIntegerMinMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> constantIntegerExpression >> qi::lit(",") >> constantIntegerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntMinMax, this, qi::_a, qi::_1, qi::_2)]; - constantIntegerMinMaxExpression.name("integer min/max expression"); - - constantIntegerFloorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> constantIntegerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntFloorCeil, this, qi::_a, qi::_1)]; - constantIntegerFloorCeilExpression.name("integer floor/ceil expression"); - - integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression); - integerConstantExpression.name("integer constant or literal"); - - integerLiteralExpression = qi::int_[qi::_val = phoenix::bind(&BaseGrammar::createIntLiteral, this, qi::_1)]; - integerLiteralExpression.name("integer literal"); - - } - - } // namespace prism - } // namespace parser -} // namespace storm diff --git a/src/parser/prismparser/ConstIntegerExpressionGrammar.h b/src/parser/prismparser/ConstIntegerExpressionGrammar.h deleted file mode 100644 index 2b6a08cae..000000000 --- a/src/parser/prismparser/ConstIntegerExpressionGrammar.h +++ /dev/null @@ -1,42 +0,0 @@ -/* - * File: ConstIntegerExpressionGrammar.h - * Author: nafur - * - * Created on April 10, 2013, 6:02 PM - */ - -#ifndef CONSTINTEGEREXPRESSIONGRAMMAR_H -#define CONSTINTEGEREXPRESSIONGRAMMAR_H - -#include "Includes.h" -#include "VariableState.h" -#include "IdentifierGrammars.h" - -namespace storm { - namespace parser { - namespace prism { - - /*! - * This grammar parses constant integer expressions as used in prism models. - */ - class ConstIntegerExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { - public: - ConstIntegerExpressionGrammar(std::shared_ptr const& state); - - private: - qi::rule(), Skipper, Unused> constantIntegerExpression; - qi::rule(), qi::locals, Skipper> constantIntegerPlusExpression; - qi::rule(), Skipper> constantIntegerMultExpression; - qi::rule(), Skipper> constantAtomicIntegerExpression; - qi::rule(), Skipper> integerConstantExpression; - qi::rule(), Skipper> integerLiteralExpression; - qi::rule(), qi::locals, Skipper> constantIntegerMinMaxExpression; - qi::rule(), qi::locals, Skipper> constantIntegerFloorCeilExpression; - }; - - - } - } -} - -#endif /* CONSTINTEGEREXPRESSIONGRAMMAR_H */ diff --git a/src/parser/prismparser/IdentifierGrammars.cpp b/src/parser/prismparser/IdentifierGrammars.cpp deleted file mode 100644 index ec6f14931..000000000 --- a/src/parser/prismparser/IdentifierGrammars.cpp +++ /dev/null @@ -1,23 +0,0 @@ -#include "IdentifierGrammars.h" - -namespace storm { - namespace parser { - namespace prism { - - IdentifierGrammar::IdentifierGrammar(std::shared_ptr const& state) - : IdentifierGrammar::base_type(identifierName), BaseGrammar(state) { - - identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isIdentifier, this->state.get(), qi::_1) ]; - identifierName.name("identifier"); - } - - FreeIdentifierGrammar::FreeIdentifierGrammar(std::shared_ptr const& state) - : FreeIdentifierGrammar::base_type(freeIdentifierName), BaseGrammar(state) { - - freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isFreeIdentifier, this->state.get(), qi::_1) ]; - freeIdentifierName.name("identifier"); - } - - } - } -} \ No newline at end of file diff --git a/src/parser/prismparser/IdentifierGrammars.h b/src/parser/prismparser/IdentifierGrammars.h deleted file mode 100644 index ccb14bbc1..000000000 --- a/src/parser/prismparser/IdentifierGrammars.h +++ /dev/null @@ -1,42 +0,0 @@ -/* - * File: Keywords.h - * Author: nafur - * - * Created on April 10, 2013, 6:03 PM - */ - -#ifndef IDENTIFIERGRAMMARS_H -#define IDENTIFIERGRAMMARS_H - -#include "Includes.h" -#include "BaseGrammar.h" -#include "VariableState.h" - -namespace storm { - namespace parser { - namespace prism { - - /*! - * This grammar parses a (possibly used) identifier as used in a prism models. - */ - class IdentifierGrammar : public qi::grammar, public BaseGrammar { - public: - IdentifierGrammar(std::shared_ptr const& state); - private: - qi::rule identifierName; - }; - - /*! - * This grammar parses an used identifier as used in a prism models. - */ - class FreeIdentifierGrammar : public qi::grammar, public BaseGrammar { - public: - FreeIdentifierGrammar(std::shared_ptr const& state); - private: - qi::rule freeIdentifierName; - }; - } - } -} -#endif /* IDENTIFIERGRAMMARS_H */ - diff --git a/src/parser/prismparser/Includes.h b/src/parser/prismparser/Includes.h deleted file mode 100644 index 49a720dad..000000000 --- a/src/parser/prismparser/Includes.h +++ /dev/null @@ -1,39 +0,0 @@ -/* - * File: Includes - * Author: Gereon Kremer - * - * Created on April 10, 2013, 4:46 PM - */ - -#ifndef BOOSTINCLUDES_H -#define BOOSTINCLUDES_H - -// Used for Boost spirit. -#include -#include -#include - -// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. -#include -#include - -namespace qi = boost::spirit::qi; -namespace phoenix = boost::phoenix; - -typedef std::string::const_iterator BaseIteratorType; -typedef boost::spirit::classic::position_iterator2 PositionIteratorType; -typedef PositionIteratorType Iterator; -typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper; -typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2; -typedef boost::spirit::unused_type Unused; - -#include "src/ir/IR.h" -using namespace storm::ir; -using namespace storm::ir::expressions; - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - -#endif /* BOOSTINCLUDES_H */ - diff --git a/src/parser/prismparser/IntegerExpressionGrammar.cpp b/src/parser/prismparser/IntegerExpressionGrammar.cpp deleted file mode 100644 index 3bcfd4d4f..000000000 --- a/src/parser/prismparser/IntegerExpressionGrammar.cpp +++ /dev/null @@ -1,42 +0,0 @@ -#include "IntegerExpressionGrammar.h" - -#include "IdentifierGrammars.h" -#include "ConstIntegerExpressionGrammar.h" - -namespace storm { - namespace parser { - namespace prism { - - IntegerExpressionGrammar::IntegerExpressionGrammar(std::shared_ptr const& state) - : IntegerExpressionGrammar::base_type(integerExpression), BaseGrammar(state) { - - integerExpression %= integerPlusExpression; - integerExpression.name("integer expression"); - - integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)]; - integerPlusExpression.name("integer expression"); - - integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]); - integerMultExpression.name("integer expression"); - - atomicIntegerExpression %= (integerMinMaxExpression | integerFloorCeilExpression | this->state->constantIntegerFormulas_ | this->state->integerFormulas_ | qi::lit("(") >> integerExpression >> qi::lit(")") | integerVariableExpression | ConstIntegerExpressionGrammar::instance(this->state)); - atomicIntegerExpression.name("integer expression"); - - integerMinMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> integerExpression >> qi::lit(",") >> integerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntMinMax, this, qi::_a, qi::_1, qi::_2)]; - integerMinMaxExpression.name("integer min/max expression"); - - integerFloorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> integerExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&BaseGrammar::createIntFloorCeil, this, qi::_a, qi::_1)]; - integerFloorCeilExpression.name("integer floor/ceil expression"); - - integerVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getIntVariable, this, qi::_1)]; - integerVariableExpression.name("integer variable"); - } - - void IntegerExpressionGrammar::prepareSecondRun() { - integerVariableExpression %= this->state->integerVariables_; - integerVariableExpression.name("integer variable"); - } - - } - } -} diff --git a/src/parser/prismparser/IntegerExpressionGrammar.h b/src/parser/prismparser/IntegerExpressionGrammar.h deleted file mode 100644 index 7531ef36e..000000000 --- a/src/parser/prismparser/IntegerExpressionGrammar.h +++ /dev/null @@ -1,50 +0,0 @@ -/* - * File: IntegerExpressionGrammar.h - * Author: nafur - * - * Created on April 10, 2013, 4:39 PM - */ - -#ifndef INTEGEREXPRESSIONGRAMMAR_H -#define INTEGEREXPRESSIONGRAMMAR_H - -#include "src/ir/IR.h" -#include "VariableState.h" -#include "Includes.h" -#include "IdentifierGrammars.h" - -#include - -namespace storm { - namespace parser { - namespace prism { - - /*! - * This grammar parses a (non constant) integer expressions as used in prism models. - */ - class IntegerExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { - public: - IntegerExpressionGrammar(std::shared_ptr const& state); - - /*! - * Switch to second run. - * Variable names may be any valid identifier in the first run, but only defined variables in the second run. - */ - virtual void prepareSecondRun(); - - private: - qi::rule(), Skipper, Unused> integerExpression; - qi::rule(), qi::locals, Skipper> integerPlusExpression; - qi::rule(), Skipper> integerMultExpression; - qi::rule(), Skipper> atomicIntegerExpression; - qi::rule(), Skipper> integerVariableExpression; - qi::rule(), qi::locals, Skipper> integerMinMaxExpression; - qi::rule(), qi::locals, Skipper> integerFloorCeilExpression; - }; - - } - } -} - -#endif /* INTEGEREXPRESSIONGRAMMAR_H */ - diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h index 57ba55c5b..c73420057 100644 --- a/src/parser/prismparser/PrismGrammar.h +++ b/src/parser/prismparser/PrismGrammar.h @@ -1,103 +1,61 @@ -/* - * File: PrismGrammar.h - * Author: nafur - * - * Created on April 30, 2013, 5:20 PM - */ +#ifndef STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H_ +#define STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H_ -#ifndef STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H -#define STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H +// Include files for file input. +#include +#include + +// Include boost spirit. +#include +#include +#include + +// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. +#include +#include + +namespace qi = boost::spirit::qi; +namespace phoenix = boost::phoenix; + +typedef std::string::const_iterator BaseIteratorType; +typedef boost::spirit::classic::position_iterator2 PositionIteratorType; +typedef PositionIteratorType Iterator; +typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper; +typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2; +typedef boost::spirit::unused_type Unused; -// All classes of the intermediate representation are used. -#include "src/ir/IR.h" -#include "src/parser/prismparser/Includes.h" #include "src/parser/prismparser/Tokens.h" -#include "src/parser/prismparser/IdentifierGrammars.h" -#include "src/parser/prismparser/VariableState.h" -#include "src/parser/prismparser/ConstBooleanExpressionGrammar.h" -#include "src/parser/prismparser/ConstDoubleExpressionGrammar.h" -#include "src/parser/prismparser/ConstIntegerExpressionGrammar.h" -#include "src/parser/prismparser/BooleanExpressionGrammar.h" -#include "src/parser/prismparser/IntegerExpressionGrammar.h" -// Used for file input. -#include -#include +#include "src/storage/prism/Program.h" +#include "src/storage/expressions/Expression.h" +using namespace storm::prism; +using namespace storm::expressions; namespace storm { namespace parser { namespace prism { - - using namespace storm::ir; - using namespace storm::ir::expressions; - - struct GlobalVariableInformation { - std::vector booleanVariables; - std::vector integerVariables; - std::map booleanVariableToIndexMap; - std::map integerVariableToIndexMap; - }; - - /*! - * The Boost spirit grammar for the PRISM language. Returns the intermediate representation of - * the input that complies with the PRISM syntax. - */ - class PrismGrammar : public qi::grammar< - Iterator, - Program(), - qi::locals< - std::map>, - std::map>, - std::map>, - GlobalVariableInformation, - std::map, - std::map> - >, - Skipper> { + class PrismGrammar : public qi::grammar { public: /*! * Default constructor that creates an empty and functional grammar. */ PrismGrammar(); - /*! - * Puts all sub-grammars into the mode for performing the second run. A two-run model was chosen - * because modules can involve variables that are only declared afterwards, so the first run - * creates all variables and the second one tries to parse the full model. - */ - void prepareForSecondRun(); - - /*! - * Resets all sub-grammars, i.e. puts them into an initial state. - */ - void resetGrammars(); - private: - - std::shared_ptr state; - struct qi::symbols moduleMap_; - // The starting point of the grammar. - qi::rule< - Iterator, - Program(), - qi::locals< - std::map>, - std::map>, - std::map>, - GlobalVariableInformation, - std::map, - std::map> - >, - Skipper> start; + qi::rule start; + + // Rules for model type. qi::rule modelTypeDefinition; - qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; - qi::rule(), Skipper> moduleDefinitionList; + + // Rules for global constant definitions. + qi::rule&, std::set&, std::set&, std::map&, std::map&, std::map&), Skipper> constantDefinitionList; // Rules for global variable definitions - qi::rule globalVariableDefinitionList; + qi::rule&, std::map), Skipper> globalVariableDefinitionList; - // Rules for module definition. + // Rules for modules definition. + qi::rule(), Skipper> moduleDefinitionList; qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; qi::rule>, Skipper> moduleRenaming; @@ -156,6 +114,9 @@ namespace storm { storm::parser::prism::modelTypeStruct modelType_; storm::parser::prism::relationalOperatorStruct relations_; + // A mapping from module names to the modules themselves so they can be looked up for renaming later. + struct qi::symbols moduleMap_; + /*! * Adds a label with the given name and expression to the given label-to-expression map. * @@ -263,5 +224,5 @@ namespace storm { } // namespace storm -#endif /* STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H */ +#endif /* STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H_ */ diff --git a/src/parser/prismparser/Tokens.h b/src/parser/prismparser/Tokens.h index bbf7e8418..bcaefce7b 100644 --- a/src/parser/prismparser/Tokens.h +++ b/src/parser/prismparser/Tokens.h @@ -1,75 +1,66 @@ -/* - * File: Tokens.h - * Author: nafur - * - * Created on April 19, 2013, 11:17 PM - */ +#ifndef STORM_PARSER_PRISMPARSER_TOKENS_H_ +#define STORM_PARSER_PRISMPARSER_TOKENS_H_ -#ifndef TOKENS_H -#define TOKENS_H +#include "src/storage/expressions/Expression.h" namespace storm { -namespace parser { -namespace prism { - - /*! - * A structure mapping the textual representation of a model type to the model type - * representation of the intermediate representation. - */ - struct modelTypeStruct : qi::symbols { - modelTypeStruct() { - add - ("dtmc", Program::ModelType::DTMC) - ("ctmc", Program::ModelType::CTMC) - ("mdp", Program::ModelType::MDP) - ("ctmdp", Program::ModelType::CTMDP) - ; - } - }; - - - /*! - * A structure defining the keywords that are not allowed to be chosen as identifiers. - */ - struct keywordsStruct : qi::symbols { - keywordsStruct() { - add - ("dtmc", 1) - ("ctmc", 2) - ("mdp", 3) - ("ctmdp", 4) - ("const", 5) - ("int", 6) - ("bool", 7) - ("module", 8) - ("endmodule", 9) - ("rewards", 10) - ("endrewards", 11) - ("true", 12) - ("false", 13) - ; - } - }; - - /*! - * A structure mapping the textual representation of a binary relation to the representation - * of the intermediate representation. - */ - struct relationalOperatorStruct : qi::symbols { - relationalOperatorStruct() { - add - ("=", BinaryRelationExpression::EQUAL) - ("!=", BinaryRelationExpression::NOT_EQUAL) - ("<", BinaryRelationExpression::LESS) - ("<=", BinaryRelationExpression::LESS_OR_EQUAL) - (">", BinaryRelationExpression::GREATER) - (">=", BinaryRelationExpression::GREATER_OR_EQUAL) - ; - } - }; -} -} + namespace parser { + namespace prism { + /*! + * A structure mapping the textual representation of a model type to the model type + * representation of the intermediate representation. + */ + struct modelTypeStruct : qi::symbols { + modelTypeStruct() { + add + ("dtmc", Program::ModelType::DTMC) + ("ctmc", Program::ModelType::CTMC) + ("mdp", Program::ModelType::MDP) + ("ctmdp", Program::ModelType::CTMDP) + ("ma", Program::ModelType::MA); + } + }; + + /*! + * A structure defining the keywords that are not allowed to be chosen as identifiers. + */ + struct keywordsStruct : qi::symbols { + keywordsStruct() { + add + ("dtmc", 1) + ("ctmc", 2) + ("mdp", 3) + ("ctmdp", 4) + ("ma", 5) + ("const", 6) + ("int", 7) + ("bool", 8) + ("module", 9) + ("endmodule", 10) + ("rewards", 11) + ("endrewards", 12) + ("true", 13) + ("false", 14); + } + }; + + /*! + * A structure mapping the textual representation of a binary relation. + */ + struct relationalOperatorStruct : qi::symbols { + relationalOperatorStruct() { + add + ("=", BinaryRelationExpression::RelationType::EQUAL) + ("!=", BinaryRelationExpression::RelationType::NOT_EQUAL) + ("<", BinaryRelationExpression::RelationType::LESS) + ("<=", BinaryRelationExpression::RelationType::LESS_OR_EQUAL) + (">", BinaryRelationExpression::RelationType::GREATER) + (">=", BinaryRelationExpression::RelationType::GREATER_OR_EQUAL); + } + }; + } + } } -#endif /* TOKENS_H */ +#endif /* STORM_PARSER_PRISMPARSER_TOKENS_H_ */ diff --git a/src/parser/prismparser/VariableState.cpp b/src/parser/prismparser/VariableState.cpp deleted file mode 100644 index 244a3f17e..000000000 --- a/src/parser/prismparser/VariableState.cpp +++ /dev/null @@ -1,191 +0,0 @@ -#include "VariableState.h" -#include "src/exceptions/InvalidArgumentException.h" - -namespace storm { - namespace parser { - namespace prism { - - using namespace storm::ir; - using namespace storm::ir::expressions; - - template - struct SymbolDump { - SymbolDump(std::ostream& out) : out(out) {} - void operator() (std::basic_string s, T elem) { - this->out << "\t" << s << " -> " << elem << std::endl; - } - private: - std::ostream& out; - }; - template - std::ostream& operator<<(std::ostream& out, qi::symbols& symbols) { - out << "Dumping symbol table" << std::endl; - SymbolDump dump(out); - symbols.for_each(dump); - return out; - } - std::ostream& operator<<(std::ostream& out, VariableState::variableNamesStruct& symbols) { - SymbolDump dump(out); - symbols.for_each(dump); - return out; - } - - - VariableState::VariableState(bool firstRun) : firstRun(firstRun), keywords(), nextLocalBooleanVariableIndex(0), nextLocalIntegerVariableIndex(0), nextGlobalBooleanVariableIndex(0), nextGlobalIntegerVariableIndex(0), nextGlobalCommandIndex(0), nextGlobalUpdateIndex(0) { - // Nothing to do here. - } - - uint_fast64_t VariableState::getNextLocalBooleanVariableIndex() const { - return this->nextLocalBooleanVariableIndex; - } - - uint_fast64_t VariableState::getNextLocalIntegerVariableIndex() const { - return this->nextLocalIntegerVariableIndex; - } - - uint_fast64_t VariableState::getNextGlobalBooleanVariableIndex() const { - return this->nextGlobalBooleanVariableIndex; - } - - uint_fast64_t VariableState::getNextGlobalIntegerVariableIndex() const { - return this->nextGlobalIntegerVariableIndex; - } - - uint_fast64_t VariableState::getNextGlobalCommandIndex() const { - return this->nextGlobalCommandIndex; - } - - uint_fast64_t VariableState::getNextGlobalUpdateIndex() const { - return this->nextGlobalUpdateIndex; - } - - uint_fast64_t VariableState::addBooleanVariable(std::string const& name) { - if (firstRun) { - LOG4CPLUS_TRACE(logger, "Adding boolean variable " << name << " with new id " << this->nextGlobalBooleanVariableIndex << "."); - this->booleanVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextGlobalBooleanVariableIndex, name))); - this->booleanVariableNames_.add(name, name); - ++this->nextGlobalBooleanVariableIndex; - ++this->nextLocalBooleanVariableIndex; - return this->nextGlobalBooleanVariableIndex - 1; - } else { - std::shared_ptr variableExpression = this->booleanVariables_.at(name); - if (variableExpression != nullptr) { - return variableExpression->getGlobalVariableIndex(); - } else { - LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist."); - throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist."; - } - } - } - - uint_fast64_t VariableState::addIntegerVariable(std::string const& name) { - if (firstRun) { - LOG4CPLUS_TRACE(logger, "Adding integer variable " << name << " with new id " << this->nextGlobalIntegerVariableIndex << "."); - this->integerVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextGlobalIntegerVariableIndex, name))); - this->integerVariableNames_.add(name, name); - ++this->nextGlobalIntegerVariableIndex; - ++this->nextLocalIntegerVariableIndex; - return this->nextGlobalIntegerVariableIndex - 1; - } else { - std::shared_ptr variableExpression = this->integerVariables_.at(name); - if (variableExpression != nullptr) { - return variableExpression->getGlobalVariableIndex(); - } else { - LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist."); - throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist."; - } - } - } - - std::shared_ptr VariableState::getBooleanVariableExpression(std::string const& name) const { - std::shared_ptr const* variableExpression = this->booleanVariables_.find(name); - if (variableExpression != nullptr) { - return *variableExpression; - } else { - if (firstRun) { - LOG4CPLUS_TRACE(logger, "Trying to retrieve boolean variable " << name << " that was not yet created; returning dummy instead."); - return std::shared_ptr(new VariableExpression(BaseExpression::bool_, name)); - } else { - LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist."); - throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist."; - } - } - } - - std::shared_ptr VariableState::getIntegerVariableExpression(std::string const& name) const { - std::shared_ptr const* variableExpression = this->integerVariables_.find(name); - if (variableExpression != nullptr) { - return *variableExpression; - } else { - if (firstRun) { - LOG4CPLUS_TRACE(logger, "Trying to retrieve integer variable " << name << " that was not yet created; returning dummy instead."); - return std::shared_ptr(new VariableExpression(BaseExpression::int_, name)); - } else { - LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist."); - throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist."; - } - } - } - - std::shared_ptr VariableState::getVariableExpression(std::string const& name) const { - std::shared_ptr const* variableExpression = this->integerVariables_.find(name); - if (variableExpression != nullptr) { - return *variableExpression; - } - - variableExpression = this->booleanVariables_.find(name); - if (variableExpression != nullptr) { - return *variableExpression; - } - LOG4CPLUS_ERROR(logger, "Variable " << name << " does not exist."); - throw storm::exceptions::InvalidArgumentException() << "Variable " << name << " does not exist."; - } - - void VariableState::clearLocalVariables() { - this->localBooleanVariables_.clear(); - this->localIntegerVariables_.clear(); - this->nextLocalBooleanVariableIndex = 0; - this->nextLocalIntegerVariableIndex = 0; - } - - bool VariableState::isFreeIdentifier(std::string const& identifier) const { - if (this->booleanVariableNames_.find(identifier) != nullptr) return false; - if (this->integerVariableNames_.find(identifier) != nullptr) return false; - if (this->allConstantNames_.find(identifier) != nullptr) return false; - if (this->labelNames_.find(identifier) != nullptr) return false; - if (this->moduleNames_.find(identifier) != nullptr) return false; - if (this->keywords.find(identifier) != nullptr) return false; - if (this->booleanFormulas_.find(identifier) != nullptr) return false; - if (this->integerFormulas_.find(identifier) != nullptr) return false; - if (this->doubleFormulas_.find(identifier) != nullptr) return false; - if (this->constantBooleanFormulas_.find(identifier) != nullptr) return false; - if (this->constantIntegerFormulas_.find(identifier) != nullptr) return false; - if (this->constantDoubleFormulas_.find(identifier) != nullptr) return false; - return true; - } - - bool VariableState::isIdentifier(std::string const& identifier) const { - if (this->allConstantNames_.find(identifier) != nullptr) return false; - if (this->keywords.find(identifier) != nullptr) return false; - return true; - } - - void VariableState::prepareForSecondRun() { - integerConstants_.clear(); - booleanConstants_.clear(); - doubleConstants_.clear(); - allConstantNames_.clear(); - constantBooleanFormulas_.clear(); - booleanFormulas_.clear(); - constantIntegerFormulas_.clear(); - integerFormulas_.clear(); - constantDoubleFormulas_.clear(); - doubleFormulas_.clear(); - this->firstRun = false; - nextGlobalCommandIndex = 0; - nextGlobalUpdateIndex = 0; - } - - } // namespace prism - } // namespace parser -} // namespace storm diff --git a/src/parser/prismparser/VariableState.h b/src/parser/prismparser/VariableState.h deleted file mode 100644 index 6dc7170a4..000000000 --- a/src/parser/prismparser/VariableState.h +++ /dev/null @@ -1,207 +0,0 @@ -/* - * File: VariableState.h - * Author: nafur - * - * Created on April 10, 2013, 4:43 PM - */ - -#ifndef STORM_PARSER_PRISMPARSER_VARIABLESTATE_H -#define STORM_PARSER_PRISMPARSER_VARIABLESTATE_H - -#include - -#include "src/ir/IR.h" -#include "Includes.h" -#include "Tokens.h" - -namespace storm { - namespace parser { - namespace prism { - - using namespace storm::ir; - using namespace storm::ir::expressions; - - template - std::ostream& operator<<(std::ostream& out, qi::symbols& symbols); - - /*! - * This class contains the internal state that is needed for parsing a PRISM model. - */ - class VariableState { - public: - /*! - * Creates a new variable state object. By default, this object will be set to a state in which - * it is ready for performing a first run on some input. The first run creates all variables - * while the second one checks for the correct usage of variables in expressions. - * - * @param firstRun If set, this object will be in a state ready for performing the first run. If - * set to false, this object will assume that it has all variable data already. - */ - VariableState(bool firstRun = true); - - /*! - * Indicator, if we are still in the first run. - */ - bool firstRun; - - /*! - * A parser for all reserved keywords. - */ - keywordsStruct keywords; - - /*! - * Internal counter for the local index of the next new boolean variable. - */ - uint_fast64_t nextLocalBooleanVariableIndex; - - /*! - * Retrieves the next free local index for a boolean variable. - * - * @return The next free local index for a boolean variable. - */ - uint_fast64_t getNextLocalBooleanVariableIndex() const; - - /*! - * Internal counter for the local index of the next new integer variable. - */ - uint_fast64_t nextLocalIntegerVariableIndex; - - /*! - * Retrieves the next free global index for a integer variable. - * - * @return The next free global index for a integer variable. - */ - uint_fast64_t getNextLocalIntegerVariableIndex() const; - - /*! - * Internal counter for the index of the next new boolean variable. - */ - uint_fast64_t nextGlobalBooleanVariableIndex; - - /*! - * Retrieves the next free global index for a boolean variable. - * - * @return The next free global index for a boolean variable. - */ - uint_fast64_t getNextGlobalBooleanVariableIndex() const; - - /*! - * Internal counter for the index of the next new integer variable. - */ - uint_fast64_t nextGlobalIntegerVariableIndex; - - /*! - * Retrieves the next free global index for a integer variable. - * - * @return The next free global index for a integer variable. - */ - uint_fast64_t getNextGlobalIntegerVariableIndex() const; - - /*! - * Internal counter for the index of the next command. - */ - uint_fast64_t nextGlobalCommandIndex; - - /*! - * Retrieves the next free global index for a command. - * - * @return The next free global index for a command. - */ - uint_fast64_t getNextGlobalCommandIndex() const; - - /*! - * Internal counter for the index of the next update. - */ - uint_fast64_t nextGlobalUpdateIndex; - - /*! - * Retrieves the next free global index for an update. - * - * @return The next free global index for an update. - */ - uint_fast64_t getNextGlobalUpdateIndex() const; - - // Structures mapping variable and constant names to the corresponding expression nodes of - // the intermediate representation. - struct qi::symbols> integerVariables_, booleanVariables_; - struct qi::symbols> integerConstants_, booleanConstants_, doubleConstants_, booleanFormulas_, constantBooleanFormulas_, integerFormulas_, constantIntegerFormulas_, doubleFormulas_, constantDoubleFormulas_; - - // A structure representing the identity function over identifier names. - struct variableNamesStruct : qi::symbols { } - integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_, - localBooleanVariables_, localIntegerVariables_, assignedBooleanVariables_, assignedIntegerVariables_, - globalBooleanVariables_, globalIntegerVariables_; - - /*! - * Adds a new boolean variable with the given name. - * - * @param name The name of the variable. - * @return The global index of the variable. - */ - uint_fast64_t addBooleanVariable(std::string const& name); - - /*! - * Adds a new integer variable with the given name. - * - * @param name The name of the variable. - * @return The global index of the variable. - */ - uint_fast64_t addIntegerVariable(std::string const& name); - - /*! - * Retrieves the variable expression for the boolean variable with the given name. - * - * @param name The name of the boolean variable for which to retrieve the variable expression. - * @return The variable expression for the boolean variable with the given name. - */ - std::shared_ptr getBooleanVariableExpression(std::string const& name) const; - - /*! - * Retrieves the variable expression for the integer variable with the given name. - * - * @param name The name of the integer variable for which to retrieve the variable expression. - * @return The variable expression for the integer variable with the given name. - */ - std::shared_ptr getIntegerVariableExpression(std::string const& name) const; - - /*! - * Retrieve the variable expression for the variable with the given name. - * - * @param name The name of the variable for which to retrieve the variable expression. - * @return The variable expression for the variable with the given name. - */ - std::shared_ptr getVariableExpression(std::string const& name) const; - - /*! - * Clears all local variables. - */ - void clearLocalVariables(); - - /*! - * Check if the given string is a free identifier. - * - * @param identifier A string to be checked. - * @return True iff the given string is a free identifier. - */ - bool isFreeIdentifier(std::string const& identifier) const; - - /*! - * Check if given string is a valid identifier. - * - * @param identifier A string to be checked. - * @return True iff the given string is an identifier. - */ - bool isIdentifier(std::string const& identifier) const; - - /*! - * Prepare state to proceed to second parser run. Currently, this clears the constants. - */ - void prepareForSecondRun(); - }; - - } // namespace prism - } // namespace parser -} // namespace storm - -#endif /* STORM_PARSER_PRISMPARSER_VARIABLESTATE_H */ - diff --git a/src/storage/prism/Assignment.cpp b/src/storage/prism/Assignment.cpp index 4455ec65d..2c639a535 100644 --- a/src/storage/prism/Assignment.cpp +++ b/src/storage/prism/Assignment.cpp @@ -2,11 +2,11 @@ namespace storm { namespace prism { - Assignment::Assignment(std::string const& variableName, storm::expressions::Expression const& expression) : variableName(variableName), expression(expression) { + Assignment::Assignment(std::string const& variableName, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variableName(variableName), expression(expression) { // Intentionally left empty. } - Assignment::Assignment(Assignment const& oldAssignment, std::map const& renaming) : variableName(oldAssignment.getVariableName()), expression(oldAssignment.getExpression().substitute(renaming)) { + Assignment::Assignment(Assignment const& oldAssignment, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variableName(oldAssignment.getVariableName()), expression(oldAssignment.getExpression().substitute(renaming)) { auto renamingPair = renaming.find(oldAssignment.variableName); if (renamingPair != renaming.end()) { this->variableName = renamingPair->second; diff --git a/src/storage/prism/Assignment.h b/src/storage/prism/Assignment.h index 48a235c8a..955c8417e 100644 --- a/src/storage/prism/Assignment.h +++ b/src/storage/prism/Assignment.h @@ -3,34 +3,39 @@ #include +#include "src/storage/prism/LocatedInformation.h" #include "src/storage/expressions/Expression.h" namespace storm { namespace prism { - class Assignment { + class Assignment : public LocatedInformation { public: /*! * Constructs an assignment using the given variable name and expression. * * @param variableName The variable that this assignment targets. * @param expression The expression to assign to the variable. + * @param filename The filename in which the assignment is defined. + * @param lineNumber The line number in which the assignment is defined. */ - Assignment(std::string const& variableName, storm::expressions::Expression const& expression); + Assignment(std::string const& variableName, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Creates a copy of the given assignment and performs the provided renaming. * * @param oldAssignment The assignment to copy. * @param renaming A mapping from names that are to be renamed to the names they are to be replaced with. + * @param filename The filename in which the assignment is defined. + * @param lineNumber The line number in which the assignment is defined. */ - Assignment(Assignment const& oldAssignment, std::map const& renaming); + Assignment(Assignment const& oldAssignment, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. Assignment() = default; - Assignment(Assignment const& otherVariable) = default; - Assignment& operator=(Assignment const& otherVariable)= default; - Assignment(Assignment&& otherVariable) = default; - Assignment& operator=(Assignment&& otherVariable) = default; + Assignment(Assignment const& other) = default; + Assignment& operator=(Assignment const& other)= default; + Assignment(Assignment&& other) = default; + Assignment& operator=(Assignment&& other) = default; /*! * Retrieves the name of the variable that this assignment targets. diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp index 39ea86304..0ce68d34d 100644 --- a/src/storage/prism/BooleanVariable.cpp +++ b/src/storage/prism/BooleanVariable.cpp @@ -2,15 +2,15 @@ namespace storm { namespace prism { - BooleanVariable::BooleanVariable(std::string const& variableName) : Variable(variableName, storm::expressions::Expression::createFalse(), true) { + BooleanVariable::BooleanVariable(std::string const& variableName, std::string const& filename, uint_fast64_t lineNumber) : Variable(variableName, storm::expressions::Expression::createFalse(), true, filename, lineNumber) { // Nothing to do here. } - BooleanVariable::BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression) : Variable(variableName, initialValueExpression, false) { + BooleanVariable::BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variableName, initialValueExpression, false, filename, lineNumber) { // Nothing to do here. } - BooleanVariable::BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, std::map const& renaming) : Variable(oldVariable, newName, renaming) { + BooleanVariable::BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : Variable(oldVariable, newName, renaming, filename, lineNumber) { // Nothing to do here. } diff --git a/src/storage/prism/BooleanVariable.h b/src/storage/prism/BooleanVariable.h index 74c046e00..580a6c33a 100644 --- a/src/storage/prism/BooleanVariable.h +++ b/src/storage/prism/BooleanVariable.h @@ -11,26 +11,30 @@ namespace storm { public: // Create default implementations of constructors/assignment. BooleanVariable() = default; - BooleanVariable(BooleanVariable const& otherVariable) = default; - BooleanVariable& operator=(BooleanVariable const& otherVariable)= default; - BooleanVariable(BooleanVariable&& otherVariable) = default; - BooleanVariable& operator=(BooleanVariable&& otherVariable) = default; - + BooleanVariable(BooleanVariable const& other) = default; + BooleanVariable& operator=(BooleanVariable const& other)= default; + BooleanVariable(BooleanVariable&& other) = default; + BooleanVariable& operator=(BooleanVariable&& other) = default; + /*! - * Creates a boolean variable with the given name and default initial value. + * Creates a boolean variable with the given name and the default initial value expression. * * @param variableName The name of the variable. + * @param filename The filename in which the variable is defined. + * @param lineNumber The line number in which the variable is defined. */ - BooleanVariable(std::string const& variableName); + BooleanVariable(std::string const& variableName, std::string const& filename, uint_fast64_t lineNumber); /*! * Creates a boolean variable with the given name and the given constant initial value expression. * * @param variableName The name of the variable. * @param initialValueExpression The constant expression that defines the initial value of the variable. + * @param filename The filename in which the variable is defined. + * @param lineNumber The line number in which the variable is defined. */ - BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression); - + BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber); + /*! * Creates a copy of the given boolean variable and performs the provided renaming. * @@ -38,8 +42,10 @@ namespace storm { * @param newName New name of this variable. * @param renaming A mapping from names that are to be renamed to the names they are to be * replaced with. + * @param filename The filename in which the variable is defined. + * @param lineNumber The line number in which the variable is defined. */ - BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, std::map const& renaming); + BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber); friend std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable); }; diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp index 5624eafdb..038884593 100644 --- a/src/storage/prism/Command.cpp +++ b/src/storage/prism/Command.cpp @@ -2,18 +2,18 @@ namespace storm { namespace prism { - Command::Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector const& updates) : actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex) { + Command::Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector const& updates, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex) { // Nothing to do here. } - Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map const& renaming) : actionName(oldCommand.getActionName()), guardExpression(oldCommand.getGuardExpression().substitute(renaming)), globalIndex(newGlobalIndex) { + Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(oldCommand.getActionName()), guardExpression(oldCommand.getGuardExpression().substitute(renaming)), globalIndex(newGlobalIndex) { auto const& namePair = renaming.find(this->actionName); if (namePair != renaming.end()) { this->actionName = namePair->second; } this->updates.reserve(oldCommand.getNumberOfUpdates()); for (Update const& update : oldCommand.getUpdates()) { - this->updates.emplace_back(update, update.getGlobalIndex(), renaming); + this->updates.emplace_back(update, update.getGlobalIndex(), renaming, filename, lineNumber); } } diff --git a/src/storage/prism/Command.h b/src/storage/prism/Command.h index 8cb905346..5780c3dce 100644 --- a/src/storage/prism/Command.h +++ b/src/storage/prism/Command.h @@ -10,7 +10,7 @@ namespace storm { namespace prism { - class Command { + class Command : public LocatedInformation { public: /*! * Creates a command with the given action name, guard and updates. @@ -19,8 +19,10 @@ namespace storm { * @param actionName The action name of the command. * @param guardExpression the expression that defines the guard of the command. * @param updates A list of updates that is associated with this command. + * @param filename The filename in which the command is defined. + * @param lineNumber The line number in which the command is defined. */ - Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector const& updates); + Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector const& updates, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Creates a copy of the given command and performs the provided renaming. @@ -28,15 +30,17 @@ namespace storm { * @param oldCommand The command to copy. * @param newGlobalIndex The global index of the copy of the command. * @param renaming A mapping from names that are to be renamed to the names they are to be replaced with. + * @param filename The filename in which the command is defined. + * @param lineNumber The line number in which the command is defined. */ - Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map const& renaming); + Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. Command() = default; - Command(Command const& otherVariable) = default; - Command& operator=(Command const& otherVariable)= default; - Command(Command&& otherVariable) = default; - Command& operator=(Command&& otherVariable) = default; + Command(Command const& other) = default; + Command& operator=(Command const& other)= default; + Command(Command&& other) = default; + Command& operator=(Command&& other) = default; /*! * Retrieves the action name of this command. diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp index 10a3f3e88..47005e6cd 100644 --- a/src/storage/prism/IntegerVariable.cpp +++ b/src/storage/prism/IntegerVariable.cpp @@ -2,15 +2,15 @@ namespace storm { namespace prism { - IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression) : Variable(variableName, lowerBoundExpression, true), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) { + IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variableName, lowerBoundExpression, true, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) { // Intentionally left empty. } - IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression) : Variable(variableName, initialValueExpression, false), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) { + IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variableName, initialValueExpression, false, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) { // Intentionally left empty. } - IntegerVariable::IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, std::map const& renaming) : Variable(oldVariable, newName, renaming), lowerBoundExpression(oldVariable.getLowerBoundExpression().substitute(renaming)), upperBoundExpression(oldVariable.getUpperBoundExpression().substitute(renaming)) { + IntegerVariable::IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : Variable(oldVariable, newName, renaming, filename, lineNumber), lowerBoundExpression(oldVariable.getLowerBoundExpression().substitute(renaming)), upperBoundExpression(oldVariable.getUpperBoundExpression().substitute(renaming)) { // Intentionally left empty. } diff --git a/src/storage/prism/IntegerVariable.h b/src/storage/prism/IntegerVariable.h index b2dbb4cb5..919bab480 100644 --- a/src/storage/prism/IntegerVariable.h +++ b/src/storage/prism/IntegerVariable.h @@ -11,10 +11,10 @@ namespace storm { public: // Create default implementations of constructors/assignment. IntegerVariable() = default; - IntegerVariable(IntegerVariable const& otherVariable) = default; - IntegerVariable& operator=(IntegerVariable const& otherVariable)= default; - IntegerVariable(IntegerVariable&& otherVariable) = default; - IntegerVariable& operator=(IntegerVariable&& otherVariable) = default; + IntegerVariable(IntegerVariable const& other) = default; + IntegerVariable& operator=(IntegerVariable const& other)= default; + IntegerVariable(IntegerVariable&& other) = default; + IntegerVariable& operator=(IntegerVariable&& other) = default; /*! * Creates an integer variable with the given name and a default initial value. @@ -22,8 +22,10 @@ namespace storm { * @param variableName The name of the variable. * @param lowerBoundExpression A constant expression defining the lower bound of the domain of the variable. * @param upperBoundExpression A constant expression defining the upper bound of the domain of the variable. + * @param filename The filename in which the variable is defined. + * @param lineNumber The line number in which the variable is defined. */ - IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression); + IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Creates an integer variable with the given name and the given initial value expression. @@ -32,8 +34,10 @@ namespace storm { * @param lowerBoundExpression A constant expression defining the lower bound of the domain of the variable. * @param upperBoundExpression A constant expression defining the upper bound of the domain of the variable. * @param initialValueExpression A constant expression that defines the initial value of the variable. + * @param filename The filename in which the variable is defined. + * @param lineNumber The line number in which the variable is defined. */ - IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression); + IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Creates a copy of the given integer variable and performs the provided renaming. @@ -41,8 +45,10 @@ namespace storm { * @param oldVariable The variable to copy. * @param newName New name of this variable. * @param renaming A mapping from names that are to be renamed to the names they are to be replaced with. + * @param filename The filename in which the variable is defined. + * @param lineNumber The line number in which the variable is defined. */ - IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, std::map const& renaming); + IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Retrieves an expression defining the lower bound for this integer variable. diff --git a/src/storage/prism/LocatedInformation.cpp b/src/storage/prism/LocatedInformation.cpp new file mode 100644 index 000000000..94d965e94 --- /dev/null +++ b/src/storage/prism/LocatedInformation.cpp @@ -0,0 +1,17 @@ +#include "src/storage/prism/LocatedInformation.h" + +namespace storm { + namespace prism { + LocatedInformation::LocatedInformation(std::string const& filename, uint_fast64_t lineNumber) : filename(filename), lineNumber(lineNumber) { + // Intentionally left empty. + } + + std::string const& LocatedInformation::getFilename() const { + return this->filename; + } + + uint_fast64_t LocatedInformation::getLineNumber() const { + return this->lineNumber; + } + } +} \ No newline at end of file diff --git a/src/storage/prism/LocatedInformation.h b/src/storage/prism/LocatedInformation.h new file mode 100644 index 000000000..f86060958 --- /dev/null +++ b/src/storage/prism/LocatedInformation.h @@ -0,0 +1,48 @@ +#ifndef STORM_STORAGE_PRISM_LOCATEDINFORMATION_H_ +#define STORM_STORAGE_PRISM_LOCATEDINFORMATION_H_ + +#include + +namespace storm { + namespace prism { + class LocatedInformation { + public: + /*! + * Constructs a located information with the given filename and line number. + * + * @param filename The file in which the information was found. + * @param lineNumber The line number in which the information was found. + */ + LocatedInformation(std::string const& filename, uint_fast64_t lineNumber); + + // Create default implementations of constructors/assignment. + LocatedInformation(LocatedInformation const& other) = default; + LocatedInformation& operator=(LocatedInformation const& other)= default; + LocatedInformation(LocatedInformation&& other) = default; + LocatedInformation& operator=(LocatedInformation&& other) = default; + + /*! + * Retrieves the name of the file in which the information was found. + * + * @return The name of the file in which the information was found. + */ + std::string const& getFilename() const; + + /*! + * Retrieves the line number in which the information was found. + * + * @return The line number in which the information was found. + */ + uint_fast64_t getLineNumber() const; + + private: + // The file in which the piece of information was found. + std::string filename; + + // The line in the file in which the piece of information was found. + uint_fast64_t lineNumber; + }; + } +} + +#endif /* STORM_STORAGE_PRISM_LOCATEDINFORMATION_H_ */ \ No newline at end of file diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 5a90c4bda..78f561734 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -5,24 +5,24 @@ namespace storm { namespace prism { - Module::Module(std::string const& moduleName, std::map const& booleanVariables, std::map const& integerVariables, std::vector const& commands) : moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands), actions(), actionsToCommandIndexMap() { + Module::Module(std::string const& moduleName, std::map const& booleanVariables, std::map const& integerVariables, std::vector const& commands, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands), actions(), actionsToCommandIndexMap() { // Initialize the internal mappings for fast information retrieval. this->collectActions(); } - Module::Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming) : moduleName(newModuleName), booleanVariables(), integerVariables(), commands(), actions(), actionsToCommandIndexMap() { + Module::Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(newModuleName), booleanVariables(), integerVariables(), commands(), actions(), actionsToCommandIndexMap() { // Iterate over boolean variables and rename them. If a variable was not renamed, this is an error and an exception is thrown. for (auto const& nameVariablePair : oldModule.getBooleanVariables()) { auto renamingPair = renaming.find(nameVariablePair.first); LOG_THROW(renamingPair == renaming.end(), storm::exceptions::InvalidArgumentException, "Boolean variable " << moduleName << "." << nameVariablePair.first << " was not renamed."); - this->booleanVariables.emplace(nameVariablePair.first, BooleanVariable(nameVariablePair.second, renamingPair->second, renaming)); + this->booleanVariables.emplace(nameVariablePair.first, BooleanVariable(nameVariablePair.second, renamingPair->second, renaming, filename, lineNumber)); } // Now do the same for the integer variables. for (auto const& nameVariablePair : oldModule.getIntegerVariables()) { auto renamingPair = renaming.find(nameVariablePair.first); LOG_THROW(renamingPair == renaming.end(), storm::exceptions::InvalidArgumentException, "Integer variable " << moduleName << "." << nameVariablePair.first << " was not renamed."); - this->integerVariables.emplace(nameVariablePair.first, IntegerVariable(nameVariablePair.second, renamingPair->second, renaming)); + this->integerVariables.emplace(nameVariablePair.first, IntegerVariable(nameVariablePair.second, renamingPair->second, renaming, filename, lineNumber)); } // Now we are ready to clone all commands and rename them if requested. diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index 789cd0e09..d8f75d13b 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -14,7 +14,7 @@ namespace storm { namespace prism { - class Module { + class Module : public LocatedInformation { public: /*! * Creates a module with the given name, variables and commands. @@ -23,10 +23,10 @@ namespace storm { * @param booleanVariables The boolean variables defined by the module. * @param integerVariables The integer variables defined by the module. * @param commands The commands of the module. + * @param filename The filename in which the module is defined. + * @param lineNumber The line number in which the module is defined. */ - Module(std::string const& moduleName, std::map const& booleanVariables, - std::map const& integerVariables, - std::vector const& commands); + Module(std::string const& moduleName, std::map const& booleanVariables, std::map const& integerVariables, std::vector const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Special copy constructor, implementing the module renaming functionality. This will create a new module @@ -35,15 +35,17 @@ namespace storm { * @param oldModule The module to be copied. * @param newModuleName The name of the new module. * @param renaming A mapping of identifiers to the new identifiers they are to be replaced with. + * @param filename The filename in which the module is defined. + * @param lineNumber The line number in which the module is defined. */ - Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming); + Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. Module() = default; - Module(Module const& otherVariable) = default; - Module& operator=(Module const& otherVariable)= default; - Module(Module&& otherVariable) = default; - Module& operator=(Module&& otherVariable) = default; + Module(Module const& other) = default; + Module& operator=(Module const& other)= default; + Module(Module&& other) = default; + Module& operator=(Module&& other) = default; /*! * Retrieves the number of boolean variables in the module. diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index a688a63dd..c01e24c0d 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -5,7 +5,7 @@ namespace storm { namespace prism { - Program::Program(ModelType modelType, std::set const& undefinedBooleanConstants, std::set const& undefinedIntegerConstants, std::set const& undefinedDoubleConstants, std::map const& globalBooleanVariables, std::map const& globalIntegerVariables, std::vector const& modules, std::map const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map const& labels) : modelType(modelType), undefinedBooleanConstants(undefinedBooleanConstants), undefinedIntegerConstants(undefinedIntegerConstants), undefinedDoubleConstants(undefinedDoubleConstants), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), modules(modules), rewardModels(rewardModels), hasInitialStatesExpression(hasInitialStatesExpression), initialStatesExpression(initialStatesExpression), labels(labels), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() { + Program::Program(ModelType modelType, std::set const& undefinedBooleanConstants, std::map definedBooleanConstants, std::set const& undefinedIntegerConstants, std::map definedIntegerConstants, std::set const& undefinedDoubleConstants, std::map definedDoubleConstants, std::map const& globalBooleanVariables, std::map const& globalIntegerVariables, std::vector const& modules, std::map const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map const& labels, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), modelType(modelType), undefinedBooleanConstants(undefinedBooleanConstants), definedBooleanConstants(definedBooleanConstants), undefinedIntegerConstants(undefinedIntegerConstants), definedIntegerConstants(definedIntegerConstants), undefinedDoubleConstants(undefinedDoubleConstants), definedDoubleConstants(definedDoubleConstants), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), modules(modules), rewardModels(rewardModels), hasInitialStatesExpression(hasInitialStatesExpression), initialStatesExpression(initialStatesExpression), labels(labels), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() { // Now build the mapping from action names to module indices so that the lookup can later be performed quickly. for (unsigned int moduleIndex = 0; moduleIndex < this->getNumberOfModules(); moduleIndex++) { Module const& module = this->getModule(moduleIndex); @@ -52,15 +52,27 @@ namespace storm { std::set const& Program::getUndefinedBooleanConstants() const { return this->undefinedBooleanConstants; } + + std::map const& Program::getDefinedBooleanConstants() const { + return this->definedBooleanConstants; + } std::set const& Program::getUndefinedIntegerConstants() const { return this->undefinedIntegerConstants; } + std::map const& Program::getDefinedIntegerConstants() const { + return this->definedIntegerConstants; + } + std::set const& Program::getUndefinedDoubleConstants() const { return this->undefinedDoubleConstants; } - + + std::map const& Program::getDefinedDoubleConstants() const { + return this->definedDoubleConstants; + } + std::map const& Program::getGlobalBooleanVariables() const { return this->globalBooleanVariables; } diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 3f1b54e0d..36326b12b 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -12,7 +12,7 @@ namespace storm { namespace prism { - class Program { + class Program : public LocatedInformation { public: /*! * An enum for the different model types. @@ -25,8 +25,11 @@ namespace storm { * * @param modelType The type of the program. * @param undefinedBooleanConstants The undefined boolean constants of the program. + * @param definedBooleanConstants The defined boolean constants of the program. * @param undefinedIntegerConstants The undefined integer constants of the program. + * @param definedIntegerConstants The defined integer constants of the program. * @param undefinedDoubleConstants The undefined double constants of the program. + * @param definedDoubleConstants The defined double constants of the program. * @param globalBooleanVariables The global boolean variables of the program. * @param globalIntegerVariables The global integer variables of the program. * @param modules The modules of the program. @@ -37,15 +40,17 @@ namespace storm { * valid) expression, e.g. false. * @param rewardModels The reward models of the program. * @param labels The labels defined for this program. + * @param filename The filename in which the program is defined. + * @param lineNumber The line number in which the program is defined. */ - Program(ModelType modelType, std::set const& undefinedBooleanConstants, std::set const& undefinedIntegerConstants, std::set const& undefinedDoubleConstants, std::map const& globalBooleanVariables, std::map const& globalIntegerVariables, std::vector const& modules, std::map const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map const& labels); + Program(ModelType modelType, std::set const& undefinedBooleanConstants, std::map definedBooleanConstants, std::set const& undefinedIntegerConstants, std::map definedIntegerConstants, std::set const& undefinedDoubleConstants, std::map definedDoubleConstants, std::map const& globalBooleanVariables, std::map const& globalIntegerVariables, std::vector const& modules, std::map const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Provide default implementations for constructors and assignments. Program() = default; - Program(Program const& otherProgram) = default; - Program& operator=(Program const& otherProgram) = default; - Program(Program&& otherProgram) = default; - Program& operator=(Program&& otherProgram) = default; + Program(Program const& other) = default; + Program& operator=(Program const& other) = default; + Program(Program&& other) = default; + Program& operator=(Program&& other) = default; /*! * Retrieves the model type of the model. @@ -89,6 +94,13 @@ namespace storm { */ std::set const& getUndefinedBooleanConstants() const; + /*! + * Retrieves the defined boolean constants of the program. + * + * @return The defined boolean constants of the program. + */ + std::map const& getDefinedBooleanConstants() const; + /*! * Retrieves the undefined integer constants of the program. * @@ -96,6 +108,13 @@ namespace storm { */ std::set const& getUndefinedIntegerConstants() const; + /*! + * Retrieves the defined integer constants of the program. + * + * @return The defined integer constants of the program. + */ + std::map const& getDefinedIntegerConstants() const; + /*! * Retrieves the undefined double constants of the program. * @@ -103,6 +122,13 @@ namespace storm { */ std::set const& getUndefinedDoubleConstants() const; + /*! + * Retrieves the defined double constants of the program. + * + * @return The defined double constants of the program. + */ + std::map const& getDefinedDoubleConstants() const; + /*! * Retrieves the global boolean variables of the program. * @@ -242,15 +268,24 @@ namespace storm { // The type of the model. ModelType modelType; - // A list of undefined boolean constants of the model. + // The undefined boolean constants of the program. std::set undefinedBooleanConstants; - // A list of undefined integer constants of the model. + // A mapping of (defined) boolean constants to their values (given as expressions). + std::map definedBooleanConstants; + + // The undefined integer constants of the program. std::set undefinedIntegerConstants; - // A list of undefined double constants of the model. + // A mapping of (defined) integer constants to their values (given as expressions). + std::map definedIntegerConstants; + + // The undefined double constants of the program. std::set undefinedDoubleConstants; + // A mapping of (defined) double constants to their values (given as expressions). + std::map definedDoubleConstants; + // A list of global boolean variables. std::map globalBooleanVariables; diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp index 006ee1054..a25d58fc9 100644 --- a/src/storage/prism/RewardModel.cpp +++ b/src/storage/prism/RewardModel.cpp @@ -2,7 +2,7 @@ namespace storm { namespace prism { - RewardModel::RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) { + RewardModel::RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) { // Nothing to do here. } diff --git a/src/storage/prism/RewardModel.h b/src/storage/prism/RewardModel.h index 6c172c744..9e9498843 100644 --- a/src/storage/prism/RewardModel.h +++ b/src/storage/prism/RewardModel.h @@ -9,7 +9,7 @@ namespace storm { namespace prism { - class RewardModel { + class RewardModel : public LocatedInformation { public: /*! * Creates a reward model with the given name, state and transition rewards. @@ -17,15 +17,17 @@ namespace storm { * @param rewardModelName The name of the reward model. * @param stateRewards A vector of state-based rewards. * @param transitionRewards A vector of transition-based rewards. + * @param filename The filename in which the reward model is defined. + * @param lineNumber The line number in which the reward model is defined. */ - RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards); + RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. RewardModel() = default; - RewardModel(RewardModel const& otherVariable) = default; - RewardModel& operator=(RewardModel const& otherVariable)= default; - RewardModel(RewardModel&& otherVariable) = default; - RewardModel& operator=(RewardModel&& otherVariable) = default; + RewardModel(RewardModel const& other) = default; + RewardModel& operator=(RewardModel const& other)= default; + RewardModel(RewardModel&& other) = default; + RewardModel& operator=(RewardModel&& other) = default; /*! * Retrieves the name of the reward model. diff --git a/src/storage/prism/StateReward.cpp b/src/storage/prism/StateReward.cpp index c4bcbd428..7e36406c5 100644 --- a/src/storage/prism/StateReward.cpp +++ b/src/storage/prism/StateReward.cpp @@ -2,7 +2,7 @@ namespace storm { namespace prism { - StateReward::StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression) : statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) { + StateReward::StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) { // Nothing to do here. } diff --git a/src/storage/prism/StateReward.h b/src/storage/prism/StateReward.h index bdd08d446..5eb98886f 100644 --- a/src/storage/prism/StateReward.h +++ b/src/storage/prism/StateReward.h @@ -1,11 +1,12 @@ #ifndef STORM_STORAGE_PRISM_STATEREWARD_H_ #define STORM_STORAGE_PRISM_STATEREWARD_H_ +#include "src/storage/prism/LocatedInformation.h" #include "src/storage/expressions/Expression.h" namespace storm { namespace prism { - class StateReward { + class StateReward : public LocatedInformation { public: /*! * Creates a state reward for the states satisfying the given expression with the value given by a second @@ -13,15 +14,17 @@ namespace storm { * * @param statePredicateExpression The predicate that states earning this state-based reward need to satisfy. * @param rewardValueExpression An expression specifying the values of the rewards to attach to the states. + * @param filename The filename in which the state reward is defined. + * @param lineNumber The line number in which the state reward is defined. */ - StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression); + StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. StateReward() = default; - StateReward(StateReward const& otherVariable) = default; - StateReward& operator=(StateReward const& otherVariable)= default; - StateReward(StateReward&& otherVariable) = default; - StateReward& operator=(StateReward&& otherVariable) = default; + StateReward(StateReward const& other) = default; + StateReward& operator=(StateReward const& other)= default; + StateReward(StateReward&& other) = default; + StateReward& operator=(StateReward&& other) = default; /*! * Retrieves the state predicate that is associated with this state reward. diff --git a/src/storage/prism/TransitionReward.cpp b/src/storage/prism/TransitionReward.cpp index f972f1270..a5b81e55f 100644 --- a/src/storage/prism/TransitionReward.cpp +++ b/src/storage/prism/TransitionReward.cpp @@ -2,7 +2,7 @@ namespace storm { namespace prism { - TransitionReward::TransitionReward(std::string const& commandName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression) : commandName(commandName), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) { + TransitionReward::TransitionReward(std::string const& commandName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), commandName(commandName), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) { // Nothing to do here. } diff --git a/src/storage/prism/TransitionReward.h b/src/storage/prism/TransitionReward.h index 1fb783101..1232e5b51 100644 --- a/src/storage/prism/TransitionReward.h +++ b/src/storage/prism/TransitionReward.h @@ -1,11 +1,12 @@ #ifndef STORM_STORAGE_PRISM_TRANSITIONREWARD_H_ #define STORM_STORAGE_PRISM_TRANSITIONREWARD_H_ +#include "src/storage/prism/LocatedInformation.h" #include "src/storage/expressions/Expression.h" namespace storm { namespace prism { - class TransitionReward { + class TransitionReward : public LocatedInformation { public: /*! * Creates a transition reward for the transitions with the given name emanating from states satisfying the @@ -15,15 +16,17 @@ namespace storm { * @param statePredicateExpression The predicate that needs to hold before taking a transition with the previously * specified name in order to obtain the reward. * @param rewardValueExpression An expression specifying the values of the rewards to attach to the transitions. + * @param filename The filename in which the transition reward is defined. + * @param lineNumber The line number in which the transition reward is defined. */ - TransitionReward(std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression); + TransitionReward(std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. TransitionReward() = default; - TransitionReward(TransitionReward const& otherVariable) = default; - TransitionReward& operator=(TransitionReward const& otherVariable)= default; - TransitionReward(TransitionReward&& otherVariable) = default; - TransitionReward& operator=(TransitionReward&& otherVariable) = default; + TransitionReward(TransitionReward const& other) = default; + TransitionReward& operator=(TransitionReward const& other)= default; + TransitionReward(TransitionReward&& other) = default; + TransitionReward& operator=(TransitionReward&& other) = default; /*! * Retrieves the action name that is associated with this transition reward. diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp index f08627479..da92823bb 100644 --- a/src/storage/prism/Update.cpp +++ b/src/storage/prism/Update.cpp @@ -3,25 +3,25 @@ namespace storm { namespace prism { - Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::map const& booleanAssignments, std::map const& integerAssignments) : likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments), globalIndex(globalIndex) { + Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::map const& booleanAssignments, std::map const& integerAssignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments), globalIndex(globalIndex) { // Nothing to do here. } - Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map const& renaming) : likelihoodExpression(update.getLikelihoodExpression().substitute(renaming)), booleanAssignments(), integerAssignments(), globalIndex(newGlobalIndex) { + Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(update.getLikelihoodExpression().substitute(renaming)), booleanAssignments(), integerAssignments(), globalIndex(newGlobalIndex) { for (auto const& variableAssignmentPair : update.getBooleanAssignments()) { auto const& namePair = renaming.find(variableAssignmentPair.first); if (namePair != renaming.end()) { - this->booleanAssignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming)); + this->booleanAssignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber)); } else { - this->booleanAssignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming)); + this->booleanAssignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber)); } } for (auto const& variableAssignmentPair : update.getIntegerAssignments()) { auto const& namePair = renaming.find(variableAssignmentPair.first); if (renaming.count(variableAssignmentPair.first) > 0) { - this->integerAssignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming)); + this->integerAssignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber)); } else { - this->integerAssignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming)); + this->integerAssignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber)); } } this->likelihoodExpression = update.getLikelihoodExpression().substitute(renaming); diff --git a/src/storage/prism/Update.h b/src/storage/prism/Update.h index 878e394c3..4999c04bd 100644 --- a/src/storage/prism/Update.h +++ b/src/storage/prism/Update.h @@ -3,11 +3,12 @@ #include -#include "Assignment.h" +#include "src/storage/prism/LocatedInformation.h" +#include "src/storage/prism/Assignment.h" namespace storm { namespace prism { - class Update { + class Update : public LocatedInformation { public: /*! * Creates an update with the given expression specifying the likelihood and the mapping of variable to @@ -16,8 +17,10 @@ namespace storm { * @param globalIndex The global index of the update. * @param likelihoodExpression An expression specifying the likelihood of this update. * @param assignments A map of variable names to their assignments. + * @param filename The filename in which the variable is defined. + * @param lineNumber The line number in which the variable is defined. */ - Update(uint_fast64_t index, storm::expressions::Expression const& likelihoodExpression, std::map const& booleanAssignments, std::map const& integerAssignments); + Update(uint_fast64_t index, storm::expressions::Expression const& likelihoodExpression, std::map const& booleanAssignments, std::map const& integerAssignments, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Creates a copy of the given update and performs the provided renaming. @@ -25,15 +28,17 @@ namespace storm { * @param update The update that is to be copied. * @param newGlobalIndex The global index of the resulting update. * @param renaming A mapping from names that are to be renamed to the names they are to be replaced with. + * @param filename The filename in which the variable is defined. + * @param lineNumber The line number in which the variable is defined. */ - Update(Update const& update, uint_fast64_t newGlobalIndex, std::map const& renaming); + Update(Update const& update, uint_fast64_t newGlobalIndex, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. Update() = default; - Update(Update const& otherVariable) = default; - Update& operator=(Update const& otherVariable)= default; - Update(Update&& otherVariable) = default; - Update& operator=(Update&& otherVariable) = default; + Update(Update const& other) = default; + Update& operator=(Update const& other)= default; + Update(Update&& other) = default; + Update& operator=(Update&& other) = default; /*! * Retrieves the expression for the likelihood of this update. diff --git a/src/storage/prism/Variable.cpp b/src/storage/prism/Variable.cpp index a6f6f57ae..8ec4f2a98 100644 --- a/src/storage/prism/Variable.cpp +++ b/src/storage/prism/Variable.cpp @@ -4,11 +4,11 @@ namespace storm { namespace prism { - Variable::Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue) : variableName(variableName), initialValueExpression(initialValueExpression), defaultInitialValue(defaultInitialValue) { + Variable::Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variableName(variableName), initialValueExpression(initialValueExpression), defaultInitialValue(defaultInitialValue) { // Nothing to do here. } - Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map const& renaming) : variableName(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute(renaming)), defaultInitialValue(oldVariable.hasDefaultInitialValue()) { + Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variableName(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute(renaming)), defaultInitialValue(oldVariable.hasDefaultInitialValue()) { // Intentionally left empty. } diff --git a/src/storage/prism/Variable.h b/src/storage/prism/Variable.h index ef77a2c2d..51516bc24 100644 --- a/src/storage/prism/Variable.h +++ b/src/storage/prism/Variable.h @@ -3,11 +3,12 @@ #include +#include "src/storage/prism/LocatedInformation.h" #include "src/storage/expressions/Expression.h" namespace storm { namespace prism { - class Variable { + class Variable : public LocatedInformation { public: // Create default implementations of constructors/assignment. Variable(Variable const& otherVariable) = default; @@ -47,8 +48,10 @@ namespace storm { * @param initialValueExpression The constant expression that defines the initial value of the variable. * @param hasDefaultInitialValue A flag indicating whether the initial value of the variable is its default * value. + * @param filename The filename in which the variable is defined. + * @param lineNumber The line number in which the variable is defined. */ - Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue); + Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Creates a copy of the given variable and performs the provided renaming. @@ -56,8 +59,10 @@ namespace storm { * @param oldVariable The variable to copy. * @param newName New name of this variable. * @param renaming A mapping from names that are to be renamed to the names they are to be replaced with. + * @param filename The filename in which the variable is defined. + * @param lineNumber The line number in which the variable is defined. */ - Variable(Variable const& oldVariable, std::string const& newName, std::map const& renaming); + Variable(Variable const& oldVariable, std::string const& newName, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); private: // The name of the variable.