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

Further refactoring of IR classes.

main
dehnert 12 years ago
parent
e30c386f23
commit
7b8b1ebd4f
59 changed files with 2100 additions and 1871 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 32
      src/adapters/ExplicitModelAdapter.cpp
  2. 71
      src/ir/Assignment.cpp
  3. 128
      src/ir/Assignment.h
  4. 57
      src/ir/BooleanVariable.cpp
  5. 94
      src/ir/BooleanVariable.h
  6. 115
      src/ir/Command.cpp
  7. 166
      src/ir/Command.h
  8. 77
      src/ir/IntegerVariable.cpp
  9. 136
      src/ir/IntegerVariable.h
  10. 306
      src/ir/Module.cpp
  11. 338
      src/ir/Module.h
  12. 192
      src/ir/Program.cpp
  13. 262
      src/ir/Program.h
  14. 82
      src/ir/RewardModel.cpp
  15. 138
      src/ir/RewardModel.h
  16. 8
      src/ir/StateReward.cpp
  17. 16
      src/ir/StateReward.h
  18. 12
      src/ir/TransitionReward.cpp
  19. 21
      src/ir/TransitionReward.h
  20. 184
      src/ir/Update.cpp
  21. 208
      src/ir/Update.h
  22. 81
      src/ir/Variable.cpp
  23. 178
      src/ir/Variable.h
  24. 4
      src/ir/expressions/BaseExpression.h
  25. 2
      src/ir/expressions/BinaryBooleanFunctionExpression.cpp
  26. 4
      src/ir/expressions/BinaryBooleanFunctionExpression.h
  27. 2
      src/ir/expressions/BinaryNumericalFunctionExpression.cpp
  28. 2
      src/ir/expressions/BinaryNumericalFunctionExpression.h
  29. 2
      src/ir/expressions/BinaryRelationExpression.cpp
  30. 2
      src/ir/expressions/BinaryRelationExpression.h
  31. 2
      src/ir/expressions/BooleanConstantExpression.cpp
  32. 2
      src/ir/expressions/BooleanConstantExpression.h
  33. 2
      src/ir/expressions/BooleanLiteralExpression.cpp
  34. 2
      src/ir/expressions/BooleanLiteralExpression.h
  35. 6
      src/ir/expressions/ConstantExpression.cpp
  36. 4
      src/ir/expressions/ConstantExpression.h
  37. 14
      src/ir/expressions/DoubleConstantExpression.cpp
  38. 7
      src/ir/expressions/DoubleConstantExpression.h
  39. 10
      src/ir/expressions/DoubleLiteralExpression.cpp
  40. 4
      src/ir/expressions/DoubleLiteralExpression.h
  41. 6
      src/ir/expressions/Expressions.h
  42. 59
      src/ir/expressions/IntegerConstantExpression.cpp
  43. 133
      src/ir/expressions/IntegerConstantExpression.h
  44. 57
      src/ir/expressions/IntegerLiteral.h
  45. 40
      src/ir/expressions/IntegerLiteralExpression.cpp
  46. 46
      src/ir/expressions/IntegerLiteralExpression.h
  47. 56
      src/ir/expressions/UnaryBooleanFunctionExpression.cpp
  48. 124
      src/ir/expressions/UnaryBooleanFunctionExpression.h
  49. 24
      src/ir/expressions/UnaryExpression.cpp
  50. 52
      src/ir/expressions/UnaryExpression.h
  51. 69
      src/ir/expressions/UnaryNumericalFunctionExpression.cpp
  52. 144
      src/ir/expressions/UnaryNumericalFunctionExpression.h
  53. 43
      src/ir/expressions/VariableExpression.cpp
  54. 69
      src/ir/expressions/VariableExpression.h
  55. 10
      src/parser/prismparser/BaseGrammar.h
  56. 24
      src/parser/prismparser/PrismGrammar.cpp
  57. 8
      src/parser/prismparser/PrismGrammar.h
  58. 22
      src/parser/prismparser/VariableState.cpp
  59. 12
      src/parser/prismparser/VariableState.h

32
src/adapters/ExplicitModelAdapter.cpp
View File

@ -107,13 +107,15 @@ namespace adapters {
return ss.str();
}
std::shared_ptr<std::vector<double>> ExplicitModelAdapter::getStateRewards(std::vector<storm::ir::StateReward> const & rewards) {
std::shared_ptr<std::vector<double>> ExplicitModelAdapter::getStateRewards(std::vector<storm::ir::StateReward> const& rewards) {
std::shared_ptr<std::vector<double>> results(new std::vector<double>(this->allStates.size()));
for (uint_fast64_t index = 0; index < this->allStates.size(); index++) {
(*results)[index] = 0;
for (auto reward: rewards) {
// Add this reward to the state.
(*results)[index] += reward.getReward(this->allStates[index]);
// Add this reward to the state if the state is included in the state reward.
if (reward.getStatePredicate()->getValueAsBool(this->allStates[index]) == true) {
(*results)[index] += reward.getRewardValue()->getValueAsDouble(this->allStates[index]);
}
}
}
return results;
@ -154,13 +156,13 @@ namespace adapters {
for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) {
storm::ir::BooleanVariable var = module.getBooleanVariable(j);
this->booleanVariables[var.getIndex()] = var;
this->booleanVariableToIndexMap[var.getName()] = var.getIndex();
this->booleanVariables[var.getGlobalIndex()] = var;
this->booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex();
}
for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) {
storm::ir::IntegerVariable var = module.getIntegerVariable(j);
this->integerVariables[var.getIndex()] = var;
this->integerVariableToIndexMap[var.getName()] = var.getIndex();
this->integerVariables[var.getGlobalIndex()] = var;
this->integerVariableToIndexMap[var.getName()] = var.getGlobalIndex();
}
}
}
@ -185,13 +187,13 @@ namespace adapters {
for (uint_fast64_t i = 0; i < this->program.getNumberOfModules(); ++i) {
storm::ir::Module const& module = this->program.getModule(i);
std::shared_ptr<std::set<uint_fast64_t>> ids = module.getCommandsByAction(action);
if (ids->size() == 0) continue;
std::set<uint_fast64_t> const& ids = module.getCommandsByAction(action);
if (ids.size() == 0) continue;
std::list<storm::ir::Command> commands;
// Look up commands by their id. Add, if guard holds.
for (uint_fast64_t id : *ids) {
storm::ir::Command cmd = module.getCommand(id);
for (uint_fast64_t id : ids) {
storm::ir::Command const& cmd = module.getCommand(id);
if (cmd.getGuard()->getValueAsBool(state)) {
commands.push_back(module.getCommand(id));
}
@ -468,7 +470,9 @@ namespace adapters {
map[elem.first] += elem.second;
if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) {
for (auto reward : this->rewardModel->getTransitionRewards()) {
rewardMap[elem.first] += reward.getReward(choice.first, this->allStates[state]);
if (reward.getStatePredicate()->getValueAsBool(this->allStates[state]) == true) {
rewardMap[elem.first] += reward.getRewardValue()->getValueAsDouble(this->allStates[state]);
}
}
}
}
@ -513,7 +517,9 @@ namespace adapters {
if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) {
double rewardValue = 0;
for (auto reward : this->rewardModel->getTransitionRewards()) {
rewardValue = reward.getReward(choice.first, this->allStates[state]);
if (reward.getStatePredicate()->getValueAsBool(this->allStates[state]) == true) {
rewardValue = reward.getRewardValue()->getValueAsDouble(this->allStates[state]);
}
}
this->transitionRewards->addNextValue(nextRow, it.first, rewardValue);
}

71
src/ir/Assignment.cpp
View File

@ -8,42 +8,41 @@
#include <sstream>
#include "Assignment.h"
#include "src/parser/prismparser/VariableState.h"
namespace storm {
namespace ir {
Assignment::Assignment() : variableName(), expression() {
// Nothing to do here.
}
Assignment::Assignment(std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& expression)
: variableName(variableName), expression(expression) {
// Nothing to do here.
}
Assignment::Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap)
: variableName(oldAssignment.variableName), expression(oldAssignment.expression->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap)) {
auto renamingPair = renaming.find(oldAssignment.variableName);
if (renamingPair != renaming.end()) {
this->variableName = renamingPair->second;
}
}
std::string const& Assignment::getVariableName() const {
return variableName;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Assignment::getExpression() const {
return expression;
}
std::string Assignment::toString() const {
std::stringstream result;
result << "(" << variableName << "' = " << expression->toString() << ")";
return result.str();
}
} // namespace ir
namespace ir {
Assignment::Assignment() : variableName(), expression() {
// Nothing to do here.
}
Assignment::Assignment(std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& expression)
: variableName(variableName), expression(expression) {
// Nothing to do here.
}
Assignment::Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState)
: variableName(oldAssignment.variableName), expression(oldAssignment.expression->clone(renaming, variableState)) {
auto renamingPair = renaming.find(oldAssignment.variableName);
if (renamingPair != renaming.end()) {
this->variableName = renamingPair->second;
}
}
std::string const& Assignment::getVariableName() const {
return variableName;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Assignment::getExpression() const {
return expression;
}
std::string Assignment::toString() const {
std::stringstream result;
result << "(" << variableName << "' = " << expression->toString() << ")";
return result.str();
}
} // namespace ir
} // namespace storm

128
src/ir/Assignment.h
View File

@ -13,68 +13,72 @@
#include "expressions/BaseExpression.h"
namespace storm {
namespace ir {
/*!
* A class representing the assignment of an expression to a variable.
*/
class Assignment {
public:
/*!
* Default constructor. Creates an empty assignment.
*/
Assignment();
/*!
* Constructs an assignment using the given variable name and expression.
*
* @param variableName The variable that this assignment targets.
* @param expression The expression to assign to the variable.
*/
Assignment(std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& expression);
/*!
* Creates a copy of the given assignment and performs the provided renaming.
*
* @param oldAssignment The assignment to copy.
* @param renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
* @param booleanVariableToIndexMap A mapping from boolean variable names to their global indices.
* @param integerVariableToIndexMap A mapping from integer variable names to their global indices.
*/
Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& bools, std::map<std::string, uint_fast64_t> const& ints);
/*!
* Retrieves the name of the variable that this assignment targets.
*
* @return The name of the variable that this assignment targets.
*/
std::string const& getVariableName() const;
/*!
* Retrieves the expression that is assigned to the variable.
*
* @return The expression that is assigned to the variable.
*/
std::shared_ptr<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 parser {
namespace prism {
class VariableState;
} // namespace prismparser
} // namespace parser
namespace ir {
/*!
* A class representing the assignment of an expression to a variable.
*/
class Assignment {
public:
/*!
* Default constructor. Creates an empty assignment.
*/
Assignment();
/*!
* Constructs an assignment using the given variable name and expression.
*
* @param variableName The variable that this assignment targets.
* @param expression The expression to assign to the variable.
*/
Assignment(std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& expression);
/*!
* Creates a copy of the given assignment and performs the provided renaming.
*
* @param oldAssignment The assignment to copy.
* @param renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
* @param variableState An object knowing about the variables in the system.
*/
Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
/*!
* Retrieves the name of the variable that this assignment targets.
*
* @return The name of the variable that this assignment targets.
*/
std::string const& getVariableName() const;
/*!
* Retrieves the expression that is assigned to the variable.
*
* @return The expression that is assigned to the variable.
*/
std::shared_ptr<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 /* STORM_IR_ASSIGNMENT_H_ */

57
src/ir/BooleanVariable.cpp
View File

@ -8,35 +8,34 @@
#include <sstream>
#include "BooleanVariable.h"
#include "src/parser/prismparser/VariableState.h"
namespace storm {
namespace ir {
BooleanVariable::BooleanVariable() : Variable() {
// Nothing to do here.
}
BooleanVariable::BooleanVariable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue)
: Variable(globalIndex, localIndex, variableName, initialValue) {
// Nothing to do here.
}
BooleanVariable::BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string,uint_fast64_t> const& integerVariableToIndexMap)
: Variable(oldVariable, newName, newGlobalIndex, renaming, booleanVariableToIndexMap, integerVariableToIndexMap) {
// Nothing to do here.
}
std::string BooleanVariable::toString() const {
std::stringstream result;
result << this->getName() << ": bool";
if (this->getInitialValue() != nullptr) {
result << " init " << this->getInitialValue()->toString();
}
result << ";";
return result.str();
}
} // namespace ir
namespace ir {
BooleanVariable::BooleanVariable() : Variable() {
// Nothing to do here.
}
BooleanVariable::BooleanVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue)
: Variable(localIndex, globalIndex, variableName, initialValue) {
// Nothing to do here.
}
BooleanVariable::BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState)
: Variable(oldVariable, newName, newGlobalIndex, renaming, variableState) {
// Nothing to do here.
}
std::string BooleanVariable::toString() const {
std::stringstream result;
result << this->getName() << ": bool";
if (this->getInitialValue() != nullptr) {
result << " init " << this->getInitialValue()->toString();
}
result << ";";
return result.str();
}
} // namespace ir
} // namespace storm

94
src/ir/BooleanVariable.h
View File

@ -14,51 +14,55 @@
#include "src/ir/Variable.h"
namespace storm {
namespace ir {
/*!
* A class representing a boolean variable.
*/
class BooleanVariable : public Variable {
public:
/*!
* Default constructor. Creates a boolean variable without a name.
*/
BooleanVariable();
/*!
* Creates a boolean variable with the given name and the given initial value.
*
* @param globalIndex A globally unique index for the variable.
* @param localIndex A module-local unique index for the variable.
* @param variableName The name of the variable.
* @param initialValue The expression that defines the initial value of the variable.
*/
BooleanVariable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr));
/*!
* Creates a copy of the given boolean variable and performs the provided renaming.
*
* @param oldVariable The variable to copy.
* @param newName New name of this variable.
* @param newGlobalIndex The new global index of the variable.
* @param renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
* @param booleanVariableToIndexMap A mapping from boolean variable names to their global indices.
* @param integerVariableToIndexMap A mapping from integer variable names to their global indices.
*/
BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string,uint_fast64_t> const& integerVariableToIndexMap);
/*!
* Retrieves a string representation of this variable.
* @returns a string representation of this variable.
*/
std::string toString() const;
};
} // namespace ir
namespace parser {
namespace prism {
class VariableState;
} // namespace prismparser
} // namespace parser
namespace ir {
/*!
* A class representing a boolean variable.
*/
class BooleanVariable : public Variable {
public:
/*!
* Default constructor. Creates a boolean variable without a name.
*/
BooleanVariable();
/*!
* Creates a boolean variable with the given name and the given initial value.
*
* @param localIndex A module-local unique index for the variable.
* @param globalIndex A globally unique index for the variable.
* @param variableName The name of the variable.
* @param initialValue The expression that defines the initial value of the variable.
*/
BooleanVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr));
/*!
* Creates a copy of the given boolean variable and performs the provided renaming.
*
* @param oldVariable The variable to copy.
* @param newName New name of this variable.
* @param newGlobalIndex The new global index of the variable.
* @param renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
* @param variableState An object knowing about the variables in the system.
*/
BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
/*!
* Retrieves a string representation of this variable.
* @returns a string representation of this variable.
*/
std::string toString() const;
};
} // namespace ir
} // namespace storm
#endif /* STORM_IR_BOOLEANVARIABLE_H_ */

115
src/ir/Command.cpp
View File

