Browse Source

Removed some unnecessary boost stuff from IR expressions. Separated header and source file for all non-expression IR entities (expressions are still to come). Added comments for these classes.

tempestpy_adaptions
dehnert 12 years ago
parent
commit
50f891b9f2
  1. 46
      src/ir/Assignment.cpp
  2. 70
      src/ir/Assignment.h
  3. 41
      src/ir/BooleanVariable.cpp
  4. 55
      src/ir/BooleanVariable.h
  5. 43
      src/ir/Command.cpp
  6. 60
      src/ir/Command.h
  7. 9
      src/ir/IR.h
  8. 39
      src/ir/IntegerVariable.cpp
  9. 61
      src/ir/IntegerVariable.h
  10. 46
      src/ir/Module.cpp
  11. 70
      src/ir/Module.h
  12. 67
      src/ir/Program.cpp
  13. 114
      src/ir/Program.h
  14. 42
      src/ir/RewardModel.cpp
  15. 67
      src/ir/RewardModel.h
  16. 35
      src/ir/StateReward.cpp
  17. 51
      src/ir/StateReward.h
  18. 35
      src/ir/TransitionReward.cpp
  19. 53
      src/ir/TransitionReward.h
  20. 45
      src/ir/Update.cpp
  21. 61
      src/ir/Update.h
  22. 38
      src/ir/Variable.cpp
  23. 68
      src/ir/Variable.h
  24. 7
      src/ir/expressions/BinaryBooleanFunctionExpression.h
  25. 7
      src/ir/expressions/BinaryNumericalFunctionExpression.h
  26. 7
      src/ir/expressions/BinaryRelationExpression.h
  27. 7
      src/ir/expressions/BooleanConstantExpression.h
  28. 5
      src/ir/expressions/BooleanLiteral.h
  29. 5
      src/ir/expressions/ConstantExpression.h
  30. 5
      src/ir/expressions/DoubleConstantExpression.h
  31. 5
      src/ir/expressions/DoubleLiteral.h
  32. 5
      src/ir/expressions/IntegerConstantExpression.h
  33. 5
      src/ir/expressions/IntegerLiteral.h
  34. 6
      src/ir/expressions/UnaryBooleanFunctionExpression.h
  35. 6
      src/ir/expressions/UnaryNumericalFunctionExpression.h
  36. 5
      src/ir/expressions/VariableExpression.h

46
src/ir/Assignment.cpp

@ -0,0 +1,46 @@
/*
* Assignment.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include "Assignment.h"
#include <sstream>
namespace storm {
namespace ir {
// Initializes all members with their default constructors.
Assignment::Assignment() : variableName(), expression() {
// Nothing to do here.
}
// Initializes all members according to the given values.
Assignment::Assignment(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> expression)
: variableName(variableName), expression(expression) {
// Nothing to do here.
}
// Returns the name of the variable associated with this assignment.
std::string const& Assignment::getVariableName() const {
return variableName;
}
// Returns the expression associated with this assignment.
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Assignment::getExpression() const {
return expression;
}
// Build a string representation of the assignment.
std::string Assignment::toString() const {
std::stringstream result;
result << "(" << variableName << "' = " << expression->toString() << ")";
return result.str();
}
} // namespace ir
} // namespace storm

70
src/ir/Assignment.h

@ -2,49 +2,65 @@
* Assignment.h
*
* Created on: 06.01.2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef ASSIGNMENT_H_
#define ASSIGNMENT_H_
#ifndef STORM_IR_ASSIGNMENT_H_
#define STORM_IR_ASSIGNMENT_H_
#include "expressions/BaseExpression.h"
#include <memory>
namespace storm {
namespace ir {
/*!
* A class representing the assignment of an expression to a variable.
*/
class Assignment {
public:
Assignment() : variableName(""), expression(nullptr) {
}
Assignment(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> expression)
: variableName(variableName), expression(expression) {
}
std::string getVariableName() {
return variableName;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> getExpression() {
return expression;
}
std::string toString() {
return "(" + variableName + "' = " + expression->toString() + ")";
}
/*!
* Default constructor. Creates an empty assignment.
*/
Assignment();
/*!
* Constructs an assignment using the given variable name and expression.
* @param variableName the variable that this assignment targets.
* @param expression the expression to assign to the variable.
*/
Assignment(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> expression);
/*!
* Retrieves the name of the variable that this assignment targets.
* @returns the name of the variable that this assignment targets.
*/
std::string const& getVariableName() const;
/*!
* Retrieves the expression that is assigned to the variable.
* @returns the expression that is assigned to the variable.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> const& getExpression() const;
/*!
* Retrieves a string representation of this assignment.
* @returns a string representation of this assignment.
*/
std::string toString() const;
private:
// The name of the variable that this assignment targets.
std::string variableName;
// The expression that is assigned to the variable.
std::shared_ptr<storm::ir::expressions::BaseExpression> expression;
};
}
} // namespace ir
}
} // namespace storm
#endif /* ASSIGNMENT_H_ */
#endif /* STORM_IR_ASSIGNMENT_H_ */

