Change output, Fix some small bugs

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

@@ -514,6 +514,11 @@ namespace storm {
                 std::cout << "Hello, Jip1" << std::endl;
                 // Simplify the model
                 storm::utility::Stopwatch simplifyingWatch(true);
+                std::ofstream outfile;
+                outfile.open("results.txt", std::ios_base::app);
+                outfile << ioSettings.getPrismInputFilename() << ", ";
+
+
                 if (model->isOfType(storm::models::ModelType::Dtmc)) {
                     auto consideredModel = (model->as<storm::models::sparse::Dtmc<ValueType>>());
                     auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<ValueType>>(*consideredModel);
@@ -543,6 +548,9 @@ namespace storm {
                 simplifyingWatch.stop();
                 STORM_PRINT(std::endl << "Time for model simplification: " << simplifyingWatch << "." << std::endl << std::endl);
                 model->printModelInformationToStream(std::cout);
+                outfile << simplifyingWatch << ", ";
+                outfile.close();
+
                 std::cout << "Bye, Jip1" << std::endl;
             }
 
@@ -562,8 +570,6 @@ namespace storm {
                 // Monotonicity
                 std::ofstream outfile;
                 outfile.open("results.txt", std::ios_base::app);
-                outfile << std::endl << ioSettings.getPrismInputFilename() << "; ";
-                outfile.close();
                 storm::utility::Stopwatch monotonicityWatch(true);
                 auto monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>(model, formulas, parSettings.isValidateAssumptionsSet());
                 monotonicityChecker.checkMonotonicity();
@@ -571,7 +577,10 @@ namespace storm {
                 STORM_PRINT(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl
                                     << std::endl);
 
+                outfile << monotonicityWatch << std::endl;
+                outfile.close();
                 std::cout << "Bye, Jip2" << std::endl;
+
                 return;
             }
 

src/storm-pars/analysis/AssumptionChecker.cpp

@@ -34,7 +34,8 @@ namespace storm {
                 auto valuation = storm::utility::parametric::Valuation<ValueType>();
                 for (auto itr = variables.begin(); itr != variables.end(); ++itr) {
                     // TODO: Type
-                    auto val = std::pair<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient>((*itr), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(boost::lexical_cast<std::string>((i+1)/(double (numberOfSamples + 1)))));
+                    // Creates samples between 0 and 1, 1/(#samples+2), 2/(#samples+2), ..., (#samples+1)/(#samples+2)
+                    auto val = std::pair<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient>((*itr), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(boost::lexical_cast<std::string>((i+1)/(double (numberOfSamples + 2)))));
                     valuation.insert(val);
                 }
                 storm::models::sparse::Dtmc<double> sampleModel = instantiator.instantiate(valuation);
@@ -127,10 +128,12 @@ namespace storm {
                 assumption->gatherVariables(vars);
 
                 STORM_LOG_THROW(assumption->getRelationType() ==
-                                storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual,
+                                storm::expressions::BinaryRelationExpression::RelationType::Greater ||assumption->getRelationType() ==
+                                                                                                             storm::expressions::BinaryRelationExpression::RelationType::Equal,
                                 storm::exceptions::NotSupportedException,
                                 "Only Greater Or Equal assumptions supported");
 
+                // TODO: implement validation of equal/greater equations
                 auto row1 = matrix.getRow(std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName()));
                 auto row2 = matrix.getRow(std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName()));
 
@@ -239,7 +242,9 @@ namespace storm {
                     result = false;
                 }
             }
-            return result && prob.evaluate(substitutions) >= 0;
+//            return result && prob.evaluate(substitutions) >= 0;
+//TODO check for > and =
+            return false;
         }
 
         template <typename ValueType>
@@ -296,7 +301,9 @@ namespace storm {
             s.add(exprBounds);
             smtResult = s.check();
 
-            return smtResult == storm::solver::SmtSolver::CheckResult::Sat;
+//            return smtResult == storm::solver::SmtSolver::CheckResult::Sat;
+//TODO check for > and =
+            return false;
         }
 
         template <typename ValueType>
@@ -387,8 +394,9 @@ namespace storm {
             assert(s.check() == storm::solver::SmtSolver::CheckResult::Sat);
             s.add(exprToCheck);
             auto smtRes = s.check();
+            //TODO check for > and =
             result = result &&  smtRes == storm::solver::SmtSolver::CheckResult::Sat;
-            return result;
+            return false;
         }
 
         template <typename ValueType>

src/storm-pars/analysis/AssumptionMaker.cpp

@@ -27,17 +27,24 @@ namespace storm {
             std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption1
                     = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
                                                                                                                                   var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
-                                                                                                                                  storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual));
+                                                                                                                              storm::expressions::BinaryRelationExpression::RelationType::Greater));
             bool result1 = (validate && assumptionChecker->validateAssumption(assumption1, lattice) && assumptionChecker->valid(assumption1));
             result[assumption1] = result1;
 
             std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption2
                     = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
                                                                                                                                   var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(),
