From 628219298e8e93edadb4e46818650f2b22ab160d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 5 Aug 2019 16:37:43 +0200 Subject: [PATCH] Some small cleanup in verification API --- src/storm/api/verification.h | 103 +++++++----------- .../storage/SymbolicModelDescription.cpp | 22 ++++ src/storm/storage/SymbolicModelDescription.h | 3 +- 3 files changed, 61 insertions(+), 67 deletions(-) diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index c22668610..3f5b9653c 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -39,7 +39,10 @@ namespace storm { storm::modelchecker::CheckTask createTask(std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { return storm::modelchecker::CheckTask(*formula, onlyInitialStatesRelevant); } - + + // + // Verifying with Abstraction Refinement engine + // struct AbstractionRefinementOptions { AbstractionRefinementOptions() = default; AbstractionRefinementOptions(std::vector&& constraints, std::vector>&& injectedRefinementPredicates) : constraints(std::move(constraints)), injectedRefinementPredicates(std::move(injectedRefinementPredicates)) { @@ -51,13 +54,10 @@ namespace storm { }; template - typename std::enable_if::value || std::is_same::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::Environment const& env, storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task, AbstractionRefinementOptions const& options = AbstractionRefinementOptions()) { - 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; - + typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::Environment const& env, storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task, AbstractionRefinementOptions const& options = AbstractionRefinementOptions()) { storm::modelchecker::GameBasedMdpModelCheckerOptions modelCheckerOptions(options.constraints, options.injectedRefinementPredicates); - + + std::unique_ptr result; if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC) { storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model, modelCheckerOptions); if (modelchecker.canHandle(task)) { @@ -69,29 +69,22 @@ namespace storm { result = modelchecker.check(env, task); } } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type is currently not supported."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model.getModelType() << " is not supported by the abstraction refinement engine."); } return result; } template - typename std::enable_if::value || std::is_same::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task, AbstractionRefinementOptions const& options = AbstractionRefinementOptions()) { - Environment env; - return verifyWithAbstractionRefinementEngine(env, model, task, options); - } - - template - typename std::enable_if::value && !std::is_same::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::Environment const& env, storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask const&, AbstractionRefinementOptions const& = AbstractionRefinementOptions()) { + typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::Environment const& env, storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask const&, AbstractionRefinementOptions const& = AbstractionRefinementOptions()) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support data type."); } template - typename std::enable_if::value && !std::is_same::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task, AbstractionRefinementOptions const& options = AbstractionRefinementOptions()) { + std::unique_ptr verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task, AbstractionRefinementOptions const& options = AbstractionRefinementOptions()) { Environment env; return verifyWithAbstractionRefinementEngine(env, model, task, options); } - template typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::Environment const& env, std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -106,53 +99,46 @@ namespace storm { result = modelchecker.check(env, task); } } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type is not supported by the dd engine."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported by the abstraction refinement engine."); } return result; } - template - typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { - Environment env; - return verifyWithAbstractionRefinementEngine(env, model, task); - } - template typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::Environment const&, std::shared_ptr> 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 verifyWithAbstractionRefinementEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { Environment env; return verifyWithAbstractionRefinementEngine(env, model, task); } + // + // Verifying with Exploration engine + // template typename std::enable_if::value, std::unique_ptr>::type verifyWithExplorationEngine(storm::Environment const& env, 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); if (checker.canHandle(task)) { result = checker.check(env, task); } - } else { + } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { storm::modelchecker::SparseExplorationModelChecker> checker(program); if (checker.canHandle(task)) { result = checker.check(env, task); } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << program.getModelType() << " is not supported by the exploration engine."); } - return result; - } - template - typename std::enable_if::value, std::unique_ptr>::type verifyWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task) { - Environment env; - return verifyWithExplorationEngine(env, model, task); + return result; } template @@ -161,11 +147,14 @@ namespace storm { } template - typename std::enable_if::value, std::unique_ptr>::type verifyWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task) { + std::unique_ptr verifyWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task) { Environment env; return verifyWithExplorationEngine(env, model, task); } + // + // Verifying with Sparse engine + // template std::unique_ptr verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr> const& dtmc, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -215,12 +204,6 @@ namespace storm { return result; } - template - typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { - Environment env; - return verifyWithSparseEngine(env, mdp, task); - } - template typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -232,7 +215,7 @@ namespace storm { } template - typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { + std::unique_ptr verifyWithSparseEngine(std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { Environment env; return verifyWithSparseEngine(env, mdp, task); } @@ -254,19 +237,13 @@ 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) { - Environment env; - return verifyWithSparseEngine(env, ma, task); - } - template typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(storm::Environment const&, std::shared_ptr> const& , storm::modelchecker::CheckTask const& ) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify MAs 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 verifyWithSparseEngine(std::shared_ptr> const& ma, storm::modelchecker::CheckTask const& task) { Environment env; return verifyWithSparseEngine(env, ma, task); } @@ -283,7 +260,7 @@ namespace storm { } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) { result = verifyWithSparseEngine(env, model->template as>(), task); } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported by the sparse engine."); } return result; } @@ -294,6 +271,9 @@ namespace storm { return verifyWithSparseEngine(env, model, task); } + // + // Verifying with Hybrid engine + // template std::unique_ptr verifyWithHybridEngine(storm::Environment const& env, std::shared_ptr> const& dtmc, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -336,19 +316,13 @@ namespace storm { return result; } - template - typename std::enable_if::value, std::unique_ptr>::type verifyWithHybridEngine(std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { - Environment env; - return verifyWithHybridEngine(env, mdp, task); - } - template typename std::enable_if::value, std::unique_ptr>::type verifyWithHybridEngine(storm::Environment const& , 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 - typename std::enable_if::value, std::unique_ptr>::type verifyWithHybridEngine(std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { + std::unique_ptr verifyWithHybridEngine(std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { Environment env; return verifyWithHybridEngine(env, mdp, task); } @@ -363,7 +337,7 @@ namespace storm { } else if (model->getType() == storm::models::ModelType::Mdp) { result = verifyWithHybridEngine(env, model->template as>(), task); } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type is not supported by the hybrid engine."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported by the hybrid engine."); } return result; } @@ -374,6 +348,9 @@ namespace storm { return verifyWithHybridEngine(env, model, task); } + // + // Verifying with DD engine + // template std::unique_ptr verifyWithDdEngine(storm::Environment const& env, std::shared_ptr> const& dtmc, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -400,19 +377,13 @@ namespace storm { return result; } - template - typename std::enable_if::value, std::unique_ptr>::type verifyWithDdEngine(std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { - Environment env; - return verifyWithDdEngine(env, mdp, task); - } - template typename std::enable_if::value, std::unique_ptr>::type verifyWithDdEngine(storm::Environment const&, std::shared_ptr> const&, storm::modelchecker::CheckTask const&) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Dd engine cannot verify MDPs with this data type."); } template - typename std::enable_if::value, std::unique_ptr>::type verifyWithDdEngine(std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { + std::unique_ptr verifyWithDdEngine(std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { Environment env; return verifyWithDdEngine(env, mdp, task); } @@ -425,7 +396,7 @@ namespace storm { } else if (model->getType() == storm::models::ModelType::Mdp) { result = verifyWithDdEngine(env, model->template as>(), task); } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type is not supported by the dd engine."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported by the dd engine."); } return result; } diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index 243cb8372..3e59f4090 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -209,5 +209,27 @@ namespace storm { } return out; } + + + std::ostream& operator<<(std::ostream& out, SymbolicModelDescription::ModelType const& type) { + switch (type) { + case SymbolicModelDescription::ModelType::DTMC: + out << "dtmc"; + break; + case SymbolicModelDescription::ModelType::CTMC: + out << "ctmc"; + break; + case SymbolicModelDescription::ModelType::MDP: + out << "mdp"; + break; + case SymbolicModelDescription::ModelType::MA: + out << "ma"; + break; + case SymbolicModelDescription::ModelType::POMDP: + out << "pomdp"; + break; + } + return out; + } } } diff --git a/src/storm/storage/SymbolicModelDescription.h b/src/storm/storage/SymbolicModelDescription.h index fb1f0e2ac..da07e10f8 100644 --- a/src/storm/storage/SymbolicModelDescription.h +++ b/src/storm/storage/SymbolicModelDescription.h @@ -64,6 +64,7 @@ namespace storm { }; std::ostream& operator<<(std::ostream& out, SymbolicModelDescription const& model); - + + std::ostream& operator<<(std::ostream& out, SymbolicModelDescription::ModelType const& type); } }