diff --git a/src/ir/RewardModel.cpp b/src/ir/RewardModel.cpp index d6611e4ec..974bf1e99 100644 --- a/src/ir/RewardModel.cpp +++ b/src/ir/RewardModel.cpp @@ -5,25 +5,22 @@ * Author: Christian Dehnert */ -#include "RewardModel.h" - #include +#include "RewardModel.h" + namespace storm { namespace ir { -// Initializes all members with their default constructors. RewardModel::RewardModel() : rewardModelName(), stateRewards(), transitionRewards() { // Nothing to do here. } -// Initializes all members according to the given values. -RewardModel::RewardModel(std::string rewardModelName, std::vector stateRewards, std::vector transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) { +RewardModel::RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) { // Nothing to do here. } -// Build a string representation of the reward model. std::string RewardModel::toString() const { std::stringstream result; result << "rewards \"" << rewardModelName << "\"" << std::endl; diff --git a/src/ir/RewardModel.h b/src/ir/RewardModel.h index cb538f173..39c2f652f 100644 --- a/src/ir/RewardModel.h +++ b/src/ir/RewardModel.h @@ -8,12 +8,12 @@ #ifndef STORM_IR_REWARDMODEL_H_ #define STORM_IR_REWARDMODEL_H_ -#include "StateReward.h" -#include "TransitionReward.h" - #include #include +#include "StateReward.h" +#include "TransitionReward.h" + namespace storm { namespace ir { @@ -30,41 +30,47 @@ public: /*! * 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 reward. - * @param transitionRewards A vector of transition-based reward. + * + * @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 rewardModelName, std::vector stateRewards, std::vector transitionRewards); + RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards); /*! - * Retrieves a string representation of this variable. - * @returns a string representation of this variable. + * 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; /*! - * Retrieve state rewards. - * @return State rewards. + * 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 getStateRewards() const; + std::vector const& getStateRewards() const; /*! * Check, if there are any transition rewards. - * @return True, iff there are any transition rewards. + * + * @return True, iff there are any transition rewards associated with this reward model. */ bool hasTransitionRewards() const; /*! - * Retrieve transition rewards. - * @return Transition rewards. + * Retrieves a vector of transition rewards associated with this reward model. + * + * @return A vector of transition rewards associated with this reward model. */ - std::vector getTransitionRewards() const; + std::vector const& getTransitionRewards() const; private: // The name of the reward model. diff --git a/src/ir/StateReward.cpp b/src/ir/StateReward.cpp index 93bf738db..46b2b638c 100644 --- a/src/ir/StateReward.cpp +++ b/src/ir/StateReward.cpp @@ -5,38 +5,28 @@ * Author: Christian Dehnert */ -#include "StateReward.h" - #include +#include "StateReward.h" + namespace storm { namespace ir { -// Initializes all members with their default constructors. StateReward::StateReward() : statePredicate(), rewardValue() { // Nothing to do here. } -// Initializes all members according to the given values. StateReward::StateReward(std::shared_ptr statePredicate, std::shared_ptr rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) { // Nothing to do here. } -// Build a string representation of the state reward. std::string StateReward::toString() const { std::stringstream result; result << "\t" << statePredicate->toString() << ": " << rewardValue->toString() << ";"; return result.str(); } -double StateReward::getReward(std::pair, std::vector> const * state) const { - if (this->statePredicate->getValueAsBool(state)) { - return this->rewardValue->getValueAsDouble(state); - } - return 0; -} - } // namespace ir } // namespace storm diff --git a/src/ir/StateReward.h b/src/ir/StateReward.h index 638b42ed7..17e58cea5 100644 --- a/src/ir/StateReward.h +++ b/src/ir/StateReward.h @@ -8,10 +8,10 @@ #ifndef STORM_IR_STATEREWARD_H_ #define STORM_IR_STATEREWARD_H_ -#include "expressions/BaseExpression.h" - #include +#include "expressions/BaseExpression.h" + namespace storm { namespace ir { @@ -29,27 +29,21 @@ public: /*! * Creates a state reward for the states satisfying the given expression with the value given * by a second expression. - * @param statePredicate the predicate that states earning this state-based reward need to + * + * @param statePredicate The predicate that states earning this state-based reward need to * satisfy. - * @param rewardValue an expression specifying the values of the rewards to attach to the + * @param rewardValue An expression specifying the values of the rewards to attach to the * states. */ StateReward(std::shared_ptr statePredicate, std::shared_ptr rewardValue); /*! * Retrieves a string representation of this state reward. - * @returns a string representation of this state reward. + * + * @return A string representation of this state reward. */ std::string toString() const; - /*! - * Returns the reward for the given state. - * It the state fulfills the predicate, the reward value is returned, zero otherwise. - * @param state State object. - * @return Reward for given state. - */ - double getReward(std::pair, std::vector> const * state) 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 680df77e6..7bf0c645f 100644 --- a/src/ir/TransitionReward.cpp +++ b/src/ir/TransitionReward.cpp @@ -5,39 +5,28 @@ * Author: Christian Dehnert */ -#include "TransitionReward.h" - #include +#include "TransitionReward.h" + namespace storm { namespace ir { -// Initializes all members with their default constructors. TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardValue() { // Nothing to do here. } -// Initializes all members according to the given values. -TransitionReward::TransitionReward(std::string commandName, std::shared_ptr statePredicate, std::shared_ptr rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) { +TransitionReward::TransitionReward(std::string const& commandName, std::shared_ptr statePredicate, std::shared_ptr rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) { // Nothing to do here. } -// Build a string representation of the transition reward. std::string TransitionReward::toString() const { std::stringstream result; result << "\t[" << commandName << "] " << statePredicate->toString() << ": " << rewardValue->toString() << ";"; return result.str(); } -double TransitionReward::getReward(std::string const & label, std::pair, std::vector> const * state) const { - if (this->commandName != label) return 0; - if (this->statePredicate->getValueAsBool(state)) { - return this->rewardValue->getValueAsDouble(state); - } - return 0; -} - } // namespace ir } // namespace storm diff --git a/src/ir/TransitionReward.h b/src/ir/TransitionReward.h index 89480109a..5bb5bd63f 100644 --- a/src/ir/TransitionReward.h +++ b/src/ir/TransitionReward.h @@ -8,10 +8,10 @@ #ifndef STORM_IR_TRANSITIONREWARD_H_ #define STORM_IR_TRANSITIONREWARD_H_ -#include "expressions/BaseExpression.h" - #include +#include "expressions/BaseExpression.h" + namespace storm { namespace ir { @@ -29,26 +29,22 @@ public: /*! * Creates a transition reward for the transitions with the given name emanating from states * satisfying the given expression with the value given by another expression. - * @param commandName the name of the command that obtains this reward. - * @param statePredicate the predicate that needs to hold before taking a transition with the + * + * @param commandName The name of the command that obtains this reward. + * @param statePredicate The predicate that needs to hold before taking a transition with the * previously specified name in order to obtain the reward. - * @param rewardValue an expression specifying the values of the rewards to attach to the + * @param rewardValue An expression specifying the values of the rewards to attach to the * transitions. */ - TransitionReward(std::string commandName, std::shared_ptr statePredicate, std::shared_ptr rewardValue); + TransitionReward(std::string const& commandName, std::shared_ptr statePredicate, std::shared_ptr rewardValue); /*! * Retrieves a string representation of this transition reward. - * @returns a string representation of this transition reward. + * + * @return A string representation of this transition reward. */ std::string toString() const; - /*! - * Retrieves reward for given transition. - * Returns reward value if source state fulfills predicate and the transition is labeled correctly, zero otherwise. - */ - double getReward(std::string const & label, std::pair, std::vector> const * state) const; - private: // The name of the command this transition-based reward is attached to. std::string commandName; diff --git a/src/ir/Update.cpp b/src/ir/Update.cpp index 2d0dc5d2a..4402354ca 100644 --- a/src/ir/Update.cpp +++ b/src/ir/Update.cpp @@ -5,51 +5,47 @@ * Author: Christian Dehnert */ -#include "Update.h" +#include +#include "Update.h" #include "src/exceptions/OutOfRangeException.h" -#include - namespace storm { namespace ir { -// Initializes all members with their default constructors. + Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignments() { // Nothing to do here. } -// Initializes all members according to the given values. Update::Update(std::shared_ptr likelihoodExpression, std::map booleanAssignments, std::map integerAssignments) : likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments) { // Nothing to do here. } -Update::Update(const Update& update, const std::map& renaming, const std::map& bools, const std::map& ints) { +Update::Update(Update const& update, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap) { for (auto it : update.booleanAssignments) { if (renaming.count(it.first) > 0) { - this->booleanAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, bools, ints); + this->booleanAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); } else { - this->booleanAssignments[it.first] = Assignment(it.second, renaming, bools, ints); + this->booleanAssignments[it.first] = Assignment(it.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); } } for (auto it : update.integerAssignments) { if (renaming.count(it.first) > 0) { - this->integerAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, bools, ints); + this->integerAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); } else { - this->integerAssignments[it.first] = Assignment(it.second, renaming, bools, ints); + this->integerAssignments[it.first] = Assignment(it.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap); } } - this->likelihoodExpression = update.likelihoodExpression->clone(renaming, bools, ints); + this->likelihoodExpression = update.likelihoodExpression->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap); } -// Return the expression for the likelihood of the update. std::shared_ptr const& Update::getLikelihoodExpression() const { return likelihoodExpression; } -// Return the number of assignments. uint_fast64_t Update::getNumberOfBooleanAssignments() const { return booleanAssignments.size(); } @@ -58,17 +54,14 @@ uint_fast64_t Update::getNumberOfIntegerAssignments() const { return integerAssignments.size(); } -// Return the boolean variable name to assignment map. std::map const& Update::getBooleanAssignments() const { return booleanAssignments; } -// Return the integer variable name to assignment map. std::map const& Update::getIntegerAssignments() const { return integerAssignments; } -// Return the assignment for the boolean variable if it exists and throw an exception otherwise. storm::ir::Assignment const& Update::getBooleanAssignment(std::string variableName) const { auto it = booleanAssignments.find(variableName); if (it == booleanAssignments.end()) { @@ -79,7 +72,6 @@ storm::ir::Assignment const& Update::getBooleanAssignment(std::string variableNa return (*it).second; } -// Return the assignment for the boolean variable if it exists and throw an exception otherwise. storm::ir::Assignment const& Update::getIntegerAssignment(std::string variableName) const { auto it = integerAssignments.find(variableName); if (it == integerAssignments.end()) { @@ -90,7 +82,6 @@ storm::ir::Assignment const& Update::getIntegerAssignment(std::string variableNa return (*it).second; } -// Build a string representation of the update. std::string Update::toString() const { std::stringstream result; result << likelihoodExpression->toString() << " : "; diff --git a/src/ir/Update.h b/src/ir/Update.h index 4ce6a2fbf..cd19a03a4 100644 --- a/src/ir/Update.h +++ b/src/ir/Update.h @@ -8,12 +8,12 @@ #ifndef STORM_IR_UPDATE_H_ #define STORM_IR_UPDATE_H_ -#include "expressions/BaseExpression.h" -#include "Assignment.h" - #include #include +#include "expressions/BaseExpression.h" +#include "Assignment.h" + namespace storm { namespace ir { @@ -31,58 +31,76 @@ public: /*! * 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. + * + * @param likelihoodExpression An expression specifying the likelihood of this update. + * @param assignments A map of variable names to their assignments. */ Update(std::shared_ptr likelihoodExpression, std::map booleanAssignments, std::map integerAssignments); - Update(const Update& update, const std::map& renaming, const std::map& bools, const std::map& ints); + /*! + * 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. - * @returns 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. - * @returns 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. - * @returns 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. - * @returns 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. - * @returns 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. - * @returns 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 variableName) const; /*! * Retrieves a reference to the assignment for the integer variable with the given name. - * @returns a reference to the assignment for the integer variable with the given name. + * + * @return A reference to the assignment for the integer variable with the given name. */ storm::ir::Assignment const& getIntegerAssignment(std::string variableName) const; /*! * Retrieves a string representation of this update. - * @returns a string representation of this update. + * + * @return A string representation of this update. */ std::string toString() const; @@ -101,4 +119,4 @@ private: } // namespace storm -#endif /*STORM_IR_UPDATE_H_ */ +#endif /* STORM_IR_UPDATE_H_ */ diff --git a/src/ir/Variable.cpp b/src/ir/Variable.cpp index 421603f4f..9e45c1cd1 100644 --- a/src/ir/Variable.cpp +++ b/src/ir/Variable.cpp @@ -5,54 +5,52 @@ * Author: Christian Dehnert */ -#include "Variable.h" - #include #include #include +#include "Variable.h" + namespace storm { namespace ir { -// Initializes all members with their default constructors. -Variable::Variable() : index(0), variableName(), initialValue() { +Variable::Variable() : globalIndex(0), localIndex(0), variableName(), initialValue() { // Nothing to do here. } -// Initializes all members according to the given values. -Variable::Variable(uint_fast64_t index, std::string variableName, std::shared_ptr initialValue) : index(index), variableName(variableName), initialValue(initialValue) { +Variable::Variable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string variableName, std::shared_ptr initialValue) + : globalIndex(globalIndex), localIndex(localIndex), variableName(variableName), initialValue(initialValue) { // Nothing to do here. } -Variable::Variable(const Variable& var, const std::string& newName, const uint_fast64_t newIndex, const std::map& renaming, const std::map& bools, const std::map& ints) { - this->index = newIndex; - this->variableName = newName; +Variable::Variable(Variable const& var, std::string const& newName, uint_fast64_t const newGlobalIndex, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap) + : globalIndex(newGlobalIndex), localIndex(var.getLocalIndex()), variableName(var.getName()) { if (var.initialValue != nullptr) { - this->initialValue = var.initialValue->clone(renaming, bools, ints); + this->initialValue = var.initialValue->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap); } } -// Return the name of the variable. std::string const& Variable::getName() const { return variableName; } -uint_fast64_t Variable::getIndex() const { - return index; +uint_fast64_t Variable::getGlobalIndex() const { + return globalIndex; +} + +uint_fast64_t Variable::getLocalIndex() const { + return localIndex; } -// Return the expression for the initial value of the variable. std::shared_ptr const& Variable::getInitialValue() const { return initialValue; } -// Set the initial value expression to the one provided. 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 610ef903a..05d356e98 100644 --- a/src/ir/Variable.h +++ b/src/ir/Variable.h @@ -8,11 +8,11 @@ #ifndef STORM_IR_VARIABLE_H_ #define STORM_IR_VARIABLE_H_ -#include "expressions/BaseExpression.h" - #include #include +#include "expressions/BaseExpression.h" + namespace storm { namespace ir { @@ -29,46 +29,69 @@ public: /*! * 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 index, std::string variableName, std::shared_ptr initialValue = std::shared_ptr()); + Variable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string variableName, std::shared_ptr initialValue = std::shared_ptr()); /*! - * Creates a copy of the given Variable and gives it a new name. - * @param var Variable to copy. + * 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(const Variable& var, const std::string& newName, const uint_fast64_t newIndex, const std::map& renaming, const std::map& bools, const std::map& ints); + Variable(const Variable& oldVariable, const std::string& newName, const uint_fast64_t newGlobalIndex, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap); /*! * Retrieves the name of the variable. - * @returns the name of the variable. + * + * @return The name of the variable. */ std::string const& getName() const; /*! - * Retrieves the index of the variable. - * @returns the index of the variable. + * 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 getIndex() const; + 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. - * @returns 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. + * + * @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 - uint_fast64_t index; + // A unique (among the variables of equal type) index for the variable over all modules. + uint_fast64_t globalIndex; + + // 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;