diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index 66d83ece7..cb33c3205 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -1,24 +1,5 @@ #include "cli.h" -#include "storm/storage/SymbolicModelDescription.h" - -#include "storm/models/ModelBase.h" - -#include "storm/exceptions/OptionParserException.h" - -#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" - -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/models/symbolic/StandardRewardModel.h" - -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/ResourceSettings.h" -#include "storm/settings/modules/JitBuilderSettings.h" -#include "storm/settings/modules/DebugSettings.h" -#include "storm/settings/modules/IOSettings.h" -#include "storm/settings/modules/CoreSettings.h" -#include "storm/settings/modules/ResourceSettings.h" -#include "storm/settings/modules/JaniExportSettings.h" #include "storm/utility/resources.h" #include "storm/utility/file.h" @@ -30,7 +11,7 @@ #include -#include "storm/api/storm.h" +#include "storm-cli-utilities/model-handling.h" // Includes for the linked libraries and versions header. @@ -231,595 +212,7 @@ namespace storm { setLogLevel(); setFileLogging(); } - - struct SymbolicInput { - // The symbolic model description. - boost::optional model; - - // The properties to check. - std::vector properties; - }; - - void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) { - if (ioSettings.isPrismOrJaniInputSet()) { - if (ioSettings.isPrismInputSet()) { - input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename()); - } else { - auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename()); - input.model = janiInput.first; - auto const& janiPropertyInput = janiInput.second; - - if (ioSettings.isJaniPropertiesSet()) { - for (auto const& propName : ioSettings.getJaniProperties()) { - auto propertyIt = janiPropertyInput.find(propName); - STORM_LOG_THROW(propertyIt != janiPropertyInput.end(), storm::exceptions::InvalidArgumentException, "No JANI property with name '" << propName << "' is known."); - input.properties.emplace_back(propertyIt->second); - } - } - } - } - } - - void parseProperties(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input, boost::optional> const& propertyFilter) { - if (ioSettings.isPropertySet()) { - std::vector newProperties; - if (input.model) { - newProperties = storm::api::parsePropertiesForSymbolicModelDescription(ioSettings.getProperty(), input.model.get(), propertyFilter); - } else { - newProperties = storm::api::parseProperties(ioSettings.getProperty(), propertyFilter); - } - - input.properties.insert(input.properties.end(), newProperties.begin(), newProperties.end()); - } - } - - SymbolicInput parseSymbolicInput() { - auto ioSettings = storm::settings::getModule(); - - // Parse the property filter, if any is given. - boost::optional> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter()); - - SymbolicInput input; - parseSymbolicModelDescription(ioSettings, input); - parseProperties(ioSettings, input, propertyFilter); - - return input; - } - - SymbolicInput preprocessSymbolicInput(SymbolicInput const& input) { - auto ioSettings = storm::settings::getModule(); - auto coreSettings = storm::settings::getModule(); - - SymbolicInput output = input; - - // Substitute constant definitions in symbolic input. - std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); - std::map constantDefinitions; - if (output.model) { - constantDefinitions = output.model.get().parseConstantDefinitions(constantDefinitionString); - output.model = output.model.get().preprocess(constantDefinitions); - } - if (!output.properties.empty()) { - output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions); - } - - // Check whether conversion for PRISM to JANI is requested or necessary. - if (input.model && input.model.get().isPrismProgram()) { - bool transformToJani = ioSettings.isPrismToJaniSet(); - bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && ioSettings.isJitSet(); - STORM_LOG_WARN_COND(transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model."); - transformToJani |= transformToJaniForJit; - - if (transformToJani) { - storm::prism::Program const& model = output.model.get().asPrismProgram(); - auto modelAndRenaming = model.toJaniWithLabelRenaming(true); - output.model = modelAndRenaming.first; - - if (!modelAndRenaming.second.empty()) { - std::map const& labelRenaming = modelAndRenaming.second; - std::vector amendedProperties; - for (auto const& property : output.properties) { - amendedProperties.emplace_back(property.substituteLabels(labelRenaming)); - } - output.properties = std::move(amendedProperties); - } - } - } - - return output; - } - - void exportSymbolicInput(SymbolicInput const& input) { - auto ioSettings = storm::settings::getModule(); - if (input.model && input.model.get().isJaniModel()) { - storm::storage::SymbolicModelDescription const& model = input.model.get(); - if (ioSettings.isExportJaniDotSet()) { - storm::api::exportJaniModelAsDot(model.asJaniModel(), ioSettings.getExportJaniDotFilename()); - } - - if (model.isJaniModel() && storm::settings::getModule().isJaniFileSet()) { - storm::api::exportJaniModel(model.asJaniModel(), input.properties, storm::settings::getModule().getJaniFilename()); - } - } - } - - SymbolicInput parseAndPreprocessSymbolicInput() { - SymbolicInput input = parseSymbolicInput(); - input = preprocessSymbolicInput(input); - exportSymbolicInput(input); - return input; - } - - std::vector> createFormulasToRespect(std::vector const& properties) { - std::vector> result = storm::api::extractFormulasFromProperties(properties); - - for (auto const& property : properties) { - if (!property.getFilter().getStatesFormula()->isInitialFormula()) { - result.push_back(property.getFilter().getStatesFormula()); - } - } - - return result; - } - - template - std::shared_ptr buildModelDd(SymbolicInput const& input) { - return storm::api::buildSymbolicModel(input.model.get(), createFormulasToRespect(input.properties)); - } - - template - std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { - auto counterexampleGeneratorSettings = storm::settings::getModule(); - storm::builder::BuilderOptions options(createFormulasToRespect(input.properties)); - options.setBuildChoiceLabels(ioSettings.isBuildChoiceLabelsSet()); - options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); - options.setBuildAllLabels(ioSettings.isBuildFullModelSet()); - options.setBuildAllRewardModels(ioSettings.isBuildFullModelSet()); - if (ioSettings.isBuildFullModelSet()) { - options.clearTerminalStates(); - } - return storm::api::buildSparseModel(input.model.get(), options, ioSettings.isJitSet(), storm::settings::getModule().isDoctorSet()); - } - - template - std::shared_ptr buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings) { - std::shared_ptr result; - if (ioSettings.isExplicitSet()) { - result = storm::api::buildExplicitModel(ioSettings.getTransitionFilename(), ioSettings.getLabelingFilename(), ioSettings.isStateRewardsSet() ? boost::optional(ioSettings.getStateRewardsFilename()) : boost::none, ioSettings.isTransitionRewardsSet() ? boost::optional(ioSettings.getTransitionRewardsFilename()) : boost::none, ioSettings.isChoiceLabelingSet() ? boost::optional(ioSettings.getChoiceLabelingFilename()) : boost::none); - } else if (ioSettings.isExplicitDRNSet()) { - result = storm::api::buildExplicitDRNModel(ioSettings.getExplicitDRNFilename()); - } else { - STORM_LOG_THROW(ioSettings.isExplicitIMCASet(), storm::exceptions::InvalidSettingsException, "Unexpected explicit model input type."); - result = storm::api::buildExplicitIMCAModel(ioSettings.getExplicitIMCAFilename()); - } - return result; - } - - template - std::shared_ptr buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { - storm::utility::Stopwatch modelBuildingWatch(true); - - std::shared_ptr result; - if (input.model) { - if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { - result = buildModelDd(input); - } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) { - result = buildModelSparse(input, ioSettings); - } - } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) { - STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); - result = buildModelExplicit(ioSettings); - } - - modelBuildingWatch.stop(); - if (result) { - STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); - } - - return result; - } - - template - std::shared_ptr> preprocessSparseMarkovAutomaton(std::shared_ptr> const& model) { - std::shared_ptr> result = model; - model->close(); - if (model->hasOnlyTrivialNondeterminism()) { - result = model->convertToCTMC(); - } - return result; - } - template - std::shared_ptr> preprocessSparseModelBisimulation(std::shared_ptr> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings) { - storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; - if (bisimulationSettings.isWeakBisimulationSet()) { - bisimType = storm::storage::BisimulationType::Weak; - } - - STORM_LOG_INFO("Performing bisimulation minimization..."); - return storm::api::performBisimulationMinimization(model, createFormulasToRespect(input.properties), bisimType); - } - - template - std::pair>, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { - auto generalSettings = storm::settings::getModule(); - auto bisimulationSettings = storm::settings::getModule(); - auto ioSettings = storm::settings::getModule(); - - std::pair>, bool> result = std::make_pair(model, false); - - if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { - result.first = preprocessSparseMarkovAutomaton(result.first->template as>()); - result.second = true; - } - - if (generalSettings.isBisimulationSet()) { - result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings); - result.second = true; - } - - return result; - } - - template - void exportSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { - auto ioSettings = storm::settings::getModule(); - - if (ioSettings.isExportExplicitSet()) { - storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), input.model ? input.model.get().getParameterNames() : std::vector()); - } - - if (ioSettings.isExportDotSet()) { - storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename()); - } - } - - template - void exportDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { - // Intentionally left empty. - } - - template - void exportModel(std::shared_ptr const& model, SymbolicInput const& input) { - if (model->isSparseModel()) { - exportSparseModel(model->as>(), input); - } else { - exportDdModel(model->as>(), input); - } - } - - template - std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { - return std::make_pair(model, false); - } - - template - std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { - storm::utility::Stopwatch preprocessingWatch(true); - - std::pair, bool> result = std::make_pair(model, false); - if (model->isSparseModel()) { - result = preprocessSparseModel(result.first->as>(), input); - } else { - STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); - result = preprocessDdModel(result.first->as>(), input); - } - - if (result.second) { - STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); - } - return result; - } - - void printComputingCounterexample(storm::jani::Property const& property) { - STORM_PRINT_AND_LOG("Computing counterexample for property " << *property.getRawFormula() << " ..." << std::endl); - } - - void printCounterexample(std::shared_ptr const& counterexample, storm::utility::Stopwatch* watch = nullptr) { - if (counterexample) { - STORM_PRINT_AND_LOG(*counterexample << std::endl); - if (watch) { - STORM_PRINT_AND_LOG("Time for computation: " << *watch << "." << std::endl); - } - } else { - STORM_PRINT_AND_LOG(" failed." << std::endl); - } - } - - template - void generateCounterexamples(std::shared_ptr const& model, SymbolicInput const& input) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Counterexample generation is not supported for this data-type."); - } - - template <> - void generateCounterexamples(std::shared_ptr const& model, SymbolicInput const& input) { - typedef double ValueType; - - STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Counterexample generation is currently only supported for sparse models."); - auto sparseModel = model->as>(); - - STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for MDPs."); - auto mdp = sparseModel->template as>(); - - auto counterexampleSettings = storm::settings::getModule(); - if (counterexampleSettings.isMinimalCommandSetGenerationSet()) { - STORM_LOG_THROW(input.model && input.model.get().isPrismProgram(), storm::exceptions::NotSupportedException, "Minimal command set counterexamples are only supported for PRISM model input."); - storm::prism::Program const& program = input.model.get().asPrismProgram(); - - bool useMilp = counterexampleSettings.isUseMilpBasedMinimalCommandSetGenerationSet(); - for (auto const& property : input.properties) { - std::shared_ptr counterexample; - printComputingCounterexample(property); - storm::utility::Stopwatch watch(true); - if (useMilp) { - counterexample = storm::api::computePrismHighLevelCounterexampleMilp(program, mdp, property.getRawFormula()); - } else { - counterexample = storm::api::computePrismHighLevelCounterexampleMaxSmt(program, mdp, property.getRawFormula()); - } - watch.stop(); - printCounterexample(counterexample, &watch); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The selected counterexample formalism is unsupported."); - } - } - - template - void printFilteredResult(std::unique_ptr const& result, storm::modelchecker::FilterType ft) { - if (result->isQuantitative()) { - switch (ft) { - case storm::modelchecker::FilterType::VALUES: - STORM_PRINT_AND_LOG(*result); - break; - case storm::modelchecker::FilterType::SUM: - STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().sum()); - break; - case storm::modelchecker::FilterType::AVG: - STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().average()); - break; - case storm::modelchecker::FilterType::MIN: - STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().getMin()); - break; - case storm::modelchecker::FilterType::MAX: - STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().getMax()); - break; - case storm::modelchecker::FilterType::ARGMIN: - case storm::modelchecker::FilterType::ARGMAX: - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Outputting states is not supported."); - case storm::modelchecker::FilterType::EXISTS: - case storm::modelchecker::FilterType::FORALL: - case storm::modelchecker::FilterType::COUNT: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for qualitative results."); - } - } else { - switch (ft) { - case storm::modelchecker::FilterType::VALUES: - STORM_PRINT_AND_LOG(*result << std::endl); - break; - case storm::modelchecker::FilterType::EXISTS: - STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().existsTrue()); - break; - case storm::modelchecker::FilterType::FORALL: - STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().forallTrue()); - break; - case storm::modelchecker::FilterType::COUNT: - STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().count()); - break; - case storm::modelchecker::FilterType::ARGMIN: - case storm::modelchecker::FilterType::ARGMAX: - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Outputting states is not supported."); - case storm::modelchecker::FilterType::SUM: - case storm::modelchecker::FilterType::AVG: - case storm::modelchecker::FilterType::MIN: - case storm::modelchecker::FilterType::MAX: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for quantitative results."); - } - } - STORM_PRINT_AND_LOG(std::endl); - } - - void printModelCheckingProperty(storm::jani::Property const& property) { - STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl); - } - - template - void printResult(std::unique_ptr const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) { - if (result) { - std::stringstream ss; - ss << "'" << *property.getFilter().getStatesFormula() << "'"; - STORM_PRINT_AND_LOG("Result (for " << (property.getFilter().getStatesFormula()->isInitialFormula() ? "initial" : ss.str()) << " states): "); - printFilteredResult(result, property.getFilter().getFilterType()); - if (watch) { - STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl); - } - } else { - STORM_PRINT_AND_LOG(" failed, property is unsupported by selected engine/settings." << std::endl); - } - } - - struct PostprocessingIdentity { - void operator()(std::unique_ptr const&) { - // Intentionally left empty. - } - }; - - template - void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula, std::shared_ptr const& states)> const& verificationCallback, std::function const&)> const& postprocessingCallback = PostprocessingIdentity()) { - for (auto const& property : properties) { - printModelCheckingProperty(property); - storm::utility::Stopwatch watch(true); - std::unique_ptr result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula()); - watch.stop(); - postprocessingCallback(result); - printResult(result, property, &watch); - } - } - - template - void verifyWithAbstractionRefinementEngine(SymbolicInput const& input) { - STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); - verifyProperties(input.properties, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { - STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states."); - return storm::api::verifyWithAbstractionRefinementEngine(input.model.get(), storm::api::createTask(formula, true)); - }); - } - - template - void verifyWithExplorationEngine(SymbolicInput const& input) { - STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); - STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Exploration does not support other data-types than floating points."); - verifyProperties(input.properties, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { - STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states."); - return storm::api::verifyWithExplorationEngine(input.model.get(), storm::api::createTask(formula, true)); - }); - } - - template - void verifyWithSparseEngine(std::shared_ptr const& model, SymbolicInput const& input) { - auto sparseModel = model->as>(); - verifyProperties(input.properties, - [&sparseModel] (std::shared_ptr const& formula, std::shared_ptr const& states) { - bool filterForInitialStates = states->isInitialFormula(); - auto task = storm::api::createTask(formula, filterForInitialStates); - std::unique_ptr result = storm::api::verifyWithSparseEngine(sparseModel, task); - - std::unique_ptr filter; - if (filterForInitialStates) { - filter = std::make_unique(sparseModel->getInitialStates()); - } else { - filter = storm::api::verifyWithSparseEngine(sparseModel, storm::api::createTask(states, false)); - } - if (result && filter) { - result->filter(filter->asQualitativeCheckResult()); - } - return result; - }); - } - - template - void verifyWithHybridEngine(std::shared_ptr const& model, SymbolicInput const& input) { - verifyProperties(input.properties, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { - bool filterForInitialStates = states->isInitialFormula(); - auto task = storm::api::createTask(formula, filterForInitialStates); - - auto symbolicModel = model->as>(); - std::unique_ptr result = storm::api::verifyWithHybridEngine(symbolicModel, task); - - std::unique_ptr filter; - if (filterForInitialStates) { - filter = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()); - } else { - filter = storm::api::verifyWithHybridEngine(symbolicModel, storm::api::createTask(states, false)); - } - if (result && filter) { - result->filter(filter->asQualitativeCheckResult()); - } - return result; - }); - } - - template - void verifyWithDdEngine(std::shared_ptr const& model, SymbolicInput const& input) { - verifyProperties(input.properties, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { - bool filterForInitialStates = states->isInitialFormula(); - auto task = storm::api::createTask(formula, filterForInitialStates); - - auto symbolicModel = model->as>(); - std::unique_ptr result = storm::api::verifyWithDdEngine(model->as>(), storm::api::createTask(formula, true)); - - std::unique_ptr filter; - if (filterForInitialStates) { - filter = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()); - } else { - filter = storm::api::verifyWithDdEngine(symbolicModel, storm::api::createTask(states, false)); - } - if (result && filter) { - result->filter(filter->asQualitativeCheckResult()); - } - return result; - }); - } - - template - typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) { - bool hybrid = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid; - if (hybrid) { - verifyWithHybridEngine(model, input); - } else { - verifyWithDdEngine(model, input); - } - } - - template - typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) { - 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) { - if (model->isSparseModel()) { - verifyWithSparseEngine(model, input); - } else { - STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); - verifySymbolicModel(model, input, coreSettings); - } - } - - template - void processInputWithValueTypeAndDdlib(SymbolicInput const& input) { - auto coreSettings = storm::settings::getModule(); - - // For several engines, no model building step is performed, but the verification is started right away. - storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine(); - if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { - verifyWithAbstractionRefinementEngine(input); - } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) { - verifyWithExplorationEngine(input); - } else { - auto ioSettings = storm::settings::getModule(); - - std::shared_ptr model; - if (!ioSettings.isNoBuildModelSet()) { - model = buildModel(engine, input, ioSettings); - } - - if (model) { - model->printModelInformationToStream(std::cout); - } - - STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); - - if (model) { - auto preprocessingResult = preprocessModel(model, input); - if (preprocessingResult.second) { - model = preprocessingResult.first; - model->printModelInformationToStream(std::cout); - } - } - - if (model) { - exportModel(model, input); - - if (coreSettings.isCounterexampleSet()) { - generateCounterexamples(model, input); - } else { - verifyModel(model, input, coreSettings); - } - } - } - } - - template - void processInputWithValueType(SymbolicInput const& input) { - auto coreSettings = storm::settings::getModule(); - - if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) { - processInputWithValueTypeAndDdlib(input); - } else { - STORM_LOG_ASSERT(coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "Unknown DD library."); - processInputWithValueTypeAndDdlib(input); - } - } void processOptions() { // Start by setting some urgent options (log levels, resources, etc.) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h new file mode 100644 index 000000000..48fb21c8e --- /dev/null +++ b/src/storm-cli-utilities/model-handling.h @@ -0,0 +1,639 @@ +#pragma once + +#include "storm/api/storm.h" + + +#include "storm/utility/resources.h" +#include "storm/utility/file.h" +#include "storm/utility/storm-version.h" +#include "storm/utility/macros.h" + +#include "storm/utility/initialize.h" +#include "storm/utility/Stopwatch.h" + +#include + + +#include "storm/storage/SymbolicModelDescription.h" + +#include "storm/models/ModelBase.h" + +#include "storm/exceptions/OptionParserException.h" + +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" + +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/symbolic/StandardRewardModel.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/JitBuilderSettings.h" +#include "storm/settings/modules/DebugSettings.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/JaniExportSettings.h" + +#include "storm/utility/Stopwatch.h" + +namespace storm { + namespace cli { + + + struct SymbolicInput { + // The symbolic model description. + boost::optional model; + + // The properties to check. + std::vector properties; + }; + + void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) { + if (ioSettings.isPrismOrJaniInputSet()) { + if (ioSettings.isPrismInputSet()) { + input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename()); + } else { + auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename()); + input.model = janiInput.first; + auto const& janiPropertyInput = janiInput.second; + + if (ioSettings.isJaniPropertiesSet()) { + for (auto const& propName : ioSettings.getJaniProperties()) { + auto propertyIt = janiPropertyInput.find(propName); + STORM_LOG_THROW(propertyIt != janiPropertyInput.end(), storm::exceptions::InvalidArgumentException, "No JANI property with name '" << propName << "' is known."); + input.properties.emplace_back(propertyIt->second); + } + } + } + } + } + + void parseProperties(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input, boost::optional> const& propertyFilter) { + if (ioSettings.isPropertySet()) { + std::vector newProperties; + if (input.model) { + newProperties = storm::api::parsePropertiesForSymbolicModelDescription(ioSettings.getProperty(), input.model.get(), propertyFilter); + } else { + newProperties = storm::api::parseProperties(ioSettings.getProperty(), propertyFilter); + } + + input.properties.insert(input.properties.end(), newProperties.begin(), newProperties.end()); + } + } + + SymbolicInput parseSymbolicInput() { + auto ioSettings = storm::settings::getModule(); + + // Parse the property filter, if any is given. + boost::optional> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter()); + + SymbolicInput input; + parseSymbolicModelDescription(ioSettings, input); + parseProperties(ioSettings, input, propertyFilter); + + return input; + } + + SymbolicInput preprocessSymbolicInput(SymbolicInput const& input) { + auto ioSettings = storm::settings::getModule(); + auto coreSettings = storm::settings::getModule(); + + SymbolicInput output = input; + + // Substitute constant definitions in symbolic input. + std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); + std::map constantDefinitions; + if (output.model) { + constantDefinitions = output.model.get().parseConstantDefinitions(constantDefinitionString); + output.model = output.model.get().preprocess(constantDefinitions); + } + if (!output.properties.empty()) { + output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions); + } + + // Check whether conversion for PRISM to JANI is requested or necessary. + if (input.model && input.model.get().isPrismProgram()) { + bool transformToJani = ioSettings.isPrismToJaniSet(); + bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && ioSettings.isJitSet(); + STORM_LOG_WARN_COND(transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model."); + transformToJani |= transformToJaniForJit; + + if (transformToJani) { + storm::prism::Program const& model = output.model.get().asPrismProgram(); + auto modelAndRenaming = model.toJaniWithLabelRenaming(true); + output.model = modelAndRenaming.first; + + if (!modelAndRenaming.second.empty()) { + std::map const& labelRenaming = modelAndRenaming.second; + std::vector amendedProperties; + for (auto const& property : output.properties) { + amendedProperties.emplace_back(property.substituteLabels(labelRenaming)); + } + output.properties = std::move(amendedProperties); + } + } + } + + return output; + } + + void exportSymbolicInput(SymbolicInput const& input) { + auto ioSettings = storm::settings::getModule(); + if (input.model && input.model.get().isJaniModel()) { + storm::storage::SymbolicModelDescription const& model = input.model.get(); + if (ioSettings.isExportJaniDotSet()) { + storm::api::exportJaniModelAsDot(model.asJaniModel(), ioSettings.getExportJaniDotFilename()); + } + + if (model.isJaniModel() && storm::settings::getModule().isJaniFileSet()) { + storm::api::exportJaniModel(model.asJaniModel(), input.properties, storm::settings::getModule().getJaniFilename()); + } + } + } + + SymbolicInput parseAndPreprocessSymbolicInput() { + SymbolicInput input = parseSymbolicInput(); + input = preprocessSymbolicInput(input); + exportSymbolicInput(input); + return input; + } + + std::vector> createFormulasToRespect(std::vector const& properties) { + std::vector> result = storm::api::extractFormulasFromProperties(properties); + + for (auto const& property : properties) { + if (!property.getFilter().getStatesFormula()->isInitialFormula()) { + result.push_back(property.getFilter().getStatesFormula()); + } + } + + return result; + } + + template + std::shared_ptr buildModelDd(SymbolicInput const& input) { + return storm::api::buildSymbolicModel(input.model.get(), createFormulasToRespect(input.properties)); + } + + template + std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { + auto counterexampleGeneratorSettings = storm::settings::getModule(); + storm::builder::BuilderOptions options(createFormulasToRespect(input.properties)); + options.setBuildChoiceLabels(ioSettings.isBuildChoiceLabelsSet()); + options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); + options.setBuildAllLabels(ioSettings.isBuildFullModelSet()); + options.setBuildAllRewardModels(ioSettings.isBuildFullModelSet()); + if (ioSettings.isBuildFullModelSet()) { + options.clearTerminalStates(); + } + return storm::api::buildSparseModel(input.model.get(), options, ioSettings.isJitSet(), storm::settings::getModule().isDoctorSet()); + } + + template + std::shared_ptr buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings) { + std::shared_ptr result; + if (ioSettings.isExplicitSet()) { + result = storm::api::buildExplicitModel(ioSettings.getTransitionFilename(), ioSettings.getLabelingFilename(), ioSettings.isStateRewardsSet() ? boost::optional(ioSettings.getStateRewardsFilename()) : boost::none, ioSettings.isTransitionRewardsSet() ? boost::optional(ioSettings.getTransitionRewardsFilename()) : boost::none, ioSettings.isChoiceLabelingSet() ? boost::optional(ioSettings.getChoiceLabelingFilename()) : boost::none); + } else if (ioSettings.isExplicitDRNSet()) { + result = storm::api::buildExplicitDRNModel(ioSettings.getExplicitDRNFilename()); + } else { + STORM_LOG_THROW(ioSettings.isExplicitIMCASet(), storm::exceptions::InvalidSettingsException, "Unexpected explicit model input type."); + result = storm::api::buildExplicitIMCAModel(ioSettings.getExplicitIMCAFilename()); + } + return result; + } + + template + std::shared_ptr buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { + storm::utility::Stopwatch modelBuildingWatch(true); + + std::shared_ptr result; + if (input.model) { + if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { + result = buildModelDd(input); + } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) { + result = buildModelSparse(input, ioSettings); + } + } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) { + STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); + result = buildModelExplicit(ioSettings); + } + + modelBuildingWatch.stop(); + if (result) { + STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); + } + + return result; + } + + template + std::shared_ptr> preprocessSparseMarkovAutomaton(std::shared_ptr> const& model) { + std::shared_ptr> result = model; + model->close(); + if (model->hasOnlyTrivialNondeterminism()) { + result = model->convertToCTMC(); + } + return result; + } + + template + std::shared_ptr> preprocessSparseModelBisimulation(std::shared_ptr> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings) { + storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; + if (bisimulationSettings.isWeakBisimulationSet()) { + bisimType = storm::storage::BisimulationType::Weak; + } + + STORM_LOG_INFO("Performing bisimulation minimization..."); + return storm::api::performBisimulationMinimization(model, createFormulasToRespect(input.properties), bisimType); + } + + template + std::pair>, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { + auto generalSettings = storm::settings::getModule(); + auto bisimulationSettings = storm::settings::getModule(); + auto ioSettings = storm::settings::getModule(); + + std::pair>, bool> result = std::make_pair(model, false); + + if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { + result.first = preprocessSparseMarkovAutomaton(result.first->template as>()); + result.second = true; + } + + if (generalSettings.isBisimulationSet()) { + result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings); + result.second = true; + } + + return result; + } + + template + void exportSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { + auto ioSettings = storm::settings::getModule(); + + if (ioSettings.isExportExplicitSet()) { + storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), input.model ? input.model.get().getParameterNames() : std::vector()); + } + + if (ioSettings.isExportDotSet()) { + storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename()); + } + } + + template + void exportDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { + // Intentionally left empty. + } + + template + void exportModel(std::shared_ptr const& model, SymbolicInput const& input) { + if (model->isSparseModel()) { + exportSparseModel(model->as>(), input); + } else { + exportDdModel(model->as>(), input); + } + } + + template + std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { + return std::make_pair(model, false); + } + + template + std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { + storm::utility::Stopwatch preprocessingWatch(true); + + std::pair, bool> result = std::make_pair(model, false); + if (model->isSparseModel()) { + result = preprocessSparseModel(result.first->as>(), input); + } else { + STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); + result = preprocessDdModel(result.first->as>(), input); + } + + if (result.second) { + STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); + } + return result; + } + + void printComputingCounterexample(storm::jani::Property const& property) { + STORM_PRINT_AND_LOG("Computing counterexample for property " << *property.getRawFormula() << " ..." << std::endl); + } + + void printCounterexample(std::shared_ptr const& counterexample, storm::utility::Stopwatch* watch = nullptr) { + if (counterexample) { + STORM_PRINT_AND_LOG(*counterexample << std::endl); + if (watch) { + STORM_PRINT_AND_LOG("Time for computation: " << *watch << "." << std::endl); + } + } else { + STORM_PRINT_AND_LOG(" failed." << std::endl); + } + } + + template + void generateCounterexamples(std::shared_ptr const& model, SymbolicInput const& input) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Counterexample generation is not supported for this data-type."); + } + + template <> + void generateCounterexamples(std::shared_ptr const& model, SymbolicInput const& input) { + typedef double ValueType; + + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Counterexample generation is currently only supported for sparse models."); + auto sparseModel = model->as>(); + + STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for MDPs."); + auto mdp = sparseModel->template as>(); + + auto counterexampleSettings = storm::settings::getModule(); + if (counterexampleSettings.isMinimalCommandSetGenerationSet()) { + STORM_LOG_THROW(input.model && input.model.get().isPrismProgram(), storm::exceptions::NotSupportedException, "Minimal command set counterexamples are only supported for PRISM model input."); + storm::prism::Program const& program = input.model.get().asPrismProgram(); + + bool useMilp = counterexampleSettings.isUseMilpBasedMinimalCommandSetGenerationSet(); + for (auto const& property : input.properties) { + std::shared_ptr counterexample; + printComputingCounterexample(property); + storm::utility::Stopwatch watch(true); + if (useMilp) { + counterexample = storm::api::computePrismHighLevelCounterexampleMilp(program, mdp, property.getRawFormula()); + } else { + counterexample = storm::api::computePrismHighLevelCounterexampleMaxSmt(program, mdp, property.getRawFormula()); + } + watch.stop(); + printCounterexample(counterexample, &watch); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The selected counterexample formalism is unsupported."); + } + } + + template + void printFilteredResult(std::unique_ptr const& result, storm::modelchecker::FilterType ft) { + if (result->isQuantitative()) { + switch (ft) { + case storm::modelchecker::FilterType::VALUES: + STORM_PRINT_AND_LOG(*result); + break; + case storm::modelchecker::FilterType::SUM: + STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().sum()); + break; + case storm::modelchecker::FilterType::AVG: + STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().average()); + break; + case storm::modelchecker::FilterType::MIN: + STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().getMin()); + break; + case storm::modelchecker::FilterType::MAX: + STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().getMax()); + break; + case storm::modelchecker::FilterType::ARGMIN: + case storm::modelchecker::FilterType::ARGMAX: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Outputting states is not supported."); + case storm::modelchecker::FilterType::EXISTS: + case storm::modelchecker::FilterType::FORALL: + case storm::modelchecker::FilterType::COUNT: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for qualitative results."); + } + } else { + switch (ft) { + case storm::modelchecker::FilterType::VALUES: + STORM_PRINT_AND_LOG(*result << std::endl); + break; + case storm::modelchecker::FilterType::EXISTS: + STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().existsTrue()); + break; + case storm::modelchecker::FilterType::FORALL: + STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().forallTrue()); + break; + case storm::modelchecker::FilterType::COUNT: + STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().count()); + break; + case storm::modelchecker::FilterType::ARGMIN: + case storm::modelchecker::FilterType::ARGMAX: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Outputting states is not supported."); + case storm::modelchecker::FilterType::SUM: + case storm::modelchecker::FilterType::AVG: + case storm::modelchecker::FilterType::MIN: + case storm::modelchecker::FilterType::MAX: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for quantitative results."); + } + } + STORM_PRINT_AND_LOG(std::endl); + } + + void printModelCheckingProperty(storm::jani::Property const& property) { + STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl); + } + + template + void printResult(std::unique_ptr const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) { + if (result) { + std::stringstream ss; + ss << "'" << *property.getFilter().getStatesFormula() << "'"; + STORM_PRINT_AND_LOG("Result (for " << (property.getFilter().getStatesFormula()->isInitialFormula() ? "initial" : ss.str()) << " states): "); + printFilteredResult(result, property.getFilter().getFilterType()); + if (watch) { + STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl); + } + } else { + STORM_PRINT_AND_LOG(" failed, property is unsupported by selected engine/settings." << std::endl); + } + } + + struct PostprocessingIdentity { + void operator()(std::unique_ptr const&) { + // Intentionally left empty. + } + }; + + template + void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula, std::shared_ptr const& states)> const& verificationCallback, std::function const&)> const& postprocessingCallback = PostprocessingIdentity()) { + for (auto const& property : properties) { + printModelCheckingProperty(property); + storm::utility::Stopwatch watch(true); + std::unique_ptr result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula()); + watch.stop(); + postprocessingCallback(result); + printResult(result, property, &watch); + } + } + + template + void verifyWithAbstractionRefinementEngine(SymbolicInput const& input) { + STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); + verifyProperties(input.properties, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { + STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states."); + return storm::api::verifyWithAbstractionRefinementEngine(input.model.get(), storm::api::createTask(formula, true)); + }); + } + + template + void verifyWithExplorationEngine(SymbolicInput const& input) { + STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); + STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Exploration does not support other data-types than floating points."); + verifyProperties(input.properties, [&input] (std::shared_ptr const& formula, std::shared_ptr const& states) { + STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states."); + return storm::api::verifyWithExplorationEngine(input.model.get(), storm::api::createTask(formula, true)); + }); + } + + template + void verifyWithSparseEngine(std::shared_ptr const& model, SymbolicInput const& input) { + auto sparseModel = model->as>(); + verifyProperties(input.properties, + [&sparseModel] (std::shared_ptr const& formula, std::shared_ptr const& states) { + bool filterForInitialStates = states->isInitialFormula(); + auto task = storm::api::createTask(formula, filterForInitialStates); + std::unique_ptr result = storm::api::verifyWithSparseEngine(sparseModel, task); + + std::unique_ptr filter; + if (filterForInitialStates) { + filter = std::make_unique(sparseModel->getInitialStates()); + } else { + filter = storm::api::verifyWithSparseEngine(sparseModel, storm::api::createTask(states, false)); + } + if (result && filter) { + result->filter(filter->asQualitativeCheckResult()); + } + return result; + }); + } + + template + void verifyWithHybridEngine(std::shared_ptr const& model, SymbolicInput const& input) { + verifyProperties(input.properties, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { + bool filterForInitialStates = states->isInitialFormula(); + auto task = storm::api::createTask(formula, filterForInitialStates); + + auto symbolicModel = model->as>(); + std::unique_ptr result = storm::api::verifyWithHybridEngine(symbolicModel, task); + + std::unique_ptr filter; + if (filterForInitialStates) { + filter = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()); + } else { + filter = storm::api::verifyWithHybridEngine(symbolicModel, storm::api::createTask(states, false)); + } + if (result && filter) { + result->filter(filter->asQualitativeCheckResult()); + } + return result; + }); + } + + template + void verifyWithDdEngine(std::shared_ptr const& model, SymbolicInput const& input) { + verifyProperties(input.properties, [&model] (std::shared_ptr const& formula, std::shared_ptr const& states) { + bool filterForInitialStates = states->isInitialFormula(); + auto task = storm::api::createTask(formula, filterForInitialStates); + + auto symbolicModel = model->as>(); + std::unique_ptr result = storm::api::verifyWithDdEngine(model->as>(), storm::api::createTask(formula, true)); + + std::unique_ptr filter; + if (filterForInitialStates) { + filter = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()); + } else { + filter = storm::api::verifyWithDdEngine(symbolicModel, storm::api::createTask(states, false)); + } + if (result && filter) { + result->filter(filter->asQualitativeCheckResult()); + } + return result; + }); + } + + template + typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) { + bool hybrid = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid; + if (hybrid) { + verifyWithHybridEngine(model, input); + } else { + verifyWithDdEngine(model, input); + } + } + + template + typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) { + 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) { + if (model->isSparseModel()) { + verifyWithSparseEngine(model, input); + } else { + STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); + verifySymbolicModel(model, input, coreSettings); + } + } + + template + std::shared_ptr buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) { + auto ioSettings = storm::settings::getModule(); + std::shared_ptr model; + if (!ioSettings.isNoBuildModelSet()) { + model = buildModel(engine, input, ioSettings); + } + + if (model) { + model->printModelInformationToStream(std::cout); + } + + STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); + + if (model) { + auto preprocessingResult = preprocessModel(model, input); + if (preprocessingResult.second) { + model = preprocessingResult.first; + model->printModelInformationToStream(std::cout); + } + exportModel(model, input); + } + return model; + } + + template + void processInputWithValueTypeAndDdlib(SymbolicInput const& input) { + auto coreSettings = storm::settings::getModule(); + + // For several engines, no model building step is performed, but the verification is started right away. + storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine(); + if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { + verifyWithAbstractionRefinementEngine(input); + } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) { + verifyWithExplorationEngine(input); + } else { + std::shared_ptr model = buildPreprocessExportModelWithValueTypeAndDdlib(input, engine); + + if (model) { + if (coreSettings.isCounterexampleSet()) { + auto ioSettings = storm::settings::getModule(); + generateCounterexamples(model, input); + } else { + auto ioSettings = storm::settings::getModule(); + verifyModel(model, input, coreSettings); + } + } + } + } + + template + void processInputWithValueType(SymbolicInput const& input) { + auto coreSettings = storm::settings::getModule(); + + if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) { + processInputWithValueTypeAndDdlib(input); + } else { + STORM_LOG_ASSERT(coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "Unknown DD library."); + processInputWithValueTypeAndDdlib(input); + } + } + +} +} \ No newline at end of file diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index ef77a720b..be8073bf7 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -58,7 +58,6 @@ namespace storm { for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) { auto const& transition = *transitionIt; - std::cout << transition.getValue() << std::endl; sum += transition.getValue(); if (!storm::utility::isConstant(transition.getValue())) { auto const& transitionVars = transition.getValue().gatherVariables(); diff --git a/src/storm/settings/Argument.cpp b/src/storm/settings/Argument.cpp index ddb39c0ab..555bcdb9d 100644 --- a/src/storm/settings/Argument.cpp +++ b/src/storm/settings/Argument.cpp @@ -12,12 +12,12 @@ namespace storm { namespace settings { template - Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(false), defaultValue(), hasDefaultValue(false) { + Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(false), defaultValue(), hasDefaultValue(false), wasSetFromDefaultValueFlag(false) { // Intentionally left empty. } template - Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(isOptional), defaultValue(), hasDefaultValue(true) { + Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(isOptional), defaultValue(), hasDefaultValue(true), wasSetFromDefaultValueFlag(false) { this->setDefaultValue(defaultValue); } @@ -71,6 +71,12 @@ namespace storm { STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument " << name << " has none."); bool result = this->setFromTypeValue(this->defaultValue, false); STORM_LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument " << name << ", because it was rejected."); + this->wasSetFromDefaultValueFlag = true; + } + + template + bool Argument::wasSetFromDefaultValue() const { + return wasSetFromDefaultValueFlag; } template diff --git a/src/storm/settings/Argument.h b/src/storm/settings/Argument.h index 080d06409..2074557cf 100644 --- a/src/storm/settings/Argument.h +++ b/src/storm/settings/Argument.h @@ -85,6 +85,8 @@ namespace storm { void setFromDefaultValue() override; + virtual bool wasSetFromDefaultValue() const override; + virtual std::string getValueAsString() const override; virtual int_fast64_t getValueAsInteger() const override; @@ -116,6 +118,9 @@ namespace storm { // A flag indicating whether a default value has been provided. bool hasDefaultValue; + // A flag indicating whether the argument was set from the default value. + bool wasSetFromDefaultValueFlag; + /*! * Sets the default value of the argument to the provided value. * diff --git a/src/storm/settings/ArgumentBase.h b/src/storm/settings/ArgumentBase.h index 6808bd815..b48a46183 100644 --- a/src/storm/settings/ArgumentBase.h +++ b/src/storm/settings/ArgumentBase.h @@ -80,6 +80,8 @@ namespace storm { */ virtual void setFromDefaultValue() = 0; + virtual bool wasSetFromDefaultValue() const = 0; + /*! * Tries to set the value of the argument from the given string. * @@ -134,7 +136,7 @@ namespace storm { friend std::ostream& operator<<(std::ostream& out, ArgumentBase const& argument); - protected: + protected: // A flag indicating whether the argument has been set. bool hasBeenSet; diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 493ea71a2..e38c5daf2 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -271,7 +271,7 @@ namespace storm { return moduleIterator->second->getPrintLengthOfLongestOption(); } - void SettingsManager::addModule(std::unique_ptr&& moduleSettings) { + void SettingsManager::addModule(std::unique_ptr&& moduleSettings, bool doRegister) { auto moduleIterator = this->modules.find(moduleSettings->getModuleName()); STORM_LOG_THROW(moduleIterator == this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Unable to register module '" << moduleSettings->getModuleName() << "' because a module with the same name already exists."); @@ -281,12 +281,15 @@ namespace storm { this->modules.emplace(moduleSettings->getModuleName(), std::move(moduleSettings)); auto iterator = this->modules.find(moduleName); std::unique_ptr const& settings = iterator->second; - - // Now register the options of the module. - this->moduleOptions.emplace(moduleName, std::vector>()); - for (auto const& option : settings->getOptions()) { - this->addOption(option); + + if (doRegister) { + // Now register the options of the module. + this->moduleOptions.emplace(moduleName, std::vector>()); + for (auto const& option : settings->getOptions()) { + this->addOption(option); + } } + } void SettingsManager::addOption(std::shared_ptr