From 22ddf9c5be78f6a1b36d9329612afd8f4e79170f Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 9 Jun 2013 22:37:11 +0200 Subject: [PATCH] On my way of cleaning up Gereon's mess. :P --- src/ir/Assignment.cpp | 20 ++- src/ir/Assignment.h | 30 +++-- src/ir/BooleanVariable.cpp | 17 ++- src/ir/BooleanVariable.h | 27 ++-- src/ir/Command.cpp | 22 ++-- src/ir/Command.h | 39 ++++-- src/ir/IntegerVariable.cpp | 20 +-- src/ir/IntegerVariable.h | 31 +++-- src/ir/Module.cpp | 153 +++++++++++------------ src/ir/Module.h | 151 ++++++++++++++-------- src/ir/Program.cpp | 81 ++++-------- src/ir/Program.h | 79 ++++++------ src/ir/RewardModel.cpp | 8 +- src/ir/StateReward.cpp | 2 +- src/ir/StateReward.h | 2 +- src/ir/TransitionReward.cpp | 2 +- src/ir/TransitionReward.h | 2 +- src/ir/Update.cpp | 38 +++--- src/ir/Update.h | 6 +- src/ir/Variable.cpp | 4 +- src/ir/Variable.h | 6 +- src/parser/prismparser/PrismGrammar.cpp | 4 +- src/parser/prismparser/VariableState.cpp | 126 ++++++++----------- src/parser/prismparser/VariableState.h | 118 +++++++++-------- 24 files changed, 524 insertions(+), 464 deletions(-) diff --git a/src/ir/Assignment.cpp b/src/ir/Assignment.cpp index 232472857..6182fda6b 100644 --- a/src/ir/Assignment.cpp +++ b/src/ir/Assignment.cpp @@ -5,43 +5,39 @@ * Author: Christian Dehnert */ -#include "Assignment.h" - #include +#include "Assignment.h" + namespace storm { namespace ir { -// Initializes all members with their default constructors. Assignment::Assignment() : variableName(), expression() { // Nothing to do here. } -// Initializes all members according to the given values. -Assignment::Assignment(std::string variableName, std::shared_ptr expression) +Assignment::Assignment(std::string const& variableName, std::shared_ptr const& expression) : variableName(variableName), expression(expression) { // Nothing to do here. } -Assignment::Assignment(const Assignment& assignment, const std::map& renaming, const std::map& bools, const std::map& ints) - : variableName(assignment.variableName), expression(assignment.expression->clone(renaming, bools, ints)) { - if (renaming.count(assignment.variableName) > 0) { - this->variableName = renaming.at(assignment.variableName); +Assignment::Assignment(Assignment const& oldAssignment, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap) + : variableName(oldAssignment.variableName), expression(oldAssignment.expression->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap)) { + auto renamingPair = renaming.find(oldAssignment.variableName); + if (renamingPair != renaming.end()) { + this->variableName = renamingPair->second; } } -// Returns the name of the variable associated with this assignment. std::string const& Assignment::getVariableName() const { return variableName; } -// Returns the expression associated with this assignment. std::shared_ptr const& Assignment::getExpression() const { return expression; } -// Build a string representation of the assignment. std::string Assignment::toString() const { std::stringstream result; result << "(" << variableName << "' = " << expression->toString() << ")"; diff --git a/src/ir/Assignment.h b/src/ir/Assignment.h index b17693bf0..2c37f995e 100644 --- a/src/ir/Assignment.h +++ b/src/ir/Assignment.h @@ -8,10 +8,10 @@ #ifndef STORM_IR_ASSIGNMENT_H_ #define STORM_IR_ASSIGNMENT_H_ -#include "expressions/BaseExpression.h" - #include +#include "expressions/BaseExpression.h" + namespace storm { namespace ir { @@ -28,22 +28,34 @@ 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 variableName The variable that this assignment targets. + * @param expression The expression to assign to the variable. */ - Assignment(std::string variableName, std::shared_ptr expression); - - Assignment(const Assignment& assignment, const std::map& renaming, const std::map& bools, const std::map& ints); + Assignment(std::string const& variableName, std::shared_ptr const& expression); + + /*! + * 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 booleanVariableToIndexMap A mapping from boolean variable names to their global indices. + * @param integerVariableToIndexMap A mapping from integer variable names to their global indices. + */ + Assignment(Assignment const& oldAssignment, std::map const& renaming, std::map const& bools, std::map const& ints); /*! * Retrieves the name of the variable that this assignment targets. - * @returns the name of the variable that this assignment targets. + * + * @return The name of the variable that this assignment targets. */ std::string const& getVariableName() const; /*! * Retrieves the expression that is assigned to the variable. - * @returns the expression that is assigned to the variable. + * + * @return The expression that is assigned to the variable. */ std::shared_ptr const& getExpression() const; diff --git a/src/ir/BooleanVariable.cpp b/src/ir/BooleanVariable.cpp index 2c03e1c44..1a660ac0e 100644 --- a/src/ir/BooleanVariable.cpp +++ b/src/ir/BooleanVariable.cpp @@ -5,31 +5,28 @@ * Author: Christian Dehnert */ -#include "BooleanVariable.h" - #include +#include "BooleanVariable.h" + namespace storm { namespace ir { -// Initializes all members with their default constructors. BooleanVariable::BooleanVariable() : Variable() { // Nothing to do here. } -// Initializes all members according to the given values. -BooleanVariable::BooleanVariable(uint_fast64_t index, std::string variableName, - std::shared_ptr initialValue) - : Variable(index, variableName, initialValue) { +BooleanVariable::BooleanVariable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string const& variableName, std::shared_ptr const& initialValue) + : Variable(globalIndex, localIndex, variableName, initialValue) { // Nothing to do here. } -BooleanVariable::BooleanVariable(const BooleanVariable& var, const std::string& newName, const std::map& renaming, const std::map& bools, const std::map& ints) - : Variable(var, newName, bools.at(newName), renaming, bools, ints) { +BooleanVariable::BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap) + : Variable(oldVariable, newName, newGlobalIndex, renaming, booleanVariableToIndexMap, integerVariableToIndexMap) { + // Nothing to do here. } -// Build a string representation of the variable. std::string BooleanVariable::toString() const { std::stringstream result; result << this->getName() << ": bool"; diff --git a/src/ir/BooleanVariable.h b/src/ir/BooleanVariable.h index bf70f01d1..4084d959d 100644 --- a/src/ir/BooleanVariable.h +++ b/src/ir/BooleanVariable.h @@ -8,10 +8,11 @@ #ifndef STORM_IR_BOOLEANVARIABLE_H_ #define STORM_IR_BOOLEANVARIABLE_H_ -#include "src/ir/Variable.h" #include #include +#include "src/ir/Variable.h" + namespace storm { namespace ir { @@ -28,14 +29,26 @@ public: /*! * Creates a boolean variable with the given name and the given initial value. - * @param index a unique (among the variables of equal type) index for the variable. - * @param variableName the name of the variable. - * @param initialValue the expression that defines the initial value of the variable. + * + * @param globalIndex A globally unique index for the variable. + * @param localIndex A module-local unique index for the variable. + * @param variableName The name of the variable. + * @param initialValue The expression that defines the initial value of the variable. */ - BooleanVariable(uint_fast64_t index, std::string variableName, std::shared_ptr initialValue = std::shared_ptr(nullptr)); + BooleanVariable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string const& variableName, std::shared_ptr const& initialValue = std::shared_ptr(nullptr)); - - BooleanVariable(const BooleanVariable& var, const std::string& newName, const std::map& renaming, const std::map& bools, const std::map& ints); + /*! + * Creates a copy of the given boolean variable and performs the provided renaming. + * + * @param oldVariable The variable to copy. + * @param newName New name of this variable. + * @param newGlobalIndex The new global index of the variable. + * @param renaming A mapping from names that are to be renamed to the names they are to be + * replaced with. + * @param booleanVariableToIndexMap A mapping from boolean variable names to their global indices. + * @param integerVariableToIndexMap A mapping from integer variable names to their global indices. + */ + BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap); /*! * Retrieves a string representation of this variable. diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp index 05fe1084c..673ce1b5e 100644 --- a/src/ir/Command.cpp +++ b/src/ir/Command.cpp @@ -20,43 +20,39 @@ Command::Command() : actionName(), guardExpression(), updates() { } // Initializes all members according to the given values. -Command::Command(std::string actionName, std::shared_ptr guardExpression, std::vector updates) +Command::Command(std::string const& actionName, std::shared_ptr guardExpression, std::vector const& updates) : actionName(actionName), guardExpression(guardExpression), updates(updates) { // Nothing to do here. } -Command::Command(const Command& cmd, const std::map& renaming, const std::map& bools, const std::map& ints) - : actionName(cmd.actionName), guardExpression(cmd.guardExpression->clone(renaming, bools, ints)) { - if (renaming.count(this->actionName) > 0) { - this->actionName = renaming.at(this->actionName); +Command::Command(Command const& oldCommand, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap) + : actionName(oldCommand.getActionName()), guardExpression(oldCommand.guardExpression->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap)) { + auto renamingPair = renaming.find(this->actionName); + if (renamingPair != renaming.end()) { + this->actionName = renamingPair->first; } - this->updates.reserve(cmd.updates.size()); - for (Update u : cmd.updates) { - this->updates.emplace_back(u, renaming, bools, ints); + this->updates.reserve(oldCommand.getNumberOfUpdates()); + for (Update const& update : oldCommand.updates) { + this->updates.emplace_back(update, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); } } -// Return the action name. std::string const& Command::getActionName() const { return this->actionName; } -// Return the expression for the guard. std::shared_ptr const& Command::getGuard() const { return guardExpression; } -// Return the number of updates. uint_fast64_t Command::getNumberOfUpdates() const { return this->updates.size(); } -// Return the requested update. storm::ir::Update const& Command::getUpdate(uint_fast64_t index) const { return this->updates[index]; } -// Build a string representation of the command. std::string Command::toString() const { std::stringstream result; result << "[" << actionName << "] " << guardExpression->toString() << " -> "; diff --git a/src/ir/Command.h b/src/ir/Command.h index b4049307c..25fcb34ce 100644 --- a/src/ir/Command.h +++ b/src/ir/Command.h @@ -8,13 +8,13 @@ #ifndef STORM_IR_COMMAND_H_ #define STORM_IR_COMMAND_H_ -#include "expressions/BaseExpression.h" -#include "Update.h" - #include #include #include +#include "expressions/BaseExpression.h" +#include "Update.h" + namespace storm { namespace ir { @@ -31,39 +31,56 @@ public: /*! * Creates a command with the given name, guard and updates. - * @param actionName the action name of the command. + * + * @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. + */ + Command(std::string const& actionName, std::shared_ptr guardExpression, std::vector const& updates); + + /*! + * Creates a copy of the given command and performs the provided renaming. + * + * @param oldCommand The command to copy. + * @param renaming A mapping from names that are to be renamed to the names they are to be + * replaced with. + * @param booleanVariableToIndexMap A mapping from boolean variable names to their global indices. + * @param integerVariableToIndexMap A mapping from integer variable names to their global indices. */ - Command(std::string actionName, std::shared_ptr guardExpression, std::vector updates); + Command(Command const& oldCommand, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap); - Command(const Command& cmd, const std::map& renaming, const std::map& bools, const std::map& ints); /*! * Retrieves the action name of this command. - * @returns the action name of this command. + * + * @return The action name of this command. */ std::string const& getActionName() const; /*! * Retrieves a reference to the guard of the command. - * @returns a reference to the guard of the command. + * + * @return A reference to the guard of the command. */ std::shared_ptr const& getGuard() const; /*! * Retrieves the number of updates associated with this command. - * @returns the number of updates associated with this command. + * + * @return The number of updates associated with this command. */ uint_fast64_t getNumberOfUpdates() const; /*! * Retrieves a reference to the update with the given index. - * @returns a reference to the update with the given index. + * + * @return A reference to the update with the given index. */ storm::ir::Update const& getUpdate(uint_fast64_t index) const; /*! * Retrieves a string representation of this command. - * @returns a string representation of this command. + * + * @return A string representation of this command. */ std::string toString() const; diff --git a/src/ir/IntegerVariable.cpp b/src/ir/IntegerVariable.cpp index a8926b046..4e70820e6 100644 --- a/src/ir/IntegerVariable.cpp +++ b/src/ir/IntegerVariable.cpp @@ -5,46 +5,38 @@ * Author: Christian Dehnert */ -#include "IntegerVariable.h" - #include - #include +#include "IntegerVariable.h" + namespace storm { namespace ir { -// Initializes all members with their default constructors. IntegerVariable::IntegerVariable() : lowerBound(), upperBound() { // Nothing to do here. } -// Initializes all members according to the given values. -IntegerVariable::IntegerVariable(uint_fast64_t index, std::string variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue) - : Variable(index, variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) { - // TODO: This behaves like prism... +IntegerVariable::IntegerVariable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string const& variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue) + : Variable(globalIndex, localIndex, variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) { if (this->getInitialValue() == nullptr) { this->setInitialValue(lowerBound); } } -IntegerVariable::IntegerVariable(const IntegerVariable& var, const std::string& newName, const std::map& renaming, const std::map& bools, const std::map& ints) - : Variable(var, newName, ints.at(newName), renaming, bools, ints), lowerBound(var.lowerBound->clone(renaming, bools, ints)), upperBound(var.upperBound->clone(renaming, bools, ints)) { +IntegerVariable::IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap) + : Variable(oldVariable, newName, newGlobalIndex, renaming, booleanVariableToIndexMap, integerVariableToIndexMap), lowerBound(oldVariable.lowerBound->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap)), upperBound(oldVariable.upperBound->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap)) { } -// Return lower bound for variable. std::shared_ptr IntegerVariable::getLowerBound() const { return this->lowerBound; } -// Return upper bound for variable. std::shared_ptr IntegerVariable::getUpperBound() const { return this->upperBound; } - -// Build a string representation of the variable. std::string IntegerVariable::toString() const { std::stringstream result; result << this->getName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]"; diff --git a/src/ir/IntegerVariable.h b/src/ir/IntegerVariable.h index 8233cbe09..cd1b2cba4 100644 --- a/src/ir/IntegerVariable.h +++ b/src/ir/IntegerVariable.h @@ -8,10 +8,11 @@ #ifndef STORM_IR_INTEGERVARIABLE_H_ #define STORM_IR_INTEGERVARIABLE_H_ -#include "expressions/BaseExpression.h" -#include "src/ir/Variable.h" #include +#include "src/ir/Variable.h" +#include "expressions/BaseExpression.h" + namespace storm { namespace ir { @@ -26,18 +27,30 @@ public: */ IntegerVariable(); - /*! - * Creates an integer variable with the given name, lower and upper bounds and the given initial - * value. - * @param index A unique (among the variables of equal type) index for the variable. - * @param variableName the name of the variable. + /*! + * Creates a boolean variable with the given name and the given initial value. + * + * @param globalIndex A globally unique index for the variable. + * @param localIndex A module-local unique index for the variable. + * @param variableName The name of the variable. * @param lowerBound the lower bound of the domain of the variable. * @param upperBound the upper bound of the domain of the variable. * @param initialValue the expression that defines the initial value of the variable. */ - IntegerVariable(uint_fast64_t index, std::string variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue = std::shared_ptr(nullptr)); + IntegerVariable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string const& variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue = std::shared_ptr(nullptr)); - IntegerVariable(const IntegerVariable& var, const std::string& newName, const std::map& renaming, const std::map& bools, const std::map& ints); + /*! + * Creates a copy of the given integer variable and performs the provided renaming. + * + * @param oldVariable The variable to copy. + * @param newName New name of this variable. + * @param newGlobalIndex The new global index of the variable. + * @param renaming A mapping from names that are to be renamed to the names they are to be + * replaced with. + * @param booleanVariableToIndexMap A mapping from boolean variable names to their global indices. + * @param integerVariableToIndexMap A mapping from integer variable names to their global indices. + */ + IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap); /*! * Retrieves the lower bound for this integer variable. diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index 624f1876c..df56b6bc5 100644 --- a/src/ir/Module.cpp +++ b/src/ir/Module.cpp @@ -5,13 +5,13 @@ * Author: Christian Dehnert */ -#include "Module.h" - -#include "src/exceptions/InvalidArgumentException.h" - #include #include +#include "Module.h" +#include "src/exceptions/OutOfRangeException.h" +#include "src/exceptions/InvalidArgumentException.h" + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; @@ -20,62 +20,58 @@ namespace storm { namespace ir { -// Initializes all members with their default constructors. -Module::Module() : moduleName(), booleanVariables(), integerVariables(), booleanVariablesToIndexMap(), - integerVariablesToIndexMap(), commands(), actions(), actionsToCommandIndexMap() { +Module::Module() : moduleName(), booleanVariables(), integerVariables(), booleanVariableToLocalIndexMap(), + integerVariableToLocalIndexMap(), commands(), actions(), actionsToCommandIndexMap() { // Nothing to do here. } -// Initializes all members according to the given values. -Module::Module(std::string moduleName, - std::vector booleanVariables, - std::vector integerVariables, - std::map booleanVariableToIndexMap, - std::map integerVariableToIndexMap, - std::vector commands) +Module::Module(std::string const& moduleName, + std::vector const& booleanVariables, + std::vector const& integerVariables, + std::map const& booleanVariableToLocalIndexMap, + std::map const& integerVariableToLocalIndexMap, + std::vector const& commands) : moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), - booleanVariablesToIndexMap(booleanVariableToIndexMap), - integerVariablesToIndexMap(integerVariableToIndexMap), commands(commands), actions(), actionsToCommandIndexMap() { + booleanVariableToLocalIndexMap(booleanVariableToLocalIndexMap), + integerVariableToLocalIndexMap(integerVariableToLocalIndexMap), commands(commands), actions(), actionsToCommandIndexMap() { + // Initialize the internal mappings for fast information retrieval. this->collectActions(); } -Module::Module(const Module& module, const std::string& moduleName, const std::map& renaming, std::shared_ptr adder) - : moduleName(moduleName) { - LOG4CPLUS_TRACE(logger, "Start renaming " << module.moduleName << " to " << moduleName); - - // First step: Create new Variables via the adder. - adder->performRenaming(renaming); - - // Second step: Get all indices of variables that are produced by the renaming. - for (auto it: renaming) { - std::shared_ptr var = adder->getVariable(it.second); - if (var != nullptr) { - if (var->getType() == expressions::BaseExpression::bool_) { - this->booleanVariablesToIndexMap[it.second] = var->getVariableIndex(); - } else if (var->getType() == expressions::BaseExpression::int_) { - this->integerVariablesToIndexMap[it.second] = var->getVariableIndex(); - } - } - } - - // Third step: Create new Variable objects. - this->booleanVariables.reserve(module.booleanVariables.size()); - for (BooleanVariable it: module.booleanVariables) { - if (renaming.count(it.getName()) > 0) { - this->booleanVariables.emplace_back(it, renaming.at(it.getName()), renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap); - } else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!"); - } - this->integerVariables.reserve(module.integerVariables.size()); - for (IntegerVariable it: module.integerVariables) { - if (renaming.count(it.getName()) > 0) { - this->integerVariables.emplace_back(it, renaming.at(it.getName()), renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap); - } else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!"); - } - - // Fourth step: Clone commands. - this->commands.reserve(module.commands.size()); - for (Command cmd: module.commands) { - this->commands.emplace_back(cmd, renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap); +Module::Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap, std::shared_ptr const& adder) + : moduleName(newModuleName), booleanVariableToLocalIndexMap(oldModule.booleanVariableToLocalIndexMap), integerVariableToLocalIndexMap(oldModule.integerVariableToLocalIndexMap) { + LOG4CPLUS_TRACE(logger, "Start renaming " << oldModule.getName() << " to " << moduleName << "."); + + // Iterate over boolean variables and rename them. If a variable was not renamed, this is an error and an exception + // is thrown. + this->booleanVariables.reserve(oldModule.getNumberOfBooleanVariables()); + for (BooleanVariable const& booleanVariable : oldModule.booleanVariables) { + auto renamingPair = renaming.find(booleanVariable.getName()); + if (renamingPair == renaming.end()) { + LOG4CPLUS_ERROR(logger, "Boolean variable " << moduleName << "." << booleanVariable.getName() << " was not renamed."); + throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << moduleName << "." << booleanVariable.getName() << " was not renamed."; + } else { + this->booleanVariables.emplace_back(booleanVariable, renamingPair->second, adder->getNextGlobalBooleanVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap); + adder->addBooleanVariable(renamingPair->second); + } + } + // Now do the same for the integer variables. + this->integerVariables.reserve(oldModule.getNumberOfIntegerVariables()); + for (IntegerVariable const& integerVariable : oldModule.integerVariables) { + auto renamingPair = renaming.find(integerVariable.getName()); + if (renamingPair == renaming.end()) { + LOG4CPLUS_ERROR(logger, "Integer variable " << moduleName << "." << integerVariable.getName() << " was not renamed."); + throw storm::exceptions::InvalidArgumentException() << "Integer variable " << moduleName << "." << integerVariable.getName() << " was not renamed."; + } else { + this->integerVariables.emplace_back(integerVariable, renamingPair->second, adder->getNextGlobalIntegerVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap); + adder->addIntegerVariable(renamingPair->second); + } + } + + // Now we are ready to clone all commands and rename them if requested. + this->commands.reserve(oldModule.getNumberOfCommands()); + for (Command const& command : oldModule.commands) { + this->commands.emplace_back(command, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); } this->collectActions(); @@ -108,31 +104,32 @@ uint_fast64_t Module::getNumberOfCommands() const { } // Return the index of the variable if it exists and throw exception otherwise. -uint_fast64_t Module::getBooleanVariableIndex(std::string variableName) const { - auto it = booleanVariablesToIndexMap.find(variableName); - if (it != booleanVariablesToIndexMap.end()) { +uint_fast64_t Module::getBooleanVariableIndex(std::string const& variableName) const { + auto it = booleanVariableToLocalIndexMap.find(variableName); + if (it != booleanVariableToLocalIndexMap.end()) { return it->second; } - throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown " - << "boolean variable " << variableName << "."; + LOG4CPLUS_ERROR(logger, "Cannot retrieve index of unknown boolean variable " << variableName << "."); + throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown boolean variable " << variableName << "."; } -// Return the index of the variable if it exists and throw exception otherwise. -uint_fast64_t Module::getIntegerVariableIndex(std::string variableName) const { - auto it = integerVariablesToIndexMap.find(variableName); - if (it != integerVariablesToIndexMap.end()) { +uint_fast64_t Module::getIntegerVariableIndex(std::string const& variableName) const { + auto it = integerVariableToLocalIndexMap.find(variableName); + if (it != integerVariableToLocalIndexMap.end()) { return it->second; } - throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown " - << "variable " << variableName << "."; + LOG4CPLUS_ERROR(logger, "Cannot retrieve index of unknown integer variable " << variableName << "."); + throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown integer variable " << variableName << "."; } -// Return the requested command. -storm::ir::Command const Module::getCommand(uint_fast64_t index) const { +storm::ir::Command const& Module::getCommand(uint_fast64_t index) const { return this->commands[index]; } + +std::string const& Module::getName() const { + return this->moduleName; +} -// Build a string representation of the variable. std::string Module::toString() const { std::stringstream result; result << "module " << moduleName << std::endl; @@ -149,29 +146,27 @@ std::string Module::toString() const { return result.str(); } -// Return set of actions. std::set const& Module::getActions() const { return this->actions; } -// Return commands with given action. -std::shared_ptr> const Module::getCommandsByAction(std::string const& action) const { - auto res = this->actionsToCommandIndexMap.find(action); - if (res == this->actionsToCommandIndexMap.end()) { - return std::shared_ptr>(new std::set()); - } else { - return res->second; +std::set const& Module::getCommandsByAction(std::string const& action) const { + auto actionsCommandSetPair = this->actionsToCommandIndexMap.find(action); + if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) { + return actionsCommandSetPair->second; } + LOG4CPLUS_ERROR(logger, "Action name '" << action << "' does not exist in module."); + throw storm::exceptions::OutOfRangeException() << "Action name '" << action << "' does not exist in module."; } void Module::collectActions() { for (unsigned int id = 0; id < this->commands.size(); id++) { - std::string action = this->commands[id].getActionName(); + std::string const& action = this->commands[id].getActionName(); if (action != "") { - if (this->actionsToCommandIndexMap.count(action) == 0) { - this->actionsToCommandIndexMap[action] = std::shared_ptr>(new std::set()); + if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) { + this->actionsToCommandIndexMap.emplace(action, std::set()); } - this->actionsToCommandIndexMap[action]->insert(id); + this->actionsToCommandIndexMap[action].insert(id); this->actions.insert(action); } } diff --git a/src/ir/Module.h b/src/ir/Module.h index e4343e357..e55b8a303 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -8,26 +8,47 @@ #ifndef STORM_IR_MODULE_H_ #define STORM_IR_MODULE_H_ -#include "BooleanVariable.h" -#include "IntegerVariable.h" -#include "expressions/VariableExpression.h" -#include "Command.h" - #include #include #include #include #include +#include "BooleanVariable.h" +#include "IntegerVariable.h" +#include "expressions/VariableExpression.h" +#include "Command.h" + namespace storm { namespace ir { struct VariableAdder { - virtual uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper) = 0; - virtual uint_fast64_t addBooleanVariable(const std::string& name) = 0; - virtual std::shared_ptr getVariable(const std::string& name) = 0; - virtual void performRenaming(const std::map& renaming) = 0; + /*! + * Adds an integer variable with the given name, lower and upper bound. + * + * @param name The name of the boolean variable to add. + */ + virtual uint_fast64_t addBooleanVariable(std::string const& name) = 0; + + /*! + * Adds an integer variable with the given name, lower and upper bound. + * + * @param name The name of the integer variable to add. + * @param lower The lower bound of the integer variable. + * @param upper The upper bound of the integer variable. + */ + virtual uint_fast64_t addIntegerVariable(std::string const& name) = 0; + + /*! + * Retrieves the next free (global) index for a boolean variable. + */ + virtual uint_fast64_t getNextGlobalBooleanVariableIndex() = 0; + + /*! + * Retrieves the next free (global) index for a integer variable. + */ + virtual uint_fast64_t getNextGlobalIntegerVariableIndex() = 0; }; /*! @@ -42,101 +63,129 @@ public: /*! * Creates a module with the given name, variables and commands. - * @param moduleName the name of the module. - * @param booleanVariables a map of boolean variables. - * @param integerVariables a map of integer variables. - * @param commands the vector of commands. + * + * @param moduleName The name of the module. + * @param booleanVariables The boolean variables defined by the module. + * @param integerVariables The integer variables defined by the module. + * @param booleanVariableToIndexMap A mapping of boolean variables to global (i.e. program-wide) indices. + * @param integerVariableToIndexMap A mapping of integer variables to global (i.e. program-wide) indices. + * @param commands The commands of the module. */ - Module(std::string moduleName, std::vector booleanVariables, - std::vector integerVariables, - std::map booleanVariableToIndexMap, - std::map integerVariableToIndexMap, - std::vector commands); - - typedef uint_fast64_t (*addIntegerVariablePtr)(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper, const std::shared_ptr init); - typedef uint_fast64_t (*addBooleanVariablePtr)(const std::string& name, const std::shared_ptr init); + Module(std::string const& moduleName, std::vector const& booleanVariables, + std::vector const& integerVariables, + std::map const& booleanVariableToLocalIndexMap, + std::map const& integerVariableToLocalIndexMap, + std::vector const& commands); + + typedef uint_fast64_t (*addIntegerVariablePtr)(std::string const& name, std::shared_ptr const& lower, std::shared_ptr const upper, std::shared_ptr const& init); + typedef uint_fast64_t (*addBooleanVariablePtr)(std::string const& name, std::shared_ptr const& init); /*! * Special copy constructor, implementing the module renaming functionality. - * This will create a new module having all identifier renamed according to the given map. - * @param module Module to be copied. - * @param moduleName Name of the new module. - * @param renaming Renaming map. + * This will create a new module having all identifiers renamed according to the given map. + * + * @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 booleanVariableToIndexMap A mapping from boolean variable names to their global indices. + * @param integerVariableToIndexMap A mapping from integer variable names to their global indices. + * @param adder An instance of the VariableAdder interface that keeps track of all the variables in the probabilistic + * program. */ - Module(const Module& module, const std::string& moduleName, const std::map& renaming, std::shared_ptr adder); + Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap, std::shared_ptr const& adder); /*! * Retrieves the number of boolean variables in the module. - * @returns the number of boolean variables in the module. + * + * @return the number of boolean variables in the module. */ uint_fast64_t getNumberOfBooleanVariables() const; /*! * Retrieves a reference to the boolean variable with the given index. - * @returns a reference to the boolean variable with the given index. + * + * @return A reference to the boolean variable with the given index. */ storm::ir::BooleanVariable const& getBooleanVariable(uint_fast64_t index) const; /*! * Retrieves the number of integer variables in the module. - * @returns the number of integer variables in the module. + * + * @return The number of integer variables in the module. */ uint_fast64_t getNumberOfIntegerVariables() const; /*! * Retrieves a reference to the integer variable with the given index. - * @returns a reference to the integer variable with the given index. + * + * @return A reference to the integer variable with the given index. */ storm::ir::IntegerVariable const& getIntegerVariable(uint_fast64_t index) const; /*! * Retrieves the number of commands of this module. - * @returns the number of commands of this module. + * + * @return the number of commands of this module. */ uint_fast64_t getNumberOfCommands() const; /*! * Retrieves the index of the boolean variable with the given name. - * @param variableName the name of the variable whose index to retrieve. - * @returns the index of the boolean variable with the given name. + * + * @param variableName The name of the boolean variable whose index to retrieve. + * @return The index of the boolean variable with the given name. */ - uint_fast64_t getBooleanVariableIndex(std::string variableName) const; + uint_fast64_t getBooleanVariableIndex(std::string const& variableName) const; /*! * Retrieves the index of the integer variable with the given name. - * @param variableName the name of the variable whose index to retrieve. - * @returns the index of the integer variable with the given name. + * + * @param variableName The name of the integer variable whose index to retrieve. + * @return The index of the integer variable with the given name. */ - uint_fast64_t getIntegerVariableIndex(std::string variableName) const; + uint_fast64_t getIntegerVariableIndex(std::string const& variableName) const; /*! * Retrieves a reference to the command with the given index. - * @returns a reference to the command with the given index. + * + * @return A reference to the command with the given index. */ - storm::ir::Command const getCommand(uint_fast64_t index) const; - + storm::ir::Command const& getCommand(uint_fast64_t index) const; + + /*! + * Retrieves the name of the module. + * + * @return The name of the module. + */ + std::string const& getName() const; + /*! - * Retrieves a string representation of this variable. - * @returns a string representation of this variable. + * Retrieves a string representation of this module. + * + * @return a string representation of this module. */ std::string toString() const; /*! * Retrieves the set of actions present in this module. - * @returns the set of actions present in this module. + * + * @return the set of actions present in this module. */ std::set const& getActions() const; /*! - * Retrieves the indices of all commands within this module that are labelled - * by the given action. - * @param action Name of the action. - * @returns Indices of all matching commands. + * Retrieves the indices of all commands within this module that are labelled by the given action. + * + * @param action The action with which the commands have to be labelled. + * @return A set of indices of commands that are labelled with the given action. */ - std::shared_ptr> const getCommandsByAction(std::string const& action) const; + std::set const& getCommandsByAction(std::string const& action) const; private: + /*! + * Computes the locally maintained mappings for fast data retrieval. + */ void collectActions(); // The name of the module. @@ -149,10 +198,10 @@ private: std::vector integerVariables; // A map of boolean variable names to their index. - std::map booleanVariablesToIndexMap; + std::map booleanVariableToLocalIndexMap; // A map of integer variable names to their index. - std::map integerVariablesToIndexMap; + std::map integerVariableToLocalIndexMap; // The commands associated with the module. std::vector commands; @@ -161,7 +210,7 @@ private: std::set actions; // A map of actions to the set of commands labeled with this action. - std::map>> actionsToCommandIndexMap; + std::map> actionsToCommandIndexMap; }; } // namespace ir diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index c854bc645..3dbc12dee 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -5,12 +5,13 @@ * Author: Christian Dehnert */ -#include "Program.h" -#include "exceptions/InvalidArgumentException.h" - #include #include +#include "Program.h" +#include "exceptions/InvalidArgumentException.h" +#include "src/exceptions/OutOfRangeException.h" + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; @@ -19,21 +20,19 @@ namespace storm { namespace ir { -// Initializes all members with their default constructors. Program::Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards(), actions(), actionsToModuleIndexMap() { // Nothing to do here. } -// Initializes all members according to the given values. Program::Program(ModelType modelType, std::map> booleanUndefinedConstantExpressions, std::map> integerUndefinedConstantExpressions, std::map> doubleUndefinedConstantExpressions, std::vector modules, std::map rewards, std::map> labels) : modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards), labels(labels), actionsToModuleIndexMap() { - // Build actionsToModuleIndexMap - for (unsigned int id = 0; id < this->modules.size(); id++) { - for (auto action : this->modules[id].getActions()) { + // Now build the mapping from action names to module indices so that the lookup can later be performed quickly. + for (unsigned int moduleId = 0; moduleId < this->modules.size(); moduleId++) { + for (auto const& action : this->modules[moduleId].getActions()) { if (this->actionsToModuleIndexMap.count(action) == 0) { this->actionsToModuleIndexMap[action] = std::set(); } - this->actionsToModuleIndexMap[action].insert(id); + this->actionsToModuleIndexMap[action].insert(moduleId); this->actions.insert(action); } } @@ -43,7 +42,6 @@ Program::ModelType Program::getModelType() const { return modelType; } -// Build a string representation of the program. std::string Program::toString() const { std::stringstream result; switch (modelType) { @@ -55,26 +53,26 @@ std::string Program::toString() const { } result << std::endl; - for (auto element : booleanUndefinedConstantExpressions) { + for (auto const& element : booleanUndefinedConstantExpressions) { result << "const bool " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; } - for (auto element : integerUndefinedConstantExpressions) { + for (auto const& element : integerUndefinedConstantExpressions) { result << "const int " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; } - for (auto element : doubleUndefinedConstantExpressions) { + for (auto const& element : doubleUndefinedConstantExpressions) { result << "const double " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; } result << std::endl; - for (auto module : modules) { + for (auto const& module : modules) { result << module.toString() << std::endl; } - for (auto rewardModel : rewards) { + for (auto const& rewardModel : rewards) { result << rewardModel.first << ": " << rewardModel.second.toString() << std::endl; } - for (auto label : labels) { + for (auto const& label : labels) { result << "label " << label.first << " = " << label.second->toString() <<";" << std::endl; } @@ -89,57 +87,32 @@ storm::ir::Module const& Program::getModule(uint_fast64_t index) const { return this->modules[index]; } -// Return set of actions. std::set const& Program::getActions() const { return this->actions; } -// Return modules with given action. -std::set const Program::getModulesByAction(std::string const& action) const { - auto res = this->actionsToModuleIndexMap.find(action); - if (res == this->actionsToModuleIndexMap.end()) { - return std::set(); - } else { - return res->second; +std::set const& Program::getModulesByAction(std::string const& action) const { + auto actionModuleSetPair = this->actionsToModuleIndexMap.find(action); + if (actionModuleSetPair == this->actionsToModuleIndexMap.end()) { + LOG4CPLUS_ERROR(logger, "Action name '" << action << "' does not exist."); + throw storm::exceptions::OutOfRangeException() << "Action name '" << action << "' does not exist."; } + return actionModuleSetPair->second; } -storm::ir::RewardModel Program::getRewardModel(std::string const & name) const { - auto it = this->rewards.find(name); - if (it == this->rewards.end()) { - LOG4CPLUS_ERROR(logger, "The given reward model \"" << name << "\" does not exist. We will proceed without rewards."); - throw "Rewardmodel does not exist."; - } else { - return it->second; +storm::ir::RewardModel const& Program::getRewardModel(std::string const& name) const { + auto nameRewardModelPair = this->rewards.find(name); + if (nameRewardModelPair == this->rewards.end()) { + LOG4CPLUS_ERROR(logger, "Reward model '" << name << "' does not exist."); + throw storm::exceptions::OutOfRangeException() << "Reward model '" << name << "' does not exist."; } + return nameRewardModelPair->second; } -std::map> Program::getLabels() const { +std::map> const& Program::getLabels() const { return this->labels; } -std::string Program::getVariableString() const { - std::map bools; - std::map ints; - uint_fast64_t maxInt = 0, maxBool = 0; - for (Module module: this->modules) { - for (uint_fast64_t i = 0; i < module.getNumberOfBooleanVariables(); i++) { - storm::ir::BooleanVariable var = module.getBooleanVariable(i); - bools[var.getIndex()] = var.getName(); - if (var.getIndex() >= maxBool) maxBool = var.getIndex()+1; - } - for (uint_fast64_t i = 0; i < module.getNumberOfIntegerVariables(); i++) { - storm::ir::IntegerVariable var = module.getIntegerVariable(i); - ints[var.getIndex()] = var.getName(); - if (var.getIndex() >= maxInt) maxInt = var.getIndex()+1; - } - } - std::stringstream ss; - for (uint_fast64_t i = 0; i < maxBool; i++) ss << bools[i] << "\t"; - for (uint_fast64_t i = 0; i < maxInt; i++) ss << ints[i] << "\t"; - return ss.str(); -} - } // namespace ir } // namepsace storm diff --git a/src/ir/Program.h b/src/ir/Program.h index c12b6dddd..145a0deb2 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -8,6 +8,11 @@ #ifndef STORM_IR_PROGRAM_H_ #define STORM_IR_PROGRAM_H_ +#include +#include +#include +#include + #include "expressions/BaseExpression.h" #include "expressions/BooleanConstantExpression.h" #include "expressions/IntegerConstantExpression.h" @@ -15,11 +20,6 @@ #include "Module.h" #include "RewardModel.h" -#include -#include -#include -#include - namespace storm { namespace ir { @@ -42,78 +42,85 @@ public: /*! * Creates a program with the given model type, undefined constants, modules, rewards and labels. - * @param modelType the type of the model that this program gives rise to. - * @param booleanUndefinedConstantExpressions a map of undefined boolean constants to their + * + * @param modelType The type of the model that this program gives rise to. + * @param booleanUndefinedConstantExpressions A map of undefined boolean constants to their * expression nodes. - * @param integerUndefinedConstantExpressions a map of undefined integer constants to their + * @param integerUndefinedConstantExpressions A map of undefined integer constants to their * expression nodes. - * @param doubleUndefinedConstantExpressions a map of undefined double constants to their + * @param doubleUndefinedConstantExpressions A map of undefined double constants to their * expression nodes. * @param modules The modules of the program. * @param rewards The reward models of the program. * @param labels The labels defined for this model. */ - Program( - ModelType modelType, - std::map> booleanUndefinedConstantExpressions, - std::map> integerUndefinedConstantExpressions, - std::map> doubleUndefinedConstantExpressions, - std::vector modules, - std::map rewards, - std::map> labels); + Program(ModelType modelType, + std::map> booleanUndefinedConstantExpressions, + std::map> integerUndefinedConstantExpressions, + std::map> doubleUndefinedConstantExpressions, + std::vector modules, + std::map rewards, + std::map> labels); /*! * Retrieves the number of modules in the program. - * @returns the number of modules in the program. + * + * @return The number of modules in the program. */ uint_fast64_t getNumberOfModules() const; /*! * Retrieves a reference to the module with the given index. - * @param index the index of the module to retrieve. + * + * @param index The index of the module to retrieve. + * @return The module with the given index. */ storm::ir::Module const& getModule(uint_fast64_t index) const; /*! * Retrieves the model type of the model. - * @returns the type of the model. + * + * @return The type of the model. */ ModelType getModelType() const; /*! * Retrieves a string representation of this program. - * @returns a string representation of this program. + * + * @return A string representation of this program. */ std::string toString() const; /*! * Retrieves the set of actions present in this module. - * @returns the set of actions present in this module. + * + * @return The set of actions present in this module. */ std::set const& getActions() const; /*! - * Retrieved the indices of all Modules within this program that contain - * commands that are labelled with the given action. - * @param action Name of the action. - * @returns Indices of all matching modules. + * Retrieves the indices of all modules within this program that contain commands that are labelled with the given + * action. + * + * @param action The name of the action the modules are supposed to possess. + * @return A set of indices of all matching modules. */ - std::set const getModulesByAction(std::string const& action) const; + std::set const& getModulesByAction(std::string const& action) const; /*! - * Retrieve reward model with given name. - * @param name Name of the reward model. - * @return Reward model with given name. + * Retrieves the reward model with the given name. + * + * @param name The name of the reward model to return. + * @return The reward model with the given name. */ - storm::ir::RewardModel getRewardModel(std::string const & name) const; + storm::ir::RewardModel const& getRewardModel(std::string const& name) const; /*! - * Retrieves all labels. - * @return All labels. + * Retrieves all labels that are defined by the probabilitic program. + * + * @return A set of labels that are defined in the program. */ - std::map> getLabels() const; - - std::string getVariableString() const; + std::map> const& getLabels() const; private: // The type of the model. diff --git a/src/ir/RewardModel.cpp b/src/ir/RewardModel.cpp index 974bf1e99..801b78515 100644 --- a/src/ir/RewardModel.cpp +++ b/src/ir/RewardModel.cpp @@ -24,10 +24,10 @@ RewardModel::RewardModel(std::string const& rewardModelName, std::vectorstateRewards.size() > 0; } -std::vector RewardModel::getStateRewards() const { +std::vector const& RewardModel::getStateRewards() const { return this->stateRewards; } @@ -46,7 +46,7 @@ bool RewardModel::hasTransitionRewards() const { return this->transitionRewards.size() > 0; } -std::vector RewardModel::getTransitionRewards() const { +std::vector const& RewardModel::getTransitionRewards() const { return this->transitionRewards; } diff --git a/src/ir/StateReward.cpp b/src/ir/StateReward.cpp index 46b2b638c..02b659635 100644 --- a/src/ir/StateReward.cpp +++ b/src/ir/StateReward.cpp @@ -17,7 +17,7 @@ StateReward::StateReward() : statePredicate(), rewardValue() { // Nothing to do here. } -StateReward::StateReward(std::shared_ptr statePredicate, std::shared_ptr rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) { +StateReward::StateReward(std::shared_ptr const& statePredicate, std::shared_ptr const& rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) { // Nothing to do here. } diff --git a/src/ir/StateReward.h b/src/ir/StateReward.h index 17e58cea5..d9d17f281 100644 --- a/src/ir/StateReward.h +++ b/src/ir/StateReward.h @@ -35,7 +35,7 @@ public: * @param rewardValue An expression specifying the values of the rewards to attach to the * states. */ - StateReward(std::shared_ptr statePredicate, std::shared_ptr rewardValue); + StateReward(std::shared_ptr const& statePredicate, std::shared_ptr const& rewardValue); /*! * Retrieves a string representation of this state reward. diff --git a/src/ir/TransitionReward.cpp b/src/ir/TransitionReward.cpp index 7bf0c645f..b32bd1b72 100644 --- a/src/ir/TransitionReward.cpp +++ b/src/ir/TransitionReward.cpp @@ -17,7 +17,7 @@ TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardVa // Nothing to do here. } -TransitionReward::TransitionReward(std::string const& commandName, std::shared_ptr statePredicate, std::shared_ptr rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) { +TransitionReward::TransitionReward(std::string const& commandName, std::shared_ptr const& statePredicate, std::shared_ptr const& rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) { // Nothing to do here. } diff --git a/src/ir/TransitionReward.h b/src/ir/TransitionReward.h index 5bb5bd63f..37f0fffdf 100644 --- a/src/ir/TransitionReward.h +++ b/src/ir/TransitionReward.h @@ -36,7 +36,7 @@ public: * @param rewardValue An expression specifying the values of the rewards to attach to the * transitions. */ - TransitionReward(std::string const& commandName, std::shared_ptr statePredicate, std::shared_ptr rewardValue); + TransitionReward(std::string const& commandName, std::shared_ptr const& statePredicate, std::shared_ptr const& rewardValue); /*! * Retrieves a string representation of this transition reward. diff --git a/src/ir/Update.cpp b/src/ir/Update.cpp index 4402354ca..51091a022 100644 --- a/src/ir/Update.cpp +++ b/src/ir/Update.cpp @@ -19,24 +19,24 @@ Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignme // Nothing to do here. } -Update::Update(std::shared_ptr likelihoodExpression, std::map booleanAssignments, std::map integerAssignments) +Update::Update(std::shared_ptr const& likelihoodExpression, std::map const& booleanAssignments, std::map const& integerAssignments) : likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments) { // Nothing to do here. } Update::Update(Update const& update, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap) { - for (auto it : update.booleanAssignments) { - if (renaming.count(it.first) > 0) { - this->booleanAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); + for (auto const& variableAssignmentPair : update.booleanAssignments) { + if (renaming.count(variableAssignmentPair.first) > 0) { + this->booleanAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); } else { - this->booleanAssignments[it.first] = Assignment(it.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); + this->booleanAssignments[variableAssignmentPair.first] = Assignment(variableAssignmentPair.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); } } - for (auto it : update.integerAssignments) { - if (renaming.count(it.first) > 0) { - this->integerAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); + for (auto const& variableAssignmentPair : update.integerAssignments) { + if (renaming.count(variableAssignmentPair.first) > 0) { + this->integerAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); } else { - this->integerAssignments[it.first] = Assignment(it.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); + this->integerAssignments[variableAssignmentPair.first] = Assignment(variableAssignmentPair.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); } } this->likelihoodExpression = update.likelihoodExpression->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap); @@ -62,31 +62,31 @@ std::map const& Update::getIntegerAssignment return integerAssignments; } -storm::ir::Assignment const& Update::getBooleanAssignment(std::string variableName) const { - auto it = booleanAssignments.find(variableName); - if (it == booleanAssignments.end()) { +storm::ir::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->toString() << "."; } - return (*it).second; + return variableAssignmentPair->second; } -storm::ir::Assignment const& Update::getIntegerAssignment(std::string variableName) const { - auto it = integerAssignments.find(variableName); - if (it == integerAssignments.end()) { +storm::ir::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->toString() << "."; } - return (*it).second; + return variableAssignmentPair->second; } std::string Update::toString() const { std::stringstream result; result << likelihoodExpression->toString() << " : "; uint_fast64_t i = 0; - for (auto assignment : booleanAssignments) { + for (auto const& assignment : booleanAssignments) { result << assignment.second.toString(); if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) { result << " & "; @@ -94,7 +94,7 @@ std::string Update::toString() const { ++i; } i = 0; - for (auto assignment : integerAssignments) { + for (auto const& assignment : integerAssignments) { result << assignment.second.toString(); if (i < integerAssignments.size() - 1) { result << " & "; diff --git a/src/ir/Update.h b/src/ir/Update.h index cd19a03a4..505277504 100644 --- a/src/ir/Update.h +++ b/src/ir/Update.h @@ -35,7 +35,7 @@ public: * @param likelihoodExpression An expression specifying the likelihood of this update. * @param assignments A map of variable names to their assignments. */ - Update(std::shared_ptr likelihoodExpression, std::map booleanAssignments, std::map integerAssignments); + Update(std::shared_ptr const& likelihoodExpression, std::map const& booleanAssignments, std::map const& integerAssignments); /*! * Creates a copy of the given update and performs the provided renaming. @@ -88,14 +88,14 @@ public: * * @return A reference to the assignment for the boolean variable with the given name. */ - storm::ir::Assignment const& getBooleanAssignment(std::string variableName) const; + storm::ir::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::ir::Assignment const& getIntegerAssignment(std::string variableName) const; + storm::ir::Assignment const& getIntegerAssignment(std::string const& variableName) const; /*! * Retrieves a string representation of this update. diff --git a/src/ir/Variable.cpp b/src/ir/Variable.cpp index 9e45c1cd1..7a87dfd10 100644 --- a/src/ir/Variable.cpp +++ b/src/ir/Variable.cpp @@ -19,12 +19,12 @@ Variable::Variable() : globalIndex(0), localIndex(0), variableName(), initialVal // Nothing to do here. } -Variable::Variable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string variableName, std::shared_ptr initialValue) +Variable::Variable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string const& variableName, std::shared_ptr const& initialValue) : globalIndex(globalIndex), localIndex(localIndex), variableName(variableName), initialValue(initialValue) { // Nothing to do here. } -Variable::Variable(Variable const& var, std::string const& newName, uint_fast64_t const newGlobalIndex, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap) +Variable::Variable(Variable const& var, std::string const& newName, uint_fast64_t newGlobalIndex, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap) : globalIndex(newGlobalIndex), localIndex(var.getLocalIndex()), variableName(var.getName()) { if (var.initialValue != nullptr) { this->initialValue = var.initialValue->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap); diff --git a/src/ir/Variable.h b/src/ir/Variable.h index 05d356e98..41f750a2d 100644 --- a/src/ir/Variable.h +++ b/src/ir/Variable.h @@ -34,10 +34,10 @@ public: * @param variableName the name of the variable. * @param initialValue the expression that defines the initial value of the variable. */ - Variable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string variableName, std::shared_ptr initialValue = std::shared_ptr()); + Variable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string const& variableName, std::shared_ptr const& initialValue = std::shared_ptr()); /*! - * Creates a copy of the given Variable and performs the provided renaming. + * Creates a copy of the given variable and performs the provided renaming. * * @param oldVariable The variable to copy. * @param newName New name of this variable. @@ -47,7 +47,7 @@ public: * @param booleanVariableToIndexMap A mapping from boolean variable names to their global indices. * @param integerVariableToIndexMap A mapping from integer variable names to their global indices. */ - Variable(const Variable& oldVariable, const std::string& newName, const uint_fast64_t newGlobalIndex, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap); + Variable(Variable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap); /*! * Retrieves the name of the variable. diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index 7189c8a03..736fce64a 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -81,7 +81,7 @@ Module PrismGrammar::createModule(const std::string name, std::vector lower, std::shared_ptr upper, std::shared_ptr init, std::vector& vars, std::map& varids) { //std::cout << "Creating int " << name << " = " << init << std::endl; - uint_fast64_t id = this->state->addIntegerVariable(name, lower, upper); + uint_fast64_t id = this->state->addIntegerVariable(name); vars.emplace_back(id, name, lower, upper, init); varids[name] = id; this->state->localIntegerVariables_.add(name, name); @@ -181,7 +181,7 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl variableDefinition.name("variable declaration"); // This block defines all entities that are needed for parsing a module. - moduleDefinition = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&VariableState::startModule, *this->state)] + moduleDefinition = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&VariableState::clearLocalVariables, *this->state)] >> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule")) [qi::_val = phoenix::bind(&PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)]; diff --git a/src/parser/prismparser/VariableState.cpp b/src/parser/prismparser/VariableState.cpp index e9be69435..1bdf7b0e0 100644 --- a/src/parser/prismparser/VariableState.cpp +++ b/src/parser/prismparser/VariableState.cpp @@ -1,4 +1,5 @@ #include "VariableState.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace parser { @@ -30,131 +31,110 @@ std::ostream& operator<<(std::ostream& out, VariableState::variableNamesStruct& } -VariableState::VariableState(bool firstRun) - : firstRun(firstRun), keywords(), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0) { +VariableState::VariableState(bool firstRun) : firstRun(firstRun), keywords(), nextGlobalBooleanVariableIndex(0), nextGlobalIntegerVariableIndex(0) { + // Nothing to do here. } -uint_fast64_t VariableState::addBooleanVariable(const std::string& name) { +uint_fast64_t VariableState::getNextGlobalBooleanVariableIndex() const { + return this->nextGlobalBooleanVariableIndex; +} + +uint_fast64_t VariableState::getNextGlobalIntegerVariableIndex() const { + return this->nextGlobalIntegerVariableIndex; +} + +uint_fast64_t VariableState::addBooleanVariable(std::string const& name) { if (firstRun) { - std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextBooleanVariableIndex, name)); - LOG4CPLUS_TRACE(logger, "Adding boolean variable " << name << " with new id " << this->nextBooleanVariableIndex); - this->booleanVariables_.add(name, varExpr); + 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->nextBooleanVariableIndex++; - return varExpr->getVariableIndex(); + ++this->nextGlobalBooleanVariableIndex; + return this->nextGlobalBooleanVariableIndex - 1; } else { std::shared_ptr res = this->booleanVariables_.at(name); if (res != nullptr) { return res->getVariableIndex(); } else { - LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " was not created in first run."); - return 0; + LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist."); + throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist."; } } } -uint_fast64_t VariableState::addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper) { +uint_fast64_t VariableState::addIntegerVariable(std::string const& name) { if (firstRun) { - std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextIntegerVariableIndex, name, lower, upper)); - LOG4CPLUS_TRACE(logger, "Adding integer variable " << name << " with new id " << this->nextIntegerVariableIndex); - this->integerVariables_.add(name, varExpr); + 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->nextIntegerVariableIndex++; - return varExpr->getVariableIndex(); + ++this->nextGlobalIntegerVariableIndex; + return this->nextGlobalIntegerVariableIndex - 1; } else { std::shared_ptr res = this->integerVariables_.at(name); if (res != nullptr) { return res->getVariableIndex(); } else { - - LOG4CPLUS_ERROR(logger, "Integer variable " << name << " was not created in first run."); - return 0; + LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist."); + throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist."; } } } -std::shared_ptr VariableState::getBooleanVariable(const std::string& name) { +std::shared_ptr VariableState::getBooleanVariableExpression(std::string const& name) { std::shared_ptr* res = this->booleanVariables_.find(name); if (res != nullptr) { return *res; } else { if (firstRun) { - LOG4CPLUS_TRACE(logger, "Getting boolean variable " << name << ", was not yet created."); - return std::shared_ptr(new VariableExpression(BaseExpression::bool_, std::numeric_limits::max(), "bool", std::shared_ptr(nullptr), std::shared_ptr(nullptr))); - } else { - LOG4CPLUS_ERROR(logger, "Getting boolean variable " << name << ", but was not found. This variable does not exist."); + LOG4CPLUS_TRACE(logger, "Trying to retrieve boolean variable " << name << " that was not yet created; returning dummy instead."); return std::shared_ptr(nullptr); + } else { + LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist."); + throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist."; } } } -std::shared_ptr VariableState::getIntegerVariable(const std::string& name) { +std::shared_ptr VariableState::getIntegerVariableExpression(std::string const& name) { std::shared_ptr* res = this->integerVariables_.find(name); if (res != nullptr) { return *res; } else { if (firstRun) { - LOG4CPLUS_TRACE(logger, "Getting integer variable " << name << ", was not yet created."); - return std::shared_ptr(new VariableExpression(BaseExpression::int_, std::numeric_limits::max(), "int", std::shared_ptr(nullptr), std::shared_ptr(nullptr))); - } else { - LOG4CPLUS_ERROR(logger, "Getting integer variable " << name << ", but was not found. This variable does not exist."); + LOG4CPLUS_TRACE(logger, "Trying to retrieve integer variable " << name << " that was not yet created; returning dummy instead."); return std::shared_ptr(nullptr); + } else { + LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist."); + throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist."; } } } -std::shared_ptr VariableState::getVariable(const std::string& name) { + +std::shared_ptr VariableState::getVariableExpression(std::string const& name) { std::shared_ptr* res = this->integerVariables_.find(name); if (res != nullptr) { return *res; - } else { - res = this->booleanVariables_.find(name); - if (res != nullptr) { - return *res; - } else { - return std::shared_ptr(nullptr); - } - } -} - -void VariableState::performRenaming(const std::map& renaming) { - for (auto it: renaming) { - std::shared_ptr* original = this->integerVariables_.find(it.first); - if (original != nullptr) { - std::shared_ptr* next = this->integerVariables_.find(it.second); - if (next == nullptr) { - this->addIntegerVariable(it.second, (*original)->getLowerBound(), (*original)->getUpperBound()); - } - } - original = this->booleanVariables_.find(it.first); - if (original != nullptr) { - if (this->booleanVariables_.find(it.second) == nullptr) { - this->addBooleanVariable(it.second); - } - } - std::string* oldCmdName = this->commandNames_.find(it.first); - if (oldCmdName != nullptr) { - LOG4CPLUS_TRACE(logger, "Adding new command name " << it.second << " due to module renaming."); - this->commandNames_.at(it.second) = it.second; - } } + LOG4CPLUS_ERROR(logger, "Variable " << name << " does not exist."); + throw storm::exceptions::InvalidArgumentException() << "Variable " << name << " does not exist."; } -void VariableState::startModule() { +void VariableState::clearLocalVariables() { this->localBooleanVariables_.clear(); this->localIntegerVariables_.clear(); } -bool VariableState::isFreeIdentifier(std::string& s) const { - if (this->integerVariableNames_.find(s) != nullptr) return false; - if (this->allConstantNames_.find(s) != nullptr) return false; - if (this->labelNames_.find(s) != nullptr) return false; - if (this->moduleNames_.find(s) != nullptr) return false; - if (this->keywords.find(s) != nullptr) return false; +bool VariableState::isFreeIdentifier(std::string const& identifier) const { + 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; return true; } -bool VariableState::isIdentifier(std::string& s) const { - if (this->allConstantNames_.find(s) != nullptr) return false; - if (this->keywords.find(s) != nullptr) return false; + +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; } @@ -166,6 +146,6 @@ void VariableState::prepareForSecondRun() { this->firstRun = false; } -} -} -} +} // namespace prism +} // namespace parser +} // namespace storm diff --git a/src/parser/prismparser/VariableState.h b/src/parser/prismparser/VariableState.h index 1d13cc270..953f46d2b 100644 --- a/src/parser/prismparser/VariableState.h +++ b/src/parser/prismparser/VariableState.h @@ -8,13 +8,16 @@ #ifndef VARIABLESTATE_H #define VARIABLESTATE_H +#include + #include "src/ir/IR.h" #include "Includes.h" #include "Tokens.h" -#include namespace storm { + namespace parser { + namespace prism { using namespace storm::ir; @@ -34,6 +37,7 @@ struct VariableState : public storm::ir::VariableAdder { * Indicator, if we are still in the first run. */ bool firstRun; + /*! * A parser for all reserved keywords. */ @@ -42,91 +46,107 @@ struct VariableState : public storm::ir::VariableAdder { /*! * Internal counter for the index of the next new boolean variable. */ - uint_fast64_t nextBooleanVariableIndex; + 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 nextIntegerVariableIndex; - + 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; + // 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_; // A structure representing the identity function over identifier names. - struct variableNamesStruct : qi::symbols { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_, + struct variableNamesStruct : qi::symbols { } + integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_, localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_; /*! - * Add a new boolean variable with the given name. - * @param name Name of the variable. - * @return Index of the variable. + * 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(const std::string& name); + uint_fast64_t addBooleanVariable(std::string const& 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. + * 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(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper); + uint_fast64_t addIntegerVariable(std::string const& name); /*! - * Retrieve boolean Variable with given name. - * @param name Variable name. - * @returns Variable. + * 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 getBooleanVariable(const std::string& name); + std::shared_ptr getBooleanVariableExpression(std::string const& name); + /*! - * Retrieve integer Variable with given name. - * @param name Variable name. - * @returns Variable. + * 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 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); - + std::shared_ptr getIntegerVariableExpression(std::string const& name); + /*! - * Perform operations necessary for a module renaming. - * This includes creating new variables and constants. - * @param renaming String mapping for renaming operation. + * 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. */ - void performRenaming(const std::map& renaming); + std::shared_ptr getVariableExpression(std::string const& name); /*! - * Start with a new module. - * Clears sets of local variables. + * Clears all local variables. */ - void startModule(); + void clearLocalVariables(); /*! - * Check if given string is a free identifier. - * @param s String. - * @returns If s is a free identifier. + * 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& s) const; + bool isFreeIdentifier(std::string const& identifier) const; + /*! * Check if given string is a valid identifier. - * @param s String. - * @returns If s is a valid identifier. + * + * @param identifier A string to be checked. + * @return True iff the given string is an identifier. */ - bool isIdentifier(std::string& s) const; + bool isIdentifier(std::string const& identifier) const; /*! - * Prepare state to proceed to second parser run. - * Clears constants. + * Prepare state to proceed to second parser run. Currently, this clears the constants. */ void prepareForSecondRun(); }; -} -} -} +} // namespace prism +} // namespace parser +} // namespace storm #endif /* VARIABLESTATE_H */