41
src/ir/BooleanVariable.cpp

@ -0,0 +1,41 @@
/*
* BooleanVariable.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include "BooleanVariable.h"
#include <sstream>
namespace storm {
namespace ir {
// Initializes all members with their default constructors.
BooleanVariable::BooleanVariable() : Variable() {
// Nothing to do here.
}
// Initializes all members according to the given values.
BooleanVariable::BooleanVariable(std::string variableName,
std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue)
: Variable(variableName, initialValue) {
// Nothing to do here.
}
// Build a string representation of the variable.
std::string BooleanVariable::toString() const {
std::stringstream result;
result << getVariableName() << ": bool";
if (this->getInitialValue() != nullptr) {
result << " init " << this->getInitialValue()->toString();
}
result << ";";
return result.str();
}
} // namespace ir
} // namespace storm

55
src/ir/BooleanVariable.h

@ -2,42 +2,45 @@
* BooleanVariable.h
*
* Created on: 08.01.2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef BOOLEANVARIABLE_H_
#define BOOLEANVARIABLE_H_
#ifndef STORM_IR_BOOLEANVARIABLE_H_
#define STORM_IR_BOOLEANVARIABLE_H_
#include "Variable.h"
#include <memory>
namespace storm {
namespace ir {
/*!
* A class representing a boolean variable.
*/
class BooleanVariable : public Variable {
public:
BooleanVariable() {
}
BooleanVariable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = nullptr) : Variable(variableName, initialValue) {
}
virtual ~BooleanVariable() {
}
virtual std::string toString() {
std::string result = getVariableName() + ": bool";
if (this->getInitialValue() != nullptr) {
result += " init " + this->getInitialValue()->toString();
}
result += ";";
return result;
}
/*!
* Default constructor. Creates a boolean variable without a name.
*/
BooleanVariable();
/*!
* Creates a boolean variable with the given name and the given initial value.
* @param variableName the name of the variable.
* @param initialValue the expression that defines the initial value of the variable.
*/
BooleanVariable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
/*!
* Retrieves a string representation of this variable.
* @returns a string representation of this variable.
*/
std::string toString() const;
};
}
} // namespace ir
}
} // namespace storm
#endif /* BOOLEANVARIABLE_H_ */
#endif /* STORM_IR_BOOLEANVARIABLE_H_ */

43
src/ir/Command.cpp

@ -0,0 +1,43 @@
/*
* Command.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include "Command.h"
#include <sstream>
namespace storm {
namespace ir {
// Initializes all members with their default constructors.
Command::Command() : commandName(), guardExpression(), updates() {
// Nothing to do here.
}
// Initializes all members according to the given values.
Command::Command(std::string commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> updates)
: commandName(commandName), guardExpression(guardExpression), updates(updates) {
// Nothing to do here.
}
// Build a string representation of the command.
std::string Command::toString() const {
std::stringstream result;
result << "[" << commandName << "] " << guardExpression->toString() << " -> ";
for (uint_fast64_t i = 0; i < updates.size(); ++i) {
result << updates[i].toString();
if (i < updates.size() - 1) {
result << " + ";
}
}
result << ";";
return result.str();
}
} // namespace ir
} // namespace storm

60
src/ir/Command.h

@ -2,54 +2,58 @@
* Command.h
*
* Created on: 06.01.2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef COMMAND_H_
#define COMMAND_H_
#ifndef STORM_IR_COMMAND_H_
#define STORM_IR_COMMAND_H_
#include "expressions/BaseExpression.h"
#include "Update.h"
#include <vector>
#include <string>
namespace storm {
namespace ir {
/*!
* A class representing a command.
*/
class Command {
public:
Command() : commandName(""), guardExpression(nullptr), updates() {
}
Command(std::string commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> updates)
: commandName(commandName), guardExpression(guardExpression), updates(updates) {
}
std::string toString() {
std::string result = "[" + commandName + "] " + guardExpression->toString() + " -> ";
for (uint_fast64_t i = 0; i < updates.size(); ++i) {
result += updates[i].toString();
if (i < updates.size() - 1) {
result += " + ";
}
}
result += ";";
return result;
}
/*!
* Default constructor. Creates a a command without name, guard and updates.
*/
Command();
/*!
* Creates a command with the given name, guard and updates.
* @param commandName the name of the command.
* @param guardExpression the expression that defines the guard of the command.
*/
Command(std::string commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> updates);
/*!
* Retrieves a string representation of this command.
* @returns a string representation of this command.
*/
std::string toString() const;
private:
// The name of the command.
std::string commandName;
// The expression that defines the guard of the command.
std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression;
std::vector<storm::ir::Update> updates;
// The list of updates of the command.
std::vector<storm::ir::Update> updates;
};
}
} // namespace ir
}
} // namespace storm
#endif /* COMMAND_H_ */
#endif /* STORM_IR_COMMAND_H_ */

