From f2c2da64fa37be4b9b246c173578f4ca2afd5038 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Fri, 14 Sep 2018 13:16:37 +0200
Subject: [PATCH] Add documentation LatticeExtender.h

---
 src/storm-pars/analysis/LatticeExtender.h | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h
index 72d91a8c1..38cc5429b 100644
--- a/src/storm-pars/analysis/LatticeExtender.h
+++ b/src/storm-pars/analysis/LatticeExtender.h
@@ -21,10 +21,32 @@ namespace storm {
         class LatticeExtender {
 
         public:
+            /*!
+             * Constructs LatticeExtender which can extend a lattice
+             *
+             * @param model The model for which the lattice should be extended.
+             */
             LatticeExtender(std::shared_ptr<storm::models::sparse::Model<ValueType>> model);
 
+            /*!
+             * Creates a lattice based on the given formula.
+             *
+             * @param formulas The formulas based on which the lattice is created, only the first is used.
+             * @return A triple with a pointer to the lattice and two states of which the current place in the lattice
+             *         is unknown but needed. When the states have as number the number of states, no states are
+             *         unplaced but needed.
+             */
             std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas);
 
+            /*!
+             * Extends the lattice based on the given assumptions.
+             *
+             * @param lattice The lattice.
+             * @param assumptions The assumptions on states.
+             * @return A triple with a pointer to the lattice and two states of which the current place in the lattice
+             *         is unknown but needed. When the states have as number the number of states, no states are
+             *         unplaced but needed.
+             */
             std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> extendLattice(storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);
 
         private: