Create AssumptionMaker

src/storm-pars-cli/storm-pars.cpp

@@ -1,6 +1,7 @@
 
 
 #include "storm-pars/analysis/LatticeExtender.h"
+#include "storm-pars/analysis/AssumptionMaker.h"
 #include "storm-cli-utilities/cli.h"
 #include "storm-cli-utilities/model-handling.h"
 
@@ -611,27 +612,16 @@ namespace storm {
 
                 // Transform to Lattice
                 storm::utility::Stopwatch latticeWatch(true);
-                storm::analysis::LatticeExtender<storm::models::sparse::Model<ValueType>> extender = storm::analysis::LatticeExtender<storm::models::sparse::Model<ValueType>>(sparseModel);
-                std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalPair = extender.toLattice(formulas);
+                storm::analysis::LatticeExtender<ValueType> *extender = new storm::analysis::LatticeExtender<ValueType>(sparseModel);
+                std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalPair = extender->toLattice(formulas);
 
-                // Declare variables for all states
-                std::shared_ptr<storm::expressions::ExpressionManager> expressionManager(new storm::expressions::ExpressionManager());
-                for (uint_fast64_t i = 0; i < sparseModel->getNumberOfStates(); ++i) {
-                    expressionManager->declareFreshIntegerVariable();
-                }
+                // TODO met assumptionmaker dingen doen
 
-                // Make assumptions
-                std::set<storm::expressions::BinaryRelationExpression*> assumptions;
-                while (std::get<1>(criticalPair) != sparseModel->getNumberOfStates()) {
-                    storm::expressions::Variable var1 = expressionManager->getVariable("_x" + std::to_string(std::get<1>(criticalPair)));
-                    storm::expressions::Variable var2 = expressionManager->getVariable("_x" + std::to_string(std::get<2>(criticalPair)));
-                    auto assumption = new storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(),
-                            var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
-                            storm::expressions::BinaryRelationExpression::RelationType::Greater);
-                    assumptions.insert(assumption);
-                    criticalPair = extender.extendLattice(std::get<0>(criticalPair), expressionManager, assumptions);
-                }
-                auto lattice = std::get<0>(criticalPair);
+
+                auto assumptionMaker = storm::analysis::AssumptionMaker<ValueType>(extender, 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));
+
+                auto lattice = result.begin()->first;
 
                 latticeWatch.stop();
                 STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);

src/storm-pars/analysis/AssumptionMaker.cpp

