diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 844393c08..dd2c3a386 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -4,6 +4,7 @@ #include "storm/storage/jani/TemplateEdge.h" #include "storm/storage/jani/Location.h" #include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" +#include "storm/storage/expressions/ExpressionManager.h" #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" @@ -21,6 +22,24 @@ namespace storm { locationToStartingIndex.push_back(0); } + storm::expressions::Variable cloneVariable(storm::expressions::ExpressionManager& manager, storm::expressions::Variable const& var, std::string const& variablePrefix) { + STORM_LOG_ASSERT(var.getManager() == manager, "expected same manager."); + return manager.declareVariable(variablePrefix + var.getName(), var.getType()); + } + + Automaton Automaton::clone(storm::expressions::ExpressionManager& manager, std::string const& nameOfClone, std::string const& variablePrefix) const { + Automaton result(*this); + result.name = nameOfClone; + result.locationExpressionVariable = cloneVariable(manager, result.locationExpressionVariable, variablePrefix); + auto allVars = result.getAllExpressionVariables(); + std::map oldToNewVarMap; + for (auto const& v : allVars) { + oldToNewVarMap[v] = cloneVariable(manager, v, variablePrefix).getExpression(); + } + result.variables.substituteExpressionVariables(oldToNewVarMap); + result.substitute(oldToNewVarMap); + } + std::string const& Automaton::getName() const { return name; } diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index f9c6d857f..dcdb594c5 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -40,6 +40,8 @@ namespace storm { Automaton(Automaton&& other) = default; Automaton& operator=(Automaton&& other) = default; + Automaton clone(storm::expressions::ExpressionManager& manager, std::string const& nameOfClone, std::string const& variablePrefix) const; + /*! * Retrieves the name of the automaton. */ diff --git a/src/storm/storage/jani/Variable.cpp b/src/storm/storage/jani/Variable.cpp index 6d4c611c3..f693445f1 100644 --- a/src/storm/storage/jani/Variable.cpp +++ b/src/storm/storage/jani/Variable.cpp @@ -26,6 +26,10 @@ namespace storm { storm::expressions::Variable const& Variable::getExpressionVariable() const { return variable; } + + void Variable::setExpressionVariable(storm::expressions::Variable const& newVariable) { + variable = newVariable; + } std::string const& Variable::getName() const { return name; diff --git a/src/storm/storage/jani/Variable.h b/src/storm/storage/jani/Variable.h index d7e3a4b9a..8de11cbba 100644 --- a/src/storm/storage/jani/Variable.h +++ b/src/storm/storage/jani/Variable.h @@ -41,6 +41,11 @@ namespace storm { */ storm::expressions::Variable const& getExpressionVariable() const; + /*! + * Sets the associated expression variable. + */ + void setExpressionVariable(storm::expressions::Variable const& newVariable); + /*! * Retrieves the name of the variable. */ diff --git a/src/storm/storage/jani/VariableSet.cpp b/src/storm/storage/jani/VariableSet.cpp index 10cdd7fba..a2fd5a660 100644 --- a/src/storm/storage/jani/VariableSet.cpp +++ b/src/storm/storage/jani/VariableSet.cpp @@ -1,5 +1,6 @@ #include "storm/storage/jani/VariableSet.h" +#include "storm/storage/expressions/Expressions.h" #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -439,5 +440,15 @@ namespace storm { variable->substitute(substitution); } } + + void VariableSet::substituteExpressionVariables(std::map const& substitution) { + for (auto& variable : variables) { + auto varIt = substitution.find(variable->getExpressionVariable()); + if (varIt != substitution.end()) { + STORM_LOG_ASSERT(varIt->second.isVariable(), "Expected that variables are only substituted by other variables. However, we substitute " << varIt->first.getName() << " by " << varIt->second << "."); + variable->setExpressionVariable(varIt->second.getBaseExpression().asVariableExpression().getVariable()); + } + } + } } } diff --git a/src/storm/storage/jani/VariableSet.h b/src/storm/storage/jani/VariableSet.h index 53f45a359..e4d4e56b9 100644 --- a/src/storm/storage/jani/VariableSet.h +++ b/src/storm/storage/jani/VariableSet.h @@ -282,6 +282,14 @@ namespace storm { */ void substitute(std::map const& substitution); + /*! + * Substitutes the actual variables according to the given substitution. + * @param substitution The substitution. Assumed to only map variables to VariableExpressions. + * @note does not substitute variables in initial expressions, variable bounds, ... + */ + void substituteExpressionVariables(std::map const& substitution); + + private: /// The vector of all variables. std::vector> variables;