@ -5,67 +5,64 @@
* Author: Christian Dehnert
*/
#include "Command.h"
#include <sstream>
#include <iostream>
namespace storm {
namespace ir {
// Initializes all members with their default constructors.
Command::Command() : actionName(), guardExpression(), updates() {
// Nothing to do here.
}
// Initializes all members according to the given values.
Command::Command(std::string const& actionName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> const& updates)
: actionName(actionName), guardExpression(guardExpression), updates(updates) {
// Nothing to do here.
}
Command::Command(Command const& oldCommand, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap)
: actionName(oldCommand.getActionName()), guardExpression(oldCommand.guardExpression->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap)) {
auto renamingPair = renaming.find(this->actionName);
if (renamingPair != renaming.end()) {
this->actionName = renamingPair->first;
}
this->updates.reserve(oldCommand.getNumberOfUpdates());
for (Update const& update : oldCommand.updates) {
this->updates.emplace_back(update, renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
}
}
std::string const& Command::getActionName() const {
return this->actionName;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Command::getGuard() const {
return guardExpression;
}
uint_fast64_t Command::getNumberOfUpdates() const {
return this->updates.size();
}
storm::ir::Update const& Command::getUpdate(uint_fast64_t index) const {
return this->updates[index];
}
std::string Command::toString() const {
std::stringstream result;
result << "[" << actionName << "] " << guardExpression->toString() << " -> ";
for (uint_fast64_t i = 0; i < updates.size(); ++i) {
result << updates[i].toString();
if (i < updates.size() - 1) {
result << " + ";
}
}
result << ";";
return result.str();
}
} // namespace ir
#include "Command.h"
#include "src/parser/prismparser/VariableState.h"
namespace storm {
namespace ir {
Command::Command() : actionName(), guardExpression(), updates() {
// Nothing to do here.
}
Command::Command(std::string const& actionName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> const& updates)
: actionName(actionName), guardExpression(guardExpression), updates(updates) {
// Nothing to do here.
}
Command::Command(Command const& oldCommand, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState)
: actionName(oldCommand.getActionName()), guardExpression(oldCommand.guardExpression->clone(renaming, variableState)) {
auto renamingPair = renaming.find(this->actionName);
if (renamingPair != renaming.end()) {
this->actionName = renamingPair->first;
}
this->updates.reserve(oldCommand.getNumberOfUpdates());
for (Update const& update : oldCommand.updates) {
this->updates.emplace_back(update, renaming, variableState);
}
}
std::string const& Command::getActionName() const {
return this->actionName;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Command::getGuard() const {
return guardExpression;
}
uint_fast64_t Command::getNumberOfUpdates() const {
return this->updates.size();
}
storm::ir::Update const& Command::getUpdate(uint_fast64_t index) const {
return this->updates[index];
}
std::string Command::toString() const {
std::stringstream result;
result << "[" << actionName << "] " << guardExpression->toString() << " -> ";
for (uint_fast64_t i = 0; i < updates.size(); ++i) {
result << updates[i].toString();
if (i < updates.size() - 1) {
result << " + ";
}
}
result << ";";
return result.str();
}
} // namespace ir
} // namespace storm

166
src/ir/Command.h
View File

@ -16,87 +16,91 @@
#include "Update.h"
namespace storm {
namespace ir {
/*!
* A class representing a command.
*/
class Command {
public:
/*!
* Default constructor. Creates a a command without name, guard and updates.
*/
Command();
/*!
* Creates a command with the given name, guard and updates.
*
* @param actionName The action name of the command.
* @param guardExpression the expression that defines the guard of the command.
* @param updates A list of updates that is associated with this command.
*/
Command(std::string const& actionName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> const& updates);
/*!
* Creates a copy of the given command and performs the provided renaming.
*
* @param oldCommand The command to copy.
* @param renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
* @param booleanVariableToIndexMap A mapping from boolean variable names to their global indices.
* @param integerVariableToIndexMap A mapping from integer variable names to their global indices.
*/
Command(Command const& oldCommand, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap);
/*!
* Retrieves the action name of this command.
*
* @return The action name of this command.
*/
std::string const& getActionName() const;
/*!
* Retrieves a reference to the guard of the command.
*
* @return A reference to the guard of the command.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> const& getGuard() const;
/*!
* Retrieves the number of updates associated with this command.
*
* @return The number of updates associated with this command.
*/
uint_fast64_t getNumberOfUpdates() const;
/*!
* Retrieves a reference to the update with the given index.
*
* @return A reference to the update with the given index.
*/
storm::ir::Update const& getUpdate(uint_fast64_t index) const;
/*!
* Retrieves a string representation of this command.
*
* @return A string representation of this command.
*/
std::string toString() const;
private:
// The name of the command.
std::string actionName;
// The expression that defines the guard of the command.
std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression;
// The list of updates of the command.
std::vector<storm::ir::Update> updates;
};
} // namespace ir
namespace parser {
namespace prism {
class VariableState;
} // namespace prismparser
} // namespace parser
namespace ir {
/*!
* A class representing a command.
*/
class Command {
public:
/*!
* Default constructor. Creates a a command without name, guard and updates.
*/
Command();
/*!
* Creates a command with the given name, guard and updates.
*
* @param actionName The action name of the command.
* @param guardExpression the expression that defines the guard of the command.
* @param updates A list of updates that is associated with this command.
*/
Command(std::string const& actionName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> const& updates);
/*!
* Creates a copy of the given command and performs the provided renaming.
*
* @param oldCommand The command to copy.
* @param renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
* @param variableState An object knowing about the variables in the system.
*/
Command(Command const& oldCommand, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
/*!
* Retrieves the action name of this command.
*
* @return The action name of this command.
*/
std::string const& getActionName() const;
/*!
* Retrieves a reference to the guard of the command.
*
* @return A reference to the guard of the command.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> const& getGuard() const;
/*!
* Retrieves the number of updates associated with this command.
*
* @return The number of updates associated with this command.
*/
uint_fast64_t getNumberOfUpdates() const;
/*!
* Retrieves a reference to the update with the given index.
*
* @return A reference to the update with the given index.
*/
storm::ir::Update const& getUpdate(uint_fast64_t index) const;
/*!
* Retrieves a string representation of this command.
*
* @return A string representation of this command.
*/
std::string toString() const;
private:
// The name of the command.
std::string actionName;
// The expression that defines the guard of the command.
std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression;
// The list of updates of the command.
std::vector<storm::ir::Update> updates;
};
} // namespace ir
} // namespace storm
#endif /* STORM_IR_COMMAND_H_ */

77
src/ir/IntegerVariable.cpp
View File

@ -9,44 +9,45 @@
#include <iostream>
#include "IntegerVariable.h"
#include "src/parser/prismparser/VariableState.h"
namespace storm {
namespace ir {
IntegerVariable::IntegerVariable() : lowerBound(), upperBound() {
// Nothing to do here.
}
IntegerVariable::IntegerVariable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue)
: Variable(globalIndex, localIndex, variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) {
if (this->getInitialValue() == nullptr) {
this->setInitialValue(lowerBound);
}
}
IntegerVariable::IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap)
: Variable(oldVariable, newName, newGlobalIndex, renaming, booleanVariableToIndexMap, integerVariableToIndexMap), lowerBound(oldVariable.lowerBound->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap)), upperBound(oldVariable.upperBound->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap)) {
}
std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getLowerBound() const {
return this->lowerBound;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getUpperBound() const {
return this->upperBound;
}
std::string IntegerVariable::toString() const {
std::stringstream result;
result << this->getName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]";
if (this->getInitialValue() != nullptr) {
result << " init " + this->getInitialValue()->toString();
}
result << ";";
return result.str();
}
} // namespace ir
namespace ir {
IntegerVariable::IntegerVariable() : lowerBound(), upperBound() {
// Nothing to do here.
}
IntegerVariable::IntegerVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue)
: Variable(localIndex, globalIndex, variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) {
if (this->getInitialValue() == nullptr) {
this->setInitialValue(lowerBound);
}
}
IntegerVariable::IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState)
: Variable(oldVariable, newName, newGlobalIndex, renaming, variableState), lowerBound(oldVariable.lowerBound->clone(renaming, variableState)), upperBound(oldVariable.upperBound->clone(renaming, variableState)) {
}
std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getLowerBound() const {
return this->lowerBound;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getUpperBound() const {
return this->upperBound;
}
std::string IntegerVariable::toString() const {
std::stringstream result;
result << this->getName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]";
if (this->getInitialValue() != nullptr) {
result << " init " + this->getInitialValue()->toString();
}
result << ";";
return result.str();
}
} // namespace ir
} // namespace storm

136
src/ir/IntegerVariable.h
View File

@ -14,72 +14,76 @@
#include "expressions/BaseExpression.h"
namespace storm {
namespace ir {
/*!
* A class representing an integer variable.
*/
class IntegerVariable : public Variable {
public:
/*!
* Default constructor. Creates an integer variable without a name and lower and upper bounds.
*/
IntegerVariable();
/*!
* Creates a boolean variable with the given name and the given initial value.
*
* @param globalIndex A globally unique index for the variable.
* @param localIndex A module-local unique index for the variable.
* @param variableName The name of the variable.
* @param lowerBound the lower bound of the domain of the variable.
* @param upperBound the upper bound of the domain of the variable.
* @param initialValue the expression that defines the initial value of the variable.
*/
IntegerVariable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string const& variableName, std::shared_ptr<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>(nullptr));
/*!
* Creates a copy of the given integer variable and performs the provided renaming.
*
* @param oldVariable The variable to copy.
* @param newName New name of this variable.
* @param newGlobalIndex The new global index of the variable.
* @param renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
* @param booleanVariableToIndexMap A mapping from boolean variable names to their global indices.
* @param integerVariableToIndexMap A mapping from integer variable names to their global indices.
*/
IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap);
/*!
* Retrieves the lower bound for this integer variable.
* @returns the lower bound for this integer variable.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> getLowerBound() const;
/*!
* Retrieves the upper bound for this integer variable.
* @returns the upper bound for this integer variable.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> getUpperBound() const;
/*!
* Retrieves a string representation of this variable.
* @returns a string representation of this variable.
*/
std::string toString() const;
private:
// The lower bound of the domain of the variable.
std::shared_ptr<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 parser {
namespace prism {
class VariableState;
} // namespace prismparser
} // namespace parser
namespace ir {
/*!
* A class representing an integer variable.
*/
class IntegerVariable : public Variable {
public:
/*!
* Default constructor. Creates an integer variable without a name and lower and upper bounds.
*/
IntegerVariable();
/*!
* Creates a boolean variable with the given name and the given initial value.
*
* @param localIndex A module-local unique index for the variable.
* @param globalIndex A globally unique index for the variable.
* @param variableName The name of the variable.
* @param lowerBound the lower bound of the domain of the variable.
* @param upperBound the upper bound of the domain of the variable.
* @param initialValue the expression that defines the initial value of the variable.
*/
IntegerVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr<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>(nullptr));
/*!
* Creates a copy of the given integer variable and performs the provided renaming.
*
* @param oldVariable The variable to copy.
* @param newName New name of this variable.
* @param newGlobalIndex The new global index of the variable.
* @param renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
* @param variableState An object knowing about the variables in the system.
*/
IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
/*!
* Retrieves the lower bound for this integer variable.
* @returns the lower bound for this integer variable.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> getLowerBound() const;
/*!
* Retrieves the upper bound for this integer variable.
* @returns the upper bound for this integer variable.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> getUpperBound() const;
/*!
* Retrieves a string representation of this variable.
* @returns a string representation of this variable.
*/
std::string toString() const;
private:
// The lower bound of the domain of the variable.
std::shared_ptr<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 /* STORM_IR_INTEGERVARIABLE_H_ */

306
src/ir/Module.cpp
View File

@ -18,161 +18,153 @@
extern log4cplus::Logger logger;
namespace storm {
namespace ir {
Module::Module() : moduleName(), booleanVariables(), integerVariables(), booleanVariableToLocalIndexMap(),
integerVariableToLocalIndexMap(), commands(), actions(), actionsToCommandIndexMap() {
// Nothing to do here.
}
Module::Module(std::string const& moduleName,
std::vector<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.
this->collectActions();
}
Module::Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap, parser::prismparser::VariableState const& variableState)
: moduleName(newModuleName), booleanVariableToLocalIndexMap(oldModule.booleanVariableToLocalIndexMap), integerVariableToLocalIndexMap(oldModule.integerVariableToLocalIndexMap) {
LOG4CPLUS_TRACE(logger, "Start renaming " << oldModule.getName() << " to " << moduleName << ".");
// Iterate over boolean variables and rename them. If a variable was not renamed, this is an error and an exception
// is thrown.
this->booleanVariables.reserve(oldModule.getNumberOfBooleanVariables());
for (BooleanVariable const& booleanVariable : oldModule.booleanVariables) {
auto renamingPair = renaming.find(booleanVariable.getName());
if (renamingPair == renaming.end()) {
LOG4CPLUS_ERROR(logger, "Boolean variable " << moduleName << "." << booleanVariable.getName() << " was not renamed.");
throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << moduleName << "." << booleanVariable.getName() << " was not renamed.";
} else {
this->booleanVariables.emplace_back(booleanVariable, renamingPair->second, variableState->getNextGlobalBooleanVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
variableState.addBooleanVariable(renamingPair->second);
}
}
// Now do the same for the integer variables.
this->integerVariables.reserve(oldModule.getNumberOfIntegerVariables());
for (IntegerVariable const& integerVariable : oldModule.integerVariables) {
auto renamingPair = renaming.find(integerVariable.getName());
if (renamingPair == renaming.end()) {
LOG4CPLUS_ERROR(logger, "Integer variable " << moduleName << "." << integerVariable.getName() << " was not renamed.");
throw storm::exceptions::InvalidArgumentException() << "Integer variable " << moduleName << "." << integerVariable.getName() << " was not renamed.";
} else {
this->integerVariables.emplace_back(integerVariable, renamingPair->second, variableState->getNextGlobalIntegerVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
variableState.addIntegerVariable(renamingPair->second);
}
}
// Now we are ready to clone all commands and rename them if requested.
this->commands.reserve(oldModule.getNumberOfCommands());
for (Command const& command : oldModule.commands) {
this->commands.emplace_back(command, renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
}
this->collectActions();
LOG4CPLUS_TRACE(logger, "Finished renaming...");
}
// Return the number of boolean variables.
uint_fast64_t Module::getNumberOfBooleanVariables() const {
return this->booleanVariables.size();
}
// Return the requested boolean variable.
storm::ir::BooleanVariable const& Module::getBooleanVariable(uint_fast64_t index) const {
return this->booleanVariables[index];
}
// Return the number of integer variables.
uint_fast64_t Module::getNumberOfIntegerVariables() const {
return this->integerVariables.size();
}
// Return the requested integer variable.
storm::ir::IntegerVariable const& Module::getIntegerVariable(uint_fast64_t index) const {
return this->integerVariables[index];
}
// Return the number of commands.
uint_fast64_t Module::getNumberOfCommands() const {
return this->commands.size();
}
// Return the index of the variable if it exists and throw exception otherwise.
uint_fast64_t Module::getBooleanVariableIndex(std::string const& variableName) const {
auto it = booleanVariableToLocalIndexMap.find(variableName);
if (it != booleanVariableToLocalIndexMap.end()) {
return it->second;
}
LOG4CPLUS_ERROR(logger, "Cannot retrieve index of unknown boolean variable " << variableName << ".");
throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown boolean variable " << variableName << ".";
}
uint_fast64_t Module::getIntegerVariableIndex(std::string const& variableName) const {
auto it = integerVariableToLocalIndexMap.find(variableName);
if (it != integerVariableToLocalIndexMap.end()) {
return it->second;
}
LOG4CPLUS_ERROR(logger, "Cannot retrieve index of unknown integer variable " << variableName << ".");
throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown integer variable " << variableName << ".";
}
storm::ir::Command const& Module::getCommand(uint_fast64_t index) const {
return this->commands[index];
}
std::string const& Module::getName() const {
return this->moduleName;
}
std::string Module::toString() const {
std::stringstream result;
result << "module " << moduleName << std::endl;
for (auto variable : booleanVariables) {
result << "\t" << variable.toString() << std::endl;
}
for (auto variable : integerVariables) {
result << "\t" << variable.toString() << std::endl;
}
for (auto command : commands) {
result << "\t" << command.toString() << std::endl;
}
result << "endmodule" << std::endl;
return result.str();
}
std::set<std::string> const& Module::getActions() const {
return this->actions;
}
std::set<uint_fast64_t> const& Module::getCommandsByAction(std::string const& action) const {
auto actionsCommandSetPair = this->actionsToCommandIndexMap.find(action);
if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) {
return actionsCommandSetPair->second;
}
LOG4CPLUS_ERROR(logger, "Action name '" << action << "' does not exist in module.");
throw storm::exceptions::OutOfRangeException() << "Action name '" << action << "' does not exist in module.";
}
void Module::collectActions() {
for (unsigned int id = 0; id < this->commands.size(); id++) {
std::string const& action = this->commands[id].getActionName();
if (action != "") {
if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) {
this->actionsToCommandIndexMap.emplace(action, std::set<uint_fast64_t>());
}
this->actionsToCommandIndexMap[action].insert(id);
this->actions.insert(action);
}
}
}
} // namespace ir
namespace ir {
Module::Module() : moduleName(), booleanVariables(), integerVariables(), booleanVariableToLocalIndexMap(),
integerVariableToLocalIndexMap(), commands(), actions(), actionsToCommandIndexMap() {
// Nothing to do here.
}
Module::Module(std::string const& moduleName,
std::vector<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.
this->collectActions();
}
Module::Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState)
: moduleName(newModuleName), booleanVariableToLocalIndexMap(oldModule.booleanVariableToLocalIndexMap), integerVariableToLocalIndexMap(oldModule.integerVariableToLocalIndexMap) {
LOG4CPLUS_TRACE(logger, "Start renaming " << oldModule.getName() << " to " << moduleName << ".");
// Iterate over boolean variables and rename them. If a variable was not renamed, this is an error and an exception
// is thrown.
this->booleanVariables.reserve(oldModule.getNumberOfBooleanVariables());
for (BooleanVariable const& booleanVariable : oldModule.booleanVariables) {
auto renamingPair = renaming.find(booleanVariable.getName());
if (renamingPair == renaming.end()) {
LOG4CPLUS_ERROR(logger, "Boolean variable " << moduleName << "." << booleanVariable.getName() << " was not renamed.");
throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << moduleName << "." << booleanVariable.getName() << " was not renamed.";
} else {
this->booleanVariables.emplace_back(booleanVariable, renamingPair->second, variableState.getNextGlobalBooleanVariableIndex(), renaming, variableState);
variableState.addBooleanVariable(renamingPair->second);
}
}
// Now do the same for the integer variables.
this->integerVariables.reserve(oldModule.getNumberOfIntegerVariables());
for (IntegerVariable const& integerVariable : oldModule.integerVariables) {
auto renamingPair = renaming.find(integerVariable.getName());
if (renamingPair == renaming.end()) {
LOG4CPLUS_ERROR(logger, "Integer variable " << moduleName << "." << integerVariable.getName() << " was not renamed.");
throw storm::exceptions::InvalidArgumentException() << "Integer variable " << moduleName << "." << integerVariable.getName() << " was not renamed.";
} else {
this->integerVariables.emplace_back(integerVariable, renamingPair->second, variableState.getNextGlobalIntegerVariableIndex(), renaming, variableState);
variableState.addIntegerVariable(renamingPair->second);
}
}
// Now we are ready to clone all commands and rename them if requested.
this->commands.reserve(oldModule.getNumberOfCommands());
for (Command const& command : oldModule.commands) {
this->commands.emplace_back(command, renaming, variableState);
}
this->collectActions();
LOG4CPLUS_TRACE(logger, "Finished renaming...");
}
uint_fast64_t Module::getNumberOfBooleanVariables() const {
return this->booleanVariables.size();
}
storm::ir::BooleanVariable const& Module::getBooleanVariable(uint_fast64_t index) const {
return this->booleanVariables[index];
}
uint_fast64_t Module::getNumberOfIntegerVariables() const {
return this->integerVariables.size();
}
storm::ir::IntegerVariable const& Module::getIntegerVariable(uint_fast64_t index) const {
return this->integerVariables[index];
}
uint_fast64_t Module::getNumberOfCommands() const {
return this->commands.size();
}
uint_fast64_t Module::getBooleanVariableIndex(std::string const& variableName) const {
auto it = booleanVariableToLocalIndexMap.find(variableName);
if (it != booleanVariableToLocalIndexMap.end()) {
return it->second;
}
LOG4CPLUS_ERROR(logger, "Cannot retrieve index of unknown boolean variable " << variableName << ".");
throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown boolean variable " << variableName << ".";
}
uint_fast64_t Module::getIntegerVariableIndex(std::string const& variableName) const {
auto it = integerVariableToLocalIndexMap.find(variableName);
if (it != integerVariableToLocalIndexMap.end()) {
return it->second;
}
LOG4CPLUS_ERROR(logger, "Cannot retrieve index of unknown integer variable " << variableName << ".");
throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown integer variable " << variableName << ".";
}
storm::ir::Command const& Module::getCommand(uint_fast64_t index) const {
return this->commands[index];
}
std::string const& Module::getName() const {
return this->moduleName;
}
std::string Module::toString() const {
std::stringstream result;
result << "module " << moduleName << std::endl;
for (auto variable : booleanVariables) {
result << "\t" << variable.toString() << std::endl;
}
for (auto variable : integerVariables) {
result << "\t" << variable.toString() << std::endl;
}
for (auto command : commands) {
result << "\t" << command.toString() << std::endl;
}
result << "endmodule" << std::endl;
return result.str();
}
std::set<std::string> const& Module::getActions() const {
return this->actions;
}
std::set<uint_fast64_t> const& Module::getCommandsByAction(std::string const& action) const {
auto actionsCommandSetPair = this->actionsToCommandIndexMap.find(action);
if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) {
return actionsCommandSetPair->second;
}
LOG4CPLUS_ERROR(logger, "Action name '" << action << "' does not exist in module.");
throw storm::exceptions::OutOfRangeException() << "Action name '" << action << "' does not exist in module.";
}
void Module::collectActions() {
for (unsigned int id = 0; id < this->commands.size(); id++) {
std::string const& action = this->commands[id].getActionName();
if (action != "") {
if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) {
this->actionsToCommandIndexMap.emplace(action, std::set<uint_fast64_t>());
}
this->actionsToCommandIndexMap[action].insert(id);
this->actions.insert(action);
}
}
}
} // namespace ir
} // namespace storm

