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

Major change in PRISM grammars and IR: the IR now uses unique pointers instead of shared pointers to express ownership of objects more clearly. 

Former-commit-id: 5b0228ee3b
main
dehnert 12 years ago
parent
20ae92e1ba
commit
f7a578e65d
65 changed files with 1116 additions and 809 deletions
Split View
  1. 8
      src/adapters/ExplicitModelAdapter.h
  2. 2
      src/adapters/SymbolicExpressionAdapter.h
  3. 21
      src/ir/Assignment.cpp
  4. 20
      src/ir/Assignment.h
  5. 12
      src/ir/BooleanVariable.cpp
  6. 4
      src/ir/BooleanVariable.h
  7. 25
      src/ir/Command.cpp
  8. 15
      src/ir/Command.h
  9. 36
      src/ir/IntegerVariable.cpp
  10. 19
      src/ir/IntegerVariable.h
  11. 3
      src/ir/Module.h
  12. 94
      src/ir/Program.cpp
  13. 44
      src/ir/Program.h
  14. 74
      src/ir/StateReward.cpp
  15. 120
      src/ir/StateReward.h
  16. 83
      src/ir/TransitionReward.cpp
  17. 24
      src/ir/TransitionReward.h
  18. 25
      src/ir/Update.cpp
  19. 20
      src/ir/Update.h
  20. 31
      src/ir/Variable.cpp
  21. 20
      src/ir/Variable.h
  22. 4
      src/ir/expressions/BaseExpression.h
  23. 12
      src/ir/expressions/BinaryBooleanFunctionExpression.cpp
  24. 6
      src/ir/expressions/BinaryBooleanFunctionExpression.h
  25. 10
      src/ir/expressions/BinaryExpression.cpp
  26. 10
      src/ir/expressions/BinaryExpression.h
  27. 12
      src/ir/expressions/BinaryNumericalFunctionExpression.cpp
  28. 8
      src/ir/expressions/BinaryNumericalFunctionExpression.h
  29. 12
      src/ir/expressions/BinaryRelationExpression.cpp
  30. 6
      src/ir/expressions/BinaryRelationExpression.h
  31. 8
      src/ir/expressions/BooleanConstantExpression.cpp
  32. 4
      src/ir/expressions/BooleanConstantExpression.h
  33. 8
      src/ir/expressions/BooleanLiteralExpression.cpp
  34. 4
      src/ir/expressions/BooleanLiteralExpression.h
  35. 8
      src/ir/expressions/DoubleConstantExpression.cpp
  36. 4
      src/ir/expressions/DoubleConstantExpression.h
  37. 8
      src/ir/expressions/DoubleLiteralExpression.cpp
  38. 4
      src/ir/expressions/DoubleLiteralExpression.h
  39. 8
      src/ir/expressions/IntegerConstantExpression.cpp
  40. 4
      src/ir/expressions/IntegerConstantExpression.h
  41. 8
      src/ir/expressions/IntegerLiteralExpression.cpp
  42. 4
      src/ir/expressions/IntegerLiteralExpression.h
  43. 10
      src/ir/expressions/UnaryBooleanFunctionExpression.cpp
  44. 6
      src/ir/expressions/UnaryBooleanFunctionExpression.h
  45. 6
      src/ir/expressions/UnaryExpression.cpp
  46. 6
      src/ir/expressions/UnaryExpression.h
  47. 10
      src/ir/expressions/UnaryNumericalFunctionExpression.cpp
  48. 6
      src/ir/expressions/UnaryNumericalFunctionExpression.h
  49. 14
      src/ir/expressions/VariableExpression.cpp
  50. 4
      src/ir/expressions/VariableExpression.h
  51. 62
      src/parser/prismparser/BaseGrammar.h
  52. 72
      src/parser/prismparser/BooleanExpressionGrammar.cpp
  53. 2
      src/parser/prismparser/BooleanExpressionGrammar.h
  54. 2
      src/parser/prismparser/ConstBooleanExpressionGrammar.cpp
  55. 2
      src/parser/prismparser/ConstBooleanExpressionGrammar.h
  56. 2
      src/parser/prismparser/ConstDoubleExpressionGrammar.cpp
  57. 44
      src/parser/prismparser/ConstDoubleExpressionGrammar.h
  58. 64
      src/parser/prismparser/ConstIntegerExpressionGrammar.cpp
  59. 44
      src/parser/prismparser/ConstIntegerExpressionGrammar.h
  60. 38
      src/parser/prismparser/IdentifierGrammars.cpp
  61. 48
      src/parser/prismparser/IdentifierGrammars.h
  62. 58
      src/parser/prismparser/IntegerExpressionGrammar.cpp
  63. 52
      src/parser/prismparser/IntegerExpressionGrammar.h
  64. 469
      src/parser/prismparser/PrismGrammar.cpp
  65. 52
      src/parser/prismparser/PrismGrammar.h

8
src/adapters/ExplicitModelAdapter.h
View File