-                                                                                                                                  storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual));
+                                                                                                                                  storm::expressions::BinaryRelationExpression::RelationType::Greater));
             bool result2 = (validate && assumptionChecker->validateAssumption(assumption2, lattice) && assumptionChecker->valid(assumption2));
             result[assumption2] = result2;
 
+            std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption3
+                    = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
+                                                                                                                                  var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(),
+                                                                                                                                  storm::expressions::BinaryRelationExpression::RelationType::Equal));
+            bool result3 = (validate && assumptionChecker->validateAssumption(assumption3, lattice) && assumptionChecker->valid(assumption3));
+            result[assumption3] = result3;
+
             return result;
         }
 

src/storm-pars/analysis/Lattice.cpp

@@ -112,11 +112,11 @@ namespace storm {
             }
 
             addedStates.set(state);
+
         }
 
         void Lattice::addToNode(uint_fast64_t state, Node *node) {
             assert(!addedStates[state]);
-
             node->states.set(state);
             nodes.at(state) = node;
             addedStates.set(state);
@@ -131,12 +131,13 @@ namespace storm {
         }
 
         void Lattice::add(uint_fast64_t state) {
+            assert(!addedStates[state]);
             addBetween(state, top, bottom);
         }
 
         void Lattice::addRelationNodes(Lattice::Node *above, Lattice::Node * below) {
             assert (compare(above, below) == UNKNOWN);
-
+            assert ((above->statesAbove & below->statesBelow).getNumberOfSetBits() == 0);
             setStatesBelow(above, below->states | below->statesBelow, true);
             setStatesAbove(below, above->states | above->statesAbove, true);
 
@@ -147,6 +148,7 @@ namespace storm {
             for (auto i = above->statesAbove.getNextSetIndex(0); i < above->statesAbove.size(); i = above->statesAbove.getNextSetIndex(i + 1)) {
                 setStatesBelow(getNode(i), below->states | below->statesBelow, true);
             }
+
         }
 
         int Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) {
@@ -314,16 +316,17 @@ namespace storm {
         }
 
         bool Lattice::above(Node *node1, Node *node2) {
-            return node1->statesBelow.get(node2->states.getNextSetIndex(0));
+            return node1->statesBelow[node2->states.getNextSetIndex(0)];
         }
 
         void Lattice::setStatesAbove(Lattice::Node *node, uint_fast64_t state, bool alreadyInitialized) {
-            assert (!node->states.get(state));
+            assert (!node->states[state]);
 
             if (!alreadyInitialized) {
                 node->statesAbove = storm::storage::BitVector(numberOfStates);
             }
 
+            assert (!node->statesBelow[state]);
             node->statesAbove.set(state);
         }
 
@@ -333,32 +336,60 @@ namespace storm {
             if (!alreadyInitialized) {
                 node->statesBelow = storm::storage::BitVector(numberOfStates);
             }
-
+            assert (!node->statesAbove[state]);
             node->statesBelow.set(state);
         }
 
         void Lattice::setStatesAbove(Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized) {
             assert((states.getNumberOfSetBits() - (node->states & states).getNumberOfSetBits()) != 0);
+            // the states to add to the above state of the current node shouldnt occur in either statesbelow or states of ndoe
 
-            auto complement = storm::storage::BitVector(node->states);
-            complement.complement();
+            assert ((node->states & states).getNumberOfSetBits() ==0);
             if (alreadyInitialized) {
-                node->statesAbove |= (states & complement);
+                assert ((node->statesBelow & states).getNumberOfSetBits() == 0);
+
+                node->statesAbove |= (states);
             } else {
-                node->statesAbove = (storm::storage::BitVector(states) & complement);
+                node->statesAbove = (storm::storage::BitVector(states));
             }
         }
 
         void Lattice::setStatesBelow(Lattice::Node *node, storm::storage::BitVector states, bool alreadyInitialized) {
             assert((states.getNumberOfSetBits() - (node->states & states).getNumberOfSetBits()) != 0);
 
-            auto complement = storm::storage::BitVector(node->states);
-            complement.complement();
+            assert ((node->states & states).getNumberOfSetBits() ==0);
             if (alreadyInitialized) {
-                node->statesBelow |= (states & complement);
+                assert ((node->statesAbove & states).getNumberOfSetBits() == 0);
+                node->statesBelow |= (states);
             } else {
-                node->statesBelow = (storm::storage::BitVector(states) & complement);
+                node->statesBelow = (storm::storage::BitVector(states));
+            }
         }
+
+        void Lattice::mergeNodes(storm::analysis::Lattice::Node *node1, storm::analysis::Lattice::Node *node2) {
+            // Merges node2 into node 1
+            // everything above n2 also above n1
+            node1->statesAbove |= node2->statesAbove;
+            // everything below node 2 also below node 1
+            node1->statesBelow |= node2->statesBelow;
+
+            // add states of node 2 to node 1
+            node1->states|= node2->states;
+            for(auto i = node2->states.getNextSetIndex(0); i < node2->states.size(); i = node2->states.getNextSetIndex(i+1)) {
+                nodes.at(i) = node1;
+            }
+
+            // TODO hier gaat het op magische wijze nog fout
+            // Add all states of combined node to states Above of all states Below of node1
+            for (auto i = node1->statesBelow.getNextSetIndex(0); i < node1->statesBelow.size(); i= node1->statesBelow.getNextSetIndex(i+1)) {
+                getNode(i)->statesAbove |= node1->states | node1->statesAbove;
+            }
+
+            // Add all states of combined node to states Below of all states Above of node1
+            for (auto i = node1->statesAbove.getNextSetIndex(0); i < node1->statesAbove.size(); i= node1->statesAbove.getNextSetIndex(i+1)) {
+                getNode(i)->statesBelow |= node1->states | node1->statesBelow;
+            }
+
         }
     }
 }