338
src/ir/Module.h
View File

@ -20,179 +20,175 @@
#include "expressions/VariableExpression.h"
namespace storm {
namespace parser {
namespace prismparser {
class VariableState;
} // namespace prismparser
} // namespace parser
namespace ir {
/*!
* A class representing a module.
*/
class Module {
public:
/*!
* Default constructor. Creates an empty module.
*/
Module();
/*!
* Creates a module with the given name, variables and commands.
*
* @param moduleName The name of the module.
* @param booleanVariables The boolean variables defined by the module.
* @param integerVariables The integer variables defined by the module.
* @param booleanVariableToIndexMap A mapping of boolean variables to global (i.e. program-wide) indices.
* @param integerVariableToIndexMap A mapping of integer variables to global (i.e. program-wide) indices.
* @param commands The commands of the module.
*/
Module(std::string const& moduleName, std::vector<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);
typedef uint_fast64_t (*addIntegerVariablePtr)(std::string const& name, std::shared_ptr<storm::ir::expressions::BaseExpression> const& lower, std::shared_ptr<storm::ir::expressions::BaseExpression> const upper, std::shared_ptr<storm::ir::expressions::BaseExpression> const& init);
typedef uint_fast64_t (*addBooleanVariablePtr)(std::string const& name, std::shared_ptr<storm::ir::expressions::BaseExpression> const& init);
/*!
* Special copy constructor, implementing the module renaming functionality.
* This will create a new module having all identifiers renamed according to the given map.
*
* @param oldModule The module to be copied.
* @param newModuleName The name of the new module.
* @param renaming A mapping of identifiers to the new identifiers they are to be replaced with.
* @param booleanVariableToIndexMap A mapping from boolean variable names to their global indices.
* @param integerVariableToIndexMap A mapping from integer variable names to their global indices.
* @param adder An instance of the VariableAdder interface that keeps track of all the variables in the probabilistic
* program.
*/
Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap, parser::prismparser::VariableState const& variableState);
/*!
* Retrieves the number of boolean variables in the module.
*
* @return the number of boolean variables in the module.
*/
uint_fast64_t getNumberOfBooleanVariables() const;
/*!
* Retrieves a reference to the boolean variable with the given index.
*
* @return A reference to the boolean variable with the given index.
*/
storm::ir::BooleanVariable const& getBooleanVariable(uint_fast64_t index) const;
/*!
* Retrieves the number of integer variables in the module.
*
* @return The number of integer variables in the module.
*/
uint_fast64_t getNumberOfIntegerVariables() const;
/*!
* Retrieves a reference to the integer variable with the given index.
*
* @return A reference to the integer variable with the given index.
*/
storm::ir::IntegerVariable const& getIntegerVariable(uint_fast64_t index) const;
/*!
* Retrieves the number of commands of this module.
*
* @return the number of commands of this module.
*/
uint_fast64_t getNumberOfCommands() const;
/*!
* Retrieves the index of the boolean variable with the given name.
*
* @param variableName The name of the boolean variable whose index to retrieve.
* @return The index of the boolean variable with the given name.
*/
uint_fast64_t getBooleanVariableIndex(std::string const& variableName) const;
/*!
* Retrieves the index of the integer variable with the given name.
*
* @param variableName The name of the integer variable whose index to retrieve.
* @return The index of the integer variable with the given name.
*/
uint_fast64_t getIntegerVariableIndex(std::string const& variableName) const;
/*!
* Retrieves a reference to the command with the given index.
*
* @return A reference to the command with the given index.
*/
storm::ir::Command const& getCommand(uint_fast64_t index) const;
/*!
* Retrieves the name of the module.
*
* @return The name of the module.
*/
std::string const& getName() const;
namespace parser {
namespace prism {
class VariableState;
} // namespace prismparser
} // namespace parser
/*!
* Retrieves a string representation of this module.
*
* @return a string representation of this module.
*/
std::string toString() const;
/*!
* Retrieves the set of actions present in this module.
*
* @return the set of actions present in this module.
*/
std::set<std::string> const& getActions() const;
/*!
* Retrieves the indices of all commands within this module that are labelled by the given action.
*
* @param action The action with which the commands have to be labelled.
* @return A set of indices of commands that are labelled with the given action.
*/
std::set<uint_fast64_t> const& getCommandsByAction(std::string const& action) const;
private:
/*!
* Computes the locally maintained mappings for fast data retrieval.
*/
void collectActions();
// The name of the module.
std::string moduleName;
// A list of boolean variables.
std::vector<storm::ir::BooleanVariable> booleanVariables;
// A list of integer variables.
std::vector<storm::ir::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.
std::vector<storm::ir::Command> commands;
// The set of actions present in this module.
std::set<std::string> actions;
// A map of actions to the set of commands labeled with this action.
std::map<std::string, std::set<uint_fast64_t>> actionsToCommandIndexMap;
};
} // namespace ir
namespace ir {
/*!
* A class representing a module.
*/
class Module {
public:
/*!
* Default constructor. Creates an empty module.
*/
Module();
/*!
* Creates a module with the given name, variables and commands.
*
* @param moduleName The name of the module.
* @param booleanVariables The boolean variables defined by the module.
* @param integerVariables The integer variables defined by the module.
* @param booleanVariableToLocalIndexMap A mapping of boolean variables to global (i.e. module-local) indices.
* @param integerVariableToLocalIndexMap A mapping of integer variables to global (i.e. module-local) indices.
* @param commands The commands of the module.
*/
Module(std::string const& moduleName, std::vector<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);
typedef uint_fast64_t (*addIntegerVariablePtr)(std::string const& name, std::shared_ptr<storm::ir::expressions::BaseExpression> const& lower, std::shared_ptr<storm::ir::expressions::BaseExpression> const upper, std::shared_ptr<storm::ir::expressions::BaseExpression> const& init);
typedef uint_fast64_t (*addBooleanVariablePtr)(std::string const& name, std::shared_ptr<storm::ir::expressions::BaseExpression> const& init);
/*!
* Special copy constructor, implementing the module renaming functionality.
* This will create a new module having all identifiers renamed according to the given map.
*
* @param oldModule The module to be copied.
* @param newModuleName The name of the new module.
* @param renaming A mapping of identifiers to the new identifiers they are to be replaced with.
* @param variableState An object knowing about the variables in the system.
*/
Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState);
/*!
* Retrieves the number of boolean variables in the module.
*
* @return the number of boolean variables in the module.
*/
uint_fast64_t getNumberOfBooleanVariables() const;
/*!
* Retrieves a reference to the boolean variable with the given index.
*
* @return A reference to the boolean variable with the given index.
*/
storm::ir::BooleanVariable const& getBooleanVariable(uint_fast64_t index) const;
/*!
* Retrieves the number of integer variables in the module.
*
* @return The number of integer variables in the module.
*/
uint_fast64_t getNumberOfIntegerVariables() const;
/*!
* Retrieves a reference to the integer variable with the given index.
*
* @return A reference to the integer variable with the given index.
*/
storm::ir::IntegerVariable const& getIntegerVariable(uint_fast64_t index) const;
/*!
* Retrieves the number of commands of this module.
*
* @return the number of commands of this module.
*/
uint_fast64_t getNumberOfCommands() const;
/*!
* Retrieves the index of the boolean variable with the given name.
*
* @param variableName The name of the boolean variable whose index to retrieve.
* @return The index of the boolean variable with the given name.
*/
uint_fast64_t getBooleanVariableIndex(std::string const& variableName) const;
/*!
* Retrieves the index of the integer variable with the given name.
*
* @param variableName The name of the integer variable whose index to retrieve.
* @return The index of the integer variable with the given name.
*/
uint_fast64_t getIntegerVariableIndex(std::string const& variableName) const;
/*!
* Retrieves a reference to the command with the given index.
*
* @return A reference to the command with the given index.
*/
storm::ir::Command const& getCommand(uint_fast64_t index) const;
/*!
* Retrieves the name of the module.
*
* @return The name of the module.
*/
std::string const& getName() const;
/*!
* Retrieves a string representation of this module.
*
* @return a string representation of this module.
*/
std::string toString() const;
/*!
* Retrieves the set of actions present in this module.
*
* @return the set of actions present in this module.
*/
std::set<std::string> const& getActions() const;
/*!
* Retrieves the indices of all commands within this module that are labelled by the given action.
*
* @param action The action with which the commands have to be labelled.
* @return A set of indices of commands that are labelled with the given action.
*/
std::set<uint_fast64_t> const& getCommandsByAction(std::string const& action) const;
private:
/*!
* Computes the locally maintained mappings for fast data retrieval.
*/
void collectActions();
// The name of the module.
std::string moduleName;
// A list of boolean variables.
std::vector<storm::ir::BooleanVariable> booleanVariables;
// A list of integer variables.
std::vector<storm::ir::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.
std::vector<storm::ir::Command> commands;
// The set of actions present in this module.
std::set<std::string> actions;
// A map of actions to the set of commands labeled with this action.
std::map<std::string, std::set<uint_fast64_t>> actionsToCommandIndexMap;
};
} // namespace ir
} // namespace storm
#endif /* STORM_IR_MODULE_H_ */

192
src/ir/Program.cpp
View File

