Create MonotonicityChecker and fix some bugs in AssumptionMaker

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

@@ -1,12 +1,14 @@
 
 
-#include "storm-pars/analysis/LatticeExtender.h"
+
 #include "storm-pars/analysis/AssumptionMaker.h"
+#include "storm-pars/analysis/Lattice.h"
+#include "storm-pars/analysis/LatticeExtender.h"
+#include "storm-pars/analysis/MonotonicityChecker.h"
+
 #include "storm-cli-utilities/cli.h"
 #include "storm-cli-utilities/model-handling.h"
 
-#include "storm-pars/analysis/Lattice.h"
-
 #include "storm-pars/api/storm-pars.h"
 #include "storm-pars/api/region.h"
 
@@ -456,88 +458,6 @@ namespace storm {
             storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, samples);
         }
 
-        template <typename ValueType>
-        std::map<carl::Variable, std::pair<bool, bool>> analyseMonotonicity(storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) {
-            //TODO: Seperate cpp file with this and criticalstatefinding/handling
-            std::map<carl::Variable, std::pair<bool, bool>> varsMonotone;
-            ofstream myfile;
-            myfile.open ("mc.dot");
-            myfile << "digraph \"MC\" {" << std::endl;
-            myfile << "\t" << "node [shape=ellipse]" << std::endl;
-            // print all nodes
-            for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) {
-                myfile << "\t\"" << i << "\" [label = \"" << i << "\"]" << std::endl;
-            }
-
-
-            for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) {
-                // go over all rows
-                auto row = matrix.getRow(i);
-
-                auto first = (*row.begin());
-                if (first.getValue() != ValueType(1)) {
-                    auto second = (*(++row.begin()));
-                    string color = "";
-                    auto val = first.getValue();
-                    auto vars = val.gatherVariables();
-                    for (auto itr = vars.begin(); itr != vars.end(); ++itr) {
-                        auto derivative = val.derivative(*itr);
-                        STORM_LOG_THROW(derivative.isConstant(), storm::exceptions::NotSupportedException, "Expecting derivative to be constant");
-
-                        if (varsMonotone.find(*itr) == varsMonotone.end()) {
-                            varsMonotone[*itr].first = true;
-                            varsMonotone[*itr].second = true;
-                        }
-
-                        auto compare = lattice->compare(first.getColumn(), second.getColumn());
-                        std::pair<bool, bool>* value = &varsMonotone.find(*itr)->second;
-                        std::pair<bool, bool> old = *value;
-                        if (compare == 1) {
-                            value->first &=derivative.constantPart() >= 0;
-                            value->second &=derivative.constantPart() <= 0;
-                        } else if (compare == 2) {
-                            value->first &=derivative.constantPart() <= 0;
-                            value->second &=derivative.constantPart() >= 0;
-                        } else if (compare == 0) {
-                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Don't know what is happening, something in monotonicity checking went wrong");
-                        } else {
-                            value->first = false;
-                            value->second = false;
-                        }
-                        if ((value->first != old.first) && (value->second != old.second)) {
-                            color = "color = red, ";
-                        } else if ((value->first != old.first)) {
-                            myfile << "\t edge[style=dashed];" << std::endl;
-                            color = "color = blue, ";
-                        } else if ((value->second != old.second)) {
-                            myfile << "\t edge[style=dotted];" << std::endl;
-                            color = "color = blue, ";
-                        }
-                    }
-
-                    myfile << "\t" << i << " -> " << first.getColumn() << "[" << color << "label=\"" << first.getValue() << "\"];"
-                           << std::endl;
-                    myfile << "\t" << i << " -> " << second.getColumn() << "[" << color << "label=\"" << second.getValue() << "\"];"
-                           << std::endl;
-                    myfile << "\t edge[style=\"\"];" << std::endl;
-                } else {
-                    myfile << "\t" << i << " -> " << first.getColumn() << "[label=\"" << first.getValue() << "\"];"
-                           << std::endl;
-                }
-            }
-
-            myfile << "\tsubgraph legend {" << std::endl;
-            myfile << "\t\tnode [color=white];" << std::endl;
-            myfile << "\t\tedge [style=invis];" << std::endl;
-            myfile << "\t\tt0 [label=\"incr? and decr?\", fontcolor=red];" << std::endl;
-            myfile << "\t\tt1 [label=\"incr? (dashed)\", fontcolor=blue];" << std::endl;
-            myfile << "\t\tt2 [label=\"decr? (dotted)\", fontcolor=blue];" << std::endl;
-
-            myfile << "\t}" << std::endl;
-            myfile << "}" << std::endl;
-            myfile.close();
-            return varsMonotone;
-        };
 
         template <storm::dd::DdType DdType, typename ValueType>
         void processInputWithValueTypeAndDdlib(SymbolicInput& input) {
@@ -610,47 +530,26 @@ namespace storm {
                 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
 
-                // Transform to Lattice
+                // Transform to Lattices
                 storm::utility::Stopwatch latticeWatch(true);
                 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);
 
-                // TODO met assumptionmaker dingen doen
-
-
                 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);
 
