From 9c685f3bdb628c807a8071273c63c0d19f7ba590 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 19 Oct 2017 16:03:26 +0200 Subject: [PATCH] started on partial bisimulation model checker --- src/storm-cli-utilities/model-handling.h | 222 +++++++++--------- src/storm/api/verification.h | 56 +++-- .../PartialBisimulationMdpModelChecker.cpp | 19 ++ .../PartialBisimulationMdpModelChecker.h | 29 +++ .../symbolic/StochasticTwoPlayerGame.cpp | 1 + .../settings/modules/AbstractionSettings.cpp | 17 ++ .../settings/modules/AbstractionSettings.h | 10 + .../storage/dd/BisimulationDecomposition.cpp | 2 + .../bisimulation/PartialQuotientExtractor.cpp | 25 +- .../bisimulation/PartialQuotientExtractor.h | 8 +- 10 files changed, 248 insertions(+), 141 deletions(-) create mode 100644 src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp create mode 100644 src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index d91d84479..2842d653a 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -37,16 +37,16 @@ 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()) { @@ -55,7 +55,7 @@ namespace storm { 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); @@ -66,7 +66,7 @@ namespace storm { } } } - + void parseProperties(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input, boost::optional> const& propertyFilter) { if (ioSettings.isPropertySet()) { std::vector newProperties; @@ -75,30 +75,30 @@ namespace storm { } 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; @@ -109,19 +109,19 @@ namespace storm { 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; @@ -132,10 +132,10 @@ namespace storm { } } } - + return output; } - + void exportSymbolicInput(SymbolicInput const& input) { auto ioSettings = storm::settings::getModule(); if (input.model && input.model.get().isJaniModel()) { @@ -143,37 +143,37 @@ namespace storm { 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), storm::settings::getModule().isBuildFullModelSet()); } - + template std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { auto counterexampleGeneratorSettings = storm::settings::getModule(); @@ -188,7 +188,7 @@ namespace storm { } 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; @@ -202,11 +202,11 @@ namespace storm { } 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) { @@ -218,15 +218,15 @@ namespace storm { 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("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; @@ -238,57 +238,57 @@ namespace storm { } 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; + 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()) { @@ -297,7 +297,7 @@ namespace storm { exportDdModel(model->as>(), input); } } - + template std::shared_ptr> preprocessDdModelBisimulation(std::shared_ptr> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings) { STORM_LOG_WARN_COND(!bisimulationSettings.isWeakBisimulationSet(), "Weak bisimulation is currently not supported on DDs. Falling back to strong bisimulation."); @@ -319,11 +319,11 @@ namespace storm { return result; } - + 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); @@ -333,17 +333,17 @@ namespace storm { } preprocessingWatch.stop(); - + if (result.second) { STORM_PRINT(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); } return result; } - + void printComputingCounterexample(storm::jani::Property const& property) { STORM_PRINT("Computing counterexample for property " << *property.getRawFormula() << " ..." << std::endl); } - + void printCounterexample(std::shared_ptr const& counterexample, storm::utility::Stopwatch* watch = nullptr) { if (counterexample) { STORM_PRINT(*counterexample << std::endl); @@ -354,27 +354,27 @@ namespace storm { STORM_PRINT(" 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; @@ -392,7 +392,7 @@ namespace storm { 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()) { @@ -446,11 +446,11 @@ namespace storm { } STORM_PRINT(std::endl); } - + void printModelCheckingProperty(storm::jani::Property const& property) { STORM_PRINT(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) { @@ -465,25 +465,25 @@ namespace storm { STORM_PRINT(" 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); - } + 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."); @@ -492,7 +492,7 @@ namespace storm { 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."); @@ -502,7 +502,7 @@ namespace storm { 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>(); @@ -511,7 +511,7 @@ namespace storm { 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()); @@ -524,16 +524,16 @@ namespace storm { 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()); @@ -546,16 +546,16 @@ namespace storm { 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()); @@ -568,22 +568,24 @@ namespace storm { 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) { + storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine();; + if (engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { verifyWithHybridEngine(model, input); - } else { + } else if (engine == storm::settings::modules::CoreSettings::Engine::Dd) { verifyWithDdEngine(model, input); + } else { + verifyWithAbstractionRefinementEngine(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()) { @@ -593,7 +595,7 @@ namespace storm { verifySymbolicModel(model, input, coreSettings); } } - + template std::shared_ptr buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) { auto ioSettings = storm::settings::getModule(); @@ -601,13 +603,13 @@ namespace storm { 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) { @@ -618,20 +620,22 @@ namespace storm { } return model; } - + template void processInputWithValueTypeAndDdlib(SymbolicInput const& input) { auto coreSettings = storm::settings::getModule(); + auto abstractionSettings = 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) { + + if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement && abstractionSettings.getMethod() == storm::settings::modules::AbstractionSettings::Method::Games) { 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(); @@ -643,12 +647,12 @@ namespace storm { } } } - + template void processInputWithValueType(SymbolicInput const& input) { auto coreSettings = storm::settings::getModule(); auto generalSettings = 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); @@ -659,6 +663,6 @@ namespace storm { processInputWithValueTypeAndDdlib(input); } } - -} + + } } diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index 16c42cd7e..6b70c80bc 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -12,6 +12,7 @@ #include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" #include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h" +#include "storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h" #include "storm/modelchecker/exploration/SparseExplorationModelChecker.h" #include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" @@ -30,7 +31,7 @@ namespace storm { namespace api { - + template storm::modelchecker::CheckTask createTask(std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { return storm::modelchecker::CheckTask(*formula, onlyInitialStatesRelevant); @@ -41,6 +42,7 @@ namespace storm { STORM_LOG_THROW(model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC || model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MDP, storm::exceptions::NotSupportedException, "Can only treat DTMCs/MDPs using the abstraction refinement engine."); std::unique_ptr result; + if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC) { storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model); if (modelchecker.canHandle(task)) { @@ -51,21 +53,47 @@ namespace storm { if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException); } return result; } - + template typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support data type."); } + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + storm::modelchecker::PartialBisimulationMdpModelChecker> modelchecker(model->as>()); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + } else if (model->getType() == storm::models::ModelType::Mdp) { + storm::modelchecker::PartialBisimulationMdpModelChecker> modelchecker(model->as>()); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type is not supported by the dd engine."); + } + return result; + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support data type."); + } + template typename std::enable_if::value, std::unique_ptr>::type verifyWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task) { STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::NotSupportedException, "Exploration engine is currently only applicable to PRISM models."); storm::prism::Program const& program = model.asPrismProgram(); STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently exploration-based verification is only available for DTMCs and MDPs."); - + std::unique_ptr result; if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { storm::modelchecker::SparseExplorationModelChecker> checker(program); @@ -80,7 +108,7 @@ namespace storm { } return result; } - + template typename std::enable_if::value, std::unique_ptr>::type verifyWithExplorationEngine(storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exploration engine does not support data type."); @@ -122,16 +150,16 @@ namespace storm { } return result; } - + template typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(std::shared_ptr> const&, storm::modelchecker::CheckTask const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify MDPs with this data type."); } - + template typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(std::shared_ptr> const& ma, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; - + // Close the MA, if it is not already closed. if (!ma->isClosed()) { STORM_LOG_WARN("Closing Markov automaton. Consider closing the MA before verification."); @@ -144,12 +172,12 @@ namespace storm { } return result; } - + template typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(std::shared_ptr> const& ma, storm::modelchecker::CheckTask const& task) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify MAs with this data type."); } - + template std::unique_ptr verifyWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -176,7 +204,7 @@ namespace storm { } return result; } - + template std::unique_ptr verifyWithHybridEngine(std::shared_ptr> const& ctmc, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -196,12 +224,12 @@ namespace storm { } return result; } - + template typename std::enable_if::value, std::unique_ptr>::type verifyWithHybridEngine(std::shared_ptr> const&, storm::modelchecker::CheckTask const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Hybrid engine cannot verify MDPs with this data type."); } - + template std::unique_ptr verifyWithHybridEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -216,7 +244,7 @@ namespace storm { } return result; } - + template std::unique_ptr verifyWithDdEngine(std::shared_ptr> const& dtmc, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -236,7 +264,7 @@ namespace storm { } return result; } - + template typename std::enable_if::value, std::unique_ptr>::type verifyWithDdEngine(std::shared_ptr> const&, storm::modelchecker::CheckTask const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Dd engine cannot verify MDPs with this data type."); diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp new file mode 100644 index 000000000..a1bb58c05 --- /dev/null +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp @@ -0,0 +1,19 @@ +#include "storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h" + +#include "storm/models/symbolic/Dtmc.h" +#include "storm/models/symbolic/Mdp.h" + +namespace storm { + namespace modelchecker { + + template + PartialBisimulationMdpModelChecker::PartialBisimulationMdpModelChecker(ModelType const& model) : model(model) { + + } + + template class PartialBisimulationMdpModelChecker>; + template class PartialBisimulationMdpModelChecker>; + template class PartialBisimulationMdpModelChecker>; + template class PartialBisimulationMdpModelChecker>; + } +} diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h new file mode 100644 index 000000000..5a745a3dd --- /dev/null +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h @@ -0,0 +1,29 @@ +#pragma once + +#include "storm/modelchecker/AbstractModelChecker.h" + +#include "storm/storage/dd/DdType.h" + +namespace storm { + namespace modelchecker { + + template + class PartialBisimulationMdpModelChecker : public AbstractModelChecker { + public: + typedef typename ModelType::ValueType ValueType; + + /*! + * Constructs a model checker for the given model. + */ + explicit PartialBisimulationMdpModelChecker(ModelType const& model); + +// /// Overridden methods from super class. +// virtual bool canHandle(CheckTask const& checkTask) const override; +// virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; +// virtual std::unique_ptr computeReachabilityProbabilities(CheckTask const& checkTask) override; + + private: + ModelType const& model; + }; + } +} diff --git a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp index c8d932b5c..b4b59e934 100644 --- a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp +++ b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp @@ -86,6 +86,7 @@ namespace storm { template class StochasticTwoPlayerGame; template class StochasticTwoPlayerGame; #ifdef STORM_HAVE_CARL + template class StochasticTwoPlayerGame; template class StochasticTwoPlayerGame; #endif diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index a4eb86fb7..7b307283e 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -12,6 +12,7 @@ namespace storm { namespace settings { namespace modules { + const std::string AbstractionSettings::methodOptionName = "method"; const std::string AbstractionSettings::moduleName = "abstraction"; const std::string AbstractionSettings::useDecompositionOptionName = "decomposition"; const std::string AbstractionSettings::splitModeOptionName = "split"; @@ -22,6 +23,12 @@ namespace storm { const std::string AbstractionSettings::reuseResultsOptionName = "reuse"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { + std::vector methods = {"games", "bisimulation", "bisim"}; + this->addOption(storm::settings::OptionBuilder(moduleName, methodOptionName, true, "Sets which abstraction-refinement method to use.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of themethod to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)) + .setDefaultValueString("bisim").build()) + .build()); + std::vector onOff = {"on", "off"}; this->addOption(storm::settings::OptionBuilder(moduleName, useDecompositionOptionName, true, "Sets whether to apply decomposition during the abstraction.") @@ -59,6 +66,16 @@ namespace storm { .build()); } + AbstractionSettings::Method AbstractionSettings::getAbstractionRefinementMethod() const { + std::string methodAsString = this->getOption(methodOptionName).getArgumentByName("method").getValueAsString(); + if (methodAsString == "games") { + return Method::Games; + } else if (methodAsString == "bisimulation" || methodAsString == "bism") { + return Method::Bisimulation; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown abstraction-refinement method '" << methodAsString << "'."); + } + bool AbstractionSettings::isUseDecompositionSet() const { return this->getOption(useDecompositionOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 9786f2957..4d5827187 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -11,6 +11,10 @@ namespace storm { */ class AbstractionSettings : public ModuleSettings { public: + enum class Method { + Games, Bisimulation + }; + enum class PivotSelectionHeuristic { NearestMaximalDeviation, MostProbablePath, MaxWeightedDeviation }; @@ -28,6 +32,11 @@ namespace storm { */ AbstractionSettings(); + /*! + * Retrieves the selected abstraction refinement method. + */ + Method getAbstractionRefinementMethod() const; + /*! * Retrieves whether the option to use the decomposition was set. * @@ -87,6 +96,7 @@ namespace storm { const static std::string moduleName; private: + const static std::string methodOptionName; const static std::string useDecompositionOptionName; const static std::string splitModeOptionName; const static std::string addAllGuardsOptionName; diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index b5cca9ec5..dbe2c5f26 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -140,6 +140,8 @@ namespace storm { QuotientExtractor extractor; quotient = extractor.extract(model, refiner->getStatePartition(), preservationInformation); } else { + STORM_LOG_THROW(model.getType() == storm::models::ModelType::Dtmc || model.getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidOperationException, "Can only extract partial quotient for discrete-time models."); + STORM_LOG_TRACE("Starting partial quotient extraction."); if (!partialQuotientExtractor) { partialQuotientExtractor = std::make_unique>(model); diff --git a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp index 124c1c077..bfff746b6 100644 --- a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp @@ -3,6 +3,7 @@ #include "storm/storage/dd/DdManager.h" #include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StochasticTwoPlayerGame.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/settings/SettingsManager.h" @@ -13,7 +14,7 @@ namespace storm { namespace dd { namespace bisimulation { - + template PartialQuotientExtractor::PartialQuotientExtractor(storm::models::symbolic::Model const& model) : model(model) { auto const& settings = storm::settings::getModule(); @@ -26,7 +27,7 @@ namespace storm { std::shared_ptr> PartialQuotientExtractor::extract(Partition const& partition, PreservationInformation const& preservationInformation) { auto start = std::chrono::high_resolution_clock::now(); std::shared_ptr> result; - + STORM_LOG_THROW(this->quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Dd, storm::exceptions::NotSupportedException, "Only DD-based partial quotient extraction is currently supported."); result = extractDdQuotient(partition, preservationInformation); auto end = std::chrono::high_resolution_clock::now(); @@ -41,7 +42,7 @@ namespace storm { std::shared_ptr> PartialQuotientExtractor::extractDdQuotient(Partition const& partition, PreservationInformation const& preservationInformation) { auto modelType = model.getType(); - if (modelType == storm::models::ModelType::Dtmc) { + if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Mdp) { // Sanity checks. STORM_LOG_ASSERT(partition.getNumberOfStates() == model.getNumberOfStates(), "Mismatching partition size."); STORM_LOG_ASSERT(partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()) == model.getReachableStates(), "Mismatching partition."); @@ -84,12 +85,6 @@ namespace storm { storm::dd::Add partitionAsAdd = partitionAsBdd.template toAdd(); storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables()); -// // Pick a representative from each block. -// auto representatives = InternalRepresentativeComputer(partitionAsBdd, model.getRowVariables()).getRepresentatives(); -// partitionAsBdd &= representatives; -// partitionAsAdd *= partitionAsBdd.template toAdd(); - -// quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()); quotientTransitionMatrix = quotientTransitionMatrix * partitionAsAdd; end = std::chrono::high_resolution_clock::now(); @@ -125,11 +120,13 @@ namespace storm { end = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); - std::set newNondeterminismVariables = model.getNondeterminismVariables(); - newNondeterminismVariables.insert(model.getRowVariables().begin(), model.getRowVariables().end()); - if (modelType == storm::models::ModelType::Dtmc) { - return std::shared_ptr>(new storm::models::symbolic::Mdp(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, newNondeterminismVariables, preservedLabelBdds, quotientRewardModels)); + return std::make_shared>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getRowVariables(), preservedLabelBdds, quotientRewardModels); + } else if (modelType == storm::models::ModelType::Mdp) { + std::set allNondeterminismVariables; + std::set_union(model.getRowVariables().begin(), model.getRowVariables().end(), model.getNondeterminismVariables().begin(), model.getNondeterminismVariables().end(), std::inserter(allNondeterminismVariables, allNondeterminismVariables.begin())); + + return std::make_shared>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getRowVariables(), model.getNondeterminismVariables(), allNondeterminismVariables, preservedLabelBdds, quotientRewardModels); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unsupported quotient type."); } @@ -140,7 +137,7 @@ namespace storm { template class PartialQuotientExtractor; template class PartialQuotientExtractor; - + #ifdef STORM_HAVE_CARL template class PartialQuotientExtractor; template class PartialQuotientExtractor; diff --git a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h index ca32a8dbf..26ae033e6 100644 --- a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h +++ b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h @@ -15,20 +15,20 @@ namespace storm { namespace dd { namespace bisimulation { - + template class PartialQuotientExtractor { - public: + public: PartialQuotientExtractor(storm::models::symbolic::Model const& model); std::shared_ptr> extract(Partition const& partition, PreservationInformation const& preservationInformation); - private: + private: std::shared_ptr> extractDdQuotient(Partition const& partition, PreservationInformation const& preservationInformation); // The model for which to compute the partial quotient. storm::models::symbolic::Model const& model; - + storm::settings::modules::BisimulationSettings::QuotientFormat quotientFormat; };