@ -17,102 +17,100 @@
extern log4cplus::Logger logger;
namespace storm {
namespace ir {
Program::Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards(), actions(), actionsToModuleIndexMap() {
// Nothing to do here.
}
Program::Program(ModelType modelType, std::map<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), actionsToModuleIndexMap() {
// Now build the mapping from action names to module indices so that the lookup can later be performed quickly.
for (unsigned int moduleId = 0; moduleId < this->modules.size(); moduleId++) {
for (auto const& action : this->modules[moduleId].getActions()) {
if (this->actionsToModuleIndexMap.count(action) == 0) {
this->actionsToModuleIndexMap[action] = std::set<uint_fast64_t>();
}
this->actionsToModuleIndexMap[action].insert(moduleId);
this->actions.insert(action);
namespace ir {
Program::Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards(), actions(), actionsToModuleIndexMap() {
// Nothing to do here.
}
}
}
Program::ModelType Program::getModelType() const {
return modelType;
}
std::string Program::toString() const {
std::stringstream result;
switch (modelType) {
case UNDEFINED: result << "undefined"; break;
case DTMC: result << "dtmc"; break;
case CTMC: result << "ctmc"; break;
case MDP: result << "mdp"; break;
case CTMDP: result << "ctmdp"; break;
}
result << std::endl;
for (auto const& element : booleanUndefinedConstantExpressions) {
result << "const bool " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl;
}
for (auto const& element : integerUndefinedConstantExpressions) {
result << "const int " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl;
}
for (auto const& element : doubleUndefinedConstantExpressions) {
result << "const double " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl;
}
result << std::endl;
for (auto const& module : modules) {
result << module.toString() << std::endl;
}
for (auto const& rewardModel : rewards) {
result << rewardModel.first << ": " << rewardModel.second.toString() << std::endl;
}
for (auto const& label : labels) {
result << "label " << label.first << " = " << label.second->toString() <<";" << std::endl;
}
return result.str();
}
uint_fast64_t Program::getNumberOfModules() const {
return this->modules.size();
}
storm::ir::Module const& Program::getModule(uint_fast64_t index) const {
return this->modules[index];
}
std::set<std::string> const& Program::getActions() const {
return this->actions;
}
std::set<uint_fast64_t> const& Program::getModulesByAction(std::string const& action) const {
auto actionModuleSetPair = this->actionsToModuleIndexMap.find(action);
if (actionModuleSetPair == this->actionsToModuleIndexMap.end()) {
LOG4CPLUS_ERROR(logger, "Action name '" << action << "' does not exist.");
throw storm::exceptions::OutOfRangeException() << "Action name '" << action << "' does not exist.";
}
return actionModuleSetPair->second;
}
storm::ir::RewardModel const& Program::getRewardModel(std::string const& name) const {
auto nameRewardModelPair = this->rewards.find(name);
if (nameRewardModelPair == this->rewards.end()) {
LOG4CPLUS_ERROR(logger, "Reward model '" << name << "' does not exist.");
throw storm::exceptions::OutOfRangeException() << "Reward model '" << name << "' does not exist.";
}
return nameRewardModelPair->second;
}
std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& Program::getLabels() const {
return this->labels;
}
} // namespace ir
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), actionsToModuleIndexMap() {
// Now build the mapping from action names to module indices so that the lookup can later be performed quickly.
for (unsigned int moduleId = 0; moduleId < this->modules.size(); moduleId++) {
for (auto const& action : this->modules[moduleId].getActions()) {
if (this->actionsToModuleIndexMap.count(action) == 0) {
this->actionsToModuleIndexMap[action] = std::set<uint_fast64_t>();
}
this->actionsToModuleIndexMap[action].insert(moduleId);
this->actions.insert(action);
}
}
}
Program::ModelType Program::getModelType() const {
return modelType;
}
std::string Program::toString() const {
std::stringstream result;
switch (modelType) {
case UNDEFINED: result << "undefined"; break;
case DTMC: result << "dtmc"; break;
case CTMC: result << "ctmc"; break;
case MDP: result << "mdp"; break;
case CTMDP: result << "ctmdp"; break;
}
result << std::endl;
for (auto const& element : booleanUndefinedConstantExpressions) {
result << "const bool " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl;
}
for (auto const& element : integerUndefinedConstantExpressions) {
result << "const int " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl;
}
for (auto const& element : doubleUndefinedConstantExpressions) {
result << "const double " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl;
}
result << std::endl;
for (auto const& module : modules) {
result << module.toString() << std::endl;
}
for (auto const& rewardModel : rewards) {
result << rewardModel.first << ": " << rewardModel.second.toString() << std::endl;
}
for (auto const& label : labels) {
result << "label " << label.first << " = " << label.second->toString() <<";" << std::endl;
}
return result.str();
}
uint_fast64_t Program::getNumberOfModules() const {
return this->modules.size();
}
storm::ir::Module const& Program::getModule(uint_fast64_t index) const {
return this->modules[index];
}
std::set<std::string> const& Program::getActions() const {
return this->actions;
}
std::set<uint_fast64_t> const& Program::getModulesByAction(std::string const& action) const {
auto actionModuleSetPair = this->actionsToModuleIndexMap.find(action);
if (actionModuleSetPair == this->actionsToModuleIndexMap.end()) {
LOG4CPLUS_ERROR(logger, "Action name '" << action << "' does not exist.");
throw storm::exceptions::OutOfRangeException() << "Action name '" << action << "' does not exist.";
}
return actionModuleSetPair->second;
}
storm::ir::RewardModel const& Program::getRewardModel(std::string const& name) const {
auto nameRewardModelPair = this->rewards.find(name);
if (nameRewardModelPair == this->rewards.end()) {
LOG4CPLUS_ERROR(logger, "Reward model '" << name << "' does not exist.");
throw storm::exceptions::OutOfRangeException() << "Reward model '" << name << "' does not exist.";
}
return nameRewardModelPair->second;
}
std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& Program::getLabels() const {
return this->labels;
}
} // namespace ir
} // namepsace storm

262
src/ir/Program.h
View File

@ -21,138 +21,136 @@
#include "RewardModel.h"
namespace storm {
namespace ir {
/*!
* A class representing a program.
*/
class Program {
public:
/*!
* An enum for the different model types.
*/
enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP};
/*!
* Default constructor. Creates an empty program.
*/
Program();
/*!
* Creates a program with the given model type, undefined constants, modules, rewards and labels.
*
* @param modelType The type of the model that this program gives rise to.
* @param booleanUndefinedConstantExpressions A map of undefined boolean constants to their
* expression nodes.
* @param integerUndefinedConstantExpressions A map of undefined integer constants to their
* expression nodes.
* @param doubleUndefinedConstantExpressions A map of undefined double constants to their
* expression nodes.
* @param modules The modules of the program.
* @param rewards The reward models of the program.
* @param labels The labels defined for this model.
*/
Program(ModelType modelType,
std::map<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 the number of modules in the program.
*
* @return The number of modules in the program.
*/
uint_fast64_t getNumberOfModules() const;
/*!
* Retrieves a reference to the module with the given index.
*
* @param index The index of the module to retrieve.
* @return The module with the given index.
*/
storm::ir::Module const& getModule(uint_fast64_t index) const;
/*!
* Retrieves the model type of the model.
*
* @return The type of the model.
*/
ModelType getModelType() const;
/*!
* Retrieves a string representation of this program.
*
* @return A string representation of this program.
*/
std::string toString() const;
/*!
* Retrieves the set of actions present in this module.
*
* @return The set of actions present in this module.
*/
std::set<std::string> const& getActions() const;
/*!
* Retrieves the indices of all modules within this program that contain commands that are labelled with the given
* action.
*
* @param action The name of the action the modules are supposed to possess.
* @return A set of indices of all matching modules.
*/
std::set<uint_fast64_t> const& getModulesByAction(std::string const& action) const;
/*!
* Retrieves the reward model with the given name.
*
* @param name The name of the reward model to return.
* @return The reward model with the given name.
*/
storm::ir::RewardModel const& getRewardModel(std::string const& name) const;
/*!
* Retrieves all labels that are defined by the probabilitic program.
*
* @return A set of labels that are defined in the program.
*/
std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& getLabels() 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 map 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;
// The set of actions present in this program.
std::set<std::string> actions;
// A map of actions to the set of modules containing commands labelled with this action.
std::map<std::string, std::set<uint_fast64_t>> actionsToModuleIndexMap;
};
} // namespace ir
namespace ir {
/*!
* A class representing a program.
*/
class Program {
public:
/*!
* An enum for the different model types.
*/
enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP};
/*!
* Default constructor. Creates an empty program.
*/
Program();
/*!
* Creates a program with the given model type, undefined constants, modules, rewards and labels.
*
* @param modelType The type of the model that this program gives rise to.
* @param booleanUndefinedConstantExpressions A map of undefined boolean constants to their
* expression nodes.
* @param integerUndefinedConstantExpressions A map of undefined integer constants to their
* expression nodes.
* @param doubleUndefinedConstantExpressions A map of undefined double constants to their
* expression nodes.
* @param modules The modules of the program.
* @param rewards The reward models of the program.
* @param labels The labels defined for this model.
*/
Program(ModelType modelType,
std::map<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 the number of modules in the program.
*
* @return The number of modules in the program.
*/
uint_fast64_t getNumberOfModules() const;
/*!
* Retrieves a reference to the module with the given index.
*
* @param index The index of the module to retrieve.
* @return The module with the given index.
*/
storm::ir::Module const& getModule(uint_fast64_t index) const;
/*!
* Retrieves the model type of the model.
*
* @return The type of the model.
*/
ModelType getModelType() const;
/*!
* Retrieves a string representation of this program.
*
* @return A string representation of this program.
*/
std::string toString() const;
/*!
* Retrieves the set of actions present in this module.
*
* @return The set of actions present in this module.
*/
std::set<std::string> const& getActions() const;
/*!
* Retrieves the indices of all modules within this program that contain commands that are labelled with the given
* action.
*
* @param action The name of the action the modules are supposed to possess.
* @return A set of indices of all matching modules.
*/
std::set<uint_fast64_t> const& getModulesByAction(std::string const& action) const;
/*!
* Retrieves the reward model with the given name.
*
* @param name The name of the reward model to return.
* @return The reward model with the given name.
*/
storm::ir::RewardModel const& getRewardModel(std::string const& name) const;
/*!
* Retrieves all labels that are defined by the probabilitic program.
*
* @return A set of labels that are defined in the program.
*/
std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& getLabels() 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 map 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;
// The set of actions present in this program.
std::set<std::string> actions;
// A map of actions to the set of modules containing commands labelled with this action.
std::map<std::string, std::set<uint_fast64_t>> actionsToModuleIndexMap;
};
} // namespace ir
} // namespace storm
#endif /* STORM_IR_PROGRAM_H_ */

82
src/ir/RewardModel.cpp
View File

@ -10,46 +10,44 @@
#include "RewardModel.h"
namespace storm {
namespace ir {
RewardModel::RewardModel() : rewardModelName(), stateRewards(), transitionRewards() {
// Nothing to do here.
}
RewardModel::RewardModel(std::string const& rewardModelName, std::vector<storm::ir::StateReward> const& stateRewards, std::vector<storm::ir::TransitionReward> const& transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) {
// Nothing to do here.
}
std::string RewardModel::toString() const {
std::stringstream result;
result << "rewards \"" << rewardModelName << "\"" << std::endl;
for (auto const& reward : stateRewards) {
result << reward.toString() << std::endl;
}
for (auto const& reward : transitionRewards) {
result << reward.toString() << std::endl;
}
result << "endrewards" << std::endl;
return result.str();
}
bool RewardModel::hasStateRewards() const {
return this->stateRewards.size() > 0;
}
std::vector<storm::ir::StateReward> const& RewardModel::getStateRewards() const {
return this->stateRewards;
}
bool RewardModel::hasTransitionRewards() const {
return this->transitionRewards.size() > 0;
}
std::vector<storm::ir::TransitionReward> const& RewardModel::getTransitionRewards() const {
return this->transitionRewards;
}
} // namespace ir
namespace ir {
RewardModel::RewardModel() : rewardModelName(), stateRewards(), transitionRewards() {
// Nothing to do here.
}
RewardModel::RewardModel(std::string const& rewardModelName, std::vector<storm::ir::StateReward> const& stateRewards, std::vector<storm::ir::TransitionReward> const& transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) {
// Nothing to do here.
}
std::string RewardModel::toString() const {
std::stringstream result;
result << "rewards \"" << rewardModelName << "\"" << std::endl;
for (auto const& reward : stateRewards) {
result << reward.toString() << std::endl;
}
for (auto const& reward : transitionRewards) {
result << reward.toString() << std::endl;
}
result << "endrewards" << std::endl;
return result.str();
}
bool RewardModel::hasStateRewards() const {
return this->stateRewards.size() > 0;
}
std::vector<storm::ir::StateReward> const& RewardModel::getStateRewards() const {
return this->stateRewards;
}
bool RewardModel::hasTransitionRewards() const {
return this->transitionRewards.size() > 0;
}
std::vector<storm::ir::TransitionReward> const& RewardModel::getTransitionRewards() const {
return this->transitionRewards;
}
} // namespace ir
} // namespace storm

138
src/ir/RewardModel.h
View File

