|
@ -3,14 +3,13 @@ |
|
|
//
|
|
|
//
|
|
|
|
|
|
|
|
|
#include "MonotonicityChecker.h"
|
|
|
#include "MonotonicityChecker.h"
|
|
|
#include "storm/exceptions/UnexpectedException.h"
|
|
|
|
|
|
#include "storm/exceptions/NotSupportedException.h"
|
|
|
#include "storm/exceptions/NotSupportedException.h"
|
|
|
|
|
|
#include "storm/exceptions/UnexpectedException.h"
|
|
|
|
|
|
|
|
|
namespace storm { |
|
|
namespace storm { |
|
|
namespace analysis { |
|
|
namespace analysis { |
|
|
template <typename ValueType> |
|
|
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) { |
|
|
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; |
|
|
auto i = 0; |
|
|
for (auto itr = map.begin(); itr != map.end(); ++itr) { |
|
|
for (auto itr = map.begin(); itr != map.end(); ++itr) { |
|
|
auto lattice = itr->first; |
|
|
auto lattice = itr->first; |
|
@ -52,7 +51,6 @@ namespace storm { |
|
|
STORM_PRINT(" - Do not know if monotone decreasing in: " << itr2->first << std::endl); |
|
|
STORM_PRINT(" - Do not know if monotone decreasing in: " << itr2->first << std::endl); |
|
|
} |
|
|
} |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
++i; |
|
|
++i; |
|
|
} |
|
|
} |
|
|
} |
|
|
} |
|
@ -65,12 +63,12 @@ namespace storm { |
|
|
myfile.open (filename); |
|
|
myfile.open (filename); |
|
|
myfile << "digraph \"MC\" {" << std::endl; |
|
|
myfile << "digraph \"MC\" {" << std::endl; |
|
|
myfile << "\t" << "node [shape=ellipse]" << std::endl; |
|
|
myfile << "\t" << "node [shape=ellipse]" << std::endl; |
|
|
|
|
|
|
|
|
// print all nodes
|
|
|
// print all nodes
|
|
|
for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { |
|
|
for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { |
|
|
myfile << "\t\"" << i << "\" [label = \"" << i << "\"]" << std::endl; |
|
|
myfile << "\t\"" << i << "\" [label = \"" << i << "\"]" << std::endl; |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { |
|
|
for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { |
|
|
// go over all rows
|
|
|
// go over all rows
|
|
|
auto row = matrix.getRow(i); |
|
|
auto row = matrix.getRow(i); |
|
@ -134,7 +132,6 @@ namespace storm { |
|
|
<< std::endl; |
|
|
<< std::endl; |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
myfile << "\t edge[style=\"\"];" << std::endl; |
|
|
myfile << "\t edge[style=\"\"];" << std::endl; |
|
|
} else { |
|
|
} else { |
|
|
myfile << "\t" << i << " -> " << first.getColumn() << "[label=\"" << first.getValue() << "\"];" |
|
|
myfile << "\t" << i << " -> " << first.getColumn() << "[label=\"" << first.getValue() << "\"];" |
|
@ -153,7 +150,8 @@ namespace storm { |
|
|
myfile << "}" << std::endl; |
|
|
myfile << "}" << std::endl; |
|
|
myfile.close(); |
|
|
myfile.close(); |
|
|
return varsMonotone; |
|
|
return varsMonotone; |
|
|
}; |
|
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
template class MonotonicityChecker<storm::RationalFunction>; |
|
|
template class MonotonicityChecker<storm::RationalFunction>; |
|
|
} |
|
|
} |
|
|
} |
|
|
} |