diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 626a27a3c..0aa12c3e0 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -568,6 +568,28 @@ namespace storm { STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); + + + if (model) { + auto preprocessingResult = storm::pars::preprocessModel(model, input); + if (preprocessingResult.changed) { + model = preprocessingResult.model; + + if (preprocessingResult.formulas) { + std::vector newProperties; + for (size_t i = 0; i < preprocessingResult.formulas.get().size(); ++i) { + auto formula = preprocessingResult.formulas.get().at(i); + STORM_LOG_ASSERT(i < input.properties.size(), "Index " << i << " greater than number of properties."); + storm::jani::Property property = input.properties.at(i); + newProperties.push_back(storm::jani::Property(property.getName(), formula, property.getUndefinedConstants(), property.getComment())); + } + input.properties = newProperties; + } + + model->printModelInformationToStream(std::cout); + } + } + if (parSettings.isMonotonicityAnalysisSet()) { std::cout << "Hello, Jip1" << std::endl; // Simplify the model @@ -612,7 +634,7 @@ namespace storm { std::cout << "Bye, Jip1" << std::endl; } - if (model) { + if (parSettings.isMonotonicityAnalysisSet() && model) { auto preprocessingResult = storm::pars::preprocessModel(model, input); if (preprocessingResult.changed) { model = preprocessingResult.model; @@ -632,6 +654,7 @@ namespace storm { } } + if (parSettings.isSccEliminationSet()) { storm::utility::Stopwatch eliminationWatch(true); // TODO: check for correct Model type