@ -518,13 +518,13 @@ namespace storm {
* @param program The program in which to undefine the constants.
*/
static void undefineUndefinedConstants(storm::ir::Program& program) {
for (auto nameExpressionPair : program.getBooleanUndefinedConstantExpressionsMap()) {
for (auto const& nameExpressionPair : program.getBooleanUndefinedConstantExpressionsMap()) {
nameExpressionPair.second->undefine();
}
for (auto nameExpressionPair : program.getIntegerUndefinedConstantExpressionsMap()) {
for (auto const& nameExpressionPair : program.getIntegerUndefinedConstantExpressionsMap()) {
nameExpressionPair.second->undefine();
}
for (auto nameExpressionPair : program.getDoubleUndefinedConstantExpressionsMap()) {
for (auto const& nameExpressionPair : program.getDoubleUndefinedConstantExpressionsMap()) {
nameExpressionPair.second->undefine();
}
}
@ -1115,7 +1115,7 @@ namespace storm {
* @return The state labeling of the given program.
*/
static storm::models::AtomicPropositionsLabeling buildStateLabeling(storm::ir::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) {
std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& labels = program.getLabels();
std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& labels = program.getLabels();
storm::models::AtomicPropositionsLabeling result(stateInformation.reachableStates.size(), labels.size() + 1);

2
src/adapters/SymbolicExpressionAdapter.h
View File

@ -26,7 +26,7 @@ public:
}
ADD* translateExpression(std::shared_ptr<storm::ir::expressions::BaseExpression> expression) {
ADD* translateExpression(std::unique_ptr<storm::ir::expressions::BaseExpression> const& expression) {
expression->accept(this);
return stack.top();
}

21
src/ir/Assignment.cpp
View File

@ -17,8 +17,8 @@ namespace storm {
// Nothing to do here.
}
Assignment::Assignment(std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& expression)
: variableName(variableName), expression(expression) {
Assignment::Assignment(std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& expression)
: variableName(variableName), expression(std::move(expression)) {
// Nothing to do here.
}
@ -30,11 +30,26 @@ namespace storm {
}
}
Assignment::Assignment(Assignment const& otherAssignment) : variableName(otherAssignment.variableName), expression() {
if (otherAssignment.expression != nullptr) {
expression = otherAssignment.expression->clone();
}
}
Assignment& Assignment::operator=(Assignment const& otherAssignment) {
if (this != &otherAssignment) {
this->variableName = otherAssignment.variableName;
this->expression = otherAssignment.expression->clone();
}
return *this;
}
std::string const& Assignment::getVariableName() const {
return variableName;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Assignment::getExpression() const {
std::unique_ptr<storm::ir::expressions::BaseExpression> const& Assignment::getExpression() const {
return expression;
}

20
src/ir/Assignment.h
View File

@ -38,7 +38,7 @@ namespace storm {
* @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);
Assignment(std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& expression);
/*!
* Creates a copy of the given assignment and performs the provided renaming.
@ -50,6 +50,20 @@ namespace storm {
*/
Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
/*!
* Performs a deep-copy of the given assignment.
*
* @param otherAssignment The assignment to copy.
*/
Assignment(Assignment const& otherAssignment);
/*!
* Performs a deep-copy of the given assignment and assigns it to the current one.
*
* @param otherAssignment The assignment to assign.
*/
Assignment& operator=(Assignment const& otherAssignment);
/*!
* Retrieves the name of the variable that this assignment targets.
*
@ -62,7 +76,7 @@ namespace storm {
*
* @return The expression that is assigned to the variable.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> const& getExpression() const;
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getExpression() const;
/*!
* Retrieves a string representation of this assignment.
@ -75,7 +89,7 @@ namespace storm {
std::string variableName;
// The expression that is assigned to the variable.
std::shared_ptr<storm::ir::expressions::BaseExpression> expression;
std::unique_ptr<storm::ir::expressions::BaseExpression> expression;
};
} // namespace ir

12
src/ir/BooleanVariable.cpp
View File

@ -17,8 +17,8 @@ namespace storm {
// 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) {
BooleanVariable::BooleanVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue)
: Variable(localIndex, globalIndex, variableName, std::move(initialValue)) {
// Nothing to do here.
}
@ -27,6 +27,14 @@ namespace storm {
// Nothing to do here.
}
BooleanVariable& BooleanVariable::operator=(BooleanVariable const& otherVariable) {
if (this != &otherVariable) {
Variable::operator=(otherVariable);
}
return *this;
}
std::string BooleanVariable::toString() const {
std::stringstream result;
result << this->getName() << ": bool";

4
src/ir/BooleanVariable.h
View File

@ -41,7 +41,7 @@ namespace storm {
* @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));
BooleanVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue = nullptr);
/*!
* Creates a copy of the given boolean variable and performs the provided renaming.
@ -55,6 +55,8 @@ namespace storm {
*/
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);
BooleanVariable& operator=(BooleanVariable const& otherVariable);
/*!
* Retrieves a string representation of this variable.
* @returns a string representation of this variable.

25
src/ir/Command.cpp
View File

@ -14,12 +14,12 @@
namespace storm {
namespace ir {
Command::Command() : actionName(), guardExpression(), updates() {
Command::Command() : actionName(), guardExpression(), updates(), globalIndex() {
// Nothing to do here.
}
Command::Command(uint_fast64_t globalIndex, 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), globalIndex(globalIndex) {
Command::Command(uint_fast64_t globalIndex, std::string const& actionName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& guardExpression, std::vector<storm::ir::Update> const& updates)
: actionName(actionName), guardExpression(std::move(guardExpression)), updates(updates), globalIndex(globalIndex) {
// Nothing to do here.
}
@ -36,11 +36,28 @@ namespace storm {
}
}
Command::Command(Command const& otherCommand) : actionName(otherCommand.actionName), guardExpression(), updates(otherCommand.updates), globalIndex(otherCommand.globalIndex) {
if (otherCommand.guardExpression != nullptr) {
guardExpression = otherCommand.guardExpression->clone();
}
}
Command& Command::operator=(Command const& otherCommand) {
if (this != &otherCommand) {
this->actionName = otherCommand.actionName;
this->guardExpression = otherCommand.guardExpression->clone();
this->updates = otherCommand.updates;
this->globalIndex = otherCommand.globalIndex;
}
return *this;
}
std::string const& Command::getActionName() const {
return this->actionName;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Command::getGuard() const {
std::unique_ptr<storm::ir::expressions::BaseExpression> const& Command::getGuard() const {
return guardExpression;
}

15
src/ir/Command.h
View File

@ -43,7 +43,7 @@ namespace storm {
* @param guardExpression the expression that defines the guard of the command.
* @param updates A list of updates that is associated with this command.
*/
Command(uint_fast64_t globalIndex, std::string const& actionName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> const& updates);
Command(uint_fast64_t globalIndex, std::string const& actionName, std::unique_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.
@ -56,6 +56,15 @@ namespace storm {
*/
Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState);
/*!
* Performs a deep-copy of the given command.
*
* @param otherCommand The command to copy.
*/
Command(Command const& otherCommand);
Command& operator=(Command const& otherCommand);
/*!
* Retrieves the action name of this command.
*
@ -68,7 +77,7 @@ namespace storm {
*
* @return A reference to the guard of the command.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> const& getGuard() const;
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getGuard() const;
/*!
* Retrieves the number of updates associated with this command.
@ -103,7 +112,7 @@ namespace storm {
std::string actionName;
// The expression that defines the guard of the command.
std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression;
std::unique_ptr<storm::ir::expressions::BaseExpression> guardExpression;
// The list of updates of the command.
std::vector<storm::ir::Update> updates;

36
src/ir/IntegerVariable.cpp
View File

@ -12,18 +12,15 @@
#include "src/parser/prismparser/VariableState.h"
namespace storm {
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(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& lowerBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& upperBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue)
: Variable(localIndex, globalIndex, variableName, std::move(initialValue)), lowerBound(std::move(lowerBound)), upperBound(std::move(upperBound)) {
// Nothing to do here.
}
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)
@ -31,11 +28,33 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getLowerBound() const {
IntegerVariable::IntegerVariable(IntegerVariable const& otherVariable) : Variable(otherVariable.getLocalIndex(), otherVariable.getGlobalIndex(), otherVariable.getName(), nullptr), lowerBound(), upperBound() {
if (otherVariable.getInitialValue() != nullptr) {
setInitialValue(otherVariable.getInitialValue()->clone());
}
if (otherVariable.lowerBound != nullptr) {
lowerBound = otherVariable.lowerBound->clone();
}
if (otherVariable.upperBound != nullptr) {
upperBound = otherVariable.upperBound->clone();
}
}
IntegerVariable& IntegerVariable::operator=(IntegerVariable const& otherVariable) {
if (this != &otherVariable) {
Variable::operator=(otherVariable);
this->lowerBound = otherVariable.lowerBound->clone();
this->upperBound = otherVariable.upperBound->clone();
}
return *this;
}
std::unique_ptr<storm::ir::expressions::BaseExpression> const& IntegerVariable::getLowerBound() const {
return this->lowerBound;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getUpperBound() const {
std::unique_ptr<storm::ir::expressions::BaseExpression> const& IntegerVariable::getUpperBound() const {
return this->upperBound;
}
@ -50,5 +69,4 @@ namespace storm {
}
} // namespace ir
} // namespace storm

19
src/ir/IntegerVariable.h
View File

@ -43,7 +43,7 @@ namespace storm {
* @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));
IntegerVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& lowerBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& upperBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue = nullptr);
/*!
* Creates a copy of the given integer variable and performs the provided renaming.
@ -57,17 +57,26 @@ namespace storm {
*/
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);
/*!
* Performs a deep-copy of the given variable.
*
* @param otherVariable The variable to copy.
*/
IntegerVariable(IntegerVariable const& otherVariable);
IntegerVariable& operator=(IntegerVariable const& otherVariable);
/*!
* 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;
std::unique_ptr<storm::ir::expressions::BaseExpression> const& 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;
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getUpperBound() const;
/*!
* Retrieves a string representation of this variable.
@ -77,10 +86,10 @@ namespace storm {
private:
// The lower bound of the domain of the variable.
std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound;
std::unique_ptr<storm::ir::expressions::BaseExpression> lowerBound;
// The upper bound of the domain of the variable.
std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound;
std::unique_ptr<storm::ir::expressions::BaseExpression> upperBound;
};
} // namespace ir

3
src/ir/Module.h
View File

@ -61,9 +61,6 @@ namespace storm {
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.

94
src/ir/Program.cpp
View File

@ -24,17 +24,34 @@ namespace storm {
}
Program::Program(ModelType modelType,
std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> const& booleanUndefinedConstantExpressions,
std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> const& integerUndefinedConstantExpressions,
std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> const& doubleUndefinedConstantExpressions,
std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& booleanUndefinedConstantExpressions,
std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& integerUndefinedConstantExpressions,
std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& doubleUndefinedConstantExpressions,
std::vector<BooleanVariable> const& globalBooleanVariables,
std::vector<IntegerVariable> const& globalIntegerVariables,
std::map<std::string, uint_fast64_t> const& globalBooleanVariableToIndexMap,
std::map<std::string, uint_fast64_t> const& globalIntegerVariableToIndexMap,
std::vector<storm::ir::Module> const& modules,
std::map<std::string, storm::ir::RewardModel> const& rewards,
std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& labels)
: modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), globalBooleanVariableToIndexMap(globalBooleanVariableToIndexMap), globalIntegerVariableToIndexMap(globalIntegerVariableToIndexMap), modules(modules), rewards(rewards), labels(labels), actionsToModuleIndexMap(), variableToModuleIndexMap() {
std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& labels)
: modelType(modelType), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables),
globalBooleanVariableToIndexMap(globalBooleanVariableToIndexMap), globalIntegerVariableToIndexMap(globalIntegerVariableToIndexMap),
modules(modules), rewards(rewards), actionsToModuleIndexMap(), variableToModuleIndexMap() {
// Perform a deep-copy of the maps.
for (auto const& booleanUndefinedConstant : booleanUndefinedConstantExpressions) {
this->booleanUndefinedConstantExpressions[booleanUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>(new storm::ir::expressions::BooleanConstantExpression(*booleanUndefinedConstant.second));
}
for (auto const& integerUndefinedConstant : integerUndefinedConstantExpressions) {
this->integerUndefinedConstantExpressions[integerUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>(new storm::ir::expressions::IntegerConstantExpression(*integerUndefinedConstant.second));
}
for (auto const& doubleUndefinedConstant : doubleUndefinedConstantExpressions) {
this->doubleUndefinedConstantExpressions[doubleUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>(new storm::ir::expressions::DoubleConstantExpression(*doubleUndefinedConstant.second));
}
for (auto const& label : labels) {
this->labels[label.first] = label.second->clone();
}
// Now build the mapping from action names to module indices so that the lookup can later be performed quickly.
for (unsigned int moduleIndex = 0; moduleIndex < this->modules.size(); moduleIndex++) {
Module const& module = this->modules[moduleIndex];
@ -57,6 +74,55 @@ namespace storm {
}
}
Program::Program(Program const& otherProgram) : modelType(otherProgram.modelType), globalBooleanVariables(otherProgram.globalBooleanVariables),
globalIntegerVariables(otherProgram.globalIntegerVariables), globalBooleanVariableToIndexMap(otherProgram.globalBooleanVariableToIndexMap),
globalIntegerVariableToIndexMap(otherProgram.globalIntegerVariableToIndexMap), modules(otherProgram.modules), rewards(otherProgram.rewards),
actionsToModuleIndexMap(), variableToModuleIndexMap() {
// Perform deep-copy of the maps.
for (auto const& booleanUndefinedConstant : otherProgram.booleanUndefinedConstantExpressions) {
this->booleanUndefinedConstantExpressions[booleanUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>(new storm::ir::expressions::BooleanConstantExpression(*booleanUndefinedConstant.second));
}
for (auto const& integerUndefinedConstant : otherProgram.integerUndefinedConstantExpressions) {
this->integerUndefinedConstantExpressions[integerUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>(new storm::ir::expressions::IntegerConstantExpression(*integerUndefinedConstant.second));
}
for (auto const& doubleUndefinedConstant : otherProgram.doubleUndefinedConstantExpressions) {
this->doubleUndefinedConstantExpressions[doubleUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>(new storm::ir::expressions::DoubleConstantExpression(*doubleUndefinedConstant.second));
}
for (auto const& label : otherProgram.labels) {
this->labels[label.first] = label.second->clone();
}
}
Program& Program::operator=(Program const& otherProgram) {
if (this != &otherProgram) {
this->modelType = otherProgram.modelType;
this->globalBooleanVariables = otherProgram.globalBooleanVariables;
this->globalIntegerVariables = otherProgram.globalIntegerVariables;
this->globalBooleanVariableToIndexMap = otherProgram.globalBooleanVariableToIndexMap;
this->globalIntegerVariableToIndexMap = otherProgram.globalIntegerVariableToIndexMap;
this->modules = otherProgram.modules;
this->rewards = otherProgram.rewards;
this->actionsToModuleIndexMap = otherProgram.actionsToModuleIndexMap;
this->variableToModuleIndexMap = otherProgram.variableToModuleIndexMap;
// Perform deep-copy of the maps.
for (auto const& booleanUndefinedConstant : otherProgram.booleanUndefinedConstantExpressions) {
this->booleanUndefinedConstantExpressions[booleanUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>(new storm::ir::expressions::BooleanConstantExpression(*booleanUndefinedConstant.second));
}
for (auto const& integerUndefinedConstant : otherProgram.integerUndefinedConstantExpressions) {
this->integerUndefinedConstantExpressions[integerUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>(new storm::ir::expressions::IntegerConstantExpression(*integerUndefinedConstant.second));
}
for (auto const& doubleUndefinedConstant : otherProgram.doubleUndefinedConstantExpressions) {
this->doubleUndefinedConstantExpressions[doubleUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>(new storm::ir::expressions::DoubleConstantExpression(*doubleUndefinedConstant.second));
}
for (auto const& label : otherProgram.labels) {
this->labels[label.first] = label.second->clone();
}
}
return *this;
}
Program::ModelType Program::getModelType() const {
return modelType;
}
@ -160,7 +226,7 @@ namespace storm {
return nameRewardModelPair->second;
}
std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& Program::getLabels() const {
std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& Program::getLabels() const {
return this->labels;
}
@ -168,7 +234,7 @@ namespace storm {
return this->booleanUndefinedConstantExpressions.find(constantName) != this->booleanUndefinedConstantExpressions.end();
}
std::shared_ptr<storm::ir::expressions::BooleanConstantExpression> Program::getUndefinedBooleanConstantExpression(std::string const& constantName) const {
std::unique_ptr<storm::ir::expressions::BooleanConstantExpression> const& Program::getUndefinedBooleanConstantExpression(std::string const& constantName) const {
auto constantExpressionPair = this->booleanUndefinedConstantExpressions.find(constantName);
if (constantExpressionPair != this->booleanUndefinedConstantExpressions.end()) {
return constantExpressionPair->second;
@ -181,7 +247,7 @@ namespace storm {
return this->integerUndefinedConstantExpressions.find(constantName) != this->integerUndefinedConstantExpressions.end();
}
std::shared_ptr<storm::ir::expressions::IntegerConstantExpression> Program::getUndefinedIntegerConstantExpression(std::string const& constantName) const {
std::unique_ptr<storm::ir::expressions::IntegerConstantExpression> const& Program::getUndefinedIntegerConstantExpression(std::string const& constantName) const {
auto constantExpressionPair = this->integerUndefinedConstantExpressions.find(constantName);
if (constantExpressionPair != this->integerUndefinedConstantExpressions.end()) {
return constantExpressionPair->second;
@ -194,7 +260,7 @@ namespace storm {
return this->doubleUndefinedConstantExpressions.find(constantName) != this->doubleUndefinedConstantExpressions.end();
}
std::shared_ptr<storm::ir::expressions::DoubleConstantExpression> Program::getUndefinedDoubleConstantExpression(std::string const& constantName) const {
std::unique_ptr<storm::ir::expressions::DoubleConstantExpression> const& Program::getUndefinedDoubleConstantExpression(std::string const& constantName) const {
auto constantExpressionPair = this->doubleUndefinedConstantExpressions.find(constantName);
if (constantExpressionPair != this->doubleUndefinedConstantExpressions.end()) {
return constantExpressionPair->second;
@ -203,22 +269,22 @@ namespace storm {
}
}
std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> const& Program::getBooleanUndefinedConstantExpressionsMap() const {
std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& Program::getBooleanUndefinedConstantExpressionsMap() const {
return this->booleanUndefinedConstantExpressions;
}
std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> const& Program::getIntegerUndefinedConstantExpressionsMap() const {
std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& Program::getIntegerUndefinedConstantExpressionsMap() const {
return this->integerUndefinedConstantExpressions;
}
std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> const& Program::getDoubleUndefinedConstantExpressionsMap() const {
std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& Program::getDoubleUndefinedConstantExpressionsMap() const {
return this->doubleUndefinedConstantExpressions;
}
uint_fast64_t Program::getGlobalIndexOfBooleanVariable(std::string const& variableName) const {
return this->globalBooleanVariableToIndexMap.at(variableName);
}
uint_fast64_t Program::getGlobalIndexOfIntegerVariable(std::string const& variableName) const {
return this->globalIntegerVariableToIndexMap.at(variableName);
}

44
src/ir/Program.h
View File

@ -60,16 +60,30 @@ namespace storm {
* @param labels The labels defined for this model.
*/
Program(ModelType modelType,
std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> const& booleanUndefinedConstantExpressions,
std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> const& integerUndefinedConstantExpressions,
std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> const& doubleUndefinedConstantExpressions,
std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& booleanUndefinedConstantExpressions,
std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& integerUndefinedConstantExpressions,
std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& doubleUndefinedConstantExpressions,
std::vector<BooleanVariable> const& globalBooleanVariables,
std::vector<IntegerVariable> const& globalIntegerVariables,
std::map<std::string, uint_fast64_t> const& globalBooleanVariableToIndexMap,
std::map<std::string, uint_fast64_t> const& globalIntegerVariableToIndexMap,
std::vector<storm::ir::Module> const& modules,
std::map<std::string, storm::ir::RewardModel> const& rewards,
std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& labels);
std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& labels);
/*!
* Performs a deep-copy of the given program.
*
* @param otherProgram The program to copy.
*/
Program(Program const& otherProgram);
/*!
* Performs a deep-copy of the given program and assigns it to the current one.
*
* @param otherProgram The program to assign.
*/
Program& operator=(Program const& otherProgram);
/*!
* Retrieves the number of modules in the program.
@ -165,7 +179,7 @@ namespace storm {
*
* @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;
std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& getLabels() const;
/*!
* Retrieves whether the given constant name is an undefined boolean constant of the program.
@ -180,7 +194,7 @@ namespace storm {
* @param constantName The name of the undefined boolean constant for which to retrieve the expression.
* @return The expression associated with the given undefined boolean constant.
*/
std::shared_ptr<storm::ir::expressions::BooleanConstantExpression> getUndefinedBooleanConstantExpression(std::string const& constantName) const;
std::unique_ptr<storm::ir::expressions::BooleanConstantExpression> const& getUndefinedBooleanConstantExpression(std::string const& constantName) const;
/*!
* Retrieves whether the given constant name is an undefined integer constant of the program.
@ -195,7 +209,7 @@ namespace storm {
* @param constantName The name of the undefined integer constant for which to retrieve the expression.
* @return The expression associated with the given undefined integer constant.
*/
std::shared_ptr<storm::ir::expressions::IntegerConstantExpression> getUndefinedIntegerConstantExpression(std::string const& constantName) const;
std::unique_ptr<storm::ir::expressions::IntegerConstantExpression> const& getUndefinedIntegerConstantExpression(std::string const& constantName) const;
/*!
* Retrieves whether the given constant name is an undefined double constant of the program.
@ -210,28 +224,28 @@ namespace storm {
* @param constantName The name of the undefined double constant for which to retrieve the expression.
* @return The expression associated with the given undefined double constant.
*/
std::shared_ptr<storm::ir::expressions::DoubleConstantExpression> getUndefinedDoubleConstantExpression(std::string const& constantName) const;
std::unique_ptr<storm::ir::expressions::DoubleConstantExpression> const& getUndefinedDoubleConstantExpression(std::string const& constantName) const;
/*!
* Retrieves the mapping of undefined boolean constant names to their expression objects.
*
* @return The mapping of undefined boolean constant names to their expression objects.
*/
std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> const& getBooleanUndefinedConstantExpressionsMap() const;
std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& getBooleanUndefinedConstantExpressionsMap() const;
/*!
* Retrieves the mapping of undefined integer constant names to their expression objects.
*
* @return The mapping of undefined integer constant names to their expression objects.
*/
std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> const& getIntegerUndefinedConstantExpressionsMap() const;
std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& getIntegerUndefinedConstantExpressionsMap() const;
/*!
* Retrieves the mapping of undefined double constant names to their expression objects.
*
* @return The mapping of undefined double constant names to their expression objects.
*/
std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> const& getDoubleUndefinedConstantExpressionsMap() const;
std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& getDoubleUndefinedConstantExpressionsMap() const;
/*!
* Retrieves the global index of the given boolean variable.
@ -252,13 +266,13 @@ namespace storm {
ModelType modelType;
// A map of undefined boolean constants to their expression nodes.
std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions;
std::map<std::string, std::unique_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;
std::map<std::string, std::unique_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;
std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions;
// A list of global boolean variables.
std::vector<BooleanVariable> globalBooleanVariables;
@ -279,7 +293,7 @@ namespace storm {
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;
std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> labels;
// The set of actions present in this program.
std::set<std::string> actions;

74
src/ir/StateReward.cpp
View File

@ -10,31 +10,51 @@
#include "StateReward.h"
namespace storm {
namespace ir {
StateReward::StateReward() : statePredicate(), rewardValue() {
// Nothing to do here.
}
StateReward::StateReward(std::shared_ptr<storm::ir::expressions::BaseExpression> const& statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> const& rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) {
// Nothing to do here.
}
std::string StateReward::toString() const {
std::stringstream result;
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 ir {
StateReward::StateReward() : statePredicate(), rewardValue() {
// Nothing to do here.
}
StateReward::StateReward(std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue) : statePredicate(std::move(statePredicate)), rewardValue(std::move(rewardValue)) {
// Nothing to do here.
}
StateReward::StateReward(StateReward const& otherReward) {
if (otherReward.statePredicate != nullptr) {
statePredicate = otherReward.statePredicate->clone();
}
if (otherReward.rewardValue != nullptr) {
rewardValue = otherReward.rewardValue->clone();
}
}
StateReward& StateReward::operator=(StateReward const& otherReward) {
if (this != & otherReward) {
if (otherReward.statePredicate != nullptr) {
this->statePredicate = otherReward.statePredicate->clone();
}
if (otherReward.rewardValue != nullptr) {
this->rewardValue = otherReward.rewardValue->clone();
}
}
return *this;
}
std::string StateReward::toString() const {
std::stringstream result;
result << "\t" << statePredicate->toString() << ": " << rewardValue->toString() << ";";
return result.str();
}
std::unique_ptr<storm::ir::expressions::BaseExpression> const& StateReward::getStatePredicate() const {
return this->statePredicate;
}
std::unique_ptr<storm::ir::expressions::BaseExpression> const& StateReward::getRewardValue() const {
return this->rewardValue;
}
} // namespace ir
} // namespace storm

120
src/ir/StateReward.h
View File

@ -13,61 +13,73 @@
#include "expressions/BaseExpression.h"
namespace storm {
namespace ir {
/*!
* A class representing a state reward.
*/
class StateReward {
public:
/*!
* Default constructor. Creates an empty state reward.
*/
StateReward();
/*!
* Creates a state reward for the states satisfying the given expression with the value given
* by a second expression.
*
* @param statePredicate The predicate that states earning this state-based reward need to
* satisfy.
* @param rewardValue An expression specifying the values of the rewards to attach to the
* states.
*/
StateReward(std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue);
/*!
* Performs a deep-copy of the given reward.
*
* @param otherReward The reward to copy.
*/
StateReward(StateReward const& otherReward);
namespace ir {
/*!
* A class representing a state reward.
*/
class StateReward {
public:
/*!
* Default constructor. Creates an empty state reward.
*/
StateReward();
/*!
* Creates a state reward for the states satisfying the given expression with the value given
* by a second expression.
*
* @param statePredicate The predicate that states earning this state-based reward need to
* satisfy.
* @param rewardValue An expression specifying the values of the rewards to attach to the
* states.
*/
StateReward(std::shared_ptr<storm::ir::expressions::BaseExpression> const& statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> const& rewardValue);
/*!
* Retrieves a string representation of this state reward.
*
* @return A string representation of this state reward.
*/
std::string toString() const;
/*!
* Retrieves the state predicate that is associated with this state reward.
*
* @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;
// The expression that specifies the value of the reward obtained.
std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue;
};
} // namespace ir
/*!
* Performs a deep-copy of the given reward and assigns it to the current one.
*
* @param otherReward The reward to assign.
*/
StateReward& operator=(StateReward const& otherReward);
/*!
* Retrieves a string representation of this state reward.
*
* @return A string representation of this state reward.
*/
std::string toString() const;
/*!
* Retrieves the state predicate that is associated with this state reward.
*
* @return The state predicate that is associated with this state reward.
*/
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getStatePredicate() const;
/*!
* Retrieves the reward value associated with this state reward.
*
* @return The reward value associated with this state reward.
*/
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getRewardValue() const;
private:
// The predicate that characterizes the states that obtain this reward.
std::unique_ptr<storm::ir::expressions::BaseExpression> statePredicate;
// The expression that specifies the value of the reward obtained.
std::unique_ptr<storm::ir::expressions::BaseExpression> rewardValue;
};
} // namespace ir
} // namespace storm
#endif /* STORM_IR_STATEREWARD_H_ */

83
src/ir/TransitionReward.cpp
View File

@ -10,35 +10,56 @@
#include "TransitionReward.h"
namespace storm {
namespace ir {
TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardValue() {
// Nothing to do here.
}
TransitionReward::TransitionReward(std::string const& commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> const& rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) {
// Nothing to do here.
}
std::string TransitionReward::toString() const {
std::stringstream result;
result << "\t[" << commandName << "] " << statePredicate->toString() << ": " << rewardValue->toString() << ";";
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 ir {
TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardValue() {
// Nothing to do here.
}
TransitionReward::TransitionReward(std::string const& commandName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue) : commandName(commandName), statePredicate(std::move(statePredicate)), rewardValue(std::move(rewardValue)) {
// Nothing to do here.
}
TransitionReward::TransitionReward(TransitionReward const& otherReward) : commandName(otherReward.commandName), statePredicate(), rewardValue() {
if (otherReward.statePredicate != nullptr) {
statePredicate = otherReward.statePredicate->clone();
}
if (otherReward.rewardValue != nullptr) {
rewardValue = otherReward.rewardValue->clone();
}
}
TransitionReward& TransitionReward::operator=(TransitionReward const& otherReward) {
if (this != &otherReward) {
this->commandName = otherReward.commandName;
if (otherReward.statePredicate != nullptr) {
this->statePredicate = otherReward.statePredicate->clone();
}
if (otherReward.rewardValue != nullptr) {
this->rewardValue = otherReward.rewardValue->clone();
}
}
return *this;
}
std::string TransitionReward::toString() const {
std::stringstream result;
result << "\t[" << commandName << "] " << statePredicate->toString() << ": " << rewardValue->toString() << ";";
return result.str();
}
std::string const& TransitionReward::getActionName() const {
return this->commandName;
}
std::unique_ptr<storm::ir::expressions::BaseExpression> const& TransitionReward::getStatePredicate() const {
return this->statePredicate;
}
std::unique_ptr<storm::ir::expressions::BaseExpression> const& TransitionReward::getRewardValue() const {
return this->rewardValue;
}
} // namespace ir
} // namespace storm

24
src/ir/TransitionReward.h
View File

@ -36,8 +36,22 @@ public:
* @param rewardValue An expression specifying the values of the rewards to attach to the
* transitions.
*/
TransitionReward(std::string const& commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> const& rewardValue);
TransitionReward(std::string const& commandName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue);
/*!
* Performs a deep-copy of the given transition reward.
*
* @param otherReward The transition reward to copy.
*/
TransitionReward(TransitionReward const& otherReward);
/*!
* Performs a deep-copy of the given transition reward and assigns it to the current one.
*
* @param otherReward The reward to assign.
*/
TransitionReward& operator=(TransitionReward const& otherReward);
/*!
* Retrieves a string representation of this transition reward.
*
@ -57,14 +71,14 @@ public:
*
* @return The state predicate that is associated with this state reward.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> getStatePredicate() const;
std::unique_ptr<storm::ir::expressions::BaseExpression> const& 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;
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getRewardValue() const;
private:
// The name of the command this transition-based reward is attached to.
@ -72,10 +86,10 @@ private:
// A predicate that needs to be satisfied by states for the reward to be obtained (by taking
// a corresponding command transition).
std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate;
std::unique_ptr<storm::ir::expressions::BaseExpression> statePredicate;
// The expression specifying the value of the reward obtained along the transitions.
std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue;
std::unique_ptr<storm::ir::expressions::BaseExpression> rewardValue;
};
} // namespace ir

25
src/ir/Update.cpp
View File

@ -18,8 +18,8 @@ namespace storm {
// Nothing to do here.
}
Update::Update(uint_fast64_t globalIndex, 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), globalIndex(globalIndex) {
Update::Update(uint_fast64_t globalIndex, std::unique_ptr<storm::ir::expressions::BaseExpression>&& likelihoodExpression, std::map<std::string, storm::ir::Assignment> const& booleanAssignments, std::map<std::string, storm::ir::Assignment> const& integerAssignments)
: likelihoodExpression(std::move(likelihoodExpression)), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments), globalIndex(globalIndex) {
// Nothing to do here.
}
@ -41,7 +41,26 @@ namespace storm {
this->likelihoodExpression = update.likelihoodExpression->clone(renaming, variableState);
}
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Update::getLikelihoodExpression() const {
Update::Update(Update const& otherUpdate) : likelihoodExpression(), booleanAssignments(otherUpdate.booleanAssignments), integerAssignments(otherUpdate.integerAssignments), globalIndex(otherUpdate.globalIndex) {
if (otherUpdate.likelihoodExpression != nullptr) {
likelihoodExpression = otherUpdate.likelihoodExpression->clone();
}
}
Update& Update::operator=(Update const& otherUpdate) {
if (this != &otherUpdate) {
if (otherUpdate.likelihoodExpression != nullptr) {
this->likelihoodExpression = otherUpdate.likelihoodExpression->clone();
}
this->booleanAssignments = otherUpdate.booleanAssignments;
this->integerAssignments = otherUpdate.integerAssignments;
this->globalIndex = otherUpdate.globalIndex;
}
return *this;
}
std::unique_ptr<storm::ir::expressions::BaseExpression> const& Update::getLikelihoodExpression() const {
return likelihoodExpression;
}

20
src/ir/Update.h
View File

@ -42,7 +42,7 @@ namespace storm {
* @param likelihoodExpression An expression specifying the likelihood of this update.
* @param assignments A map of variable names to their assignments.
*/
Update(uint_fast64_t globalIndex, 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);
Update(uint_fast64_t globalIndex, std::unique_ptr<storm::ir::expressions::BaseExpression>&& 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.
@ -55,12 +55,26 @@ namespace storm {
*/
Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState);
/*!
* Peforms a deep-copy of the given update.
*
* @param otherUpdate The update to copy.
*/
Update(Update const& otherUpdate);
/*!
* Performs a deep-copy of the given update and assigns it to the current one.
*
* @param otherUpdate The update to assign.
*/
Update& operator=(Update const& otherUpdate);
/*!
* 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;
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getLikelihoodExpression() const;
/*!
* Retrieves the number of boolean assignments associated with this update.
@ -120,7 +134,7 @@ namespace storm {
private:
// An expression specifying the likelihood of taking this update.
std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression;
std::unique_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;

31
src/ir/Variable.cpp
View File

@ -19,18 +19,37 @@ namespace storm {
// 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) {
Variable::Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue)
: localIndex(localIndex), globalIndex(globalIndex), variableName(variableName), initialValue(std::move(initialValue)) {
// Nothing to do here.
}
Variable::Variable(Variable const& otherVariable) : localIndex(otherVariable.localIndex), globalIndex(otherVariable.globalIndex), variableName(otherVariable.variableName), initialValue() {
if (otherVariable.initialValue != nullptr) {
initialValue = otherVariable.initialValue->clone();
}
}
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(newName) {
: localIndex(var.getLocalIndex()), globalIndex(newGlobalIndex), variableName(newName), initialValue() {
if (var.initialValue != nullptr) {
this->initialValue = var.initialValue->clone(renaming, variableState);
}
}
Variable& Variable::operator=(Variable const& otherVariable) {
if (this != &otherVariable) {
this->localIndex = otherVariable.localIndex;
this->globalIndex = otherVariable.globalIndex;
this->variableName = otherVariable.variableName;
if (otherVariable.initialValue != nullptr) {
this->initialValue = otherVariable.initialValue->clone();
}
}
return *this;
}
std::string const& Variable::getName() const {
return variableName;
}
@ -43,12 +62,12 @@ namespace storm {
return localIndex;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Variable::getInitialValue() const {
std::unique_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;
void Variable::setInitialValue(std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue) {
this->initialValue = std::move(initialValue);
}
} // namespace ir

20
src/ir/Variable.h
View File

@ -41,7 +41,7 @@ namespace storm {
* @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>());
Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue = nullptr);
/*!
* Creates a copy of the given variable and performs the provided renaming.
@ -55,6 +55,18 @@ namespace storm {
*/
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);
/*!
* Creates a deep-copy of the given variable.
*
* @param otherVariable The variable to copy.
*/
Variable(Variable const& otherVariable);
/*!
* Creates a deep-copy of the given variable and assigns it to the current one.
*/
Variable& operator=(Variable const& otherVariable);
/*!
* Retrieves the name of the variable.
*
@ -83,14 +95,14 @@ namespace storm {
*
* @return The expression defining the initial value of the variable.
*/
std::shared_ptr<storm::ir::expressions::BaseExpression> const& getInitialValue() const;
std::unique_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);
void setInitialValue(std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue);
private:
// A unique (among the variables of equal type) index for the variable inside its module.
@ -103,7 +115,7 @@ namespace storm {
std::string variableName;
// The expression defining the initial value of the variable.
std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue;
std::unique_ptr<storm::ir::expressions::BaseExpression> initialValue;
};
} // namespace ir

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

@ -69,7 +69,7 @@ namespace storm {
*
* @return A deep-copy of the expression.
*/
virtual std::shared_ptr<BaseExpression> clone() const = 0;
virtual std::unique_ptr<BaseExpression> clone() const = 0;
/*!
* Copies the expression tree underneath (including) the current node and performs the provided renaming.
@ -77,7 +77,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, storm::parser::prism::VariableState const& variableState) const = 0;
virtual std::unique_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.

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

@ -13,8 +13,8 @@ namespace storm {
namespace ir {
namespace expressions {
BinaryBooleanFunctionExpression::BinaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, FunctionType functionType)
: BinaryExpression(bool_, left, right), functionType(functionType) {
BinaryBooleanFunctionExpression::BinaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType)
: BinaryExpression(bool_, std::move(left), std::move(right)), functionType(functionType) {
// Nothing to do here.
}
@ -23,12 +23,12 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone() const {
return std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(), this->getRight()->clone(), functionType));
std::unique_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone() const {
return std::unique_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(), this->getRight()->clone(), functionType));
}
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));
std::unique_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::unique_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType));
}
bool BinaryBooleanFunctionExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {

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

@ -31,7 +31,7 @@ namespace storm {
* @param right The right child of the node.
* @param functionType The operator that is to be applied to the two children.
*/
BinaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, FunctionType functionType);
BinaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType);
/*!
* Copy-constructs from the given expression.
@ -40,9 +40,9 @@ namespace storm {
*/
BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& binaryBooleanFunctionExpression);
virtual std::shared_ptr<BaseExpression> clone() const override;
virtual std::unique_ptr<BaseExpression> clone() 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 std::unique_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;

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

@ -11,20 +11,20 @@ namespace storm {
namespace ir {
namespace expressions {
BinaryExpression::BinaryExpression(ReturnType type, std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right)
: BaseExpression(type), left(left), right(right) {
BinaryExpression::BinaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right)
: BaseExpression(type), left(std::move(left)), right(std::move(right)) {
// Nothing to do here.
}
BinaryExpression::BinaryExpression(BinaryExpression const& binaryExpression) : BaseExpression(binaryExpression.getType()), left(binaryExpression.left), right(binaryExpression.right) {
BinaryExpression::BinaryExpression(BinaryExpression const& binaryExpression) : BaseExpression(binaryExpression.getType()), left(binaryExpression.left->clone()), right(binaryExpression.right->clone()) {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> const& BinaryExpression::getLeft() const {
std::unique_ptr<BaseExpression> const& BinaryExpression::getLeft() const {
return left;
}
std::shared_ptr<BaseExpression> const& BinaryExpression::getRight() const {
std::unique_ptr<BaseExpression> const& BinaryExpression::getRight() const {
return right;
}

10
src/ir/expressions/BinaryExpression.h
View File

@ -25,7 +25,7 @@ namespace storm {
* @param left The left child of the binary expression.
* @param right The right child of the binary expression.
*/
BinaryExpression(ReturnType type, std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right);
BinaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right);
/*!
* Copy-constructs from the given expression.
@ -39,21 +39,21 @@ namespace storm {
*
* @return The left child of the expression node.
*/
std::shared_ptr<BaseExpression> const& getLeft() const;
std::unique_ptr<BaseExpression> const& getLeft() const;
/*!
* Retrieves the right child of the expression node.
*
* @return The right child of the expression node.
*/
std::shared_ptr<BaseExpression> const& getRight() const;
std::unique_ptr<BaseExpression> const& getRight() const;
private:
// The left child of the binary expression.
std::shared_ptr<BaseExpression> left;
std::unique_ptr<BaseExpression> left;
// The right child of the binary expression.
std::shared_ptr<BaseExpression> right;
std::unique_ptr<BaseExpression> right;
};
} // namespace expressions

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

@ -13,8 +13,8 @@ namespace storm {
namespace ir {
namespace expressions {
BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, FunctionType functionType)
: BinaryExpression(type, left, right), functionType(functionType) {
BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType)
: BinaryExpression(type, std::move(left), std::move(right)), functionType(functionType) {
// Nothing to do here.
}
@ -23,12 +23,12 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone() const {
return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(), this->getRight()->clone(), functionType));
std::unique_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone() const {
return std::unique_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(), this->getRight()->clone(), functionType));
}
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));
std::unique_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::unique_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType));
}
BinaryNumericalFunctionExpression::FunctionType BinaryNumericalFunctionExpression::getFunctionType() const {

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

@ -32,18 +32,18 @@ namespace storm {
* @param right The right child of the expression tree node.
* @param functionType The function that is applied to the children of this node.
*/
BinaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, FunctionType functionType);
BinaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType);
/*!
* Copy-constructs from the given expression.
* Performs a deep-copy of the given expression.
*
* @param binaryNumericalFunctionExpression The expression to copy.
*/
BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& binaryNumericalFunctionExpression);
virtual std::shared_ptr<BaseExpression> clone() const override;
virtual std::unique_ptr<BaseExpression> clone() 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 std::unique_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.

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

@ -13,8 +13,8 @@ namespace storm {
namespace ir {
namespace expressions {
BinaryRelationExpression::BinaryRelationExpression(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, RelationType relationType)
: BinaryExpression(bool_, left, right), relationType(relationType) {
BinaryRelationExpression::BinaryRelationExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, RelationType relationType)
: BinaryExpression(bool_, std::move(left), std::move(right)), relationType(relationType) {
// Nothing to do here.
}
@ -23,12 +23,12 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> BinaryRelationExpression::clone() const {
return std::shared_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(), this->getRight()->clone(), relationType));
std::unique_ptr<BaseExpression> BinaryRelationExpression::clone() const {
return std::unique_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(), this->getRight()->clone(), relationType));
}
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));
std::unique_ptr<BaseExpression> BinaryRelationExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::unique_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->relationType));
}
bool BinaryRelationExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {

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

@ -31,7 +31,7 @@ namespace storm {
* @param right The right child of the binary expression.
* @param relationType The type of the relation associated with this node.
*/
BinaryRelationExpression(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, RelationType relationType);
BinaryRelationExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, RelationType relationType);
/*!
* Copy-constructs from the given expression.
@ -40,9 +40,9 @@ namespace storm {
*/
BinaryRelationExpression(BinaryRelationExpression const& binaryRelationExpression);
virtual std::shared_ptr<BaseExpression> clone() const override;
virtual std::unique_ptr<BaseExpression> clone() 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 std::unique_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;

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

@ -19,12 +19,12 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> BooleanConstantExpression::clone() const {
return std::shared_ptr<BaseExpression>(new BooleanConstantExpression(*this));
std::unique_ptr<BaseExpression> BooleanConstantExpression::clone() const {
return std::unique_ptr<BaseExpression>(new BooleanConstantExpression(*this));
}
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));
std::unique_ptr<BaseExpression> BooleanConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::unique_ptr<BaseExpression>(new BooleanConstantExpression(*this));
}
bool BooleanConstantExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {

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

@ -33,9 +33,9 @@ namespace storm {
*/
BooleanConstantExpression(BooleanConstantExpression const& booleanConstantExpression);
virtual std::shared_ptr<BaseExpression> clone() const override;
virtual std::unique_ptr<BaseExpression> clone() 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 std::unique_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;

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

@ -20,12 +20,12 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> BooleanLiteralExpression::clone() const {
return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(*this));
std::unique_ptr<BaseExpression> BooleanLiteralExpression::clone() const {
return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(*this));
}
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));
std::unique_ptr<BaseExpression> BooleanLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(this->value));
}
bool BooleanLiteralExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {

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

@ -33,9 +33,9 @@ namespace storm {
*/
BooleanLiteralExpression(BooleanLiteralExpression const& booleanLiteralExpression);
virtual std::shared_ptr<BaseExpression> clone() const override;
virtual std::unique_ptr<BaseExpression> clone() 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 std::unique_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;

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

@ -19,12 +19,12 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> DoubleConstantExpression::clone() const {
return std::shared_ptr<BaseExpression>(new DoubleConstantExpression(*this));
std::unique_ptr<BaseExpression> DoubleConstantExpression::clone() const {
return std::unique_ptr<BaseExpression>(new DoubleConstantExpression(*this));
}
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));
std::unique_ptr<BaseExpression> DoubleConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::unique_ptr<BaseExpression>(new DoubleConstantExpression(*this));
}
double DoubleConstantExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {

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

@ -33,9 +33,9 @@ namespace storm {
*/
DoubleConstantExpression(DoubleConstantExpression const& doubleConstantExpression);
virtual std::shared_ptr<BaseExpression> clone() const override;
virtual std::unique_ptr<BaseExpression> clone() 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 std::unique_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;

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

@ -22,12 +22,12 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> DoubleLiteralExpression::clone() const {
return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(*this));
std::unique_ptr<BaseExpression> DoubleLiteralExpression::clone() const {
return std::unique_ptr<BaseExpression>(new DoubleLiteralExpression(*this));
}
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));
std::unique_ptr<BaseExpression> DoubleLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::unique_ptr<BaseExpression>(new DoubleLiteralExpression(this->value));
}
double DoubleLiteralExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {

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

@ -33,9 +33,9 @@ namespace storm {
*/
DoubleLiteralExpression(DoubleLiteralExpression const& doubleLiteralExpression);
virtual std::shared_ptr<BaseExpression> clone() const override;
virtual std::unique_ptr<BaseExpression> clone() 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 std::unique_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;

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

@ -19,12 +19,12 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> IntegerConstantExpression::clone() const {
return std::shared_ptr<BaseExpression>(new IntegerConstantExpression(*this));
std::unique_ptr<BaseExpression> IntegerConstantExpression::clone() const {
return std::unique_ptr<BaseExpression>(new IntegerConstantExpression(*this));
}
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));
std::unique_ptr<BaseExpression> IntegerConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::unique_ptr<BaseExpression>(new IntegerConstantExpression(*this));
}
double IntegerConstantExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {

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

@ -33,9 +33,9 @@ namespace storm {
*/
IntegerConstantExpression(IntegerConstantExpression const& integerConstantExpression);
virtual std::shared_ptr<BaseExpression> clone() const override;
virtual std::unique_ptr<BaseExpression> clone() 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 std::unique_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;

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

@ -22,12 +22,12 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> IntegerLiteralExpression::clone() const {
return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(*this));
std::unique_ptr<BaseExpression> IntegerLiteralExpression::clone() const {
return std::unique_ptr<BaseExpression>(new IntegerLiteralExpression(*this));
}
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));
std::unique_ptr<BaseExpression> IntegerLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::unique_ptr<BaseExpression>(new IntegerLiteralExpression(this->value));
}
double IntegerLiteralExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {

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

@ -33,9 +33,9 @@ namespace storm {
*/
IntegerLiteralExpression(IntegerLiteralExpression const& integerLiteralExpression);
virtual std::shared_ptr<BaseExpression> clone() const override;
virtual std::unique_ptr<BaseExpression> clone() 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 std::unique_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/UnaryBooleanFunctionExpression.cpp
View File

@ -13,7 +13,7 @@ namespace storm {
namespace ir {
namespace expressions {
UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> child, FunctionType functionType) : UnaryExpression(bool_, child), functionType(functionType) {
UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& child, FunctionType functionType) : UnaryExpression(bool_, std::move(child)), functionType(functionType) {
// Nothing to do here.
}
@ -21,12 +21,12 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone() const {
return std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(), functionType));
std::unique_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone() const {
return std::unique_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(), functionType));
}
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));
std::unique_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::unique_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, variableState), this->functionType));
}
UnaryBooleanFunctionExpression::FunctionType UnaryBooleanFunctionExpression::getFunctionType() const {

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

@ -30,7 +30,7 @@ namespace storm {
* @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);
UnaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& child, FunctionType functionType);
/*!
* Copy-constructs from the given expression.
@ -39,9 +39,9 @@ namespace storm {
*/
UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& unaryBooleanFunctionExpression);
virtual std::shared_ptr<BaseExpression> clone() const override;
virtual std::unique_ptr<BaseExpression> clone() 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 std::unique_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.

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

