Browse Source

Add return to check monotonicity

tempestpy_adaptions
Jip Spel 6 years ago
parent
commit
d99e728add
  1. 5
      src/storm-pars/analysis/MonotonicityChecker.cpp
  2. 2
      src/storm-pars/analysis/MonotonicityChecker.h

5
src/storm-pars/analysis/MonotonicityChecker.cpp

@ -9,8 +9,9 @@
namespace storm { namespace storm {
namespace analysis { namespace analysis {
template <typename ValueType> template <typename ValueType>
void MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
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) {
auto i = 0; auto i = 0;
std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> result;
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;
auto assumptions = itr->second; auto assumptions = itr->second;
@ -53,7 +54,9 @@ namespace storm {
} }
} }
++i; ++i;
result.insert(std::pair<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>>(lattice, varsMonotone));
} }
return result;
} }
template <typename ValueType> template <typename ValueType>

2
src/storm-pars/analysis/MonotonicityChecker.h

@ -24,7 +24,7 @@ namespace storm {
* @param map The map with lattices and the assumptions made to create the lattices. * @param map The map with lattices and the assumptions made to create the lattices.
* @param matrix The transition matrix. * @param matrix The transition matrix.
*/ */
void checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix);
std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix);
private: private:
std::map<carl::Variable, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) ; std::map<carl::Variable, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) ;

Loading…
Cancel
Save