diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 11fa5e8ac..c1bb6c8a0 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -443,7 +443,7 @@ namespace storm { } template - std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { + std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input, storm::utility::Engine const& engine) { auto bisimulationSettings = storm::settings::getModule(); auto generalSettings = storm::settings::getModule(); std::pair>, bool> intermediateResult = std::make_pair(model, false); @@ -462,7 +462,7 @@ namespace storm { result = std::make_unique>, bool>>(symbolicModel->template toValueType(), !std::is_same::value); } - if (result && result->first->isSymbolicModel() && storm::settings::getModule().getEngine() == storm::utility::Engine::DdSparse) { + if (result && result->first->isSymbolicModel() && engine == storm::utility::Engine::DdSparse) { // Mark as changed. result->second = true; @@ -479,7 +479,7 @@ namespace storm { } template - std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { + std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input, storm::utility::Engine const& engine) { storm::utility::Stopwatch preprocessingWatch(true); std::pair, bool> result = std::make_pair(model, false); @@ -487,7 +487,7 @@ namespace storm { result = preprocessSparseModel(result.first->as>(), input); } else { STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); - result = preprocessDdModel(result.first->as>(), input); + result = preprocessDdModel(result.first->as>(), input, engine); } preprocessingWatch.stop(); @@ -885,8 +885,7 @@ namespace storm { } template - typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) { - storm::utility::Engine engine = coreSettings.getEngine();; + typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, storm::utility::Engine const& engine) { if (engine == storm::utility::Engine::Hybrid) { verifyWithHybridEngine(model, input); } else if (engine == storm::utility::Engine::Dd) { @@ -897,17 +896,17 @@ namespace storm { } template - typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) { + typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const&, SymbolicInput const& , storm::utility::Engine const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support the selected data-type."); } template - void verifyModel(std::shared_ptr const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) { + void verifyModel(std::shared_ptr const& model, SymbolicInput const& input, storm::utility::Engine const& engine) { if (model->isSparseModel()) { verifyWithSparseEngine(model, input); } else { STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); - verifySymbolicModel(model, input, coreSettings); + verifySymbolicModel(model, input, engine); } } @@ -927,7 +926,7 @@ namespace storm { STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); if (model) { - auto preprocessingResult = preprocessModel(model, input); + auto preprocessingResult = preprocessModel(model, input, engine); if (preprocessingResult.second) { model = preprocessingResult.first; model->printModelInformationToStream(std::cout); @@ -938,48 +937,44 @@ namespace storm { } template - void processInputWithValueTypeAndDdlib(SymbolicInput const& input) { - auto coreSettings = storm::settings::getModule(); + void processInputWithValueTypeAndDdlib(SymbolicInput const& input, storm::utility::Engine const& engine) { auto abstractionSettings = storm::settings::getModule(); auto counterexampleSettings = storm::settings::getModule(); // For several engines, no model building step is performed, but the verification is started right away. - storm::utility::Engine engine = coreSettings.getEngine(); - if (engine == storm::utility::Engine::AbstractionRefinement && abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) { verifyWithAbstractionRefinementEngine(input); } else if (engine == storm::utility::Engine::Exploration) { verifyWithExplorationEngine(input); } else { std::shared_ptr model = buildPreprocessExportModelWithValueTypeAndDdlib(input, engine); - if (model) { if (counterexampleSettings.isCounterexampleSet()) { generateCounterexamples(model, input); } else { - verifyModel(model, input, coreSettings); + verifyModel(model, input, engine); } } } } template - void processInputWithValueType(SymbolicInput const& input) { + void processInputWithValueType(SymbolicInput const& input, storm::utility::Engine const& engine) { auto coreSettings = storm::settings::getModule(); auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue() && generalSettings.isExactSet()) { STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic."); - processInputWithValueTypeAndDdlib(input); + processInputWithValueTypeAndDdlib(input, engine); } else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue() && std::is_same::value && generalSettings.isBisimulationSet() && bisimulationSettings.useExactArithmeticInDdBisimulation()) { STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic."); - processInputWithValueTypeAndDdlib(input); + processInputWithValueTypeAndDdlib(input, engine); } else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) { - processInputWithValueTypeAndDdlib(input); + processInputWithValueTypeAndDdlib(input, engine); } else { STORM_LOG_ASSERT(coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "Unknown DD library."); - processInputWithValueTypeAndDdlib(input); + processInputWithValueTypeAndDdlib(input, engine); } } diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 187d10e52..a8f98fbdc 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -200,14 +200,13 @@ namespace storm { } template - PreprocessResult preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { - auto coreSettings = storm::settings::getModule(); + PreprocessResult preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input, storm::utility::Engine const& engine) { auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); - + PreprocessResult result(model, false); - if (coreSettings.getEngine() == storm::utility::Engine::Hybrid) { + if (engine == storm::utility::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.model = storm::api::transformSymbolicToSparseModel(model); @@ -219,7 +218,7 @@ namespace storm { result.formulas = sparsePreprocessingResult.formulas; } } else { - STORM_LOG_ASSERT(coreSettings.getEngine() == storm::utility::Engine::Dd, "Expected Dd engine."); + STORM_LOG_ASSERT(engine == storm::utility::Engine::Dd, "Expected Dd engine."); if (generalSettings.isBisimulationSet()) { result.model = storm::cli::preprocessDdModelBisimulation(result.model->template as>(), input, bisimulationSettings); result.changed = true; @@ -229,7 +228,7 @@ namespace storm { } template - PreprocessResult preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { + PreprocessResult preprocessModel(std::shared_ptr const& model, SymbolicInput const& input, storm::utility::Engine const& engine) { storm::utility::Stopwatch preprocessingWatch(true); PreprocessResult result(model, false); @@ -237,7 +236,7 @@ namespace storm { result = storm::pars::preprocessSparseModel(result.model->as>(), input); } else { STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); - result = storm::pars::preprocessDdModel(result.model->as>(), input); + result = storm::pars::preprocessDdModel(result.model->as>(), input, engine); } if (result.changed) { @@ -565,17 +564,13 @@ namespace storm { } } - template - void processInputWithValueTypeAndDdlib(SymbolicInput& input) { - auto coreSettings = storm::settings::getModule(); + void processInputWithValueTypeAndDdlib(SymbolicInput& input, storm::utility::Engine const& engine) { auto ioSettings = storm::settings::getModule(); - auto buildSettings = storm::settings::getModule(); auto parSettings = storm::settings::getModule(); auto monSettings = storm::settings::getModule(); - auto engine = coreSettings.getEngine(); STORM_LOG_THROW(engine == storm::utility::Engine::Sparse || engine == storm::utility::Engine::Hybrid || engine == storm::utility::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models."); std::shared_ptr model; @@ -592,7 +587,7 @@ namespace storm { if (model) { - auto preprocessingResult = storm::pars::preprocessModel(model, input); + auto preprocessingResult = storm::pars::preprocessModel(model, input, engine); if (preprocessingResult.changed) { model = preprocessingResult.model; @@ -646,7 +641,7 @@ namespace storm { } if (model) { - auto preprocessingResult = storm::pars::preprocessModel(model, input); + auto preprocessingResult = storm::pars::preprocessModel(model, input, engine); if (preprocessingResult.changed) { model = preprocessingResult.model; @@ -791,7 +786,7 @@ namespace storm { // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(engine); - processInputWithValueTypeAndDdlib(symbolicInput); + processInputWithValueTypeAndDdlib(symbolicInput, engine); } }