9
src/ir/IR.h

@ -2,12 +2,13 @@
* IR.h
*
* Created on: 06.01.2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef IR_H_
#define IR_H_
#ifndef STORM_IR_IR_H_
#define STORM_IR_IR_H_
// Bundle all headers to make it easy to include them.
#include "expressions/Expressions.h"
#include "Assignment.h"
#include "Update.h"
@ -21,4 +22,4 @@
#include "RewardModel.h"
#include "Program.h"
#endif /* IR_H_ */
#endif /* STORM_IR_IR_H_ */

39
src/ir/IntegerVariable.cpp

@ -0,0 +1,39 @@
/*
* IntegerVariable.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include "IntegerVariable.h"
#include <sstream>
namespace storm {
namespace ir {
// Initializes all members with their default constructors.
IntegerVariable::IntegerVariable() : lowerBound(), upperBound() {
// Nothing to do here.
}
// Initializes all members according to the given values.
IntegerVariable::IntegerVariable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue) : Variable(variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) {
// Nothing to do here.
}
// Build a string representation of the variable.
std::string IntegerVariable::toString() const {
std::stringstream result;
result << this->getVariableName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]";
if (this->getInitialValue() != nullptr) {
result << " init " + this->getInitialValue()->toString();
}
result << ";";
return result.str();
}
} // namespace ir
} // namespace storm

61
src/ir/IntegerVariable.h

@ -2,49 +2,56 @@
* IntegerVariable.h
*
* Created on: 08.01.2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef INTEGERVARIABLE_H_
#define INTEGERVARIABLE_H_
#ifndef STORM_IR_INTEGERVARIABLE_H_
#define STORM_IR_INTEGERVARIABLE_H_
#include "Variable.h"
#include "expressions/BaseExpression.h"
#include "Variable.h"
#include <memory>
namespace storm {
namespace ir {
/*!
* A class representing an integer variable.
*/
class IntegerVariable : public Variable {
public:
IntegerVariable() : lowerBound(nullptr), upperBound(nullptr) {
}
IntegerVariable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = nullptr) : Variable(variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) {
}
virtual ~IntegerVariable() {
}
virtual std::string toString() {
std::string result = getVariableName() + ": [" + lowerBound->toString() + ".." + upperBound->toString() + "]";
if (this->getInitialValue() != nullptr) {
result += " init " + this->getInitialValue()->toString();
}
result += ";";
return result;
}
/*!
* Default constructor. Creates an integer variable without a name and lower and upper bounds.
*/
IntegerVariable();
/*!
* Creates an integer variable with the given name, lower and upper bounds and the given initial
* value.
* @param variableName the name of the variable.
* @param lowerBound the lower bound of the domain of the variable.
* @param upperBound the upper bound of the domain of the variable.
* @param initialValue the expression that defines the initial value of the variable.
*/
IntegerVariable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
/*!
* Retrieves a string representation of this variable.
* @returns a string representation of this variable.
*/
std::string toString() const;
private:
// The lower bound of the domain of the variable.
std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound;
// The upper bound of the domain of the variable.
std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound;
};
}
} // namespace ir
}
} // namespace storm
#endif /* INTEGERVARIABLE_H_ */
#endif /* STORM_IR_INTEGERVARIABLE_H_ */

46
src/ir/Module.cpp