@ -11,15 +11,15 @@ namespace storm {
namespace ir {
namespace expressions {
UnaryExpression::UnaryExpression(ReturnType type, std::shared_ptr<BaseExpression> child) : BaseExpression(type), child(child) {
UnaryExpression::UnaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child) : BaseExpression(type), child(std::move(child)) {
// Nothing to do here.
}
UnaryExpression::UnaryExpression(UnaryExpression const& unaryExpression) : BaseExpression(unaryExpression), child(unaryExpression.child) {
UnaryExpression::UnaryExpression(UnaryExpression const& unaryExpression) : BaseExpression(unaryExpression), child(unaryExpression.child->clone()) {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> const& UnaryExpression::getChild() const {
std::unique_ptr<BaseExpression> const& UnaryExpression::getChild() const {
return child;
}

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

@ -24,7 +24,7 @@ namespace storm {
* @param type The type of the unary expression.
* @param right The child of the unary expression.
*/
UnaryExpression(ReturnType type, std::shared_ptr<BaseExpression> child);
UnaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child);
/*!
* Copy-constructs from the given expression.
@ -38,11 +38,11 @@ namespace storm {
*
* @return The child of the expression node.
*/
std::shared_ptr<BaseExpression> const& getChild() const;
std::unique_ptr<BaseExpression> const& getChild() const;
private:
// The left child of the unary expression.
std::shared_ptr<BaseExpression> child;
std::unique_ptr<BaseExpression> child;
};
} // namespace expressions

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

@ -11,7 +11,7 @@ namespace storm {
namespace ir {
namespace expressions {
UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> child, FunctionType functionType) : UnaryExpression(type, child), functionType(functionType) {
UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child, FunctionType functionType) : UnaryExpression(type, std::move(child)), functionType(functionType) {
// Nothing to do here.
}
@ -19,12 +19,12 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone() const {
return std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(), functionType));
std::unique_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone() const {
return std::unique_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(), functionType));
}
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));
std::unique_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
return std::unique_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 {

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

@ -30,7 +30,7 @@ namespace storm {
* @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);
UnaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child, FunctionType functionType);
/*!
* Copy-constructs from the given expression.
@ -39,9 +39,9 @@ namespace storm {
*/
UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& unaryNumericalFunctionExpression);
virtual std::shared_ptr<BaseExpression> clone() const override;
virtual std::unique_ptr<BaseExpression> clone() 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 std::unique_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;

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