src/storm-pars/analysis/Lattice.h

@@ -165,6 +165,13 @@ namespace storm {
                      */
                     void toDotFile(std::ostream &out);
 
+                    /*!
+                     * Merges node2 into node1
+                     * @param node1
+                     * @param node2
+                     */
+                    void mergeNodes(Node* node1, Node* node2);
+
                     /*!
                      * Constants for comparison of nodes/states
                      */

src/storm-pars/analysis/LatticeExtender.cpp

@@ -4,6 +4,7 @@
 
 #include "LatticeExtender.h"
 #include "storm/utility/macros.h"
+#include "storm/utility/graph.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/utility/graph.h"
 #include <storm/logic/Formula.h>
@@ -35,7 +36,7 @@ namespace storm {
 
         template <typename ValueType>
         std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas) {
-            storm::utility::Stopwatch latticeWatch(true);
+//            storm::utility::Stopwatch latticeWatch(true);
 
             STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis");
             STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula()
@@ -66,6 +67,16 @@ namespace storm {
             // Transform to Lattice
             auto matrix = this->model->getTransitionMatrix();
 
+            auto initialMiddleStates = storm::storage::BitVector(numberOfStates);
+            // Check if MC contains cycles
+            auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(model->getTransitionMatrix(), false, false);
+            acyclic = true;
+            for (auto i = 0; acyclic && i < decomposition.size(); ++i) {
+                acyclic &= decomposition.getBlock(i).size() <= 1;
+            }
+            if (acyclic) {
+                states = storm::utility::graph::getTopologicalSort(matrix);
+            } else {
                 for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
                     stateMap[i] = storm::storage::BitVector(numberOfStates, false);
 
@@ -77,10 +88,6 @@ namespace storm {
                         }
                     }
                 }
-
-            auto initialMiddleStates = storm::storage::BitVector(numberOfStates);
-            // Check if MC contains cycles
-            auto decomposition = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(model->getTransitionMatrix(), false, false);
                 for (auto i = 0; i < decomposition.size(); ++i) {
                     auto scc = decomposition.getBlock(i);
                     if (scc.size() > 1) {
@@ -101,12 +108,13 @@ namespace storm {
                         }
                     }
                 }
+            }
 
             // Create the Lattice
             Lattice *lattice = new Lattice(topStates, bottomStates, initialMiddleStates, numberOfStates);
 
-            latticeWatch.stop();
-            STORM_PRINT(std::endl << "Time for initialization of lattice: " << latticeWatch << "." << std::endl << std::endl);
+//            latticeWatch.stop();
+//            STORM_PRINT(std::endl << "Time for initialization of lattice: " << latticeWatch << "." << std::endl << std::endl);
             return this->extendLattice(lattice);
         }
 
