diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 62be096db..0d98cd3f9 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -3,14 +3,13 @@ // #include "MonotonicityChecker.h" -#include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/UnexpectedException.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; @@ -52,7 +51,6 @@ namespace storm { STORM_PRINT(" - Do not know if monotone decreasing in: " << itr2->first << std::endl); } } - ++i; } } @@ -65,12 +63,12 @@ namespace storm { 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); @@ -134,7 +132,6 @@ namespace storm { << std::endl; } - myfile << "\t edge[style=\"\"];" << std::endl; } else { myfile << "\t" << i << " -> " << first.getColumn() << "[label=\"" << first.getValue() << "\"];" @@ -153,7 +150,8 @@ namespace storm { 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 index 7b1dcb1f1..9d90e8b5d 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.h +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -18,6 +18,12 @@ namespace storm { class MonotonicityChecker { public: + /*! + * Checks for all lattices in the map if they are monotone increasing or monotone decreasing. + * + * @param map The map with lattices and the assumptions made to create the lattices. + * @param matrix The transition matrix. + */ void checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix); private: