From 7610bc8e76d5927f02693d2bb01dca0fa216733d Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 8 Apr 2014 20:52:15 +0200 Subject: [PATCH] Started reducing the complexity in the PRISM grammar. Former-commit-id: c17dc6d27bf1ca822cbe7510825b2f5aa9c9e1a8 --- src/parser/prismparser/PrismGrammar.cpp | 285 +++++++--------------- src/parser/prismparser/PrismGrammar.h | 207 +++++----------- src/parser/prismparser/Tokens.h | 79 ++++-- src/storage/expressions/Expression.h | 2 +- src/storage/expressions/Expressions.h | 13 + src/storage/prism/Program.cpp | 8 +- src/storage/prism/Program.h | 17 +- src/storage/prism/Update.cpp | 63 ++--- src/storage/prism/Update.h | 48 +--- test/functional/parser/ParsePrismTest.cpp | 32 --- 10 files changed, 269 insertions(+), 485 deletions(-) create mode 100644 src/storage/expressions/Expressions.h delete mode 100644 test/functional/parser/ParsePrismTest.cpp diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index b6de4f0f4..7c81b31ce 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -1,152 +1,96 @@ -/* - * PrismGrammar.cpp - * - * Created on: 11.01.2013 - * Author: chris - */ - -// Needed for file IO. -#include -#include -#include - -#include "PrismGrammar.h" - -#include "src/utility/OsDetection.h" - -#include "src/parser/prismparser/Includes.h" -#include "src/parser/prismparser/BooleanExpressionGrammar.h" -#include "src/parser/prismparser/ConstBooleanExpressionGrammar.h" -#include "src/parser/prismparser/ConstDoubleExpressionGrammar.h" -#include "src/parser/prismparser/ConstIntegerExpressionGrammar.h" -#include "src/parser/prismparser/IntegerExpressionGrammar.h" -#include "src/parser/prismparser/IdentifierGrammars.h" -#include "src/parser/prismparser/VariableState.h" +#include "src/parser/prismparser/PrismGrammar.h" #include "src/exceptions/InvalidArgumentException.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - -// Some typedefs and namespace definitions to reduce code size. -typedef std::string::const_iterator BaseIteratorType; -typedef boost::spirit::classic::position_iterator2 PositionIteratorType; -namespace qi = boost::spirit::qi; -namespace phoenix = boost::phoenix; - namespace storm { namespace parser { namespace prism { - - void PrismGrammar::addLabel(std::string const& name, std::shared_ptr const& value, std::map>& nameToExpressionMap) { - this->state->labelNames_.add(name, name); - nameToExpressionMap[name] = value->clone(); - } - - void PrismGrammar::addIntegerAssignment(std::string const& variable, std::shared_ptr const& value, std::map& variableToAssignmentMap) { - this->state->assignedIntegerVariables_.add(variable, variable); - variableToAssignmentMap[variable] = Assignment(variable, value->clone()); - } - - void PrismGrammar::addBooleanAssignment(std::string const& variable, std::shared_ptr const& value, std::map& variableToAssigmentMap) { - this->state->assignedBooleanVariables_.add(variable, variable); - variableToAssigmentMap[variable] = Assignment(variable, value->clone()); - } - - void PrismGrammar::addUndefinedBooleanConstant(std::string const& name, std::map>& nameToExpressionMap) { - this->state->booleanConstants_.add(name, std::shared_ptr(new BooleanConstantExpression(name))); - this->state->allConstantNames_.add(name, name); - nameToExpressionMap.emplace(name, std::unique_ptr(new BooleanConstantExpression(dynamic_cast(*this->state->booleanConstants_.at(name))))); - } - - void PrismGrammar::addUndefinedIntegerConstant(std::string const& name, std::map>& nameToExpressionMap) { - this->state->integerConstants_.add(name, std::shared_ptr(new IntegerConstantExpression(name))); - this->state->allConstantNames_.add(name, name); - nameToExpressionMap.emplace(name, std::unique_ptr(new IntegerConstantExpression(dynamic_cast(*this->state->integerConstants_.at(name))))); - } - - void PrismGrammar::addUndefinedDoubleConstant(std::string const& name, std::map>& nameToExpressionMap) { - this->state->doubleConstants_.add(name, std::shared_ptr(new DoubleConstantExpression(name))); - this->state->allConstantNames_.add(name, name); - nameToExpressionMap.emplace(name, std::unique_ptr(new DoubleConstantExpression(dynamic_cast(*this->state->doubleConstants_.at(name))))); - } - - Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map const& renaming) { - this->state->moduleNames_.add(newName, newName); - Module* old = this->moduleMap_.find(oldName); - if (old == nullptr) { - LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldName << " does not exist."); - throw storm::exceptions::InvalidArgumentException() << "Renaming module failed: module " << oldName << " does not exist."; - } - Module res(*old, newName, renaming, *this->state); - this->moduleMap_.at(newName) = res; - return res; - } - - Module PrismGrammar::createModule(std::string const& name, std::vector const& bools, std::vector const& ints, std::map const& boolids, std::map const& intids, std::vector const& commands) { - this->state->moduleNames_.add(name, name); - Module res(name, bools, ints, boolids, intids, commands); - this->moduleMap_.at(name) = res; - return res; - } - - void PrismGrammar::createIntegerVariable(std::string const& name, std::shared_ptr const& lower, std::shared_ptr const& upper, std::shared_ptr const& init, std::vector& vars, std::map& varids, bool isGlobalVariable) { - uint_fast64_t id = this->state->addIntegerVariable(name); - uint_fast64_t newLocalIndex = this->state->nextLocalIntegerVariableIndex; - vars.emplace_back(newLocalIndex, id, name, lower != nullptr ? lower->clone() : nullptr, upper != nullptr ? upper->clone() : nullptr, init != nullptr ? init->clone() : nullptr); - varids[name] = newLocalIndex; - ++this->state->nextLocalIntegerVariableIndex; - this->state->localIntegerVariables_.add(name, name); - if (isGlobalVariable) { - this->state->globalIntegerVariables_.add(name, name); - } - } - - void PrismGrammar::createBooleanVariable(std::string const& name, std::shared_ptr const& init, std::vector& vars, std::map& varids, bool isGlobalVariable) { - uint_fast64_t id = this->state->addBooleanVariable(name); - uint_fast64_t newLocalIndex = this->state->nextLocalBooleanVariableIndex; - vars.emplace_back(newLocalIndex, id, name, init != nullptr ? init->clone() : nullptr); - varids[name] = newLocalIndex; - ++this->state->nextLocalBooleanVariableIndex; - this->state->localBooleanVariables_.add(name, name); - if (isGlobalVariable) { - this->state->globalBooleanVariables_.add(name, name); - } - } - - StateReward createStateReward(std::shared_ptr const& guard, std::shared_ptr const& reward) { - return StateReward(guard->clone(), reward->clone()); - } - TransitionReward createTransitionReward(std::string const& label, std::shared_ptr const& guard, std::shared_ptr const& reward) { - return TransitionReward(label, guard->clone(), reward->clone()); - } - void createRewardModel(std::string const& name, std::vector& stateRewards, std::vector& transitionRewards, std::map& mapping) { - mapping[name] = RewardModel(name, stateRewards, transitionRewards); - } - Update PrismGrammar::createUpdate(std::shared_ptr const& likelihood, std::map const& bools, std::map const& ints) { - this->state->nextGlobalUpdateIndex++; - return Update(this->state->getNextGlobalUpdateIndex() - 1, likelihood != nullptr ? likelihood->clone() : nullptr, bools, ints); - } - Command PrismGrammar::createCommand(std::string const& label, std::shared_ptr const& guard, std::vector const& updates) { - this->state->nextGlobalCommandIndex++; - return Command(this->state->getNextGlobalCommandIndex() - 1, label, guard->clone(), updates); - } - Program createProgram( - Program::ModelType modelType, - std::map> const& undefBoolConst, - std::map> const& undefIntConst, - std::map> const& undefDoubleConst, - GlobalVariableInformation const& globalVariableInformation, - std::vector const& modules, - std::map const& rewards, - std::map> const& labels) { - return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst, - globalVariableInformation.booleanVariables, globalVariableInformation.integerVariables, - globalVariableInformation.booleanVariableToIndexMap, - globalVariableInformation.integerVariableToIndexMap, modules, rewards, labels); - } - - PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new VariableState()) { + PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start) { + // Parse simple identifier. + identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]] - keywords_; + identifier.name("identifier"); + + // Parse a composed expression. + expression %= (booleanExpression | numericalExpression); + expression.name("expression"); + + booleanExpression %= orExpression; + expression.name("boolean expression"); + + orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = qi::_val * qi::_1]; + orExpression.name("boolean expression"); + + andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = qi::_val * qi::_1]; + andExpression.name("boolean expression"); + + notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = !qi::_1]; + notExpression.name("boolean expression"); + + atomicBooleanExpression %= relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")"); + atomicBooleanExpression.name("boolean expression"); + + relativeExpression = ((numericalExpression >> ">") > numericalExpression)[qi::_val = qi::_1 > qi::_2] | ((numericalExpression >> ">=") > numericalExpression)[qi::_val = qi::_1 >= qi::_2] | ((numericalExpression >> "<") > numericalExpression)[qi::_val = qi::_1 < qi::_2] | ((numericalExpression >> "<=") > numericalExpression)[qi::_val = qi::_1 <= qi::_2]; + relativeExpression.name("relative expression"); + + booleanVariableExpression = identifier[qi::_val = phoenix::bind(&storm::expressions::Expression::createBooleanVariable, qi::_1)]; + booleanVariableExpression.name("boolean variable"); + + numericalExpression %= plusExpression; + numericalExpression.name("numerical expression"); + + plusExpression = multiplicationExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> multiplicationExpression)[phoenix::if_(qi::_a) [qi::_val = qi::_val + qi::_1] .else_ [qi::_val = qi::_val - qi::_1]]; + plusExpression.name("numerical expression"); + + multiplicationExpression = atomicNumericalExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicNumericalExpression[qi::_val = qi::_val * qi::_1]); + multiplicationExpression.name("numerical expression"); + + atomicNumericalExpression %= minMaxExpression | floorCeilExpression | numericalVariableExpression | qi::lit("(") >> numericalExpression >> qi::lit(")"); + atomicNumericalExpression.name("numerical expression"); + + minMaxExpression %= ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> numericalExpression >> qi::lit(",") >> numericalExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&storm::expressions::Expression::minimum, qi::_1, qi::_2)] .else_ [qi::_val = phoenix::bind(&storm::expressions::Expression::maximum, qi::_1, qi::_2)]]; + minMaxExpression.name("min/max expression"); + + floorCeilExpression %= ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> numericalExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&storm::expressions::Expression::floor, qi::_1)] .else_ [qi::_val = phoenix::bind(&storm::expressions::Expression::ceil, qi::_1)]]; + floorCeilExpression.name("integer floor/ceil expression"); + + numericalVariableExpression = identifier[qi::_val = phoenix::bind(&storm::expressions::Expression::createDoubleVariable, qi::_1)]; + numericalVariableExpression.name("numerical variable"); + + // Parse a model type. + modelTypeDefinition = modelType_; + modelTypeDefinition.name("model type"); + + // This block defines all entities that are needed for parsing constant definitions. + definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=") > expression > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedBooleanConstantDefinition.name("defined boolean constant declaration"); + + definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedIntegerConstantDefinition.name("defined integer constant declaration"); + definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedDoubleConstantDefinition.name("defined double constant declaration"); + undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedBooleanConstant, this, qi::_1, qi::_r1)]; + undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); + undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedIntegerConstant, this, qi::_1, qi::_r1)]; + undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); + undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedDoubleConstant, this, qi::_1, qi::_r1)]; + undefinedDoubleConstantDefinition.name("undefined double constant definition"); + definedConstantDefinition %= (definedBooleanConstantDefinition(qi::_r1) | definedIntegerConstantDefinition(qi::_r2) | definedDoubleConstantDefinition(qi::_r3)); + definedConstantDefinition.name("defined constant definition"); + undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); + undefinedConstantDefinition.name("undefined constant definition"); + constantDefinitionList = *(undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3) | definedConstantDefinition(qi::_r4, qi::_r5, qi::_r6)); + constantDefinitionList.name("constant definition list"); + + // Parse the ingredients of a probabilistic program. + start = (qi::eps > + modelTypeDefinition > + constantDefinitionList(qi::_a, qi::_b, qi::_c, qi::_d, qi::_e, qi::_f) > + formulaDefinitionList > + globalVariableDefinitionList(qi::_d) > + moduleDefinitionList > + rewardDefinitionList(qi::_e) > + labelDefinitionList(qi::_f))[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2, qi::_e, qi::_f)]; + start.name("probabilistic program declaration"); + labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> FreeIdentifierGrammar::instance(this->state) >> -qi::lit("\"") >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";")) [phoenix::bind(&PrismGrammar::addLabel, this, qi::_1, qi::_2, qi::_r1)]; @@ -222,26 +166,6 @@ namespace storm { globalVariableDefinitionList = *(qi::lit("global") > (booleanVariableDefinition(bind(&GlobalVariableInformation::booleanVariables, qi::_r1), bind(&GlobalVariableInformation::booleanVariableToIndexMap, qi::_r1), true) | integerVariableDefinition(bind(&GlobalVariableInformation::integerVariables, qi::_r1), bind(&GlobalVariableInformation::integerVariableToIndexMap, qi::_r1), true))); globalVariableDefinitionList.name("global variable declaration list"); - // This block defines all entities that are needed for parsing constant definitions. - definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstBooleanExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; - definedBooleanConstantDefinition.name("defined boolean constant declaration"); - definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; - definedIntegerConstantDefinition.name("defined integer constant declaration"); - definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; - definedDoubleConstantDefinition.name("defined double constant declaration"); - undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedBooleanConstant, this, qi::_1, qi::_r1)]; - undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); - undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedIntegerConstant, this, qi::_1, qi::_r1)]; - undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); - undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedDoubleConstant, this, qi::_1, qi::_r1)]; - undefinedDoubleConstantDefinition.name("undefined double constant declaration"); - definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); - definedConstantDefinition.name("defined constant declaration"); - undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); - undefinedConstantDefinition.name("undefined constant declaration"); - constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)); - constantDefinitionList.name("constant declaration list"); - constantBooleanFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstBooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantBooleanFormulas_.add, qi::_1, qi::_2)]; constantBooleanFormulaDefinition.name("constant boolean formula definition"); booleanFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->booleanFormulas_.add, qi::_1, qi::_2)]; @@ -256,40 +180,7 @@ namespace storm { formulaDefinition.name("formula definition"); formulaDefinitionList = *formulaDefinition; formulaDefinitionList.name("formula definition list"); - - // This block defines all entities that are needed for parsing a program. - modelTypeDefinition = modelType_; - modelTypeDefinition.name("model type"); - start = (qi::eps > - modelTypeDefinition > - constantDefinitionList(qi::_a, qi::_b, qi::_c) > - formulaDefinitionList > - globalVariableDefinitionList(qi::_d) > - moduleDefinitionList > - rewardDefinitionList(qi::_e) > - labelDefinitionList(qi::_f))[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2, qi::_e, qi::_f)]; - start.name("probabilistic program declaration"); - } - - void PrismGrammar::prepareForSecondRun() { - LOG4CPLUS_INFO(logger, "Preparing parser for second run."); - this->state->prepareForSecondRun(); - BooleanExpressionGrammar::secondRun(); - ConstBooleanExpressionGrammar::secondRun(); - ConstDoubleExpressionGrammar::secondRun(); - ConstIntegerExpressionGrammar::secondRun(); - IntegerExpressionGrammar::secondRun(); - } - - void PrismGrammar::resetGrammars() { - LOG4CPLUS_INFO(logger, "Resetting grammars."); - BooleanExpressionGrammar::resetInstance(); - ConstBooleanExpressionGrammar::resetInstance(); - ConstDoubleExpressionGrammar::resetInstance(); - ConstIntegerExpressionGrammar::resetInstance(); - IntegerExpressionGrammar::resetInstance(); } - } // namespace prism } // namespace parser } // namespace storm diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h index c73420057..77a5406fc 100644 --- a/src/parser/prismparser/PrismGrammar.h +++ b/src/parser/prismparser/PrismGrammar.h @@ -34,7 +34,7 @@ using namespace storm::expressions; namespace storm { namespace parser { namespace prism { - class PrismGrammar : public qi::grammar { + class PrismGrammar : public qi::grammar, std::set, std::set, std::map, std::map, std::map, std::map>, Skipper> { public: /*! * Default constructor that creates an empty and functional grammar. @@ -43,182 +43,89 @@ namespace storm { private: // The starting point of the grammar. - qi::rule start; + // The locals are used for: (a) undefined boolean constants, (b) undefined integer constants, (c) undefined double constants, (d) defined boolean constants, (e) defined integer constants, (f) defined double constants, (g) module name to module map + qi::rule, std::set, std::set, std::map, std::map, std::map, std::map>, Skipper> start; // Rules for model type. qi::rule modelTypeDefinition; - // Rules for global constant definitions. - qi::rule&, std::set&, std::set&, std::map&, std::map&, std::map&), Skipper> constantDefinitionList; - - // Rules for global variable definitions + // Rules for constant definitions. + qi::rule&, std::set&, std::set&, std::map&, std::map&, std::map&), Skipper> constantDefinitionList; + qi::rule&, std::set&, std::set&), Skipper> undefinedConstantDefinition; + qi::rule&, std::map&, std::map&), Skipper> definedConstantDefinition; + qi::rule&), Skipper> undefinedBooleanConstantDefinition; + qi::rule&), Skipper> undefinedIntegerConstantDefinition; + qi::rule&), Skipper> undefinedDoubleConstantDefinition; + qi::rule&), Skipper> definedBooleanConstantDefinition; + qi::rule&), Skipper> definedIntegerConstantDefinition; + qi::rule&), Skipper> definedDoubleConstantDefinition; + + // Rules for global variable definitions. qi::rule&, std::map), Skipper> globalVariableDefinitionList; // Rules for modules definition. qi::rule(), Skipper> moduleDefinitionList; - qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; - qi::rule>, Skipper> moduleRenaming; + qi::rule, std::map>, Skipper> moduleDefinition; + qi::rule&), qi::locals>, Skipper> moduleRenaming; // Rules for variable definitions. - qi::rule&, std::vector&, std::map&, std::map&), Skipper> variableDefinition; - qi::rule&, std::map&, bool), qi::locals>, Skipper> booleanVariableDefinition; - qi::rule&, std::map&, bool), qi::locals>, Skipper> integerVariableDefinition; + qi::rule&, std::map&), Skipper> variableDefinition; + qi::rule&), Skipper> booleanVariableDefinition; + qi::rule&), Skipper> integerVariableDefinition; // Rules for command definitions. qi::rule, Skipper> commandDefinition; qi::rule(), Skipper> updateListDefinition; - qi::rule, std::map>, Skipper> updateDefinition; - qi::rule&, std::map&), Skipper> assignmentDefinitionList; - qi::rule&, std::map&), Skipper> assignmentDefinition; - - // Rules for variable/command names. - qi::rule commandName; - qi::rule unassignedLocalBooleanVariableName; - qi::rule unassignedLocalIntegerVariableName; + qi::rule>, Skipper> updateDefinition; + qi::rule&), Skipper> assignmentDefinitionList; + qi::rule assignmentDefinition; // Rules for reward definitions. - qi::rule&), Skipper> rewardDefinitionList; + qi::rule(), Skipper> rewardDefinitionList; qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; qi::rule stateRewardDefinition; - qi::rule, Skipper> transitionRewardDefinition; + qi::rule transitionRewardDefinition; // Rules for label definitions. - qi::rule>&), Skipper> labelDefinitionList; - qi::rule>&), Skipper> labelDefinition; - - // Rules for constant definitions. - qi::rule(), Skipper> constantDefinition; - qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; - qi::rule(), Skipper> definedConstantDefinition; - qi::rule>&), Skipper> undefinedBooleanConstantDefinition; - qi::rule>&), Skipper> undefinedIntegerConstantDefinition; - qi::rule>&), Skipper> undefinedDoubleConstantDefinition; - qi::rule(), Skipper> definedBooleanConstantDefinition; - qi::rule(), Skipper> definedIntegerConstantDefinition; - qi::rule(), Skipper> definedDoubleConstantDefinition; + qi::rule(), Skipper> labelDefinitionList; + qi::rule&), Skipper> labelDefinition; // Rules for formula definitions. - qi::rule formulaDefinitionList; - qi::rule formulaDefinition; - qi::rule constantIntegerFormulaDefinition; - qi::rule integerFormulaDefinition; - qi::rule constantDoubleFormulaDefinition; - qi::rule constantBooleanFormulaDefinition; - qi::rule booleanFormulaDefinition; - - // Rules for variable recognition. - qi::rule(), Skipper> booleanVariableCreatorExpression; - qi::rule(), qi::locals>, Skipper> integerVariableCreatorExpression; - + qi::rule(), Skipper> formulaDefinitionList; + qi::rule&), Skipper> formulaDefinition; + + // Rules for identifier parsing. + qi::rule identifier; + + // Rules for parsing a composed expression. + qi::rule expression; + qi::rule booleanExpression; + qi::rule orExpression; + qi::rule andExpression; + qi::rule notExpression; + qi::rule atomicBooleanExpression; + qi::rule relativeExpression; + qi::rule booleanVariableExpression; + qi::rule numericalExpression; + qi::rule, Skipper> plusExpression; + qi::rule multiplicationExpression; + qi::rule atomicNumericalExpression; + qi::rule numericalVariableExpression; + qi::rule, Skipper> minMaxExpression; + qi::rule, Skipper> floorCeilExpression; + + // Parsers that recognize special keywords and operations. storm::parser::prism::keywordsStruct keywords_; 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_; + storm::parser::prism::BinaryRelationOperatorStruct relationOperator_; + storm::parser::prism::BinaryBooleanOperatorStruct binaryBooleanOperator_; + storm::parser::prism::UnaryBooleanOperatorStruct unaryBooleanOperator_; + storm::parser::prism::BinaryNumericalOperatorStruct binaryNumericalOperator_; + storm::parser::prism::UnaryNumericalOperatorStruct unaryNumericalOperator_; - /*! - * Adds a label with the given name and expression to the given label-to-expression map. - * - * @param name The name of the label. - * @param expression The expression associated with the label. - * @param nameToExpressionMap The map to which the label is added. - */ - void addLabel(std::string const& name, std::shared_ptr const& value, std::map>& nameToExpressionMap); - - /*! - * Adds a boolean assignment for the given variable with the given expression and adds it to the - * provided variable-to-assignment map. - * - * @param variable The name of the variable that the assignment targets. - * @param expression The expression that is assigned to the variable. - * @param variableToAssignmentMap The map to which the assignment is added. - */ - void addBooleanAssignment(std::string const& variable, std::shared_ptr const& expression, std::map& variableToAssignmentMap); - - /*! - * Adds a boolean assignment for the given variable with the given expression and adds it to the - * provided variable-to-assignment map. - * - * @param variable The name of the variable that the assignment targets. - * @param expression The expression that is assigned to the variable. - * @param variableToAssignmentMap The map to which the assignment is added. - */ - void addIntegerAssignment(std::string const& variable, std::shared_ptr const& expression, std::map& variableToAssignmentMap); - - void addUndefinedBooleanConstant(std::string const& name, std::map>& nameToExpressionMap); - - void addUndefinedIntegerConstant(std::string const& name, std::map>& nameToExpressionMap); - - void addUndefinedDoubleConstant(std::string const& name, std::map>& nameToExpressionMap); - - /*! - * Creates a module by renaming, i.e. takes the module given by the old name, creates a new module - * with the given name which renames all identifiers according to the given mapping. - * - * @param name The name of the new module. - * @param oldName The name of the module that is to be copied (modulo renaming). - * @param renaming A mapping from identifiers to their new names. - */ - Module renameModule(std::string const& name, std::string const& oldName, std::map const& renaming); - - /*! - * Creates a new module with the given name, boolean and integer variables and commands. - * - * @param name The name of the module to create. - * @param booleanVariables The boolean variables of the module. - * @param integerVariables The integer variables of the module. - * @param booleanVariableToLocalIndexMap A mapping of boolean variables to module-local indices. - * @param integerVariableToLocalIndexMap A mapping of boolean variables to module-local indices. - * @param commands The commands associated with this module. - */ - Module createModule(std::string const& name, std::vector const& booleanVariables, std::vector const& integerVariables, std::map const& booleanVariableToLocalIndexMap, std::map const& integerVariableToLocalIndexMap, std::vector const& commands); - - /*! - * Creates an integer variable with the given name, domain and initial value and adds it to the - * provided list of integer variables and the given mappings. - * - * @param name The name of the integer variable. - * @param lower The expression that defines the lower bound of the domain. - * @param upper The expression that defines the upper bound of the domain. - * @param init The expression that defines the initial value of the variable. - * @param integerVariableToGlobalIndexMap A mapping of integer variables to global indices. - * @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not. - */ - void createIntegerVariable(std::string const& name, std::shared_ptr const& lower, std::shared_ptr const& upper, std::shared_ptr const& init, std::vector& integerVariables, std::map& integerVariableToGlobalIndexMap, bool isGlobalVariable); - - /*! - * Creates an boolean variable with the given name and initial value and adds it to the - * provided list of boolean variables and the given mappings. - * - * @param name The name of the boolean variable. - * @param init The expression that defines the initial value of the variable. - * @param booleanVariableToGlobalIndexMap A mapping of boolean variables to global indices. - * @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not. - */ - void createBooleanVariable(std::string const& name, std::shared_ptr const& init, std::vector& booleanVariables, std::map& booleanVariableToGlobalIndexMap, bool isGlobalVariable); - - /*! - * Creates a command with the given label, guard and updates. - * - * @param label The label of the command. - * @param guard The guard of the command. - * @param updates The updates associated with the command. - */ - Command createCommand(std::string const& label, std::shared_ptr const& guard, std::vector const& updates); - - /*! - * Creates an update with the given likelihood and the given assignments to boolean and integer variables, respectively. - * - * @param likelihood The likelihood of this update being executed. - * @param booleanAssignments The assignments to boolean variables this update involves. - * @param integerAssignments The assignments to integer variables this update involves. - */ - Update createUpdate(std::shared_ptr const& likelihood, std::map const& booleanAssignments, std::map const& integerAssignments); + // Helper methods that add data to data structures. }; - - } // namespace prism } // namespace parser } // namespace storm diff --git a/src/parser/prismparser/Tokens.h b/src/parser/prismparser/Tokens.h index bcaefce7b..866bbbf24 100644 --- a/src/parser/prismparser/Tokens.h +++ b/src/parser/prismparser/Tokens.h @@ -1,7 +1,8 @@ #ifndef STORM_PARSER_PRISMPARSER_TOKENS_H_ #define STORM_PARSER_PRISMPARSER_TOKENS_H_ -#include "src/storage/expressions/Expression.h" +#include "src/storage/prism/Program.h" +#include "src/storage/expressions/Expressions.h" namespace storm { namespace parser { @@ -10,14 +11,14 @@ namespace storm { * A structure mapping the textual representation of a model type to the model type * representation of the intermediate representation. */ - struct modelTypeStruct : qi::symbols { + 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); + ("dtmc", storm::prism::Program::ModelType::DTMC) + ("ctmc", storm::prism::Program::ModelType::CTMC) + ("mdp", storm::prism::Program::ModelType::MDP) + ("ctmdp", storm::prism::Program::ModelType::CTMDP) + ("ma", storm::prism::Program::ModelType::MA); } }; @@ -45,17 +46,63 @@ namespace storm { }; /*! - * A structure mapping the textual representation of a binary relation. + * A structure mapping the textual representation of binary relations to the corresponding enum values. */ - struct relationalOperatorStruct : qi::symbols { - relationalOperatorStruct() { + struct BinaryRelationOperatorStruct : qi::symbols { + BinaryRelationOperatorStruct() { add - ("=", BinaryRelationExpression::RelationType::EQUAL) - ("!=", BinaryRelationExpression::RelationType::NOT_EQUAL) - ("<", BinaryRelationExpression::RelationType::LESS) - ("<=", BinaryRelationExpression::RelationType::LESS_OR_EQUAL) - (">", BinaryRelationExpression::RelationType::GREATER) - (">=", BinaryRelationExpression::RelationType::GREATER_OR_EQUAL); + ("=", storm::expressions::BinaryRelationExpression::RelationType::Equal) + ("!=", storm::expressions::BinaryRelationExpression::RelationType::NotEqual) + ("<", storm::expressions::BinaryRelationExpression::RelationType::Less) + ("<=", storm::expressions::BinaryRelationExpression::RelationType::LessOrEqual) + (">", storm::expressions::BinaryRelationExpression::RelationType::Greater) + (">=", storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual); + } + }; + + /*! + * A structure mapping the textual representation of binary operators to the corresponding enum values. + */ + struct BinaryBooleanOperatorStruct : qi::symbols { + BinaryBooleanOperatorStruct() { + add + ("&", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And) + ("|", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or) + ("=>", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies) + ("<=>", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff); + } + }; + + /*! + * A structure mapping the textual representation of binary operators to the corresponding enum values. + */ + struct UnaryBooleanOperatorStruct : qi::symbols { + UnaryBooleanOperatorStruct() { + add + ("!", storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not); + } + }; + + /*! + * A structure mapping the textual representation of binary boolean operators to the corresponding enum values. + */ + struct BinaryNumericalOperatorStruct : qi::symbols { + BinaryNumericalOperatorStruct() { + add + ("+", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus) + ("-", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Minus) + ("*", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Times) + ("/", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide); + } + }; + + /*! + * A structure mapping the textual representation of binary operators to the corresponding enum values. + */ + struct UnaryNumericalOperatorStruct : qi::symbols { + UnaryNumericalOperatorStruct() { + add + ("!", storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus); } }; } diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 875bcfbdc..e7768432d 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -1,7 +1,7 @@ #ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ #define STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ -#include +#include #include "src/storage/expressions/BaseExpression.h" diff --git a/src/storage/expressions/Expressions.h b/src/storage/expressions/Expressions.h new file mode 100644 index 000000000..09febb4a4 --- /dev/null +++ b/src/storage/expressions/Expressions.h @@ -0,0 +1,13 @@ +#include "src/storage/expressions/BinaryBooleanFunctionExpression.h" +#include "src/storage/expressions/BinaryNumericalFunctionExpression.h" +#include "src/storage/expressions/BinaryRelationExpression.h" +#include "src/storage/expressions/BooleanConstantExpression.h" +#include "src/storage/expressions/BooleanLiteralExpression.h" +#include "src/storage/expressions/DoubleConstantExpression.h" +#include "src/storage/expressions/DoubleLiteralExpression.h" +#include "src/storage/expressions/IntegerConstantExpression.h" +#include "src/storage/expressions/IntegerLiteralExpression.h" +#include "src/storage/expressions/UnaryBooleanFunctionExpression.h" +#include "src/storage/expressions/UnaryNumericalFunctionExpression.h" +#include "src/storage/expressions/VariableExpression.h" +#include "src/storage/expressions/Expression.h" \ No newline at end of file diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index c01e24c0d..97daf8142 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::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() { + Program::Program(ModelType modelType, std::set const& undefinedBooleanConstants, std::map const& definedBooleanConstants, std::set const& undefinedIntegerConstants, std::map const& definedIntegerConstants, std::set const& undefinedDoubleConstants, std::map const& definedDoubleConstants, std::map const& globalBooleanVariables, std::map const& globalIntegerVariables, std::mapconst& formulas, 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), formulas(formulas), 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); @@ -101,6 +101,10 @@ namespace storm { return this->getGlobalIntegerVariables().size(); } + std::map const& Program::getFormulas() const { + return this->formulas; + } + std::size_t Program::getNumberOfModules() const { return this->getModules().size(); } @@ -175,7 +179,7 @@ namespace storm { newModules.push_back(module.restrictCommands(indexSet)); } - return Program(this->getModelType(), this->getUndefinedBooleanConstants(), this->getUndefinedIntegerConstants(), this->getUndefinedDoubleConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), newModules, this->getRewardModels(), this->definesInitialStatesExpression(), this->getInitialStatesExpression(), this->getLabels()); + return Program(this->getModelType(), this->getUndefinedBooleanConstants(), this->getDefinedBooleanConstants(), this->getUndefinedIntegerConstants(), this->getDefinedIntegerConstants(), this->getUndefinedDoubleConstants(), this->getDefinedDoubleConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getRewardModels(), this->definesInitialStatesExpression(), this->getInitialStatesExpression(), this->getLabels()); } std::ostream& operator<<(std::ostream& stream, Program const& program) { diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 36326b12b..33056833a 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -32,6 +32,7 @@ namespace storm { * @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 formulas The formulas defined in the program. * @param modules The modules of the program. * @param hasInitialStatesExpression A flag indicating whether the program specifies its initial states via * an explicit initial construct. @@ -43,7 +44,7 @@ namespace storm { * @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::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); + Program(ModelType modelType, std::set const& undefinedBooleanConstants, std::map const& definedBooleanConstants, std::set const& undefinedIntegerConstants, std::map const& definedIntegerConstants, std::set const& undefinedDoubleConstants, std::map const& definedDoubleConstants, std::map const& globalBooleanVariables, std::map const& globalIntegerVariables, std::map const& formulas, 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; @@ -173,6 +174,13 @@ namespace storm { */ std::size_t getNumberOfGlobalIntegerVariables() const; + /*! + * Retrieves the formulas defined in the program. + * + * @return The formulas defined in the program. + */ + std::map const& getFormulas() const; + /*! * Retrieves the number of modules in the program. * @@ -286,12 +294,15 @@ namespace storm { // A mapping of (defined) double constants to their values (given as expressions). std::map definedDoubleConstants; - // A list of global boolean variables. + // The global boolean variables. std::map globalBooleanVariables; - // A list of global integer variables. + // The global integer variables. std::map globalIntegerVariables; + // A mapping of formula names to the corresponding expressions. + std::map formulas; + // The modules associated with the program. std::vector modules; diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp index da92823bb..edd400ee2 100644 --- a/src/storage/prism/Update.cpp +++ b/src/storage/prism/Update.cpp @@ -3,25 +3,17 @@ namespace storm { namespace prism { - 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) { + Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::map const& assignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), assignments(assignments), globalIndex(globalIndex) { // Nothing to do here. } - 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()) { + 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)), assignments(), globalIndex(newGlobalIndex) { + for (auto const& variableAssignmentPair : update.getAssignments()) { auto const& namePair = renaming.find(variableAssignmentPair.first); if (namePair != renaming.end()) { - this->booleanAssignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber)); + this->assignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber)); } else { - 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, filename, lineNumber)); - } else { - this->integerAssignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber)); + this->assignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber)); } } this->likelihoodExpression = update.getLikelihoodExpression().substitute(renaming); @@ -31,35 +23,18 @@ namespace storm { return likelihoodExpression; } - std::size_t Update::getNumberOfBooleanAssignments() const { - return booleanAssignments.size(); - } - - std::size_t Update::getNumberOfIntegerAssignments() const { - return integerAssignments.size(); - } - - std::map const& Update::getBooleanAssignments() const { - return booleanAssignments; - } - - std::map const& Update::getIntegerAssignments() const { - return integerAssignments; + std::size_t Update::getNumberOfAssignments() const { + return this->assignments.size(); } - storm::prism::Assignment const& Update::getBooleanAssignment(std::string const& variableName) const { - auto variableAssignmentPair = booleanAssignments.find(variableName); - if (variableAssignmentPair == booleanAssignments.end()) { - throw storm::exceptions::OutOfRangeException() << "Cannot find boolean assignment for variable '" << variableName << "' in update " << *this << "."; - } - - return variableAssignmentPair->second; + std::map const& Update::getAssignments() const { + return this->assignments; } - storm::prism::Assignment const& Update::getIntegerAssignment(std::string const& variableName) const { - auto variableAssignmentPair = integerAssignments.find(variableName); - if (variableAssignmentPair == integerAssignments.end()) { - throw storm::exceptions::OutOfRangeException() << "Cannot find integer assignment for variable '" << variableName << "' in update " << *this << "."; + storm::prism::Assignment const& Update::getAssignment(std::string const& variableName) const { + auto variableAssignmentPair = this->getAssignments().find(variableName); + if (variableAssignmentPair == this->getAssignments().end()) { + throw storm::exceptions::OutOfRangeException() << "Cannot find assignment for variable '" << variableName << "' in update " << *this << "."; } return variableAssignmentPair->second; @@ -72,17 +47,9 @@ namespace storm { std::ostream& operator<<(std::ostream& stream, Update const& update) { stream << update.getLikelihoodExpression() << " : "; uint_fast64_t i = 0; - for (auto const& assignment : update.getBooleanAssignments()) { - stream << assignment.second; - if (i < update.getBooleanAssignments().size() - 1 || update.getIntegerAssignments().size() > 0) { - stream << " & "; - } - ++i; - } - i = 0; - for (auto const& assignment : update.getIntegerAssignments()) { + for (auto const& assignment : update.getAssignments()) { stream << assignment.second; - if (i < update.getIntegerAssignments().size() - 1) { + if (i < update.getAssignments().size() - 1) { stream << " & "; } ++i; diff --git a/src/storage/prism/Update.h b/src/storage/prism/Update.h index 4999c04bd..517803c2b 100644 --- a/src/storage/prism/Update.h +++ b/src/storage/prism/Update.h @@ -20,7 +20,7 @@ namespace storm { * @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, std::string const& filename = "", uint_fast64_t lineNumber = 0); + Update(uint_fast64_t index, storm::expressions::Expression const& likelihoodExpression, std::map const& assignments, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Creates a copy of the given update and performs the provided renaming. @@ -48,46 +48,25 @@ namespace storm { storm::expressions::Expression const& getLikelihoodExpression() const; /*! - * Retrieves the number of boolean assignments associated with this update. + * Retrieves the number of assignments associated with this update. * - * @return The number of boolean assignments associated with this update. + * @return The number of assignments associated with this update. */ - std::size_t getNumberOfBooleanAssignments() const; + std::size_t getNumberOfAssignments() const; /*! - * Retrieves the number of integer assignments associated with this update. + * Retrieves a reference to the map of variable names to their respective assignments. * - * @return The number of integer assignments associated with this update. + * @return A reference to the map of variable names to their respective assignments. */ - std::size_t getNumberOfIntegerAssignments() const; + std::map const& getAssignments() const; /*! - * Retrieves a reference to the map of boolean variable names to their respective assignments. + * Retrieves a reference to the assignment for the variable with the given name. * - * @return A reference to the map of boolean variable names to their respective assignments. + * @return A reference to the assignment for the variable with the given name. */ - std::map const& getBooleanAssignments() const; - - /*! - * Retrieves a reference to the map of integer variable names to their respective assignments. - * - * @return A reference to the map of integer variable names to their respective assignments. - */ - std::map const& getIntegerAssignments() const; - - /*! - * Retrieves a reference to the assignment for the boolean variable with the given name. - * - * @return A reference to the assignment for the boolean variable with the given name. - */ - storm::prism::Assignment const& getBooleanAssignment(std::string const& variableName) const; - - /*! - * Retrieves a reference to the assignment for the integer variable with the given name. - * - * @return A reference to the assignment for the integer variable with the given name. - */ - storm::prism::Assignment const& getIntegerAssignment(std::string const& variableName) const; + storm::prism::Assignment const& getAssignment(std::string const& variableName) const; /*! * Retrieves the global index of the update, that is, a unique index over all modules. @@ -102,11 +81,8 @@ namespace storm { // An expression specifying the likelihood of taking this update. storm::expressions::Expression likelihoodExpression; - // A mapping of boolean variable names to their assignments in this update. - std::map booleanAssignments; - - // A mapping of integer variable names to their assignments in this update. - std::map integerAssignments; + // A mapping of variable names to their assignments in this update. + std::map assignments; // The global index of the update. uint_fast64_t globalIndex; diff --git a/test/functional/parser/ParsePrismTest.cpp b/test/functional/parser/ParsePrismTest.cpp deleted file mode 100644 index 0a8abb420..000000000 --- a/test/functional/parser/ParsePrismTest.cpp +++ /dev/null @@ -1,32 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" -#include "src/parser/PrismParser.h" -//#include "src/utility/IoUtility.h" -#include "src/ir/Program.h" -#include "src/adapters/ExplicitModelAdapter.h" -#include "src/models/Dtmc.h" -#include "src/models/Mdp.h" -#include "src/settings/Settings.h" -#include "src/settings/InternalOptionMemento.h" - -TEST(ParsePrismTest, parseCrowds5_5) { - storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true); - ASSERT_TRUE(storm::settings::Settings::getInstance()->isSet("fixDeadlocks")); - storm::ir::Program program; - ASSERT_NO_THROW(program = storm::parser::PrismParserFromFile(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.pm")); - std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(program); - - ASSERT_EQ(model->getNumberOfStates(), 8607ull); - ASSERT_EQ(model->getNumberOfTransitions(), 15113ull); -} - -TEST(ParsePrismTest, parseTwoDice) { - storm::ir::Program program; - ASSERT_NO_THROW(program = storm::parser::PrismParserFromFile(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.nm")); - - std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(program, "", "coinflips"); - - ASSERT_EQ(model->getNumberOfStates(), 169ull); - ASSERT_EQ(model->as>()->getNumberOfChoices(), 254ull); - ASSERT_EQ(model->getNumberOfTransitions(), 436ull); -}