@@ -0,0 +1,97 @@
+//
+// Created by Jip Spel on 03.09.18.
+//
+
+#include "AssumptionMaker.h"
+
+namespace storm {
+    namespace analysis {
+        template<typename ValueType>
+        AssumptionMaker<ValueType>::AssumptionMaker(storm::analysis::LatticeExtender<ValueType>* latticeExtender, uint_fast64_t numberOfStates) {
+            this->latticeExtender = latticeExtender;
+            this->numberOfStates = numberOfStates;
+            this->expressionManager = std::make_shared<storm::expressions::ExpressionManager>(storm::expressions::ExpressionManager());
+            for (uint_fast64_t i = 0; i < this->numberOfStates; ++i) {
+                expressionManager->declareIntegerVariable(std::to_string(i));
+                expressionManager->declareFreshIntegerVariable();
+            }
+        }
+
+
+        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) {
+
+            std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
+
+            std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> emptySet;
+            if (critical1 == numberOfStates || critical2 == numberOfStates) {
+                result.insert(std::pair<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, emptySet));
+            } else {
+                storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(critical1));
+                storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2));
+                std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions1;
+                std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption1
+                    = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(),
+                        var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
+                        storm::expressions::BinaryRelationExpression::RelationType::Greater));
+                assumptions1.insert(assumption1);
+                auto lattice1 = new storm::analysis::Lattice(*lattice);
+                auto myMap = (runRecursive(lattice1, assumptions1));
+                result.insert(myMap.begin(), myMap.end());
+
+                std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions2;
+                std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption2
+                    = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(),
+                        var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(),
+                        storm::expressions::BinaryRelationExpression::RelationType::Greater));
+                assumptions2.insert(assumption2);
+
+                auto lattice2 = new storm::analysis::Lattice(*lattice);
+                auto myMap2 = (runRecursive(lattice2, assumptions2));
+                result.insert(myMap2.begin(), myMap2.end());
+            }
+            return result;
+        }
+
+        template<typename ValueType>
+        std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> AssumptionMaker<ValueType>::runRecursive(storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
+            std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
+            std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalPair = this->latticeExtender->extendLattice(lattice, assumptions);
+
+            if (std::get<1>(criticalPair) == numberOfStates) {
+                result.insert(std::pair<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, assumptions));
+            } else {
+                storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(std::get<1>(criticalPair)));
+                storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(std::get<2>(criticalPair)));
+
+                std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions1 = std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions);
+                std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption1 = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(),
+                                                                                    var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
+                                                                                    storm::expressions::BinaryRelationExpression::RelationType::Greater));
+                assumptions1.insert(assumption1);
+                auto lattice1 = new storm::analysis::Lattice(*lattice);
+                auto myMap = (runRecursive(lattice1, assumptions1));
+                result.insert(myMap.begin(), myMap.end());
+
+
+                std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>  assumptions2 = assumptions;
+                std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption2 = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(),
+                                                                                    var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(),
+                                                                                    storm::expressions::BinaryRelationExpression::RelationType::Greater))   ;
+                assumptions2.insert(assumption2);
+                auto lattice2 = new storm::analysis::Lattice(*lattice);
+                myMap = (runRecursive(lattice2, assumptions2));
+                result.insert(myMap.begin(), myMap.end());
+            }
+
+            return result;
+        }
+
+
+        template class AssumptionMaker<storm::RationalFunction>;
+    }
+}
+
+
+// Een map met daarin een pointer naar de lattic en een set met de geldende assumptions voor die lattice

src/storm-pars/analysis/AssumptionMaker.h

@@ -0,0 +1,34 @@
+//
+// Created by Jip Spel on 03.09.18.
+//
+
+#ifndef STORM_ASSUMPTIONMAKER_H
+#define STORM_ASSUMPTIONMAKER_H
+
+#include "Lattice.h"
+#include "storm/storage/expressions/BinaryRelationExpression.h"
+#include "LatticeExtender.h"
+
+namespace storm {
+    namespace analysis {
+
+        template<typename ValueType>
+        class AssumptionMaker {
+        public:
+            AssumptionMaker(storm::analysis::LatticeExtender<ValueType>* latticeExtender, 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);
+
+
+        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);
+
+            storm::analysis::LatticeExtender<ValueType>* latticeExtender;
+
+            std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
+
+            uint_fast64_t numberOfStates;
+        };
+    }
+}
+#endif //STORM_ASSUMPTIONMAKER_H

src/storm-pars/analysis/Lattice.cpp

@@ -76,11 +76,13 @@ namespace storm {
                     return SAME;
                 }
 