-                // Write lattice to file
-                ofstream myfile;
-                myfile.open ("lattice.dot");
-                lattice->toDotFile(myfile);
-                myfile.close();
 
                 // Monotonicity?
-                auto matrix = sparseModel->getTransitionMatrix();
+
                 storm::utility::Stopwatch monotonicityWatch(true);
-                std::map<carl::Variable, std::pair<bool, bool>> varsMonotone = analyseMonotonicity<ValueType>(lattice, matrix);
+                auto monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>();
+                monotonicityChecker.checkMonotonicity(result, sparseModel->getTransitionMatrix());
                 monotonicityWatch.stop();
                 STORM_PRINT(std::endl << "Time for monotonicity: " << monotonicityWatch << "." << std::endl << std::endl);
 
-                for (auto itr = varsMonotone.begin(); itr != varsMonotone.end(); ++itr) {
-                    if (itr->second.first) {
-                        STORM_PRINT("Monotone increasing in: " << itr->first << std::endl);
-                    } else {
-                        STORM_PRINT("Do not know if monotone increasing in: " << itr->first << std::endl);
-                    }
-                    if (itr->second.second) {
-                        STORM_PRINT("Monotone decreasing in: " << itr->first << std::endl);
-                    } else {
-                        STORM_PRINT("Do not know if monotone decreasing in: " << itr->first << std::endl);
-                    }
-                }
 
                 std::cout << "Bye, Jip2" << std::endl;
                 return;

src/storm-pars/analysis/AssumptionMaker.cpp

@@ -28,6 +28,8 @@ namespace storm {
             if (critical1 == numberOfStates || critical2 == numberOfStates) {
                 result.insert(std::pair<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, emptySet));
             } else {
+
+                //TODO: opruimen
                 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;
@@ -36,18 +38,18 @@ namespace storm {
                         var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
                         storm::expressions::BinaryRelationExpression::RelationType::Greater));
                 assumptions1.insert(assumption1);
-                auto lattice1 = new storm::analysis::Lattice(*lattice);
+                auto lattice1 = lattice->deepCopy();
                 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(),
+                    = std::make_shared<storm::expressions::BinaryRelationExpression>(storm::expressions::BinaryRelationExpression(*expressionManager, var2.getType(),
                         var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(),
                         storm::expressions::BinaryRelationExpression::RelationType::Greater));
                 assumptions2.insert(assumption2);
 
-                auto lattice2 = new storm::analysis::Lattice(*lattice);
+                auto lattice2 = lattice->deepCopy();
                 auto myMap2 = (runRecursive(lattice2, assumptions2));
                 result.insert(myMap2.begin(), myMap2.end());
             }
@@ -70,7 +72,7 @@ namespace storm {
                                                                                     var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(),
                                                                                     storm::expressions::BinaryRelationExpression::RelationType::Greater));
                 assumptions1.insert(assumption1);
-                auto lattice1 = new storm::analysis::Lattice(*lattice);
+                auto lattice1 = lattice->deepCopy();
                 auto myMap = (runRecursive(lattice1, assumptions1));
                 result.insert(myMap.begin(), myMap.end());
 
@@ -80,7 +82,7 @@ namespace storm {
                                                                                     var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(),
                                                                                     storm::expressions::BinaryRelationExpression::RelationType::Greater))   ;
                 assumptions2.insert(assumption2);
-                auto lattice2 = new storm::analysis::Lattice(*lattice);
+                auto lattice2 = lattice->deepCopy();
                 myMap = (runRecursive(lattice2, assumptions2));
                 result.insert(myMap.begin(), myMap.end());
             }

src/storm-pars/analysis/Lattice.cpp