@ -26,24 +26,24 @@ namespace storm {
// Nothing to do here.
}
std::shared_ptr<BaseExpression> VariableExpression::clone() const {
return std::shared_ptr<BaseExpression>(new VariableExpression(*this));
std::unique_ptr<BaseExpression> VariableExpression::clone() const {
return std::unique_ptr<BaseExpression>(new VariableExpression(*this));
}
std::shared_ptr<BaseExpression> VariableExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
std::unique_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()) {
if (this->getType() == int_) {
return variableState.getIntegerVariableExpression(renamingPair->second);
return variableState.getIntegerVariableExpression(renamingPair->second)->clone();
} else {
return variableState.getBooleanVariableExpression(renamingPair->second);
return variableState.getBooleanVariableExpression(renamingPair->second)->clone();
}
} else {
if (this->getType() == int_) {
return variableState.getIntegerVariableExpression(this->variableName);
return variableState.getIntegerVariableExpression(this->variableName)->clone();
} else {
return variableState.getBooleanVariableExpression(this->variableName);
return variableState.getBooleanVariableExpression(this->variableName)->clone();
}
}
}

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

@ -52,9 +52,9 @@ namespace storm {
*/
VariableExpression(VariableExpression const& variableExpression);
virtual std::shared_ptr<BaseExpression> clone() const override;
virtual std::unique_ptr<BaseExpression> clone() 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 std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
virtual void accept(ExpressionVisitor* visitor) override;

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

@ -26,14 +26,14 @@ namespace prism {
/*!
* Constructor.
*/
BaseGrammar(std::shared_ptr<VariableState>& state) : state(state) {}
BaseGrammar(std::shared_ptr<VariableState> const& state) : state(state) {}
/*!
* Create and return a new instance of class T, usually the subclass.
* @param state VariableState to be given to the constructor.
* @returns Instance of class T.
*/
static T& instance(std::shared_ptr<VariableState> state = nullptr) {
static T& instance(std::shared_ptr<VariableState> const& state = nullptr) {
if (BaseGrammar::instanceObject == nullptr) {
BaseGrammar::instanceObject = std::shared_ptr<T>(new T(state));
if (!state->firstRun) BaseGrammar::instanceObject->secondRun();
@ -62,24 +62,24 @@ namespace prism {
* @param value Value of the literal.
* @returns Boolean literal.
*/
std::shared_ptr<BaseExpression> createBoolLiteral(const bool value) {
return std::shared_ptr<BooleanLiteralExpression>(new BooleanLiteralExpression(value));
std::shared_ptr<BaseExpression> createBoolLiteral(bool value) {
return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(value));
}
/*!
* Create a new double literal with the given value.
* @param value Value of the literal.
* @returns Double literal.
*/
std::shared_ptr<BaseExpression> createDoubleLiteral(const double value) {
return std::shared_ptr<DoubleLiteralExpression>(new DoubleLiteralExpression(value));
std::shared_ptr<BaseExpression> createDoubleLiteral(double value) {
return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(value));
}
/*!
* Create a new integer literal with the given value.
* @param value Value of the literal.
* @returns Integer literal.
*/
std::shared_ptr<BaseExpression> createIntLiteral(const int_fast64_t value) {
return std::shared_ptr<IntegerLiteralExpression>(new IntegerLiteralExpression(value));
std::shared_ptr<BaseExpression> createIntLiteral(int_fast64_t value) {
return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(value));
}
/*!
@ -90,11 +90,11 @@ namespace prism {
* @param type Return type.
* @returns Plus expression.
*/
std::shared_ptr<BaseExpression> createPlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right, BaseExpression::ReturnType type) {
std::shared_ptr<BaseExpression> createPlus(std::shared_ptr<BaseExpression> const& left, bool addition, std::shared_ptr<BaseExpression> const& right, BaseExpression::ReturnType type) {
if (addition) {
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(type, left, right, BinaryNumericalFunctionExpression::PLUS));
return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(type, left->clone(), right->clone(), BinaryNumericalFunctionExpression::PLUS));
} else {
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(type, left, right, BinaryNumericalFunctionExpression::MINUS));
return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(type, left->clone(), right->clone(), BinaryNumericalFunctionExpression::MINUS));
}
}
/*!
@ -104,7 +104,7 @@ namespace prism {
* @param right Right operand.
* @returns Double plus expression.
*/
std::shared_ptr<BaseExpression> createDoublePlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right) {
std::shared_ptr<BaseExpression> createDoublePlus(std::shared_ptr<BaseExpression> const& left, bool addition, std::shared_ptr<BaseExpression> const& right) {
return this->createPlus(left, addition, right, BaseExpression::double_);
}
/*!
@ -114,7 +114,7 @@ namespace prism {
* @param right Right operand.
* @returns Integer plus expression.
*/
std::shared_ptr<BaseExpression> createIntPlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right) {
std::shared_ptr<BaseExpression> createIntPlus(std::shared_ptr<BaseExpression> const& left, bool addition, std::shared_ptr<BaseExpression> const& right) {
return this->createPlus(left, addition, right, BaseExpression::int_);
}
@ -124,8 +124,8 @@ namespace prism {
* @param right Right operand.
* @returns Integer multiplication expression.
*/
std::shared_ptr<BaseExpression> createIntMult(const std::shared_ptr<BaseExpression> left, const std::shared_ptr<BaseExpression> right) {
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::int_, left, right, BinaryNumericalFunctionExpression::TIMES));
std::shared_ptr<BaseExpression> createIntMult(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right) {
return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(BaseExpression::int_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::TIMES));
}
/*!
* Create a new integer multiplication expression. If multiplication is true, it will be an multiplication, otherwise a division.
@ -134,11 +134,11 @@ namespace prism {
* @param right Right operand.
* @returns Integer multiplication expression.
*/
std::shared_ptr<BaseExpression> createDoubleMult(const std::shared_ptr<BaseExpression> left, bool multiplication, const std::shared_ptr<BaseExpression> right) {
std::shared_ptr<BaseExpression> createDoubleMult(std::shared_ptr<BaseExpression> const& left, bool multiplication, std::shared_ptr<BaseExpression> const& right) {
if (multiplication) {
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::TIMES));
return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::TIMES));
} else {
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::DIVIDE));
return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::DIVIDE));
}
}
/*!
@ -148,16 +148,16 @@ namespace prism {
* @param right Right operand.
* @returns Binary relation expression.
*/
std::shared_ptr<BaseExpression> createRelation(std::shared_ptr<BaseExpression> left, BinaryRelationExpression::RelationType relationType, std::shared_ptr<BaseExpression> right) {
return std::shared_ptr<BinaryRelationExpression>(new BinaryRelationExpression(left, right, relationType));
std::shared_ptr<BaseExpression> createRelation(std::shared_ptr<BaseExpression> const& left, BinaryRelationExpression::RelationType relationType, std::shared_ptr<BaseExpression> const& right) {
return std::shared_ptr<BaseExpression>(new BinaryRelationExpression(left->clone(), right->clone(), relationType));
}
/*!
* Create a new negation expression.
* @param child Expression to be negated.
* @returns Negation expression.
*/
std::shared_ptr<BaseExpression> createNot(std::shared_ptr<BaseExpression> child) {
return std::shared_ptr<UnaryBooleanFunctionExpression>(new UnaryBooleanFunctionExpression(child, UnaryBooleanFunctionExpression::NOT));
std::shared_ptr<BaseExpression> createNot(std::shared_ptr<BaseExpression> const& child) {
return std::shared_ptr<UnaryBooleanFunctionExpression>(new UnaryBooleanFunctionExpression(child->clone(), UnaryBooleanFunctionExpression::NOT));
}
/*!
* Create a new And expression.
@ -165,9 +165,8 @@ namespace prism {
* @param right Right operand.
* @returns And expression.
*/
std::shared_ptr<BaseExpression> createAnd(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) {
//std::cerr << "Creating " << left->toString() << " & " << right->toString() << std::endl;
return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::AND));
std::shared_ptr<BaseExpression> createAnd(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right) {
return std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(left->clone(), right->clone(), BinaryBooleanFunctionExpression::AND));
}
/*!
* Create a new Or expression.
@ -175,24 +174,24 @@ namespace prism {
* @param right Right operand.
* @returns Or expression.
*/
std::shared_ptr<BaseExpression> createOr(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) {
return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::OR));
std::shared_ptr<BaseExpression> createOr(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right) {
return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left->clone(), right->clone(), BinaryBooleanFunctionExpression::OR));
}
/*!
* Retrieve boolean variable by name.
* @param name Variable name.
* @returns Boolean variable.
*/
std::shared_ptr<BaseExpression> getBoolVariable(const std::string name) {
return state->getBooleanVariableExpression(name);
std::shared_ptr<BaseExpression> getBoolVariable(std::string const& name) {
return std::shared_ptr<BaseExpression>(new VariableExpression(*state->getBooleanVariableExpression(name)));
}
/*!
* Retrieve integer variable by name.
* @param name Variable name.
* @returns Integer variable.
*/
std::shared_ptr<BaseExpression> getIntVariable(const std::string name) {
return state->getIntegerVariableExpression(name);
std::shared_ptr<BaseExpression> getIntVariable(std::string const& name) {
return std::shared_ptr<BaseExpression>(new VariableExpression(*state->getIntegerVariableExpression(name)));
}
/*!
@ -200,6 +199,7 @@ namespace prism {
* Any subclass that needs to do something in order to proceed to the second run should override this method.
*/
virtual void prepareSecondRun() {}
protected:
/*!
* Pointer to variable state.

72
src/parser/prismparser/BooleanExpressionGrammar.cpp
View File

@ -4,39 +4,39 @@
#include "ConstBooleanExpressionGrammar.h"
namespace storm {
namespace parser {
namespace prism {
BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr<VariableState>& state)
: BooleanExpressionGrammar::base_type(booleanExpression), BaseGrammar(state) {
booleanExpression %= orExpression;
booleanExpression.name("boolean expression");
orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&BaseGrammar::createOr, this, qi::_val, qi::_1)];
orExpression.name("boolean expression");
andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::bind(&BaseGrammar::createAnd, this, qi::_val, qi::_1)];
andExpression.name("boolean expression");
notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)];
notExpression.name("boolean expression");
atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | ConstBooleanExpressionGrammar::instance(this->state));
atomicBooleanExpression.name("boolean expression");
relativeExpression = (IntegerExpressionGrammar::instance(this->state) >> relations_ >> IntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)];
relativeExpression.name("relative expression");
booleanVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getBoolVariable, this, qi::_1)];
booleanVariableExpression.name("boolean variable");
}
void BooleanExpressionGrammar::prepareSecondRun() {
booleanVariableExpression %= this->state->booleanVariables_;
booleanVariableExpression.name("boolean variable");
}
}
}
}
namespace parser {
namespace prism {
BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr<VariableState> const& state)
: BooleanExpressionGrammar::base_type(booleanExpression), BaseGrammar(state) {
booleanExpression %= orExpression;
booleanExpression.name("boolean expression");
orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&BaseGrammar::createOr, this, qi::_val, qi::_1)];
orExpression.name("boolean expression");
andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::bind(&BaseGrammar::createAnd, this, qi::_val, qi::_1)];
andExpression.name("boolean expression");
notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)];
notExpression.name("boolean expression");
atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | ConstBooleanExpressionGrammar::instance(this->state));
atomicBooleanExpression.name("boolean expression");
relativeExpression = (IntegerExpressionGrammar::instance(this->state) >> relations_ >> IntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)];
relativeExpression.name("relative expression");
booleanVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getBoolVariable, this, qi::_1)];
booleanVariableExpression.name("boolean variable");
}
void BooleanExpressionGrammar::prepareSecondRun() {
booleanVariableExpression %= this->state->booleanVariables_;
booleanVariableExpression.name("boolean variable");
}
} // namespace prism
} // namespace parser
} // namespace storm

2
src/parser/prismparser/BooleanExpressionGrammar.h
View File

@ -24,7 +24,7 @@ namespace prism {
*/
class BooleanExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<BooleanExpressionGrammar> {
public:
BooleanExpressionGrammar(std::shared_ptr<VariableState>& state);
BooleanExpressionGrammar(std::shared_ptr<VariableState> const& state);
/*!
* Switch to second run.
* Variable names may be any valid identifier in the first run, but only defined variables in the second run.

2
src/parser/prismparser/ConstBooleanExpressionGrammar.cpp
View File

@ -6,7 +6,7 @@ namespace storm {
namespace parser {
namespace prism {
ConstBooleanExpressionGrammar::ConstBooleanExpressionGrammar(std::shared_ptr<VariableState>& state)
ConstBooleanExpressionGrammar::ConstBooleanExpressionGrammar(std::shared_ptr<VariableState> const& state)
: ConstBooleanExpressionGrammar::base_type(constantBooleanExpression), BaseGrammar(state) {
constantBooleanExpression %= constantOrExpression;

2
src/parser/prismparser/ConstBooleanExpressionGrammar.h
View File

@ -22,7 +22,7 @@ namespace prism {
*/
class ConstBooleanExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstBooleanExpressionGrammar> {
public:
ConstBooleanExpressionGrammar(std::shared_ptr<VariableState>& state);
ConstBooleanExpressionGrammar(std::shared_ptr<VariableState> const& state);
private:

2
src/parser/prismparser/ConstDoubleExpressionGrammar.cpp
View File

@ -4,7 +4,7 @@ namespace storm {
namespace parser {
namespace prism {
ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr<VariableState>& state)
ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr<VariableState> const& state)
: ConstDoubleExpressionGrammar::base_type(constantDoubleExpression), BaseGrammar(state) {
constantDoubleExpression %= constantDoublePlusExpression;

44
src/parser/prismparser/ConstDoubleExpressionGrammar.h
View File

@ -13,28 +13,28 @@
#include "IdentifierGrammars.h"
namespace storm {
namespace parser {
namespace prism {
/*!
* This grammar parses constant double expressions as used in prism models.
*/
class ConstDoubleExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstDoubleExpressionGrammar> {
public:
ConstDoubleExpressionGrammar(std::shared_ptr<VariableState>& state);
private:
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantDoubleExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoublePlusExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoubleMultExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicDoubleExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleConstantExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleLiteralExpression;
};
}
}
namespace parser {
namespace prism {
/*!
* This grammar parses constant double expressions as used in prism models.
*/
class ConstDoubleExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstDoubleExpressionGrammar> {
public:
ConstDoubleExpressionGrammar(std::shared_ptr<VariableState> const& state);
private:
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantDoubleExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoublePlusExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoubleMultExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicDoubleExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleConstantExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleLiteralExpression;
};
}
}
}
#endif /* CONSTDOUBLEEXPRESSIONGRAMMAR_H */

64
src/parser/prismparser/ConstIntegerExpressionGrammar.cpp
View File

@ -1,35 +1,35 @@
#include "ConstIntegerExpressionGrammar.h"
namespace storm {
namespace parser {
namespace prism {
ConstIntegerExpressionGrammar::ConstIntegerExpressionGrammar(std::shared_ptr<VariableState>& state)
: ConstIntegerExpressionGrammar::base_type(constantIntegerExpression), BaseGrammar(state) {
constantIntegerExpression %= constantIntegerPlusExpression;
constantIntegerExpression.name("constant integer expression");
constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression)
[qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)];
constantIntegerPlusExpression.name("constant integer expression");
constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)
[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)];
constantIntegerMultExpression.name("constant integer expression");
constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression);
constantAtomicIntegerExpression.name("constant integer expression");
integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression);
integerConstantExpression.name("integer constant or literal");
integerLiteralExpression = qi::int_[qi::_val = phoenix::bind(&BaseGrammar::createIntLiteral, this, qi::_1)];
integerLiteralExpression.name("integer literal");
}
}
}
}
namespace parser {
namespace prism {
ConstIntegerExpressionGrammar::ConstIntegerExpressionGrammar(std::shared_ptr<VariableState> const& state)
: ConstIntegerExpressionGrammar::base_type(constantIntegerExpression), BaseGrammar(state) {
constantIntegerExpression %= constantIntegerPlusExpression;
constantIntegerExpression.name("constant integer expression");
constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression)
[qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)];
constantIntegerPlusExpression.name("constant integer expression");
constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)
[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)];
constantIntegerMultExpression.name("constant integer expression");
constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression);
constantAtomicIntegerExpression.name("constant integer expression");
integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression);
integerConstantExpression.name("integer constant or literal");
integerLiteralExpression = qi::int_[qi::_val = phoenix::bind(&BaseGrammar::createIntLiteral, this, qi::_1)];
integerLiteralExpression.name("integer literal");
}
} // namespace prism
} // namespace parser
} // namespace storm

