Browse Source

simplify prism programs now also simplifies labels

tempestpy_adaptions
Sebastian Junges 5 years ago
parent
commit
bb200fe9f4
  1. 9
      src/storm/storage/prism/Program.cpp

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

@ -1498,8 +1498,13 @@ namespace storm {
}
}
}
return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, getLabels(), getObservationLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
std::vector<Label> newLabels;
for(auto const& label : this->getLabels()) {
newLabels.emplace_back(label.getName(), label.getStatePredicateExpression().simplify());
}
return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, newLabels, getObservationLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
}
Program Program::flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {

Loading…
Cancel
Save