-                if (above(node1, node2)) {
+                std::set<Node*>* seen1 = new std::set<Node*>({});
+                if (above(node1, node2, seen1)) {
                     return ABOVE;
                 }
 
-                if (above(node2, node1)) {
+                std::set<Node*>* seen2 = new std::set<Node*>({});
+                if (above(node2, node1, seen2)) {
                     return BELOW;
                 }
             }
@@ -108,7 +110,7 @@ namespace storm {
             std::vector<Node*> printedNodes = std::vector<Node*>({});
             for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
 
-                if (std::find(printedNodes.begin(), printedNodes.end(), (*itr)) == printedNodes.end()) {
+                if ((*itr) != nullptr && std::find(printedNodes.begin(), printedNodes.end(), (*itr)) == printedNodes.end()) {
                     Node *node = *itr;
                     printedNodes.push_back(*itr);
                     out << "Node: {";
@@ -123,24 +125,23 @@ namespace storm {
                     out << "}" << "\n";
                     out << "  Address: " << node << "\n";
                     out << "    Above: {";
-                    for (auto itr2 = node->above.begin(); itr2 != node->above.end(); ++itr2) {
-                        Node *above = *itr2;
-                        out << "{";
-                        index = above->states.getNextSetIndex(0);
-                        while (index < numberOfStates) {
-                            out << index;
-                            index = above->states.getNextSetIndex(index + 1);
-                            if (index < numberOfStates) {
-                                out << ", ";
+
+                        for (auto itr2 = node->above.begin(); itr2 != node->above.end(); ++itr2) {
+                            Node *above = *itr2;
+                            index = above->states.getNextSetIndex(0);
+                            out << "{";
+                            while (index < numberOfStates) {
+                                out << index;
+                                index = above->states.getNextSetIndex(index + 1);
+                                if (index < numberOfStates) {
+                                    out << ", ";
+                                }
                             }
-                        }
 
-                        out << "}";
-                        if ((++itr2) != node->above.end()) {
-                            out << ", ";
+                            out << "}";
                         }
-                    }
-                    out << "}" << "\n";
+                        out << "}" << "\n";
+
 
                     out << "    Below: {";
                     for (auto itr2 = node->below.begin(); itr2 != node->below.end(); ++itr2) {
@@ -156,9 +157,6 @@ namespace storm {
                         }
 
                         out << "}";
-                        if ((++itr2) != node->below.end()) {
-                            out << ", ";
-                        }
                     }
                     out << "}" << "\n";
                 }
@@ -166,50 +164,53 @@ namespace storm {
         }
 
         void Lattice::toDotFile(std::ostream &out) {
-            out << "digraph \"Lattice\" {" << std::endl;
-
-            // print all nodes
-            std::vector<Node*> printed;
-            out << "\t" << "node [shape=ellipse]" << std::endl;
-            for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
-                if (find(printed.begin(), printed.end(), (*itr)) == printed.end()) {
-                    out << "\t\"" << (*itr) << "\" [label = \"";
-                    uint_fast64_t index = (*itr)->states.getNextSetIndex(0);
-                    while (index < numberOfStates) {
-                        out << index;
-                        index = (*itr)->states.getNextSetIndex(index + 1);
-                        if (index < numberOfStates) {
-                            out << ", ";
-                        }
+        out << "digraph \"Lattice\" {" << std::endl;
+
+        // print all nodes
+        std::vector<Node*> printed;
+        out << "\t" << "node [shape=ellipse]" << std::endl;
+        for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
+
+            if ((*itr) != nullptr && find(printed.begin(), printed.end(), (*itr)) == printed.end()) {
+                out << "\t\"" << (*itr) << "\" [label = \"";
+                uint_fast64_t index = (*itr)->states.getNextSetIndex(0);
+                while (index < numberOfStates) {
+                    out << index;
+                    index = (*itr)->states.getNextSetIndex(index + 1);
+                    if (index < numberOfStates) {
+                        out << ", ";
                     }
-
-                    out << "\"]" << std::endl;
-                    printed.push_back(*itr);
                 }
+
+                out << "\"]" << std::endl;
+                printed.push_back(*itr);
             }
+        }
 
-            // print arcs
-            printed.clear();
-            for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
-                if (find(printed.begin(), printed.end(), (*itr)) == printed.end()) {
-                    auto below = (*itr)->below;
-                    for (auto itr2 = below.begin(); itr2 != below.end(); ++itr2) {
-                        out << "\t\"" << (*itr) << "\" -> \"" << (*itr2) << "\";" << std::endl;
-                    }
-                    printed.push_back(*itr);
+        // print arcs
+        printed.clear();
+        for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
+            if ((*itr) != nullptr && find(printed.begin(), printed.end(), (*itr)) == printed.end()) {
+                auto below = (*itr)->below;
+                for (auto itr2 = below.begin(); itr2 != below.end(); ++itr2) {
+                    out << "\t\"" << (*itr) << "\" -> \"" << (*itr2) << "\";" << std::endl;
                 }
+                printed.push_back(*itr);
             }
-
-            out << "}" << std::endl;
         }
 
-        bool Lattice::above(Node *node1, Node *node2) {
-            bool result = !node1->below.empty() && std::find(node1->below.begin(), node1->below.end(), node2) != node1->below.end();
+        out << "}" << std::endl;
+    }
 
-            for (auto itr = node1->below.begin(); !result && node1->below.end() != itr; ++itr) {
-                result |= above(*itr, node2);
+    bool Lattice::above(Node *node1, Node *node2, std::set<Node *>* seenNodes) {
+        bool result = !node1->below.empty() && std::find(node1->below.begin(), node1->below.end(), node2) != node1->below.end();
+        for (auto itr = node1->below.begin(); !result && node1->below.end() != itr; ++itr) {
+            if (std::find(seenNodes->begin(), seenNodes->end(), (*itr)) == seenNodes->end()) {
+                seenNodes->insert(*itr);
+                result |= above(*itr, node2, seenNodes);
             }
-            return result;
         }
+        return result;
     }
 }
+}

src/storm-pars/analysis/Lattice.h

@@ -120,7 +120,14 @@ namespace storm {
 
                     uint_fast64_t numberOfStates;
 
-                    bool above(Node *, Node *);
+                    /**
+                     * Check if node1 lies above node2
+                     * @param node1
+                     * @param node2
+                     * @param seenNodes
+                     * @return
+                     */
+                    bool above(Node * node1, Node * node2, std::set<Node*>* seenNodes);
                 };
             }
 }

src/storm-pars/analysis/LatticeExtender.cpp

@@ -24,13 +24,13 @@
 namespace storm {
     namespace analysis {
 
-        template<typename SparseModelType>
-        LatticeExtender<SparseModelType>::LatticeExtender(std::shared_ptr<SparseModelType> model) : model(model) {
+        template<typename ValueType>
+        LatticeExtender<ValueType>::LatticeExtender(std::shared_ptr<storm::models::sparse::Model<ValueType>> model) : model(model) {
             // intentionally left empty
         }
 
-        template <typename SparseModelType>
-        std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<SparseModelType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas) {
+        template <typename ValueType>
+        std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas) {
             STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis");
             STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula()
                             && ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()
@@ -38,7 +38,7 @@ namespace storm {
 
             uint_fast64_t numberOfStates = this->model->getNumberOfStates();
 
-            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*model);
+            storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> propositionalChecker(*model);
             storm::storage::BitVector phiStates;
             storm::storage::BitVector psiStates;
             if ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()) {
@@ -76,15 +76,14 @@ namespace storm {
             return this->extendLattice(lattice);
         }
 
-        template <typename SparseModelType>
-        std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<SparseModelType>::extendLattice(storm::analysis::Lattice* lattice) {
-            std::shared_ptr<storm::expressions::ExpressionManager> expressionManager(new storm::expressions::ExpressionManager());
-            std::set<storm::expressions::BinaryRelationExpression*> assumptions;
-            return this->extendLattice(lattice, expressionManager, assumptions);
+        template <typename ValueType>
+        std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::extendLattice(storm::analysis::Lattice* lattice) {
+            std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
+            return this->extendLattice(lattice, assumptions);
         }
 
-        template <typename SparseModelType>
-        std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<SparseModelType>::extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::ExpressionManager> expressionManager, std::set<storm::expressions::BinaryRelationExpression*> assumptions) {
+        template <typename ValueType>
+        std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::extendLattice(storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
             auto numberOfStates = this->model->getNumberOfStates();
             // First handle assumptions
             for (auto itr = assumptions.begin(); itr != assumptions.end(); ++itr) {
@@ -93,20 +92,19 @@ namespace storm {
                 if (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()) {
                     storm::expressions::Variable largest = expr.getFirstOperand()->asVariableExpression().getVariable();
                     storm::expressions::Variable smallest = expr.getSecondOperand()->asVariableExpression().getVariable();
-
-                    if (lattice->compare(largest.getOffset(), smallest.getOffset()) != storm::analysis::Lattice::ABOVE) {
-                        storm::analysis::Lattice::Node* n1 = lattice->getNode(largest.getOffset());
-                        storm::analysis::Lattice::Node* n2 = lattice->getNode(smallest.getOffset());
+                    if (lattice->compare(std::stoul(largest.getName(), nullptr, 0), std::stoul(smallest.getName(), nullptr, 0)) != storm::analysis::Lattice::ABOVE) {
+                        storm::analysis::Lattice::Node* n1 = lattice->getNode(std::stoul(largest.getName(), nullptr, 0));
+                        storm::analysis::Lattice::Node* n2 = lattice->getNode(std::stoul(smallest.getName(), nullptr, 0));
 
                         if (n1 != nullptr && n2 != nullptr) {
                             lattice->addRelationNodes(n1, n2);
                         } else if (n1 != nullptr) {
-                            lattice->addBetween(smallest.getOffset(), n1, lattice->getBottom());
+                            lattice->addBetween(std::stoul(smallest.getName(), nullptr, 0), n1, lattice->getBottom());
                         } else if (n2 != nullptr) {
-                            lattice->addBetween(largest.getOffset(), lattice->getTop(), n2);
+                            lattice->addBetween(std::stoul(largest.getName(), nullptr, 0), lattice->getTop(), n2);
                         } else {
-                            lattice->add(largest.getOffset());
-                            lattice->addBetween(smallest.getOffset(), lattice->getNode(largest.getOffset()),
+                            lattice->add(std::stoul(largest.getName(), nullptr, 0));
+                            lattice->addBetween(std::stoul(smallest.getName(), nullptr, 0), lattice->getNode(std::stoul(largest.getName(), nullptr, 0)),
                                                 lattice->getBottom());
                         }
                     }
@@ -141,6 +139,7 @@ namespace storm {
                         // Otherwise, check how the two states compare, and add if the comparison is possible.
                         uint_fast64_t successor1 = successors.getNextSetIndex(0);
                         uint_fast64_t successor2 = successors.getNextSetIndex(successor1 + 1);
+
                         int compareResult = lattice->compare(successor1, successor2);
                         if (compareResult == storm::analysis::Lattice::ABOVE) {
                             // successor 1 is closer to top than successor 2
@@ -163,6 +162,6 @@ namespace storm {
             return std::make_tuple(lattice, numberOfStates, numberOfStates);
         }
 
-        template class LatticeExtender<storm::models::sparse::Model<storm::RationalFunction>>;
+        template class LatticeExtender<storm::RationalFunction>;
     }
 }

src/storm-pars/analysis/LatticeExtender.h

@@ -17,18 +17,18 @@ namespace storm {
     namespace analysis {
 
 
-        template<typename SparseModelType>
+        template<typename ValueType>
         class LatticeExtender {
 
         public:
-            LatticeExtender(std::shared_ptr<SparseModelType> model);
+            LatticeExtender(std::shared_ptr<storm::models::sparse::Model<ValueType>> model);
 
             std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas);
 
-            std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::ExpressionManager> expressionManager, std::set<storm::expressions::BinaryRelationExpression*> assumptions);
+            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:
-            std::shared_ptr<SparseModelType> model;
+            std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
 
             std::map<uint_fast64_t, storm::storage::BitVector> stateMap;