44
src/parser/prismparser/ConstIntegerExpressionGrammar.h
View File

@ -13,28 +13,28 @@
#include "IdentifierGrammars.h"
namespace storm {
namespace parser {
namespace prism {
/*!
* This grammar parses constant integer expressions as used in prism models.
*/
class ConstIntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstIntegerExpressionGrammar> {
public:
ConstIntegerExpressionGrammar(std::shared_ptr<VariableState>& state);
private:
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantIntegerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantIntegerPlusExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantIntegerMultExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicIntegerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerConstantExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerLiteralExpression;
};
}
}
namespace parser {
namespace prism {
/*!
* This grammar parses constant integer expressions as used in prism models.
*/
class ConstIntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstIntegerExpressionGrammar> {
public:
ConstIntegerExpressionGrammar(std::shared_ptr<VariableState> const& state);
private:
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantIntegerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantIntegerPlusExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantIntegerMultExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicIntegerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerConstantExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerLiteralExpression;
};
}
}
}
#endif /* CONSTINTEGEREXPRESSIONGRAMMAR_H */

38
src/parser/prismparser/IdentifierGrammars.cpp
View File

@ -1,23 +1,23 @@
#include "IdentifierGrammars.h"
namespace storm {
namespace parser {
namespace prism {
IdentifierGrammar::IdentifierGrammar(std::shared_ptr<VariableState>& state)
: IdentifierGrammar::base_type(identifierName), BaseGrammar(state) {
identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isIdentifier, this->state.get(), qi::_1) ];
identifierName.name("identifier");
}
FreeIdentifierGrammar::FreeIdentifierGrammar(std::shared_ptr<VariableState>& state)
: FreeIdentifierGrammar::base_type(freeIdentifierName), BaseGrammar(state) {
freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isFreeIdentifier, this->state.get(), qi::_1) ];
freeIdentifierName.name("identifier");
}
}
}
namespace parser {
namespace prism {
IdentifierGrammar::IdentifierGrammar(std::shared_ptr<VariableState> const& state)
: IdentifierGrammar::base_type(identifierName), BaseGrammar(state) {
identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isIdentifier, this->state.get(), qi::_1) ];
identifierName.name("identifier");
}
FreeIdentifierGrammar::FreeIdentifierGrammar(std::shared_ptr<VariableState> const& state)
: FreeIdentifierGrammar::base_type(freeIdentifierName), BaseGrammar(state) {
freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isFreeIdentifier, this->state.get(), qi::_1) ];
freeIdentifierName.name("identifier");
}
}
}
}