@ -0,0 +1,46 @@
/*
* Module.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include "Module.h"
#include <sstream>
namespace storm {
namespace ir {
// Initializes all members with their default constructors.
Module::Module() : moduleName(), booleanVariables(), integerVariables(), commands() {
// Nothing to do here.
}
// Initializes all members according to the given values.
Module::Module(std::string moduleName, std::map<std::string, storm::ir::BooleanVariable> booleanVariables, std::map<std::string, storm::ir::IntegerVariable> integerVariables, std::vector<storm::ir::Command> commands)
: moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands) {
// Nothing to do here.
}
// Build a string representation of the variable.
std::string Module::toString() const {
std::stringstream result;
result << "module " << moduleName << std::endl;
for (auto variable : booleanVariables) {
result << "\t" << variable.second.toString() << std::endl;
}
for (auto variable : integerVariables) {
result << "\t" << variable.second.toString() << std::endl;
}
for (auto command : commands) {
result << "\t" << command.toString() << std::endl;
}
result << "endmodule" << std::endl;
return result.str();
}
} // namespace ir
} // namespace storm

70
src/ir/Module.h

@ -2,61 +2,65 @@
* Module.h
*
* Created on: 04.01.2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef MODULE_H_
#define MODULE_H_
#ifndef STORM_IR_MODULE_H_
#define STORM_IR_MODULE_H_
#include "BooleanVariable.h"
#include "IntegerVariable.h"
#include "Command.h"
#include <map>
#include <string>
#include <vector>
namespace storm {
namespace ir {
/*!
* A class representing a module.
*/
class Module {
public:
Module() : moduleName(""), booleanVariables(), integerVariables(), commands() {
}
Module(std::string moduleName, std::map<std::string, storm::ir::BooleanVariable> booleanVariables, std::map<std::string, storm::ir::IntegerVariable> integerVariables, std::vector<storm::ir::Command> commands)
: moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands) {
}
Module(std::string moduleName, std::vector<storm::ir::Command> commands) : moduleName(moduleName), booleanVariables(), integerVariables(), commands(commands) {
}
std::string toString() {
std::string result = "module " + moduleName + "\n";
for (auto variable : booleanVariables) {
result += "\t" + variable.second.toString() + "\n";
}
for (auto variable : integerVariables) {
result += "\t" + variable.second.toString() + "\n";
}
for (auto command : commands) {
result += "\t" + command.toString() + "\n";
}
result += "endmodule\n";
return result;
}
/*!
* 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 a map of boolean variables.
* @param integerVariables a map of integer variables.
* @param commands the vector of commands.
*/
Module(std::string moduleName, std::map<std::string, storm::ir::BooleanVariable> booleanVariables, std::map<std::string, storm::ir::IntegerVariable> integerVariables, std::vector<storm::ir::Command> commands);
/*!
* Retrieves a string representation of this variable.
* @returns a string representation of this variable.
*/
std::string toString() const;
private:
// The name of the module.
std::string moduleName;
// A map of boolean variable names to their details.
std::map<std::string, storm::ir::BooleanVariable> booleanVariables;
// A map of integer variable names to their details.
std::map<std::string, storm::ir::IntegerVariable> integerVariables;
// The commands associated with the module.
std::vector<storm::ir::Command> commands;
};
}
} // namespace ir
}
} // namespace storm
#endif /* MODULE_H_ */
#endif /* STORM_IR_MODULE_H_ */

67
src/ir/Program.cpp