@ -15,76 +15,74 @@
#include "TransitionReward.h"
namespace storm {
namespace ir {
/*!
* A class representing a reward model.
*/
class RewardModel {
public:
/*!
* Default constructor. Creates an empty reward model.
*/
RewardModel();
/*!
* Creates a reward module with the given name, state and transition rewards.
*
* @param rewardModelName The name of the reward model.
* @param stateRewards A vector of state-based rewards.
* @param transitionRewards A vector of transition-based rewards.
*/
RewardModel(std::string const& rewardModelName, std::vector<storm::ir::StateReward> const& stateRewards, std::vector<storm::ir::TransitionReward> const& transitionRewards);
/*!
* Retrieves a string representation of this reward model.
*
* @return a string representation of this reward model.
*/
std::string toString() const;
/*!
* Check, if there are any state rewards.
*
* @return True, iff there are any state rewards.
*/
bool hasStateRewards() const;
/*!
* Retrieves a vector of state rewards associated with this reward model.
*
* @return A vector containing the state rewards associated with this reward model.
*/
std::vector<storm::ir::StateReward> const& getStateRewards() const;
/*!
* Check, if there are any transition rewards.
*
* @return True, iff there are any transition rewards associated with this reward model.
*/
bool hasTransitionRewards() const;
/*!
* Retrieves a vector of transition rewards associated with this reward model.
*
* @return A vector of transition rewards associated with this reward model.
*/
std::vector<storm::ir::TransitionReward> const& getTransitionRewards() 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 ir {
/*!
* A class representing a reward model.
*/
class RewardModel {
public:
/*!
* Default constructor. Creates an empty reward model.
*/
RewardModel();
/*!
* Creates a reward module with the given name, state and transition rewards.
*
* @param rewardModelName The name of the reward model.
* @param stateRewards A vector of state-based rewards.
* @param transitionRewards A vector of transition-based rewards.
*/
RewardModel(std::string const& rewardModelName, std::vector<storm::ir::StateReward> const& stateRewards, std::vector<storm::ir::TransitionReward> const& transitionRewards);
/*!
* Retrieves a string representation of this reward model.
*
* @return a string representation of this reward model.
*/
std::string toString() const;
/*!
* Check, if there are any state rewards.
*
* @return True, iff there are any state rewards.
*/
bool hasStateRewards() const;
/*!
* Retrieves a vector of state rewards associated with this reward model.
*
* @return A vector containing the state rewards associated with this reward model.
*/
std::vector<storm::ir::StateReward> const& getStateRewards() const;
/*!
* Check, if there are any transition rewards.
*
* @return True, iff there are any transition rewards associated with this reward model.
*/
bool hasTransitionRewards() const;
/*!
* Retrieves a vector of transition rewards associated with this reward model.
*
* @return A vector of transition rewards associated with this reward model.
*/
std::vector<storm::ir::TransitionReward> const& getTransitionRewards() 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 /* STORM_IR_REWARDMODEL_H_ */

8
src/ir/StateReward.cpp
View File

@ -26,7 +26,15 @@ std::string StateReward::toString() const {
result << "\t" << statePredicate->toString() << ": " << rewardValue->toString() << ";";
return result.str();
}
std::shared_ptr<storm::ir::expressions::BaseExpression> StateReward::getStatePredicate() const {
return this->statePredicate;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> StateReward::getRewardValue() const {
return this->rewardValue;
}
} // namespace ir
} // namespace storm

16
src/ir/StateReward.h
View File

@ -43,7 +43,21 @@ public:
* @return A string representation of this state reward.
*/
std::string toString() const;
/*!
* Retrieves the state predicate that is associated with this state reward.
*
* @return The state predicate that is associated with this state reward.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> getStatePredicate() const;
/*!
* Retrieves the reward value associated with this state reward.
*
* @return The reward value associated with this state reward.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> getRewardValue() const;
private:
// The predicate that characterizes the states that obtain this reward.
std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate;

12
src/ir/TransitionReward.cpp
View File

@ -27,6 +27,18 @@ std::string TransitionReward::toString() const {
return result.str();
}
std::string const& TransitionReward::getActionName() const {
return this->commandName;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> TransitionReward::getStatePredicate() const {
return this->statePredicate;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> TransitionReward::getRewardValue() const {
return this->rewardValue;
}
} // namespace ir
} // namespace storm

21
src/ir/TransitionReward.h
View File

@ -44,6 +44,27 @@ public:
* @return A string representation of this transition reward.
*/
std::string toString() const;
/*!
* Retrieves the action name that is associated with this transition reward.
*
* @return The action name that is associated with this transition reward.
*/
std::string const& getActionName() const;
/*!
* Retrieves the state predicate that is associated with this state reward.
*
* @return The state predicate that is associated with this state reward.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> getStatePredicate() const;
/*!
* Retrieves the reward value associated with this state reward.
*
* @return The reward value associated with this state reward.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> getRewardValue() const;
private:
// The name of the command this transition-based reward is attached to.

184
src/ir/Update.cpp
View File

@ -8,102 +8,100 @@
#include <sstream>
#include "Update.h"
#include "src/parser/prismparser/VariableState.h"
#include "src/exceptions/OutOfRangeException.h"
namespace storm {
namespace ir {
Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignments() {
// Nothing to do here.
}
Update::Update(std::shared_ptr<storm::ir::expressions::BaseExpression> const& likelihoodExpression, std::map<std::string, storm::ir::Assignment> const& booleanAssignments, std::map<std::string, storm::ir::Assignment> const& integerAssignments)
: likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments) {
// Nothing to do here.
}
Update::Update(Update const& update, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap) {
for (auto const& variableAssignmentPair : update.booleanAssignments) {
if (renaming.count(variableAssignmentPair.first) > 0) {
this->booleanAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
} else {
this->booleanAssignments[variableAssignmentPair.first] = Assignment(variableAssignmentPair.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
}
}
for (auto const& variableAssignmentPair : update.integerAssignments) {
if (renaming.count(variableAssignmentPair.first) > 0) {
this->integerAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
} else {
this->integerAssignments[variableAssignmentPair.first] = Assignment(variableAssignmentPair.second, renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
}
}
this->likelihoodExpression = update.likelihoodExpression->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
}
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Update::getLikelihoodExpression() const {
return likelihoodExpression;
}
uint_fast64_t Update::getNumberOfBooleanAssignments() const {
return booleanAssignments.size();
}
uint_fast64_t Update::getNumberOfIntegerAssignments() const {
return integerAssignments.size();
}
std::map<std::string, storm::ir::Assignment> const& Update::getBooleanAssignments() const {
return booleanAssignments;
}
std::map<std::string, storm::ir::Assignment> const& Update::getIntegerAssignments() const {
return integerAssignments;
}
storm::ir::Assignment const& Update::getBooleanAssignment(std::string const& variableName) const {
auto variableAssignmentPair = booleanAssignments.find(variableName);
if (variableAssignmentPair == booleanAssignments.end()) {
throw storm::exceptions::OutOfRangeException() << "Cannot find boolean assignment for variable '"
namespace ir {
Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignments() {
// Nothing to do here.
}
Update::Update(std::shared_ptr<storm::ir::expressions::BaseExpression> const& likelihoodExpression, std::map<std::string, storm::ir::Assignment> const& booleanAssignments, std::map<std::string, storm::ir::Assignment> const& integerAssignments)
: likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments) {
// Nothing to do here.
}
Update::Update(Update const& update, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) {
for (auto const& variableAssignmentPair : update.booleanAssignments) {
if (renaming.count(variableAssignmentPair.first) > 0) {
this->booleanAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, variableState);
} else {
this->booleanAssignments[variableAssignmentPair.first] = Assignment(variableAssignmentPair.second, renaming, variableState);
}
}
for (auto const& variableAssignmentPair : update.integerAssignments) {
if (renaming.count(variableAssignmentPair.first) > 0) {
this->integerAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, variableState);
} else {
this->integerAssignments[variableAssignmentPair.first] = Assignment(variableAssignmentPair.second, renaming, variableState);
}
}
this->likelihoodExpression = update.likelihoodExpression->clone(renaming, variableState);
}
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Update::getLikelihoodExpression() const {
return likelihoodExpression;
}
uint_fast64_t Update::getNumberOfBooleanAssignments() const {
return booleanAssignments.size();
}
uint_fast64_t Update::getNumberOfIntegerAssignments() const {
return integerAssignments.size();
}
std::map<std::string, storm::ir::Assignment> const& Update::getBooleanAssignments() const {
return booleanAssignments;
}
std::map<std::string, storm::ir::Assignment> const& Update::getIntegerAssignments() const {
return integerAssignments;
}
storm::ir::Assignment const& Update::getBooleanAssignment(std::string const& variableName) const {
auto variableAssignmentPair = booleanAssignments.find(variableName);
if (variableAssignmentPair == booleanAssignments.end()) {
throw storm::exceptions::OutOfRangeException() << "Cannot find boolean assignment for variable '"
<< variableName << "' in update " << this->toString() << ".";
}
return variableAssignmentPair->second;
}
storm::ir::Assignment const& Update::getIntegerAssignment(std::string const& variableName) const {
auto variableAssignmentPair = integerAssignments.find(variableName);
if (variableAssignmentPair == integerAssignments.end()) {
throw storm::exceptions::OutOfRangeException() << "Cannot find integer assignment for variable '"
}
return variableAssignmentPair->second;
}
storm::ir::Assignment const& Update::getIntegerAssignment(std::string const& variableName) const {
auto variableAssignmentPair = integerAssignments.find(variableName);
if (variableAssignmentPair == integerAssignments.end()) {
throw storm::exceptions::OutOfRangeException() << "Cannot find integer assignment for variable '"
<< variableName << "' in update " << this->toString() << ".";
}
return variableAssignmentPair->second;
}
std::string Update::toString() const {
std::stringstream result;
result << likelihoodExpression->toString() << " : ";
uint_fast64_t i = 0;
for (auto const& assignment : booleanAssignments) {
result << assignment.second.toString();
if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) {
result << " & ";
}
++i;
}
i = 0;
for (auto const& assignment : integerAssignments) {
result << assignment.second.toString();
if (i < integerAssignments.size() - 1) {
result << " & ";
}
++i;
}
return result.str();
}
} // namespace ir
}
return variableAssignmentPair->second;
}
std::string Update::toString() const {
std::stringstream result;
result << likelihoodExpression->toString() << " : ";
uint_fast64_t i = 0;
for (auto const& assignment : booleanAssignments) {
result << assignment.second.toString();
if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) {
result << " & ";
}
++i;
}
i = 0;
for (auto const& assignment : integerAssignments) {
result << assignment.second.toString();
if (i < integerAssignments.size() - 1) {
result << " & ";
}
++i;
}
return result.str();
}
} // namespace ir
} // namespace storm

208
src/ir/Update.h
View File

@ -15,108 +15,112 @@
#include "Assignment.h"
namespace storm {
namespace ir {
/*!
* A class representing an update of a command.
*/
class Update {
public:
/*!
* Default constructor. Creates an empty update.
*/
Update();
/*!
* Creates an update with the given expression specifying the likelihood and the mapping of
* variable to their assignments.
*
* @param likelihoodExpression An expression specifying the likelihood of this update.
* @param assignments A map of variable names to their assignments.
*/
Update(std::shared_ptr<storm::ir::expressions::BaseExpression> const& likelihoodExpression, std::map<std::string, storm::ir::Assignment> const& booleanAssignments, std::map<std::string, storm::ir::Assignment> const& integerAssignments);
/*!
* Creates a copy of the given update and performs the provided renaming.
*
* update The update that is to be copied.
* renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
* @param booleanVariableToIndexMap A mapping from boolean variable names to their global indices.
* @param integerVariableToIndexMap A mapping from integer variable names to their global indices.
*/
Update(Update const& update, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap);
/*!
* Retrieves the expression for the likelihood of this update.
*
* @return The expression for the likelihood of this update.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> const& getLikelihoodExpression() const;
/*!
* Retrieves the number of boolean assignments associated with this update.
*
* @return The number of boolean assignments associated with this update.
*/
uint_fast64_t getNumberOfBooleanAssignments() const;
/*!
* Retrieves the number of integer assignments associated with this update.
*
* @return The number of integer assignments associated with this update.
*/
uint_fast64_t getNumberOfIntegerAssignments() const;
/*!
* Retrieves a reference to the map of boolean variable names to their respective assignments.
*
* @return A reference to the map of boolean variable names to their respective assignments.
*/
std::map<std::string, storm::ir::Assignment> const& getBooleanAssignments() const;
/*!
* Retrieves a reference to the map of integer variable names to their respective assignments.
*
* @return A reference to the map of integer variable names to their respective assignments.
*/
std::map<std::string, storm::ir::Assignment> const& getIntegerAssignments() const;
/*!
* Retrieves a reference to the assignment for the boolean variable with the given name.
*
* @return A reference to the assignment for the boolean variable with the given name.
*/
storm::ir::Assignment const& getBooleanAssignment(std::string const& variableName) const;
/*!
* Retrieves a reference to the assignment for the integer variable with the given name.
*
* @return A reference to the assignment for the integer variable with the given name.
*/
storm::ir::Assignment const& getIntegerAssignment(std::string const& variableName) const;
/*!
* Retrieves a string representation of this update.
*
* @return A string representation of this update.
*/
std::string toString() const;
private:
// An expression specifying the likelihood of taking this update.
std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression;
// A mapping of boolean variable names to their assignments in this update.
std::map<std::string, storm::ir::Assignment> booleanAssignments;
// A mapping of integer variable names to their assignments in this update.
std::map<std::string, storm::ir::Assignment> integerAssignments;
};
} // namespace ir
namespace parser {
namespace prism {
class VariableState;
} // namespace prismparser
} // namespace parser
namespace ir {
/*!
* A class representing an update of a command.
*/
class Update {
public:
/*!
* Default constructor. Creates an empty update.
*/
Update();
/*!
* Creates an update with the given expression specifying the likelihood and the mapping of
* variable to their assignments.
*
* @param likelihoodExpression An expression specifying the likelihood of this update.
* @param assignments A map of variable names to their assignments.
*/
Update(std::shared_ptr<storm::ir::expressions::BaseExpression> const& likelihoodExpression, std::map<std::string, storm::ir::Assignment> const& booleanAssignments, std::map<std::string, storm::ir::Assignment> const& integerAssignments);
/*!
* Creates a copy of the given update and performs the provided renaming.
*
* update The update that is to be copied.
* renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
* @param variableState An object knowing about the variables in the system.
*/
Update(Update const& update, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
/*!
* Retrieves the expression for the likelihood of this update.
*
* @return The expression for the likelihood of this update.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> const& getLikelihoodExpression() const;
/*!
* Retrieves the number of boolean assignments associated with this update.
*
* @return The number of boolean assignments associated with this update.
*/
uint_fast64_t getNumberOfBooleanAssignments() const;
/*!
* Retrieves the number of integer assignments associated with this update.
*
* @return The number of integer assignments associated with this update.
*/
uint_fast64_t getNumberOfIntegerAssignments() const;
/*!
* Retrieves a reference to the map of boolean variable names to their respective assignments.
*
* @return A reference to the map of boolean variable names to their respective assignments.
*/
std::map<std::string, storm::ir::Assignment> const& getBooleanAssignments() const;
/*!
* Retrieves a reference to the map of integer variable names to their respective assignments.
*
* @return A reference to the map of integer variable names to their respective assignments.
*/
std::map<std::string, storm::ir::Assignment> const& getIntegerAssignments() const;
/*!
* Retrieves a reference to the assignment for the boolean variable with the given name.
*
* @return A reference to the assignment for the boolean variable with the given name.
*/
storm::ir::Assignment const& getBooleanAssignment(std::string const& variableName) const;
/*!
* Retrieves a reference to the assignment for the integer variable with the given name.
*
* @return A reference to the assignment for the integer variable with the given name.
*/
storm::ir::Assignment const& getIntegerAssignment(std::string const& variableName) const;
/*!
* Retrieves a string representation of this update.
*
* @return A string representation of this update.
*/
std::string toString() const;
private:
// An expression specifying the likelihood of taking this update.
std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression;
// A mapping of boolean variable names to their assignments in this update.
std::map<std::string, storm::ir::Assignment> booleanAssignments;
// A mapping of integer variable names to their assignments in this update.
std::map<std::string, storm::ir::Assignment> integerAssignments;
};
} // namespace ir
} // namespace storm
#endif /* STORM_IR_UPDATE_H_ */

81
src/ir/Variable.cpp
View File

@ -10,47 +10,46 @@
#include <iostream>
#include "Variable.h"
#include "src/parser/prismparser/VariableState.h"
namespace storm {
namespace ir {
Variable::Variable() : globalIndex(0), localIndex(0), variableName(), initialValue() {
// Nothing to do here.
}
Variable::Variable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue)
: globalIndex(globalIndex), localIndex(localIndex), variableName(variableName), initialValue(initialValue) {
// Nothing to do here.
}
Variable::Variable(Variable const& var, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap)
: globalIndex(newGlobalIndex), localIndex(var.getLocalIndex()), variableName(var.getName()) {
if (var.initialValue != nullptr) {
this->initialValue = var.initialValue->clone(renaming, booleanVariableToIndexMap, integerVariableToIndexMap);
}
}
std::string const& Variable::getName() const {
return variableName;
}
uint_fast64_t Variable::getGlobalIndex() const {
return globalIndex;
}
uint_fast64_t Variable::getLocalIndex() const {
return localIndex;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Variable::getInitialValue() const {
return initialValue;
}
void Variable::setInitialValue(std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue) {
this->initialValue = initialValue;
}
} // namespace ir
namespace ir {
Variable::Variable() : localIndex(0), globalIndex(0), variableName(), initialValue() {
// Nothing to do here.
}
Variable::Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue)
: localIndex(localIndex), globalIndex(globalIndex), variableName(variableName), initialValue(initialValue) {
// Nothing to do here.
}
Variable::Variable(Variable const& var, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState)
: localIndex(var.getLocalIndex()), globalIndex(newGlobalIndex), variableName(var.getName()) {
if (var.initialValue != nullptr) {
this->initialValue = var.initialValue->clone(renaming, variableState);
}
}
std::string const& Variable::getName() const {
return variableName;
}
uint_fast64_t Variable::getGlobalIndex() const {
return globalIndex;
}
uint_fast64_t Variable::getLocalIndex() const {
return localIndex;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Variable::getInitialValue() const {
return initialValue;
}
void Variable::setInitialValue(std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue) {
this->initialValue = initialValue;
}
} // namespace ir
} // namespace storm

178
src/ir/Variable.h
View File

@ -14,95 +14,99 @@
#include "expressions/BaseExpression.h"
namespace storm {
namespace ir {
/*!
* A class representing a untyped variable.
*/
class Variable {
public:
/*!
* Default constructor. Creates an unnamed, untyped variable without initial value.
*/
Variable();
/*!
* Creates an untyped variable with the given name and initial value.
*
* @param index A unique (among the variables of equal type) index for the variable.
* @param variableName the name of the variable.
* @param initialValue the expression that defines the initial value of the variable.
*/
Variable(uint_fast64_t globalIndex, uint_fast64_t localIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
/*!
* Creates a copy of the given variable and performs the provided renaming.
*
* @param oldVariable The variable to copy.
* @param newName New name of this variable.
* @param newGlobalIndex The new global index of the variable.
* @param renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
* @param booleanVariableToIndexMap A mapping from boolean variable names to their global indices.
* @param integerVariableToIndexMap A mapping from integer variable names to their global indices.
*/
Variable(Variable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::map<std::string, uint_fast64_t> const& booleanVariableToIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToIndexMap);
/*!
* Retrieves the name of the variable.
*
* @return The name of the variable.
*/
std::string const& getName() const;
/*!
* Retrieves the global index of the variable, i.e. the index in all variables of equal type
* of all modules.
*
* @return The global index of the variable.
*/
uint_fast64_t getGlobalIndex() const;
/*!
* Retrieves the global index of the variable, i.e. the index in all variables of equal type in
* the same module.
*
* @return The local index of the variable.
*/
uint_fast64_t getLocalIndex() const;
/*!
* Retrieves the expression defining the initial value of the variable.
*
* @return The expression defining the initial value of the variable.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> const& getInitialValue() const;
/*!
* Sets the initial value to the given expression.
*
* @param initialValue The new initial value.
*/
void setInitialValue(std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue);
private:
// A unique (among the variables of equal type) index for the variable over all modules.
uint_fast64_t globalIndex;
namespace parser {
namespace prism {
class VariableState;
} // namespace prismparser
} // namespace parser
// A unique (among the variables of equal type) index for the variable inside its module.
uint_fast64_t localIndex;
// The name of the variable.
std::string variableName;
// The expression defining the initial value of the variable.
std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue;
};
} // namespace ir
namespace ir {
/*!
* A class representing a untyped variable.
*/
class Variable {
public:
/*!
* Default constructor. Creates an unnamed, untyped variable without initial value.
*/
Variable();
/*!
* Creates an untyped variable with the given name and initial value.
*
* @param localIndex A module-local index for the variable.
* @param globalIndex A globally unique (among the variables of equal type) index for the variable.
* @param variableName the name of the variable.
* @param initialValue the expression that defines the initial value of the variable.
*/
Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
/*!
* Creates a copy of the given variable and performs the provided renaming.
*
* @param oldVariable The variable to copy.
* @param newName New name of this variable.
* @param newGlobalIndex The new global index of the variable.
* @param renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
* @param variableState An object knowing about the variables in the system.
*/
Variable(Variable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
/*!
* Retrieves the name of the variable.
*
* @return The name of the variable.
*/
std::string const& getName() const;
/*!
* Retrieves the global index of the variable, i.e. the index in all variables of equal type
* of all modules.
*
* @return The global index of the variable.
*/
uint_fast64_t getGlobalIndex() const;
/*!
* Retrieves the global index of the variable, i.e. the index in all variables of equal type in
* the same module.
*
* @return The local index of the variable.
*/
uint_fast64_t getLocalIndex() const;
/*!
* Retrieves the expression defining the initial value of the variable.
*
* @return The expression defining the initial value of the variable.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> const& getInitialValue() const;
/*!
* Sets the initial value to the given expression.
*
* @param initialValue The new initial value.
*/
void setInitialValue(std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue);
private:
// A unique (among the variables of equal type) index for the variable inside its module.
uint_fast64_t localIndex;
// A unique (among the variables of equal type) index for the variable over all modules.
uint_fast64_t globalIndex;
// The name of the variable.
std::string variableName;
// The expression defining the initial value of the variable.
std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue;
};
} // namespace ir
} // namespace storm
#endif /* STORM_IR_VARIABLE_H_ */

4
src/ir/expressions/BaseExpression.h
View File

@ -21,7 +21,7 @@ namespace storm {
// Forward-declare VariableState.
namespace parser {
namespace prismparser {
namespace prism {
class VariableState;
} // namespace prismparser
} // namespace parser
@ -70,7 +70,7 @@ namespace storm {
* @param renaming A mapping from identifier names to strings they are to be replaced with.
* @param variableState An object knowing about the global variable state.
*/
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const = 0;
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const = 0;
/*!
* Retrieves the value of the expression as an integer given the provided variable valuation.

2
src/ir/expressions/BinaryBooleanFunctionExpression.cpp
View File

@ -18,7 +18,7 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const {
std::shared_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType));
}

4
src/ir/expressions/BinaryBooleanFunctionExpression.h
View File

@ -8,7 +8,7 @@
#ifndef STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_
#define STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_
#include "src/ir/expressions/BinaryExpression.h"
#include "BinaryExpression.h"
namespace storm {
namespace ir {
@ -33,7 +33,7 @@ namespace storm {
*/
BinaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, FunctionType functionType);
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const override;
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

2
src/ir/expressions/BinaryNumericalFunctionExpression.cpp
View File

@ -18,7 +18,7 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const {
std::shared_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType));
}

2
src/ir/expressions/BinaryNumericalFunctionExpression.h
View File

@ -34,7 +34,7 @@ namespace storm {
*/
BinaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, FunctionType functionType);
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const override;
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
/*!
* Retrieves the operator that is associated with this node.

2
src/ir/expressions/BinaryRelationExpression.cpp
View File

@ -18,7 +18,7 @@ namespace storm {
// Nothing to do here
}
std::shared_ptr<BaseExpression> BinaryRelationExpression::clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const {
std::shared_ptr<BaseExpression> BinaryRelationExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->relationType));
}

2
src/ir/expressions/BinaryRelationExpression.h
View File

@ -33,7 +33,7 @@ namespace storm {
*/
BinaryRelationExpression(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, RelationType relationType);
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const override;
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

2
src/ir/expressions/BooleanConstantExpression.cpp
View File

@ -18,7 +18,7 @@ namespace storm {
value = false;
}
std::shared_ptr<BaseExpression> BooleanConstantExpression::clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const {
std::shared_ptr<BaseExpression> BooleanConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new BooleanConstantExpression(*this));
}

2
src/ir/expressions/BooleanConstantExpression.h
View File

@ -26,7 +26,7 @@ namespace storm {
*/
BooleanConstantExpression(std::string const& constantName);
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const override;
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

2
src/ir/expressions/BooleanLiteralExpression.cpp
View File

@ -15,7 +15,7 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> BooleanLiteralExpression::clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const {
std::shared_ptr<BaseExpression> BooleanLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->value));
}

2
src/ir/expressions/BooleanLiteralExpression.h
View File

@ -26,7 +26,7 @@ namespace storm {
*/
BooleanLiteralExpression(bool value);
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const override;
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

6
src/ir/expressions/ConstantExpression.cpp
View File

@ -5,13 +5,13 @@
* Author: Christian Dehnert
*/
#include "src/ir/expressions/ConstantExpression.h"
#include "ConstantExpression.h"
namespace storm {
namespace ir {
namespace expressions {
ConstantExpression::ConstantExpression(ReturnType type, std::string constantName) : BaseExpression(type), constantName(constantName) {
ConstantExpression::ConstantExpression(ReturnType type, std::string const& constantName) : BaseExpression(type), constantName(constantName) {
// Nothing to do here.
}
@ -19,7 +19,7 @@ namespace storm {
return constantName;
}
virtual std::string ConstantExpression::toString() const {
std::string ConstantExpression::toString() const {
return constantName;
}

4
src/ir/expressions/ConstantExpression.h
View File

@ -8,7 +8,7 @@
#ifndef STORM_IR_EXPRESSIONS_CONSTANTEXPRESSION_H_
#define STORM_IR_EXPRESSIONS_CONSTANTEXPRESSION_H_
#include "src/ir/expressions/BaseExpression.h"
#include "BaseExpression.h"
namespace storm {
namespace ir {
@ -26,7 +26,7 @@ namespace storm {
* @param type The type of the constant.
* @param constantName The name of the constant.
*/
ConstantExpression(ReturnType type, std::string constantName);
ConstantExpression(ReturnType type, std::string const& constantName);
/*!
* Retrieves the name of the constant.

14
src/ir/expressions/DoubleConstantExpression.cpp
View File

@ -13,11 +13,11 @@ namespace storm {
namespace ir {
namespace expressions {
DoubleConstantExpression::DoubleConstantExpression(std::string const& constantName) : ConstantExpression(double_, constantName), defined(false), value(0) {
DoubleConstantExpression::DoubleConstantExpression(std::string const& constantName) : ConstantExpression(double_, constantName), value(0), defined(false) {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> DoubleConstantExpression::clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const {
std::shared_ptr<BaseExpression> DoubleConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new DoubleConstantExpression(*this));
}
@ -30,24 +30,24 @@ namespace storm {
}
}
virtual void DoubleConstantExpression::accept(ExpressionVisitor* visitor) {
void DoubleConstantExpression::accept(ExpressionVisitor* visitor) {
visitor->visit(this);
}
virtual std::string DoubleConstantExpression::toString() const {
std::string DoubleConstantExpression::toString() const {
std::stringstream result;
result << this->constantName;
result << this->getConstantName();
if (defined) {
result << "[" << value << "]";
}
return result.str();
}
bool DoubleConstantExpression::isDefined() {
bool DoubleConstantExpression::isDefined() const {
return defined;
}
double DoubleConstantExpression::getValue() {
double DoubleConstantExpression::getValue() const {
return value;
}

7
src/ir/expressions/DoubleConstantExpression.h
View File

@ -19,9 +19,14 @@ namespace storm {
*/
class DoubleConstantExpression : public ConstantExpression {
public:
/*!
* Creates a double constant expression with the given constant name.
*
* @param constantName The name of the constant to use.
*/
DoubleConstantExpression(std::string const& constantName);
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const override;
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;

10
src/ir/expressions/DoubleLiteralExpression.cpp
View File

@ -17,19 +17,19 @@ namespace storm {
// Nothing to do here.
}
virtual std::shared_ptr<BaseExpression> DoubleLiteralExpression::clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new DoubleLiteral(this->value));
std::shared_ptr<BaseExpression> DoubleLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->value));
}
virtual double DoubleLiteralExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
double DoubleLiteralExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
return value;
}
virtual void DoubleLiteralExpression::accept(ExpressionVisitor* visitor) {
void DoubleLiteralExpression::accept(ExpressionVisitor* visitor) {
visitor->visit(this);
}
virtual std::string DoubleLiteralExpression::toString() const {
std::string DoubleLiteralExpression::toString() const {
std::stringstream result;
result << value;
return result.str();

4
src/ir/expressions/DoubleLiteralExpression.h
View File

@ -26,7 +26,7 @@ namespace storm {
*/
DoubleLiteralExpression(double value);
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const override;
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
@ -35,7 +35,7 @@ namespace storm {
virtual std::string toString() const override;
private:
// The value of the boolean literal.
// The value of the double literal.
double value;
};

6
src/ir/expressions/Expressions.h
View File

@ -12,9 +12,9 @@
#include "BinaryBooleanFunctionExpression.h"
#include "BinaryNumericalFunctionExpression.h"
#include "BinaryRelationExpression.h"
#include "BooleanLiteral.h"
#include "DoubleLiteral.h"
#include "IntegerLiteral.h"
#include "BooleanLiteralExpression.h"
#include "DoubleLiteralExpression.h"
#include "IntegerLiteralExpression.h"
#include "UnaryBooleanFunctionExpression.h"
#include "UnaryNumericalFunctionExpression.h"
#include "VariableExpression.h"

59
src/ir/expressions/IntegerConstantExpression.cpp
View File

@ -0,0 +1,59 @@
/*
* IntegerConstantExpression.cpp
*
* Created on: 10.06.2013
* Author: Christian Dehnert
*/
#include "IntegerConstantExpression.h"
namespace storm {
namespace ir {
namespace expressions {
IntegerConstantExpression::IntegerConstantExpression(std::string const& constantName) : ConstantExpression(int_, constantName), value(0), defined(false) {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> IntegerConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new IntegerConstantExpression(*this));
}
int_fast64_t IntegerConstantExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
if (!defined) {
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< "Integer constant '" << this->getConstantName() << "' is undefined.";
} else {
return value;
}
}
void IntegerConstantExpression::accept(ExpressionVisitor* visitor) {
visitor->visit(this);
}
std::string IntegerConstantExpression::toString() const {
std::stringstream result;
result << this->getConstantName();
if (defined) {
result << "[" << value << "]";
}
return result.str();
}
bool IntegerConstantExpression::isDefined() const {
return defined;
}
int_fast64_t IntegerConstantExpression::getValue() const {
return value;
}
void IntegerConstantExpression::define(int_fast64_t value) {
defined = true;
this->value = value;
}
} // namespace expressions
} // namespace ir
} // namespace storm

133
src/ir/expressions/IntegerConstantExpression.h
View File

@ -2,84 +2,67 @@
* IntegerConstantExpression.h
*
* Created on: 04.01.2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef INTEGERCONSTANTEXPRESSION_H_
#define INTEGERCONSTANTEXPRESSION_H_
#ifndef STORM_IR_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_
#define STORM_IR_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_
#include "ConstantExpression.h"
namespace storm {
namespace ir {
namespace expressions {
class IntegerConstantExpression : public ConstantExpression {
public:
IntegerConstantExpression(std::string constantName) : ConstantExpression(int_, constantName), defined(false), value(0) {
}
IntegerConstantExpression(const IntegerConstantExpression& ice)
: ConstantExpression(ice), defined(ice.defined), value(ice.value) {
}
virtual ~IntegerConstantExpression() {
}
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new IntegerConstantExpression(*this));
}
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
if (!defined) {
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< "Integer constant '" << this->getConstantName() << "' is undefined.";
} else {
return value;
}
}
virtual void accept(ExpressionVisitor* visitor) {
visitor->visit(this);
}
virtual std::string toString() const {
std::string result = this->constantName;
if (defined) {
result += "[" + boost::lexical_cast<std::string>(value) + "]";
}
return result;
}
virtual std::string dump(std::string prefix) const {
std::stringstream result;
result << prefix << "IntegerConstantExpression " << this->toString() << std::endl;
return result.str();
}
bool isDefined() {
return defined;
}
int_fast64_t getValue() {
return value;
}
void define(int_fast64_t value) {
defined = true;
this->value = value;
}
private:
bool defined;
int_fast64_t value;
};
}
}
}
#endif /* INTEGERCONSTANTEXPRESSION_H_ */
namespace ir {
namespace expressions {
/*!
* A class representing a constant expression of type integer.
*/
class IntegerConstantExpression : public ConstantExpression {
public:
/*!
* Creates an integer constant expression with the given constant name.
*
* @param constantName The name of the constant to use.
*/
IntegerConstantExpression(std::string const& constantName);
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
virtual void accept(ExpressionVisitor* visitor) override;
virtual std::string toString() const override;
/*!
* Retrieves whether the constant is defined or not.
*
* @return True if the constant is defined.
*/
bool isDefined() const;
/*!
* Retrieves the value of the constant if it is defined and false otherwise.
*/
int_fast64_t getValue() const;
/*!
* Defines the constant using the given value.
*
* @param value The value to use for defining the constant.
*/
void define(int_fast64_t value);
private:
// This member stores the value of the constant if it is defined.
int_fast64_t value;
// A flag indicating whether the member is defined or not.
bool defined;
};
} // namespace expressions
} // namespace ir
} // namespace storm
#endif /* STORM_IR_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_ */

57
src/ir/expressions/IntegerLiteral.h
View File

@ -1,57 +0,0 @@
/*
* IntegerLiteral.h
*
* Created on: 03.01.2013
* Author: chris
*/
#ifndef INTEGERLITERAL_H_
#define INTEGERLITERAL_H_
#include "src/ir/expressions/BaseExpression.h"
namespace storm {
namespace ir {
namespace expressions {
class IntegerLiteral : public BaseExpression {
public:
int_fast64_t value;
IntegerLiteral(int_fast64_t value) : BaseExpression(int_), value(value) {
}
virtual ~IntegerLiteral() {
}
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new IntegerLiteral(this->value));
}
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
return value;
}
virtual void accept(ExpressionVisitor* visitor) {
visitor->visit(this);
}
virtual std::string toString() const {
return boost::lexical_cast<std::string>(value);
}
virtual std::string dump(std::string prefix) const {
std::stringstream result;
result << prefix << "IntegerLiteral " << this->toString() << std::endl;
return result.str();
}
};
}
}
}
#endif /* INTEGERLITERAL_H_ */

40
src/ir/expressions/IntegerLiteralExpression.cpp
View File

@ -0,0 +1,40 @@
/*
* IntegerLiteralExpression.cpp
*
* Created on: 03.01.2013
* Author: Christian Dehnert
*/
#include <sstream>
#include "IntegerLiteralExpression.h"
namespace storm {
namespace ir {
namespace expressions {
IntegerLiteralExpression::IntegerLiteralExpression(int_fast64_t value) : BaseExpression(int_), value(value) {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> IntegerLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->value));
}
int_fast64_t IntegerLiteralExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
return value;
}
void IntegerLiteralExpression::accept(ExpressionVisitor* visitor) {
visitor->visit(this);
}
std::string IntegerLiteralExpression::toString() const {
std::stringstream result;
result << value;
return result.str();
}
} // namespace expressions
} // namespace ir
} // namespace storm

