From 3fcf4f83c056b3d7ddd764181804961c1d200198 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Fri, 14 Sep 2018 11:31:21 +0200
Subject: [PATCH] Clean up AssumptionMaker

---
 src/storm-pars-cli/storm-pars.cpp           |  3 ++-
 src/storm-pars/analysis/AssumptionMaker.cpp |  3 ++-
 src/storm-pars/analysis/AssumptionMaker.h   | 22 ++++++++++++++++++---
 3 files changed, 23 insertions(+), 5 deletions(-)

diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index ed8cc4a57..e2fec0e19 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -549,7 +549,8 @@ namespace storm {
                 auto assumptionChecker = storm::analysis::AssumptionChecker<ValueType>(formulas[0], dtmcModel, 3);
                 auto assumptionMaker = storm::analysis::AssumptionMaker<ValueType>(extender, &assumptionChecker, sparseModel->getNumberOfStates());
 
-                std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result = assumptionMaker.startMakingAssumptions(std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair));
+                std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result = assumptionMaker.makeAssumptions(
+                        std::get<0>(criticalPair), std::get<1>(criticalPair), std::get<2>(criticalPair));
 
 
                 latticeWatch.stop();
diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp
index db98a3498..711a069cd 100644
--- a/src/storm-pars/analysis/AssumptionMaker.cpp
+++ b/src/storm-pars/analysis/AssumptionMaker.cpp
@@ -19,7 +19,8 @@ namespace storm {
 
         template<typename ValueType>
         std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>
-                AssumptionMaker<ValueType>::startMakingAssumptions(storm::analysis::Lattice* lattice, uint_fast64_t critical1, uint_fast64_t critical2) {
+                AssumptionMaker<ValueType>::makeAssumptions(storm::analysis::Lattice *lattice, uint_fast64_t critical1,
+                                                            uint_fast64_t critical2) {
             std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
 
             std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> emptySet;
diff --git a/src/storm-pars/analysis/AssumptionMaker.h b/src/storm-pars/analysis/AssumptionMaker.h
index 49b50d3ea..a4d1a3478 100644
--- a/src/storm-pars/analysis/AssumptionMaker.h
+++ b/src/storm-pars/analysis/AssumptionMaker.h
@@ -5,10 +5,10 @@
 #ifndef STORM_ASSUMPTIONMAKER_H
 #define STORM_ASSUMPTIONMAKER_H
 
-#include "Lattice.h"
 #include "AssumptionChecker.h"
-#include "storm/storage/expressions/BinaryRelationExpression.h"
+#include "Lattice.h"
 #include "LatticeExtender.h"
+#include "storm/storage/expressions/BinaryRelationExpression.h"
 #include "storm-pars/utility/ModelInstantiator.h"
 
 
@@ -18,9 +18,25 @@ namespace storm {
         template<typename ValueType>
         class AssumptionMaker {
         public:
+            /*!
+             * Constructs AssumptionMaker based on the lattice extender, the assumption checker and number of states of the model.
+             *
+             * @param latticeExtender The LatticeExtender which needs the assumptions made by the AssumptionMaker.
+             * @param checker The AssumptionChecker which checks the assumptions at sample points.
+             * @param numberOfStates The number of states of the model.
+             */
             AssumptionMaker(storm::analysis::LatticeExtender<ValueType>* latticeExtender, storm::analysis::AssumptionChecker<ValueType>* checker, uint_fast64_t numberOfStates);
 
-            std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> startMakingAssumptions(storm::analysis::Lattice* lattice, uint_fast64_t critical1, uint_fast64_t critical2);
+            /*!
+             * Make the assumptions given a lattice and two states which could not be added to the lattice. Returns when no more assumptions can be made.
+             *
+             * @param lattice The lattice on which assumptions are needed to allow further extension.
+             * @param critical1 State number
+             * @param critical2 State number
+             * @return A mapping from pointers to different lattices and assumptions made to create the specific lattice.
+             */
+            std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> makeAssumptions(
+                    storm::analysis::Lattice *lattice, uint_fast64_t critical1, uint_fast64_t critical2);
 
         private:
             std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> runRecursive(storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);