From 6e2046e3577429068d36166bb36f1be2811d4162 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 19 Sep 2018 14:27:41 +0200 Subject: [PATCH] fixed formula substitution within renamed modules of a prism program --- src/storm/storage/prism/Program.cpp | 98 +++++++++++++++++++++-------- src/storm/storage/prism/Program.h | 21 ++++++- 2 files changed, 91 insertions(+), 28 deletions(-) diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index c89da44fe..864b4df81 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -324,22 +324,77 @@ namespace storm { } std::map Program::getConstantsSubstitution() const { - std::map constantsSubstitution; - for (auto const& constant : this->getConstants()) { - if (constant.isDefined()) { - constantsSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression()); + return getConstantsFormulasSubstitution(true, false); + } + + std::map Program::getFormulasSubstitution() const { + return getConstantsFormulasSubstitution(false, true); + } + + std::map Program::getConstantsFormulasSubstitution(bool getConstantsSubstitution, bool getFormulasSubstitution) const { + std::map result; + if (getConstantsSubstitution) { + for (auto const& constant : this->getConstants()) { + if (constant.isDefined()) { + result.emplace(constant.getExpressionVariable(), constant.getExpression().substitute(result)); + } } } - return constantsSubstitution; + if (getFormulasSubstitution) { + for (auto const& formula : this->getFormulas()) { + result.emplace(formula.getExpressionVariable(), formula.getExpression().substitute(result)); + } + } + return result; } - std::map Program::getConstantsFormulasSubstitution() const { - auto result = getConstantsSubstitution(); - for (auto const& formula : this->getFormulas()) { - result.emplace(formula.getExpressionVariable(), formula.getExpression()); + std::map Program::getSubstitutionForRenamedModule(Module const& renamedModule, std::map const& substitution) const { + auto renaming = getFinalRenamingOfModule(renamedModule); + std::map renamingAsSubstitution; + for (auto const& renamingPair : renaming) { + if (getManager().hasVariable(renamingPair.first)) { + assert(getManager().hasVariable(renamingPair.second)); + renamingAsSubstitution.emplace(getManager().getVariable(renamingPair.first), getManager().getVariableExpression(renamingPair.second)); + } } - return result; + + std::map newSubstitution; + for (auto const& substVarExpr : substitution) { + STORM_LOG_ASSERT(renamingAsSubstitution.count(substVarExpr.first) == 0, "Conflict: The substitution substitutes the renamed variable " << substVarExpr.first.getName() << "."); + newSubstitution.emplace(substVarExpr.first, substVarExpr.second.substitute(renamingAsSubstitution)); + } + return newSubstitution; + } + + std::map Program::getFinalRenamingOfModule(Module const& renamedModule) const { + std::vector moduleStack = {&renamedModule}; + while (moduleStack.back()->isRenamedFromModule()) { + moduleStack.push_back(&getModule(moduleStack.back()->getBaseModule())); + } + + assert(!moduleStack.back()->isRenamedFromModule()); + moduleStack.pop_back(); + assert(moduleStack.empty() || moduleStack.back()->isRenamedFromModule()); + std::map currentRenaming; + while (!moduleStack.empty()) { + Module const& currentModule = *moduleStack.back(); + moduleStack.pop_back(); + assert(currentModule.isRenamedFromModule()); + std::map newRenaming = currentModule.getRenaming(); + for (auto const& renaimingPair : newRenaming) { + auto findRes = currentRenaming.find(renaimingPair.second); + if (findRes != currentRenaming.end()) { + newRenaming[renaimingPair.second] = findRes->second; + currentRenaming.erase(findRes); + } + } + newRenaming.insert(currentRenaming.begin(), currentRenaming.end()); + currentRenaming = std::move(newRenaming); + } + return currentRenaming; } + + std::size_t Program::getNumberOfConstants() const { return this->getConstants().size(); @@ -805,36 +860,20 @@ namespace storm { Program Program::substituteConstantsFormulas(bool substituteConstants, bool substituteFormulas) const { // We start by creating the appropriate substitution. - std::map substitution; + std::map substitution = getConstantsFormulasSubstitution(substituteConstants, substituteFormulas); - // Start with substituting constants. In a sane model, constant definitions do not contain formulas. std::vector newConstants; newConstants.reserve(this->getNumberOfConstants()); for (auto const& oldConstant : this->getConstants()) { - // apply the substitutions gathered so far to the constant definition *before* adding it to the substitution. newConstants.push_back(oldConstant.substitute(substitution)); - - // Put the corresponding expression in the substitution (if requested). - auto const& constant = newConstants.back(); - if (substituteConstants && constant.isDefined()) { - substitution.emplace(constant.getExpressionVariable(), constant.getExpression().simplify()); - } } - // Secondly, handle the formulas. These might contain constants std::vector newFormulas; newFormulas.reserve(this->getNumberOfFormulas()); for (auto const& oldFormula : this->getFormulas()) { - // apply the currently gathered substitutions on the formula definition *before* adding it to the substitution. newFormulas.emplace_back(oldFormula.substitute(substitution)); - // Put the corresponding expression in the substitution (if requested). - auto const& formula = newFormulas.back(); - if (substituteFormulas) { - substitution.emplace(formula.getExpressionVariable(), formula.getExpression().simplify()); - } } - // Now we can substitute the constants/formulas in all expressions appearing in the program. std::vector newBooleanVariables; newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables()); for (auto const& booleanVariable : this->getGlobalBooleanVariables()) { @@ -850,6 +889,11 @@ namespace storm { std::vector newModules; newModules.reserve(this->getNumberOfModules()); for (auto const& module : this->getModules()) { + if (module.isRenamedFromModule()) { + // The renaming needs to be applied to the substitution as well. + auto renamedSubstitution = getSubstitutionForRenamedModule(module, substitution); + newModules.emplace_back(module.substitute(renamedSubstitution)); + } newModules.emplace_back(module.substitute(substitution)); } diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 151388cbb..5046b5541 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -138,13 +138,31 @@ namespace storm { */ std::map getConstantsSubstitution() const; + /*! + * Retrieves a mapping of all formula variables to their defining expressions. + * + * @return A mapping from constants to their 'values'. + */ + std::map getFormulasSubstitution() const; + /*! * Retrieves a mapping of all defined constants and formula variables to their defining expressions * * @return A mapping from constants and formulas to their expressions. */ - std::map getConstantsFormulasSubstitution() const; + std::map getConstantsFormulasSubstitution(bool getConstantsSubstitution = true, bool getFormulasSubstitution = true) const; + /*! + * Applies the renaming of a renamed module to the given substitution. + */ + std::map getSubstitutionForRenamedModule(Module const& renamedModule, std::map const& substitution) const; + + /*! + * Gets the renaming of a module after flattening all renamings. + * Note that the base of a renamed module might again be a renamed module. + */ + std::map getFinalRenamingOfModule(Module const& renamedModule) const; + /*! * Retrieves all constants defined in the program. * @@ -580,6 +598,7 @@ namespace storm { /*! * Substitutes all formulas appearing in the expressions of the program by their defining expressions. * + * The resulting program still contains the function definition, but does not apply them. * @return The resulting program that only contains expressions over variables of the program (and maybe constants). */ Program substituteFormulas() const;