@@ -164,6 +164,7 @@ namespace storm {
         }
 
         void Lattice::toDotFile(std::ostream &out) {
+            // TODO: op de een of andere manier ontstaan er nodes die nergens eindigen/beginnen
         out << "digraph \"Lattice\" {" << std::endl;
 
         // print all nodes
@@ -202,6 +203,53 @@ namespace storm {
         out << "}" << std::endl;
     }
 
+        Lattice* Lattice::deepCopy() {
+            // TODO zonder bottom is eigenlijk beter
+            Lattice* result = new Lattice(top->states, bottom->states, numberOfStates);
+
+            for (auto itr = top->below.begin(); itr != top->below.end(); ++itr) {
+                result->nogBedenken(*itr, result->getTop(), storm::storage::BitVector(numberOfStates));
+            }
+
+
+            return result;
+        }
+
+        void Lattice::nogBedenken(Lattice::Node* nodeFromOld, Lattice::Node* higherNode, storm::storage::BitVector seenStates) {
+            auto index = numberOfStates;
+            std::set<Node*> seenNodes = std::set<Node*>({});
+            for (auto i = nodeFromOld->states.getNextSetIndex(0); i < numberOfStates; i =nodeFromOld->states.getNextSetIndex(i+1)) {
+                Node * nodeI = getNode(i);
+                if (nodeI == nullptr && index == numberOfStates) {
+                    nodeI = new Node();
+                    nodeI->states = storm::storage::BitVector(numberOfStates);
+                    nodeI->states.set(i);
+                    higherNode->above.insert(nodeI);
+                    nodeI->below.insert(higherNode);
+                    addedStates.set(i);
+                    nodes.at(i) = nodeI;
+                } else if (nodeI == nullptr) {
+                    addToNode(i, getNode(index));
+                } else {
+                    nodeI->above.insert(higherNode);
+                    higherNode->below.insert(nodeI);
+                    addedStates.set(i);
+                }
+                seenStates.set(i);
+                index = i;
+                seenNodes.insert(nodeI);
+            }
+
+            for (auto itr = nodeFromOld->below.begin(); itr != nodeFromOld->below.end(); itr++) {
+//                if (!seenStates.get((*itr)->states.getNextSetIndex(0))) {
+                    for (auto itr2 = seenNodes.begin(); itr2 != seenNodes.end(); ++itr2) {
+                        nogBedenken(*itr, *itr2, seenStates);
+                    }
+//                }
+            }
+
+        }
+
         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) {

src/storm-pars/analysis/Lattice.h

@@ -104,11 +104,18 @@ namespace storm {
                      */
                     void toDotFile(std::ostream &out);
 
+                    Lattice* deepCopy();
+
                     static const int UNKNOWN = -1;
                     static const int BELOW = 2;
                     static const int ABOVE = 1;
                     static const int SAME = 0;
 
+                protected:
+                    void addBelow(uint_fast64_t state, Node* node);
+
+                    void addAbove(uint_fast64_t state, Node* node);
+
                 private:
                     std::vector<Node*> nodes;
 
@@ -120,6 +127,7 @@ namespace storm {
 
                     uint_fast64_t numberOfStates;
 
+                    void nogBedenken(Node* nodeFromOld, Node* higherNode, storm::storage::BitVector seenStates);
                     /**
                      * Check if node1 lies above node2
                      * @param node1

src/storm-pars/analysis/MonotonicityChecker.cpp

@@ -0,0 +1,144 @@
+//
+// Created by Jip Spel on 05.09.18.
+//
+
+#include "MonotonicityChecker.h"
+#include "storm/exceptions/UnexpectedException.h"
+#include "storm/exceptions/NotSupportedException.h"
+
+namespace storm {
+    namespace analysis {
+        template <typename ValueType>
+        void MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
+
+            auto i = 0;
+            for (auto itr = map.begin(); itr != map.end(); ++itr) {
+                auto lattice = itr->first;
+                auto assumptions = itr->second;
+                std::ofstream myfile;
+                std::string filename = "lattice" + std::to_string(i) + ".dot";
+                myfile.open (filename);
+                lattice->toDotFile(myfile);
+                myfile.close();
+
+                STORM_PRINT("Given assumptions: " << std::endl);
+                bool first = true;
+                for (auto itr = assumptions.begin(); itr != assumptions.end(); ++itr) {
+                    if (!first) {
+                        STORM_PRINT(" ^ ");
+                    } else {
+                        STORM_PRINT("    ");
+                    }
+                    first = false;
+                    std::shared_ptr<storm::expressions::BinaryRelationExpression> expression = *itr;
+                    auto var1 = expression->getFirstOperand();
+                    auto var2 = expression->getSecondOperand();
+                    STORM_PRINT("(" << var1->getIdentifier() << " > " << var2->getIdentifier() << ")");
+                }
+                STORM_PRINT(std::endl);
+
+                std::map<carl::Variable, std::pair<bool, bool>> varsMonotone = analyseMonotonicity(i, lattice, matrix);
+                for (auto itr2 = varsMonotone.begin(); itr2 != varsMonotone.end(); ++itr2) {
+                    if (itr2->second.first) {
+                        STORM_PRINT("  - Monotone increasing in: " << itr2->first << std::endl);
+                    } else {
+                        STORM_PRINT("  - Do not know if monotone increasing in: " << itr2->first << std::endl);
+                    }
+                    if (itr2->second.second) {
+                        STORM_PRINT("  - Monotone decreasing in: " << itr2->first << std::endl);
+                    } else {
+                        STORM_PRINT("  - Do not know if monotone decreasing in: " << itr2->first << std::endl);
+                    }
+                }
+
+                ++i;
+            }
+        }
+
+        template <typename ValueType>
+        std::map<carl::Variable, std::pair<bool, bool>> MonotonicityChecker<ValueType>::analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) {
+            std::map<carl::Variable, std::pair<bool, bool>> varsMonotone;
+            std::ofstream myfile;
+            std::string filename = "mc" + std::to_string(i) + ".dot";
+            myfile.open (filename);
+            myfile << "digraph \"MC\" {" << std::endl;
+            myfile << "\t" << "node [shape=ellipse]" << std::endl;
+            // print all nodes
+            for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) {
+                myfile << "\t\"" << i << "\" [label = \"" << i << "\"]" << std::endl;
+            }
+
+
+            for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) {
+                // go over all rows
+                auto row = matrix.getRow(i);
+
+                auto first = (*row.begin());
+                if (first.getValue() != ValueType(1)) {
+                    auto second = (*(++row.begin()));
+                    std::string color = "";
+                    auto val = first.getValue();
+                    auto vars = val.gatherVariables();
+                    for (auto itr = vars.begin(); itr != vars.end(); ++itr) {
+                        auto derivative = val.derivative(*itr);
+                        STORM_LOG_THROW(derivative.isConstant(), storm::exceptions::NotSupportedException, "Expecting derivative to be constant");
+
+                        if (varsMonotone.find(*itr) == varsMonotone.end()) {
+                            varsMonotone[*itr].first = true;
+                            varsMonotone[*itr].second = true;
+                        }
+
+                        auto compare = lattice->compare(first.getColumn(), second.getColumn());
+                        std::pair<bool, bool>* value = &varsMonotone.find(*itr)->second;
+                        std::pair<bool, bool> old = *value;
+                        if (compare == 1) {
+                            value->first &=derivative.constantPart() >= 0;
+                            value->second &=derivative.constantPart() <= 0;
+                        } else if (compare == 2) {
+                            value->first &=derivative.constantPart() <= 0;
+                            value->second &=derivative.constantPart() >= 0;
+                        } else if (compare == 0) {
+                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Don't know what is happening, something in monotonicity checking went wrong");
+                        } else {
+                            value->first = false;
+                            value->second = false;
+                        }
+                        if ((value->first != old.first) && (value->second != old.second)) {
+                            color = "color = red, ";
+                        } else if ((value->first != old.first)) {
+                            myfile << "\t edge[style=dashed];" << std::endl;
+                            color = "color = blue, ";
+                        } else if ((value->second != old.second)) {
+                            myfile << "\t edge[style=dotted];" << std::endl;
+                            color = "color = blue, ";
+                        }
+                    }
+
+                    myfile << "\t" << i << " -> " << first.getColumn() << "[" << color << "label=\"" << first.getValue() << "\"];"
+                           << std::endl;
+                    myfile << "\t" << i << " -> " << second.getColumn() << "[" << color << "label=\"" << second.getValue() << "\"];"
+                           << std::endl;
+                    myfile << "\t edge[style=\"\"];" << std::endl;
+                } else {
+                    myfile << "\t" << i << " -> " << first.getColumn() << "[label=\"" << first.getValue() << "\"];"
+                           << std::endl;
+                }
+            }
+
+            myfile << "\tsubgraph legend {" << std::endl;
+            myfile << "\t\tnode [color=white];" << std::endl;
+            myfile << "\t\tedge [style=invis];" << std::endl;
+            myfile << "\t\tt0 [label=\"incr? and decr?\", fontcolor=red];" << std::endl;
+            myfile << "\t\tt1 [label=\"incr? (dashed)\", fontcolor=blue];" << std::endl;
+            myfile << "\t\tt2 [label=\"decr? (dotted)\", fontcolor=blue];" << std::endl;
+
+            myfile << "\t}" << std::endl;
+            myfile << "}" << std::endl;
+            myfile.close();
+            return varsMonotone;
+        };
+        template class MonotonicityChecker<storm::RationalFunction>;
+    }
+
+}
+

src/storm-pars/analysis/MonotonicityChecker.h

@@ -0,0 +1,29 @@
+//
+// Created by Jip Spel on 03.09.18.
+//
+
+#ifndef STORM_MONOTONICITYCHECKER_H
+#define STORM_MONOTONICITYCHECKER_H
+
+#include <map>
+#include "Lattice.h"
+#include "storm/storage/expressions/BinaryRelationExpression.h"
+#include "storm/storage/SparseMatrix.h"
+#include "carl/core/Variable.h"
+
+namespace storm {
+    namespace analysis {
+
+        template <typename ValueType>
+        class MonotonicityChecker {
+
+        public:
+            void checkMonotonicity(std::map<storm::analysis::Lattice*, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix);
+
+        private:
+            std::map<carl::Variable, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) ;
+
+        };
+    }
+}
+#endif //STORM_MONOTONICITYCHECKER_H