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

fixed ToJaniConverter for the case where not all variables are global

tempestpy_adaptions
TimQu 6 years ago
parent
bb04291860
commit
e2cb1dd78a
2 changed files with 52 additions and 26 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 3
      src/storm/storage/prism/Program.cpp
  2. 65
      src/storm/storage/prism/ToJaniConverter.cpp

3
src/storm/storage/prism/Program.cpp
View File

@ -17,6 +17,7 @@
#include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/InvalidTypeException.h"
#include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/InvalidOperationException.h"
#include "storm/solver/SmtSolver.h" #include "storm/solver/SmtSolver.h"
#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
#include "storm/storage/prism/CompositionVisitor.h" #include "storm/storage/prism/CompositionVisitor.h"
#include "storm/storage/prism/Compositions.h" #include "storm/storage/prism/Compositions.h"
@ -360,7 +361,7 @@ namespace storm {
std::map<storm::expressions::Variable, storm::expressions::Expression> newSubstitution; std::map<storm::expressions::Variable, storm::expressions::Expression> newSubstitution;
for (auto const& substVarExpr : substitution) { 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; return newSubstitution;
} }

65
src/storm/storage/prism/ToJaniConverter.cpp
View File

@ -126,20 +126,38 @@ namespace storm {
for (uint_fast64_t index = 0; index < program.getNumberOfModules(); ++index) { for (uint_fast64_t index = 0; index < program.getNumberOfModules(); ++index) {
storm::prism::Module const& module = program.getModule(index); storm::prism::Module const& module = program.getModule(index);
// Gather all variables occurring in this module
std::set<storm::expressions::Variable> variables;
for (auto const& command : module.getCommands()) { for (auto const& command : module.getCommands()) {
std::set<storm::expressions::Variable> 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& update : command.getUpdates()) {
for (auto const& assignment : update.getAssignments()) { for (auto const& assignment : update.getAssignments()) {
variables = assignment.getExpression().getVariables();
assignment.getExpression().getBaseExpression().gatherVariables(variables);
variables.insert(assignment.getVariable());
}
}
}
// insert the accessing module index for each accessed variable
std::map<storm::expressions::Variable, storm::expressions::Expression> renamedFormulaToFunctionCallMap;
if (module.isRenamedFromModule()) {
renamedFormulaToFunctionCallMap = program.getSubstitutionForRenamedModule(module, formulaToFunctionCallMap);
}
for (auto const& variable : variables) { for (auto const& variable : variables) {
variablesToAccessingModuleIndices[variable].insert(index);
// Check whether the variable actually is a formula
if (formulaToFunctionCallMap.count(variable) > 0) {
std::set<storm::expressions::Variable> variablesInFunctionCall;
if (module.isRenamedFromModule()) {
variablesInFunctionCall = renamedFormulaToFunctionCallMap[variable].getVariables();
} else {
variablesInFunctionCall = formulaToFunctionCallMap[variable].getVariables();
} }
variablesToAccessingModuleIndices[assignment.getVariable()].insert(index);
for (auto const& funVar : variablesInFunctionCall) {
variablesToAccessingModuleIndices[funVar].insert(index);
} }
} else {
variablesToAccessingModuleIndices[variable].insert(index);
} }
} }
} }
@ -168,9 +186,15 @@ namespace storm {
// Variables that are accessed in the label predicate expression should be made global. // Variables that are accessed in the label predicate expression should be made global.
std::set<storm::expressions::Variable> variables = label.getStatePredicateExpression().getVariables(); std::set<storm::expressions::Variable> variables = label.getStatePredicateExpression().getVariables();
for (auto const& variable : variables) { for (auto const& variable : variables) {
if (formulaToFunctionCallMap.count(variable) > 0) {
for (auto const& funVar : formulaToFunctionCallMap[variable].getVariables()) {
variablesToMakeGlobal[funVar] = true;
}
} else {
variablesToMakeGlobal[variable] = true; variablesToMakeGlobal[variable] = true;
} }
} }
}
// Create an initial state restriction if there was an initial construct in the program. // Create an initial state restriction if there was an initial construct in the program.
if (program.hasInitialConstruct()) { if (program.hasInitialConstruct()) {
@ -178,8 +202,14 @@ namespace storm {
// Variables in the initial state expression should be made global // Variables in the initial state expression should be made global
std::set<storm::expressions::Variable> variables = program.getInitialConstruct().getInitialStatesExpression().getVariables(); std::set<storm::expressions::Variable> variables = program.getInitialConstruct().getInitialStatesExpression().getVariables();
for (auto const& variable : variables) { for (auto const& variable : variables) {
if (formulaToFunctionCallMap.count(variable) > 0) {
for (auto const& funVar : formulaToFunctionCallMap[variable].getVariables()) {
variablesToMakeGlobal[funVar] = true;
}
} else {
variablesToMakeGlobal[variable] = true; variablesToMakeGlobal[variable] = true;
} }
}
} else { } else {
janiModel.setInitialStatesRestriction(manager->boolean(true)); janiModel.setInitialStatesRestriction(manager->boolean(true));
} }
@ -219,9 +249,15 @@ namespace storm {
// Variables that are accessed in a reward term should be made global. // Variables that are accessed in a reward term should be made global.
std::set<storm::expressions::Variable> variables = transientLocationExpression.getVariables(); std::set<storm::expressions::Variable> variables = transientLocationExpression.getVariables();
for (auto const& variable : variables) { for (auto const& variable : variables) {
if (formulaToFunctionCallMap.count(variable) > 0) {
for (auto const& funVar : formulaToFunctionCallMap[variable].getVariables()) {
variablesToMakeGlobal[funVar] = true;
}
} else {
variablesToMakeGlobal[variable] = true; variablesToMakeGlobal[variable] = true;
} }
} }
}
std::map<uint_fast64_t, storm::expressions::Expression> actionIndexToExpression; std::map<uint_fast64_t, storm::expressions::Expression> actionIndexToExpression;
for (auto const& actionReward : rewardModel.getStateActionRewards()) { for (auto const& actionReward : rewardModel.getStateActionRewards()) {
@ -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. // 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. // Note that the formula placeholders of non-renamed modules are replaced later.
if (program.getNumberOfFormulas() > 0 && module.isRenamedFromModule()) { if (program.getNumberOfFormulas() > 0 && module.isRenamedFromModule()) {
auto renaming = program.getFinalRenamingOfModule(module);
std::map<storm::expressions::Variable, storm::expressions::Expression> 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<storm::expressions::Variable, storm::expressions::Expression> renamedFormulaToFunctionCallMap;
for (auto const& formulaToFunctionCall : formulaToFunctionCallMap) {
renamedFormulaToFunctionCallMap[formulaToFunctionCall.first] = storm::jani::substituteJaniExpression(formulaToFunctionCall.second, renamingAsSubstitution);
}
auto renamedFormulaToFunctionCallMap = program.getSubstitutionForRenamedModule(module, formulaToFunctionCallMap);
automaton.substitute(renamedFormulaToFunctionCallMap); automaton.substitute(renamedFormulaToFunctionCallMap);
} }

Write Preview
Loading…
Cancel
Save