46
src/ir/expressions/IntegerLiteralExpression.h
View File

@ -0,0 +1,46 @@
/*
* IntegerLiteralExpression.h
*
* Created on: 03.01.2013
* Author: Christian Dehnert
*/
#ifndef STORM_IR_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_
#define STORM_IR_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_
#include "src/ir/expressions/BaseExpression.h"
namespace storm {
namespace ir {
namespace expressions {
/*!
* A class representing an integer literal.
*/
class IntegerLiteralExpression : public BaseExpression {
public:
/*!
* Creates an integer literal expression with the given value.
*
* @param value The value for the integer literal.
*/
IntegerLiteralExpression(int_fast64_t value);
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
virtual void accept(ExpressionVisitor* visitor) override;
virtual std::string toString() const override;
private:
// The value of the double literal.
int_fast64_t value;
};
} // namespace expressions
} // namespace ir
} // namespace storm
#endif /* STORM_IR_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_ */

56
src/ir/expressions/UnaryBooleanFunctionExpression.cpp
View File

@ -0,0 +1,56 @@
/*
* UnaryBooleanFunctionExpression.cpp
*
* Created on: 10.06.2013
* Author: Christian Dehnert
*/
#ifndef STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_
#define STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_
#include <sstream>
#include "UnaryBooleanFunctionExpression.h"
namespace storm {
namespace ir {
namespace expressions {
UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> child, FunctionType functionType) : UnaryExpression(bool_, child), functionType(functionType) {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, variableState), this->functionType));
}
FunctionType UnaryBooleanFunctionExpression::getFunctionType() const {
return functionType;
}
bool UnaryBooleanFunctionExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
bool resultChild = this->getChild()->getValueAsBool(variableValues);
switch(functionType) {
case NOT: return !resultChild; break;
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< "Unknown boolean unary operator: '" << functionType << "'.";
}
}
void UnaryBooleanFunctionExpression::accept(ExpressionVisitor* visitor) {
visitor->visit(this);
}
std::string UnaryBooleanFunctionExpression::toString() const {
std::stringstream result;
switch (functionType) {
case NOT: result << "!"; break;
}
result << "(" << this->getChild()->toString() << ")";
return result.str();
}
} // namespace expressions
} // namespace ir
} // namespace storm

