From e2cb1dd78a301326ab960d9b6bc8bc7456e1b6da Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 20 Sep 2018 15:09:55 +0200 Subject: [PATCH] fixed ToJaniConverter for the case where not all variables are global --- src/storm/storage/prism/Program.cpp | 3 +- src/storm/storage/prism/ToJaniConverter.cpp | 75 ++++++++++++++------- 2 files changed, 52 insertions(+), 26 deletions(-) diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 18299f4bd..b9806207f 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -17,6 +17,7 @@ #include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/solver/SmtSolver.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" #include "storm/storage/prism/CompositionVisitor.h" #include "storm/storage/prism/Compositions.h" @@ -360,7 +361,7 @@ namespace storm { std::map newSubstitution; for (auto const& substVarExpr : substitution) { - newSubstitution.emplace(substVarExpr.first, substVarExpr.second.substitute(renamingAsSubstitution)); + newSubstitution.emplace(substVarExpr.first, storm::jani::substituteJaniExpression(substVarExpr.second, renamingAsSubstitution)); } return newSubstitution; } diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index c1f9b14d3..2ab209f6b 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -126,20 +126,38 @@ namespace storm { for (uint_fast64_t index = 0; index < program.getNumberOfModules(); ++index) { storm::prism::Module const& module = program.getModule(index); + // Gather all variables occurring in this module + std::set variables; for (auto const& command : module.getCommands()) { - std::set variables = command.getGuardExpression().getVariables(); - for (auto const& variable : variables) { - variablesToAccessingModuleIndices[variable].insert(index); - } - + command.getGuardExpression().getBaseExpression().gatherVariables(variables); for (auto const& update : command.getUpdates()) { for (auto const& assignment : update.getAssignments()) { - variables = assignment.getExpression().getVariables(); - for (auto const& variable : variables) { - variablesToAccessingModuleIndices[variable].insert(index); - } - variablesToAccessingModuleIndices[assignment.getVariable()].insert(index); + assignment.getExpression().getBaseExpression().gatherVariables(variables); + variables.insert(assignment.getVariable()); + } + } + } + + // insert the accessing module index for each accessed variable + std::map renamedFormulaToFunctionCallMap; + if (module.isRenamedFromModule()) { + renamedFormulaToFunctionCallMap = program.getSubstitutionForRenamedModule(module, formulaToFunctionCallMap); + } + + for (auto const& variable : variables) { + // Check whether the variable actually is a formula + if (formulaToFunctionCallMap.count(variable) > 0) { + std::set variablesInFunctionCall; + if (module.isRenamedFromModule()) { + variablesInFunctionCall = renamedFormulaToFunctionCallMap[variable].getVariables(); + } else { + variablesInFunctionCall = formulaToFunctionCallMap[variable].getVariables(); + } + for (auto const& funVar : variablesInFunctionCall) { + variablesToAccessingModuleIndices[funVar].insert(index); } + } else { + variablesToAccessingModuleIndices[variable].insert(index); } } } @@ -168,7 +186,13 @@ namespace storm { // Variables that are accessed in the label predicate expression should be made global. std::set variables = label.getStatePredicateExpression().getVariables(); for (auto const& variable : variables) { - variablesToMakeGlobal[variable] = true; + if (formulaToFunctionCallMap.count(variable) > 0) { + for (auto const& funVar : formulaToFunctionCallMap[variable].getVariables()) { + variablesToMakeGlobal[funVar] = true; + } + } else { + variablesToMakeGlobal[variable] = true; + } } } @@ -178,7 +202,13 @@ namespace storm { // Variables in the initial state expression should be made global std::set variables = program.getInitialConstruct().getInitialStatesExpression().getVariables(); for (auto const& variable : variables) { - variablesToMakeGlobal[variable] = true; + if (formulaToFunctionCallMap.count(variable) > 0) { + for (auto const& funVar : formulaToFunctionCallMap[variable].getVariables()) { + variablesToMakeGlobal[funVar] = true; + } + } else { + variablesToMakeGlobal[variable] = true; + } } } else { janiModel.setInitialStatesRestriction(manager->boolean(true)); @@ -219,7 +249,13 @@ namespace storm { // Variables that are accessed in a reward term should be made global. std::set variables = transientLocationExpression.getVariables(); for (auto const& variable : variables) { - variablesToMakeGlobal[variable] = true; + if (formulaToFunctionCallMap.count(variable) > 0) { + for (auto const& funVar : formulaToFunctionCallMap[variable].getVariables()) { + variablesToMakeGlobal[funVar] = true; + } + } else { + variablesToMakeGlobal[variable] = true; + } } } @@ -371,18 +407,7 @@ 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, renamingAsSubstitution); - } + auto renamedFormulaToFunctionCallMap = program.getSubstitutionForRenamedModule(module, formulaToFunctionCallMap); automaton.substitute(renamedFormulaToFunctionCallMap); }