From 90095a5455669c60716c4a6a07fca3d5a6a759f7 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 19 Sep 2018 14:28:25 +0200 Subject: [PATCH] correct conversion of prism formulas to jani functions when modules were renamed --- src/storm/storage/prism/ToJaniConverter.cpp | 100 +++++++++++++++----- src/storm/storage/prism/ToJaniConverter.h | 4 + 2 files changed, 80 insertions(+), 24 deletions(-) diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index 322a3baa2..0aebd241f 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -7,6 +7,7 @@ #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Property.h" #include "storm/storage/jani/TemplateEdge.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" #include "storm/storage/jani/expressions/FunctionCallExpression.h" #include "storm/settings/SettingsManager.h" @@ -20,7 +21,8 @@ namespace storm { storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix, bool standardCompliant) { labelRenaming.clear(); rewardModelRenaming.clear(); - + formulaToFunctionCallMap.clear(); + std::shared_ptr manager = program.getManager().getSharedPointer(); bool produceStateRewards = !standardCompliant || program.getModelType() == storm::prism::Program::ModelType::CTMC || program.getModelType() == storm::prism::Program::ModelType::MA; @@ -50,12 +52,41 @@ namespace storm { } // Add all formulas of the PRISM program to the JANI model. - // Also collect a set of variables that occurr in a formula expressions as these need to be made global. - std::set formulaExpressionVariables; + // Also collect a substitution of formula placeholder variables to function call expressions. for (auto const& formula : program.getFormulas()) { - storm::jani::FunctionDefinition funDef(formula.getName(), formula.getType(), {}, formula.getExpression()); + // First find all variables that occurr in the formula definition (including the ones used in called formulae) and the called formulae + std::set variablesInFormula, placeholdersInFormula; + for (auto const& var : formula.getExpression().getVariables()) { + // Check whether var is an actual variable/constant or another formula + auto functionCallIt = formulaToFunctionCallMap.find(var); + if (functionCallIt == formulaToFunctionCallMap.end()) { + variablesInFormula.insert(var); + } else { + storm::expressions::FunctionCallExpression const& innerFunctionCall = dynamic_cast(functionCallIt->second.getBaseExpression()); + for (auto const& innerFunctionArg : innerFunctionCall.getArguments()) { + variablesInFormula.insert(innerFunctionArg->asVariableExpression().getVariable()); + } + placeholdersInFormula.insert(var); + } + } + + // Add a function argument and parameter for each occurring variable and prepare the substitution for the function body + std::map functionBodySubstitution; + std::vector functionParameters; + std::vector> functionArguments; + for (auto const& var : variablesInFormula) { + functionArguments.push_back(var.getExpression().getBaseExpressionPointer()); + functionParameters.push_back(manager->declareVariable(formula.getName() + "__param__" + var.getName() + suffix, var.getType())); + functionBodySubstitution[var] = functionParameters.back().getExpression(); + } + for (auto const& formulaVar : placeholdersInFormula) { + functionBodySubstitution[formulaVar] = storm::jani::substituteJaniExpression(formulaToFunctionCallMap[formulaVar], functionBodySubstitution); + } + + storm::jani::FunctionDefinition funDef(formula.getName(), formula.getType(), functionParameters, storm::jani::substituteJaniExpression(formula.getExpression(), functionBodySubstitution)); janiModel.addFunctionDefinition(funDef); - formula.getExpression().getBaseExpression().gatherVariables(formulaExpressionVariables); + auto functionCallExpression = std::make_shared(*manager, formula.getType(), formula.getName(), functionArguments); + formulaToFunctionCallMap[formula.getExpressionVariable()] = functionCallExpression->toExpression(); } // Maintain a mapping from expression variables to JANI variables so we can fill in the correct objects when @@ -120,7 +151,7 @@ namespace storm { for (auto const& varMods : variablesToAccessingModuleIndices) { assert(!varMods.second.empty()); // If there is exactly one module reading and writing the variable, we can make the variable local to this module. - variablesToMakeGlobal[varMods.first] = allVariablesGlobal || (varMods.second.size() > 1) || formulaExpressionVariables.count(varMods.first) > 0; + variablesToMakeGlobal[varMods.first] = allVariablesGlobal || (varMods.second.size() > 1); } // Go through the labels and construct assignments to transient variables that are added to the locations. @@ -361,6 +392,24 @@ namespace storm { } } + // if there are formulas and if the current module was renamed, we need to apply the renaming to the resulting function calls before replacing the formula placeholders. + // Note that the formula placeholders of non-renamed modules are replaced later. + if (program.getNumberOfFormulas() > 0 && module.isRenamedFromModule()) { + auto renaming = program.getFinalRenamingOfModule(module); + std::map renamingAsSubstitution; + for (auto const& renamingPair : renaming) { + if (manager->hasVariable(renamingPair.first)) { + assert(manager->hasVariable(renamingPair.second)); + renamingAsSubstitution.emplace(manager->getVariable(renamingPair.first), manager->getVariableExpression(renamingPair.second)); + } + } + std::map renamedFormulaToFunctionCallMap; + for (auto const& formulaToFunctionCall : formulaToFunctionCallMap) { + renamedFormulaToFunctionCallMap[formulaToFunctionCall.first] = storm::jani::substituteJaniExpression(formulaToFunctionCall.second, renamedFormulaToFunctionCallMap); + } + automaton.substitute(renamedFormulaToFunctionCallMap); + } + janiModel.addAutomaton(automaton); firstModule = false; } @@ -373,15 +422,10 @@ namespace storm { janiModel.setSystemComposition(janiModel.getStandardSystemComposition()); } - // if there are formulas, replace the placeholder variables by actual function calls in all expressions + // if there are formulas, replace the remaining placeholder variables by actual function calls in all expressions if (program.getNumberOfFormulas() > 0) { janiModel.getModelFeatures().add(storm::jani::ModelFeature::Functions); - std::map substitution; - for (auto const& formula : program.getFormulas()) { - storm::expressions::Expression functionCallExpr = std::make_shared(*manager, formula.getType(), formula.getName(), std::vector>())->toExpression(); - substitution.emplace(formula.getExpressionVariable(), functionCallExpr); - } - janiModel.substitute(substitution); + janiModel.substitute(formulaToFunctionCallMap); } janiModel.finalize(); @@ -406,19 +450,27 @@ namespace storm { } storm::jani::Property ToJaniConverter::applyRenaming(storm::jani::Property const& property) const { + storm::jani::Property result; + bool initialized = false; + if (rewardModelsWereRenamed()) { - auto res = property.substituteRewardModelNames(getRewardModelRenaming()); - if (labelsWereRenamed()) { - res = res.substituteLabels(getLabelRenaming()); - } - return res; - } else { - if (labelsWereRenamed()) { - return property.substituteLabels(getLabelRenaming()); - } else { - return property.clone(); - } + result = property.substituteRewardModelNames(getRewardModelRenaming()); + initialized = true; + } + if (labelsWereRenamed()) { + storm::jani::Property const& currProperty = initialized ? result : property; + result = currProperty.substituteLabels(getLabelRenaming()); + initialized = true; } + if (!formulaToFunctionCallMap.empty()) { + storm::jani::Property const& currProperty = initialized ? result : property; + result = currProperty.substitute(formulaToFunctionCallMap); + initialized = true; + } + if (!initialized) { + result = property.clone(); + } + return result; } std::vector ToJaniConverter::applyRenaming(std::vector const& properties) const { diff --git a/src/storm/storage/prism/ToJaniConverter.h b/src/storm/storage/prism/ToJaniConverter.h index 236855b54..3af62b61d 100644 --- a/src/storm/storage/prism/ToJaniConverter.h +++ b/src/storm/storage/prism/ToJaniConverter.h @@ -3,6 +3,9 @@ #include #include +#include "storm/storage/expressions/Variable.h" +#include "storm/storage/expressions/Expression.h" + namespace storm { namespace jani { class Model; @@ -28,6 +31,7 @@ namespace storm { private: std::map labelRenaming; std::map rewardModelRenaming; + std::map formulaToFunctionCallMap; }; }