@ -0,0 +1,67 @@
/*
* Program.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include "Program.h"
#include <sstream>
namespace storm {
namespace ir {
// Initializes all members with their default constructors.
Program::Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards() {
// Nothing to do here.
}
// Initializes all members according to the given values.
Program::Program(ModelType modelType, std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions, std::vector<storm::ir::Module> modules, std::map<std::string, storm::ir::RewardModel> rewards, std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels)
: modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards), labels(labels) {
// Nothing to do here.
}
// Build a string representation of the program.
std::string Program::toString() const {
std::stringstream result;
switch (modelType) {
case UNDEFINED: result << "undefined"; break;
case DTMC: result << "dtmc"; break;
case CTMC: result << "ctmc"; break;
case MDP: result << "mdp"; break;
case CTMDP: result << "ctmdp"; break;
}
result << std::endl;
for (auto element : booleanUndefinedConstantExpressions) {
result << "const bool " << element.first << ";" << std::endl;
}
for (auto element : integerUndefinedConstantExpressions) {
result << "const int " << element.first << ";" << std::endl;
}
for (auto element : doubleUndefinedConstantExpressions) {
result << "const double " << element.first << ";" << std::endl;
}
result << std::endl;
for (auto mod : modules) {
result << mod.toString() << std::endl;
}
for (auto rewardModel : rewards) {
result << rewardModel.second.toString() << std::endl;
}
for (auto label : labels) {
result << "label " << label.first << " = " << label.second->toString() <<";" << std::endl;
}
return result.str();
}
} // namespace ir
} // namepsace storm

114
src/ir/Program.h

@ -2,11 +2,11 @@
* Program.h
*
* Created on: 04.01.2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef PROGRAM_H_
#define PROGRAM_H_
#ifndef STORM_IR_PROGRAM_H_
#define STORM_IR_PROGRAM_H_
#include "expressions/BaseExpression.h"
#include "expressions/BooleanConstantExpression.h"
@ -15,82 +15,76 @@
#include "Module.h"
#include "RewardModel.h"
#include <map>
#include <vector>
#include <memory>
namespace storm {
namespace ir {
/*!
* A class representing a program.
*/
class Program {
public:
/*!
* An enum for the different model types.
*/
enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP};
Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards() {
}
Program(ModelType modelType, std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions, std::vector<storm::ir::Module> modules, std::map<std::string, storm::ir::RewardModel> rewards, std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels)
: modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards), labels(labels) {
}
Program(ModelType modelType, std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions, std::vector<storm::ir::Module> modules)
: modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards() {
}
Program(ModelType modelType, std::vector<storm::ir::Module> modules) : modelType(modelType), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(modules), rewards() {
}
std::string toString() {
std::string result = "";
switch (modelType) {
case UNDEFINED: result += "undefined\n\n"; break;
case DTMC: result += "dtmc\n\n"; break;
case CTMC: result += "ctmc\n\n"; break;
case MDP: result += "mdp\n\n"; break;
case CTMDP: result += "ctmdp\n\n"; break;
}
for (auto element : booleanUndefinedConstantExpressions) {
result += "const bool " + element.first + ";\n";
}
for (auto element : integerUndefinedConstantExpressions) {
result += "const int " + element.first + ";\n";
}
for (auto element : doubleUndefinedConstantExpressions) {
result += "const double " + element.first + ";\n";
}
result += "\n";
for (auto mod : modules) {
result += mod.toString();
result += "\n";
}
for (auto rewardModel : rewards) {
result += rewardModel.second.toString();
result +="\n";
}
for (auto label : labels) {
result += "label " + label.first + " = " + label.second->toString() + ";\n";
}
return result;
}
/*!
* Default constructor. Creates an empty program.
*/
Program();
/*!
* Creates a program with the given model type, undefined constants, modules, rewards and labels.
* @param modelType the type of the model that this program gives rise to.
* @param booleanUndefinedConstantExpressions a map of undefined boolean constants to their
* expression nodes.
* @param integerUndefinedConstantExpressions a map of undefined integer constants to their
* expression nodes.
* @param doubleUndefinedConstantExpressions a map of undefined double constants to their
* expression nodes.
* @param modules The modules of the program.
* @param rewards The reward models of the program.
* @param labels The labels defined for this model.
*/
Program(ModelType modelType, std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions, std::vector<storm::ir::Module> modules, std::map<std::string, storm::ir::RewardModel> rewards, std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels);
/*!
* Retrieves a string representation of this program.
* @returns a string representation of this program.
*/
std::string toString() const;
private:
// The type of the model.
ModelType modelType;
// A map of undefined boolean constants to their expression nodes.
std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions;
// A map of undefined integer constants to their expressions nodes.
std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions;
// A mpa of undefined double constants to their expressions nodes.
std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions;
// The modules associated with the program.
std::vector<storm::ir::Module> modules;
// The reward models associated with the program.
std::map<std::string, storm::ir::RewardModel> rewards;
// The labels that are defined for this model.
std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels;
};
}
} // namespace ir
}
} // namespace storm
#endif /* PROGRAM_H_ */
#endif /* STORM_IR_PROGRAM_H_ */

42
src/ir/RewardModel.cpp

