From b415c12c25f81678a7d3c8c4bdf557c5f4dbfae7 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 19 Oct 2017 22:07:41 +0200 Subject: [PATCH] further preparation of partial bisimulation model checker --- src/storm-cli-utilities/model-handling.h | 16 +++++++-- src/storm/api/verification.h | 8 ++--- .../PartialBisimulationMdpModelChecker.cpp | 35 +++++++++++++++---- .../PartialBisimulationMdpModelChecker.h | 15 ++++---- .../settings/modules/AbstractionSettings.cpp | 4 +-- src/storm/utility/resources.h | 1 + 6 files changed, 54 insertions(+), 25 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 2842d653a..ef3102d46 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -30,6 +30,7 @@ #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/AbstractionSettings.h" #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/JaniExportSettings.h" @@ -209,7 +210,7 @@ namespace storm { std::shared_ptr result; if (input.model) { - if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { + if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { result = buildModelDd(input); } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) { result = buildModelSparse(input, ioSettings); @@ -554,7 +555,7 @@ namespace storm { 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 result = storm::api::verifyWithDdEngine(symbolicModel, storm::api::createTask(formula, true)); std::unique_ptr filter; if (filterForInitialStates) { @@ -569,6 +570,15 @@ namespace storm { }); } + template + void verifyWithAbstractionRefinementEngine(std::shared_ptr const& model, SymbolicInput const& input) { + verifyProperties(input.properties, [&model] (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."); + auto symbolicModel = model->as>(); + return storm::api::verifyWithAbstractionRefinementEngine(symbolicModel, storm::api::createTask(formula, true)); + }); + } + template typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) { storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine();; @@ -629,7 +639,7 @@ namespace storm { // 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 && abstractionSettings.getMethod() == storm::settings::modules::AbstractionSettings::Method::Games) { + if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement && abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) { verifyWithAbstractionRefinementEngine(input); } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) { verifyWithExplorationEngine(input); diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index 6b70c80bc..ab787123a 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -48,13 +48,13 @@ namespace storm { if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } - } else { + } else if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MDP) { storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type is currently not supported."); } return result; } @@ -68,12 +68,12 @@ namespace storm { 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>()); + storm::modelchecker::PartialBisimulationMdpModelChecker> modelchecker(*model->template as>()); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Mdp) { - storm::modelchecker::PartialBisimulationMdpModelChecker> modelchecker(model->as>()); + storm::modelchecker::PartialBisimulationMdpModelChecker> modelchecker(*model->template as>()); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp index a1bb58c05..d52065969 100644 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp @@ -3,17 +3,38 @@ #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Mdp.h" +#include "storm/modelchecker/results/CheckResult.h" + +#include "storm/logic/FragmentSpecification.h" + namespace storm { namespace modelchecker { - template - PartialBisimulationMdpModelChecker::PartialBisimulationMdpModelChecker(ModelType const& model) : model(model) { - + template + PartialBisimulationMdpModelChecker::PartialBisimulationMdpModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model) { + // Intentionally left empty. + } + + template + bool PartialBisimulationMdpModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); + storm::logic::FragmentSpecification fragment = storm::logic::reachability(); + return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet(); + } + + template + std::unique_ptr PartialBisimulationMdpModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + return nullptr; + } + + template + std::unique_ptr PartialBisimulationMdpModelChecker::computeReachabilityProbabilities(CheckTask const& checkTask) { + return nullptr; } - template class PartialBisimulationMdpModelChecker>; - template class PartialBisimulationMdpModelChecker>; - template class PartialBisimulationMdpModelChecker>; - template class PartialBisimulationMdpModelChecker>; + 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 index 5a745a3dd..de8bc9e22 100644 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h @@ -1,14 +1,14 @@ #pragma once -#include "storm/modelchecker/AbstractModelChecker.h" +#include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h" #include "storm/storage/dd/DdType.h" namespace storm { namespace modelchecker { - template - class PartialBisimulationMdpModelChecker : public AbstractModelChecker { + template + class PartialBisimulationMdpModelChecker : public SymbolicPropositionalModelChecker { public: typedef typename ModelType::ValueType ValueType; @@ -18,12 +18,9 @@ namespace storm { 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; + 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; }; } } diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 7b307283e..fb68a1a0e 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -67,10 +67,10 @@ namespace storm { } AbstractionSettings::Method AbstractionSettings::getAbstractionRefinementMethod() const { - std::string methodAsString = this->getOption(methodOptionName).getArgumentByName("method").getValueAsString(); + std::string methodAsString = this->getOption(methodOptionName).getArgumentByName("name").getValueAsString(); if (methodAsString == "games") { return Method::Games; - } else if (methodAsString == "bisimulation" || methodAsString == "bism") { + } else if (methodAsString == "bisimulation" || methodAsString == "bisim") { return Method::Bisimulation; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown abstraction-refinement method '" << methodAsString << "'."); diff --git a/src/storm/utility/resources.h b/src/storm/utility/resources.h index e843882ee..2858f6332 100644 --- a/src/storm/utility/resources.h +++ b/src/storm/utility/resources.h @@ -56,6 +56,7 @@ namespace storm { rl.rlim_cur = megabytes * 1024 * 1024; setrlimit(RLIMIT_AS, &rl); #else + (void)megabytes; STORM_LOG_WARN("Setting a memory limit is not supported for your operating system."); #endif }