48
src/parser/prismparser/IdentifierGrammars.h
View File

@ -13,30 +13,30 @@
#include "VariableState.h"
namespace storm {
namespace parser {
namespace prism {
/*!
* This grammar parses a (possibly used) identifier as used in a prism models.
*/
class IdentifierGrammar : public qi::grammar<Iterator, std::string(), Skipper, Unused>, public BaseGrammar<IdentifierGrammar> {
public:
IdentifierGrammar(std::shared_ptr<VariableState>& state);
private:
qi::rule<Iterator, std::string(), Skipper> identifierName;
};
/*!
* This grammar parses an used identifier as used in a prism models.
*/
class FreeIdentifierGrammar : public qi::grammar<Iterator, std::string(), Skipper, Unused>, public BaseGrammar<IdentifierGrammar> {
public:
FreeIdentifierGrammar(std::shared_ptr<VariableState>& state);
private:
qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
};
}
}
namespace parser {
namespace prism {
/*!
* This grammar parses a (possibly used) identifier as used in a prism models.
*/
class IdentifierGrammar : public qi::grammar<Iterator, std::string(), Skipper, Unused>, public BaseGrammar<IdentifierGrammar> {
public:
IdentifierGrammar(std::shared_ptr<VariableState> const& state);
private:
qi::rule<Iterator, std::string(), Skipper> identifierName;
};
/*!
* This grammar parses an used identifier as used in a prism models.
*/
class FreeIdentifierGrammar : public qi::grammar<Iterator, std::string(), Skipper, Unused>, public BaseGrammar<IdentifierGrammar> {
public:
FreeIdentifierGrammar(std::shared_ptr<VariableState> const& state);
private:
qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
};
}
}
}
#endif /* IDENTIFIERGRAMMARS_H */

58
src/parser/prismparser/IntegerExpressionGrammar.cpp
View File

@ -4,33 +4,33 @@
#include "ConstIntegerExpressionGrammar.h"
namespace storm {
namespace parser {
namespace prism {
IntegerExpressionGrammar::IntegerExpressionGrammar(std::shared_ptr<VariableState>& state)
: IntegerExpressionGrammar::base_type(integerExpression), BaseGrammar(state) {
integerExpression %= integerPlusExpression;
integerExpression.name("integer expression");
integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)];
integerPlusExpression.name("integer expression");
integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]);
integerMultExpression.name("integer expression");
atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | ConstIntegerExpressionGrammar::instance(this->state));
atomicIntegerExpression.name("integer expression");
integerVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getIntVariable, this, qi::_1)];
integerVariableExpression.name("integer variable");
}
void IntegerExpressionGrammar::prepareSecondRun() {
integerVariableExpression %= this->state->integerVariables_;
integerVariableExpression.name("integer variable");
}
}
}
namespace parser {
namespace prism {
IntegerExpressionGrammar::IntegerExpressionGrammar(std::shared_ptr<VariableState> const& state)
: IntegerExpressionGrammar::base_type(integerExpression), BaseGrammar(state) {
integerExpression %= integerPlusExpression;
integerExpression.name("integer expression");
integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)];
integerPlusExpression.name("integer expression");
integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]);
integerMultExpression.name("integer expression");
atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | ConstIntegerExpressionGrammar::instance(this->state));
atomicIntegerExpression.name("integer expression");
integerVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getIntVariable, this, qi::_1)];
integerVariableExpression.name("integer variable");
}
void IntegerExpressionGrammar::prepareSecondRun() {
integerVariableExpression %= this->state->integerVariables_;
integerVariableExpression.name("integer variable");
}
}
}
}

52
src/parser/prismparser/IntegerExpressionGrammar.h
View File

@ -16,32 +16,32 @@
#include <memory>
namespace storm {
namespace parser {
namespace prism {
/*!
* This grammar parses a (non constant) integer expressions as used in prism models.
*/
class IntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<IntegerExpressionGrammar> {
public:
IntegerExpressionGrammar(std::shared_ptr<VariableState>& state);
/*!
* Switch to second run.
* Variable names may be any valid identifier in the first run, but only defined variables in the second run.
*/
virtual void prepareSecondRun();
private:
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> integerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> integerPlusExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerMultExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> atomicIntegerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerVariableExpression;
};
}
}
namespace parser {
namespace prism {
/*!
* This grammar parses a (non constant) integer expressions as used in prism models.
*/
class IntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<IntegerExpressionGrammar> {
public:
IntegerExpressionGrammar(std::shared_ptr<VariableState> const& state);
/*!
* Switch to second run.
* Variable names may be any valid identifier in the first run, but only defined variables in the second run.
*/
virtual void prepareSecondRun();
private:
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> integerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> integerPlusExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerMultExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> atomicIntegerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerVariableExpression;
};
}
}
}
#endif /* INTEGEREXPRESSIONGRAMMAR_H */

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