@ -0,0 +1,42 @@
/*
* RewardModel.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include "RewardModel.h"
#include <sstream>
namespace storm {
namespace ir {
// Initializes all members with their default constructors.
RewardModel::RewardModel() : rewardModelName(), stateRewards(), transitionRewards() {
// Nothing to do here.
}
// Initializes all members according to the given values.
RewardModel::RewardModel(std::string rewardModelName, std::vector<storm::ir::StateReward> stateRewards, std::vector<storm::ir::TransitionReward> transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) {
// Nothing to do here.
}
// Build a string representation of the reward model.
std::string RewardModel::toString() const {
std::stringstream result;
result << "rewards \"" << rewardModelName << "\"" << std::endl;
for (auto reward : stateRewards) {
result << reward.toString() << std::endl;
}
for (auto reward : transitionRewards) {
result << reward.toString() << std::endl;
}
result << "endrewards" << std::endl;
return result.str();
}
} // namespace ir
} // namespace storm

67
src/ir/RewardModel.h

@ -2,52 +2,59 @@
* RewardModel.h
*
* Created on: 04.01.2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef REWARDMODEL_H_
#define REWARDMODEL_H_
#ifndef STORM_IR_REWARDMODEL_H_
#define STORM_IR_REWARDMODEL_H_
#include <iostream>
#include "StateReward.h"
#include "TransitionReward.h"
#include <string>
#include <vector>
namespace storm {
namespace ir {
/*!
* A class representing a reward model.
*/
class RewardModel {
public:
RewardModel() : rewardModelName(""), stateRewards(), transitionRewards() {
}
RewardModel(std::string rewardModelName, std::vector<storm::ir::StateReward> stateRewards, std::vector<storm::ir::TransitionReward> transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) {
}
RewardModel(RewardModel const& other) : rewardModelName(other.rewardModelName), stateRewards(other.stateRewards), transitionRewards(other.transitionRewards) {
}
std::string toString() {
std::string result = "rewards \"" + rewardModelName + "\"\n";
for (auto reward : stateRewards) {
result += reward.toString() + "\n";
}
for (auto reward : transitionRewards) {
result += reward.toString() + "\n";
}
result += "endrewards\n";
return result;
}
/*!
* Default constructor. Creates an empty reward model.
*/
RewardModel();
/*!
* Creates a reward module with the given name, state and transition rewards.
* @param rewardModelName the name of the reward model.
* @param stateRewards A vector of state-based reward.
* @param transitionRewards A vector of transition-based reward.
*/
RewardModel(std::string rewardModelName, std::vector<storm::ir::StateReward> stateRewards, std::vector<storm::ir::TransitionReward> transitionRewards);
/*!
* Retrieves a string representation of this variable.
* @returns a string representation of this variable.
*/
std::string toString() const;
private:
// The name of the reward model.
std::string rewardModelName;
// The state-based rewards associated with this reward model.
std::vector<storm::ir::StateReward> stateRewards;
// The transition-based rewards associated with this reward model.
std::vector<storm::ir::TransitionReward> transitionRewards;
};
}
} // namespace ir
}
} // namespace storm
#endif /* REWARDMODEL_H_ */
#endif /* STORM_IR_REWARDMODEL_H_ */

35
src/ir/StateReward.cpp

@ -0,0 +1,35 @@
/*
* StateReward.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include "StateReward.h"
#include <sstream>
namespace storm {
namespace ir {
// Initializes all members with their default constructors.
StateReward::StateReward() : statePredicate(), rewardValue() {
// Nothing to do here.
}
// Initializes all members according to the given values.
StateReward::StateReward(std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) {
// Nothing to do here.
}
// Build a string representation of the state reward.
std::string StateReward::toString() const {
std::stringstream result;
result << "\t" << statePredicate->toString() << ": " << rewardValue->toString() << ";";
return result.str();
}
} // namespace ir
} // namespace storm

51
src/ir/StateReward.h

@ -2,39 +2,56 @@
* StateReward.h
*
* Created on: Jan 10, 2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef STATEREWARD_H_
#define STATEREWARD_H_
#ifndef STORM_IR_STATEREWARD_H_
#define STORM_IR_STATEREWARD_H_
#include "expressions/BaseExpression.h"
#include <memory>
namespace storm {
namespace ir {
/*!
* A class representing a state reward.
*/
class StateReward {
public:
StateReward() : statePredicate(nullptr), rewardValue(nullptr) {
}
StateReward(std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) {
}
std::string toString() {
return "\t" + statePredicate->toString() + ": " + rewardValue->toString() + ";";
}
/*!
* 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(std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue);
/*!
* Retrieves a string representation of this state reward.
* @returns a string representation of this state reward.
*/
std::string toString() const;
private:
// The predicate that characterizes the states that obtain this reward.
std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate;
// The expression that specifies the value of the reward obtained.
std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue;
};
}
} // namespace ir
}
} // namespace storm
#endif /* STATEREWARD_H_ */
#endif /* STORM_IR_STATEREWARD_H_ */

35
src/ir/TransitionReward.cpp

@ -0,0 +1,35 @@
/*
* TransitionReward.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include "TransitionReward.h"
#include <sstream>
namespace storm {
namespace ir {
// Initializes all members with their default constructors.
TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardValue() {
// Nothing to do here.
}
// Initializes all members according to the given values.
TransitionReward::TransitionReward(std::string commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) {
// Nothing to do here.
}
// Build a string representation of the transition reward.
std::string TransitionReward::toString() const {
std::stringstream result;
result << "\t[" << commandName << "] " << statePredicate->toString() << ": " << rewardValue->toString() << ";";
return result.str();
}
} // namespace ir
} // namespace storm

53
src/ir/TransitionReward.h

@ -2,11 +2,11 @@
* TransitionReward.h
*
* Created on: Jan 10, 2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef TRANSITIONREWARD_H_
#define TRANSITIONREWARD_H_
#ifndef STORM_IR_TRANSITIONREWARD_H_
#define STORM_IR_TRANSITIONREWARD_H_
#include "expressions/BaseExpression.h"
@ -14,28 +14,47 @@ namespace storm {
namespace ir {
/*!
* A class representing a transition reward.
*/
class TransitionReward {
public:
TransitionReward() : commandName(""), statePredicate(nullptr), rewardValue(nullptr) {
}
TransitionReward(std::string commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) {
}
std::string toString() {
return "\t[" + commandName + "] " + statePredicate->toString() + ": " + rewardValue->toString() + ";";
}
/*!
* 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 commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue);
/*!
* Retrieves a string representation of this transition reward.
* @returns a string representation of this transition reward.
*/
std::string toString() 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).
std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate;
// The expression specifying the value of the reward obtained along the transitions.
std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue;
};
}
} // namespace ir
}
} // namespace storm
#endif /* TRANSITIONREWARD_H_ */
#endif /* STORM_IR_TRANSITIONREWARD_H_ */

