From fba6fe76b5c334b5a879a8ee454ff92a06ffc415 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Fri, 14 Sep 2018 11:30:59 +0200
Subject: [PATCH] Clean up AssumptionChecker

---
 src/storm-pars/analysis/AssumptionChecker.cpp | 26 +++++--------------
 src/storm-pars/analysis/AssumptionChecker.h   | 22 ++++++++++------
 2 files changed, 21 insertions(+), 27 deletions(-)

diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp
index bba77fb37..5cc5e6ea9 100644
--- a/src/storm-pars/analysis/AssumptionChecker.cpp
+++ b/src/storm-pars/analysis/AssumptionChecker.cpp
@@ -1,26 +1,26 @@
 //
 // Created by Jip Spel on 12.09.18.
 //
+#include "AssumptionChecker.h"
 
 #include "storm-pars/utility/ModelInstantiator.h"
-#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+
+#include "storm/environment/Environment.h"
 #include "storm/exceptions/NotSupportedException.h"
-#include "AssumptionChecker.h"
 #include "storm/modelchecker/CheckTask.h"
-#include "storm/environment/Environment.h"
+#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
 #include "storm/modelchecker/results/CheckResult.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "storm/storage/expressions/SimpleValuation.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 
-
-
 namespace storm {
     namespace analysis {
         template <typename ValueType>
         AssumptionChecker<ValueType>::AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples) {
             this->formula = formula;
 
+            // Create sample points
             auto instantiator = storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<ValueType>, storm::models::sparse::Dtmc<double>>(*model.get());
             auto matrix = model->getTransitionMatrix();
             std::set<storm::RationalFunctionVariable> variables =  storm::models::sparse::getProbabilityParameters(*model);
@@ -51,19 +51,6 @@ namespace storm {
                 std::vector<double> values = quantitativeResult.getValueVector();
                 results.push_back(values);
             }
-//            this->numberOfStates = model->getNumberOfStates();
-//            this->initialStates = model->getInitialStates();
-        }
-
-        template <typename ValueType>
-        bool AssumptionChecker<ValueType>::checkOnSamples(uint_fast64_t val1, uint_fast64_t val2) {
-            bool result = true;
-            for (auto itr = results.begin(); result && itr != results.end(); ++itr) {
-                // TODO: als expressie
-                auto values = (*itr);
-                result &= (values[val1] >= values[val2]);
-            }
-            return result;
         }
 
         template <typename ValueType>
@@ -80,6 +67,7 @@ namespace storm {
                     auto index = std::stoi(par.getName());
                     valuation.setRationalValue(par, values[index]);
                 }
+                assert(assumption->hasBooleanType());
                 result &= assumption->evaluateAsBool(&valuation);
             }
             return result;
@@ -87,4 +75,4 @@ namespace storm {
 
         template class AssumptionChecker<storm::RationalFunction>;
     }
-}
\ No newline at end of file
+}
diff --git a/src/storm-pars/analysis/AssumptionChecker.h b/src/storm-pars/analysis/AssumptionChecker.h
index 78e209ab2..2f0f8313a 100644
--- a/src/storm-pars/analysis/AssumptionChecker.h
+++ b/src/storm-pars/analysis/AssumptionChecker.h
@@ -10,29 +10,35 @@
 #include "storm/environment/Environment.h"
 #include "storm/storage/expressions/BinaryRelationExpression.h"
 
-
 namespace storm {
     namespace analysis {
         template<typename ValueType>
         class AssumptionChecker {
         public:
+            /*!
+             * Constructs an AssumptionChecker based on the number of samples, for the given formula and model.
+             *
+             * @param formula The formula to check.
+             * @param model The model to check the formula on.
+             * @param numberOfSamples Number of sample points.
+             */
             AssumptionChecker(std::shared_ptr<storm::logic::Formula const> formula, std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples);
 
-            bool checkOnSamples(uint_fast64_t val1, uint_fast64_t val2);
+            /*!
+             * Checks if the assumption holds at the sample points of the AssumptionChecker.
+             *
+             * @param assumption The assumption to check.
+             * @return true if the assumption holds at the sample points
+             */
             bool checkOnSamples(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
+
         private:
             std::shared_ptr<storm::logic::Formula const> formula;
 
-//            std::vector<storm::models::sparse::Dtmc<double>> sampleModels;
-
             std::vector<std::vector<double>> results;
 
-//            uint_fast64_t numberOfStates;
-//
-//            storm::storage::BitVector initialStates;
         };
     }
 }
 
-
 #endif //STORM_ASSUMPTIONCHECKER_H