@ -35,234 +35,243 @@ namespace qi = boost::spirit::qi;
namespace phoenix = boost::phoenix;
namespace storm {
namespace parser {
namespace prism {
std::shared_ptr<BaseExpression> PrismGrammar::addIntegerConstant(std::string const& name, std::shared_ptr<BaseExpression> const& value) {
this->state->integerConstants_.add(name, value);
this->state->allConstantNames_.add(name, name);
return value;
}
void PrismGrammar::addLabel(std::string const& name, std::shared_ptr<BaseExpression> const& value, std::map<std::string, std::shared_ptr<BaseExpression>>& nameToExpressionMap) {
this->state->labelNames_.add(name, name);
nameToExpressionMap[name] = value;
}
void PrismGrammar::addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssignmentMap) {
this->state->assignedIntegerVariables_.add(variable, variable);
variableToAssignmentMap[variable] = Assignment(variable, value);
}
void PrismGrammar::addBooleanAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssigmentMap) {
this->state->assignedBooleanVariables_.add(variable, variable);
variableToAssigmentMap[variable] = Assignment(variable, value);
}
Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map<std::string, std::string> const& renaming) {
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(newName) = res;
return res;
}
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(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, bool isGlobalVariable) {
uint_fast64_t id = this->state->addIntegerVariable(name);
uint_fast64_t newLocalIndex = this->state->nextLocalIntegerVariableIndex;
vars.emplace_back(newLocalIndex, id, name, lower, upper, init);
varids[name] = newLocalIndex;
++this->state->nextLocalIntegerVariableIndex;
this->state->localIntegerVariables_.add(name, name);
if (isGlobalVariable) {
this->state->globalIntegerVariables_.add(name, name);
}
}
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, bool isGlobalVariable) {
uint_fast64_t id = this->state->addBooleanVariable(name);
uint_fast64_t newLocalIndex = this->state->nextLocalBooleanVariableIndex;
vars.emplace_back(newLocalIndex, id, name, init);
varids[name] = newLocalIndex;
++this->state->nextLocalBooleanVariableIndex;
this->state->localBooleanVariables_.add(name, name);
if (isGlobalVariable) {
this->state->globalBooleanVariables_.add(name, name);
}
}
StateReward createStateReward(std::shared_ptr<BaseExpression> guard, std::shared_ptr<BaseExpression> reward) {
return StateReward(guard, reward);
}
TransitionReward createTransitionReward(std::string const& label, std::shared_ptr<BaseExpression> guard, std::shared_ptr<BaseExpression> reward) {
return TransitionReward(label, guard, reward);
}
void createRewardModel(std::string const& name, std::vector<StateReward>& stateRewards, std::vector<TransitionReward>& transitionRewards, std::map<std::string, RewardModel>& mapping) {
mapping[name] = RewardModel(name, stateRewards, transitionRewards);
}
Update PrismGrammar::createUpdate(std::shared_ptr<BaseExpression> likelihood, std::map<std::string, Assignment> const& bools, std::map<std::string, Assignment> const& ints) {
this->state->nextGlobalUpdateIndex++;
return Update(this->state->getNextGlobalUpdateIndex() - 1, likelihood, bools, ints);
}
Command PrismGrammar::createCommand(std::string const& label, std::shared_ptr<BaseExpression> guard, std::vector<Update> const& updates) {
this->state->nextGlobalCommandIndex++;
return Command(this->state->getNextGlobalCommandIndex() - 1, label, guard, updates);
}
Program createProgram(
Program::ModelType modelType,
std::map<std::string, std::shared_ptr<BooleanConstantExpression>> const& undefBoolConst,
std::map<std::string, std::shared_ptr<IntegerConstantExpression>> const& undefIntConst,
std::map<std::string, std::shared_ptr<DoubleConstantExpression>> const& undefDoubleConst,
GlobalVariableInformation const& globalVariableInformation,
std::vector<Module> const& modules,
std::map<std::string, RewardModel> const& rewards,
std::map<std::string, std::shared_ptr<BaseExpression>> const& labels) {
return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst,
globalVariableInformation.booleanVariables, globalVariableInformation.integerVariables,
globalVariableInformation.booleanVariableToIndexMap,
globalVariableInformation.integerVariableToIndexMap, modules, rewards, labels);
}
PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new VariableState()) {
labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> FreeIdentifierGrammar::instance(this->state) >> -qi::lit("\"") >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))
[phoenix::bind(&PrismGrammar::addLabel, this, qi::_1, qi::_2, qi::_r1)];
labelDefinition.name("label declaration");
labelDefinitionList %= *labelDefinition(qi::_r1);
labelDefinitionList.name("label declaration list");
// This block defines all entities that are needed for parsing a reward model.
stateRewardDefinition = (BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[qi::_val = phoenix::bind(&createStateReward, qi::_1, qi::_2)];
stateRewardDefinition.name("state reward definition");
transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[qi::_val = phoenix::bind(&createTransitionReward, qi::_a, qi::_2, qi::_3)];
transitionRewardDefinition.name("transition reward definition");
rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > FreeIdentifierGrammar::instance(this->state) > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards"))
[phoenix::bind(&createRewardModel, qi::_1, qi::_a, qi::_b, qi::_r1)];
rewardDefinition.name("reward definition");
rewardDefinitionList = *rewardDefinition(qi::_r1);
rewardDefinitionList.name("reward definition list");
commandName %= this->state->commandNames_;
commandName.name("command name");
unassignedLocalBooleanVariableName %= (this->state->localBooleanVariables_ | this->state->globalBooleanVariables_) - this->state->assignedBooleanVariables_;
unassignedLocalBooleanVariableName.name("unassigned local/global boolean variable");
unassignedLocalIntegerVariableName %= (this->state->localIntegerVariables_ | this->state->globalIntegerVariables_) - this->state->assignedIntegerVariables_;
unassignedLocalIntegerVariableName.name("unassigned local/global integer variable");
// 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::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");
updateDefinition = (ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)];
updateDefinition.name("update");
updateListDefinition = +updateDefinition % "+";
updateListDefinition.name("update list");
commandDefinition = (
qi::lit("[") > -(
(FreeIdentifierGrammar::instance(this->state)[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1]
) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit("->") > updateListDefinition > qi::lit(";")
)[qi::_val = phoenix::bind(&PrismGrammar::createCommand, this, qi::_a, qi::_2, qi::_3)];
commandDefinition.name("command");
// This block defines all entities that are needed for parsing variable definitions.
booleanVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
[phoenix::bind(&PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2, qi::_r3)];
booleanVariableDefinition.name("boolean variable declaration");
integerVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("..") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("]") > -(qi::lit("init") > ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
[phoenix::bind(&PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2, qi::_r3)];
integerVariableDefinition.name("integer variable declaration");
variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3, false) | integerVariableDefinition(qi::_r2, qi::_r4, false));
variableDefinition.name("variable declaration");
// This block defines all entities that are needed for parsing a module.
moduleDefinition = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&VariableState::clearLocalVariables, *this->state)]
>> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule"))
[qi::_val = phoenix::bind(&PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)];
moduleDefinition.name("module");
moduleRenaming = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=")
> this->state->moduleNames_ > qi::lit("[") > *(
(IdentifierGrammar::instance(this->state) > qi::lit("=") > IdentifierGrammar::instance(this->state) >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))]
) > qi::lit("]") > qi::lit("endmodule"))
[qi::_val = phoenix::bind(&PrismGrammar::renameModule, this, qi::_1, qi::_2, qi::_a)];
moduleRenaming.name("renamed module");
moduleDefinitionList %= +(moduleDefinition | moduleRenaming);
moduleDefinitionList.name("module list");
// This block defines all entities that are needed for parsing global variable definitions.
globalVariableDefinitionList = *(qi::lit("global") > (booleanVariableDefinition(bind(&GlobalVariableInformation::booleanVariables, qi::_r1), bind(&GlobalVariableInformation::booleanVariableToIndexMap, qi::_r1), true) | integerVariableDefinition(bind(&GlobalVariableInformation::integerVariables, qi::_r1), bind(&GlobalVariableInformation::integerVariableToIndexMap, qi::_r1), true)));
globalVariableDefinitionList.name("global variable declaration list");
// This block defines all entities that are needed for parsing constant definitions.
definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstBooleanExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
definedBooleanConstantDefinition.name("defined boolean constant declaration");
definedIntegerConstantDefinition = (
qi::lit("const") >> qi::lit("int") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >>
ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";")
)[ qi::_val = phoenix::bind(&PrismGrammar::addIntegerConstant, this, qi::_1, qi::_2) ];
definedIntegerConstantDefinition.name("defined integer constant declaration");
definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
definedDoubleConstantDefinition.name("defined double constant declaration");
undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<BooleanConstantExpression>>(phoenix::new_<BooleanConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<BooleanConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)];
undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<IntegerConstantExpression>>(phoenix::new_<IntegerConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<IntegerConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)];
undefinedIntegerConstantDefinition.name("undefined integer constant declaration");
undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<DoubleConstantExpression>>(phoenix::new_<DoubleConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<DoubleConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)];
undefinedDoubleConstantDefinition.name("undefined double constant declaration");
definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
definedConstantDefinition.name("defined constant declaration");
undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3));
undefinedConstantDefinition.name("undefined constant declaration");
constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3));
constantDefinitionList.name("constant declaration list");
// This block defines all entities that are needed for parsing a program.
modelTypeDefinition = modelType_;
modelTypeDefinition.name("model type");
start = (
modelTypeDefinition >
constantDefinitionList(qi::_a, qi::_b, qi::_c) >
globalVariableDefinitionList(qi::_d) >
moduleDefinitionList >
rewardDefinitionList(qi::_e) >
labelDefinitionList(qi::_f))[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2, qi::_e, qi::_f)];
start.name("probabilistic program declaration");
}
void PrismGrammar::prepareForSecondRun() {
LOG4CPLUS_INFO(logger, "Preparing parser for second run.");
this->state->prepareForSecondRun();
BooleanExpressionGrammar::secondRun();
ConstBooleanExpressionGrammar::secondRun();
ConstDoubleExpressionGrammar::secondRun();
ConstIntegerExpressionGrammar::secondRun();
IntegerExpressionGrammar::secondRun();
}
void PrismGrammar::resetGrammars() {
LOG4CPLUS_INFO(logger, "Resetting grammars.");
BooleanExpressionGrammar::resetInstance();
ConstBooleanExpressionGrammar::resetInstance();
ConstDoubleExpressionGrammar::resetInstance();
ConstIntegerExpressionGrammar::resetInstance();
IntegerExpressionGrammar::resetInstance();
}
} // namespace prism
} // namespace parser
namespace parser {
namespace prism {
void PrismGrammar::addLabel(std::string const& name, std::shared_ptr<BaseExpression> const& value, std::map<std::string, std::unique_ptr<BaseExpression>>& nameToExpressionMap) {
this->state->labelNames_.add(name, name);
nameToExpressionMap[name] = value->clone();
}
void PrismGrammar::addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssignmentMap) {
this->state->assignedIntegerVariables_.add(variable, variable);
variableToAssignmentMap[variable] = Assignment(variable, value->clone());
}
void PrismGrammar::addBooleanAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssigmentMap) {
this->state->assignedBooleanVariables_.add(variable, variable);
variableToAssigmentMap[variable] = Assignment(variable, value->clone());
}
void PrismGrammar::addUndefinedBooleanConstant(std::string const& name, std::map<std::string, std::unique_ptr<BooleanConstantExpression>>& nameToExpressionMap) {
this->state->booleanConstants_.add(name, std::shared_ptr<BaseExpression>(new BooleanConstantExpression(name)));
this->state->allConstantNames_.add(name, name);
nameToExpressionMap.emplace(name, std::unique_ptr<BooleanConstantExpression>(new BooleanConstantExpression(dynamic_cast<BooleanConstantExpression&>(*this->state->booleanConstants_.at(name)))));
}
void PrismGrammar::addUndefinedIntegerConstant(std::string const& name, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>& nameToExpressionMap) {
this->state->integerConstants_.add(name, std::shared_ptr<BaseExpression>(new IntegerConstantExpression(name)));
this->state->allConstantNames_.add(name, name);
nameToExpressionMap.emplace(name, std::unique_ptr<IntegerConstantExpression>(new IntegerConstantExpression(dynamic_cast<IntegerConstantExpression&>(*this->state->integerConstants_.at(name)))));
}
void PrismGrammar::addUndefinedDoubleConstant(std::string const& name, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>& nameToExpressionMap) {
this->state->doubleConstants_.add(name, std::shared_ptr<BaseExpression>(new DoubleConstantExpression(name)));
this->state->allConstantNames_.add(name, name);
nameToExpressionMap.emplace(name, std::unique_ptr<DoubleConstantExpression>(new DoubleConstantExpression(dynamic_cast<DoubleConstantExpression&>(*this->state->doubleConstants_.at(name)))));
}
Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map<std::string, std::string> const& renaming) {
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(newName) = res;
return res;
}
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(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, bool isGlobalVariable) {
uint_fast64_t id = this->state->addIntegerVariable(name);
uint_fast64_t newLocalIndex = this->state->nextLocalIntegerVariableIndex;
vars.emplace_back(newLocalIndex, id, name, lower->clone(), upper->clone(), init->clone());
varids[name] = newLocalIndex;
++this->state->nextLocalIntegerVariableIndex;
this->state->localIntegerVariables_.add(name, name);
if (isGlobalVariable) {
this->state->globalIntegerVariables_.add(name, name);
}
}
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, bool isGlobalVariable) {
uint_fast64_t id = this->state->addBooleanVariable(name);
uint_fast64_t newLocalIndex = this->state->nextLocalBooleanVariableIndex;
vars.emplace_back(newLocalIndex, id, name, init->clone());
varids[name] = newLocalIndex;
++this->state->nextLocalBooleanVariableIndex;
this->state->localBooleanVariables_.add(name, name);
if (isGlobalVariable) {
this->state->globalBooleanVariables_.add(name, name);
}
}
StateReward createStateReward(std::shared_ptr<BaseExpression> const& guard, std::shared_ptr<BaseExpression> const& reward) {
return StateReward(guard->clone(), reward->clone());
}
TransitionReward createTransitionReward(std::string const& label, std::shared_ptr<BaseExpression> const& guard, std::shared_ptr<BaseExpression> const& reward) {
return TransitionReward(label, guard->clone(), reward->clone());
}
void createRewardModel(std::string const& name, std::vector<StateReward>& stateRewards, std::vector<TransitionReward>& transitionRewards, std::map<std::string, RewardModel>& mapping) {
mapping[name] = RewardModel(name, stateRewards, transitionRewards);
}
Update PrismGrammar::createUpdate(std::shared_ptr<BaseExpression> const& likelihood, std::map<std::string, Assignment> const& bools, std::map<std::string, Assignment> const& ints) {
this->state->nextGlobalUpdateIndex++;
return Update(this->state->getNextGlobalUpdateIndex() - 1, likelihood->clone(), bools, ints);
}
Command PrismGrammar::createCommand(std::string const& label, std::shared_ptr<BaseExpression> const& guard, std::vector<Update> const& updates) {
this->state->nextGlobalCommandIndex++;
return Command(this->state->getNextGlobalCommandIndex() - 1, label, guard->clone(), updates);
}
Program createProgram(
Program::ModelType modelType,
std::map<std::string, std::unique_ptr<BooleanConstantExpression>> const& undefBoolConst,
std::map<std::string, std::unique_ptr<IntegerConstantExpression>> const& undefIntConst,
std::map<std::string, std::unique_ptr<DoubleConstantExpression>> const& undefDoubleConst,
GlobalVariableInformation const& globalVariableInformation,
std::vector<Module> const& modules,
std::map<std::string, RewardModel> const& rewards,
std::map<std::string, std::unique_ptr<BaseExpression>> const& labels) {
return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst,
globalVariableInformation.booleanVariables, globalVariableInformation.integerVariables,
globalVariableInformation.booleanVariableToIndexMap,
globalVariableInformation.integerVariableToIndexMap, modules, rewards, labels);
}
PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new VariableState()) {
labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> FreeIdentifierGrammar::instance(this->state) >> -qi::lit("\"") >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))
[phoenix::bind(&PrismGrammar::addLabel, this, qi::_1, qi::_2, qi::_r1)];
labelDefinition.name("label declaration");
labelDefinitionList %= *labelDefinition(qi::_r1);
labelDefinitionList.name("label declaration list");
// This block defines all entities that are needed for parsing a reward model.
stateRewardDefinition = (BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[qi::_val = phoenix::bind(&createStateReward, qi::_1, qi::_2)];
stateRewardDefinition.name("state reward definition");
transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[qi::_val = phoenix::bind(&createTransitionReward, qi::_a, qi::_2, qi::_3)];
transitionRewardDefinition.name("transition reward definition");
rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > FreeIdentifierGrammar::instance(this->state) > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards"))
[phoenix::bind(&createRewardModel, qi::_1, qi::_a, qi::_b, qi::_r1)];
rewardDefinition.name("reward definition");
rewardDefinitionList = *rewardDefinition(qi::_r1);
rewardDefinitionList.name("reward definition list");
commandName %= this->state->commandNames_;
commandName.name("command name");
unassignedLocalBooleanVariableName %= (this->state->localBooleanVariables_ | this->state->globalBooleanVariables_) - this->state->assignedBooleanVariables_;
unassignedLocalBooleanVariableName.name("unassigned local/global boolean variable");
unassignedLocalIntegerVariableName %= (this->state->localIntegerVariables_ | this->state->globalIntegerVariables_) - this->state->assignedIntegerVariables_;
unassignedLocalIntegerVariableName.name("unassigned local/global integer variable");
// 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::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");
updateDefinition = (ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)];
updateDefinition.name("update");
updateListDefinition = +updateDefinition % "+";
updateListDefinition.name("update list");
commandDefinition = (
qi::lit("[") > -(
(FreeIdentifierGrammar::instance(this->state)[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1]
) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit("->") > updateListDefinition > qi::lit(";")
)[qi::_val = phoenix::bind(&PrismGrammar::createCommand, this, qi::_a, qi::_2, qi::_3)];
commandDefinition.name("command");
// This block defines all entities that are needed for parsing variable definitions.
booleanVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
[phoenix::bind(&PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2, qi::_r3)];
booleanVariableDefinition.name("boolean variable declaration");
integerVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("..") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("]") > -(qi::lit("init") > ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
[phoenix::bind(&PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2, qi::_r3)];
integerVariableDefinition.name("integer variable declaration");
variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3, false) | integerVariableDefinition(qi::_r2, qi::_r4, false));
variableDefinition.name("variable declaration");
// This block defines all entities that are needed for parsing a module.
moduleDefinition = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&VariableState::clearLocalVariables, *this->state)]
>> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule"))
[qi::_val = phoenix::bind(&PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)];
moduleDefinition.name("module");
moduleRenaming = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=")
> this->state->moduleNames_ > qi::lit("[") > *(
(IdentifierGrammar::instance(this->state) > qi::lit("=") > IdentifierGrammar::instance(this->state) >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))]
) > qi::lit("]") > qi::lit("endmodule"))
[qi::_val = phoenix::bind(&PrismGrammar::renameModule, this, qi::_1, qi::_2, qi::_a)];
moduleRenaming.name("renamed module");
moduleDefinitionList %= +(moduleDefinition | moduleRenaming);
moduleDefinitionList.name("module list");
// This block defines all entities that are needed for parsing global variable definitions.
globalVariableDefinitionList = *(qi::lit("global") > (booleanVariableDefinition(bind(&GlobalVariableInformation::booleanVariables, qi::_r1), bind(&GlobalVariableInformation::booleanVariableToIndexMap, qi::_r1), true) | integerVariableDefinition(bind(&GlobalVariableInformation::integerVariables, qi::_r1), bind(&GlobalVariableInformation::integerVariableToIndexMap, qi::_r1), true)));
globalVariableDefinitionList.name("global variable declaration list");
// This block defines all entities that are needed for parsing constant definitions.
definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstBooleanExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
definedBooleanConstantDefinition.name("defined boolean constant declaration");
definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
definedIntegerConstantDefinition.name("defined integer constant declaration");
definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
definedDoubleConstantDefinition.name("defined double constant declaration");
undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedBooleanConstant, this, qi::_1, qi::_r1)];
undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedIntegerConstant, this, qi::_1, qi::_r1)];
undefinedIntegerConstantDefinition.name("undefined integer constant declaration");
undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedDoubleConstant, this, qi::_1, qi::_r1)];
undefinedDoubleConstantDefinition.name("undefined double constant declaration");
definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
definedConstantDefinition.name("defined constant declaration");
undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3));
undefinedConstantDefinition.name("undefined constant declaration");
constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3));
constantDefinitionList.name("constant declaration list");
// This block defines all entities that are needed for parsing a program.
modelTypeDefinition = modelType_;
modelTypeDefinition.name("model type");
start = (
modelTypeDefinition >
constantDefinitionList(qi::_a, qi::_b, qi::_c) >
globalVariableDefinitionList(qi::_d) >
moduleDefinitionList >
rewardDefinitionList(qi::_e) >
labelDefinitionList(qi::_f))[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2, qi::_e, qi::_f)];
start.name("probabilistic program declaration");
}
void PrismGrammar::prepareForSecondRun() {
LOG4CPLUS_INFO(logger, "Preparing parser for second run.");
this->state->prepareForSecondRun();
BooleanExpressionGrammar::secondRun();
ConstBooleanExpressionGrammar::secondRun();
ConstDoubleExpressionGrammar::secondRun();
ConstIntegerExpressionGrammar::secondRun();
IntegerExpressionGrammar::secondRun();
}
void PrismGrammar::resetGrammars() {
LOG4CPLUS_INFO(logger, "Resetting grammars.");
BooleanExpressionGrammar::resetInstance();
ConstBooleanExpressionGrammar::resetInstance();
ConstDoubleExpressionGrammar::resetInstance();
ConstIntegerExpressionGrammar::resetInstance();
IntegerExpressionGrammar::resetInstance();
}
} // namespace prism
} // namespace parser
} // namespace storm

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