45
src/ir/Update.cpp

@ -0,0 +1,45 @@
/*
* Update.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include "Update.h"
#include <sstream>
namespace storm {
namespace ir {
// Initializes all members with their default constructors.
Update::Update() : likelihoodExpression(), assignments() {
// Nothing to do here.
}
// Initializes all members according to the given values.
Update::Update(std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression, std::map<std::string, storm::ir::Assignment> assignments)
: likelihoodExpression(likelihoodExpression), assignments(assignments) {
// Nothing to do here.
}
// Build a string representation of the update.
std::string Update::toString() const {
std::stringstream result;
result << likelihoodExpression->toString() << " : ";
uint_fast64_t i = 0;
for (auto assignment : assignments) {
result << assignment.second.toString();
++i;
if (i < assignments.size() - 1) {
result << " & ";
}
}
return result.str();
}
} // namespace ir
} // namespace storm

61
src/ir/Update.h

@ -2,51 +2,56 @@
* Update.h
*
* Created on: 06.01.2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef UPDATE_H_
#define UPDATE_H_
#ifndef STORM_IR_UPDATE_H_
#define STORM_IR_UPDATE_H_
#include "expressions/BaseExpression.h"
#include "Assignment.h"
#include <map>
#include <memory>
namespace storm {
namespace ir {
/*!
* A class representing an update of a command.
*/
class Update {
public:
Update() : likelihoodExpression(nullptr), assignments() {
}
Update(std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression, std::map<std::string, storm::ir::Assignment> assignments)
: likelihoodExpression(likelihoodExpression), assignments(assignments) {
}
std::string toString() {
std::string result = likelihoodExpression->toString() + " : ";
uint_fast64_t i = 0;
for (auto assignment : assignments) {
result += assignment.second.toString();
++i;
if (i < assignments.size() - 1) {
result += " & ";
}
}
return result;
}
/*!
* Default constructor. Creates an empty update.
*/
Update();
/*!
* Creates an update with the given expression specifying the likelihood and the mapping of
* variable to their assignments.
* @param likelihoodExpression an expression specifying the likelihood of this update.
* @param assignments a map of variable names to their assignments.
*/
Update(std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression, std::map<std::string, storm::ir::Assignment> assignments);
/*!
* Retrieves a string representation of this update.
* @returns a string representation of this update.
*/
std::string toString() const;
private:
// An expression specifying the likelihood of taking this update.
std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression;
// A mapping of variable names to their assignments in this update.
std::map<std::string, storm::ir::Assignment> assignments;
};
}
} // namespace ir
}
} // namespace storm
#endif /* UPDATE_H_ */
#endif /*STORM_IR_UPDATE_H_ */

38
src/ir/Variable.cpp

