From 7b8b1ebd4ffb00490f118a363032dd839209b027 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 10 Jun 2013 21:25:10 +0200 Subject: [PATCH] Further refactoring of IR classes. --- src/adapters/ExplicitModelAdapter.cpp | 32 +- src/ir/Assignment.cpp | 71 ++-- src/ir/Assignment.h | 128 +++---- src/ir/BooleanVariable.cpp | 57 ++- src/ir/BooleanVariable.h | 94 ++--- src/ir/Command.cpp | 115 +++--- src/ir/Command.h | 166 ++++----- src/ir/IntegerVariable.cpp | 77 ++-- src/ir/IntegerVariable.h | 136 +++---- src/ir/Module.cpp | 306 ++++++++-------- src/ir/Module.h | 338 +++++++++--------- src/ir/Program.cpp | 192 +++++----- src/ir/Program.h | 262 +++++++------- src/ir/RewardModel.cpp | 82 +++-- src/ir/RewardModel.h | 138 ++++--- src/ir/StateReward.cpp | 8 + src/ir/StateReward.h | 16 +- src/ir/TransitionReward.cpp | 12 + src/ir/TransitionReward.h | 21 ++ src/ir/Update.cpp | 184 +++++----- src/ir/Update.h | 208 +++++------ src/ir/Variable.cpp | 81 +++-- src/ir/Variable.h | 178 ++++----- src/ir/expressions/BaseExpression.h | 4 +- .../BinaryBooleanFunctionExpression.cpp | 2 +- .../BinaryBooleanFunctionExpression.h | 4 +- .../BinaryNumericalFunctionExpression.cpp | 2 +- .../BinaryNumericalFunctionExpression.h | 2 +- .../expressions/BinaryRelationExpression.cpp | 2 +- src/ir/expressions/BinaryRelationExpression.h | 2 +- .../expressions/BooleanConstantExpression.cpp | 2 +- .../expressions/BooleanConstantExpression.h | 2 +- .../expressions/BooleanLiteralExpression.cpp | 2 +- src/ir/expressions/BooleanLiteralExpression.h | 2 +- src/ir/expressions/ConstantExpression.cpp | 6 +- src/ir/expressions/ConstantExpression.h | 4 +- .../expressions/DoubleConstantExpression.cpp | 14 +- src/ir/expressions/DoubleConstantExpression.h | 7 +- .../expressions/DoubleLiteralExpression.cpp | 10 +- src/ir/expressions/DoubleLiteralExpression.h | 4 +- src/ir/expressions/Expressions.h | 6 +- .../expressions/IntegerConstantExpression.cpp | 59 +++ .../expressions/IntegerConstantExpression.h | 133 +++---- src/ir/expressions/IntegerLiteral.h | 57 --- .../expressions/IntegerLiteralExpression.cpp | 40 +++ src/ir/expressions/IntegerLiteralExpression.h | 46 +++ .../UnaryBooleanFunctionExpression.cpp | 56 +++ .../UnaryBooleanFunctionExpression.h | 124 +++---- src/ir/expressions/UnaryExpression.cpp | 24 ++ src/ir/expressions/UnaryExpression.h | 52 +-- .../UnaryNumericalFunctionExpression.cpp | 69 ++++ .../UnaryNumericalFunctionExpression.h | 144 +++----- src/ir/expressions/VariableExpression.cpp | 43 +-- src/ir/expressions/VariableExpression.h | 69 ++-- src/parser/prismparser/BaseGrammar.h | 10 +- src/parser/prismparser/PrismGrammar.cpp | 24 +- src/parser/prismparser/PrismGrammar.h | 8 +- src/parser/prismparser/VariableState.cpp | 22 +- src/parser/prismparser/VariableState.h | 12 +- 59 files changed, 2100 insertions(+), 1871 deletions(-) create mode 100644 src/ir/expressions/IntegerConstantExpression.cpp delete mode 100644 src/ir/expressions/IntegerLiteral.h create mode 100644 src/ir/expressions/IntegerLiteralExpression.cpp create mode 100644 src/ir/expressions/IntegerLiteralExpression.h create mode 100644 src/ir/expressions/UnaryBooleanFunctionExpression.cpp create mode 100644 src/ir/expressions/UnaryExpression.cpp create mode 100644 src/ir/expressions/UnaryNumericalFunctionExpression.cpp diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index b7aef607c..54c885b11 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -107,13 +107,15 @@ namespace adapters { return ss.str(); } - std::shared_ptr> ExplicitModelAdapter::getStateRewards(std::vector const & rewards) { + std::shared_ptr> ExplicitModelAdapter::getStateRewards(std::vector const& rewards) { std::shared_ptr> results(new std::vector(this->allStates.size())); for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { (*results)[index] = 0; for (auto reward: rewards) { - // Add this reward to the state. - (*results)[index] += reward.getReward(this->allStates[index]); + // Add this reward to the state if the state is included in the state reward. + if (reward.getStatePredicate()->getValueAsBool(this->allStates[index]) == true) { + (*results)[index] += reward.getRewardValue()->getValueAsDouble(this->allStates[index]); + } } } return results; @@ -154,13 +156,13 @@ namespace adapters { for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { storm::ir::BooleanVariable var = module.getBooleanVariable(j); - this->booleanVariables[var.getIndex()] = var; - this->booleanVariableToIndexMap[var.getName()] = var.getIndex(); + this->booleanVariables[var.getGlobalIndex()] = var; + this->booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); } for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { storm::ir::IntegerVariable var = module.getIntegerVariable(j); - this->integerVariables[var.getIndex()] = var; - this->integerVariableToIndexMap[var.getName()] = var.getIndex(); + this->integerVariables[var.getGlobalIndex()] = var; + this->integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); } } } @@ -185,13 +187,13 @@ namespace adapters { for (uint_fast64_t i = 0; i < this->program.getNumberOfModules(); ++i) { storm::ir::Module const& module = this->program.getModule(i); - std::shared_ptr> ids = module.getCommandsByAction(action); - if (ids->size() == 0) continue; + std::set const& ids = module.getCommandsByAction(action); + if (ids.size() == 0) continue; std::list commands; // Look up commands by their id. Add, if guard holds. - for (uint_fast64_t id : *ids) { - storm::ir::Command cmd = module.getCommand(id); + for (uint_fast64_t id : ids) { + storm::ir::Command const& cmd = module.getCommand(id); if (cmd.getGuard()->getValueAsBool(state)) { commands.push_back(module.getCommand(id)); } @@ -468,7 +470,9 @@ namespace adapters { map[elem.first] += elem.second; if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { for (auto reward : this->rewardModel->getTransitionRewards()) { - rewardMap[elem.first] += reward.getReward(choice.first, this->allStates[state]); + if (reward.getStatePredicate()->getValueAsBool(this->allStates[state]) == true) { + rewardMap[elem.first] += reward.getRewardValue()->getValueAsDouble(this->allStates[state]); + } } } } @@ -513,7 +517,9 @@ namespace adapters { if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { double rewardValue = 0; for (auto reward : this->rewardModel->getTransitionRewards()) { - rewardValue = reward.getReward(choice.first, this->allStates[state]); + if (reward.getStatePredicate()->getValueAsBool(this->allStates[state]) == true) { + rewardValue = reward.getRewardValue()->getValueAsDouble(this->allStates[state]); + } } this->transitionRewards->addNextValue(nextRow, it.first, rewardValue); } diff --git a/src/ir/Assignment.cpp b/src/ir/Assignment.cpp index 6182fda6b..60a776b49 100644 --- a/src/ir/Assignment.cpp +++ b/src/ir/Assignment.cpp @@ -8,42 +8,41 @@ #include #include "Assignment.h" +#include "src/parser/prismparser/VariableState.h" namespace storm { - -namespace ir { - -Assignment::Assignment() : variableName(), expression() { - // Nothing to do here. -} - -Assignment::Assignment(std::string const& variableName, std::shared_ptr const& expression) - : variableName(variableName), expression(expression) { - // Nothing to do here. -} - -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; - } -} - -std::string const& Assignment::getVariableName() const { - return variableName; -} - -std::shared_ptr const& Assignment::getExpression() const { - return expression; -} - -std::string Assignment::toString() const { - std::stringstream result; - result << "(" << variableName << "' = " << expression->toString() << ")"; - return result.str(); -} - -} // namespace ir - + namespace ir { + + Assignment::Assignment() : variableName(), expression() { + // Nothing to do here. + } + + Assignment::Assignment(std::string const& variableName, std::shared_ptr const& expression) + : variableName(variableName), expression(expression) { + // Nothing to do here. + } + + Assignment::Assignment(Assignment const& oldAssignment, std::map const& renaming, storm::parser::prism::VariableState const& variableState) + : variableName(oldAssignment.variableName), expression(oldAssignment.expression->clone(renaming, variableState)) { + auto renamingPair = renaming.find(oldAssignment.variableName); + if (renamingPair != renaming.end()) { + this->variableName = renamingPair->second; + } + } + + std::string const& Assignment::getVariableName() const { + return variableName; + } + + std::shared_ptr const& Assignment::getExpression() const { + return expression; + } + + std::string Assignment::toString() const { + std::stringstream result; + result << "(" << variableName << "' = " << expression->toString() << ")"; + return result.str(); + } + + } // namespace ir } // namespace storm diff --git a/src/ir/Assignment.h b/src/ir/Assignment.h index 2c37f995e..caf7c520c 100644 --- a/src/ir/Assignment.h +++ b/src/ir/Assignment.h @@ -13,68 +13,72 @@ #include "expressions/BaseExpression.h" namespace storm { - -namespace ir { - -/*! - * A class representing the assignment of an expression to a variable. - */ -class Assignment { -public: - /*! - * Default constructor. Creates an empty assignment. - */ - Assignment(); - - /*! - * 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. - */ - 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. - * - * @return The name of the variable that this assignment targets. - */ - std::string const& getVariableName() const; - - /*! - * Retrieves the expression that is assigned to the variable. - * - * @return The expression that is assigned to the variable. - */ - std::shared_ptr const& getExpression() const; - - /*! - * Retrieves a string representation of this assignment. - * @returns a string representation of this assignment. - */ - std::string toString() const; - -private: - // The name of the variable that this assignment targets. - std::string variableName; - - // The expression that is assigned to the variable. - std::shared_ptr expression; -}; - -} // namespace ir - + + namespace parser { + namespace prism { + class VariableState; + } // namespace prismparser + } // namespace parser + + namespace ir { + + /*! + * A class representing the assignment of an expression to a variable. + */ + class Assignment { + public: + /*! + * Default constructor. Creates an empty assignment. + */ + Assignment(); + + /*! + * 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. + */ + 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 variableState An object knowing about the variables in the system. + */ + Assignment(Assignment const& oldAssignment, std::map const& renaming, storm::parser::prism::VariableState const& variableState); + + /*! + * Retrieves 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. + * + * @return The expression that is assigned to the variable. + */ + std::shared_ptr const& getExpression() const; + + /*! + * Retrieves a string representation of this assignment. + * @returns a string representation of this assignment. + */ + std::string toString() const; + + private: + // The name of the variable that this assignment targets. + std::string variableName; + + // The expression that is assigned to the variable. + std::shared_ptr expression; + }; + + } // namespace ir } // namespace storm #endif /* STORM_IR_ASSIGNMENT_H_ */ diff --git a/src/ir/BooleanVariable.cpp b/src/ir/BooleanVariable.cpp index 1a660ac0e..f673633a1 100644 --- a/src/ir/BooleanVariable.cpp +++ b/src/ir/BooleanVariable.cpp @@ -8,35 +8,34 @@ #include #include "BooleanVariable.h" +#include "src/parser/prismparser/VariableState.h" namespace storm { - -namespace ir { - -BooleanVariable::BooleanVariable() : Variable() { - // Nothing to do here. -} - -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(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. -} - -std::string BooleanVariable::toString() const { - std::stringstream result; - result << this->getName() << ": bool"; - if (this->getInitialValue() != nullptr) { - result << " init " << this->getInitialValue()->toString(); - } - result << ";"; - return result.str(); -} - -} // namespace ir - + namespace ir { + + BooleanVariable::BooleanVariable() : Variable() { + // Nothing to do here. + } + + BooleanVariable::BooleanVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr const& initialValue) + : Variable(localIndex, globalIndex, variableName, initialValue) { + // Nothing to do here. + } + + BooleanVariable::BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState const& variableState) + : Variable(oldVariable, newName, newGlobalIndex, renaming, variableState) { + // Nothing to do here. + } + + std::string BooleanVariable::toString() const { + std::stringstream result; + result << this->getName() << ": bool"; + if (this->getInitialValue() != nullptr) { + result << " init " << this->getInitialValue()->toString(); + } + result << ";"; + return result.str(); + } + + } // namespace ir } // namespace storm diff --git a/src/ir/BooleanVariable.h b/src/ir/BooleanVariable.h index 4084d959d..491be1c6f 100644 --- a/src/ir/BooleanVariable.h +++ b/src/ir/BooleanVariable.h @@ -14,51 +14,55 @@ #include "src/ir/Variable.h" namespace storm { - -namespace ir { - -/*! - * A class representing a boolean variable. - */ -class BooleanVariable : public Variable { -public: - /*! - * Default constructor. Creates a boolean variable without a name. - */ - BooleanVariable(); - - /*! - * 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 initialValue The expression that defines the initial value of the variable. - */ - BooleanVariable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string const& variableName, std::shared_ptr const& initialValue = std::shared_ptr(nullptr)); - - /*! - * 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. - * @returns a string representation of this variable. - */ - std::string toString() const; -}; - -} // namespace ir - + + namespace parser { + namespace prism { + class VariableState; + } // namespace prismparser + } // namespace parser + + namespace ir { + + /*! + * A class representing a boolean variable. + */ + class BooleanVariable : public Variable { + public: + /*! + * Default constructor. Creates a boolean variable without a name. + */ + BooleanVariable(); + + /*! + * Creates a boolean variable with the given name and the given initial value. + * + * @param localIndex A module-local unique index for the variable. + * @param globalIndex A globally 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 localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr const& initialValue = std::shared_ptr(nullptr)); + + /*! + * 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 variableState An object knowing about the variables in the system. + */ + BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState const& variableState); + + /*! + * Retrieves a string representation of this variable. + * @returns a string representation of this variable. + */ + std::string toString() const; + }; + + } // namespace ir } // namespace storm #endif /* STORM_IR_BOOLEANVARIABLE_H_ */ diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp index 673ce1b5e..b1e4fe8ef 100644 --- a/src/ir/Command.cpp +++ b/src/ir/Command.cpp @@ -5,67 +5,64 @@ * Author: Christian Dehnert */ -#include "Command.h" - #include #include -namespace storm { - -namespace ir { - -// Initializes all members with their default constructors. -Command::Command() : actionName(), guardExpression(), updates() { - // Nothing to do here. -} - -// Initializes all members according to the given values. -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(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(oldCommand.getNumberOfUpdates()); - for (Update const& update : oldCommand.updates) { - this->updates.emplace_back(update, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); - } -} - -std::string const& Command::getActionName() const { - return this->actionName; -} - -std::shared_ptr const& Command::getGuard() const { - return guardExpression; -} - -uint_fast64_t Command::getNumberOfUpdates() const { - return this->updates.size(); -} - -storm::ir::Update const& Command::getUpdate(uint_fast64_t index) const { - return this->updates[index]; -} - -std::string Command::toString() const { - std::stringstream result; - result << "[" << actionName << "] " << guardExpression->toString() << " -> "; - for (uint_fast64_t i = 0; i < updates.size(); ++i) { - result << updates[i].toString(); - if (i < updates.size() - 1) { - result << " + "; - } - } - result << ";"; - return result.str(); -} - -} // namespace ir +#include "Command.h" +#include "src/parser/prismparser/VariableState.h" +namespace storm { + namespace ir { + + Command::Command() : actionName(), guardExpression(), updates() { + // Nothing to do here. + } + + 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(Command const& oldCommand, std::map const& renaming, storm::parser::prism::VariableState const& variableState) + : actionName(oldCommand.getActionName()), guardExpression(oldCommand.guardExpression->clone(renaming, variableState)) { + auto renamingPair = renaming.find(this->actionName); + if (renamingPair != renaming.end()) { + this->actionName = renamingPair->first; + } + this->updates.reserve(oldCommand.getNumberOfUpdates()); + for (Update const& update : oldCommand.updates) { + this->updates.emplace_back(update, renaming, variableState); + } + } + + std::string const& Command::getActionName() const { + return this->actionName; + } + + std::shared_ptr const& Command::getGuard() const { + return guardExpression; + } + + uint_fast64_t Command::getNumberOfUpdates() const { + return this->updates.size(); + } + + storm::ir::Update const& Command::getUpdate(uint_fast64_t index) const { + return this->updates[index]; + } + + std::string Command::toString() const { + std::stringstream result; + result << "[" << actionName << "] " << guardExpression->toString() << " -> "; + for (uint_fast64_t i = 0; i < updates.size(); ++i) { + result << updates[i].toString(); + if (i < updates.size() - 1) { + result << " + "; + } + } + result << ";"; + return result.str(); + } + + } // namespace ir } // namespace storm diff --git a/src/ir/Command.h b/src/ir/Command.h index 25fcb34ce..c2045afd8 100644 --- a/src/ir/Command.h +++ b/src/ir/Command.h @@ -16,87 +16,91 @@ #include "Update.h" namespace storm { - -namespace ir { - -/*! - * A class representing a command. - */ -class Command { -public: - /*! - * Default constructor. Creates a a command without name, guard and updates. - */ - Command(); - - /*! - * Creates a command with the given name, guard and updates. - * - * @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(Command const& oldCommand, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap); - - /*! - * Retrieves 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. - * - * @return A reference to the guard of the command. - */ - std::shared_ptr const& getGuard() const; - - /*! - * Retrieves 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. - * - * @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. - * - * @return A string representation of this command. - */ - std::string toString() const; - -private: - // The name of the command. - std::string actionName; - - // The expression that defines the guard of the command. - std::shared_ptr guardExpression; - - // The list of updates of the command. - std::vector updates; -}; - -} // namespace ir - + + namespace parser { + namespace prism { + class VariableState; + } // namespace prismparser + } // namespace parser + + namespace ir { + + /*! + * A class representing a command. + */ + class Command { + public: + /*! + * Default constructor. Creates a a command without name, guard and updates. + */ + Command(); + + /*! + * Creates a command with the given name, guard and updates. + * + * @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 variableState An object knowing about the variables in the system. + */ + Command(Command const& oldCommand, std::map const& renaming, storm::parser::prism::VariableState const& variableState); + + /*! + * Retrieves 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. + * + * @return A reference to the guard of the command. + */ + std::shared_ptr const& getGuard() const; + + /*! + * Retrieves 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. + * + * @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. + * + * @return A string representation of this command. + */ + std::string toString() const; + + private: + // The name of the command. + std::string actionName; + + // The expression that defines the guard of the command. + std::shared_ptr guardExpression; + + // The list of updates of the command. + std::vector updates; + }; + + } // namespace ir } // namespace storm #endif /* STORM_IR_COMMAND_H_ */ diff --git a/src/ir/IntegerVariable.cpp b/src/ir/IntegerVariable.cpp index 4e70820e6..8b4902ce7 100644 --- a/src/ir/IntegerVariable.cpp +++ b/src/ir/IntegerVariable.cpp @@ -9,44 +9,45 @@ #include #include "IntegerVariable.h" +#include "src/parser/prismparser/VariableState.h" namespace storm { - -namespace ir { - -IntegerVariable::IntegerVariable() : lowerBound(), upperBound() { - // Nothing to do here. -} - -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(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)) { -} - -std::shared_ptr IntegerVariable::getLowerBound() const { - return this->lowerBound; -} - -std::shared_ptr IntegerVariable::getUpperBound() const { - return this->upperBound; -} - -std::string IntegerVariable::toString() const { - std::stringstream result; - result << this->getName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]"; - if (this->getInitialValue() != nullptr) { - result << " init " + this->getInitialValue()->toString(); - } - result << ";"; - return result.str(); -} - -} // namespace ir - + + namespace ir { + + IntegerVariable::IntegerVariable() : lowerBound(), upperBound() { + // Nothing to do here. + } + + IntegerVariable::IntegerVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue) + : Variable(localIndex, globalIndex, variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) { + if (this->getInitialValue() == nullptr) { + this->setInitialValue(lowerBound); + } + } + + IntegerVariable::IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState const& variableState) + : Variable(oldVariable, newName, newGlobalIndex, renaming, variableState), lowerBound(oldVariable.lowerBound->clone(renaming, variableState)), upperBound(oldVariable.upperBound->clone(renaming, variableState)) { + } + + std::shared_ptr IntegerVariable::getLowerBound() const { + return this->lowerBound; + } + + std::shared_ptr IntegerVariable::getUpperBound() const { + return this->upperBound; + } + + std::string IntegerVariable::toString() const { + std::stringstream result; + result << this->getName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]"; + if (this->getInitialValue() != nullptr) { + result << " init " + this->getInitialValue()->toString(); + } + result << ";"; + return result.str(); + } + + } // namespace ir + } // namespace storm diff --git a/src/ir/IntegerVariable.h b/src/ir/IntegerVariable.h index cd1b2cba4..cd1c20be4 100644 --- a/src/ir/IntegerVariable.h +++ b/src/ir/IntegerVariable.h @@ -14,72 +14,76 @@ #include "expressions/BaseExpression.h" namespace storm { - -namespace ir { - -/*! - * A class representing an integer variable. - */ -class IntegerVariable : public Variable { -public: - /*! - * Default constructor. Creates an integer variable without a name and lower and upper bounds. - */ - IntegerVariable(); - - /*! - * 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 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)); - - /*! - * 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. - * @returns the lower bound for this integer variable. - */ - std::shared_ptr getLowerBound() const; - - /*! - * Retrieves the upper bound for this integer variable. - * @returns the upper bound for this integer variable. - */ - std::shared_ptr getUpperBound() const; - - /*! - * Retrieves a string representation of this variable. - * @returns a string representation of this variable. - */ - std::string toString() const; - -private: - // The lower bound of the domain of the variable. - std::shared_ptr lowerBound; - - // The upper bound of the domain of the variable. - std::shared_ptr upperBound; -}; - -} // namespace ir - + + namespace parser { + namespace prism { + class VariableState; + } // namespace prismparser + } // namespace parser + + namespace ir { + + /*! + * A class representing an integer variable. + */ + class IntegerVariable : public Variable { + public: + /*! + * Default constructor. Creates an integer variable without a name and lower and upper bounds. + */ + IntegerVariable(); + + /*! + * Creates a boolean variable with the given name and the given initial value. + * + * @param localIndex A module-local unique index for the variable. + * @param globalIndex A globally 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 localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue = std::shared_ptr(nullptr)); + + /*! + * 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 variableState An object knowing about the variables in the system. + */ + IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState const& variableState); + + /*! + * Retrieves the lower bound for this integer variable. + * @returns the lower bound for this integer variable. + */ + std::shared_ptr getLowerBound() const; + + /*! + * Retrieves the upper bound for this integer variable. + * @returns the upper bound for this integer variable. + */ + std::shared_ptr getUpperBound() const; + + /*! + * Retrieves a string representation of this variable. + * @returns a string representation of this variable. + */ + std::string toString() const; + + private: + // The lower bound of the domain of the variable. + std::shared_ptr lowerBound; + + // The upper bound of the domain of the variable. + std::shared_ptr upperBound; + }; + + } // namespace ir } // namespace storm #endif /* STORM_IR_INTEGERVARIABLE_H_ */ diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index b1a4c975f..e29d07671 100644 --- a/src/ir/Module.cpp +++ b/src/ir/Module.cpp @@ -18,161 +18,153 @@ extern log4cplus::Logger logger; namespace storm { - -namespace ir { - -Module::Module() : moduleName(), booleanVariables(), integerVariables(), booleanVariableToLocalIndexMap(), - integerVariableToLocalIndexMap(), commands(), actions(), actionsToCommandIndexMap() { - // Nothing to do here. -} - -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), - booleanVariableToLocalIndexMap(booleanVariableToLocalIndexMap), - integerVariableToLocalIndexMap(integerVariableToLocalIndexMap), commands(commands), actions(), actionsToCommandIndexMap() { - // Initialize the internal mappings for fast information retrieval. - this->collectActions(); -} - - Module::Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap, parser::prismparser::VariableState const& variableState) - : 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, variableState->getNextGlobalBooleanVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap); - variableState.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, variableState->getNextGlobalIntegerVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap); - variableState.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(); - - LOG4CPLUS_TRACE(logger, "Finished renaming..."); -} - -// Return the number of boolean variables. -uint_fast64_t Module::getNumberOfBooleanVariables() const { - return this->booleanVariables.size(); -} - -// Return the requested boolean variable. -storm::ir::BooleanVariable const& Module::getBooleanVariable(uint_fast64_t index) const { - return this->booleanVariables[index]; -} - -// Return the number of integer variables. -uint_fast64_t Module::getNumberOfIntegerVariables() const { - return this->integerVariables.size(); -} - -// Return the requested integer variable. -storm::ir::IntegerVariable const& Module::getIntegerVariable(uint_fast64_t index) const { - return this->integerVariables[index]; -} - -// Return the number of commands. -uint_fast64_t Module::getNumberOfCommands() const { - return this->commands.size(); -} - -// Return the index of the variable if it exists and throw exception otherwise. -uint_fast64_t Module::getBooleanVariableIndex(std::string const& variableName) const { - auto it = booleanVariableToLocalIndexMap.find(variableName); - if (it != booleanVariableToLocalIndexMap.end()) { - return it->second; - } - LOG4CPLUS_ERROR(logger, "Cannot retrieve index of unknown boolean variable " << variableName << "."); - throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown boolean variable " << variableName << "."; -} - -uint_fast64_t Module::getIntegerVariableIndex(std::string const& variableName) const { - auto it = integerVariableToLocalIndexMap.find(variableName); - if (it != integerVariableToLocalIndexMap.end()) { - return it->second; - } - LOG4CPLUS_ERROR(logger, "Cannot retrieve index of unknown integer variable " << variableName << "."); - throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown integer variable " << variableName << "."; -} - -storm::ir::Command const& Module::getCommand(uint_fast64_t index) const { - return this->commands[index]; -} - -std::string const& Module::getName() const { - return this->moduleName; -} - -std::string Module::toString() const { - std::stringstream result; - result << "module " << moduleName << std::endl; - for (auto variable : booleanVariables) { - result << "\t" << variable.toString() << std::endl; - } - for (auto variable : integerVariables) { - result << "\t" << variable.toString() << std::endl; - } - for (auto command : commands) { - result << "\t" << command.toString() << std::endl; - } - result << "endmodule" << std::endl; - return result.str(); -} - -std::set const& Module::getActions() const { - return this->actions; -} - -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 const& action = this->commands[id].getActionName(); - if (action != "") { - if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) { - this->actionsToCommandIndexMap.emplace(action, std::set()); - } - this->actionsToCommandIndexMap[action].insert(id); - this->actions.insert(action); - } - } -} - -} // namespace ir - + namespace ir { + + Module::Module() : moduleName(), booleanVariables(), integerVariables(), booleanVariableToLocalIndexMap(), + integerVariableToLocalIndexMap(), commands(), actions(), actionsToCommandIndexMap() { + // Nothing to do here. + } + + 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), + booleanVariableToLocalIndexMap(booleanVariableToLocalIndexMap), + integerVariableToLocalIndexMap(integerVariableToLocalIndexMap), commands(commands), actions(), actionsToCommandIndexMap() { + // Initialize the internal mappings for fast information retrieval. + this->collectActions(); + } + + Module::Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, storm::parser::prism::VariableState& variableState) + : 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, variableState.getNextGlobalBooleanVariableIndex(), renaming, variableState); + variableState.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, variableState.getNextGlobalIntegerVariableIndex(), renaming, variableState); + variableState.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, variableState); + } + this->collectActions(); + + LOG4CPLUS_TRACE(logger, "Finished renaming..."); + } + + uint_fast64_t Module::getNumberOfBooleanVariables() const { + return this->booleanVariables.size(); + } + + storm::ir::BooleanVariable const& Module::getBooleanVariable(uint_fast64_t index) const { + return this->booleanVariables[index]; + } + + uint_fast64_t Module::getNumberOfIntegerVariables() const { + return this->integerVariables.size(); + } + + storm::ir::IntegerVariable const& Module::getIntegerVariable(uint_fast64_t index) const { + return this->integerVariables[index]; + } + + uint_fast64_t Module::getNumberOfCommands() const { + return this->commands.size(); + } + + uint_fast64_t Module::getBooleanVariableIndex(std::string const& variableName) const { + auto it = booleanVariableToLocalIndexMap.find(variableName); + if (it != booleanVariableToLocalIndexMap.end()) { + return it->second; + } + LOG4CPLUS_ERROR(logger, "Cannot retrieve index of unknown boolean variable " << variableName << "."); + throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown boolean variable " << variableName << "."; + } + + uint_fast64_t Module::getIntegerVariableIndex(std::string const& variableName) const { + auto it = integerVariableToLocalIndexMap.find(variableName); + if (it != integerVariableToLocalIndexMap.end()) { + return it->second; + } + LOG4CPLUS_ERROR(logger, "Cannot retrieve index of unknown integer variable " << variableName << "."); + throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown integer variable " << variableName << "."; + } + + storm::ir::Command const& Module::getCommand(uint_fast64_t index) const { + return this->commands[index]; + } + + std::string const& Module::getName() const { + return this->moduleName; + } + + std::string Module::toString() const { + std::stringstream result; + result << "module " << moduleName << std::endl; + for (auto variable : booleanVariables) { + result << "\t" << variable.toString() << std::endl; + } + for (auto variable : integerVariables) { + result << "\t" << variable.toString() << std::endl; + } + for (auto command : commands) { + result << "\t" << command.toString() << std::endl; + } + result << "endmodule" << std::endl; + return result.str(); + } + + std::set const& Module::getActions() const { + return this->actions; + } + + 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 const& action = this->commands[id].getActionName(); + if (action != "") { + if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) { + this->actionsToCommandIndexMap.emplace(action, std::set()); + } + this->actionsToCommandIndexMap[action].insert(id); + this->actions.insert(action); + } + } + } + + } // namespace ir } // namespace storm diff --git a/src/ir/Module.h b/src/ir/Module.h index 89c409607..1b20991ea 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -20,179 +20,175 @@ #include "expressions/VariableExpression.h" namespace storm { - -namespace parser { -namespace prismparser { - class VariableState; -} // namespace prismparser -} // namespace parser - -namespace ir { -/*! - * A class representing a module. - */ -class Module { -public: - /*! - * Default constructor. Creates an empty module. - */ - Module(); - - /*! - * Creates a module with the given name, variables and 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 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 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(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap, parser::prismparser::VariableState const& variableState); - - /*! - * Retrieves 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. - * - * @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. - * - * @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. - * - * @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. - * - * @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 boolean variable whose index to retrieve. - * @return The index of the boolean variable with the given name. - */ - 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 integer variable whose index to retrieve. - * @return The index of the integer variable with the given name. - */ - uint_fast64_t getIntegerVariableIndex(std::string const& variableName) const; - - /*! - * Retrieves 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; - - /*! - * Retrieves the name of the module. - * - * @return The name of the module. - */ - std::string const& getName() const; + namespace parser { + namespace prism { + class VariableState; + } // namespace prismparser + } // namespace parser - /*! - * 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. - * - * @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 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::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. - std::string moduleName; - - // A list of boolean variables. - std::vector booleanVariables; - - // A list of integer variables. - std::vector integerVariables; - - // A map of boolean variable names to their index. - std::map booleanVariableToLocalIndexMap; - - // A map of integer variable names to their index. - std::map integerVariableToLocalIndexMap; - - // The commands associated with the module. - std::vector commands; - - // The set of actions present in this module. - std::set actions; - - // A map of actions to the set of commands labeled with this action. - std::map> actionsToCommandIndexMap; -}; - -} // namespace ir - + namespace ir { + + /*! + * A class representing a module. + */ + class Module { + public: + /*! + * Default constructor. Creates an empty module. + */ + Module(); + + /*! + * Creates a module with the given name, variables and 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 booleanVariableToLocalIndexMap A mapping of boolean variables to global (i.e. module-local) indices. + * @param integerVariableToLocalIndexMap A mapping of integer variables to global (i.e. module-local) indices. + * @param commands The commands of the 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); + + 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 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 variableState An object knowing about the variables in the system. + */ + Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, storm::parser::prism::VariableState& variableState); + + /*! + * Retrieves 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. + * + * @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. + * + * @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. + * + * @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. + * + * @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 boolean variable whose index to retrieve. + * @return The index of the boolean variable with the given name. + */ + 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 integer variable whose index to retrieve. + * @return The index of the integer variable with the given name. + */ + uint_fast64_t getIntegerVariableIndex(std::string const& variableName) const; + + /*! + * Retrieves 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; + + /*! + * Retrieves the name of the module. + * + * @return The name of the module. + */ + std::string const& getName() const; + + /*! + * 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. + * + * @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 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::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. + std::string moduleName; + + // A list of boolean variables. + std::vector booleanVariables; + + // A list of integer variables. + std::vector integerVariables; + + // A map of boolean variable names to their index. + std::map booleanVariableToLocalIndexMap; + + // A map of integer variable names to their index. + std::map integerVariableToLocalIndexMap; + + // The commands associated with the module. + std::vector commands; + + // The set of actions present in this module. + std::set actions; + + // A map of actions to the set of commands labeled with this action. + std::map> actionsToCommandIndexMap; + }; + + } // namespace ir } // namespace storm #endif /* STORM_IR_MODULE_H_ */ diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index 3dbc12dee..0db9f7342 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -17,102 +17,100 @@ extern log4cplus::Logger logger; namespace storm { - -namespace ir { - -Program::Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards(), actions(), actionsToModuleIndexMap() { - // Nothing to do here. -} - -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() { - // 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(moduleId); - this->actions.insert(action); + namespace ir { + + Program::Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards(), actions(), actionsToModuleIndexMap() { + // Nothing to do here. } - } -} - -Program::ModelType Program::getModelType() const { - return modelType; -} - -std::string Program::toString() const { - std::stringstream result; - switch (modelType) { - case UNDEFINED: result << "undefined"; break; - case DTMC: result << "dtmc"; break; - case CTMC: result << "ctmc"; break; - case MDP: result << "mdp"; break; - case CTMDP: result << "ctmdp"; break; - } - result << std::endl; - - for (auto const& element : booleanUndefinedConstantExpressions) { - result << "const bool " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; - } - for (auto const& element : integerUndefinedConstantExpressions) { - result << "const int " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; - } - for (auto const& element : doubleUndefinedConstantExpressions) { - result << "const double " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; - } - result << std::endl; - - for (auto const& module : modules) { - result << module.toString() << std::endl; - } - - for (auto const& rewardModel : rewards) { - result << rewardModel.first << ": " << rewardModel.second.toString() << std::endl; - } - - for (auto const& label : labels) { - result << "label " << label.first << " = " << label.second->toString() <<";" << std::endl; - } - - return result.str(); -} - -uint_fast64_t Program::getNumberOfModules() const { - return this->modules.size(); -} - -storm::ir::Module const& Program::getModule(uint_fast64_t index) const { - return this->modules[index]; -} - -std::set const& Program::getActions() const { - return this->actions; -} - -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 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> const& Program::getLabels() const { - return this->labels; -} - -} // namespace ir - + + 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() { + // 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(moduleId); + this->actions.insert(action); + } + } + } + + Program::ModelType Program::getModelType() const { + return modelType; + } + + std::string Program::toString() const { + std::stringstream result; + switch (modelType) { + case UNDEFINED: result << "undefined"; break; + case DTMC: result << "dtmc"; break; + case CTMC: result << "ctmc"; break; + case MDP: result << "mdp"; break; + case CTMDP: result << "ctmdp"; break; + } + result << std::endl; + + for (auto const& element : booleanUndefinedConstantExpressions) { + result << "const bool " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; + } + for (auto const& element : integerUndefinedConstantExpressions) { + result << "const int " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; + } + for (auto const& element : doubleUndefinedConstantExpressions) { + result << "const double " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; + } + result << std::endl; + + for (auto const& module : modules) { + result << module.toString() << std::endl; + } + + for (auto const& rewardModel : rewards) { + result << rewardModel.first << ": " << rewardModel.second.toString() << std::endl; + } + + for (auto const& label : labels) { + result << "label " << label.first << " = " << label.second->toString() <<";" << std::endl; + } + + return result.str(); + } + + uint_fast64_t Program::getNumberOfModules() const { + return this->modules.size(); + } + + storm::ir::Module const& Program::getModule(uint_fast64_t index) const { + return this->modules[index]; + } + + std::set const& Program::getActions() const { + return this->actions; + } + + 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 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> const& Program::getLabels() const { + return this->labels; + } + + } // namespace ir } // namepsace storm diff --git a/src/ir/Program.h b/src/ir/Program.h index 145a0deb2..891b6abbf 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -21,138 +21,136 @@ #include "RewardModel.h" namespace storm { - -namespace ir { - -/*! - * A class representing a program. - */ -class Program { -public: - - /*! - * An enum for the different model types. - */ - enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP}; - - /*! - * Default constructor. Creates an empty program. - */ - Program(); - - /*! - * 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 - * expression nodes. - * @param integerUndefinedConstantExpressions A map of undefined integer constants to their - * expression nodes. - * @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); - - /*! - * Retrieves 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. - * @return The module with the given index. - */ - storm::ir::Module const& getModule(uint_fast64_t index) const; - - /*! - * Retrieves the model type of the model. - * - * @return The type of the model. - */ - ModelType getModelType() const; - - /*! - * Retrieves 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. - * - * @return The set of actions present in this module. - */ - std::set const& getActions() const; - - /*! - * 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; - - /*! - * 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 const& getRewardModel(std::string const& name) const; - - /*! - * Retrieves all labels that are defined by the probabilitic program. - * - * @return A set of labels that are defined in the program. - */ - std::map> const& getLabels() const; - -private: - // The type of the model. - ModelType modelType; - - // A map of undefined boolean constants to their expression nodes. - std::map> booleanUndefinedConstantExpressions; - - // A map of undefined integer constants to their expressions nodes. - std::map> integerUndefinedConstantExpressions; - - // A map of undefined double constants to their expressions nodes. - std::map> doubleUndefinedConstantExpressions; - - // The modules associated with the program. - std::vector modules; - - // The reward models associated with the program. - std::map rewards; - - // The labels that are defined for this model. - std::map> labels; - - // The set of actions present in this program. - std::set actions; - - // A map of actions to the set of modules containing commands labelled with this action. - std::map> actionsToModuleIndexMap; -}; - -} // namespace ir - + namespace ir { + + /*! + * A class representing a program. + */ + class Program { + public: + + /*! + * An enum for the different model types. + */ + enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP}; + + /*! + * Default constructor. Creates an empty program. + */ + Program(); + + /*! + * 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 + * expression nodes. + * @param integerUndefinedConstantExpressions A map of undefined integer constants to their + * expression nodes. + * @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); + + /*! + * Retrieves 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. + * @return The module with the given index. + */ + storm::ir::Module const& getModule(uint_fast64_t index) const; + + /*! + * Retrieves the model type of the model. + * + * @return The type of the model. + */ + ModelType getModelType() const; + + /*! + * Retrieves 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. + * + * @return The set of actions present in this module. + */ + std::set const& getActions() const; + + /*! + * 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; + + /*! + * 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 const& getRewardModel(std::string const& name) const; + + /*! + * Retrieves all labels that are defined by the probabilitic program. + * + * @return A set of labels that are defined in the program. + */ + std::map> const& getLabels() const; + + private: + // The type of the model. + ModelType modelType; + + // A map of undefined boolean constants to their expression nodes. + std::map> booleanUndefinedConstantExpressions; + + // A map of undefined integer constants to their expressions nodes. + std::map> integerUndefinedConstantExpressions; + + // A map of undefined double constants to their expressions nodes. + std::map> doubleUndefinedConstantExpressions; + + // The modules associated with the program. + std::vector modules; + + // The reward models associated with the program. + std::map rewards; + + // The labels that are defined for this model. + std::map> labels; + + // The set of actions present in this program. + std::set actions; + + // A map of actions to the set of modules containing commands labelled with this action. + std::map> actionsToModuleIndexMap; + }; + + } // namespace ir } // namespace storm #endif /* STORM_IR_PROGRAM_H_ */ diff --git a/src/ir/RewardModel.cpp b/src/ir/RewardModel.cpp index 801b78515..9d6a79ed3 100644 --- a/src/ir/RewardModel.cpp +++ b/src/ir/RewardModel.cpp @@ -10,46 +10,44 @@ #include "RewardModel.h" namespace storm { - -namespace ir { - -RewardModel::RewardModel() : rewardModelName(), stateRewards(), transitionRewards() { - // Nothing to do here. -} - -RewardModel::RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) { - // Nothing to do here. -} - -std::string RewardModel::toString() const { - std::stringstream result; - result << "rewards \"" << rewardModelName << "\"" << std::endl; - for (auto const& reward : stateRewards) { - result << reward.toString() << std::endl; - } - for (auto const& reward : transitionRewards) { - result << reward.toString() << std::endl; - } - result << "endrewards" << std::endl; - return result.str(); -} - -bool RewardModel::hasStateRewards() const { - return this->stateRewards.size() > 0; -} - -std::vector const& RewardModel::getStateRewards() const { - return this->stateRewards; -} - -bool RewardModel::hasTransitionRewards() const { - return this->transitionRewards.size() > 0; -} - -std::vector const& RewardModel::getTransitionRewards() const { - return this->transitionRewards; -} - -} // namespace ir - + namespace ir { + + RewardModel::RewardModel() : rewardModelName(), stateRewards(), transitionRewards() { + // Nothing to do here. + } + + RewardModel::RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) { + // Nothing to do here. + } + + std::string RewardModel::toString() const { + std::stringstream result; + result << "rewards \"" << rewardModelName << "\"" << std::endl; + for (auto const& reward : stateRewards) { + result << reward.toString() << std::endl; + } + for (auto const& reward : transitionRewards) { + result << reward.toString() << std::endl; + } + result << "endrewards" << std::endl; + return result.str(); + } + + bool RewardModel::hasStateRewards() const { + return this->stateRewards.size() > 0; + } + + std::vector const& RewardModel::getStateRewards() const { + return this->stateRewards; + } + + bool RewardModel::hasTransitionRewards() const { + return this->transitionRewards.size() > 0; + } + + std::vector const& RewardModel::getTransitionRewards() const { + return this->transitionRewards; + } + + } // namespace ir } // namespace storm diff --git a/src/ir/RewardModel.h b/src/ir/RewardModel.h index 39c2f652f..827248810 100644 --- a/src/ir/RewardModel.h +++ b/src/ir/RewardModel.h @@ -15,76 +15,74 @@ #include "TransitionReward.h" namespace storm { - -namespace ir { - -/*! - * A class representing a reward model. - */ -class RewardModel { -public: - /*! - * Default constructor. Creates an empty reward model. - */ - RewardModel(); - - /*! - * Creates a reward module with the given name, state and transition rewards. - * - * @param rewardModelName The name of the reward model. - * @param stateRewards A vector of state-based rewards. - * @param transitionRewards A vector of transition-based rewards. - */ - RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards); - - /*! - * Retrieves a string representation of this reward model. - * - * @return a string representation of this reward model. - */ - std::string toString() const; - - /*! - * Check, if there are any state rewards. - * - * @return True, iff there are any state rewards. - */ - bool hasStateRewards() const; - - /*! - * Retrieves a vector of state rewards associated with this reward model. - * - * @return A vector containing the state rewards associated with this reward model. - */ - std::vector const& getStateRewards() const; - - /*! - * Check, if there are any transition rewards. - * - * @return True, iff there are any transition rewards associated with this reward model. - */ - bool hasTransitionRewards() const; - - /*! - * Retrieves a vector of transition rewards associated with this reward model. - * - * @return A vector of transition rewards associated with this reward model. - */ - std::vector const& getTransitionRewards() const; - -private: - // The name of the reward model. - std::string rewardModelName; - - // The state-based rewards associated with this reward model. - std::vector stateRewards; - - // The transition-based rewards associated with this reward model. - std::vector transitionRewards; -}; - -} // namespace ir - + namespace ir { + + /*! + * A class representing a reward model. + */ + class RewardModel { + public: + /*! + * Default constructor. Creates an empty reward model. + */ + RewardModel(); + + /*! + * Creates a reward module with the given name, state and transition rewards. + * + * @param rewardModelName The name of the reward model. + * @param stateRewards A vector of state-based rewards. + * @param transitionRewards A vector of transition-based rewards. + */ + RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards); + + /*! + * Retrieves a string representation of this reward model. + * + * @return a string representation of this reward model. + */ + std::string toString() const; + + /*! + * Check, if there are any state rewards. + * + * @return True, iff there are any state rewards. + */ + bool hasStateRewards() const; + + /*! + * Retrieves a vector of state rewards associated with this reward model. + * + * @return A vector containing the state rewards associated with this reward model. + */ + std::vector const& getStateRewards() const; + + /*! + * Check, if there are any transition rewards. + * + * @return True, iff there are any transition rewards associated with this reward model. + */ + bool hasTransitionRewards() const; + + /*! + * Retrieves a vector of transition rewards associated with this reward model. + * + * @return A vector of transition rewards associated with this reward model. + */ + std::vector const& getTransitionRewards() const; + + private: + // The name of the reward model. + std::string rewardModelName; + + // The state-based rewards associated with this reward model. + std::vector stateRewards; + + // The transition-based rewards associated with this reward model. + std::vector transitionRewards; + }; + + } // namespace ir } // namespace storm #endif /* STORM_IR_REWARDMODEL_H_ */ diff --git a/src/ir/StateReward.cpp b/src/ir/StateReward.cpp index 02b659635..605afcb21 100644 --- a/src/ir/StateReward.cpp +++ b/src/ir/StateReward.cpp @@ -26,7 +26,15 @@ std::string StateReward::toString() const { result << "\t" << statePredicate->toString() << ": " << rewardValue->toString() << ";"; return result.str(); } + +std::shared_ptr StateReward::getStatePredicate() const { + return this->statePredicate; +} +std::shared_ptr StateReward::getRewardValue() const { + return this->rewardValue; +} + } // namespace ir } // namespace storm diff --git a/src/ir/StateReward.h b/src/ir/StateReward.h index d9d17f281..633c8c635 100644 --- a/src/ir/StateReward.h +++ b/src/ir/StateReward.h @@ -43,7 +43,21 @@ public: * @return A string representation of this state reward. */ std::string toString() const; - + + /*! + * Retrieves the state predicate that is associated with this state reward. + * + * @return The state predicate that is associated with this state reward. + */ + std::shared_ptr getStatePredicate() const; + + /*! + * Retrieves the reward value associated with this state reward. + * + * @return The reward value associated with this state reward. + */ + std::shared_ptr getRewardValue() const; + private: // The predicate that characterizes the states that obtain this reward. std::shared_ptr statePredicate; diff --git a/src/ir/TransitionReward.cpp b/src/ir/TransitionReward.cpp index b32bd1b72..60e504984 100644 --- a/src/ir/TransitionReward.cpp +++ b/src/ir/TransitionReward.cpp @@ -27,6 +27,18 @@ std::string TransitionReward::toString() const { return result.str(); } +std::string const& TransitionReward::getActionName() const { + return this->commandName; +} + +std::shared_ptr TransitionReward::getStatePredicate() const { + return this->statePredicate; +} + +std::shared_ptr TransitionReward::getRewardValue() const { + return this->rewardValue; +} + } // namespace ir } // namespace storm diff --git a/src/ir/TransitionReward.h b/src/ir/TransitionReward.h index 37f0fffdf..479810755 100644 --- a/src/ir/TransitionReward.h +++ b/src/ir/TransitionReward.h @@ -44,6 +44,27 @@ public: * @return A string representation of this transition reward. */ std::string toString() const; + + /*! + * Retrieves the action name that is associated with this transition reward. + * + * @return The action name that is associated with this transition reward. + */ + std::string const& getActionName() const; + + /*! + * Retrieves the state predicate that is associated with this state reward. + * + * @return The state predicate that is associated with this state reward. + */ + std::shared_ptr getStatePredicate() const; + + /*! + * Retrieves the reward value associated with this state reward. + * + * @return The reward value associated with this state reward. + */ + std::shared_ptr getRewardValue() const; private: // The name of the command this transition-based reward is attached to. diff --git a/src/ir/Update.cpp b/src/ir/Update.cpp index 51091a022..1c66789c6 100644 --- a/src/ir/Update.cpp +++ b/src/ir/Update.cpp @@ -8,102 +8,100 @@ #include #include "Update.h" +#include "src/parser/prismparser/VariableState.h" #include "src/exceptions/OutOfRangeException.h" namespace storm { - -namespace ir { - - -Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignments() { - // Nothing to do here. -} - -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 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[variableAssignmentPair.first] = Assignment(variableAssignmentPair.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[variableAssignmentPair.first] = Assignment(variableAssignmentPair.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); - } - } - this->likelihoodExpression = update.likelihoodExpression->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap); -} - -std::shared_ptr const& Update::getLikelihoodExpression() const { - return likelihoodExpression; -} - -uint_fast64_t Update::getNumberOfBooleanAssignments() const { - return booleanAssignments.size(); -} - -uint_fast64_t Update::getNumberOfIntegerAssignments() const { - return integerAssignments.size(); -} - -std::map const& Update::getBooleanAssignments() const { - return booleanAssignments; -} - -std::map const& Update::getIntegerAssignments() const { - return integerAssignments; -} - -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 '" + namespace ir { + + Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignments() { + // Nothing to do here. + } + + 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, storm::parser::prism::VariableState const& variableState) { + for (auto const& variableAssignmentPair : update.booleanAssignments) { + if (renaming.count(variableAssignmentPair.first) > 0) { + this->booleanAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, variableState); + } else { + this->booleanAssignments[variableAssignmentPair.first] = Assignment(variableAssignmentPair.second, renaming, variableState); + } + } + for (auto const& variableAssignmentPair : update.integerAssignments) { + if (renaming.count(variableAssignmentPair.first) > 0) { + this->integerAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, variableState); + } else { + this->integerAssignments[variableAssignmentPair.first] = Assignment(variableAssignmentPair.second, renaming, variableState); + } + } + this->likelihoodExpression = update.likelihoodExpression->clone(renaming, variableState); + } + + std::shared_ptr const& Update::getLikelihoodExpression() const { + return likelihoodExpression; + } + + uint_fast64_t Update::getNumberOfBooleanAssignments() const { + return booleanAssignments.size(); + } + + uint_fast64_t Update::getNumberOfIntegerAssignments() const { + return integerAssignments.size(); + } + + std::map const& Update::getBooleanAssignments() const { + return booleanAssignments; + } + + std::map const& Update::getIntegerAssignments() const { + return integerAssignments; + } + + 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 variableAssignmentPair->second; -} - -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 '" + } + + return variableAssignmentPair->second; + } + + 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 variableAssignmentPair->second; -} - -std::string Update::toString() const { - std::stringstream result; - result << likelihoodExpression->toString() << " : "; - uint_fast64_t i = 0; - for (auto const& assignment : booleanAssignments) { - result << assignment.second.toString(); - if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) { - result << " & "; - } - ++i; - } - i = 0; - for (auto const& assignment : integerAssignments) { - result << assignment.second.toString(); - if (i < integerAssignments.size() - 1) { - result << " & "; - } - ++i; - } - return result.str(); -} - -} // namespace ir - + } + + return variableAssignmentPair->second; + } + + std::string Update::toString() const { + std::stringstream result; + result << likelihoodExpression->toString() << " : "; + uint_fast64_t i = 0; + for (auto const& assignment : booleanAssignments) { + result << assignment.second.toString(); + if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) { + result << " & "; + } + ++i; + } + i = 0; + for (auto const& assignment : integerAssignments) { + result << assignment.second.toString(); + if (i < integerAssignments.size() - 1) { + result << " & "; + } + ++i; + } + return result.str(); + } + + } // namespace ir } // namespace storm diff --git a/src/ir/Update.h b/src/ir/Update.h index 505277504..4fe4b05be 100644 --- a/src/ir/Update.h +++ b/src/ir/Update.h @@ -15,108 +15,112 @@ #include "Assignment.h" namespace storm { - -namespace ir { - -/*! - * A class representing an update of a command. - */ -class Update { -public: - /*! - * Default constructor. Creates an empty update. - */ - Update(); - - /*! - * Creates an update with the given expression specifying the likelihood and the mapping of - * variable to their assignments. - * - * @param likelihoodExpression An expression specifying the likelihood of this update. - * @param assignments A map of variable names to their assignments. - */ - 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. - * - * update The update that is to be copied. - * 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. - */ - Update(Update const& update, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap); - - /*! - * Retrieves the expression for the likelihood of this update. - * - * @return The expression for the likelihood of this update. - */ - std::shared_ptr const& getLikelihoodExpression() const; - - /*! - * Retrieves the number of boolean assignments associated with this update. - * - * @return The number of boolean assignments associated with this update. - */ - uint_fast64_t getNumberOfBooleanAssignments() const; - - /*! - * Retrieves the number of integer assignments associated with this update. - * - * @return The number of integer assignments associated with this update. - */ - uint_fast64_t getNumberOfIntegerAssignments() const; - - /*! - * Retrieves a reference to the map of boolean variable names to their respective assignments. - * - * @return A reference to the map of boolean variable names to their respective assignments. - */ - 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::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 const& variableName) const; - - /*! - * Retrieves a string representation of this update. - * - * @return A string representation of this update. - */ - std::string toString() const; - -private: - // An expression specifying the likelihood of taking this update. - std::shared_ptr 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; -}; - -} // namespace ir - + + namespace parser { + namespace prism { + class VariableState; + } // namespace prismparser + } // namespace parser + + namespace ir { + + /*! + * A class representing an update of a command. + */ + class Update { + public: + /*! + * Default constructor. Creates an empty update. + */ + Update(); + + /*! + * Creates an update with the given expression specifying the likelihood and the mapping of + * variable to their assignments. + * + * @param likelihoodExpression An expression specifying the likelihood of this update. + * @param assignments A map of variable names to their assignments. + */ + 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. + * + * update The update that is to be copied. + * renaming A mapping from names that are to be renamed to the names they are to be + * replaced with. + * @param variableState An object knowing about the variables in the system. + */ + Update(Update const& update, std::map const& renaming, storm::parser::prism::VariableState const& variableState); + + /*! + * Retrieves the expression for the likelihood of this update. + * + * @return The expression for the likelihood of this update. + */ + std::shared_ptr const& getLikelihoodExpression() const; + + /*! + * Retrieves the number of boolean assignments associated with this update. + * + * @return The number of boolean assignments associated with this update. + */ + uint_fast64_t getNumberOfBooleanAssignments() const; + + /*! + * Retrieves the number of integer assignments associated with this update. + * + * @return The number of integer assignments associated with this update. + */ + uint_fast64_t getNumberOfIntegerAssignments() const; + + /*! + * Retrieves a reference to the map of boolean variable names to their respective assignments. + * + * @return A reference to the map of boolean variable names to their respective assignments. + */ + 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::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 const& variableName) const; + + /*! + * Retrieves a string representation of this update. + * + * @return A string representation of this update. + */ + std::string toString() const; + + private: + // An expression specifying the likelihood of taking this update. + std::shared_ptr 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; + }; + + } // namespace ir } // namespace storm #endif /* STORM_IR_UPDATE_H_ */ diff --git a/src/ir/Variable.cpp b/src/ir/Variable.cpp index 7a87dfd10..eefa63063 100644 --- a/src/ir/Variable.cpp +++ b/src/ir/Variable.cpp @@ -10,47 +10,46 @@ #include #include "Variable.h" +#include "src/parser/prismparser/VariableState.h" namespace storm { - -namespace ir { - -Variable::Variable() : globalIndex(0), localIndex(0), variableName(), initialValue() { - // Nothing to do here. -} - -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 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); - } -} - -std::string const& Variable::getName() const { - return variableName; -} - -uint_fast64_t Variable::getGlobalIndex() const { - return globalIndex; -} - -uint_fast64_t Variable::getLocalIndex() const { - return localIndex; -} - -std::shared_ptr const& Variable::getInitialValue() const { - return initialValue; -} - -void Variable::setInitialValue(std::shared_ptr const& initialValue) { - this->initialValue = initialValue; -} - -} // namespace ir - + namespace ir { + + Variable::Variable() : localIndex(0), globalIndex(0), variableName(), initialValue() { + // Nothing to do here. + } + + Variable::Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr const& initialValue) + : localIndex(localIndex), globalIndex(globalIndex), variableName(variableName), initialValue(initialValue) { + // Nothing to do here. + } + + Variable::Variable(Variable const& var, std::string const& newName, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState const& variableState) + : localIndex(var.getLocalIndex()), globalIndex(newGlobalIndex), variableName(var.getName()) { + if (var.initialValue != nullptr) { + this->initialValue = var.initialValue->clone(renaming, variableState); + } + } + + std::string const& Variable::getName() const { + return variableName; + } + + uint_fast64_t Variable::getGlobalIndex() const { + return globalIndex; + } + + uint_fast64_t Variable::getLocalIndex() const { + return localIndex; + } + + std::shared_ptr const& Variable::getInitialValue() const { + return initialValue; + } + + void Variable::setInitialValue(std::shared_ptr const& initialValue) { + this->initialValue = initialValue; + } + + } // namespace ir } // namespace storm diff --git a/src/ir/Variable.h b/src/ir/Variable.h index 41f750a2d..36bb6e669 100644 --- a/src/ir/Variable.h +++ b/src/ir/Variable.h @@ -14,95 +14,99 @@ #include "expressions/BaseExpression.h" namespace storm { - -namespace ir { - -/*! - * A class representing a untyped variable. - */ -class Variable { -public: - /*! - * Default constructor. Creates an unnamed, untyped variable without initial value. - */ - Variable(); - - /*! - * Creates an untyped variable with the given name and 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. - */ - 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. - * - * @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. - */ - 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. - * - * @return The name of the variable. - */ - std::string const& getName() const; - - /*! - * Retrieves the global index of the variable, i.e. the index in all variables of equal type - * of all modules. - * - * @return The global index of the variable. - */ - uint_fast64_t getGlobalIndex() const; - /*! - * Retrieves the global index of the variable, i.e. the index in all variables of equal type in - * the same module. - * - * @return The local index of the variable. - */ - uint_fast64_t getLocalIndex() const; - - /*! - * Retrieves the expression defining the initial value of the variable. - * - * @return The expression defining the initial value of the variable. - */ - std::shared_ptr const& getInitialValue() const; - - /*! - * Sets the initial value to the given expression. - * - * @param initialValue The new initial value. - */ - void setInitialValue(std::shared_ptr const& initialValue); - -private: - // A unique (among the variables of equal type) index for the variable over all modules. - uint_fast64_t globalIndex; + namespace parser { + namespace prism { + class VariableState; + } // namespace prismparser + } // namespace parser - // A unique (among the variables of equal type) index for the variable inside its module. - uint_fast64_t localIndex; - - // The name of the variable. - std::string variableName; - - // The expression defining the initial value of the variable. - std::shared_ptr initialValue; -}; - -} // namespace ir - + namespace ir { + + /*! + * A class representing a untyped variable. + */ + class Variable { + public: + /*! + * Default constructor. Creates an unnamed, untyped variable without initial value. + */ + Variable(); + + /*! + * Creates an untyped variable with the given name and initial value. + * + * @param localIndex A module-local index for the variable. + * @param globalIndex A globally 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. + */ + Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr const& initialValue = std::shared_ptr()); + + /*! + * 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. + * @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 variableState An object knowing about the variables in the system. + */ + Variable(Variable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState const& variableState); + + /*! + * Retrieves the name of the variable. + * + * @return The name of the variable. + */ + std::string const& getName() const; + + /*! + * Retrieves the global index of the variable, i.e. the index in all variables of equal type + * of all modules. + * + * @return The global index of the variable. + */ + uint_fast64_t getGlobalIndex() const; + + /*! + * Retrieves the global index of the variable, i.e. the index in all variables of equal type in + * the same module. + * + * @return The local index of the variable. + */ + uint_fast64_t getLocalIndex() const; + + /*! + * Retrieves the expression defining the initial value of the variable. + * + * @return The expression defining the initial value of the variable. + */ + std::shared_ptr const& getInitialValue() const; + + /*! + * Sets the initial value to the given expression. + * + * @param initialValue The new initial value. + */ + void setInitialValue(std::shared_ptr const& initialValue); + + private: + // A unique (among the variables of equal type) index for the variable inside its module. + uint_fast64_t localIndex; + + // A unique (among the variables of equal type) index for the variable over all modules. + uint_fast64_t globalIndex; + + // The name of the variable. + std::string variableName; + + // The expression defining the initial value of the variable. + std::shared_ptr initialValue; + }; + + } // namespace ir } // namespace storm - #endif /* STORM_IR_VARIABLE_H_ */ diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h index ef5a0d44c..27d033be8 100644 --- a/src/ir/expressions/BaseExpression.h +++ b/src/ir/expressions/BaseExpression.h @@ -21,7 +21,7 @@ namespace storm { // Forward-declare VariableState. namespace parser { - namespace prismparser { + namespace prism { class VariableState; } // namespace prismparser } // namespace parser @@ -70,7 +70,7 @@ namespace storm { * @param renaming A mapping from identifier names to strings they are to be replaced with. * @param variableState An object knowing about the global variable state. */ - virtual std::shared_ptr clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const = 0; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const = 0; /*! * Retrieves the value of the expression as an integer given the provided variable valuation. diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.cpp b/src/ir/expressions/BinaryBooleanFunctionExpression.cpp index f122f0a95..d5c67ed4e 100644 --- a/src/ir/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/ir/expressions/BinaryBooleanFunctionExpression.cpp @@ -18,7 +18,7 @@ namespace storm { // Nothing to do here. } - std::shared_ptr BinaryBooleanFunctionExpression::clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const { + std::shared_ptr BinaryBooleanFunctionExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new BinaryBooleanFunctionExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType)); } diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.h b/src/ir/expressions/BinaryBooleanFunctionExpression.h index e1b52968c..f8a3313df 100644 --- a/src/ir/expressions/BinaryBooleanFunctionExpression.h +++ b/src/ir/expressions/BinaryBooleanFunctionExpression.h @@ -8,7 +8,7 @@ #ifndef STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ #define STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ -#include "src/ir/expressions/BinaryExpression.h" +#include "BinaryExpression.h" namespace storm { namespace ir { @@ -33,7 +33,7 @@ namespace storm { */ BinaryBooleanFunctionExpression(std::shared_ptr const& left, std::shared_ptr const& right, FunctionType functionType); - virtual std::shared_ptr clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp index 21052f98c..16765428f 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp @@ -18,7 +18,7 @@ namespace storm { // Nothing to do here. } - std::shared_ptr BinaryNumericalFunctionExpression::clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const { + std::shared_ptr BinaryNumericalFunctionExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType)); } diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h index d30effb8e..e1b62b346 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.h +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.h @@ -34,7 +34,7 @@ namespace storm { */ BinaryNumericalFunctionExpression(ReturnType type, std::shared_ptr const& left, std::shared_ptr const& right, FunctionType functionType); - virtual std::shared_ptr clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; /*! * Retrieves the operator that is associated with this node. diff --git a/src/ir/expressions/BinaryRelationExpression.cpp b/src/ir/expressions/BinaryRelationExpression.cpp index 407d3cd31..c5aa0fe34 100644 --- a/src/ir/expressions/BinaryRelationExpression.cpp +++ b/src/ir/expressions/BinaryRelationExpression.cpp @@ -18,7 +18,7 @@ namespace storm { // Nothing to do here } - std::shared_ptr BinaryRelationExpression::clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const { + std::shared_ptr BinaryRelationExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new BinaryRelationExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->relationType)); } diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h index 330152b89..d2e07f437 100644 --- a/src/ir/expressions/BinaryRelationExpression.h +++ b/src/ir/expressions/BinaryRelationExpression.h @@ -33,7 +33,7 @@ namespace storm { */ BinaryRelationExpression(std::shared_ptr const& left, std::shared_ptr const& right, RelationType relationType); - virtual std::shared_ptr clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/BooleanConstantExpression.cpp b/src/ir/expressions/BooleanConstantExpression.cpp index 71d84e33e..1a3a89deb 100644 --- a/src/ir/expressions/BooleanConstantExpression.cpp +++ b/src/ir/expressions/BooleanConstantExpression.cpp @@ -18,7 +18,7 @@ namespace storm { value = false; } - std::shared_ptr BooleanConstantExpression::clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const { + std::shared_ptr BooleanConstantExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new BooleanConstantExpression(*this)); } diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h index 72288588d..c72ad34cb 100644 --- a/src/ir/expressions/BooleanConstantExpression.h +++ b/src/ir/expressions/BooleanConstantExpression.h @@ -26,7 +26,7 @@ namespace storm { */ BooleanConstantExpression(std::string const& constantName); - virtual std::shared_ptr clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/BooleanLiteralExpression.cpp b/src/ir/expressions/BooleanLiteralExpression.cpp index d0658bd50..c984e803f 100644 --- a/src/ir/expressions/BooleanLiteralExpression.cpp +++ b/src/ir/expressions/BooleanLiteralExpression.cpp @@ -15,7 +15,7 @@ namespace storm { // Nothing to do here. } - std::shared_ptr BooleanLiteralExpression::clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const { + std::shared_ptr BooleanLiteralExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new BooleanLiteralExpression(this->value)); } diff --git a/src/ir/expressions/BooleanLiteralExpression.h b/src/ir/expressions/BooleanLiteralExpression.h index 3879d320f..5ce5a180e 100644 --- a/src/ir/expressions/BooleanLiteralExpression.h +++ b/src/ir/expressions/BooleanLiteralExpression.h @@ -26,7 +26,7 @@ namespace storm { */ BooleanLiteralExpression(bool value); - virtual std::shared_ptr clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/ConstantExpression.cpp b/src/ir/expressions/ConstantExpression.cpp index 114ce10b1..65a9a54a5 100644 --- a/src/ir/expressions/ConstantExpression.cpp +++ b/src/ir/expressions/ConstantExpression.cpp @@ -5,13 +5,13 @@ * Author: Christian Dehnert */ -#include "src/ir/expressions/ConstantExpression.h" +#include "ConstantExpression.h" namespace storm { namespace ir { namespace expressions { - ConstantExpression::ConstantExpression(ReturnType type, std::string constantName) : BaseExpression(type), constantName(constantName) { + ConstantExpression::ConstantExpression(ReturnType type, std::string const& constantName) : BaseExpression(type), constantName(constantName) { // Nothing to do here. } @@ -19,7 +19,7 @@ namespace storm { return constantName; } - virtual std::string ConstantExpression::toString() const { + std::string ConstantExpression::toString() const { return constantName; } diff --git a/src/ir/expressions/ConstantExpression.h b/src/ir/expressions/ConstantExpression.h index 316367f1a..d313c11d4 100644 --- a/src/ir/expressions/ConstantExpression.h +++ b/src/ir/expressions/ConstantExpression.h @@ -8,7 +8,7 @@ #ifndef STORM_IR_EXPRESSIONS_CONSTANTEXPRESSION_H_ #define STORM_IR_EXPRESSIONS_CONSTANTEXPRESSION_H_ -#include "src/ir/expressions/BaseExpression.h" +#include "BaseExpression.h" namespace storm { namespace ir { @@ -26,7 +26,7 @@ namespace storm { * @param type The type of the constant. * @param constantName The name of the constant. */ - ConstantExpression(ReturnType type, std::string constantName); + ConstantExpression(ReturnType type, std::string const& constantName); /*! * Retrieves the name of the constant. diff --git a/src/ir/expressions/DoubleConstantExpression.cpp b/src/ir/expressions/DoubleConstantExpression.cpp index 99727e7b7..85ac47f78 100644 --- a/src/ir/expressions/DoubleConstantExpression.cpp +++ b/src/ir/expressions/DoubleConstantExpression.cpp @@ -13,11 +13,11 @@ namespace storm { namespace ir { namespace expressions { - DoubleConstantExpression::DoubleConstantExpression(std::string const& constantName) : ConstantExpression(double_, constantName), defined(false), value(0) { + DoubleConstantExpression::DoubleConstantExpression(std::string const& constantName) : ConstantExpression(double_, constantName), value(0), defined(false) { // Nothing to do here. } - std::shared_ptr DoubleConstantExpression::clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const { + std::shared_ptr DoubleConstantExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new DoubleConstantExpression(*this)); } @@ -30,24 +30,24 @@ namespace storm { } } - virtual void DoubleConstantExpression::accept(ExpressionVisitor* visitor) { + void DoubleConstantExpression::accept(ExpressionVisitor* visitor) { visitor->visit(this); } - virtual std::string DoubleConstantExpression::toString() const { + std::string DoubleConstantExpression::toString() const { std::stringstream result; - result << this->constantName; + result << this->getConstantName(); if (defined) { result << "[" << value << "]"; } return result.str(); } - bool DoubleConstantExpression::isDefined() { + bool DoubleConstantExpression::isDefined() const { return defined; } - double DoubleConstantExpression::getValue() { + double DoubleConstantExpression::getValue() const { return value; } diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h index 48faaa3a0..6a996ff45 100644 --- a/src/ir/expressions/DoubleConstantExpression.h +++ b/src/ir/expressions/DoubleConstantExpression.h @@ -19,9 +19,14 @@ namespace storm { */ class DoubleConstantExpression : public ConstantExpression { public: + /*! + * Creates a double constant expression with the given constant name. + * + * @param constantName The name of the constant to use. + */ DoubleConstantExpression(std::string const& constantName); - virtual std::shared_ptr clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/DoubleLiteralExpression.cpp b/src/ir/expressions/DoubleLiteralExpression.cpp index fecfb4556..9508767ff 100644 --- a/src/ir/expressions/DoubleLiteralExpression.cpp +++ b/src/ir/expressions/DoubleLiteralExpression.cpp @@ -17,19 +17,19 @@ namespace storm { // Nothing to do here. } - virtual std::shared_ptr DoubleLiteralExpression::clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const { - return std::shared_ptr(new DoubleLiteral(this->value)); + std::shared_ptr DoubleLiteralExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { + return std::shared_ptr(new DoubleLiteralExpression(this->value)); } - virtual double DoubleLiteralExpression::getValueAsDouble(std::pair, std::vector> const* variableValues) const { + double DoubleLiteralExpression::getValueAsDouble(std::pair, std::vector> const* variableValues) const { return value; } - virtual void DoubleLiteralExpression::accept(ExpressionVisitor* visitor) { + void DoubleLiteralExpression::accept(ExpressionVisitor* visitor) { visitor->visit(this); } - virtual std::string DoubleLiteralExpression::toString() const { + std::string DoubleLiteralExpression::toString() const { std::stringstream result; result << value; return result.str(); diff --git a/src/ir/expressions/DoubleLiteralExpression.h b/src/ir/expressions/DoubleLiteralExpression.h index bf37351e8..fd020485a 100644 --- a/src/ir/expressions/DoubleLiteralExpression.h +++ b/src/ir/expressions/DoubleLiteralExpression.h @@ -26,7 +26,7 @@ namespace storm { */ DoubleLiteralExpression(double value); - virtual std::shared_ptr clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const override; @@ -35,7 +35,7 @@ namespace storm { virtual std::string toString() const override; private: - // The value of the boolean literal. + // The value of the double literal. double value; }; diff --git a/src/ir/expressions/Expressions.h b/src/ir/expressions/Expressions.h index 0de025b9f..634a0585d 100644 --- a/src/ir/expressions/Expressions.h +++ b/src/ir/expressions/Expressions.h @@ -12,9 +12,9 @@ #include "BinaryBooleanFunctionExpression.h" #include "BinaryNumericalFunctionExpression.h" #include "BinaryRelationExpression.h" -#include "BooleanLiteral.h" -#include "DoubleLiteral.h" -#include "IntegerLiteral.h" +#include "BooleanLiteralExpression.h" +#include "DoubleLiteralExpression.h" +#include "IntegerLiteralExpression.h" #include "UnaryBooleanFunctionExpression.h" #include "UnaryNumericalFunctionExpression.h" #include "VariableExpression.h" diff --git a/src/ir/expressions/IntegerConstantExpression.cpp b/src/ir/expressions/IntegerConstantExpression.cpp new file mode 100644 index 000000000..15d04c5d1 --- /dev/null +++ b/src/ir/expressions/IntegerConstantExpression.cpp @@ -0,0 +1,59 @@ +/* + * IntegerConstantExpression.cpp + * + * Created on: 10.06.2013 + * Author: Christian Dehnert + */ + +#include "IntegerConstantExpression.h" + +namespace storm { + namespace ir { + namespace expressions { + + IntegerConstantExpression::IntegerConstantExpression(std::string const& constantName) : ConstantExpression(int_, constantName), value(0), defined(false) { + // Nothing to do here. + } + + std::shared_ptr IntegerConstantExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { + return std::shared_ptr(new IntegerConstantExpression(*this)); + } + + int_fast64_t IntegerConstantExpression::getValueAsInt(std::pair, std::vector> const* variableValues) const { + if (!defined) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Integer constant '" << this->getConstantName() << "' is undefined."; + } else { + return value; + } + } + + void IntegerConstantExpression::accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + std::string IntegerConstantExpression::toString() const { + std::stringstream result; + result << this->getConstantName(); + if (defined) { + result << "[" << value << "]"; + } + return result.str(); + } + + bool IntegerConstantExpression::isDefined() const { + return defined; + } + + int_fast64_t IntegerConstantExpression::getValue() const { + return value; + } + + void IntegerConstantExpression::define(int_fast64_t value) { + defined = true; + this->value = value; + } + + } // namespace expressions + } // namespace ir +} // namespace storm \ No newline at end of file diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h index 00406fe8c..80676f246 100644 --- a/src/ir/expressions/IntegerConstantExpression.h +++ b/src/ir/expressions/IntegerConstantExpression.h @@ -2,84 +2,67 @@ * IntegerConstantExpression.h * * Created on: 04.01.2013 - * Author: chris + * Author: Christian Dehnert */ -#ifndef INTEGERCONSTANTEXPRESSION_H_ -#define INTEGERCONSTANTEXPRESSION_H_ +#ifndef STORM_IR_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_ +#define STORM_IR_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_ #include "ConstantExpression.h" namespace storm { - -namespace ir { - -namespace expressions { - -class IntegerConstantExpression : public ConstantExpression { -public: - IntegerConstantExpression(std::string constantName) : ConstantExpression(int_, constantName), defined(false), value(0) { - } - IntegerConstantExpression(const IntegerConstantExpression& ice) - : ConstantExpression(ice), defined(ice.defined), value(ice.value) { - } - - virtual ~IntegerConstantExpression() { - - } - - virtual std::shared_ptr clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const { - return std::shared_ptr(new IntegerConstantExpression(*this)); - } - - virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { - if (!defined) { - throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Integer constant '" << this->getConstantName() << "' is undefined."; - } else { - return value; - } - } - - virtual void accept(ExpressionVisitor* visitor) { - visitor->visit(this); - } - - virtual std::string toString() const { - std::string result = this->constantName; - if (defined) { - result += "[" + boost::lexical_cast(value) + "]"; - } - return result; - } - virtual std::string dump(std::string prefix) const { - std::stringstream result; - result << prefix << "IntegerConstantExpression " << this->toString() << std::endl; - return result.str(); - } - - bool isDefined() { - return defined; - } - - int_fast64_t getValue() { - return value; - } - - void define(int_fast64_t value) { - defined = true; - this->value = value; - } - -private: - bool defined; - int_fast64_t value; -}; - -} - -} - -} - -#endif /* INTEGERCONSTANTEXPRESSION_H_ */ + namespace ir { + namespace expressions { + + /*! + * A class representing a constant expression of type integer. + */ + class IntegerConstantExpression : public ConstantExpression { + public: + /*! + * Creates an integer constant expression with the given constant name. + * + * @param constantName The name of the constant to use. + */ + IntegerConstantExpression(std::string const& constantName); + + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; + + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const override; + + virtual void accept(ExpressionVisitor* visitor) override; + + virtual std::string toString() const override; + + /*! + * Retrieves whether the constant is defined or not. + * + * @return True if the constant is defined. + */ + bool isDefined() const; + + /*! + * Retrieves the value of the constant if it is defined and false otherwise. + */ + int_fast64_t getValue() const; + + /*! + * Defines the constant using the given value. + * + * @param value The value to use for defining the constant. + */ + void define(int_fast64_t value); + + private: + // This member stores the value of the constant if it is defined. + int_fast64_t value; + + // A flag indicating whether the member is defined or not. + bool defined; + }; + + } // namespace expressions + } // namespace ir +} // namespace storm + +#endif /* STORM_IR_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_ */ diff --git a/src/ir/expressions/IntegerLiteral.h b/src/ir/expressions/IntegerLiteral.h deleted file mode 100644 index d89e63fbf..000000000 --- a/src/ir/expressions/IntegerLiteral.h +++ /dev/null @@ -1,57 +0,0 @@ -/* - * IntegerLiteral.h - * - * Created on: 03.01.2013 - * Author: chris - */ - -#ifndef INTEGERLITERAL_H_ -#define INTEGERLITERAL_H_ - -#include "src/ir/expressions/BaseExpression.h" - -namespace storm { - -namespace ir { - -namespace expressions { - -class IntegerLiteral : public BaseExpression { -public: - int_fast64_t value; - - IntegerLiteral(int_fast64_t value) : BaseExpression(int_), value(value) { - } - - virtual ~IntegerLiteral() { - } - - virtual std::shared_ptr clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const { - return std::shared_ptr(new IntegerLiteral(this->value)); - } - - virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { - return value; - } - - virtual void accept(ExpressionVisitor* visitor) { - visitor->visit(this); - } - - virtual std::string toString() const { - return boost::lexical_cast(value); - } - virtual std::string dump(std::string prefix) const { - std::stringstream result; - result << prefix << "IntegerLiteral " << this->toString() << std::endl; - return result.str(); - } -}; - -} - -} - -} - -#endif /* INTEGERLITERAL_H_ */ diff --git a/src/ir/expressions/IntegerLiteralExpression.cpp b/src/ir/expressions/IntegerLiteralExpression.cpp new file mode 100644 index 000000000..24c4bed21 --- /dev/null +++ b/src/ir/expressions/IntegerLiteralExpression.cpp @@ -0,0 +1,40 @@ +/* + * IntegerLiteralExpression.cpp + * + * Created on: 03.01.2013 + * Author: Christian Dehnert + */ + +#include + +#include "IntegerLiteralExpression.h" + +namespace storm { + namespace ir { + namespace expressions { + + IntegerLiteralExpression::IntegerLiteralExpression(int_fast64_t value) : BaseExpression(int_), value(value) { + // Nothing to do here. + } + + std::shared_ptr IntegerLiteralExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { + return std::shared_ptr(new IntegerLiteralExpression(this->value)); + } + + int_fast64_t IntegerLiteralExpression::getValueAsInt(std::pair, std::vector> const* variableValues) const { + return value; + } + + void IntegerLiteralExpression::accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + std::string IntegerLiteralExpression::toString() const { + std::stringstream result; + result << value; + return result.str(); + } + + } // namespace expressions + } // namespace ir +} // namespace storm \ No newline at end of file diff --git a/src/ir/expressions/IntegerLiteralExpression.h b/src/ir/expressions/IntegerLiteralExpression.h new file mode 100644 index 000000000..c824ef022 --- /dev/null +++ b/src/ir/expressions/IntegerLiteralExpression.h @@ -0,0 +1,46 @@ +/* + * IntegerLiteralExpression.h + * + * Created on: 03.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_ +#define STORM_IR_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_ + +#include "src/ir/expressions/BaseExpression.h" + +namespace storm { + namespace ir { + namespace expressions { + + /*! + * A class representing an integer literal. + */ + class IntegerLiteralExpression : public BaseExpression { + public: + /*! + * Creates an integer literal expression with the given value. + * + * @param value The value for the integer literal. + */ + IntegerLiteralExpression(int_fast64_t value); + + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; + + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const override; + + virtual void accept(ExpressionVisitor* visitor) override; + + virtual std::string toString() const override; + + private: + // The value of the double literal. + int_fast64_t value; + }; + + } // namespace expressions + } // namespace ir +} // namespace storm + +#endif /* STORM_IR_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_ */ diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.cpp b/src/ir/expressions/UnaryBooleanFunctionExpression.cpp new file mode 100644 index 000000000..9f8443985 --- /dev/null +++ b/src/ir/expressions/UnaryBooleanFunctionExpression.cpp @@ -0,0 +1,56 @@ +/* + * UnaryBooleanFunctionExpression.cpp + * + * Created on: 10.06.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_ +#define STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_ + +#include + +#include "UnaryBooleanFunctionExpression.h" + +namespace storm { + namespace ir { + namespace expressions { + + UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(std::shared_ptr child, FunctionType functionType) : UnaryExpression(bool_, child), functionType(functionType) { + // Nothing to do here. + } + + std::shared_ptr UnaryBooleanFunctionExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { + return std::shared_ptr(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, variableState), this->functionType)); + } + + FunctionType UnaryBooleanFunctionExpression::getFunctionType() const { + return functionType; + } + + bool UnaryBooleanFunctionExpression::getValueAsBool(std::pair, std::vector> const* variableValues) const { + bool resultChild = this->getChild()->getValueAsBool(variableValues); + switch(functionType) { + case NOT: return !resultChild; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean unary operator: '" << functionType << "'."; + } + } + + void UnaryBooleanFunctionExpression::accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + std::string UnaryBooleanFunctionExpression::toString() const { + std::stringstream result; + switch (functionType) { + case NOT: result << "!"; break; + } + result << "(" << this->getChild()->toString() << ")"; + + return result.str(); + } + + } // namespace expressions + } // namespace ir +} // namespace storm diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.h b/src/ir/expressions/UnaryBooleanFunctionExpression.h index 06ea12172..957c223a8 100644 --- a/src/ir/expressions/UnaryBooleanFunctionExpression.h +++ b/src/ir/expressions/UnaryBooleanFunctionExpression.h @@ -2,80 +2,60 @@ * UnaryBooleanFunctionExpression.h * * Created on: 03.01.2013 - * Author: chris + * Author: Christian Dehnert */ -#ifndef UNARYBOOLEANFUNCTIONEXPRESSION_H_ -#define UNARYBOOLEANFUNCTIONEXPRESSION_H_ +#ifndef STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_ +#define STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_ -#include "src/ir/expressions/UnaryExpression.h" +#include "UnaryExpression.h" namespace storm { - -namespace ir { - -namespace expressions { - -class UnaryBooleanFunctionExpression : public UnaryExpression { -public: - enum FunctionType {NOT}; - - UnaryBooleanFunctionExpression(std::shared_ptr child, FunctionType functionType) : UnaryExpression(bool_, child), functionType(functionType) { - - } - - virtual ~UnaryBooleanFunctionExpression() { - - } - - virtual std::shared_ptr clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const { - return std::shared_ptr(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, variableState), this->functionType)); - } - - FunctionType getFunctionType() const { - return functionType; - } - - virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { - bool resultChild = this->getChild()->getValueAsBool(variableValues); - switch(functionType) { - case NOT: return !resultChild; break; - default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean unary operator: '" << functionType << "'."; - } - } - - virtual void accept(ExpressionVisitor* visitor) { - visitor->visit(this); - } - - virtual std::string toString() const { - std::string result = ""; - switch (functionType) { - case NOT: result += "!"; break; - } - result += "(" + this->getChild()->toString() + ")"; - - return result; - } - virtual std::string dump(std::string prefix) const { - std::stringstream result; - result << prefix << "UnaryBooleanFunctionExpression" << std::endl; - switch (functionType) { - case NOT: result << prefix << "!" << std::endl; break; - } - result << this->getChild()->dump(prefix + "\t"); - return result.str(); - } - -private: - FunctionType functionType; -}; - -} - -} - -} - -#endif /* UNARYBOOLEANFUNCTIONEXPRESSION_H_ */ + namespace ir { + namespace expressions { + + /*! + * A class representing a unary function expression of boolean type. + */ + class UnaryBooleanFunctionExpression : public UnaryExpression { + public: + /*! + * An enum type specifying the different functions applicable. + */ + enum FunctionType {NOT}; + + /*! + * Creates a unary boolean function expression tree node with the given child and function type. + * + * @param child The child of the node. + * @param functionType The operator that is to be applied to the two children. + */ + UnaryBooleanFunctionExpression(std::shared_ptr child, FunctionType functionType); + + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; + + /*! + * Retrieves the operator that is associated with this node. + * + * @param The operator that is associated with this node. + */ + FunctionType getFunctionType() const { + return functionType; + } + + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const override; + + virtual void accept(ExpressionVisitor* visitor) override; + + virtual std::string toString() const override; + + private: + // The operator that is associated with this node. + FunctionType functionType; + }; + + } // namespace expressions + } // namespace ir +} // namespace storm + +#endif /* STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_ */ diff --git a/src/ir/expressions/UnaryExpression.cpp b/src/ir/expressions/UnaryExpression.cpp new file mode 100644 index 000000000..0198cf295 --- /dev/null +++ b/src/ir/expressions/UnaryExpression.cpp @@ -0,0 +1,24 @@ +/* + * UnaryExpression.cpp + * + * Created on: 27.01.2013 + * Author: Christian Dehnert + */ + +#include "UnaryExpression.h" + +namespace storm { + namespace ir { + namespace expressions { + + UnaryExpression::UnaryExpression(ReturnType type, std::shared_ptr child) : BaseExpression(type), child(child) { + // Nothing to do here. + } + + std::shared_ptr const& UnaryExpression::getChild() const { + return child; + } + + } // namespace expressions + } // namespace ir +} // namespace storm diff --git a/src/ir/expressions/UnaryExpression.h b/src/ir/expressions/UnaryExpression.h index 177b5593e..492c43faf 100644 --- a/src/ir/expressions/UnaryExpression.h +++ b/src/ir/expressions/UnaryExpression.h @@ -11,29 +11,35 @@ #include "BaseExpression.h" namespace storm { - -namespace ir { - -namespace expressions { - -class UnaryExpression : public BaseExpression { -public: - UnaryExpression(ReturnType type, std::shared_ptr child) : BaseExpression(type), child(child) { - - } - - std::shared_ptr const& getChild() const { - return child; - } - -private: - std::shared_ptr child; -}; - -} // namespace expressions - -} // namespace ir - + namespace ir { + namespace expressions { + + /*! + * A class representing a generic unary expression. + */ + class UnaryExpression : public BaseExpression { + public: + /*! + * Constructs a unary expression with the given type and child. + * @param type The type of the unary expression. + * @param right The child of the unary expression. + */ + UnaryExpression(ReturnType type, std::shared_ptr child); + + /*! + * Retrieves the child of the expression node. + * + * @return The child of the expression node. + */ + std::shared_ptr const& getChild() const; + + private: + // The left child of the unary expression. + std::shared_ptr child; + }; + + } // namespace expressions + } // namespace ir } // namespace storm #endif /* STORM_IR_EXPRESSIONS_UNARYEXPRESSION_H_ */ diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.cpp b/src/ir/expressions/UnaryNumericalFunctionExpression.cpp new file mode 100644 index 000000000..7985a4ccd --- /dev/null +++ b/src/ir/expressions/UnaryNumericalFunctionExpression.cpp @@ -0,0 +1,69 @@ +/* + * UnaryFunctionExpression.h + * + * Created on: 03.01.2013 + * Author: Christian Dehnert + */ + +#include "UnaryNumericalFunctionExpression.h" + +namespace storm { + namespace ir { + namespace expressions { + + UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr child, FunctionType functionType) : UnaryExpression(type, child), functionType(functionType) { + // Nothing to do here. + } + + std::shared_ptr UnaryNumericalFunctionExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { + return std::shared_ptr(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, variableState), this->functionType)); + } + + int_fast64_t UnaryNumericalFunctionExpression::getValueAsInt(std::pair, std::vector> const* variableValues) const { + if (this->getType() != int_) { + BaseExpression::getValueAsInt(variableValues); + } + + int_fast64_t resultChild = this->getChild()->getValueAsInt(variableValues); + switch(functionType) { + case MINUS: return -resultChild; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown numerical unary operator: '" << functionType << "'."; + } + } + + double UnaryNumericalFunctionExpression::getValueAsDouble(std::pair, std::vector> const* variableValues) const { + if (this->getType() != double_) { + BaseExpression::getValueAsDouble(variableValues); + } + + double resultChild = this->getChild()->getValueAsDouble(variableValues); + switch(functionType) { + case MINUS: return -resultChild; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown numerical unary operator: '" << functionType << "'."; + } + } + + FunctionType UnaryNumericalFunctionExpression::getFunctionType() const { + return functionType; + } + + void UnaryNumericalFunctionExpression::accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + std::string UnaryNumericalFunctionExpression::toString() const { + std::string result = ""; + switch (functionType) { + case MINUS: result += "-"; break; + } + result += this->getChild()->toString(); + + return result; + } + + } // namespace expressions + } // namespace ir +} // namespace storm + diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h index 73b0dca87..3a1bfcab0 100644 --- a/src/ir/expressions/UnaryNumericalFunctionExpression.h +++ b/src/ir/expressions/UnaryNumericalFunctionExpression.h @@ -2,98 +2,62 @@ * UnaryFunctionExpression.h * * Created on: 03.01.2013 - * Author: chris + * Author: Christian Dehnert */ -#ifndef UNARYFUNCTIONEXPRESSION_H_ -#define UNARYFUNCTIONEXPRESSION_H_ +#ifndef STORM_IR_EXPRESSIONS_UNARYFUNCTIONEXPRESSION_H_ +#define STORM_IR_EXPRESSIONS_UNARYFUNCTIONEXPRESSION_H_ -#include "src/ir/expressions/UnaryExpression.h" +#include "UnaryExpression.h" namespace storm { - -namespace ir { - -namespace expressions { - -class UnaryNumericalFunctionExpression : public UnaryExpression { -public: - enum FunctionType {MINUS}; - - UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr child, FunctionType functionType) : UnaryExpression(type, child), functionType(functionType) { - - } - - virtual ~UnaryNumericalFunctionExpression() { - - } - - virtual std::shared_ptr clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const { - return std::shared_ptr(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, variableState), this->functionType)); - } - - virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { - if (this->getType() != int_) { - BaseExpression::getValueAsInt(variableValues); - } - - int_fast64_t resultChild = this->getChild()->getValueAsInt(variableValues); - switch(functionType) { - case MINUS: return -resultChild; break; - default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown numerical unary operator: '" << functionType << "'."; - } - } - - virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const { - if (this->getType() != double_) { - BaseExpression::getValueAsDouble(variableValues); - } - - double resultChild = this->getChild()->getValueAsDouble(variableValues); - switch(functionType) { - case MINUS: return -resultChild; break; - default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown numerical unary operator: '" << functionType << "'."; - } - } - - FunctionType getFunctionType() const { - return functionType; - } - - virtual void accept(ExpressionVisitor* visitor) { - visitor->visit(this); - } - - virtual std::string toString() const { - std::string result = ""; - switch (functionType) { - case MINUS: result += "-"; break; - } - result += this->getChild()->toString(); - - return result; - } - - virtual std::string dump(std::string prefix) const { - std::stringstream result; - result << prefix << "UnaryNumericalFunctionExpression" << std::endl; - switch (functionType) { - case MINUS: result << prefix << "-" << std::endl; break; - } - result << this->getChild()->dump(prefix + "\t"); - return result.str(); - } - -private: - FunctionType functionType; -}; - -} - -} - -} - -#endif /* UNARYFUNCTIONEXPRESSION_H_ */ + namespace ir { + namespace expressions { + + /*! + * A class representing a unary function expression of numerical type. + */ + class UnaryNumericalFunctionExpression : public UnaryExpression { + public: + /*! + * An enum type specifying the different functions applicable. + */ + enum FunctionType {MINUS}; + + /*! + * Creates a unary numerical function expression tree node with the given child and function type. + * + * @param child The child of the node. + * @param functionType The operator that is to be applied to the two children. + */ + UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr child, FunctionType functionType); + + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; + + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const override; + + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const override; + + /*! + * Retrieves the operator that is associated with this node. + * + * @param The operator that is associated with this node. + */ + FunctionType getFunctionType() const { + return functionType; + } + + virtual void accept(ExpressionVisitor* visitor) override; + + virtual std::string toString() const override; + + private: + // The operator that is associated with this node. + FunctionType functionType; + }; + + } // namespace expressions + } // namespace ir +} // namespace storm + +#endif /* STORM_IR_EXPRESSIONS_UNARYFUNCTIONEXPRESSION_H_ */ diff --git a/src/ir/expressions/VariableExpression.cpp b/src/ir/expressions/VariableExpression.cpp index 474c67f05..245c9f50d 100644 --- a/src/ir/expressions/VariableExpression.cpp +++ b/src/ir/expressions/VariableExpression.cpp @@ -7,30 +7,22 @@ #include "VariableExpression.h" #include "src/parser/prismparser/VariableState.h" +#include "src/exceptions/ExpressionEvaluationException.h" namespace storm { namespace ir { namespace expressions { - VariableExpression::VariableExpression(ReturnType type, std::string variableName) : BaseExpression(type), localIndex(0), globalIndex(0), variableName(variableName) { + VariableExpression::VariableExpression(ReturnType type, std::string const& variableName) : BaseExpression(type), globalIndex(0), variableName(variableName) { // Nothing to do here. } - VariableExpression::VariableExpression(ReturnType type, uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string variableName) - : BaseExpression(type), localIndex(localIndex), globalIndex(globalIndex), variableName(variableName) { + VariableExpression::VariableExpression(ReturnType type, uint_fast64_t globalIndex, std::string const& variableName) + : BaseExpression(type), globalIndex(globalIndex), variableName(variableName) { // Nothing to do here. } - VariableExpression::VariableExpression(VariableExpression const& oldExpression, std::string const& newName, uint_fast64_t newGlobalIndex) - : BaseExpression(oldExpression.getType()), localIndex(oldExpression.localIndex), globalIndex(newGlobalIndex), variableName(newName) { - // Nothing to do here. - } - - virtual VariableExpression::~VariableExpression() { - // Nothing to do here. - } - - virtual std::shared_ptr VariableExpression::clone(std::map const& renaming, VariableState const& variableState) { + std::shared_ptr VariableExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { // Perform the proper cloning. auto renamingPair = renaming.find(this->variableName); if (renamingPair != renaming.end()) { @@ -40,22 +32,15 @@ namespace storm { } } - virtual void VariableExpression::accept(ExpressionVisitor* visitor) { - std::cout << "Visitor!" << std::endl; + void VariableExpression::accept(ExpressionVisitor* visitor) { visitor->visit(this); } - virtual std::string VariableExpression::toString() const { + std::string VariableExpression::toString() const { return this->variableName; } - virtual std::string VariableExpression::dump(std::string prefix) const { - std::stringstream result; - result << prefix << this->variableName << " " << index << std::endl; - return result.str(); - } - - virtual int_fast64_t VariableExpression::getValueAsInt(std::pair, std::vector> const* variableValues) const { + int_fast64_t VariableExpression::getValueAsInt(std::pair, std::vector> const* variableValues) const { if (this->getType() != int_) { BaseExpression::getValueAsInt(variableValues); } @@ -68,7 +53,7 @@ namespace storm { } } - virtual bool VariableExpression::getValueAsBool(std::pair, std::vector> const* variableValues) const { + bool VariableExpression::getValueAsBool(std::pair, std::vector> const* variableValues) const { if (this->getType() != bool_) { BaseExpression::getValueAsBool(variableValues); } @@ -81,12 +66,12 @@ namespace storm { } } - virtual double VariableExpression::getValueAsDouble(std::pair, std::vector> const* variableValues) const { + double VariableExpression::getValueAsDouble(std::pair, std::vector> const* variableValues) const { if (this->getType() != double_) { BaseExpression::getValueAsDouble(variableValues); } - throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression with " + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression with " << " variable '" << variableName << "' of type double."; } @@ -94,14 +79,10 @@ namespace storm { return variableName; } - uint_fast64_t VariableExpression::getLocalVariableIndex() const { - return this->localIndex; - } - uint_fast64_t VariableExpression::getGlobalVariableIndex() const { return this->globalIndex; } } // namespace expressions } // namespace ir -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h index ef5b8388c..9a8d47172 100644 --- a/src/ir/expressions/VariableExpression.h +++ b/src/ir/expressions/VariableExpression.h @@ -5,18 +5,10 @@ * Author: Christian Dehnert */ -#ifndef VARIABLEEXPRESSION_H_ -#define VARIABLEEXPRESSION_H_ - -#include -#include +#ifndef STORM_IR_EXPRESSIONS_VARIABLEEXPRESSION_H_ +#define STORM_IR_EXPRESSIONS_VARIABLEEXPRESSION_H_ #include "BaseExpression.h" -#include "src/exceptions/InvalidArgumentException.h" - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; namespace storm { @@ -30,37 +22,60 @@ namespace storm { namespace ir { namespace expressions { + /*! + * A class representing a variable in the expression tree. + */ class VariableExpression : public BaseExpression { public: - VariableExpression(ReturnType type, std::string variableName); - - VariableExpression(ReturnType type, uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string variableName); + /*! + * Creates a variable expression of the given type with the given name. As this variable has no indices + * it is only meant as a dummy and needs to be replaced with a "full" variable expression. + * + * @param type The type of the variable. + * @param variableName The name of the variable. + */ + VariableExpression(ReturnType type, std::string const& variableName); - VariableExpression(VariableExpression const& oldExpression, std::string const& newName, uint_fast64_t newGlobalIndex); + /*! + * Creates a variable expression of the given type with the given name and indices. + * + * @param type The type of the variable. + * @param globalIndex The global (i.e. program-wide) index of the variable. + * @param variableName The name of the variable. + */ + VariableExpression(ReturnType type, uint_fast64_t globalIndex, std::string const& variableName); + + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; - virtual ~VariableExpression(); + virtual void accept(ExpressionVisitor* visitor) override; - virtual std::shared_ptr clone(std::map const& renaming, parser::prismparser::VariableState const& variableState) const; + virtual std::string toString() const override; - virtual void accept(ExpressionVisitor* visitor); + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const override; - virtual std::string toString() const; + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const override; - virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const; - - virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const; - - virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const; + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const override; + /*! + * Retrieves the name of the variable. + * + * @return The name of the variable. + */ std::string const& getVariableName() const; - uint_fast64_t getLocalVariableIndex() const; - + /*! + * Retrieves the global (i.e. program-wide) index of the variable. + * + * @return The global index of the variable. + */ uint_fast64_t getGlobalVariableIndex() const; private: - uint_fast64_t localIndex; + // The global index of the variable. uint_fast64_t globalIndex; + + // The name of the variable. std::string variableName; }; @@ -68,4 +83,4 @@ namespace storm { } // namespace ir } // namespace storm -#endif /* VARIABLEEXPRESSION_H_ */ +#endif /* STORM_IR_EXPRESSIONS_VARIABLEEXPRESSION_H_ */ diff --git a/src/parser/prismparser/BaseGrammar.h b/src/parser/prismparser/BaseGrammar.h index e0c5d4df8..ab6059820 100644 --- a/src/parser/prismparser/BaseGrammar.h +++ b/src/parser/prismparser/BaseGrammar.h @@ -63,7 +63,7 @@ namespace prism { * @returns Boolean literal. */ std::shared_ptr createBoolLiteral(const bool value) { - return std::shared_ptr(new BooleanLiteral(value)); + return std::shared_ptr(new BooleanLiteralExpression(value)); } /*! * Create a new double literal with the given value. @@ -71,7 +71,7 @@ namespace prism { * @returns Double literal. */ std::shared_ptr createDoubleLiteral(const double value) { - return std::shared_ptr(new DoubleLiteral(value)); + return std::shared_ptr(new DoubleLiteralExpression(value)); } /*! * Create a new integer literal with the given value. @@ -79,7 +79,7 @@ namespace prism { * @returns Integer literal. */ std::shared_ptr createIntLiteral(const int_fast64_t value) { - return std::shared_ptr(new IntegerLiteral(value)); + return std::shared_ptr(new IntegerLiteralExpression(value)); } /*! @@ -184,7 +184,7 @@ namespace prism { * @returns Boolean variable. */ std::shared_ptr getBoolVariable(const std::string name) { - return state->getBooleanVariable(name); + return state->getBooleanVariableExpression(name); } /*! * Retrieve integer variable by name. @@ -192,7 +192,7 @@ namespace prism { * @returns Integer variable. */ std::shared_ptr getIntVariable(const std::string name) { - return state->getIntegerVariable(name); + return state->getIntegerVariableExpression(name); } /*! diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index 79459f3e7..341e22a66 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -22,6 +22,7 @@ #include "src/parser/prismparser/IntegerExpressionGrammar.h" #include "src/parser/prismparser/IdentifierGrammars.h" #include "src/parser/prismparser/VariableState.h" +#include "src/exceptions/InvalidArgumentException.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -63,33 +64,34 @@ void PrismGrammar::addBooleanAssignment(std::string const& variable, std::shared } Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map& renaming) { - this->state->moduleNames_.add(name, name); - Module* old = this->moduleMap_.find(oldname); + 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(name) = res; + Module res(*old, newName, renaming, *this->state); + this->moduleMap_.at(newName) = res; return res; } -Module PrismGrammar::createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector commands) { +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(const std::string name, std::shared_ptr lower, std::shared_ptr upper, std::shared_ptr init, std::vector& vars, std::map& varids) { +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) { uint_fast64_t id = this->state->addIntegerVariable(name); - vars.emplace_back(id, name, lower, upper, init); + vars.emplace_back(this->state->nextLocalIntegerVariableIndex++, id, name, lower, upper, init); varids[name] = id; this->state->localIntegerVariables_.add(name, name); } -void PrismGrammar::createBooleanVariable(const std::string name, std::shared_ptr init, std::vector& vars, std::map& varids) { + +void PrismGrammar::createBooleanVariable(std::string const& name, std::shared_ptr const& init, std::vector& vars, std::map& varids) { uint_fast64_t id = this->state->addBooleanVariable(name); - vars.emplace_back(id, name, init); + vars.emplace_back(this->state->nextLocalIntegerVariableIndex++, id, name, init); varids[name] = id; this->state->localBooleanVariables_.add(name, name); } @@ -148,8 +150,8 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl // This block defines all entities that are needed for parsing a single command. assignmentDefinition = - (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > IntegerExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addIntAssignment, this, qi::_1, qi::_2, qi::_r2)] | - (qi::lit("(") >> unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addBoolAssignment, this, qi::_1, qi::_2, qi::_r1)]; + (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > IntegerExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addIntegerAssignment, this, qi::_1, qi::_2, qi::_r2)] | + (qi::lit("(") >> unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addBooleanAssignment, this, qi::_1, qi::_2, qi::_r1)]; assignmentDefinition.name("assignment"); assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&"; assignmentDefinitionList.name("assignment list"); diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h index 6aeb0282e..5731e35c7 100644 --- a/src/parser/prismparser/PrismGrammar.h +++ b/src/parser/prismparser/PrismGrammar.h @@ -192,7 +192,7 @@ private: * @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 integerVariableToLocalIndexMap, std::vector const& commands); + 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 @@ -202,10 +202,9 @@ private: * @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 integerVariableToLocalIndexMap A mapping of integer variables to local indices. * @param integerVariableToGlobalIndexMap A mapping of integer variables to global indices. */ - 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& integerVariableToLocalIndexMap, std::map& integerVariableToGlobalIndexMap); + 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); /*! * Creates an boolean variable with the given name and initial value and adds it to the @@ -213,10 +212,9 @@ private: * * @param name The name of the boolean variable. * @param init The expression that defines the initial value of the variable. - * @param booleanVariableToLocalIndexMap A mapping of boolean variables to local indices. * @param booleanVariableToGlobalIndexMap A mapping of boolean variables to global indices. */ - void createBooleanVariable(std::string const& name, std::shared_ptr const& init, std::vector& booleanVariables, std::map& booleanVariableToLocalIndexMap, std::map& booleanVariableToGlobalIndexMap); + void createBooleanVariable(std::string const& name, std::shared_ptr const& init, std::vector& booleanVariables, std::map& booleanVariableToGlobalIndexMap); }; diff --git a/src/parser/prismparser/VariableState.cpp b/src/parser/prismparser/VariableState.cpp index c0e57237c..9ee35dd02 100644 --- a/src/parser/prismparser/VariableState.cpp +++ b/src/parser/prismparser/VariableState.cpp @@ -51,18 +51,18 @@ uint_fast64_t VariableState::getNextGlobalIntegerVariableIndex() const { return this->nextGlobalIntegerVariableIndex; } -std::pair VariableState::addBooleanVariable(std::string const& name) { +uint_fast64_t VariableState::addBooleanVariable(std::string const& name) { if (firstRun) { LOG4CPLUS_TRACE(logger, "Adding boolean variable " << name << " with new id " << this->nextGlobalBooleanVariableIndex << "."); - this->booleanVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextLocalBooleanVariableIndex, this->nextGlobalBooleanVariableIndex, name))); + this->booleanVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextGlobalBooleanVariableIndex, name))); this->booleanVariableNames_.add(name, name); ++this->nextGlobalBooleanVariableIndex; ++this->nextLocalBooleanVariableIndex; - return std::make_pair(this->nextLocalBooleanVariableIndex - 1, this->nextGlobalBooleanVariableIndex - 1); + return this->nextGlobalBooleanVariableIndex - 1; } else { std::shared_ptr variableExpression = this->booleanVariables_.at(name); if (variableExpression != nullptr) { - return std::make_pair(variableExpression->getLocalVariableIndex(), variableExpression->getGlobalVariableIndex()); + return variableExpression->getGlobalVariableIndex(); } else { LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist."); throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist."; @@ -70,18 +70,18 @@ std::pair VariableState::addBooleanVariable(std::s } } -std::pair VariableState::addIntegerVariable(std::string const& name) { +uint_fast64_t VariableState::addIntegerVariable(std::string const& name) { if (firstRun) { LOG4CPLUS_TRACE(logger, "Adding integer variable " << name << " with new id " << this->nextGlobalIntegerVariableIndex << "."); - this->integerVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextLocalIntegerVariableIndex, this->nextGlobalIntegerVariableIndex, name))); + this->integerVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextGlobalIntegerVariableIndex, name))); this->integerVariableNames_.add(name, name); ++this->nextGlobalIntegerVariableIndex; ++this->nextLocalIntegerVariableIndex; - return std::make_pair(this->nextLocalIntegerVariableIndex, this->nextGlobalIntegerVariableIndex - 1); + return this->nextGlobalIntegerVariableIndex - 1; } else { std::shared_ptr variableExpression = this->integerVariables_.at(name); if (variableExpression != nullptr) { - return std::make_pair(variableExpression->getLocalVariableIndex(), variableExpression->getGlobalVariableIndex()); + return variableExpression->getGlobalVariableIndex(); } else { LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist."); throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist."; @@ -90,7 +90,7 @@ std::pair VariableState::addIntegerVariable(std::s } std::shared_ptr VariableState::getBooleanVariableExpression(std::string const& name) const { - std::shared_ptr* variableExpression = this->booleanVariables_.find(name); + std::shared_ptr const* variableExpression = this->booleanVariables_.find(name); if (variableExpression != nullptr) { return *variableExpression; } else { @@ -105,7 +105,7 @@ std::shared_ptr VariableState::getBooleanVariableExpression( } std::shared_ptr VariableState::getIntegerVariableExpression(std::string const& name) const { - std::shared_ptr* variableExpression = this->integerVariables_.find(name); + std::shared_ptr const* variableExpression = this->integerVariables_.find(name); if (variableExpression != nullptr) { return *variableExpression; } else { @@ -120,7 +120,7 @@ std::shared_ptr VariableState::getIntegerVariableExpression( } std::shared_ptr VariableState::getVariableExpression(std::string const& name) const { - std::shared_ptr* variableExpression = this->integerVariables_.find(name); + std::shared_ptr const* variableExpression = this->integerVariables_.find(name); if (variableExpression != nullptr) { return *variableExpression; } diff --git a/src/parser/prismparser/VariableState.h b/src/parser/prismparser/VariableState.h index fee670e40..1ca299c43 100644 --- a/src/parser/prismparser/VariableState.h +++ b/src/parser/prismparser/VariableState.h @@ -29,8 +29,8 @@ std::ostream& operator<<(std::ostream& out, qi::symbols& symbols); /*! * This class contains the internal state that is needed for parsing a PRISM model. */ -struct VariableState { - +class VariableState { +public: /*! * Creates a new variable state object. By default, this object will be set to a state in which * it is ready for performing a first run on some input. The first run creates all variables @@ -113,17 +113,17 @@ struct VariableState { * Adds a new boolean variable with the given name. * * @param name The name of the variable. - * @return A pair containing the local and global index of the variable. + * @return The global index of the variable. */ - virtual std::pair addBooleanVariable(std::string const& name); + uint_fast64_t addBooleanVariable(std::string const& name); /*! * Adds a new integer variable with the given name. * * @param name The name of the variable. - * @return A pair containing the local and global index of the variable. + * @return The global index of the variable. */ - virtual std::pair addIntegerVariable(std::string const& name); + uint_fast64_t addIntegerVariable(std::string const& name); /*! * Retrieves the variable expression for the boolean variable with the given name.