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> 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 toLattice(std::vector> 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 extendLattice(storm::analysis::Lattice* lattice, std::set> assumptions); private: