From 28b77e6a7d8e7872e451741e1e050a47225377f8 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Thu, 6 Sep 2018 13:08:01 +0200 Subject: [PATCH] Create MonotonicityChecker and fix some bugs in AssumptionMaker --- src/storm-pars-cli/storm-pars.cpp | 119 ++------------- src/storm-pars/analysis/AssumptionMaker.cpp | 12 +- src/storm-pars/analysis/Lattice.cpp | 50 +++++- src/storm-pars/analysis/Lattice.h | 8 + .../analysis/MonotonicityChecker.cpp | 144 ++++++++++++++++++ src/storm-pars/analysis/MonotonicityChecker.h | 29 ++++ 6 files changed, 246 insertions(+), 116 deletions(-) create mode 100644 src/storm-pars/analysis/MonotonicityChecker.cpp create mode 100644 src/storm-pars/analysis/MonotonicityChecker.h diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index c44e8a8f8..3a67b13a9 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/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(model->as>(), input, regions, samples); } - template - std::map> analyseMonotonicity(storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) { - //TODO: Seperate cpp file with this and criticalstatefinding/handling - std::map> 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* value = &varsMonotone.find(*itr)->second; - std::pair 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 void processInputWithValueTypeAndDdlib(SymbolicInput& input) { @@ -610,47 +530,26 @@ namespace storm { std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); std::shared_ptr> sparseModel = model->as>(); - // Transform to Lattice + // Transform to Lattices storm::utility::Stopwatch latticeWatch(true); storm::analysis::LatticeExtender *extender = new storm::analysis::LatticeExtender(sparseModel); std::tuple criticalPair = extender->toLattice(formulas); - // TODO met assumptionmaker dingen doen - - auto assumptionMaker = storm::analysis::AssumptionMaker(extender, sparseModel->getNumberOfStates()); std::map>> 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> varsMonotone = analyseMonotonicity(lattice, matrix); + auto monotonicityChecker = storm::analysis::MonotonicityChecker(); + 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; diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index 7124748b2..eec265d23 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -28,6 +28,8 @@ namespace storm { if (critical1 == numberOfStates || critical2 == numberOfStates) { result.insert(std::pair>>(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> 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> assumptions2; std::shared_ptr assumption2 - = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(), + = std::make_shared(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()); } diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 189cff147..e65363cd0 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/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,7 +203,54 @@ namespace storm { out << "}" << std::endl; } - bool Lattice::above(Node *node1, Node *node2, std::set* seenNodes) { + 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 seenNodes = std::set({}); + 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* 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()) { diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index 3d36b9120..02cbdf30a 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/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 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 diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp new file mode 100644 index 000000000..4d490ae9b --- /dev/null +++ b/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 + void MonotonicityChecker::checkMonotonicity(std::map>> map, storm::storage::SparseMatrix 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 expression = *itr; + auto var1 = expression->getFirstOperand(); + auto var2 = expression->getSecondOperand(); + STORM_PRINT("(" << var1->getIdentifier() << " > " << var2->getIdentifier() << ")"); + } + STORM_PRINT(std::endl); + + std::map> 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 + std::map> MonotonicityChecker::analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) { + std::map> 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* value = &varsMonotone.find(*itr)->second; + std::pair 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; + } + +} + diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h new file mode 100644 index 000000000..7b1dcb1f1 --- /dev/null +++ b/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 +#include "Lattice.h" +#include "storm/storage/expressions/BinaryRelationExpression.h" +#include "storm/storage/SparseMatrix.h" +#include "carl/core/Variable.h" + +namespace storm { + namespace analysis { + + template + class MonotonicityChecker { + + public: + void checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix); + + private: + std::map> analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) ; + + }; + } +} +#endif //STORM_MONOTONICITYCHECKER_H