From bcde728c3c87abe2a2bfa15ca2c23b6356f75cd2 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 30 Jan 2019 22:14:42 +0100 Subject: [PATCH] Transform formulas to deterministic-time as well --- src/storm-pars-cli/storm-pars.cpp | 80 ++++++++++++++++++++----------- 1 file changed, 53 insertions(+), 27 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index e522f0baf..b001381b7 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -45,6 +45,16 @@ namespace storm { bool graphPreserving; bool exact; }; + + struct PreprocessResult { + PreprocessResult(std::shared_ptr const& model, bool changed) : changed(changed), model(model) { + // Intentionally left empty. + } + + bool changed; + std::shared_ptr model; + boost::optional>> formulas; + }; template std::vector> parseRegions(std::shared_ptr const& model) { @@ -127,72 +137,76 @@ namespace storm { } template - std::pair, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { + PreprocessResult preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); auto parametricSettings = storm::settings::getModule(); - std::pair, bool> result = std::make_pair(model, false); + PreprocessResult result(model, false); - if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { - result.first = storm::cli::preprocessSparseMarkovAutomaton(result.first->template as>()); - result.second = true; + if (result.model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + result.model = storm::cli::preprocessSparseMarkovAutomaton(result.model->template as>()); + result.changed = true; } if (generalSettings.isBisimulationSet()) { - result.first = storm::cli::preprocessSparseModelBisimulation(result.first->template as>(), input, bisimulationSettings); - result.second = true; + result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as>(), input, bisimulationSettings); + result.changed = true; } - if (parametricSettings.transformContinuousModel() && (result.first->isOfType(storm::models::ModelType::Ctmc) || result.first->isOfType(storm::models::ModelType::MarkovAutomaton))) { - result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as>()), storm::api::extractFormulasFromProperties(input.properties)).first; - result.second = true; + if (parametricSettings.transformContinuousModel() && (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton))) { + auto transformResult = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*model->template as>()), storm::api::extractFormulasFromProperties(input.properties)); + result.model = transformResult.first; + // Set transformed properties as new properties in input + result.formulas = transformResult.second; + result.changed = true; } return result; } template - std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { + PreprocessResult preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto coreSettings = storm::settings::getModule(); auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); - std::pair, bool> result = std::make_pair(model, false); + PreprocessResult result(model, false); if (coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid) { // Currently, hybrid engine for parametric models just refers to building the model symbolically. STORM_LOG_INFO("Translating symbolic model to sparse model..."); - result.first = storm::api::transformSymbolicToSparseModel(model); - result.second = true; + result.model = storm::api::transformSymbolicToSparseModel(model); + result.changed = true; // Invoke preprocessing on the sparse model - auto sparsePreprocessingResult = storm::pars::preprocessSparseModel(result.first->as>(), input); - if (sparsePreprocessingResult.second) { - result.first = sparsePreprocessingResult.first; + PreprocessResult sparsePreprocessingResult = storm::pars::preprocessSparseModel(result.model->as>(), input); + if (sparsePreprocessingResult.changed) { + result.model = sparsePreprocessingResult.model; + result.formulas = sparsePreprocessingResult.formulas; } } else { STORM_LOG_ASSERT(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Dd, "Expected Dd engine."); if (generalSettings.isBisimulationSet()) { - result.first = storm::cli::preprocessDdModelBisimulation(result.first->template as>(), input, bisimulationSettings); - result.second = true; + result.model = storm::cli::preprocessDdModelBisimulation(result.model->template as>(), input, bisimulationSettings); + result.changed = true; } } return result; } template - std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { + PreprocessResult preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { storm::utility::Stopwatch preprocessingWatch(true); - - std::pair, bool> result = std::make_pair(model, false); + + PreprocessResult result(model, false); if (model->isSparseModel()) { - result = storm::pars::preprocessSparseModel(result.first->as>(), input); + result = storm::pars::preprocessSparseModel(result.model->as>(), input); } else { STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); - result = storm::pars::preprocessDdModel(result.first->as>(), input); + result = storm::pars::preprocessDdModel(result.model->as>(), input); } - if (result.second) { + if (result.changed) { STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); } return result; @@ -536,8 +550,20 @@ namespace storm { if (model) { auto preprocessingResult = storm::pars::preprocessModel(model, input); - if (preprocessingResult.second) { - model = preprocessingResult.first; + 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); } }