@@ -115,7 +123,7 @@ namespace storm {
             assert (assumption != nullptr);
 
             storm::expressions::BinaryRelationExpression expr = *assumption;
-            assert (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual
+            assert (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater
                 || expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal);
 
             if (expr.getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) {
@@ -131,8 +139,7 @@ namespace storm {
                 Lattice::Node *n2 = lattice->getNode(val2);
 
                 if (n1 != nullptr && n2 != nullptr) {
-                    // TODO: mergeNode method
-                    assert(false);
+                    lattice->mergeNodes(n1,n2);
                 } else if (n1 != nullptr) {
                     lattice->addToNode(val2, n1);
                 } else if (n2 != nullptr) {
@@ -219,6 +226,8 @@ namespace storm {
             return std::make_tuple(lattice, numberOfStates, numberOfStates);
         }
 
+
+
         template <typename ValueType>
         std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::extendLattice(Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
             auto numberOfStates = this->model->getNumberOfStates();
@@ -230,17 +239,52 @@ namespace storm {
             auto oldNumberSet = numberOfStates;
             while (oldNumberSet != lattice->getAddedStates().getNumberOfSetBits()) {
                 oldNumberSet = lattice->getAddedStates().getNumberOfSetBits();
+
+                if (acyclic && states.size() > 0) {
+                    auto nextState = *(states.begin());
+                    while (lattice->getAddedStates().get(nextState) && states.size() > 0) {
+                        states.erase(states.begin());
+
+                        nextState = *(states.begin());
+                    }
+
+                    if (! lattice->getAddedStates().get(nextState)) {
+                        auto row = this->model->getTransitionMatrix().getRow(nextState);
+                        auto successors = storm::storage::BitVector(lattice->getAddedStates().size());
+                        for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) {
+                            // ignore self-loops when there are more transitions
+                            if (nextState != rowItr->getColumn()) {
+                                successors.set(rowItr->getColumn());
+                            }
+                        }
+                        auto seenStates = (lattice->getAddedStates());
+                        assert ((seenStates & successors) == successors);
+
+                        auto result = extendAllSuccAdded(lattice, nextState, successors);
+                        if (std::get<1>(result) != successors.size()) {
+                            return result;
+                        } else {
+                            states.erase(states.begin());
+                        }
+                    }
+                    assert (lattice->getNode(nextState) != nullptr);
+
+                } else if (!acyclic) {
                     // TODO: kan dit niet efficienter
-                for (auto stateItr = stateMap.begin(); stateItr != stateMap.end(); ++stateItr) {
+                    auto addedStates = lattice->getAddedStates();
+                    for (auto stateNumber = addedStates.getNextUnsetIndex(0); stateNumber < addedStates.size(); stateNumber = addedStates.getNextUnsetIndex(stateNumber+1)) {
                         // Iterate over all states
-                    auto stateNumber = stateItr->first;
-                    storm::storage::BitVector successors = stateItr->second;
+//                        auto stateNumber = i;
+                        storm::storage::BitVector successors = stateMap[stateNumber];
 
                         auto seenStates = (lattice->getAddedStates());
 
+                        assert(!acyclic);
                         // Check if current state has not been added yet, and all successors have
                         bool check = !seenStates[stateNumber];
-                    for (auto succIndex = successors.getNextSetIndex(0); check && succIndex != successors.size(); succIndex = successors.getNextSetIndex(++succIndex)) {
+                        for (auto succIndex = successors.getNextSetIndex(0);
+                             check && succIndex != successors.size(); succIndex = successors.getNextSetIndex(
+                                ++succIndex)) {
                             // if the stateNumber equals succIndex we have a self-loop, ignoring selfloop as seenStates[stateNumber] = false
                             if (succIndex != stateNumber) {
                                 check &= seenStates[succIndex];
@@ -264,6 +308,7 @@ namespace storm {
 
                             if (!seenStates[succ1]) {
                                 std::swap(succ1, succ2);
+                                std::swap(succ1, succ2);
                             }
 
                             auto compare = lattice->compare(stateNumber, succ1);
@@ -278,9 +323,9 @@ namespace storm {
                         }
                     }
                 }
+            }
             return std::make_tuple(lattice, numberOfStates, numberOfStates);
         }
-
         template class LatticeExtender<storm::RationalFunction>;
     }
 }

src/storm-pars/analysis/LatticeExtender.h

@@ -29,31 +29,35 @@ namespace storm {
             LatticeExtender(std::shared_ptr<storm::models::sparse::Model<ValueType>> model);
 
             /*!
-             * Creates a lattice based on the given formula.
+             * Extends the lattice based on the given assumption.
              *
-             * @param formulas The formulas based on which the lattice is created, only the first is used.
+             * @param lattice The lattice.
+             * @param assumption The assumption 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> 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::BinaryRelationExpression> assumption = nullptr);
 
             /*!
-             * Extends the lattice based on the given assumption.
+             * Creates a lattice based on the given formula.
              *
-             * @param lattice The lattice.
-             * @param assumption The assumption on states.
+             * @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> extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption = nullptr);
+            std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas);
 
         private:
             std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
 
             std::map<uint_fast64_t, storm::storage::BitVector> stateMap;
 
+            std::vector<uint_fast64_t> states;
+
+            bool acyclic;
+
             void handleAssumption(Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
 
             std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> extendAllSuccAdded(Lattice* lattice, uint_fast64_t stateNumber, storm::storage::BitVector successors);

src/storm-pars/analysis/MonotonicityChecker.cpp

@@ -27,8 +27,6 @@
 
 #include "storm/storage/expressions/RationalFunctionToExpression.h"
 
-
-
 namespace storm {
     namespace analysis {
         template <typename ValueType>
@@ -41,7 +39,7 @@ namespace storm {
             if (model != nullptr) {
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
                 this->extender = new storm::analysis::LatticeExtender<ValueType>(sparseModel);
-                outfile << model->getNumberOfStates() << "; " << model->getNumberOfTransitions() << "; ";
+                outfile << model->getNumberOfStates() << ", " << model->getNumberOfTransitions() << ", ";
             }
             outfile.close();
             totalWatch = storm::utility::Stopwatch(true);
@@ -49,9 +47,11 @@ namespace storm {
 
         template <typename ValueType>
         std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity() {
-            totalWatch = storm::utility::Stopwatch(true);
             // TODO: check on samples or not?
+            totalWatch = storm::utility::Stopwatch(true);
+            auto latticeWatch = storm::utility::Stopwatch(true);
             auto map = createLattice();
+            // STORM_PRINT(std::endl << "Time for creating lattice: " << latticeWatch << "." << std::endl << std::endl);
             std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
             auto matrix = sparseModel->getTransitionMatrix();
             return checkMonotonicity(map, matrix);
@@ -101,10 +101,21 @@ namespace storm {
                     bool assumptionsHold = true;
                     for (auto itr = assumptions.begin(); assumptionsHold && itr != assumptions.end(); ++itr) {
                         auto assumption = *itr;
-                        assert (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual);
-                        auto state1 = std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName());
-                        auto state2 = std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName());
+                        if (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Greater) {
+                            auto state1 = std::stoi(
+                                    assumption->getFirstOperand()->asVariableExpression().getVariableName());
+                            auto state2 = std::stoi(
+                                    assumption->getSecondOperand()->asVariableExpression().getVariableName());
                             assumptionsHold &= valuesLower[state1] >= valuesUpper[state2];
+                        } else if (assumption->getRelationType() == storm::expressions::BinaryRelationExpression::RelationType::Equal) {
+                            auto state1 = std::stoi(
+                                    assumption->getFirstOperand()->asVariableExpression().getVariableName());
+                            auto state2 = std::stoi(
+                                    assumption->getSecondOperand()->asVariableExpression().getVariableName());
+                            assumptionsHold &= valuesLower[state1] == valuesUpper[state2];
+                        } else {
+                            assert(false);
+                        }
                     }
                     if (!assumptionsHold) {
                         std::vector<storm::storage::ParameterRegion<ValueType>> newRegions;
@@ -126,55 +137,67 @@ namespace storm {
 
         template <typename ValueType>
         std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
-            storm::utility::Stopwatch finalCheckWatch(true);
+            storm::utility::Stopwatch monotonicityCheckWatch(true);
             std::map<storm::analysis::Lattice *, std::map<carl::Variable, std::pair<bool, bool>>> result;
 
+            outfile.open(filename, std::ios_base::app);
 
             if (map.size() == 0) {
-                outfile.open(filename, std::ios_base::app);
-                outfile << " | No assumptions, ? | ;";
-                outfile.close();
-                STORM_PRINT(std::endl << "Do not know about monotonicity" << std::endl);
+                // Nothing is known
+                outfile << " No assumptions; ?";
+                // STORM_PRINT(std::endl << "Do not know about monotonicity" << std::endl);
             } else {
                 auto i = 0;
                 for (auto itr = map.begin(); i < map.size() && itr != map.end(); ++itr) {
                     auto lattice = itr->first;
-                    outfile.open(filename, std::ios_base::app);
-                    outfile << "|";
-                    outfile.close();
+                    if (itr != map.begin()) {
+                        outfile << ";";
+                    }
                     std::map<carl::Variable, std::pair<bool, bool>> varsMonotone = analyseMonotonicity(i, lattice,
                                                                                                       matrix);
 
-                    outfile.open(filename, std::ios_base::app);
                     auto assumptions = itr->second;
                     bool validSomewhere = true;
                     if (assumptions.size() > 0) {
-                        auto regions = checkAssumptionsOnRegion(assumptions);
-                        if (regions.size() > 0) {
-                            STORM_PRINT("For regions: " << std::endl);
-                        }
+//                        auto regions = checkAssumptionsOnRegion(assumptions);
+//                        if (regions.size() > 0) {
+//                            // STORM_PRINT("For regions: " << std::endl);
+//                            bool first = true;
+//                            for (auto itr2 = regions.begin(); itr2 != regions.end(); ++itr2) {
+//                                if (first) {
+//                                    // STORM_PRINT("    ");
+//                                    first = false;
+//                                }
+//                                // STORM_PRINT(*itr2);
+//                                outfile << (*itr2);
+//                            }
+//                            // STORM_PRINT(std::endl);
+//                            outfile << ", ";
+//                        } else {
+                            // STORM_PRINT("Assumption(s): ");
                             bool first = true;
-                        for (auto itr2 = regions.begin(); itr2 != regions.end(); ++itr2) {
-                            if (first) {
-                                STORM_PRINT("    ");
+                            for (auto itr2 = assumptions.begin(); itr2 != assumptions.end(); ++itr2) {
+                                if (!first) {
+                                    // STORM_PRINT(" ^ ");
+                                    outfile << (" ^ ");
+                                } else {
                                     first = false;
                                 }
-                            STORM_PRINT(*itr2);
-                            outfile << (*itr2);
-                        }
-                        if (regions.size() > 0) {
-                            STORM_PRINT(std::endl);
-                            outfile << ", ";
+                                // STORM_PRINT(*(*itr2));
+                                outfile << (*(*itr2));
                             }
+                            // STORM_PRINT(std::endl);
+                            outfile << " - ";
+//                        }
                     }
 
                     if (validSomewhere && assumptions.size() == 0) {
-                        outfile << "No assumptions, ";
+                        outfile << "No assumptions - ";
                     }
 
 
                     if (validSomewhere && varsMonotone.size() == 0) {
-                        STORM_PRINT("Result is constant" << std::endl);
+                        // STORM_PRINT("Result is constant" << std::endl);
                         outfile << "No params";
                     } else if (validSomewhere) {
                         auto itr2 = varsMonotone.begin();
@@ -182,45 +205,41 @@ namespace storm {
                             if (resultCheckOnSamples.find(itr2->first) != resultCheckOnSamples.end() &&
                                 (!resultCheckOnSamples[itr2->first].first &&
                                  !resultCheckOnSamples[itr2->first].second)) {
-                                STORM_PRINT("  - Not monotone in: " << itr2->first << std::endl);
+                                // STORM_PRINT("  - Not monotone in: " << itr2->first << std::endl);
                                 outfile << "X " << itr2->first;
                             } else {
                                 if (itr2->second.first && itr2->second.second) {
-                                    STORM_PRINT("  - Constant in" << itr2->first << std::endl);
+                                    // STORM_PRINT("  - Constant in" << itr2->first << std::endl);
                                     outfile << "C " << itr2->first;
                                 } else if (itr2->second.first) {
-                                    STORM_PRINT("  - Monotone increasing in: " << itr2->first << std::endl);
+                                    // STORM_PRINT("  - Monotone increasing in: " << itr2->first << std::endl);
                                     outfile << "I " << itr2->first;
                                 } else if (itr2->second.second) {
-                                    STORM_PRINT("  - Monotone decreasing in: " << itr2->first << std::endl);
+                                    // STORM_PRINT("  - Monotone decreasing in: " << itr2->first << std::endl);
                                     outfile << "D " << itr2->first;
                                 } else {
 
-                                    STORM_PRINT(
-                                            "  - Do not know if monotone incr/decreasing in: " << itr2->first << std::endl);
+                                    // STORM_PRINT("  - Do not know if monotone incr/decreasing in: " << itr2->first << std::endl);
                                     outfile << "? " << itr2->first;
                                 }
                             }
                             ++itr2;
                             if (itr2 != varsMonotone.end()) {
-                                outfile << ", ";
+                                outfile << " ";
                             }
                         }
                         result.insert(
                                 std::pair<storm::analysis::Lattice *, std::map<carl::Variable, std::pair<bool, bool>>>(
                                         lattice, varsMonotone));
                     }
-                    outfile << "| ";
-                    outfile.close();
                     ++i;
                 }
             }
+            outfile << ", ";
 
-            finalCheckWatch.stop();
-            STORM_PRINT(std::endl << "Time for monotonicity check on lattice: " << finalCheckWatch << "." << std::endl << std::endl);
-            outfile.open(filename, std::ios_base::app);
-            totalWatch.stop();
-            outfile << totalWatch << "; ";
+            monotonicityCheckWatch.stop();
+            outfile << monotonicityCheckWatch << ", ";
+            // STORM_PRINT(std::endl << "Time for monotonicity check on lattice: " << monotonicityCheckWatch << "." << std::endl << std::endl);
             outfile.close();
             return result;
         }
@@ -259,8 +278,10 @@ namespace storm {
                 assert(false);
             }
             latticeWatch.stop();
-            STORM_PRINT(std::endl << "Total time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);
-            outfile << latticeWatch << "; ";
+            // STORM_PRINT(std::endl << "Total time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);
+            outfile.open(filename, std::ios_base::app);
+            outfile << latticeWatch << ", ";
+            outfile.close();
             return result;
         }
 
@@ -273,19 +294,27 @@ namespace storm {
                 assert (val1 == val2);
                 result.insert(std::pair<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, assumptions));
             } else {
-                auto assumptionPair = assumptionMaker->createAndCheckAssumption(val1, val2, lattice);
-                assert (assumptionPair.size() == 2);
-                auto itr = assumptionPair.begin();
+
+                // TODO: should be triple
+                auto assumptionTriple = assumptionMaker->createAndCheckAssumption(val1, val2, lattice);
+                assert (assumptionTriple.size() == 3);
+                auto itr = assumptionTriple.begin();
                 auto assumption1 = *itr;
                 ++itr;
                 auto assumption2 = *itr;
+                ++itr;
+                auto assumption3 = *itr;
 
                 if (!assumption1.second && !assumption2.second) {
+                    // Both assumption cannot be validated, so we need to keep them both
                     // TODO: hier niet verder gaan als je iets gevonden hebt?
                     auto assumptionsCopy = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions);
+                    auto assumptionsCopy2 = std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(assumptions);
                     auto latticeCopy = new storm::analysis::Lattice(lattice);
+                    auto latticeCopy2 = new storm::analysis::Lattice(lattice);
                     assumptions.push_back(assumption1.first);
                     assumptionsCopy.push_back(assumption2.first);
+                    assumptionsCopy2.push_back(assumption2.first);
 
                     auto criticalTuple = extender->extendLattice(lattice, assumption1.first);
                     if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
@@ -300,7 +329,16 @@ namespace storm {
                                                            assumptionsCopy);
                         result.insert(map.begin(), map.end());
                     }
+                    // TODO verbeteren
+//                    criticalTuple = extender->extendLattice(latticeCopy2, assumption3.first);
+//                    if (somewhereMonotonicity(std::get<0>(criticalTuple))) {
+//                        auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker,
+//                                                                std::get<1>(criticalTuple), std::get<2>(criticalTuple),
+//                                                                assumptionsCopy2);
+//                        result.insert(map.begin(), map.end());
+//                    }
                 } else if (assumption1.second && assumption2.second) {
+                    //TODO  Both assumptions hold --> should not happen if we change it to < instead of <=
                     auto assumption = assumptionMaker->createEqualAssumption(val1, val2);
                     if (!validate) {
                         assumptions.push_back(assumption);
@@ -312,6 +350,7 @@ namespace storm {
                     }
                 } else if (assumption1.second) {
                     if (!validate) {
+                        assert(false);
                         assumptions.push_back(assumption1.first);
                     }
                     // if validate is true and both hold, then they must be valid, so no need to add to assumptions
@@ -339,7 +378,7 @@ namespace storm {
 
         template <typename ValueType>
         std::map<carl::Variable, std::pair<bool, bool>> MonotonicityChecker<ValueType>::analyseMonotonicity(uint_fast64_t j, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) {
-            storm::utility::Stopwatch analyseWatch(true);
+//            storm::utility::Stopwatch analyseWatch(true);
 
             std::map<carl::Variable, std::pair<bool, bool>> varsMonotone;
 
@@ -413,9 +452,9 @@ namespace storm {
                 }
             }
 
-            analyseWatch.stop();
-            STORM_PRINT(std::endl << "Time to check monotonicity based on the lattice: " << analyseWatch << "." << std::endl << std::endl);
-            outfile << analyseWatch << "; ";
+//            analyseWatch.stop();
+            // STORM_PRINT(std::endl << "Time to check monotonicity based on the lattice: " << analyseWatch << "." << std::endl << std::endl);
+//            outfile << analyseWatch << "; ";
             return varsMonotone;
         }
 
@@ -609,7 +648,7 @@ namespace storm {
             }
 
             samplesWatch.stop();
-            STORM_PRINT(std::endl << "Time to check monotonicity on samples: " << samplesWatch << "." << std::endl << std::endl);
+            // STORM_PRINT(std::endl << "Time to check monotonicity on samples: " << samplesWatch << "." << std::endl << std::endl);
             resultCheckOnSamples = result;
             return result;
         }
@@ -680,7 +719,7 @@ namespace storm {
             }
 
             samplesWatch.stop();
-            STORM_PRINT(std::endl << "Time to check monotonicity on samples: " << samplesWatch << "." << std::endl << std::endl);
+            // STORM_PRINT(std::endl << "Time to check monotonicity on samples: " << samplesWatch << "." << std::endl << std::endl);
             resultCheckOnSamples = result;
             return result;
         }

src/test/storm-pars/analysis/AssumptionCheckerTest.cpp

@@ -62,6 +62,20 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) {
                                                          storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual));
     EXPECT_TRUE(checker.checkOnSamples(assumption));
 
+    assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(
+            storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
+                                                         expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(),
+                                                         expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(),
+                                                         storm::expressions::BinaryRelationExpression::RelationType::Greater));
+    EXPECT_TRUE(checker.checkOnSamples(assumption));
+
+    assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(
+            storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
+                                                         expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(),
+                                                         expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(),
+                                                         storm::expressions::BinaryRelationExpression::RelationType::Equal));
+    EXPECT_FALSE(checker.checkOnSamples(assumption));
+
     storm::storage::BitVector above(8);
     above.set(0);
     storm::storage::BitVector below(8);
@@ -79,17 +93,17 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) {
             storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
                                                          expressionManager->getVariable("6").getExpression().getBaseExpressionPointer(),
                                                          expressionManager->getVariable("8").getExpression().getBaseExpressionPointer(),
-                                                         storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual));
+                                                         storm::expressions::BinaryRelationExpression::RelationType::Greater));
     above = storm::storage::BitVector(13);
     above.set(12);
     below = storm::storage::BitVector(13);
     below.set(9);
     initialMiddle = storm::storage::BitVector(13);
     dummyLattice = new storm::analysis::Lattice(above, below, initialMiddle, 13);
-    EXPECT_TRUE(checker.checkOnSamples(assumption));
-    EXPECT_TRUE(checker.validateAssumption(assumption, dummyLattice));
+    EXPECT_FALSE(checker.checkOnSamples(assumption));
+    EXPECT_FALSE(checker.validateAssumption(assumption, dummyLattice));
     EXPECT_TRUE(checker.validated(assumption));
-    EXPECT_TRUE(checker.valid(assumption));
+    EXPECT_FALSE(checker.valid(assumption));
 }
 
 

src/test/storm-pars/analysis/AssumptionMakerTest.cpp

@@ -61,14 +61,14 @@ TEST(AssumptionMakerTest, Brp_without_bisimulation) {
     auto var1 = itr->first->getManager().getVariable("183");
     auto var2 = itr->first->getManager().getVariable("186");
 
-    EXPECT_EQ(2, result.size());
+    EXPECT_EQ(3, result.size());
 
     EXPECT_EQ(false, itr->second);
     EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable());
     EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable());
     EXPECT_EQ(var1, itr->first->getFirstOperand()->asVariableExpression().getVariable());
     EXPECT_EQ(var2, itr->first->getSecondOperand()->asVariableExpression().getVariable());
-    EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, itr->first->getRelationType());
+    EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType());
 
     ++itr;
     EXPECT_EQ(false, itr->second);
@@ -76,6 +76,14 @@ TEST(AssumptionMakerTest, Brp_without_bisimulation) {
     EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable());
     EXPECT_EQ(var2, itr->first->getFirstOperand()->asVariableExpression().getVariable());
     EXPECT_EQ(var1, itr->first->getSecondOperand()->asVariableExpression().getVariable());
-    EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual, itr->first->getRelationType());
+    EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Greater, itr->first->getRelationType());
+
+    ++itr;
+    EXPECT_EQ(false, itr->second);
+    EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable());
+    EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable());
+    EXPECT_EQ(var2, itr->first->getFirstOperand()->asVariableExpression().getVariable());
+    EXPECT_EQ(var1, itr->first->getSecondOperand()->asVariableExpression().getVariable());
+    EXPECT_EQ(storm::expressions::BinaryRelationExpression::RelationType::Equal, itr->first->getRelationType());
     // TODO: createEqualsAssumption checken
 }

src/test/storm-pars/analysis/LatticeTest.cpp

@@ -139,3 +139,37 @@ TEST(LatticeTest, copy_lattice) {
     EXPECT_EQ(storm::analysis::Lattice::BELOW, latticeCopy.compare(6,5));
     EXPECT_EQ(storm::analysis::Lattice::ABOVE, latticeCopy.compare(5,6));
 }
+
+TEST(LatticeTest, merge_nodes) {
+    auto numberOfStates = 7;
+    auto above = storm::storage::BitVector(numberOfStates);
+    above.set(0);
+    auto below = storm::storage::BitVector(numberOfStates);
+    below.set(1);
+    auto initialMiddle = storm::storage::BitVector(numberOfStates);
+
+    auto lattice = storm::analysis::Lattice(above, below, initialMiddle, numberOfStates);
+    lattice.add(2);
+    lattice.add(3);
+    lattice.addToNode(4, lattice.getNode(2));
+    lattice.addBetween(5, lattice.getNode(0), lattice.getNode(3));
+    lattice.addBetween(6, lattice.getNode(5), lattice.getNode(3));
+
+    lattice.mergeNodes(lattice.getNode(4), lattice.getNode(5));
+    EXPECT_EQ(storm::analysis::Lattice::SAME, lattice.compare(2,4));
+    EXPECT_EQ(storm::analysis::Lattice::SAME, lattice.compare(2,5));
+
+    EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,5));
+    EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,2));
+    EXPECT_EQ(storm::analysis::Lattice::ABOVE, lattice.compare(0,4));
+
+    EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(6,2));
+    EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(6,4));
+    EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(6,5));
+    EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(3,2));
+    EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(3,4));
+    EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(3,5));
+    EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,2));
+    EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,4));
+    EXPECT_EQ(storm::analysis::Lattice::BELOW, lattice.compare(1,5));
+}