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

Fixed an issue with templated variadic template arguments (see http://stackoverflow.com/questions/23119273/use-a-templated-variadic-template-parameter-as-specialized-parameter for discussion) 

Former-commit-id: e7d2d054b6
tempestpy_adaptions
PBerger 11 years ago
parent
94b25c02ca
commit
1d8ae9fc89
20 changed files with 100 additions and 77 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 12
      src/parser/PrismParser.cpp
  2. 23
      src/storage/expressions/Expression.cpp
  3. 28
      src/storage/expressions/Expression.h
  4. 37
      src/storage/expressions/IdentifierSubstitutionVisitor.cpp
  5. 6
      src/storage/expressions/IdentifierSubstitutionVisitor.h
  6. 37
      src/storage/expressions/SubstitutionVisitor.cpp
  7. 6
      src/storage/expressions/SubstitutionVisitor.h
  8. 2
      src/storage/prism/Assignment.cpp
  9. 2
      src/storage/prism/BooleanVariable.cpp
  10. 2
      src/storage/prism/Command.cpp
  11. 2
      src/storage/prism/Constant.cpp
  12. 2
      src/storage/prism/Formula.cpp
  13. 2
      src/storage/prism/IntegerVariable.cpp
  14. 2
      src/storage/prism/Label.cpp
  15. 4
      src/storage/prism/Program.cpp
  16. 2
      src/storage/prism/StateReward.cpp
  17. 2
      src/storage/prism/TransitionReward.cpp
  18. 2
      src/storage/prism/Update.cpp
  19. 2
      src/storage/prism/Variable.cpp
  20. 2
      test/functional/storage/ExpressionTest.cpp

12
src/parser/PrismParser.cpp
View File

@ -585,7 +585,7 @@ namespace storm {
auto const& renamingPair = renaming.find(variable.getName());
LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Boolean variable '" << variable.getName() << " was not renamed.");
booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute<std::map>(expressionRenaming), this->getFilename(), get_line(qi::_1)));
booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
}
// Rename the integer variables.
@ -594,7 +594,7 @@ namespace storm {
auto const& renamingPair = renaming.find(variable.getName());
LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Integer variable '" << variable.getName() << " was not renamed.");
integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute<std::map>(expressionRenaming), variable.getUpperBoundExpression().substitute<std::map>(expressionRenaming), variable.getInitialValueExpression().substitute<std::map>(expressionRenaming), this->getFilename(), get_line(qi::_1)));
integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
}
// Rename commands.
@ -606,12 +606,12 @@ namespace storm {
for (auto const& assignment : update.getAssignments()) {
auto const& renamingPair = renaming.find(assignment.getVariableName());
if (renamingPair != renaming.end()) {
assignments.emplace_back(renamingPair->second, assignment.getExpression().substitute<std::map>(expressionRenaming), this->getFilename(), get_line(qi::_1));
assignments.emplace_back(renamingPair->second, assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1));
} else {
assignments.emplace_back(assignment.getVariableName(), assignment.getExpression().substitute<std::map>(expressionRenaming), this->getFilename(), get_line(qi::_1));
assignments.emplace_back(assignment.getVariableName(), assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1));
}
}
updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute<std::map>(expressionRenaming), assignments, this->getFilename(), get_line(qi::_1));
updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments, this->getFilename(), get_line(qi::_1));
++globalProgramInformation.currentUpdateIndex;
}
@ -621,7 +621,7 @@ namespace storm {
newActionName = renamingPair->second;
}
commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName, command.getGuardExpression().substitute<std::map>(expressionRenaming), updates, this->getFilename(), get_line(qi::_1));
commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1));
++globalProgramInformation.currentCommandIndex;
}

23
src/storage/expressions/Expression.cpp
View File

