Browse Source

Formula substitutions need to be performed before constant substitutions because otherwise, constants appearing in formula expressions can not be handled properly

tempestpy_adaptions
TimQu 6 years ago
parent
commit
ccb5a89de3
  1. 6
      src/storm/storage/prism/Program.cpp

6
src/storm/storage/prism/Program.cpp

@ -857,6 +857,10 @@ namespace storm {
} }
Program Program::substituteConstantsFormulas(bool substituteConstants, bool substituteFormulas) const { Program Program::substituteConstantsFormulas(bool substituteConstants, bool substituteFormulas) const {
// Formulas need to be substituted first. otherwise, constants appearing in formula expressions can not be handled properly
if (substituteConstants && substituteFormulas) {
return this->substituteFormulas().substituteConstants();
}
// We start by creating the appropriate substitution. // We start by creating the appropriate substitution.
std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = getConstantsFormulasSubstitution(substituteConstants, substituteFormulas); std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = getConstantsFormulasSubstitution(substituteConstants, substituteFormulas);
@ -1316,7 +1320,7 @@ namespace storm {
Program Program::simplify() { Program Program::simplify() {
// Start by substituting the constants, because this will potentially erase some commands or even actions. // Start by substituting the constants, because this will potentially erase some commands or even actions.
Program substitutedProgram = this->substituteConstants();
Program substitutedProgram = this->substituteConstantsFormulas();
// As we possibly delete some commands and some actions might be dropped from modules altogether, we need to // As we possibly delete some commands and some actions might be dropped from modules altogether, we need to
// maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a] // maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a]

Loading…
Cancel
Save