124
src/ir/expressions/UnaryBooleanFunctionExpression.h
View File

@ -2,80 +2,60 @@
* UnaryBooleanFunctionExpression.h
*
* Created on: 03.01.2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef UNARYBOOLEANFUNCTIONEXPRESSION_H_
#define UNARYBOOLEANFUNCTIONEXPRESSION_H_
#ifndef STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_
#define STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_
#include "src/ir/expressions/UnaryExpression.h"
#include "UnaryExpression.h"
namespace storm {
namespace ir {
namespace expressions {
class UnaryBooleanFunctionExpression : public UnaryExpression {
public:
enum FunctionType {NOT};
UnaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> child, FunctionType functionType) : UnaryExpression(bool_, child), functionType(functionType) {
}
virtual ~UnaryBooleanFunctionExpression() {
}
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, variableState), this->functionType));
}
FunctionType getFunctionType() const {
return functionType;
}
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
bool resultChild = this->getChild()->getValueAsBool(variableValues);
switch(functionType) {
case NOT: return !resultChild; break;
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< "Unknown boolean unary operator: '" << functionType << "'.";
}
}
virtual void accept(ExpressionVisitor* visitor) {
visitor->visit(this);
}
virtual std::string toString() const {
std::string result = "";
switch (functionType) {
case NOT: result += "!"; break;
}
result += "(" + this->getChild()->toString() + ")";
return result;
}
virtual std::string dump(std::string prefix) const {
std::stringstream result;
result << prefix << "UnaryBooleanFunctionExpression" << std::endl;
switch (functionType) {
case NOT: result << prefix << "!" << std::endl; break;
}
result << this->getChild()->dump(prefix + "\t");
return result.str();
}
private:
FunctionType functionType;
};
}
}
}
#endif /* UNARYBOOLEANFUNCTIONEXPRESSION_H_ */
namespace ir {
namespace expressions {
/*!
* A class representing a unary function expression of boolean type.
*/
class UnaryBooleanFunctionExpression : public UnaryExpression {
public:
/*!
* An enum type specifying the different functions applicable.
*/
enum FunctionType {NOT};
/*!
* Creates a unary boolean function expression tree node with the given child and function type.
*
* @param child The child of the node.
* @param functionType The operator that is to be applied to the two children.
*/
UnaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> child, FunctionType functionType);
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
/*!
* Retrieves the operator that is associated with this node.
*
* @param The operator that is associated with this node.
*/
FunctionType getFunctionType() const {
return functionType;
}
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
virtual void accept(ExpressionVisitor* visitor) override;
virtual std::string toString() const override;
private:
// The operator that is associated with this node.
FunctionType functionType;
};
} // namespace expressions
} // namespace ir
} // namespace storm
#endif /* STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_ */

24
src/ir/expressions/UnaryExpression.cpp
View File

@ -0,0 +1,24 @@
/*
* UnaryExpression.cpp
*
* Created on: 27.01.2013
* Author: Christian Dehnert
*/
#include "UnaryExpression.h"
namespace storm {
namespace ir {
namespace expressions {
UnaryExpression::UnaryExpression(ReturnType type, std::shared_ptr<BaseExpression> child) : BaseExpression(type), child(child) {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> const& UnaryExpression::getChild() const {
return child;
}
} // namespace expressions
} // namespace ir
} // namespace storm

52
src/ir/expressions/UnaryExpression.h
View File

@ -11,29 +11,35 @@
#include "BaseExpression.h"
namespace storm {
namespace ir {
namespace expressions {
class UnaryExpression : public BaseExpression {
public:
UnaryExpression(ReturnType type, std::shared_ptr<BaseExpression> child) : BaseExpression(type), child(child) {
}
std::shared_ptr<BaseExpression> const& getChild() const {
return child;
}
private:
std::shared_ptr<BaseExpression> child;
};
} // namespace expressions
} // namespace ir
namespace ir {
namespace expressions {
/*!
* A class representing a generic unary expression.
*/
class UnaryExpression : public BaseExpression {
public:
/*!
* Constructs a unary expression with the given type and child.
* @param type The type of the unary expression.
* @param right The child of the unary expression.
*/
UnaryExpression(ReturnType type, std::shared_ptr<BaseExpression> child);
/*!
* Retrieves the child of the expression node.
*
* @return The child of the expression node.
*/
std::shared_ptr<BaseExpression> const& getChild() const;
private:
// The left child of the unary expression.
std::shared_ptr<BaseExpression> child;
};
} // namespace expressions
} // namespace ir
} // namespace storm
#endif /* STORM_IR_EXPRESSIONS_UNARYEXPRESSION_H_ */

69
src/ir/expressions/UnaryNumericalFunctionExpression.cpp
View File

@ -0,0 +1,69 @@
/*
* UnaryFunctionExpression.h
*
* Created on: 03.01.2013
* Author: Christian Dehnert
*/
#include "UnaryNumericalFunctionExpression.h"
namespace storm {
namespace ir {
namespace expressions {
UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> child, FunctionType functionType) : UnaryExpression(type, child), functionType(functionType) {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, variableState), this->functionType));
}
int_fast64_t UnaryNumericalFunctionExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
if (this->getType() != int_) {
BaseExpression::getValueAsInt(variableValues);
}
int_fast64_t resultChild = this->getChild()->getValueAsInt(variableValues);
switch(functionType) {
case MINUS: return -resultChild; break;
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< "Unknown numerical unary operator: '" << functionType << "'.";
}
}
double UnaryNumericalFunctionExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
if (this->getType() != double_) {
BaseExpression::getValueAsDouble(variableValues);
}
double resultChild = this->getChild()->getValueAsDouble(variableValues);
switch(functionType) {
case MINUS: return -resultChild; break;
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< "Unknown numerical unary operator: '" << functionType << "'.";
}
}
FunctionType UnaryNumericalFunctionExpression::getFunctionType() const {
return functionType;
}
void UnaryNumericalFunctionExpression::accept(ExpressionVisitor* visitor) {
visitor->visit(this);
}
std::string UnaryNumericalFunctionExpression::toString() const {
std::string result = "";
switch (functionType) {
case MINUS: result += "-"; break;
}
result += this->getChild()->toString();
return result;
}
} // namespace expressions
} // namespace ir
} // namespace storm

144
src/ir/expressions/UnaryNumericalFunctionExpression.h
View File

@ -2,98 +2,62 @@
* UnaryFunctionExpression.h
*
* Created on: 03.01.2013
* Author: chris
* Author: Christian Dehnert
*/
#ifndef UNARYFUNCTIONEXPRESSION_H_
#define UNARYFUNCTIONEXPRESSION_H_
#ifndef STORM_IR_EXPRESSIONS_UNARYFUNCTIONEXPRESSION_H_
#define STORM_IR_EXPRESSIONS_UNARYFUNCTIONEXPRESSION_H_
#include "src/ir/expressions/UnaryExpression.h"
#include "UnaryExpression.h"
namespace storm {
namespace ir {
namespace expressions {
class UnaryNumericalFunctionExpression : public UnaryExpression {
public:
enum FunctionType {MINUS};
UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> child, FunctionType functionType) : UnaryExpression(type, child), functionType(functionType) {
}
virtual ~UnaryNumericalFunctionExpression() {
}
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const {
return std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, variableState), this->functionType));
}
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
if (this->getType() != int_) {
BaseExpression::getValueAsInt(variableValues);
}
int_fast64_t resultChild = this->getChild()->getValueAsInt(variableValues);
switch(functionType) {
case MINUS: return -resultChild; break;
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< "Unknown numerical unary operator: '" << functionType << "'.";
}
}
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
if (this->getType() != double_) {
BaseExpression::getValueAsDouble(variableValues);
}
double resultChild = this->getChild()->getValueAsDouble(variableValues);
switch(functionType) {
case MINUS: return -resultChild; break;
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< "Unknown numerical unary operator: '" << functionType << "'.";
}
}
FunctionType getFunctionType() const {
return functionType;
}
virtual void accept(ExpressionVisitor* visitor) {
visitor->visit(this);
}
virtual std::string toString() const {
std::string result = "";
switch (functionType) {
case MINUS: result += "-"; break;
}
result += this->getChild()->toString();
return result;
}
virtual std::string dump(std::string prefix) const {
std::stringstream result;
result << prefix << "UnaryNumericalFunctionExpression" << std::endl;
switch (functionType) {
case MINUS: result << prefix << "-" << std::endl; break;
}
result << this->getChild()->dump(prefix + "\t");
return result.str();
}
private:
FunctionType functionType;
};
}
}
}
#endif /* UNARYFUNCTIONEXPRESSION_H_ */
namespace ir {
namespace expressions {
/*!
* A class representing a unary function expression of numerical type.
*/
class UnaryNumericalFunctionExpression : public UnaryExpression {
public:
/*!
* An enum type specifying the different functions applicable.
*/
enum FunctionType {MINUS};
/*!
* Creates a unary numerical function expression tree node with the given child and function type.
*
* @param child The child of the node.
* @param functionType The operator that is to be applied to the two children.
*/
UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> child, FunctionType functionType);
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
/*!
* Retrieves the operator that is associated with this node.
*
* @param The operator that is associated with this node.
*/
FunctionType getFunctionType() const {
return functionType;
}
virtual void accept(ExpressionVisitor* visitor) override;
virtual std::string toString() const override;
private:
// The operator that is associated with this node.
FunctionType functionType;
};
} // namespace expressions
} // namespace ir
} // namespace storm
#endif /* STORM_IR_EXPRESSIONS_UNARYFUNCTIONEXPRESSION_H_ */

43
src/ir/expressions/VariableExpression.cpp
View File