@ -27,15 +27,21 @@ namespace storm {
// Intentionally left empty.
}
template<template<typename... Arguments> class MapType>
Expression Expression::substitute(MapType<std::string, Expression> const& identifierToExpressionMap) const {
return SubstitutionVisitor<MapType>(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
Expression Expression::substitute(std::map<std::string, Expression> const& identifierToExpressionMap) const {
return SubstitutionVisitor< std::map<std::string, Expression> >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
}
Expression Expression::substitute(std::unordered_map<std::string, Expression> const& identifierToExpressionMap) const {
return SubstitutionVisitor< std::unordered_map<std::string, Expression> >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
}
template<template<typename... Arguments> class MapType>
Expression Expression::substitute(MapType<std::string, std::string> const& identifierToIdentifierMap) const {
return IdentifierSubstitutionVisitor<MapType>(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
Expression Expression::substitute(std::map<std::string, std::string> const& identifierToIdentifierMap) const {
return IdentifierSubstitutionVisitor< std::map<std::string, std::string> >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
}
Expression Expression::substitute(std::unordered_map<std::string, std::string> const& identifierToIdentifierMap) const {
return IdentifierSubstitutionVisitor< std::unordered_map<std::string, std::string> >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
}
bool Expression::evaluateAsBool(Valuation const* valuation) const {
return this->getBaseExpression().evaluateAsBool(valuation);
@ -247,11 +253,6 @@ namespace storm {
return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(ExpressionReturnType::Int, this->getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Ceil)));
}
template Expression Expression::substitute<std::map>(std::map<std::string, storm::expressions::Expression> const&) const;
template Expression Expression::substitute<std::unordered_map>(std::unordered_map<std::string, storm::expressions::Expression> const&) const;
template Expression Expression::substitute<std::map>(std::map<std::string, std::string> const&) const;
template Expression Expression::substitute<std::unordered_map>(std::unordered_map<std::string, std::string> const&) const;
std::ostream& operator<<(std::ostream& stream, Expression const& expression) {
stream << expression.getBaseExpression();
return stream;

28
src/storage/expressions/Expression.h
View File

@ -2,6 +2,8 @@
#define STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_
#include <memory>
#include <map>
#include <unordered_map>
#include "src/storage/expressions/BaseExpression.h"
#include "src/utility/OsDetection.h"
@ -76,8 +78,18 @@ namespace storm {
* @return An expression in which all identifiers in the key set of the mapping are replaced by the
* expression they are mapped to.
*/
template<template<typename... Arguments> class MapType>
Expression substitute(MapType<std::string, Expression> const& identifierToExpressionMap) const;
Expression substitute(std::map<std::string, Expression> const& identifierToExpressionMap) const;
/*!
* Substitutes all occurrences of identifiers according to the given map. Note that this substitution is
* done simultaneously, i.e., identifiers appearing in the expressions that were "plugged in" are not
* substituted.
*
* @param identifierToExpressionMap A mapping from identifiers to the expression they are substituted with.
* @return An expression in which all identifiers in the key set of the mapping are replaced by the
* expression they are mapped to.
*/
Expression substitute(std::unordered_map<std::string, Expression> const& identifierToExpressionMap) const;
/*!
* Substitutes all occurrences of identifiers with different names given by a mapping.
@ -86,8 +98,16 @@ namespace storm {
* @return An expression in which all identifiers in the key set of the mapping are replaced by the
* identifiers they are mapped to.
*/
template<template<typename... Arguments> class MapType>
Expression substitute(MapType<std::string, std::string> const& identifierToIdentifierMap) const;
Expression substitute(std::map<std::string, std::string> const& identifierToIdentifierMap) const;
/*!
* Substitutes all occurrences of identifiers with different names given by a mapping.
*
* @param identifierToIdentifierMap A mapping from identifiers to identifiers they are substituted with.
* @return An expression in which all identifiers in the key set of the mapping are replaced by the
* identifiers they are mapped to.
*/
Expression substitute(std::unordered_map<std::string, std::string> const& identifierToIdentifierMap) const;
/*!
* Evaluates the expression under the valuation of unknowns (variables and constants) given by the

37
src/storage/expressions/IdentifierSubstitutionVisitor.cpp
View File

@ -1,5 +1,6 @@
#include <map>
#include <unordered_map>
#include <string>
#include "src/storage/expressions/IdentifierSubstitutionVisitor.h"
@ -19,18 +20,18 @@
namespace storm {
namespace expressions {
template<template<typename... Arguments> class MapType>
IdentifierSubstitutionVisitor<MapType>::IdentifierSubstitutionVisitor(MapType<std::string, std::string> const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) {
template<typename MapType>
IdentifierSubstitutionVisitor<MapType>::IdentifierSubstitutionVisitor(MapType const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) {
// Intentionally left empty.
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
Expression IdentifierSubstitutionVisitor<MapType>::substitute(BaseExpression const* expression) {
expression->accept(this);
return Expression(this->expressionStack.top());
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(IfThenElseExpression const* expression) {
expression->getCondition()->accept(this);
std::shared_ptr<BaseExpression const> conditionExpression = expressionStack.top();
@ -52,7 +53,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(BinaryBooleanFunctionExpression const* expression) {
expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
@ -70,7 +71,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(BinaryNumericalFunctionExpression const* expression) {
expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
@ -88,7 +89,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(BinaryRelationExpression const* expression) {
expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
@ -106,7 +107,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(BooleanConstantExpression const* expression) {
// If the boolean constant is in the key set of the substitution, we need to replace it.
auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName());
@ -117,7 +118,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(DoubleConstantExpression const* expression) {
// If the double constant is in the key set of the substitution, we need to replace it.
auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName());
@ -128,7 +129,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(IntegerConstantExpression const* expression) {
// If the integer constant is in the key set of the substitution, we need to replace it.
auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName());
@ -139,7 +140,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(VariableExpression const* expression) {
// If the variable is in the key set of the substitution, we need to replace it.
auto const& namePair = this->identifierToIdentifierMap.find(expression->getVariableName());
@ -150,7 +151,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(UnaryBooleanFunctionExpression const* expression) {
expression->getOperand()->accept(this);
std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top();
@ -164,7 +165,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(UnaryNumericalFunctionExpression const* expression) {
expression->getOperand()->accept(this);
std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top();
@ -178,23 +179,23 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(BooleanLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer());
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(IntegerLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer());
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void IdentifierSubstitutionVisitor<MapType>::visit(DoubleLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer());
}
// Explicitly instantiate the class with map and unordered_map.
template class IdentifierSubstitutionVisitor<std::map>;
template class IdentifierSubstitutionVisitor<std::unordered_map>;
template class IdentifierSubstitutionVisitor< std::map<std::string, std::string> >;
template class IdentifierSubstitutionVisitor< std::unordered_map<std::string, std::string> >;
}
}

6
src/storage/expressions/IdentifierSubstitutionVisitor.h
View File

@ -8,7 +8,7 @@
namespace storm {
namespace expressions {
template<template<typename... Arguments> class MapType>
template<typename MapType>
class IdentifierSubstitutionVisitor : public ExpressionVisitor {
public:
/*!
@ -16,7 +16,7 @@ namespace storm {
*
* @param identifierToExpressionMap A mapping from identifiers to expressions.
*/
IdentifierSubstitutionVisitor(MapType<std::string, std::string> const& identifierToExpressionMap);
IdentifierSubstitutionVisitor(MapType const& identifierToExpressionMap);
/*!
* Substitutes the identifiers in the given expression according to the previously given map and returns the
@ -47,7 +47,7 @@ namespace storm {
std::stack<std::shared_ptr<BaseExpression const>> expressionStack;
// A mapping of identifier names to expressions with which they shall be replaced.
MapType<std::string, std::string> const& identifierToIdentifierMap;
MapType const& identifierToIdentifierMap;
};
}
}

37
src/storage/expressions/SubstitutionVisitor.cpp
View File

@ -1,5 +1,6 @@
#include <map>
#include <unordered_map>
#include <string>
#include "src/storage/expressions/SubstitutionVisitor.h"
@ -19,18 +20,18 @@
namespace storm {
namespace expressions {
template<template<typename... Arguments> class MapType>
SubstitutionVisitor<MapType>::SubstitutionVisitor(MapType<std::string, Expression> const& identifierToExpressionMap) : identifierToExpressionMap(identifierToExpressionMap) {
template<typename MapType>
SubstitutionVisitor<MapType>::SubstitutionVisitor(MapType const& identifierToExpressionMap) : identifierToExpressionMap(identifierToExpressionMap) {
// Intentionally left empty.
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
Expression SubstitutionVisitor<MapType>::substitute(BaseExpression const* expression) {
expression->accept(this);
return Expression(this->expressionStack.top());
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void SubstitutionVisitor<MapType>::visit(IfThenElseExpression const* expression) {
expression->getCondition()->accept(this);
std::shared_ptr<BaseExpression const> conditionExpression = expressionStack.top();
@ -52,7 +53,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void SubstitutionVisitor<MapType>::visit(BinaryBooleanFunctionExpression const* expression) {
expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
@ -70,7 +71,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void SubstitutionVisitor<MapType>::visit(BinaryNumericalFunctionExpression const* expression) {
expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
@ -88,7 +89,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void SubstitutionVisitor<MapType>::visit(BinaryRelationExpression const* expression) {
expression->getFirstOperand()->accept(this);
std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
@ -106,7 +107,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void SubstitutionVisitor<MapType>::visit(BooleanConstantExpression const* expression) {
// If the boolean constant is in the key set of the substitution, we need to replace it.
auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName());
@ -117,7 +118,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void SubstitutionVisitor<MapType>::visit(DoubleConstantExpression const* expression) {
// If the double constant is in the key set of the substitution, we need to replace it.
auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName());
@ -128,7 +129,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void SubstitutionVisitor<MapType>::visit(IntegerConstantExpression const* expression) {
// If the integer constant is in the key set of the substitution, we need to replace it.
auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getConstantName());
@ -139,7 +140,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void SubstitutionVisitor<MapType>::visit(VariableExpression const* expression) {
// If the variable is in the key set of the substitution, we need to replace it.
auto const& nameExpressionPair = this->identifierToExpressionMap.find(expression->getVariableName());
@ -150,7 +151,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void SubstitutionVisitor<MapType>::visit(UnaryBooleanFunctionExpression const* expression) {
expression->getOperand()->accept(this);
std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top();
@ -164,7 +165,7 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void SubstitutionVisitor<MapType>::visit(UnaryNumericalFunctionExpression const* expression) {
expression->getOperand()->accept(this);
std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top();
@ -178,23 +179,23 @@ namespace storm {
}
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void SubstitutionVisitor<MapType>::visit(BooleanLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer());
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void SubstitutionVisitor<MapType>::visit(IntegerLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer());
}
template<template<typename... Arguments> class MapType>
template<typename MapType>
void SubstitutionVisitor<MapType>::visit(DoubleLiteralExpression const* expression) {
this->expressionStack.push(expression->getSharedPointer());
}
// Explicitly instantiate the class with map and unordered_map.
template class SubstitutionVisitor<std::map>;
template class SubstitutionVisitor<std::unordered_map>;
template class SubstitutionVisitor< std::map<std::string, Expression> >;
template class SubstitutionVisitor< std::unordered_map<std::string, Expression> >;
}
}

6
src/storage/expressions/SubstitutionVisitor.h
View File

@ -8,7 +8,7 @@
namespace storm {
namespace expressions {
template<template<typename... Arguments> class MapType>
template<typename MapType>
class SubstitutionVisitor : public ExpressionVisitor {
public:
/*!
@ -16,7 +16,7 @@ namespace storm {
*
* @param identifierToExpressionMap A mapping from identifiers to expressions.
*/
SubstitutionVisitor(MapType<std::string, Expression> const& identifierToExpressionMap);
SubstitutionVisitor(MapType const& identifierToExpressionMap);
/*!
* Substitutes the identifiers in the given expression according to the previously given map and returns the
@ -47,7 +47,7 @@ namespace storm {
std::stack<std::shared_ptr<BaseExpression const>> expressionStack;
// A mapping of identifier names to expressions with which they shall be replaced.
MapType<std::string, Expression> const& identifierToExpressionMap;
MapType const& identifierToExpressionMap;
};
}
}

2
src/storage/prism/Assignment.cpp
View File

@ -15,7 +15,7 @@ namespace storm {
}
Assignment Assignment::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return Assignment(this->getVariableName(), this->getExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
return Assignment(this->getVariableName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {

2
src/storage/prism/BooleanVariable.cpp
View File

@ -11,7 +11,7 @@ namespace storm {
}
BooleanVariable BooleanVariable::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return BooleanVariable(this->getName(), this->getInitialValueExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
return BooleanVariable(this->getName(), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) {

2
src/storage/prism/Command.cpp
View File

@ -37,7 +37,7 @@ namespace storm {
newUpdates.emplace_back(update.substitute(substitution));
}
return Command(this->getGlobalIndex(), this->getActionName(), this->getGuardExpression().substitute<std::map>(substitution), newUpdates, this->getFilename(), this->getLineNumber());
return Command(this->getGlobalIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution), newUpdates, this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, Command const& command) {

2
src/storage/prism/Constant.cpp
View File

@ -27,7 +27,7 @@ namespace storm {
}
Constant Constant::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return Constant(this->getType(), this->getName(), this->getExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
return Constant(this->getType(), this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, Constant const& constant) {

2
src/storage/prism/Formula.cpp
View File

@ -19,7 +19,7 @@ namespace storm {
}
Formula Formula::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return Formula(this->getName(), this->getExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
return Formula(this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, Formula const& formula) {

2
src/storage/prism/IntegerVariable.cpp
View File

@ -19,7 +19,7 @@ namespace storm {
}
IntegerVariable IntegerVariable::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return IntegerVariable(this->getName(), this->getLowerBoundExpression().substitute<std::map>(substitution), this->getUpperBoundExpression().substitute<std::map>(substitution), this->getInitialValueExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
return IntegerVariable(this->getName(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) {

2
src/storage/prism/Label.cpp
View File

@ -15,7 +15,7 @@ namespace storm {
}
Label Label::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return Label(this->getName(), this->getStatePredicateExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
return Label(this->getName(), this->getStatePredicateExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, Label const& label) {

4
src/storage/prism/Program.cpp
View File

@ -229,7 +229,7 @@ namespace storm {
LOG_THROW(constantDefinitions.find(constant.getName()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'.");
// Now replace the occurrences of undefined constants in its defining expression.
newConstants.emplace_back(constant.getType(), constant.getName(), constant.getExpression().substitute<std::map>(constantDefinitions), constant.getFilename(), constant.getLineNumber());
newConstants.emplace_back(constant.getType(), constant.getName(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber());
} else {
auto const& variableExpressionPair = constantDefinitions.find(constant.getName());
@ -306,7 +306,7 @@ namespace storm {
newRewardModels.emplace_back(rewardModel.substitute(constantSubstitution));
}
storm::expressions::Expression newInitialStateExpression = this->getInitialStatesExpression().substitute<std::map>(constantSubstitution);
storm::expressions::Expression newInitialStateExpression = this->getInitialStatesExpression().substitute(constantSubstitution);
std::vector<Label> newLabels;
newLabels.reserve(this->getNumberOfLabels());

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

@ -15,7 +15,7 @@ namespace storm {
}
StateReward StateReward::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return StateReward(this->getStatePredicateExpression().substitute<std::map>(substitution), this->getRewardValueExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
return StateReward(this->getStatePredicateExpression().substitute(substitution), this->getRewardValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, StateReward const& stateReward) {

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

@ -19,7 +19,7 @@ namespace storm {
}
TransitionReward TransitionReward::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return TransitionReward(this->getActionName(), this->getStatePredicateExpression().substitute<std::map>(substitution), this->getRewardValueExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
return TransitionReward(this->getActionName(), this->getStatePredicateExpression().substitute(substitution), this->getRewardValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, TransitionReward const& transitionReward) {

2
src/storage/prism/Update.cpp
View File

@ -44,7 +44,7 @@ namespace storm {
newAssignments.emplace_back(assignment.substitute(substitution));
}
return Update(this->getGlobalIndex(), this->getLikelihoodExpression().substitute<std::map>(substitution), newAssignments, this->getFilename(), this->getLineNumber());
return Update(this->getGlobalIndex(), this->getLikelihoodExpression().substitute(substitution), newAssignments, this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, Update const& update) {

2
src/storage/prism/Variable.cpp
View File

@ -8,7 +8,7 @@ namespace storm {
// Nothing to do here.
}
Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), name(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute<std::map>(renaming)), defaultInitialValue(oldVariable.hasDefaultInitialValue()) {
Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), name(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute(renaming)), defaultInitialValue(oldVariable.hasDefaultInitialValue()) {
// Intentionally left empty.
}

2
test/functional/storage/ExpressionTest.cpp
View File

@ -306,7 +306,7 @@ TEST(Expression, SubstitutionTest) {
std::map<std::string, storm::expressions::Expression> substution = { std::make_pair("y", doubleConstExpression), std::make_pair("x", storm::expressions::Expression::createTrue()), std::make_pair("a", storm::expressions::Expression::createTrue()) };
storm::expressions::Expression substitutedExpression;
ASSERT_NO_THROW(substitutedExpression = tempExpression.substitute<std::map>(substution));
ASSERT_NO_THROW(substitutedExpression = tempExpression.substitute(substution));
EXPECT_TRUE(substitutedExpression.simplify().isTrue());
}

Write Preview
Loading…
Cancel
Save