@ -0,0 +1,38 @@
/*
* Variable.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include "Variable.h"
#include <sstream>
namespace storm {
namespace ir {
// Initializes all members with their default constructors.
Variable::Variable() : variableName(), initialValue() {
// Nothing to do here.
}
// Initializes all members according to the given values.
Variable::Variable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue) : variableName(variableName), initialValue(initialValue) {
// Nothing to do here.
}
// Return the name of the variable.
std::string const& Variable::getVariableName() const {
return variableName;
}
// Return the expression for the initial value of the variable.
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Variable::getInitialValue() const {
return initialValue;
}
} // namespace ir
} // namespace storm

68
src/ir/Variable.h

@ -2,50 +2,60 @@
* Variable.h
*
* Created on: 06.01.2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef VARIABLE_H_
#define VARIABLE_H_
#ifndef STORM_IR_VARIABLE_H_
#define STORM_IR_VARIABLE_H_
#include "expressions/BaseExpression.h"
#include <string>
namespace storm {
namespace ir {
/*!
* A class representing a untyped variable.
*/
class Variable {
public:
Variable() : variableName(""), initialValue(nullptr) {
}
Variable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = nullptr) : variableName(variableName), initialValue(initialValue) {
}
virtual ~Variable() {
}
virtual std::string toString() {
return variableName;
}
std::string getVariableName() {
return variableName;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> getInitialValue() {
return initialValue;
}
/*!
* Default constructor. Creates an unnamed, untyped variable without initial value.
*/
Variable();
/*!
* Creates an untyped variable with the given name and initial value.
* @param variableName the name of the variable.
* @param initialValue the expression that defines the initial value of the variable.
*/
Variable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
/*!
* Retrieves the name of the variable.
* @returns the name of the variable.
*/
std::string const& getVariableName() const;
/*!
* Retrieves the expression defining the initial value of the variable.
* @returns the expression defining the initial value of the variable.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> const& getInitialValue() const;
private:
// The name of the variable.
std::string variableName;
// The expression defining the initial value of the variable.
std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue;
};
}
} // namespace ir
}
} // namespace storm
#endif /* VARIABLE_H_ */
#endif /* STORM_IR_VARIABLE_H_ */

7
src/ir/expressions/BinaryBooleanFunctionExpression.h

@ -53,11 +53,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::BinaryBooleanFunctionExpression,
(std::shared_ptr<storm::ir::expressions::BaseExpression>, left)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, right)
(storm::ir::expressions::BinaryBooleanFunctionExpression::FunctorType, functor)
)
#endif /* BINARYBOOLEANFUNCTIONEXPRESSION_H_ */

7
src/ir/expressions/BinaryNumericalFunctionExpression.h

@ -53,11 +53,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::BinaryNumericalFunctionExpression,
(std::shared_ptr<storm::ir::expressions::BaseExpression>, left)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, right)
(storm::ir::expressions::BinaryNumericalFunctionExpression::FunctorType, functor)
)
#endif /* BINARYFUNCTIONEXPRESSION_H_ */

7
src/ir/expressions/BinaryRelationExpression.h

@ -54,11 +54,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::BinaryRelationExpression,
(std::shared_ptr<storm::ir::expressions::BaseExpression>, left)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, right)
(storm::ir::expressions::BinaryRelationExpression::RelationType, relation)
)
#endif /* BINARYRELATIONEXPRESSION_H_ */

7
src/ir/expressions/BooleanConstantExpression.h

@ -10,6 +10,8 @@
#include "ConstantExpression.h"
#include <boost/lexical_cast.hpp>
namespace storm {
namespace ir {
@ -58,9 +60,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::BooleanConstantExpression,
(std::string, constantName)
)
#endif /* BOOLEANCONSTANTEXPRESSION_H_ */

5
src/ir/expressions/BooleanLiteral.h

@ -43,9 +43,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::BooleanLiteral,
(bool, value)
)
#endif /* BOOLEANLITERAL_H_ */

5
src/ir/expressions/ConstantExpression.h

@ -39,9 +39,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::ConstantExpression,
(std::string, constantName)
)
#endif /* CONSTANTEXPRESSION_H_ */

5
src/ir/expressions/DoubleConstantExpression.h

@ -58,9 +58,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::DoubleConstantExpression,
(std::string, constantName)
)
#endif /* DOUBLECONSTANTEXPRESSION_H_ */

5
src/ir/expressions/DoubleLiteral.h

@ -41,9 +41,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::DoubleLiteral,
(double, value)
)
#endif /* DOUBLELITERAL_H_ */

5
src/ir/expressions/IntegerConstantExpression.h

@ -58,9 +58,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::IntegerConstantExpression,
(std::string, constantName)
)
#endif /* INTEGERCONSTANTEXPRESSION_H_ */

5
src/ir/expressions/IntegerLiteral.h

@ -39,9 +39,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::IntegerLiteral,
(int, value)
)
#endif /* INTEGERLITERAL_H_ */

6
src/ir/expressions/UnaryBooleanFunctionExpression.h

@ -47,10 +47,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::UnaryBooleanFunctionExpression,
(std::shared_ptr<storm::ir::expressions::BaseExpression>, child)
(storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType, functor)
)
#endif /* UNARYBOOLEANFUNCTIONEXPRESSION_H_ */

6
src/ir/expressions/UnaryNumericalFunctionExpression.h

@ -47,10 +47,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::UnaryNumericalFunctionExpression,
(std::shared_ptr<storm::ir::expressions::BaseExpression>, child)
(storm::ir::expressions::UnaryNumericalFunctionExpression::FunctorType, functor)
)
#endif /* UNARYFUNCTIONEXPRESSION_H_ */

5
src/ir/expressions/VariableExpression.h

@ -41,9 +41,4 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::VariableExpression,
(std::string, variableName)
)
#endif /* VARIABLEEXPRESSION_H_ */
Loading…
Cancel
Save