sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

PRISM classes almost adapted to new expression classes. TODO: source file of PRISM program. 

Former-commit-id: 929a78684d
main
dehnert 11 years ago
parent
5407978e8e
commit
d88876d0cd
9 changed files with 387 additions and 567 deletions
Unified View
  1. 187
      src/storage/prism/Module.cpp
  2. 154
      src/storage/prism/Module.h
  3. 175
      src/storage/prism/Program.h
  4. 51
      src/storage/prism/RewardModel.cpp
  5. 73
      src/storage/prism/RewardModel.h
  6. 38
      src/storage/prism/StateReward.cpp
  7. 76
      src/storage/prism/StateReward.h
  8. 41
      src/storage/prism/TransitionReward.cpp
  9. 89
      src/storage/prism/TransitionReward.h

187
src/storage/prism/Module.cpp
View File

@ -1,177 +1,100 @@
/* #include "src/storage/prism/Module.h"
* Module.cpp #include "src/exceptions/ExceptionMacros.h"
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include <sstream>
#include <iostream>
#include "utility/OsDetection.h"
#include "Module.h"
#include "src/parser/prismparser/VariableState.h"
#include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/OutOfRangeException.h"
#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidArgumentException.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm { namespace storm {
namespace ir { namespace prism {
Module::Module(std::string const& moduleName, std::map<std::string, storm::prism::BooleanVariable> const& booleanVariables, std::map<std::string, storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands) : moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands), actions(), actionsToCommandIndexMap() {
Module::Module() : moduleName(), booleanVariables(), integerVariables(), booleanVariableToLocalIndexMap(),
integerVariableToLocalIndexMap(), commands(), actions(), actionsToCommandIndexMap() {
// Nothing to do here.
}
Module::Module(std::string const& moduleName,
std::vector<storm::ir::BooleanVariable> const& booleanVariables,
std::vector<storm::ir::IntegerVariable> const& integerVariables,
std::map<std::string, uint_fast64_t> const& booleanVariableToLocalIndexMap,
std::map<std::string, uint_fast64_t> const& integerVariableToLocalIndexMap,
std::vector<storm::ir::Command> const& commands)
: moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables),
booleanVariableToLocalIndexMap(booleanVariableToLocalIndexMap),
integerVariableToLocalIndexMap(integerVariableToLocalIndexMap), commands(commands), actions(), actionsToCommandIndexMap() {
// Initialize the internal mappings for fast information retrieval. // Initialize the internal mappings for fast information retrieval.
this->collectActions(); this->collectActions();
} }
Module::Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState) Module::Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming) : moduleName(newModuleName), booleanVariables(), integerVariables(), commands(), actions(), actionsToCommandIndexMap() {
: moduleName(newModuleName), booleanVariableToLocalIndexMap(oldModule.booleanVariableToLocalIndexMap), integerVariableToLocalIndexMap(oldModule.integerVariableToLocalIndexMap) { // Iterate over boolean variables and rename them. If a variable was not renamed, this is an error and an exception is thrown.
LOG4CPLUS_TRACE(logger, "Start renaming " << oldModule.getName() << " to " << moduleName << "."); for (auto const& nameVariablePair : oldModule.getBooleanVariables()) {
auto renamingPair = renaming.find(nameVariablePair.first);
// Iterate over boolean variables and rename them. If a variable was not renamed, this is an error and an exception LOG_THROW(renamingPair == renaming.end(), storm::exceptions::InvalidArgumentException, "Boolean variable " << moduleName << "." << nameVariablePair.first << " was not renamed.");
// is thrown. this->booleanVariables.emplace(nameVariablePair.first, BooleanVariable(nameVariablePair.second, renamingPair->second, renaming));
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);
}
} }
// Now do the same for the integer variables. // Now do the same for the integer variables.
this->integerVariables.reserve(oldModule.getNumberOfIntegerVariables()); for (auto const& nameVariablePair : oldModule.getIntegerVariables()) {
for (IntegerVariable const& integerVariable : oldModule.integerVariables) { auto renamingPair = renaming.find(nameVariablePair.first);
auto renamingPair = renaming.find(integerVariable.getName()); LOG_THROW(renamingPair == renaming.end(), storm::exceptions::InvalidArgumentException, "Integer variable " << moduleName << "." << nameVariablePair.first << " was not renamed.");
if (renamingPair == renaming.end()) { this->integerVariables.emplace(nameVariablePair.first, IntegerVariable(nameVariablePair.second, renamingPair->second, renaming));
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);
}
} }
// Now we are ready to clone all commands and rename them if requested. // Now we are ready to clone all commands and rename them if requested.
this->commands.reserve(oldModule.getNumberOfCommands()); this->commands.reserve(oldModule.getNumberOfCommands());
for (Command const& command : oldModule.commands) { for (Command const& command : oldModule.getCommands()) {
this->commands.emplace_back(command, variableState.getNextGlobalCommandIndex(), renaming, variableState); this->commands.emplace_back(command, command.getGlobalIndex(), renaming);
variableState.nextGlobalCommandIndex++;
} }
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(); return this->booleanVariables.size();
} }
storm::ir::BooleanVariable const& Module::getBooleanVariable(uint_fast64_t index) const { std::size_t Module::getNumberOfIntegerVariables() const {
return this->booleanVariables[index]; return this->integerVariables.size();
} }
storm::ir::BooleanVariable const& Module::getBooleanVariable(std::string const& variableName) const { storm::prism::BooleanVariable const& Module::getBooleanVariable(std::string const& variableName) const {
uint_fast64_t index = this->getBooleanVariableIndex(variableName); auto const& nameVariablePair = this->getBooleanVariables().find(variableName);
return this->booleanVariables[index]; LOG_THROW(nameVariablePair == this->getBooleanVariables().end(), storm::exceptions::InvalidArgumentException, "Unknown boolean variable '" << variableName << "'.");
return nameVariablePair->second;
} }
uint_fast64_t Module::getNumberOfIntegerVariables() const { std::map<std::string, storm::prism::BooleanVariable> const& Module::getBooleanVariables() const {
return this->integerVariables.size(); return this->booleanVariables;
} }
storm::ir::IntegerVariable const& Module::getIntegerVariable(uint_fast64_t index) const { storm::prism::IntegerVariable const& Module::getIntegerVariable(std::string const& variableName) const {
return this->integerVariables[index]; 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 { std::map<std::string, storm::prism::IntegerVariable> const& Module::getIntegerVariables() const {
uint_fast64_t index = this->getIntegerVariableIndex(variableName); return this->integerVariables;
return this->integerVariables[index];
} }
uint_fast64_t Module::getNumberOfCommands() const { std::size_t Module::getNumberOfCommands() const {
return this->commands.size(); return this->commands.size();
} }
uint_fast64_t Module::getBooleanVariableIndex(std::string const& variableName) const { storm::prism::Command const& Module::getCommand(uint_fast64_t index) const {
auto it = booleanVariableToLocalIndexMap.find(variableName); return this->commands[index];
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 { std::vector<storm::prism::Command> const& Module::getCommands() const {
return this->commands[index]; return this->commands;
} }
std::string const& Module::getName() const { std::string const& Module::getName() const {
return this->moduleName; 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<std::string> const& Module::getActions() const { std::set<std::string> const& Module::getActions() const {
return this->actions; return this->actions;
} }
bool Module::hasAction(std::string const& action) const { bool Module::hasAction(std::string const& action) const {
auto const& actionEntry = this->actions.find(action); auto const& actionEntry = this->actions.find(action);
if (actionEntry != this->actions.end()) { return actionEntry != this->actions.end();
return true;
}
return false;
} }
std::set<uint_fast64_t> const& Module::getCommandsByAction(std::string const& action) const { std::set<uint_fast64_t> const& Module::getCommandIndicesByAction(std::string const& action) const {
auto actionsCommandSetPair = this->actionsToCommandIndexMap.find(action); auto actionsCommandSetPair = this->actionsToCommandIndexMap.find(action);
if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) { if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) {
return actionsCommandSetPair->second; return actionsCommandSetPair->second;
} }
LOG4CPLUS_ERROR(logger, "Action name '" << action << "' does not exist in module."); LOG_THROW(false, storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist in module.");
throw storm::exceptions::OutOfRangeException() << "Action name '" << action << "' does not exist in module.";
} }
void Module::collectActions() { void Module::collectActions() {
@ -199,19 +122,33 @@ namespace storm {
} }
} }
void Module::restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) { Module Module::restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) {
// First construct the new vector of commands. // First construct the new vector of commands.
std::vector<storm::ir::Command> newCommands; std::vector<storm::prism::Command> newCommands;
for (auto const& command : commands) { for (auto const& command : commands) {
if (indexSet.find(command.getGlobalIndex()) != indexSet.end()) { 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. return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands);
this->collectActions(); }
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 ir
} // namespace storm } // namespace storm

154
src/storage/prism/Module.h
View File

@ -1,149 +1,115 @@
/* #ifndef STORM_STORAGE_PRISM_MODULE_H_
* Module.h #define STORM_STORAGE_PRISM_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 <boost/container/flat_set.hpp>
#ifdef LINUX
#include <boost/container/map.hpp>
#endif
#include <map>
#include <set> #include <set>
#include <string> #include <string>
#include <vector> #include <vector>
#include <memory> #include <memory>
#include <boost/container/flat_set.hpp>
#include "BooleanVariable.h" #include "src/storage/prism/BooleanVariable.h"
#include "IntegerVariable.h" #include "src/storage/prism/IntegerVariable.h"
#include "Command.h" #include "src/storage/prism/Command.h"
#include "expressions/VariableExpression.h" #include "src/storage/expressions/VariableExpression.h"
namespace storm { namespace storm {
namespace parser {
namespace prism { namespace prism {
class VariableState;
} // namespace prismparser
} // namespace parser
namespace ir {
/*!
* A class representing a module.
*/
class Module { class Module {
public: public:
/*!
* Default constructor. Creates an empty module.
*/
Module();
/*! /*!
* Creates a module with the given name, variables and commands. * Creates a module with the given name, variables and commands.
* *
* @param moduleName The name of the module. * @param moduleName The name of the module.
* @param booleanVariables The boolean variables defined by the module. * @param booleanVariables The boolean variables defined by the module.
* @param integerVariables The integer 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. * @param commands The commands of the module.
*/ */
Module(std::string const& moduleName, std::vector<storm::ir::BooleanVariable> const& booleanVariables, Module(std::string const& moduleName, std::map<std::string, storm::prism::BooleanVariable> const& booleanVariables,
std::vector<storm::ir::IntegerVariable> const& integerVariables, std::map<std::string, storm::prism::IntegerVariable> const& integerVariables,
std::map<std::string, uint_fast64_t> const& booleanVariableToLocalIndexMap, std::vector<storm::prism::Command> const& commands);
std::map<std::string, uint_fast64_t> const& integerVariableToLocalIndexMap,
std::vector<storm::ir::Command> const& commands);
/*! /*!
* Special copy constructor, implementing the module renaming functionality. * Special copy constructor, implementing the module renaming functionality. This will create a new module
* This will create a new module having all identifiers renamed according to the given map. * having all identifiers renamed according to the given map.
* *
* @param oldModule The module to be copied. * @param oldModule The module to be copied.
* @param newModuleName The name of the new module. * @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 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<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState); Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> 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. * Retrieves the number of boolean variables in the module.
* *
* @return 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. * 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. * @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<std::string, storm::prism::BooleanVariable> 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<std::string, storm::prism::IntegerVariable> const& getIntegerVariables() const;
/*! /*!
* Retrieves the number of commands of this module. * Retrieves the number of commands of this module.
* *
* @return 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.
*/
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. * @param index The index of the command to retrieve.
* @return The index of the integer variable with the given name. * @return A reference to the command with the given index.
*/ */
uint_fast64_t getIntegerVariableIndex(std::string const& variableName) const; storm::prism::Command const& getCommand(uint_fast64_t index) const;
/*! /*!
* Retrieves a reference to the command with the given index. * Retrieves the commands of the module.
* *
* @return A reference to the command with the given index. * @return The commands of the module.
*/ */
storm::ir::Command const& getCommand(uint_fast64_t index) const; std::vector<storm::prism::Command> const& getCommands() const;
/*! /*!
* Retrieves the name of the module. * Retrieves the name of the module.
@ -152,13 +118,6 @@ namespace storm {
*/ */
std::string const& getName() const; 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. * 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. * 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. * @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; bool hasAction(std::string const& action) const;
@ -180,14 +139,17 @@ namespace storm {
* @param action The action with which the commands have to be labelled. * @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. * @return A set of indices of commands that are labelled with the given action.
*/ */
std::set<uint_fast64_t> const& getCommandsByAction(std::string const& action) const; std::set<uint_fast64_t> 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. * @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<uint_fast64_t> const& indexSet); Module restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet);
friend std::ostream& operator<<(std::ostream& stream, Module const& module);
private: private:
/*! /*!
@ -199,16 +161,10 @@ namespace storm {
std::string moduleName; std::string moduleName;
// A list of boolean variables. // A list of boolean variables.
std::vector<storm::ir::BooleanVariable> booleanVariables; std::map<std::string, storm::prism::BooleanVariable> booleanVariables;
// A list of integer variables. // A list of integer variables.
std::vector<storm::ir::IntegerVariable> integerVariables; std::map<std::string, storm::prism::IntegerVariable> integerVariables;
// A map of boolean variable names to their index.
std::map<std::string, uint_fast64_t> booleanVariableToLocalIndexMap;
// A map of integer variable names to their index.
std::map<std::string, uint_fast64_t> integerVariableToLocalIndexMap;
// The commands associated with the module. // The commands associated with the module.
std::vector<storm::ir::Command> commands; std::vector<storm::ir::Command> commands;
@ -220,7 +176,7 @@ namespace storm {
std::map<std::string, std::set<uint_fast64_t>> actionsToCommandIndexMap; std::map<std::string, std::set<uint_fast64_t>> actionsToCommandIndexMap;
}; };
} // namespace ir } // namespace prism
} // namespace storm } // namespace storm
#endif /* STORM_IR_MODULE_H_ */ #endif /* STORM_STORAGE_PRISM_MODULE_H_ */

175
src/storage/prism/Program.h
View File

@ -1,66 +1,44 @@
/* #ifndef STORM_STORAGE_PRISM_PROGRAM_H_
* Program.h #define STORM_STORAGE_PRISM_PROGRAM_H_
*
* Created on: 04.01.2013
* Author: Christian Dehnert
*/
#ifndef STORM_IR_PROGRAM_H_
#define STORM_IR_PROGRAM_H_
#include <map> #include <map>
#include <vector> #include <vector>
#include <memory>
#include <set> #include <set>
#include <boost/container/flat_set.hpp> #include <boost/container/flat_set.hpp>
#include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expression.h"
#include "Module.h" #include "src/storage/prism/Module.h"
#include "RewardModel.h" #include "src/storage/prism/RewardModel.h"
namespace storm { namespace storm {
namespace ir { namespace prism {
/*!
* A class representing a program.
*/
class Program { class Program {
public: public:
/*! /*!
* An enum for the different model types. * 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 modelType The type of the program.
* @param booleanUndefinedConstantExpressions A map of undefined boolean constants to their * @param undefinedBooleanConstants The undefined boolean constants of the program.
* expression nodes. * @param undefinedIntegerConstants The undefined integer constants of the program.
* @param integerUndefinedConstantExpressions A map of undefined integer constants to their * @param undefinedDoubleConstants The undefined double constants of the program.
* expression nodes. * @param globalBooleanVariables The global boolean variables of the program.
* @param doubleUndefinedConstantExpressions A map of undefined double constants to their * @param globalIntegerVariables The global integer variables of the program.
* 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 modules The modules of the program. * @param modules The modules of the program.
* @param rewards The reward models of the program. * @param hasInitialStatesExpression A flag indicating whether the program specifies its initial states via
* @param labels The labels defined for this model. * an explicit initial construct.
*/ * @param initialStatesExpression If the model specifies an explicit initial construct, this expression
Program(ModelType modelType, * defines its initial states. Otherwise it is irrelevant and may be set to an arbitrary (but valid)
std::set<std::string> const& booleanUndefinedConstantExpressions, * expression, e.g. false.
std::set<std::string> const& integerUndefinedConstantExpressions, * @param rewardModels The reward models of the program.
std::set<std::string> const& doubleUndefinedConstantExpressions, * @param labels The labels defined for this program.
std::map<std::string, BooleanVariable> const& globalBooleanVariables, */
std::map<std::string, IntegerVariable> const& globalIntegerVariables, Program(ModelType modelType, std::set<std::string> const& undefinedBooleanConstants, std::set<std::string> const& undefinedIntegerConstants, std::set<std::string> const& undefinedDoubleConstants, std::map<std::string, BooleanVariable> const& globalBooleanVariables, std::map<std::string, IntegerVariable> const& globalIntegerVariables, std::vector<storm::prism::Module> const& modules, std::map<std::string, storm::prism::RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map<std::string, storm::expressions::Expression> const& labels);
std::vector<storm::ir::Module> const& modules,
std::map<std::string, storm::ir::RewardModel> const& rewards,
std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& labels);
// Provide default implementations for constructors and assignments. // Provide default implementations for constructors and assignments.
Program() = default; Program() = default;
@ -76,31 +54,82 @@ namespace storm {
*/ */
ModelType getModelType() const; 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; 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; 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; 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; bool hasUndefinedDoubleConstants() const;
/*!
* Retrieves the undefined boolean constants of the program.
*
* @return The undefined boolean constants of the program.
*/
std::set<std::string> const& getUndefinedBooleanConstants() const; std::set<std::string> const& getUndefinedBooleanConstants() const;
/*!
* Retrieves the undefined integer constants of the program.
*
* @return The undefined integer constants of the program.
*/
std::set<std::string> const& getUndefinedIntegerConstants() const; std::set<std::string> const& getUndefinedIntegerConstants() const;
/*!
* Retrieves the undefined double constants of the program.
*
* @return The undefined double constants of the program.
*/
std::set<std::string> const& getUndefinedDoubleConstants() const; std::set<std::string> const& getUndefinedDoubleConstants() const;
std::map<std::string, storm::ir::BooleanVariable> const& getGlobalBooleanVariables() const; /*!
* Retrieves the global boolean variables of the program.
*
* @return The global boolean variables of the program.
*/
std::map<std::string, storm::prism::BooleanVariable> 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; storm::ir::BooleanVariable const& getGlobalBooleanVariable(std::string const& variableName) const;
std::map<std::string, storm::ir::IntegerVariable> const& getGlobalIntegerVariables() const; /*!
* Retrieves the global integer variables of the program.
*
* @return The global integer variables of the program.
*/
std::map<std::string, storm::prism::IntegerVariable> 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; 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. * @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. * Retrieves the number of global integer variables of the program.
* *
* @return 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. * Retrieves the number of modules in the program.
* *
* @return 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. * @param index The index of the module to retrieve.
* @return The module with the given index. * @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. * Retrieves the set of actions present in the program.
@ -141,8 +170,8 @@ namespace storm {
std::set<std::string> const& getActions() const; std::set<std::string> const& getActions() const;
/*! /*!
* Retrieves the indices of all modules within this program that contain commands that are labelled with the given * Retrieves the indices of all modules within this program that contain commands that are labelled with the
* action. * given action.
* *
* @param action The name of the action the modules are supposed to possess. * @param action The name of the action the modules are supposed to possess.
* @return A set of indices of all matching modules. * @return A set of indices of all matching modules.
@ -157,15 +186,20 @@ namespace storm {
*/ */
uint_fast64_t getModuleIndexByVariable(std::string const& variableName) const; uint_fast64_t getModuleIndexByVariable(std::string const& variableName) const;
std::map<std::string, storm::ir::RewardModel> const& getRewardModels() const; /*!
* Retrieves the reward models of the program.
*
* @return The reward models of the program.
*/
std::map<std::string, storm::prism::RewardModel> const& getRewardModels() const;
/*! /*!
* Retrieves the reward model with the given name. * 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. * @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. * Retrieves all labels that are defined by the probabilitic program.
@ -200,16 +234,23 @@ namespace storm {
std::map<std::string, BooleanVariable> globalBooleanVariables; std::map<std::string, BooleanVariable> globalBooleanVariables;
// A list of global integer variables. // A list of global integer variables.
std::std::string, IntegerVariable> globalIntegerVariables; std::map<std::string, IntegerVariable> globalIntegerVariables;
// The modules associated with the program. // The modules associated with the program.
std::vector<storm::ir::Module> modules; std::vector<storm::prism::Module> modules;
// The reward models associated with the program. // The reward models associated with the program.
std::map<std::string, storm::ir::RewardModel> rewardModels; std::map<std::string, storm::prism::RewardModel> 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. // The labels that are defined for this model.
std::map<std::string, Expression> labels; std::map<std::string, storm::expressions::Expression> labels;
// The set of actions present in this program. // The set of actions present in this program.
std::set<std::string> actions; std::set<std::string> actions;
@ -221,7 +262,7 @@ namespace storm {
std::map<std::string, uint_fast64_t> variableToModuleIndexMap; std::map<std::string, uint_fast64_t> variableToModuleIndexMap;
}; };
} // namespace ir } // namespace prism
} // namespace storm } // namespace storm
#endif /* STORM_IR_PROGRAM_H_ */ #endif /* STORM_STORAGE_PRISM_PROGRAM_H_ */

51
src/storage/prism/RewardModel.cpp
View File

@ -1,43 +1,20 @@
/* #include "src/storage/prism/RewardModel.h"
* RewardModel.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include <sstream>
#include "RewardModel.h"
namespace storm { namespace storm {
namespace ir { namespace prism {
RewardModel::RewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) {
RewardModel::RewardModel() : rewardModelName(), stateRewards(), transitionRewards() {
// Nothing to do here.
}
RewardModel::RewardModel(std::string const& rewardModelName, std::vector<storm::ir::StateReward> const& stateRewards, std::vector<storm::ir::TransitionReward> const& transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) {
// Nothing to do here. // Nothing to do here.
} }
std::string RewardModel::toString() const { std::string const& RewardModel::getName() const {
std::stringstream result; return this->rewardModelName;
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 { bool RewardModel::hasStateRewards() const {
return this->stateRewards.size() > 0; return this->stateRewards.size() > 0;
} }
std::vector<storm::ir::StateReward> const& RewardModel::getStateRewards() const { std::vector<storm::prism::StateReward> const& RewardModel::getStateRewards() const {
return this->stateRewards; return this->stateRewards;
} }
@ -45,9 +22,21 @@ namespace storm {
return this->transitionRewards.size() > 0; return this->transitionRewards.size() > 0;
} }
std::vector<storm::ir::TransitionReward> const& RewardModel::getTransitionRewards() const { std::vector<storm::prism::TransitionReward> const& RewardModel::getTransitionRewards() const {
return this->transitionRewards; 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 } // namespace storm

73
src/storage/prism/RewardModel.h
View File

@ -1,88 +1,81 @@
/* #ifndef STORM_STORAGE_PRISM_REWARDMODEL_H_
* RewardModel.h #define STORM_STORAGE_PRISM_REWARDMODEL_H_
*
* Created on: 04.01.2013
* Author: Christian Dehnert
*/
#ifndef STORM_IR_REWARDMODEL_H_
#define STORM_IR_REWARDMODEL_H_
#include <string> #include <string>
#include <vector> #include <vector>
#include "StateReward.h" #include "src/storage/prism/StateReward.h"
#include "TransitionReward.h" #include "src/storage/prism/TransitionReward.h"
namespace storm { namespace storm {
namespace ir { namespace prism {
/*!
* A class representing a reward model.
*/
class RewardModel { class RewardModel {
public: public:
/*! /*!
* Default constructor. Creates an empty reward model. * Creates a reward model with the given name, state and transition rewards.
*/
RewardModel();
/*!
* Creates a reward module with the given name, state and transition rewards.
* *
* @param rewardModelName The name of the reward model. * @param rewardModelName The name of the reward model.
* @param stateRewards A vector of state-based rewards. * @param stateRewards A vector of state-based rewards.
* @param transitionRewards A vector of transition-based rewards. * @param transitionRewards A vector of transition-based rewards.
*/ */
RewardModel(std::string const& rewardModelName, std::vector<storm::ir::StateReward> const& stateRewards, std::vector<storm::ir::TransitionReward> const& transitionRewards); RewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::TransitionReward> 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; 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<storm::ir::StateReward> const& getStateRewards() const; std::vector<storm::prism::StateReward> 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; 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<storm::ir::TransitionReward> const& getTransitionRewards() const; std::vector<storm::prism::TransitionReward> const& getTransitionRewards() const;
friend std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel);
private: private:
// The name of the reward model. // The name of the reward model.
std::string rewardModelName; std::string rewardModelName;
// The state-based rewards associated with this reward model. // The state-based rewards associated with this reward model.
std::vector<storm::ir::StateReward> stateRewards; std::vector<storm::prism::StateReward> stateRewards;
// The transition-based rewards associated with this reward model. // The transition-based rewards associated with this reward model.
std::vector<storm::ir::TransitionReward> transitionRewards; std::vector<storm::prism::TransitionReward> transitionRewards;
}; };
} // namespace ir } // namespace prism
} // namespace storm } // namespace storm
#endif /* STORM_IR_REWARDMODEL_H_ */ #endif /* STORM_STORAGE_PRISM_REWARDMODEL_H_ */

38
src/storage/prism/StateReward.cpp
View File

@ -1,38 +1,22 @@
/* #include "src/storage/prism/StateReward.h"
* StateReward.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include <sstream>
#include "StateReward.h"
namespace storm { namespace storm {
namespace ir { namespace prism {
StateReward::StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression) : statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) {
StateReward::StateReward() : statePredicate(), rewardValue() {
// Nothing to do here. // Nothing to do here.
} }
StateReward::StateReward(storm::expressions::Expression const& statePredicate, storm::expressions::Expression const& rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) { storm::expressions::Expression const& StateReward::getStatePredicateExpression() const {
// Nothing to do here. return this->statePredicateExpression;
} }
std::string StateReward::toString() const { storm::expressions::Expression const& StateReward::getRewardValueExpression() const {
std::stringstream result; return this->rewardValueExpression;
result << "\t" << statePredicate << ": " << rewardValue << ";";
return result.str();
} }
storm::expressions::Expression const& StateReward::getStatePredicate() const { std::ostream& operator<<(std::ostream& stream, StateReward const& stateReward) {
return this->statePredicate; stream << "\t" << stateReward.getStatePredicateExpression() << ": " << stateReward.getRewardValueExpression() << ";";
return stream;
} }
} // namespace prism
storm::expressions::Expression const& StateReward::getRewardValue() const {
return this->rewardValue;
}
} // namespace ir
} // namespace storm } // namespace storm

76
src/storage/prism/StateReward.h
View File

@ -1,85 +1,53 @@
/* #ifndef STORM_STORAGE_PRISM_STATEREWARD_H_
* StateReward.h #define STORM_STORAGE_PRISM_STATEREWARD_H_
*
* Created on: Jan 10, 2013
* Author: Christian Dehnert
*/
#ifndef STORM_IR_STATEREWARD_H_
#define STORM_IR_STATEREWARD_H_
#include <memory>
#include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expression.h"
namespace storm { namespace storm {
namespace ir { namespace prism {
/*!
* A class representing a state reward.
*/
class StateReward { class StateReward {
public: public:
/*! /*!
* Default constructor. Creates an empty state reward. * Creates a state reward for the states satisfying the given expression with the value given by a second
*/ * expression.
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. * @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(StateReward const& otherReward) = default; StateReward(storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression);
/*! // Create default implementations of constructors/assignment.
* Performs a deep-copy of the given reward and assigns it to the current one. StateReward() = default;
* StateReward(StateReward const& otherVariable) = default;
* @param otherReward The reward to assign. StateReward& operator=(StateReward const& otherVariable)= default;
*/ StateReward(StateReward&& otherVariable) = default;
StateReward& operator=(StateReward const& otherReward) = default; StateReward& operator=(StateReward&& otherVariable) = default;
/*!
* Retrieves a string representation of this state reward.
*
* @return A string representation of this state reward.
*/
std::string toString() const;
/*! /*!
* Retrieves the state predicate that is associated with this state reward. * Retrieves the state predicate that is associated with this state reward.
* *
* @return 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. * Retrieves the reward value associated with this state reward.
* *
* @return 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: private:
// The predicate that characterizes the states that obtain this reward. // 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. // The expression that specifies the value of the reward obtained.
storm::expressions::Expression rewardValue; storm::expressions::Expression rewardValueExpression;
}; };
} // namespace ir } // namespace prism
} // namespace storm } // namespace storm
#endif /* STORM_IR_STATEREWARD_H_ */ #endif /* STORM_STORAGE_PRISM_STATEREWARD_H_ */

41
src/storage/prism/TransitionReward.cpp
View File

@ -1,42 +1,27 @@
/* #include "src/storage/prism/TransitionReward.h"
* TransitionReward.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include <sstream>
#include "TransitionReward.h"
namespace storm { namespace storm {
namespace ir { namespace prism {
TransitionReward::TransitionReward(std::string const& commandName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression) : commandName(commandName), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) {
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) {
// Nothing to do here. // 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 { std::string const& TransitionReward::getActionName() const {
return this->commandName; return this->commandName;
} }
storm::expressions::Expression const& TransitionReward::getStatePredicate() const { storm::expressions::Expression const& TransitionReward::getStatePredicateExpression() const {
return this->statePredicate; return this->statePredicateExpression;
}
storm::expressions::Expression const& TransitionReward::getRewardValueExpression() const {
return this->rewardValueExpression;
} }
storm::expressions::Expression const& TransitionReward::getRewardValue() const { std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward) {
return this->rewardValue; stream << "\t[" << transitionReward.getActionName() << "] " << transitionReward.getStatePredicateExpression() << ": " << transitionReward.getRewardValueExpression() << ";";
return stream;
} }
} // namespace ir } // namespace prism
} // namespace storm } // namespace storm

89
src/storage/prism/TransitionReward.h
View File

@ -1,63 +1,29 @@
/* #ifndef STORM_STORAGE_PRISM_TRANSITIONREWARD_H_
* TransitionReward.h #define STORM_STORAGE_PRISM_TRANSITIONREWARD_H_
*
* Created on: Jan 10, 2013
* Author: Christian Dehnert
*/
#ifndef STORM_IR_TRANSITIONREWARD_H_
#define STORM_IR_TRANSITIONREWARD_H_
#include <memory>
#include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expression.h"
namespace storm { namespace storm {
namespace prism {
namespace ir {
/*!
* A class representing a transition reward.
*/
class TransitionReward { class TransitionReward {
public: public:
/*! /*!
* Default constructor. Creates an empty transition reward. * 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.
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. * @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& operator=(TransitionReward const& otherReward) = default; TransitionReward(std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression);
/*! // Create default implementations of constructors/assignment.
* Retrieves a string representation of this transition reward. TransitionReward() = default;
* TransitionReward(TransitionReward const& otherVariable) = default;
* @return A string representation of this transition reward. TransitionReward& operator=(TransitionReward const& otherVariable)= default;
*/ TransitionReward(TransitionReward&& otherVariable) = default;
std::string toString() const; TransitionReward& operator=(TransitionReward&& otherVariable) = default;
/*! /*!
* Retrieves the action name that is associated with this transition reward. * Retrieves the action name that is associated with this transition reward.
@ -67,18 +33,20 @@ public:
std::string const& getActionName() const; std::string const& getActionName() const;
/*! /*!
* Retrieves the state predicate that is associated with this state reward. * Retrieves the state predicate expression that is associated with this state reward.
* *
* @return The state predicate that is associated with this state reward. * @return The state predicate expression 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. * Retrieves the reward value expression associated with this state reward.
* *
* @return The reward value associated with this state reward. * @return The reward value expression associated with this state reward.
*/ */
storm::expressions::Expression const& getRewardValue() const; storm::expressions::Expression const& getRewardValueExpression() const;
friend std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward);
private: private:
// The name of the command this transition-based reward is attached to. // The name of the command this transition-based reward is attached to.
@ -86,14 +54,13 @@ private:
// A predicate that needs to be satisfied by states for the reward to be obtained (by taking // A predicate that needs to be satisfied by states for the reward to be obtained (by taking
// a corresponding command transition). // a corresponding command transition).
storm::expressions::Expression statePredicate; storm::expressions::Expression statePredicateExpression;
// The expression specifying the value of the reward obtained along the transitions. // The expression specifying the value of the reward obtained along the transitions.
storm::expressions::Expression rewardValue; storm::expressions::Expression rewardValueExpression;
}; };
} // namespace ir } // namespace prism
} // namespace storm } // namespace storm
#endif /* STORM_IR_TRANSITIONREWARD_H_ */ #endif /* STORM_STORAGE_PRISM_TRANSITIONREWARD_H_ */
Write Preview
|||||||
100:0
Loading…
Cancel
Save