diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 5724db8df..6da269889 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -1,177 +1,100 @@ -/* - * Module.cpp - * - * Created on: 12.01.2013 - * Author: Christian Dehnert - */ - -#include -#include -#include "utility/OsDetection.h" - -#include "Module.h" -#include "src/parser/prismparser/VariableState.h" +#include "src/storage/prism/Module.h" +#include "src/exceptions/ExceptionMacros.h" #include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/InvalidArgumentException.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -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() { + namespace prism { + Module::Module(std::string const& moduleName, std::map const& booleanVariables, std::map const& integerVariables, std::vector const& commands) : moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), 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 { - uint_fast64_t globalIndex = variableState.addBooleanVariable(renamingPair->second); - this->booleanVariables.emplace_back(booleanVariable, renamingPair->second, globalIndex, renaming, variableState); - } + Module::Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming) : moduleName(newModuleName), booleanVariables(), integerVariables(), commands(), actions(), actionsToCommandIndexMap() { + // Iterate over boolean variables and rename them. If a variable was not renamed, this is an error and an exception is thrown. + for (auto const& nameVariablePair : oldModule.getBooleanVariables()) { + auto renamingPair = renaming.find(nameVariablePair.first); + LOG_THROW(renamingPair == renaming.end(), storm::exceptions::InvalidArgumentException, "Boolean variable " << moduleName << "." << nameVariablePair.first << " was not renamed."); + this->booleanVariables.emplace(nameVariablePair.first, BooleanVariable(nameVariablePair.second, renamingPair->second, renaming)); } + // 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 { - uint_fast64_t globalIndex = variableState.addIntegerVariable(renamingPair->second); - this->integerVariables.emplace_back(integerVariable, renamingPair->second, globalIndex, renaming, variableState); - } + for (auto const& nameVariablePair : oldModule.getIntegerVariables()) { + auto renamingPair = renaming.find(nameVariablePair.first); + LOG_THROW(renamingPair == renaming.end(), storm::exceptions::InvalidArgumentException, "Integer variable " << moduleName << "." << nameVariablePair.first << " was not renamed."); + this->integerVariables.emplace(nameVariablePair.first, IntegerVariable(nameVariablePair.second, renamingPair->second, renaming)); } // 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, variableState.getNextGlobalCommandIndex(), renaming, variableState); - variableState.nextGlobalCommandIndex++; + for (Command const& command : oldModule.getCommands()) { + this->commands.emplace_back(command, command.getGlobalIndex(), renaming); } - this->collectActions(); - LOG4CPLUS_TRACE(logger, "Finished renaming..."); + // Finally, update internal mapping. + this->collectActions(); } - uint_fast64_t Module::getNumberOfBooleanVariables() const { + std::size_t Module::getNumberOfBooleanVariables() const { return this->booleanVariables.size(); } - storm::ir::BooleanVariable const& Module::getBooleanVariable(uint_fast64_t index) const { - return this->booleanVariables[index]; + std::size_t Module::getNumberOfIntegerVariables() const { + return this->integerVariables.size(); } - storm::ir::BooleanVariable const& Module::getBooleanVariable(std::string const& variableName) const { - uint_fast64_t index = this->getBooleanVariableIndex(variableName); - return this->booleanVariables[index]; + storm::prism::BooleanVariable const& Module::getBooleanVariable(std::string const& variableName) const { + auto const& nameVariablePair = this->getBooleanVariables().find(variableName); + LOG_THROW(nameVariablePair == this->getBooleanVariables().end(), storm::exceptions::InvalidArgumentException, "Unknown boolean variable '" << variableName << "'."); + return nameVariablePair->second; } - uint_fast64_t Module::getNumberOfIntegerVariables() const { - return this->integerVariables.size(); + std::map const& Module::getBooleanVariables() const { + return this->booleanVariables; } - - storm::ir::IntegerVariable const& Module::getIntegerVariable(uint_fast64_t index) const { - return this->integerVariables[index]; + + storm::prism::IntegerVariable const& Module::getIntegerVariable(std::string const& variableName) const { + auto const& nameVariablePair = this->getIntegerVariables().find(variableName); + LOG_THROW(nameVariablePair == this->getIntegerVariables().end(), storm::exceptions::InvalidArgumentException, "Unknown integer variable '" << variableName << "'."); + return nameVariablePair->second; } - storm::ir::IntegerVariable const& Module::getIntegerVariable(std::string const& variableName) const { - uint_fast64_t index = this->getIntegerVariableIndex(variableName); - return this->integerVariables[index]; + std::map const& Module::getIntegerVariables() const { + return this->integerVariables; } - uint_fast64_t Module::getNumberOfCommands() const { + std::size_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::prism::Command const& Module::getCommand(uint_fast64_t index) const { + return this->commands[index]; } - storm::ir::Command const& Module::getCommand(uint_fast64_t index) const { - return this->commands[index]; + std::vector const& Module::getCommands() const { + return this->commands; } 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; } bool Module::hasAction(std::string const& action) const { auto const& actionEntry = this->actions.find(action); - if (actionEntry != this->actions.end()) { - return true; - } - return false; + return actionEntry != this->actions.end(); } - std::set const& Module::getCommandsByAction(std::string const& action) const { + std::set const& Module::getCommandIndicesByAction(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."; + LOG_THROW(false, storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist in module."); } void Module::collectActions() { @@ -199,19 +122,33 @@ namespace storm { } } - void Module::restrictCommands(boost::container::flat_set const& indexSet) { + Module Module::restrictCommands(boost::container::flat_set const& indexSet) { // First construct the new vector of commands. - std::vector newCommands; + std::vector newCommands; for (auto const& command : commands) { if (indexSet.find(command.getGlobalIndex()) != indexSet.end()) { - newCommands.push_back(std::move(command)); + newCommands.push_back(command); } } - commands = std::move(newCommands); - // Then refresh the internal mappings. - this->collectActions(); + return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands); + } + + std::ostream& operator<<(std::ostream& stream, Module const& module) { + stream << "module " << module.getName() << std::endl; + for (auto const& nameVariablePair : module.getBooleanVariables()) { + stream << "\t" << nameVariablePair.second << std::endl; + } + for (auto const& nameVariablePair : module.getIntegerVariables()) { + stream << "\t" << nameVariablePair.second << std::endl; + } + for (auto const& command : module.getCommands()) { + stream << "\t" << command << std::endl; + } + stream << "endmodule" << std::endl; + return stream; } + } // namespace ir } // namespace storm diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index d9570c652..595a48c5c 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -1,149 +1,115 @@ -/* - * Module.h - * - * Created on: 04.01.2013 - * Author: Christian Dehnert - */ - -#ifndef STORM_IR_MODULE_H_ -#define STORM_IR_MODULE_H_ - -#include "utility/OsDetection.h" -#include - -#ifdef LINUX -#include -#endif -#include +#ifndef STORM_STORAGE_PRISM_MODULE_H_ +#define STORM_STORAGE_PRISM_MODULE_H_ #include #include #include #include +#include -#include "BooleanVariable.h" -#include "IntegerVariable.h" -#include "Command.h" -#include "expressions/VariableExpression.h" +#include "src/storage/prism/BooleanVariable.h" +#include "src/storage/prism/IntegerVariable.h" +#include "src/storage/prism/Command.h" +#include "src/storage/expressions/VariableExpression.h" namespace storm { - - namespace parser { - namespace prism { - class VariableState; - } // namespace prismparser - } // namespace parser - - namespace ir { - - /*! - * A class representing a module. - */ + namespace prism { 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 local (i.e. module-local) indices. - * @param integerVariableToLocalIndexMap A mapping of integer variables to local (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); + Module(std::string const& moduleName, std::map const& booleanVariables, + std::map const& integerVariables, + std::vector const& commands); /*! - * Special copy constructor, implementing the module renaming functionality. - * This will create a new module having all identifiers renamed according to the given map. + * 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); + Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming); + + // Create default implementations of constructors/assignment. + Module() = default; + Module(Module const& otherVariable) = default; + Module& operator=(Module const& otherVariable)= default; + Module(Module&& otherVariable) = default; + Module& operator=(Module&& otherVariable) = default; /*! * Retrieves the number of boolean variables in the module. * * @return the number of boolean variables in the module. */ - uint_fast64_t getNumberOfBooleanVariables() const; + std::size_t getNumberOfBooleanVariables() const; /*! - * Retrieves a reference to the boolean variable with the given index. + * Retrieves the number of integer variables in the module. * - * @return A reference to the boolean variable with the given index. + * @return The number of integer variables in the module. */ - storm::ir::BooleanVariable const& getBooleanVariable(uint_fast64_t index) const; + std::size_t getNumberOfIntegerVariables() const; /*! * Retrieves a reference to the boolean variable with the given name. * + * @param variableName The name of the boolean variable to retrieve. * @return A reference to the boolean variable with the given name. */ - storm::ir::BooleanVariable const& getBooleanVariable(std::string const& variableName) const; + storm::prism::BooleanVariable const& getBooleanVariable(std::string const& variableName) const; /*! - * Retrieves the number of integer variables in the module. + * Retrieves the boolean variables of the module. * - * @return The number of integer variables in the module. + * @return The boolean variables of the module. */ - uint_fast64_t getNumberOfIntegerVariables() const; + std::map const& getBooleanVariables() const; /*! - * Retrieves a reference to the integer variable with the given index. + * Retrieves a reference to the integer variable with the given name. * - * @return A reference to the integer variable with the given index. + * @param variableName The name of the integer variable to retrieve. + * @return A reference to the integer variable with the given name. */ - storm::ir::IntegerVariable const& getIntegerVariable(uint_fast64_t index) const; - + storm::prism::IntegerVariable const& getIntegerVariable(std::string const& variableName) const; + /*! - * Retrieves a reference to the boolean variable with the given name. + * Retrieves the integer variables of the module. * - * @return A reference to the boolean variable with the given name. + * @return The integer variables of the module. */ - storm::ir::IntegerVariable const& getIntegerVariable(std::string const& variableName) const; - + std::map const& getIntegerVariables() const; + /*! * Retrieves the number of commands of this module. * * @return the number of commands of this module. */ - uint_fast64_t getNumberOfCommands() const; + std::size_t getNumberOfCommands() const; /*! - * Retrieves the index of the boolean variable with the given name. + * Retrieves a reference to the command with the given index. * - * @param variableName The name of the boolean variable whose index to retrieve. - * @return The index of the boolean variable with the given name. + * @param index The index of the command to retrieve. + * @return A reference to the command with the given index. */ - uint_fast64_t getBooleanVariableIndex(std::string const& variableName) const; + storm::prism::Command const& getCommand(uint_fast64_t index) const; /*! - * Retrieves the index of the integer variable with the given name. + * Retrieves the commands of the module. * - * @param variableName The name of the integer variable whose index to retrieve. - * @return The index of the integer variable with the given name. + * @return The commands of the module. */ - 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; + std::vector const& getCommands() const; /*! * Retrieves the name of the module. @@ -152,13 +118,6 @@ namespace storm { */ 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. * @@ -170,7 +129,7 @@ namespace storm { * Retrieves whether or not this module contains a command labeled with the given action. * * @param action The action name to look for in this module. - * @return True if the module has at least one command labeled with the given action. + * @return True iff the module has at least one command labeled with the given action. */ bool hasAction(std::string const& action) const; @@ -180,15 +139,18 @@ namespace storm { * @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; + std::set const& getCommandIndicesByAction(std::string const& action) const; /*! - * Deletes all commands with indices not in the given set from the module. + * Creates a new module that drops all commands whose indices are not in the given set. * * @param indexSet The set of indices for which to keep the commands. + * @return The module resulting from erasing all commands whose indices are not in the given set. */ - void restrictCommands(boost::container::flat_set const& indexSet); + Module restrictCommands(boost::container::flat_set const& indexSet); + friend std::ostream& operator<<(std::ostream& stream, Module const& module); + private: /*! * Computes the locally maintained mappings for fast data retrieval. @@ -199,16 +161,10 @@ namespace storm { std::string moduleName; // A list of boolean variables. - std::vector booleanVariables; + std::map 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; + std::map integerVariables; // The commands associated with the module. std::vector commands; @@ -220,7 +176,7 @@ namespace storm { std::map> actionsToCommandIndexMap; }; - } // namespace ir + } // namespace prism } // namespace storm -#endif /* STORM_IR_MODULE_H_ */ +#endif /* STORM_STORAGE_PRISM_MODULE_H_ */ diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 169a3fe32..172d3f3b5 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -1,66 +1,44 @@ -/* - * Program.h - * - * Created on: 04.01.2013 - * Author: Christian Dehnert - */ - -#ifndef STORM_IR_PROGRAM_H_ -#define STORM_IR_PROGRAM_H_ +#ifndef STORM_STORAGE_PRISM_PROGRAM_H_ +#define STORM_STORAGE_PRISM_PROGRAM_H_ #include #include -#include #include #include #include "src/storage/expressions/Expression.h" -#include "Module.h" -#include "RewardModel.h" +#include "src/storage/prism/Module.h" +#include "src/storage/prism/RewardModel.h" namespace storm { - namespace ir { - - /*! - * A class representing a program. - */ + namespace prism { class Program { public: - /*! * An enum for the different model types. */ - enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP}; + enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA}; /*! - * Creates a program with the given model type, undefined constants, modules, rewards and labels. + * Creates a program with the given model type, undefined constants, global variables, modules, reward + * models, labels and initial states. * - * @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 globalBooleanVariables A list of global boolean variables. - * @param globalIntegerVariables A list of global integer variables. - * @param globalBooleanVariableToIndexMap A mapping from global boolean variable names to the index in the - * list of global boolean variables. - * @param globalIntegerVariableToIndexMap A mapping from global integer variable names to the index in the - * list of global integer variables. + * @param modelType The type of the program. + * @param undefinedBooleanConstants The undefined boolean constants of the program. + * @param undefinedIntegerConstants The undefined integer constants of the program. + * @param undefinedDoubleConstants The undefined double constants of the program. + * @param globalBooleanVariables The global boolean variables of the program. + * @param globalIntegerVariables The global integer variables of the program. * @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::set const& booleanUndefinedConstantExpressions, - std::set const& integerUndefinedConstantExpressions, - std::set const& doubleUndefinedConstantExpressions, - std::map const& globalBooleanVariables, - std::map const& globalIntegerVariables, - std::vector const& modules, - std::map const& rewards, - std::map> const& labels); + * @param hasInitialStatesExpression A flag indicating whether the program specifies its initial states via + * an explicit initial construct. + * @param initialStatesExpression If the model specifies an explicit initial construct, this expression + * defines its initial states. Otherwise it is irrelevant and may be set to an arbitrary (but valid) + * expression, e.g. false. + * @param rewardModels The reward models of the program. + * @param labels The labels defined for this program. + */ + Program(ModelType modelType, std::set const& undefinedBooleanConstants, std::set const& undefinedIntegerConstants, std::set const& undefinedDoubleConstants, std::map const& globalBooleanVariables, std::map const& globalIntegerVariables, std::vector const& modules, std::map const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map const& labels); // Provide default implementations for constructors and assignments. Program() = default; @@ -76,31 +54,82 @@ namespace storm { */ ModelType getModelType() const; + /*! + * Retrieves whether there are undefined constants of any type in the program. + * + * @return True iff there are undefined constants of any type in the program. + */ bool hasUndefinedConstants() const; + /*! + * Retrieves whether there are boolean undefined constants in the program. + * + * @return True iff there are boolean undefined constants in the program. + */ bool hasUndefinedBooleanConstants() const; + + /*! + * Retrieves whether there are integer undefined constants in the program. + * + * @return True iff there are integer undefined constants in the program. + */ bool hasUndefinedIntegerConstants() const; + + /*! + * Retrieves whether there are double undefined constants in the program. + * + * @return True iff there are double undefined constants in the program. + */ bool hasUndefinedDoubleConstants() const; + /*! + * Retrieves the undefined boolean constants of the program. + * + * @return The undefined boolean constants of the program. + */ std::set const& getUndefinedBooleanConstants() const; + + /*! + * Retrieves the undefined integer constants of the program. + * + * @return The undefined integer constants of the program. + */ std::set const& getUndefinedIntegerConstants() const; + + /*! + * Retrieves the undefined double constants of the program. + * + * @return The undefined double constants of the program. + */ std::set const& getUndefinedDoubleConstants() const; - std::map const& getGlobalBooleanVariables() const; + /*! + * Retrieves the global boolean variables of the program. + * + * @return The global boolean variables of the program. + */ + std::map const& getGlobalBooleanVariables() const; /*! - * Retrieves a reference to the global boolean variable with the given index. + * Retrieves a the global boolean variable with the given name. * - * @return A reference to the global boolean variable with the given index. + * @param variableName The name of the global boolean variable to retrieve. + * @return The global boolean variable with the given name. */ storm::ir::BooleanVariable const& getGlobalBooleanVariable(std::string const& variableName) const; - std::map const& getGlobalIntegerVariables() const; + /*! + * Retrieves the global integer variables of the program. + * + * @return The global integer variables of the program. + */ + std::map const& getGlobalIntegerVariables() const; /*! - * Retrieves a reference to the global integer variable with the given index. + * Retrieves a the global integer variable with the given name. * - * @return A reference to the global integer variable with the given index. + * @param variableName The name of the global integer variable to retrieve. + * @return The global integer variable with the given name. */ storm::ir::IntegerVariable const& getGlobalIntegerVariable(std::string const& variableName) const; @@ -109,29 +138,29 @@ namespace storm { * * @return The number of global boolean variables of the program. */ - uint_fast64_t getNumberOfGlobalBooleanVariables() const; + std::size_t getNumberOfGlobalBooleanVariables() const; /*! * Retrieves the number of global integer variables of the program. * * @return The number of global integer variables of the program. */ - uint_fast64_t getNumberOfGlobalIntegerVariables() const; + std::size_t getNumberOfGlobalIntegerVariables() const; /*! * Retrieves the number of modules in the program. * * @return The number of modules in the program. */ - uint_fast64_t getNumberOfModules() const; + std::size_t getNumberOfModules() const; /*! - * Retrieves a reference to the module with the given index. + * Retrieves 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; + storm::prism::Module const& getModule(uint_fast64_t index) const; /*! * Retrieves the set of actions present in the program. @@ -141,8 +170,8 @@ namespace storm { std::set const& getActions() const; /*! - * Retrieves the indices of all modules within this program that contain commands that are labelled with the given - * action. + * 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. @@ -157,15 +186,20 @@ namespace storm { */ uint_fast64_t getModuleIndexByVariable(std::string const& variableName) const; - std::map const& getRewardModels() const; + /*! + * Retrieves the reward models of the program. + * + * @return The reward models of the program. + */ + std::map const& getRewardModels() const; /*! * Retrieves the reward model with the given name. * - * @param name The name of the reward model to return. + * @param rewardModelName 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; + storm::prism::RewardModel const& getRewardModel(std::string const& rewardModelName) const; /*! * Retrieves all labels that are defined by the probabilitic program. @@ -200,16 +234,23 @@ namespace storm { std::map globalBooleanVariables; // A list of global integer variables. - std::std::string, IntegerVariable> globalIntegerVariables; + std::map globalIntegerVariables; // The modules associated with the program. - std::vector modules; + std::vector modules; // The reward models associated with the program. - std::map rewardModels; + std::map rewardModels; + + // A flag that indicates whether the initial states of the program were given explicitly (in the form of an + // initial construct) or implicitly (attached to the variable declarations). + bool hasInitialStatesExpression; + + // The expression contained in the initial construct (if any). + storm::expressions::Expression initialStatesExpression; // The labels that are defined for this model. - std::map labels; + std::map labels; // The set of actions present in this program. std::set actions; @@ -221,7 +262,7 @@ namespace storm { std::map variableToModuleIndexMap; }; - } // namespace ir + } // namespace prism } // namespace storm -#endif /* STORM_IR_PROGRAM_H_ */ +#endif /* STORM_STORAGE_PRISM_PROGRAM_H_ */ diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp index 9d6a79ed3..006ee1054 100644 --- a/src/storage/prism/RewardModel.cpp +++ b/src/storage/prism/RewardModel.cpp @@ -1,43 +1,20 @@ -/* - * RewardModel.cpp - * - * Created on: 12.01.2013 - * Author: Christian Dehnert - */ - -#include - -#include "RewardModel.h" +#include "src/storage/prism/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) { + namespace prism { + 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(); + std::string const& RewardModel::getName() const { + return this->rewardModelName; } bool RewardModel::hasStateRewards() const { return this->stateRewards.size() > 0; } - std::vector const& RewardModel::getStateRewards() const { + std::vector const& RewardModel::getStateRewards() const { return this->stateRewards; } @@ -45,9 +22,21 @@ namespace storm { return this->transitionRewards.size() > 0; } - std::vector const& RewardModel::getTransitionRewards() const { + std::vector const& RewardModel::getTransitionRewards() const { return this->transitionRewards; } - } // namespace ir + std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel) { + stream << "rewards \"" << rewardModel.getName() << "\"" << std::endl; + for (auto const& reward : rewardModel.getStateRewards()) { + stream << reward << std::endl; + } + for (auto const& reward : rewardModel.getTransitionRewards()) { + stream << reward << std::endl; + } + stream << "endrewards" << std::endl; + return stream; + } + + } // namespace prism } // namespace storm diff --git a/src/storage/prism/RewardModel.h b/src/storage/prism/RewardModel.h index 827248810..6c172c744 100644 --- a/src/storage/prism/RewardModel.h +++ b/src/storage/prism/RewardModel.h @@ -1,88 +1,81 @@ -/* - * RewardModel.h - * - * Created on: 04.01.2013 - * Author: Christian Dehnert - */ - -#ifndef STORM_IR_REWARDMODEL_H_ -#define STORM_IR_REWARDMODEL_H_ +#ifndef STORM_STORAGE_PRISM_REWARDMODEL_H_ +#define STORM_STORAGE_PRISM_REWARDMODEL_H_ #include #include -#include "StateReward.h" -#include "TransitionReward.h" +#include "src/storage/prism/StateReward.h" +#include "src/storage/prism/TransitionReward.h" namespace storm { - namespace ir { - - /*! - * A class representing a reward model. - */ + namespace prism { class RewardModel { public: /*! - * Default constructor. Creates an empty reward model. - */ - RewardModel(); - - /*! - * Creates a reward module with the given name, state and transition rewards. + * Creates a reward model 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); + RewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards); + + // Create default implementations of constructors/assignment. + RewardModel() = default; + RewardModel(RewardModel const& otherVariable) = default; + RewardModel& operator=(RewardModel const& otherVariable)= default; + RewardModel(RewardModel&& otherVariable) = default; + RewardModel& operator=(RewardModel&& otherVariable) = default; /*! - * Retrieves a string representation of this reward model. + * Retrieves the name of the reward model. * - * @return a string representation of this reward model. + * @return The name of the reward model. */ - std::string toString() const; + std::string const& getName() const; /*! - * Check, if there are any state rewards. + * Retrieves whether there are any state rewards. * - * @return True, iff 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. + * Retrieves all state rewards associated with this reward model. * - * @return A vector containing the state rewards associated with this reward model. + * @return The state rewards associated with this reward model. */ - std::vector const& getStateRewards() const; + std::vector const& getStateRewards() const; /*! - * Check, if there are any transition rewards. + * Retrieves whether there are any transition rewards. * - * @return True, iff there are any transition rewards associated with this reward model. + * @return True iff there are any transition rewards. */ bool hasTransitionRewards() const; /*! - * Retrieves a vector of transition rewards associated with this reward model. + * Retrieves all transition rewards associated with this reward model. * - * @return A vector of transition rewards associated with this reward model. + * @return The transition rewards associated with this reward model. */ - std::vector const& getTransitionRewards() const; + std::vector const& getTransitionRewards() const; + friend std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel); + private: // The name of the reward model. std::string rewardModelName; // The state-based rewards associated with this reward model. - std::vector stateRewards; + std::vector stateRewards; // The transition-based rewards associated with this reward model. - std::vector transitionRewards; + std::vector transitionRewards; }; - } // namespace ir + } // namespace prism } // namespace storm -#endif /* STORM_IR_REWARDMODEL_H_ */ +#endif /* STORM_STORAGE_PRISM_REWARDMODEL_H_ */ diff --git a/src/storage/prism/StateReward.cpp b/src/storage/prism/StateReward.cpp index 50457cabc..c4bcbd428 100644 --- a/src/storage/prism/StateReward.cpp +++ b/src/storage/prism/StateReward.cpp @@ -1,38 +1,22 @@ -/* - * StateReward.cpp - * - * Created on: 12.01.2013 - * Author: Christian Dehnert - */ - -#include - -#include "StateReward.h" +#include "src/storage/prism/StateReward.h" namespace storm { - namespace ir { - - StateReward::StateReward() : statePredicate(), rewardValue() { + namespace prism { + StateReward::StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression) : statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) { // Nothing to do here. } - StateReward::StateReward(storm::expressions::Expression const& statePredicate, storm::expressions::Expression const& rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) { - // Nothing to do here. + storm::expressions::Expression const& StateReward::getStatePredicateExpression() const { + return this->statePredicateExpression; } - std::string StateReward::toString() const { - std::stringstream result; - result << "\t" << statePredicate << ": " << rewardValue << ";"; - return result.str(); + storm::expressions::Expression const& StateReward::getRewardValueExpression() const { + return this->rewardValueExpression; } - storm::expressions::Expression const& StateReward::getStatePredicate() const { - return this->statePredicate; + std::ostream& operator<<(std::ostream& stream, StateReward const& stateReward) { + stream << "\t" << stateReward.getStatePredicateExpression() << ": " << stateReward.getRewardValueExpression() << ";"; + return stream; } - - storm::expressions::Expression const& StateReward::getRewardValue() const { - return this->rewardValue; - } - - } // namespace ir + } // namespace prism } // namespace storm diff --git a/src/storage/prism/StateReward.h b/src/storage/prism/StateReward.h index d8c09f4e2..bdd08d446 100644 --- a/src/storage/prism/StateReward.h +++ b/src/storage/prism/StateReward.h @@ -1,85 +1,53 @@ -/* - * StateReward.h - * - * Created on: Jan 10, 2013 - * Author: Christian Dehnert - */ - -#ifndef STORM_IR_STATEREWARD_H_ -#define STORM_IR_STATEREWARD_H_ - -#include +#ifndef STORM_STORAGE_PRISM_STATEREWARD_H_ +#define STORM_STORAGE_PRISM_STATEREWARD_H_ #include "src/storage/expressions/Expression.h" namespace storm { - namespace ir { - - /*! - * A class representing a state reward. - */ + namespace prism { class StateReward { public: /*! - * Default constructor. Creates an empty state reward. - */ - StateReward(); - - /*! - * 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 - * satisfy. - * @param rewardValue An expression specifying the values of the rewards to attach to the - * states. - */ - StateReward(storm::expressions::Expression const& statePredicate, storm::expressions::Expression const& rewardValue); - - /*! - * Performs a deep-copy of the given reward. - * - * @param otherReward The reward to copy. - */ - StateReward(StateReward const& otherReward) = default; - - /*! - * Performs a deep-copy of the given reward and assigns it to the current one. + * Creates a state reward for the states satisfying the given expression with the value given by a second + * expression. * - * @param otherReward The reward to assign. + * @param statePredicateExpression The predicate that states earning this state-based reward need to satisfy. + * @param rewardValueExpression An expression specifying the values of the rewards to attach to the states. */ - StateReward& operator=(StateReward const& otherReward) = default; + StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression); - /*! - * Retrieves a string representation of this state reward. - * - * @return A string representation of this state reward. - */ - std::string toString() const; + // Create default implementations of constructors/assignment. + StateReward() = default; + StateReward(StateReward const& otherVariable) = default; + StateReward& operator=(StateReward const& otherVariable)= default; + StateReward(StateReward&& otherVariable) = default; + StateReward& operator=(StateReward&& otherVariable) = default; /*! * Retrieves the state predicate that is associated with this state reward. * * @return The state predicate that is associated with this state reward. */ - storm::expressions::Expression const& getStatePredicate() const; + storm::expressions::Expression const& getStatePredicateExpression() const; /*! * Retrieves the reward value associated with this state reward. * * @return The reward value associated with this state reward. */ - storm::expressions::Expression const& getRewardValue() const; + storm::expressions::Expression const& getRewardValueExpression() const; + friend std::ostream& operator<<(std::ostream& stream, StateReward const& stateReward); + private: // The predicate that characterizes the states that obtain this reward. - storm::expressions::Expression statePredicate; + storm::expressions::Expression statePredicateExpression; // The expression that specifies the value of the reward obtained. - storm::expressions::Expression rewardValue; + storm::expressions::Expression rewardValueExpression; }; - } // namespace ir + } // namespace prism } // namespace storm -#endif /* STORM_IR_STATEREWARD_H_ */ +#endif /* STORM_STORAGE_PRISM_STATEREWARD_H_ */ diff --git a/src/storage/prism/TransitionReward.cpp b/src/storage/prism/TransitionReward.cpp index 93d951731..f972f1270 100644 --- a/src/storage/prism/TransitionReward.cpp +++ b/src/storage/prism/TransitionReward.cpp @@ -1,42 +1,27 @@ -/* - * TransitionReward.cpp - * - * Created on: 12.01.2013 - * Author: Christian Dehnert - */ - -#include - -#include "TransitionReward.h" +#include "src/storage/prism/TransitionReward.h" namespace storm { - namespace ir { - - TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardValue() { - // Nothing to do here. - } - - TransitionReward::TransitionReward(std::string const& commandName, storm::expressions::Expression const& statePredicate, storm::expressions::Expression const& rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) { + namespace prism { + TransitionReward::TransitionReward(std::string const& commandName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression) : commandName(commandName), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) { // Nothing to do here. } - std::string TransitionReward::toString() const { - std::stringstream result; - result << "\t[" << commandName << "] " << statePredicate << ": " << rewardValue << ";"; - return result.str(); - } - std::string const& TransitionReward::getActionName() const { return this->commandName; } - storm::expressions::Expression const& TransitionReward::getStatePredicate() const { - return this->statePredicate; + storm::expressions::Expression const& TransitionReward::getStatePredicateExpression() const { + return this->statePredicateExpression; + } + + storm::expressions::Expression const& TransitionReward::getRewardValueExpression() const { + return this->rewardValueExpression; } - storm::expressions::Expression const& TransitionReward::getRewardValue() const { - return this->rewardValue; + std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward) { + stream << "\t[" << transitionReward.getActionName() << "] " << transitionReward.getStatePredicateExpression() << ": " << transitionReward.getRewardValueExpression() << ";"; + return stream; } - } // namespace ir + } // namespace prism } // namespace storm diff --git a/src/storage/prism/TransitionReward.h b/src/storage/prism/TransitionReward.h index b21eeb12f..1fb783101 100644 --- a/src/storage/prism/TransitionReward.h +++ b/src/storage/prism/TransitionReward.h @@ -1,99 +1,66 @@ -/* - * TransitionReward.h - * - * Created on: Jan 10, 2013 - * Author: Christian Dehnert - */ - -#ifndef STORM_IR_TRANSITIONREWARD_H_ -#define STORM_IR_TRANSITIONREWARD_H_ - -#include +#ifndef STORM_STORAGE_PRISM_TRANSITIONREWARD_H_ +#define STORM_STORAGE_PRISM_TRANSITIONREWARD_H_ #include "src/storage/expressions/Expression.h" namespace storm { + namespace prism { + class TransitionReward { + 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 actionName The name of the command that obtains this reward. + * @param statePredicateExpression The predicate that needs to hold before taking a transition with the previously + * specified name in order to obtain the reward. + * @param rewardValueExpression An expression specifying the values of the rewards to attach to the transitions. + */ + TransitionReward(std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression); + + // Create default implementations of constructors/assignment. + TransitionReward() = default; + TransitionReward(TransitionReward const& otherVariable) = default; + TransitionReward& operator=(TransitionReward const& otherVariable)= default; + TransitionReward(TransitionReward&& otherVariable) = default; + TransitionReward& operator=(TransitionReward&& otherVariable) = default; + + /*! + * 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 expression that is associated with this state reward. + * + * @return The state predicate expression that is associated with this state reward. + */ + storm::expressions::Expression const& getStatePredicateExpression() const; + + /*! + * Retrieves the reward value expression associated with this state reward. + * + * @return The reward value expression associated with this state reward. + */ + storm::expressions::Expression const& getRewardValueExpression() const; + + friend std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward); -namespace ir { - -/*! - * A class representing a transition reward. - */ -class TransitionReward { -public: - /*! - * Default constructor. Creates an empty transition reward. - */ - TransitionReward(); - - /*! - * 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 - * previously specified name in order to obtain the reward. - * @param rewardValue An expression specifying the values of the rewards to attach to the - * transitions. - */ - TransitionReward(std::string const& commandName, storm::expressions::Expression const& statePredicate, storm::expressions::Expression const& rewardValue); - - /*! - * Performs a deep-copy of the given transition reward. - * - * @param otherReward The transition reward to copy. - */ - TransitionReward(TransitionReward const& otherReward) = default; - - /*! - * Performs a deep-copy of the given transition reward and assigns it to the current one. - * - * @param otherReward The reward to assign. - */ - TransitionReward& operator=(TransitionReward const& otherReward) = default; - - /*! - * Retrieves a string representation of this transition reward. - * - * @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. - */ - storm::expressions::Expression const& getStatePredicate() const; - - /*! - * Retrieves the reward value associated with this state reward. - * - * @return The reward value associated with this state reward. - */ - storm::expressions::Expression const& getRewardValue() const; - -private: - // The name of the command this transition-based reward is attached to. - std::string commandName; - - // A predicate that needs to be satisfied by states for the reward to be obtained (by taking - // a corresponding command transition). - storm::expressions::Expression statePredicate; - - // The expression specifying the value of the reward obtained along the transitions. - storm::expressions::Expression rewardValue; -}; - -} // namespace ir - + private: + // The name of the command this transition-based reward is attached to. + std::string commandName; + + // A predicate that needs to be satisfied by states for the reward to be obtained (by taking + // a corresponding command transition). + storm::expressions::Expression statePredicateExpression; + + // The expression specifying the value of the reward obtained along the transitions. + storm::expressions::Expression rewardValueExpression; + }; + + } // namespace prism } // namespace storm -#endif /* STORM_IR_TRANSITIONREWARD_H_ */ +#endif /* STORM_STORAGE_PRISM_TRANSITIONREWARD_H_ */