@ -7,30 +7,22 @@
#include "VariableExpression.h"
#include "src/parser/prismparser/VariableState.h"
#include "src/exceptions/ExpressionEvaluationException.h"
namespace storm {
namespace ir {
namespace expressions {
VariableExpression::VariableExpression(ReturnType type, std::string variableName) : BaseExpression(type), localIndex(0), globalIndex(0), variableName(variableName) {
VariableExpression::VariableExpression(ReturnType type, std::string const& variableName) : BaseExpression(type), globalIndex(0), variableName(variableName) {
// Nothing to do here.
}
VariableExpression::VariableExpression(ReturnType type, uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string variableName)
: BaseExpression(type), localIndex(localIndex), globalIndex(globalIndex), variableName(variableName) {
VariableExpression::VariableExpression(ReturnType type, uint_fast64_t globalIndex, std::string const& variableName)
: BaseExpression(type), globalIndex(globalIndex), variableName(variableName) {
// Nothing to do here.
}
VariableExpression::VariableExpression(VariableExpression const& oldExpression, std::string const& newName, uint_fast64_t newGlobalIndex)
: BaseExpression(oldExpression.getType()), localIndex(oldExpression.localIndex), globalIndex(newGlobalIndex), variableName(newName) {
// Nothing to do here.
}
virtual VariableExpression::~VariableExpression() {
// Nothing to do here.
}
virtual std::shared_ptr<BaseExpression> VariableExpression::clone(std::map<std::string, std::string> const& renaming, VariableState const& variableState) {
std::shared_ptr<BaseExpression> VariableExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
// Perform the proper cloning.
auto renamingPair = renaming.find(this->variableName);
if (renamingPair != renaming.end()) {
@ -40,22 +32,15 @@ namespace storm {
}
}
virtual void VariableExpression::accept(ExpressionVisitor* visitor) {
std::cout << "Visitor!" << std::endl;
void VariableExpression::accept(ExpressionVisitor* visitor) {
visitor->visit(this);
}
virtual std::string VariableExpression::toString() const {
std::string VariableExpression::toString() const {
return this->variableName;
}
virtual std::string VariableExpression::dump(std::string prefix) const {
std::stringstream result;
result << prefix << this->variableName << " " << index << std::endl;
return result.str();
}
virtual int_fast64_t VariableExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
int_fast64_t VariableExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
if (this->getType() != int_) {
BaseExpression::getValueAsInt(variableValues);
}
@ -68,7 +53,7 @@ namespace storm {
}
}
virtual bool VariableExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
bool VariableExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
if (this->getType() != bool_) {
BaseExpression::getValueAsBool(variableValues);
}
@ -81,12 +66,12 @@ namespace storm {
}
}
virtual double VariableExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
double VariableExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
if (this->getType() != double_) {
BaseExpression::getValueAsDouble(variableValues);
}
throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression with "
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression with "
<< " variable '" << variableName << "' of type double.";
}
@ -94,14 +79,10 @@ namespace storm {
return variableName;
}
uint_fast64_t VariableExpression::getLocalVariableIndex() const {
return this->localIndex;
}
uint_fast64_t VariableExpression::getGlobalVariableIndex() const {
return this->globalIndex;
}
} // namespace expressions
} // namespace ir
} // namespace storm
} // namespace storm

69
src/ir/expressions/VariableExpression.h
View File

@ -5,18 +5,10 @@
* Author: Christian Dehnert
*/
#ifndef VARIABLEEXPRESSION_H_
#define VARIABLEEXPRESSION_H_
#include <memory>
#include <iostream>
#ifndef STORM_IR_EXPRESSIONS_VARIABLEEXPRESSION_H_
#define STORM_IR_EXPRESSIONS_VARIABLEEXPRESSION_H_
#include "BaseExpression.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm {
@ -30,37 +22,60 @@ namespace storm {
namespace ir {
namespace expressions {
/*!
* A class representing a variable in the expression tree.
*/
class VariableExpression : public BaseExpression {
public:
VariableExpression(ReturnType type, std::string variableName);
VariableExpression(ReturnType type, uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string variableName);
/*!
* Creates a variable expression of the given type with the given name. As this variable has no indices
* it is only meant as a dummy and needs to be replaced with a "full" variable expression.
*
* @param type The type of the variable.
* @param variableName The name of the variable.
*/
VariableExpression(ReturnType type, std::string const& variableName);
VariableExpression(VariableExpression const& oldExpression, std::string const& newName, uint_fast64_t newGlobalIndex);
/*!
* Creates a variable expression of the given type with the given name and indices.
*
* @param type The type of the variable.
* @param globalIndex The global (i.e. program-wide) index of the variable.
* @param variableName The name of the variable.
*/
VariableExpression(ReturnType type, uint_fast64_t globalIndex, std::string const& variableName);
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
virtual ~VariableExpression();
virtual void accept(ExpressionVisitor* visitor) override;
virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, parser::prismparser::VariableState const& variableState) const;
virtual std::string toString() const override;
virtual void accept(ExpressionVisitor* visitor);
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
virtual std::string toString() const;
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const;
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const;
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const;
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
/*!
* Retrieves the name of the variable.
*
* @return The name of the variable.
*/
std::string const& getVariableName() const;
uint_fast64_t getLocalVariableIndex() const;
/*!
* Retrieves the global (i.e. program-wide) index of the variable.
*
* @return The global index of the variable.
*/
uint_fast64_t getGlobalVariableIndex() const;
private:
uint_fast64_t localIndex;
// The global index of the variable.
uint_fast64_t globalIndex;
// The name of the variable.
std::string variableName;
};
@ -68,4 +83,4 @@ namespace storm {
} // namespace ir
} // namespace storm
#endif /* VARIABLEEXPRESSION_H_ */
#endif /* STORM_IR_EXPRESSIONS_VARIABLEEXPRESSION_H_ */

10
src/parser/prismparser/BaseGrammar.h
View File

@ -63,7 +63,7 @@ namespace prism {
* @returns Boolean literal.
*/
std::shared_ptr<BaseExpression> createBoolLiteral(const bool value) {
return std::shared_ptr<BooleanLiteral>(new BooleanLiteral(value));
return std::shared_ptr<BooleanLiteralExpression>(new BooleanLiteralExpression(value));
}
/*!
* Create a new double literal with the given value.
@ -71,7 +71,7 @@ namespace prism {
* @returns Double literal.
*/
std::shared_ptr<BaseExpression> createDoubleLiteral(const double value) {
return std::shared_ptr<DoubleLiteral>(new DoubleLiteral(value));
return std::shared_ptr<DoubleLiteralExpression>(new DoubleLiteralExpression(value));
}
/*!
* Create a new integer literal with the given value.
@ -79,7 +79,7 @@ namespace prism {
* @returns Integer literal.
*/
std::shared_ptr<BaseExpression> createIntLiteral(const int_fast64_t value) {
return std::shared_ptr<IntegerLiteral>(new IntegerLiteral(value));
return std::shared_ptr<IntegerLiteralExpression>(new IntegerLiteralExpression(value));
}
/*!
@ -184,7 +184,7 @@ namespace prism {
* @returns Boolean variable.
*/
std::shared_ptr<BaseExpression> getBoolVariable(const std::string name) {
return state->getBooleanVariable(name);
return state->getBooleanVariableExpression(name);
}
/*!
* Retrieve integer variable by name.
@ -192,7 +192,7 @@ namespace prism {
* @returns Integer variable.
*/
std::shared_ptr<BaseExpression> getIntVariable(const std::string name) {
return state->getIntegerVariable(name);
return state->getIntegerVariableExpression(name);
}
/*!

24
src/parser/prismparser/PrismGrammar.cpp
View File

@ -22,6 +22,7 @@
#include "src/parser/prismparser/IntegerExpressionGrammar.h"
#include "src/parser/prismparser/IdentifierGrammars.h"
#include "src/parser/prismparser/VariableState.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
@ -63,33 +64,34 @@ void PrismGrammar::addBooleanAssignment(std::string const& variable, std::shared
}
Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map<std::string, std::string>& renaming) {
this->state->moduleNames_.add(name, name);
Module* old = this->moduleMap_.find(oldname);
this->state->moduleNames_.add(newName, newName);
Module* old = this->moduleMap_.find(oldName);
if (old == nullptr) {
LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldName << " does not exist.");
throw storm::exceptions::InvalidArgumentException() << "Renaming module failed: module " << oldName << " does not exist.";
}
Module res(*old, newName, renaming, this->state);
this->moduleMap_.at(name) = res;
Module res(*old, newName, renaming, *this->state);
this->moduleMap_.at(newName) = res;
return res;
}
Module PrismGrammar::createModule(const std::string name, std::vector<BooleanVariable>& bools, std::vector<IntegerVariable>& ints, std::map<std::string, uint_fast64_t>& boolids, std::map<std::string, uint_fast64_t> intids, std::vector<storm::ir::Command> commands) {
Module PrismGrammar::createModule(std::string const& name, std::vector<BooleanVariable> const& bools, std::vector<IntegerVariable> const& ints, std::map<std::string, uint_fast64_t> const& boolids, std::map<std::string, uint_fast64_t> const& intids, std::vector<storm::ir::Command> const& commands) {
this->state->moduleNames_.add(name, name);
Module res(name, bools, ints, boolids, intids, commands);
this->moduleMap_.at(name) = res;
return res;
}
void PrismGrammar::createIntegerVariable(const std::string name, std::shared_ptr<BaseExpression> lower, std::shared_ptr<BaseExpression> upper, std::shared_ptr<BaseExpression> init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids) {
void PrismGrammar::createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids) {
uint_fast64_t id = this->state->addIntegerVariable(name);
vars.emplace_back(id, name, lower, upper, init);
vars.emplace_back(this->state->nextLocalIntegerVariableIndex++, id, name, lower, upper, init);
varids[name] = id;
this->state->localIntegerVariables_.add(name, name);
}
void PrismGrammar::createBooleanVariable(const std::string name, std::shared_ptr<BaseExpression> init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids) {
void PrismGrammar::createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids) {
uint_fast64_t id = this->state->addBooleanVariable(name);
vars.emplace_back(id, name, init);
vars.emplace_back(this->state->nextLocalIntegerVariableIndex++, id, name, init);
varids[name] = id;
this->state->localBooleanVariables_.add(name, name);
}
@ -148,8 +150,8 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl
// This block defines all entities that are needed for parsing a single command.
assignmentDefinition =
(qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > IntegerExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addIntAssignment, this, qi::_1, qi::_2, qi::_r2)] |
(qi::lit("(") >> unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addBoolAssignment, this, qi::_1, qi::_2, qi::_r1)];
(qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > IntegerExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addIntegerAssignment, this, qi::_1, qi::_2, qi::_r2)] |
(qi::lit("(") >> unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addBooleanAssignment, this, qi::_1, qi::_2, qi::_r1)];
assignmentDefinition.name("assignment");
assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&";
assignmentDefinitionList.name("assignment list");

8
src/parser/prismparser/PrismGrammar.h
View File

@ -192,7 +192,7 @@ private:
* @param integerVariableToLocalIndexMap A mapping of boolean variables to module-local indices.
* @param commands The commands associated with this module.
*/
Module createModule(std::string const& name, std::vector<BooleanVariable> const& booleanVariables, std::vector<IntegerVariable> const& integerVariables, std::map<std::string, uint_fast64_t> const& booleanVariableToLocalIndexMap, std::map<std::string, uint_fast64_t> integerVariableToLocalIndexMap, std::vector<storm::ir::Command> const& commands);
Module createModule(std::string const& name, std::vector<BooleanVariable> const& booleanVariables, std::vector<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);
/*!
* Creates an integer variable with the given name, domain and initial value and adds it to the
@ -202,10 +202,9 @@ private:
* @param lower The expression that defines the lower bound of the domain.
* @param upper The expression that defines the upper bound of the domain.
* @param init The expression that defines the initial value of the variable.
* @param integerVariableToLocalIndexMap A mapping of integer variables to local indices.
* @param integerVariableToGlobalIndexMap A mapping of integer variables to global indices.
*/
void createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& integerVariables, std::map<std::string, uint_fast64_t>& integerVariableToLocalIndexMap, std::map<std::string, uint_fast64_t>& integerVariableToGlobalIndexMap);
void createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& integerVariables, std::map<std::string, uint_fast64_t>& integerVariableToGlobalIndexMap);
/*!
* Creates an boolean variable with the given name and initial value and adds it to the
@ -213,10 +212,9 @@ private:
*
* @param name The name of the boolean variable.
* @param init The expression that defines the initial value of the variable.
* @param booleanVariableToLocalIndexMap A mapping of boolean variables to local indices.
* @param booleanVariableToGlobalIndexMap A mapping of boolean variables to global indices.
*/
void createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& booleanVariables, std::map<std::string, uint_fast64_t>& booleanVariableToLocalIndexMap, std::map<std::string, uint_fast64_t>& booleanVariableToGlobalIndexMap);
void createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& booleanVariables, std::map<std::string, uint_fast64_t>& booleanVariableToGlobalIndexMap);
};

22
src/parser/prismparser/VariableState.cpp
View File

@ -51,18 +51,18 @@ uint_fast64_t VariableState::getNextGlobalIntegerVariableIndex() const {
return this->nextGlobalIntegerVariableIndex;
}
std::pair<uint_fast64_t, uint_fast64_t> VariableState::addBooleanVariable(std::string const& name) {
uint_fast64_t VariableState::addBooleanVariable(std::string const& name) {
if (firstRun) {
LOG4CPLUS_TRACE(logger, "Adding boolean variable " << name << " with new id " << this->nextGlobalBooleanVariableIndex << ".");
this->booleanVariables_.add(name, std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextLocalBooleanVariableIndex, this->nextGlobalBooleanVariableIndex, name)));
this->booleanVariables_.add(name, std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextGlobalBooleanVariableIndex, name)));
this->booleanVariableNames_.add(name, name);
++this->nextGlobalBooleanVariableIndex;
++this->nextLocalBooleanVariableIndex;
return std::make_pair(this->nextLocalBooleanVariableIndex - 1, this->nextGlobalBooleanVariableIndex - 1);
return this->nextGlobalBooleanVariableIndex - 1;
} else {
std::shared_ptr<VariableExpression> variableExpression = this->booleanVariables_.at(name);
if (variableExpression != nullptr) {
return std::make_pair(variableExpression->getLocalVariableIndex(), variableExpression->getGlobalVariableIndex());
return variableExpression->getGlobalVariableIndex();
} else {
LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist.");
throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist.";
@ -70,18 +70,18 @@ std::pair<uint_fast64_t, uint_fast64_t> VariableState::addBooleanVariable(std::s
}
}
std::pair<uint_fast64_t, uint_fast64_t> VariableState::addIntegerVariable(std::string const& name) {
uint_fast64_t VariableState::addIntegerVariable(std::string const& name) {
if (firstRun) {
LOG4CPLUS_TRACE(logger, "Adding integer variable " << name << " with new id " << this->nextGlobalIntegerVariableIndex << ".");
this->integerVariables_.add(name, std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextLocalIntegerVariableIndex, this->nextGlobalIntegerVariableIndex, name)));
this->integerVariables_.add(name, std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextGlobalIntegerVariableIndex, name)));
this->integerVariableNames_.add(name, name);
++this->nextGlobalIntegerVariableIndex;
++this->nextLocalIntegerVariableIndex;
return std::make_pair(this->nextLocalIntegerVariableIndex, this->nextGlobalIntegerVariableIndex - 1);
return this->nextGlobalIntegerVariableIndex - 1;
} else {
std::shared_ptr<VariableExpression> variableExpression = this->integerVariables_.at(name);
if (variableExpression != nullptr) {
return std::make_pair(variableExpression->getLocalVariableIndex(), variableExpression->getGlobalVariableIndex());
return variableExpression->getGlobalVariableIndex();
} else {
LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist.");
throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist.";
@ -90,7 +90,7 @@ std::pair<uint_fast64_t, uint_fast64_t> VariableState::addIntegerVariable(std::s
}
std::shared_ptr<VariableExpression> VariableState::getBooleanVariableExpression(std::string const& name) const {
std::shared_ptr<VariableExpression>* variableExpression = this->booleanVariables_.find(name);
std::shared_ptr<VariableExpression> const* variableExpression = this->booleanVariables_.find(name);
if (variableExpression != nullptr) {
return *variableExpression;
} else {
@ -105,7 +105,7 @@ std::shared_ptr<VariableExpression> VariableState::getBooleanVariableExpression(
}
std::shared_ptr<VariableExpression> VariableState::getIntegerVariableExpression(std::string const& name) const {
std::shared_ptr<VariableExpression>* variableExpression = this->integerVariables_.find(name);
std::shared_ptr<VariableExpression> const* variableExpression = this->integerVariables_.find(name);
if (variableExpression != nullptr) {
return *variableExpression;
} else {
@ -120,7 +120,7 @@ std::shared_ptr<VariableExpression> VariableState::getIntegerVariableExpression(
}
std::shared_ptr<VariableExpression> VariableState::getVariableExpression(std::string const& name) const {
std::shared_ptr<VariableExpression>* variableExpression = this->integerVariables_.find(name);
std::shared_ptr<VariableExpression> const* variableExpression = this->integerVariables_.find(name);
if (variableExpression != nullptr) {
return *variableExpression;
}

12
src/parser/prismparser/VariableState.h
View File

@ -29,8 +29,8 @@ std::ostream& operator<<(std::ostream& out, qi::symbols<char, T>& symbols);
/*!
* This class contains the internal state that is needed for parsing a PRISM model.
*/
struct VariableState {
class VariableState {
public:
/*!
* Creates a new variable state object. By default, this object will be set to a state in which
* it is ready for performing a first run on some input. The first run creates all variables
@ -113,17 +113,17 @@ struct VariableState {
* Adds a new boolean variable with the given name.
*
* @param name The name of the variable.
* @return A pair containing the local and global index of the variable.
* @return The global index of the variable.
*/
virtual std::pair<uint_fast64_t, uint_fast64_t> addBooleanVariable(std::string const& name);
uint_fast64_t addBooleanVariable(std::string const& name);
/*!
* Adds a new integer variable with the given name.
*
* @param name The name of the variable.
* @return A pair containing the local and global index of the variable.
* @return The global index of the variable.
*/
virtual std::pair<uint_fast64_t, uint_fast64_t> addIntegerVariable(std::string const& name);
uint_fast64_t addIntegerVariable(std::string const& name);
/*!
* Retrieves the variable expression for the boolean variable with the given name.

Write Preview
Loading…
Cancel
Save