@ -46,12 +46,12 @@ namespace storm {
Iterator,
Program(),
qi::locals<
std::map<std::string, std::shared_ptr<BooleanConstantExpression>>,
std::map<std::string, std::shared_ptr<IntegerConstantExpression>>,
std::map<std::string, std::shared_ptr<DoubleConstantExpression>>,
std::map<std::string, std::unique_ptr<BooleanConstantExpression>>,
std::map<std::string, std::unique_ptr<IntegerConstantExpression>>,
std::map<std::string, std::unique_ptr<DoubleConstantExpression>>,
GlobalVariableInformation,
std::map<std::string, RewardModel>,
std::map<std::string, std::shared_ptr<BaseExpression>>
std::map<std::string, std::unique_ptr<BaseExpression>>
>,
Skipper> {
public:
@ -82,16 +82,16 @@ namespace storm {
Iterator,
Program(),
qi::locals<
std::map<std::string, std::shared_ptr<BooleanConstantExpression>>,
std::map<std::string, std::shared_ptr<IntegerConstantExpression>>,
std::map<std::string, std::shared_ptr<DoubleConstantExpression>>,
std::map<std::string, std::unique_ptr<BooleanConstantExpression>>,
std::map<std::string, std::unique_ptr<IntegerConstantExpression>>,
std::map<std::string, std::unique_ptr<DoubleConstantExpression>>,
GlobalVariableInformation,
std::map<std::string, RewardModel>,
std::map<std::string, std::shared_ptr<BaseExpression>>
std::map<std::string, std::unique_ptr<BaseExpression>>
>,
Skipper> start;
qi::rule<Iterator, Program::ModelType(), Skipper> modelTypeDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> constantDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BooleanConstantExpression>>&, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>&, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>&), Skipper> constantDefinitionList;
qi::rule<Iterator, std::vector<Module>(), Skipper> moduleDefinitionList;
// Rules for global variable definitions
@ -125,16 +125,16 @@ namespace storm {
qi::rule<Iterator, TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
// Rules for label definitions.
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BaseExpression>>&), Skipper> labelDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BaseExpression>>&), Skipper> labelDefinition;
// Rules for constant definitions.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BooleanConstantExpression>>&, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>&, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&), qi::locals<std::shared_ptr<BooleanConstantExpression>>, Skipper> undefinedBooleanConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&), qi::locals<std::shared_ptr<IntegerConstantExpression>>, Skipper> undefinedIntegerConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), qi::locals<std::shared_ptr<DoubleConstantExpression>>, Skipper> undefinedDoubleConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BooleanConstantExpression>>&), Skipper> undefinedBooleanConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<IntegerConstantExpression>>&), Skipper> undefinedIntegerConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<DoubleConstantExpression>>&), Skipper> undefinedDoubleConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedBooleanConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedIntegerConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedDoubleConstantDefinition;
@ -147,14 +147,6 @@ namespace storm {
storm::parser::prism::modelTypeStruct modelType_;
storm::parser::prism::relationalOperatorStruct relations_;
/*!
* Adds a constant of type integer with the given name and value.
*
* @param name The name of the constant.
* @param value An expression definining the value of the constant.
*/
std::shared_ptr<BaseExpression> addIntegerConstant(std::string const& name, std::shared_ptr<BaseExpression> const& value);
/*!
* Adds a label with the given name and expression to the given label-to-expression map.
*
@ -162,7 +154,7 @@ namespace storm {
* @param expression The expression associated with the label.
* @param nameToExpressionMap The map to which the label is added.
*/
void addLabel(std::string const& name, std::shared_ptr<BaseExpression> const& value, std::map<std::string, std::shared_ptr<BaseExpression>>& nameToExpressionMap);
void addLabel(std::string const& name, std::shared_ptr<BaseExpression> const& value, std::map<std::string, std::unique_ptr<BaseExpression>>& nameToExpressionMap);
/*!
* Adds a boolean assignment for the given variable with the given expression and adds it to the
@ -182,8 +174,14 @@ namespace storm {
* @param expression The expression that is assigned to the variable.
* @param variableToAssignmentMap The map to which the assignment is added.
*/
void addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssignmentMap);
void addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& expression, std::map<std::string, Assignment>& variableToAssignmentMap);
void addUndefinedBooleanConstant(std::string const& name, std::map<std::string, std::unique_ptr<BooleanConstantExpression>>& nameToExpressionMap);
void addUndefinedIntegerConstant(std::string const& name, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>& nameToExpressionMap);
void addUndefinedDoubleConstant(std::string const& name, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>& nameToExpressionMap);
/*!
* Creates a module by renaming, i.e. takes the module given by the old name, creates a new module
* with the given name which renames all identifiers according to the given mapping.
@ -237,7 +235,7 @@ namespace storm {
* @param guard The guard of the command.
* @param updates The updates associated with the command.
*/
Command createCommand(std::string const& label, std::shared_ptr<BaseExpression> guard, std::vector<Update> const& updates);
Command createCommand(std::string const& label, std::shared_ptr<BaseExpression> const& guard, std::vector<Update> const& updates);
/*!
* Creates an update with the given likelihood and the given assignments to boolean and integer variables, respectively.
@ -246,7 +244,7 @@ namespace storm {
* @param booleanAssignments The assignments to boolean variables this update involves.
* @param integerAssignments The assignments to integer variables this update involves.
*/
Update createUpdate(std::shared_ptr<BaseExpression> likelihood, std::map<std::string, Assignment> const& booleanAssignments, std::map<std::string, Assignment> const& integerAssignments);
Update createUpdate(std::shared_ptr<BaseExpression> const& likelihood, std::map<std::string, Assignment> const& booleanAssignments, std::map<std::string, Assignment> const& integerAssignments);
};

Write Preview
|||||||
100:0
Loading…
Cancel
Save