From 7dee6d3da281302a6309927a2fd79a23be3462af Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 14 Mar 2016 16:04:07 +0100
Subject: [PATCH] started on learning-based MDP model checking

Former-commit-id: 9a901e619b0f66553cc90abb41ef45bd0b5b8a7b
---
 SparseLearningModelChecker.cpp                |  0
 src/cli/entrypoints.h                         | 22 ++++++++++++++++++-
 .../reachability/SparseLearningModelChecker.h |  0
 3 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 SparseLearningModelChecker.cpp
 create mode 100644 src/modelchecker/reachability/SparseLearningModelChecker.h

diff --git a/SparseLearningModelChecker.cpp b/SparseLearningModelChecker.cpp
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index 359d58d13..a467825e9 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -56,7 +56,27 @@ namespace storm {
         
         template<typename ValueType>
         void verifySymbolicModelWithLearningEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented.");
+            
+            for (auto const& formula : formulas) {
+                STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidSettingsException, "Currently learning-based verification is only available for DTMCs and MDPs.");
+                std::cout << std::endl << "Model checking property: " << *formula << " ...";
+                storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant);
+                storm::modelchecker::SparseLearningModelChecker<ValueType> checker(program);
+                std::unique_ptr<storm::modelchecker::CheckResult> result;
+                if (checker.canHandle(formula)) {
+                    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(task);
+                } else {
+                    std::cout << " skipped, because the formula cannot be handled by the selected engine/method." << std::endl;
+                }
+                if (result) {
+                    std::cout << " done." << std::endl;
+                    std::cout << "Result (initial states): ";
+                    result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
+                    std::cout << *result << std::endl;
+                } else {
+                    std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+                }
+            }
         }
 
         template<storm::dd::DdType DdType>
diff --git a/src/modelchecker/reachability/SparseLearningModelChecker.h b/src/modelchecker/reachability/SparseLearningModelChecker.h
new file mode 100644
index 000000000..e69de29bb