diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index 177d0f601..b7aef607c 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -26,36 +26,39 @@ namespace storm { namespace adapters { -ExplicitModelAdapter::ExplicitModelAdapter(storm::ir::Program program) : program(program), - booleanVariables(), integerVariables(), booleanVariableToIndexMap(), integerVariableToIndexMap(), - allStates(), stateToIndexMap(), numberOfTransitions(0), numberOfChoices(0), transitionRewards(nullptr), transitionMap() { - this->initializeVariables(); - storm::settings::Settings* s = storm::settings::instance(); - this->precision = s->get("precision"); -} - -ExplicitModelAdapter::~ExplicitModelAdapter() { - this->clearInternalState(); -} - - std::shared_ptr> ExplicitModelAdapter::getModel(std::string const & rewardModelName) { + ExplicitModelAdapter::ExplicitModelAdapter(storm::ir::Program program) : program(program), + booleanVariables(), integerVariables(), booleanVariableToIndexMap(), integerVariableToIndexMap(), + allStates(), stateToIndexMap(), numberOfTransitions(0), numberOfChoices(0), transitionRewards(nullptr), transitionMap() { + // Get variables from program. + this->initializeVariables(); + storm::settings::Settings* s = storm::settings::instance(); + this->precision = s->get("precision"); + } + ExplicitModelAdapter::~ExplicitModelAdapter() { + this->clearInternalState(); + } + std::shared_ptr> ExplicitModelAdapter::getModel(std::string const & rewardModelName) { + // Initialize rewardModel. + this->rewardModel = nullptr; + if (rewardModelName != "") { + this->rewardModel = std::unique_ptr(new storm::ir::RewardModel(this->program.getRewardModel(rewardModelName))); + } + + // State expansion, build temporary map, compute transition rewards. this->buildTransitionMap(); - + + // Compute labeling. std::shared_ptr stateLabeling = this->getStateLabeling(this->program.getLabels()); + + // Compute state rewards. std::shared_ptr> stateRewards = nullptr; - - this->rewardModel = nullptr; - if (rewardModelName != "") { - this->rewardModel = std::unique_ptr(new storm::ir::RewardModel(this->program.getRewardModel(rewardModelName)));; - if (this->rewardModel != nullptr) { - if (this->rewardModel->hasStateRewards()) { - stateRewards = this->getStateRewards(this->rewardModel->getStateRewards()); - } - } + if ((this->rewardModel != nullptr) && this->rewardModel->hasStateRewards()) { + stateRewards = this->getStateRewards(this->rewardModel->getStateRewards()); } + // Build and return actual model. switch (this->program.getModelType()) { case storm::ir::Program::DTMC: @@ -107,8 +110,10 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { std::shared_ptr> ExplicitModelAdapter::getStateRewards(std::vector const & rewards) { std::shared_ptr> results(new std::vector(this->allStates.size())); for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { + (*results)[index] = 0; for (auto reward: rewards) { - (*results)[index] = reward.getReward(this->allStates[index]); + // Add this reward to the state. + (*results)[index] += reward.getReward(this->allStates[index]); } } return results; @@ -116,11 +121,13 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { std::shared_ptr ExplicitModelAdapter::getStateLabeling(std::map> labels) { std::shared_ptr results(new storm::models::AtomicPropositionsLabeling(this->allStates.size(), labels.size())); + // Initialize labeling. for (auto it: labels) { results->addAtomicProposition(it.first); } for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { for (auto label: labels) { + // Add label to state, if guard is true. if (label.second->getValueAsBool(this->allStates[index])) { results->addAtomicPropositionToState(label.first, index); } @@ -132,6 +139,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { void ExplicitModelAdapter::initializeVariables() { uint_fast64_t numberOfIntegerVariables = 0; uint_fast64_t numberOfBooleanVariables = 0; + // Count number of variables. for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables(); numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables(); @@ -140,6 +148,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { this->booleanVariables.resize(numberOfBooleanVariables); this->integerVariables.resize(numberOfIntegerVariables); + // Create variables. for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { storm::ir::Module const& module = program.getModule(i); diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index d9b66de5f..a69d7382c 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -53,17 +53,25 @@ public: class ExplicitModelAdapter { public: + /*! + * Initialize adapter with given program. + */ ExplicitModelAdapter(storm::ir::Program program); ~ExplicitModelAdapter(); + /*! + * Convert program to an AbstractModel. + * The model will be of the type specified in the program. + * The model will contain rewards that are specified by the given reward model. + * @param rewardModelName Name of reward model to be added to the model. + * @return Model resulting from the program. + */ std::shared_ptr> getModel(std::string const & rewardModelName = ""); private: double precision; - // First some generic routines to operate on states. - /*! * Set some boolean variable in the given state object. * @param state State to be changed. @@ -78,6 +86,11 @@ private: * @param value New value. */ static void setValue(StateType* const state, uint_fast64_t const index, int_fast64_t const value); + /*! + * Transforms a state into a somewhat readable string. + * @param state State. + * @return String representation of the state. + */ static std::string toString(StateType const * const state); /*! * Apply an update to the given state and return the resulting new state object. @@ -103,7 +116,18 @@ private: */ void initializeVariables(); + /*! + * Calculate state reward for every reachable state based on given reward models. + * @param rewards List of state reward models. + * @return Reward for every state. + */ std::shared_ptr> getStateRewards(std::vector const & rewards); + + /*! + * Determines the labels for every reachable state, based on a list of available labels. + * @param labels Mapping from label names to boolean expressions. + * @returns The resulting labeling. + */ std::shared_ptr getStateLabeling(std::map> labels); /*! @@ -168,29 +192,41 @@ private: std::shared_ptr> buildNondeterministicMatrix(); /*! - * Build matrix from model. Starts with all initial states and explores the reachable state space. - * While exploring, the transitions are stored in a temporary map. - * Afterwards, we transform this map into the actual matrix. - * @return result matrix. + * Generate internal transition map from given model. + * Starts with all initial states and explores the reachable state space. */ void buildTransitionMap(); + /*! + * Clear all members that are initialized during the computation. + */ void clearInternalState(); // Program that should be converted. storm::ir::Program program; + // List of all boolean variables. std::vector booleanVariables; + // List of all integer variables. std::vector integerVariables; + // Maps boolean variable names to their index. std::map booleanVariableToIndexMap; + // Maps integer variable names to their index. std::map integerVariableToIndexMap; - // Members that are filled during the conversion. + //// Members that are filled during the conversion. + // Selected reward model. std::unique_ptr rewardModel; + // List of all reachable states. std::vector allStates; + // Maps states to their index (within allStates). std::unordered_map stateToIndexMap; + // Number of transitions. uint_fast64_t numberOfTransitions; + // Number of choices. (Is number of rows in matrix of nondeterministic model.) uint_fast64_t numberOfChoices; - std::shared_ptr> choiceIndices; + // Number of choices for each state. + std::shared_ptr> choiceIndices; + // Rewards for transitions. std::shared_ptr> transitionRewards; /*! diff --git a/src/parser/prismparser/BaseGrammar.h b/src/parser/prismparser/BaseGrammar.h index 345a377e0..e0c5d4df8 100644 --- a/src/parser/prismparser/BaseGrammar.h +++ b/src/parser/prismparser/BaseGrammar.h @@ -16,11 +16,23 @@ 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& 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 state = nullptr) { if (BaseGrammar::instanceObject == nullptr) { BaseGrammar::instanceObject = std::shared_ptr(new T(state)); @@ -29,26 +41,55 @@ namespace prism { 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(const bool value) { return std::shared_ptr(new BooleanLiteral(value)); } + /*! + * Create a new double literal with the given value. + * @param value Value of the literal. + * @returns Double literal. + */ std::shared_ptr createDoubleLiteral(const double value) { return std::shared_ptr(new DoubleLiteral(value)); } + /*! + * Create a new integer literal with the given value. + * @param value Value of the literal. + * @returns Integer literal. + */ std::shared_ptr createIntLiteral(const int_fast64_t value) { return std::shared_ptr(new IntegerLiteral(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(const std::shared_ptr left, bool addition, const std::shared_ptr right, BaseExpression::ReturnType type) { if (addition) { return std::shared_ptr(new BinaryNumericalFunctionExpression(type, left, right, BinaryNumericalFunctionExpression::PLUS)); @@ -56,16 +97,43 @@ namespace prism { return std::shared_ptr(new BinaryNumericalFunctionExpression(type, left, right, 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(const std::shared_ptr left, bool addition, const std::shared_ptr 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(const std::shared_ptr left, bool addition, const std::shared_ptr 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(const std::shared_ptr left, const std::shared_ptr right) { return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::int_, left, right, 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(const std::shared_ptr left, bool multiplication, const std::shared_ptr right) { if (multiplication) { return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::TIMES)); @@ -73,29 +141,69 @@ namespace prism { return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::DIVIDE)); } } - + /*! + * 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 left, BinaryRelationExpression::RelationType relationType, std::shared_ptr right) { return std::shared_ptr(new BinaryRelationExpression(left, right, relationType)); } + /*! + * Create a new negation expression. + * @param child Expression to be negated. + * @returns Negation expression. + */ std::shared_ptr createNot(std::shared_ptr child) { return std::shared_ptr(new UnaryBooleanFunctionExpression(child, 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 left, std::shared_ptr right) { //std::cerr << "Creating " << left->toString() << " & " << right->toString() << std::endl; return std::shared_ptr(new BinaryBooleanFunctionExpression(left, right, 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 left, std::shared_ptr right) { return std::shared_ptr(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::OR)); } + /*! + * Retrieve boolean variable by name. + * @param name Variable name. + * @returns Boolean variable. + */ std::shared_ptr getBoolVariable(const std::string name) { return state->getBooleanVariable(name); } + /*! + * Retrieve integer variable by name. + * @param name Variable name. + * @returns Integer variable. + */ std::shared_ptr getIntVariable(const std::string name) { return state->getIntegerVariable(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: diff --git a/src/parser/prismparser/BooleanExpressionGrammar.h b/src/parser/prismparser/BooleanExpressionGrammar.h index 9e976e64d..4f94dffbf 100644 --- a/src/parser/prismparser/BooleanExpressionGrammar.h +++ b/src/parser/prismparser/BooleanExpressionGrammar.h @@ -19,9 +19,16 @@ 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& 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: @@ -33,6 +40,9 @@ private: qi::rule(), Skipper> relativeExpression; qi::rule(), Skipper> booleanVariableExpression; + /*! + * Parser relation operators. + */ storm::parser::prism::relationalOperatorStruct relations_; }; diff --git a/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp b/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp index 203894638..ffa0b219b 100644 --- a/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp +++ b/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp @@ -6,47 +6,31 @@ namespace storm { namespace parser { namespace prism { - std::shared_ptr ConstBooleanExpressionGrammar::createRelation(std::shared_ptr left, BinaryRelationExpression::RelationType relationType, std::shared_ptr right) { - return std::shared_ptr(new BinaryRelationExpression(left, right, relationType)); - } - std::shared_ptr ConstBooleanExpressionGrammar::createNot(std::shared_ptr child) { - return std::shared_ptr(new UnaryBooleanFunctionExpression(child, UnaryBooleanFunctionExpression::NOT)); - } - std::shared_ptr ConstBooleanExpressionGrammar::createAnd(std::shared_ptr left, std::shared_ptr right) { - return std::shared_ptr(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::AND)); - } - std::shared_ptr ConstBooleanExpressionGrammar::createOr(std::shared_ptr left, std::shared_ptr right) { - return std::shared_ptr(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::OR)); - } - std::shared_ptr ConstBooleanExpressionGrammar::createLiteral(const bool value) { - return std::shared_ptr(new BooleanLiteral(value)); - } - ConstBooleanExpressionGrammar::ConstBooleanExpressionGrammar(std::shared_ptr& 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(&ConstBooleanExpressionGrammar::createOr, this, qi::_val, qi::_1)]; + 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(&ConstBooleanExpressionGrammar::createAnd, this, qi::_val, qi::_1)]; + 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(&ConstBooleanExpressionGrammar::createNot, this, qi::_1)]; + 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 | 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(&ConstBooleanExpressionGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)]; + 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(&ConstBooleanExpressionGrammar::createLiteral, this, qi::_1)]; + 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 index 4c8a5f7fb..f47c95bb5 100644 --- a/src/parser/prismparser/ConstBooleanExpressionGrammar.h +++ b/src/parser/prismparser/ConstBooleanExpressionGrammar.h @@ -17,6 +17,9 @@ 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& state); @@ -33,12 +36,6 @@ private: qi::rule(), Skipper> booleanLiteralExpression; storm::parser::prism::relationalOperatorStruct relations_; - - std::shared_ptr createRelation(std::shared_ptr left, BinaryRelationExpression::RelationType relationType, std::shared_ptr right); - std::shared_ptr createNot(std::shared_ptr child); - std::shared_ptr createAnd(std::shared_ptr left, std::shared_ptr right); - std::shared_ptr createOr(std::shared_ptr left, std::shared_ptr right); - std::shared_ptr createLiteral(const bool value); }; diff --git a/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp b/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp index ddd1341f5..1927909e1 100644 --- a/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp +++ b/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp @@ -4,25 +4,6 @@ namespace storm { namespace parser { namespace prism { - - std::shared_ptr ConstDoubleExpressionGrammar::createLiteral(double value) { - return std::shared_ptr(new DoubleLiteral(value)); - } - std::shared_ptr ConstDoubleExpressionGrammar::createPlus(const std::shared_ptr left, bool addition, const std::shared_ptr right) { - if (addition) { - return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::PLUS)); - } else { - return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::MINUS)); - } - } - std::shared_ptr ConstDoubleExpressionGrammar::createMult(const std::shared_ptr left, bool multiplication, const std::shared_ptr right) { - if (multiplication) { - return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::TIMES)); - } else { - return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::DIVIDE)); - } - } - ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr& state) : ConstDoubleExpressionGrammar::base_type(constantDoubleExpression), BaseGrammar(state) { @@ -30,11 +11,11 @@ ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantDoubleMultExpression) - [qi::_val = phoenix::bind(&ConstDoubleExpressionGrammar::createPlus, this, qi::_val, qi::_a, qi::_1)]; + [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(&ConstDoubleExpressionGrammar::createMult, this, qi::_val, qi::_a, qi::_1)]; + [qi::_val = phoenix::bind(&BaseGrammar::createDoubleMult, this, qi::_val, qi::_a, qi::_1)]; constantDoubleMultExpression.name("constant double expression"); constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression); @@ -43,7 +24,7 @@ ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptrstate->doubleConstants_ | this->state->integerConstants_ | doubleLiteralExpression); doubleConstantExpression.name("double constant or literal"); - doubleLiteralExpression = qi::double_[qi::_val = phoenix::bind(&ConstDoubleExpressionGrammar::createLiteral, this, qi::_1)]; + 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 index 9d70f9877..a964ec367 100644 --- a/src/parser/prismparser/ConstDoubleExpressionGrammar.h +++ b/src/parser/prismparser/ConstDoubleExpressionGrammar.h @@ -16,11 +16,13 @@ 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& state); - private: qi::rule(), Skipper, Unused> constantDoubleExpression; qi::rule(), qi::locals, Skipper> constantDoublePlusExpression; @@ -28,10 +30,6 @@ private: qi::rule(), Skipper> constantAtomicDoubleExpression; qi::rule(), Skipper> doubleConstantExpression; qi::rule(), Skipper> doubleLiteralExpression; - - std::shared_ptr createLiteral(double value); - std::shared_ptr createPlus(const std::shared_ptr left, bool addition, const std::shared_ptr right); - std::shared_ptr createMult(const std::shared_ptr left, bool multiplication, const std::shared_ptr right); }; diff --git a/src/parser/prismparser/ConstIntegerExpressionGrammar.h b/src/parser/prismparser/ConstIntegerExpressionGrammar.h index 847892e10..c7360553e 100644 --- a/src/parser/prismparser/ConstIntegerExpressionGrammar.h +++ b/src/parser/prismparser/ConstIntegerExpressionGrammar.h @@ -16,6 +16,9 @@ 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& state); diff --git a/src/parser/prismparser/IdentifierGrammars.h b/src/parser/prismparser/IdentifierGrammars.h index 936ee732a..5305cf277 100644 --- a/src/parser/prismparser/IdentifierGrammars.h +++ b/src/parser/prismparser/IdentifierGrammars.h @@ -16,13 +16,19 @@ 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& 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& state); diff --git a/src/parser/prismparser/IntegerExpressionGrammar.h b/src/parser/prismparser/IntegerExpressionGrammar.h index 0f44b0d01..5bc842192 100644 --- a/src/parser/prismparser/IntegerExpressionGrammar.h +++ b/src/parser/prismparser/IntegerExpressionGrammar.h @@ -19,9 +19,17 @@ 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& 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: diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index ced118dce..7189c8a03 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -63,19 +63,19 @@ void PrismGrammar::addBoolAssignment(const std::string& variable, std::shared_pt } Module PrismGrammar::renameModule(const std::string& name, const std::string& oldname, std::map& mapping) { this->state->moduleNames_.add(name, name); - Module* old = this->state->moduleMap_.find(oldname); + Module* old = this->moduleMap_.find(oldname); if (old == nullptr) { LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldname << " does not exist!"); throw "Renaming module failed"; } Module res(*old, name, mapping, this->state); - this->state->moduleMap_.at(name) = res; + this->moduleMap_.at(name) = res; return res; } Module PrismGrammar::createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector commands) { this->state->moduleNames_.add(name, name); Module res(name, bools, ints, boolids, intids, commands); - this->state->moduleMap_.at(name) = res; + this->moduleMap_.at(name) = res; return res; } diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h index 5844659be..a512befb9 100644 --- a/src/parser/prismparser/PrismGrammar.h +++ b/src/parser/prismparser/PrismGrammar.h @@ -54,6 +54,7 @@ public: private: std::shared_ptr state; + struct qi::symbols moduleMap_; // The starting point of the grammar. qi::rule< diff --git a/src/parser/prismparser/Tokens.h b/src/parser/prismparser/Tokens.h index bd246d358..bbf7e8418 100644 --- a/src/parser/prismparser/Tokens.h +++ b/src/parser/prismparser/Tokens.h @@ -12,9 +12,10 @@ 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. + /*! + * 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 @@ -27,7 +28,9 @@ namespace prism { }; - // A structure defining the keywords that are not allowed to be chosen as identifiers. + /*! + * A structure defining the keywords that are not allowed to be chosen as identifiers. + */ struct keywordsStruct : qi::symbols { keywordsStruct() { add @@ -48,8 +51,10 @@ namespace prism { } }; - // A structure mapping the textual representation of a binary relation to the representation - // of the intermediate representation. + /*! + * A structure mapping the textual representation of a binary relation to the representation + * of the intermediate representation. + */ struct relationalOperatorStruct : qi::symbols { relationalOperatorStruct() { add diff --git a/src/parser/prismparser/VariableState.h b/src/parser/prismparser/VariableState.h index 620c029ff..1d13cc270 100644 --- a/src/parser/prismparser/VariableState.h +++ b/src/parser/prismparser/VariableState.h @@ -23,43 +23,104 @@ using namespace storm::ir::expressions; template std::ostream& operator<<(std::ostream& out, qi::symbols& symbols); +/*! + * This class contains the state that is needed during the parsing of a prism model. + */ struct VariableState : public storm::ir::VariableAdder { -public: VariableState(bool firstRun = true); - -public: + + /*! + * Indicator, if we are still in the first run. + */ bool firstRun; + /*! + * A parser for all reserved keywords. + */ keywordsStruct keywords; - // Used for indexing the variables. + /*! + * Internal counter for the index of the next new boolean variable. + */ uint_fast64_t nextBooleanVariableIndex; + /*! + * Internal counter for the index of the next new integer variable. + */ uint_fast64_t nextIntegerVariableIndex; // 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_; - struct qi::symbols moduleMap_; // A structure representing the identity function over identifier names. struct variableNamesStruct : qi::symbols { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_, localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_; -public: + + /*! + * Add a new boolean variable with the given name. + * @param name Name of the variable. + * @return Index of the variable. + */ uint_fast64_t addBooleanVariable(const std::string& name); + /*! + * Add a new integer variable with the given name and constraints. + * @param name Name of the variable. + * @param lower Lower bound for the variable value. + * @param upper Upper bound for the variable value. + * @return Index of the variable. + */ uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper); + /*! + * Retrieve boolean Variable with given name. + * @param name Variable name. + * @returns Variable. + */ std::shared_ptr getBooleanVariable(const std::string& name); + /*! + * Retrieve integer Variable with given name. + * @param name Variable name. + * @returns Variable. + */ std::shared_ptr getIntegerVariable(const std::string& name); + /*! + * Retrieve any Variable with given name. + * @param name Variable name. + * @returns Variable. + */ std::shared_ptr getVariable(const std::string& name); + /*! + * Perform operations necessary for a module renaming. + * This includes creating new variables and constants. + * @param renaming String mapping for renaming operation. + */ void performRenaming(const std::map& renaming); + /*! + * Start with a new module. + * Clears sets of local variables. + */ void startModule(); + /*! + * Check if given string is a free identifier. + * @param s String. + * @returns If s is a free identifier. + */ bool isFreeIdentifier(std::string& s) const; + /*! + * Check if given string is a valid identifier. + * @param s String. + * @returns If s is a valid identifier. + */ bool isIdentifier(std::string& s) const; + /*! + * Prepare state to proceed to second parser run. + * Clears constants. + */ void prepareForSecondRun(); };