From 7ad2c211ed774a9ca4551df11e23ce3e5040ba4e Mon Sep 17 00:00:00 2001 From: alzeha Date: Wed, 28 Aug 2024 14:40:41 +0200 Subject: [PATCH] improved non-deterministic --- include/tchecker/zg/zone_container.hh | 44 +++++++--- .../virtual_clock_algorithm.cc | 87 ++++++++++++++++++- 2 files changed, 113 insertions(+), 18 deletions(-) diff --git a/include/tchecker/zg/zone_container.hh b/include/tchecker/zg/zone_container.hh index bb87a622..8bfc51cc 100644 --- a/include/tchecker/zg/zone_container.hh +++ b/include/tchecker/zg/zone_container.hh @@ -284,6 +284,22 @@ std::shared_ptr> logical_and_container(zone_container_t & return result; } + +template +std::shared_ptr> logical_and_container(std::vector>> & lo_container, + std::shared_ptr (*factory)(tchecker::clock_id_t)) +{ + assert(!lo_container.empty()); + + auto iter = lo_container.begin(); + auto result = std::make_shared>(**iter); + iter++; + for( ; iter < lo_container.end(); iter++) { + result = logical_and_container(*result, **iter, factory); + } + return result; +} + /* \brief a matrix of container for all subtypes of zone */ @@ -295,14 +311,14 @@ public: /*! \brief Constructor - \param row_size : number of rows in matrix - \param column_size : number of columns in matrix + \param no_of_rows : number of rows in matrix + \param no_of_columns : number of columns in matrix \param dim : the dimension of the zones */ - zone_matrix_t(size_t row_size, size_t column_size, tchecker::clock_id_t dim) : - _dim(dim), _row_size(row_size), _column_size(column_size), _matrix(std::vector>>(row_size * column_size)) { + zone_matrix_t(size_t no_of_rows, size_t no_of_columns, tchecker::clock_id_t dim) : + _dim(dim), _no_of_rows(no_of_rows), _no_of_columns(no_of_columns), _matrix(std::vector>>(no_of_rows * no_of_columns)) { - for(std::size_t i = 0; i < row_size*column_size; ++i) { + for(std::size_t i = 0; i < no_of_rows*no_of_columns; ++i) { _matrix[i] = std::make_shared>(dim); } }; @@ -314,23 +330,23 @@ public: \return pointer to the element */ std::shared_ptr> get(size_t row, size_t column) { - assert(row < _row_size); - assert(column < _column_size); + assert(row < _no_of_rows); + assert(column < _no_of_columns); - return _matrix[row*_column_size + column]; + return _matrix[row*_no_of_columns + column]; } /*! \brief Accessor for the row size \return the row size */ - size_t get_row_size() const { return _row_size; } + size_t get_no_of_rows() const { return _no_of_rows; } /*! \brief Accessor for the column size \return the column size */ - size_t get_column_size() const { return _column_size; } + size_t get_no_of_columns() const { return _no_of_columns; } /*! \brief Accessor for the dim @@ -341,7 +357,7 @@ public: std::shared_ptr>>> get_row(size_t row) { auto result = std::make_shared>>>(); - for(size_t i = 0; i < this->get_column_size(); i++) { + for(size_t i = 0; i < this->get_no_of_columns(); i++) { result->emplace_back(this->get(row, i)); } return result; @@ -350,7 +366,7 @@ public: std::shared_ptr>>> get_column(size_t column) { auto result = std::make_shared>>>(); - for(size_t i = 0; i < this->get_row_size(); i++) { + for(size_t i = 0; i < this->get_no_of_rows(); i++) { result->emplace_back(this->get(i, column)); } return result; @@ -358,7 +374,7 @@ public: void print_zone_matrix(std::ostream & os) { - for(auto i = 0; i < _row_size; ++i) { + for(auto i = 0; i < _no_of_rows; ++i) { auto row = get_row(i); for(auto cur : row) { row->print_container(os); @@ -372,7 +388,7 @@ public: const tchecker::clock_id_t _dim; - const size_t _row_size, _column_size; + const size_t _no_of_rows, _no_of_columns; std::vector>> _matrix; }; diff --git a/src/strong-timed-bisim/virtual_clock_algorithm.cc b/src/strong-timed-bisim/virtual_clock_algorithm.cc index e4672356..56881bee 100644 --- a/src/strong-timed-bisim/virtual_clock_algorithm.cc +++ b/src/strong-timed-bisim/virtual_clock_algorithm.cc @@ -405,6 +405,85 @@ Lieb_et_al::check_target_pair(tchecker::zg::state_sptr_t target_state_A, tchecke } +bool contradiction_still_possible(tchecker::zone_matrix_t & found_cont, + std::vector< std::vector > finished) +{ + + assert(found_cont.get_no_of_rows() > 0); + assert(found_cont.get_no_of_columns() > 0); + + assert(finished.size() == found_cont.get_no_of_rows()); + std::for_each(finished.begin(), finished.end(), [found_cont](std::vector cur) { assert(cur.size() == found_cont.get_no_of_columns()); } ); + + // if all pairs are finished, there cannot be another contradiction found + bool all_finished = true; + for(size_t i = 0; i < found_cont.get_no_of_rows(); ++i) { + for(size_t j = 0; j < found_cont.get_no_of_columns(); ++j) { + if(!finished[i][j]) { + all_finished = false; + } + } + } + + if(all_finished) { + return false; + } + + // first check all rows + for(size_t i = 0; i < found_cont.get_no_of_rows(); i++) { + + auto row = found_cont.get_row(i); + std::vector>> usable + = std::vector>>(); + + // append all finished elements to usable (no_of_columns = no of elements in a row) + for(size_t j = 0; j < found_cont.get_no_of_columns(); j++) { + if(finished[i][j]) { + usable.emplace_back((*row)[j]); + } + } + + // if none of the pair is finished there are still contradictions possible + if(usable.size() == 0) { + return true; + } + + auto conjunction = logical_and_container( + usable, [] (tchecker::clock_id_t dim) {return tchecker::virtual_constraint::factory(dim - 1);}); + if(!conjunction->is_empty()) { + return true; + } + } + + // now check all columns + for(size_t i = 0; i < found_cont.get_no_of_columns(); i++) { + + auto row = found_cont.get_row(i); + std::vector>> usable + = std::vector>>(); + // append all finished elements to usable + for(size_t j = 0; j < found_cont.get_no_of_rows(); j++) { + if(finished[j][i]) { + usable.emplace_back((*row)[j]); + } + } + + // if none of the pair is finished there are still contradictions possible + if(usable.size() == 0) { + return true; + } + + auto conjunction = logical_and_container( + usable, [] (tchecker::clock_id_t dim) {return tchecker::virtual_constraint::factory(dim - 1);}); + if(!conjunction->is_empty()) { + return true; + } + } + // if there is no overall contradiction possible anymore, return false + return false; + +} + std::shared_ptr> Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::zone_t const & zone_A, tchecker::zg::zone_t const & zone_B, std::vector & trans_A, std::vector & trans_B, @@ -439,7 +518,7 @@ Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::zone_t const & zone_A, } tchecker::zone_matrix_t found_cont{trans_A.size(), trans_B.size(), _A->get_no_of_virtual_clocks() + 1}; - std::vector finished(trans_A.size() * trans_B.size(), false); + std::vector> finished(trans_A.size(), std::vector(trans_B.size(), false)); // init the finished matrix with false // we add an optimization here. We first check if the union of the targets of both sides are virtually equivalent. If they are not, we can already stop here. // We do this by running the search_contradiction function without an empty matrix and checking, whether this already returns a contradiction. @@ -457,7 +536,7 @@ Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::zone_t const & zone_A, assert(tchecker::dbm::is_tight(s_A->zone().dbm(), s_A->zone().dim())); for(size_t idx_B = 0; idx_B < trans_B.size(); idx_B++) { - if(finished[idx_A *trans_B.size() + idx_B]) { + if(finished[idx_A][idx_B]) { continue; } auto && [status_B, s_B, t_B] = *(trans_B[idx_B]); @@ -478,7 +557,7 @@ Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::zone_t const & zone_A, auto new_cont = check_target_pair(s_A_constrained, t_A, s_B_constrained, t_B, found_cont.get(idx_A, idx_B), visited); if(new_cont->is_empty()) { - finished[idx_A *trans_B.size() + idx_B] = true; + finished[idx_A][idx_B] = true; } else { found_cont.get(idx_A, idx_B)->append_container(new_cont); found_cont.get(idx_A, idx_B)->compress(); @@ -492,7 +571,7 @@ Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::zone_t const & zone_A, return contradiction; } - } while(std::count(finished.begin(), finished.end(), false) > 0); + } while(contradiction_still_possible(found_cont, finished)); return std::make_shared>(_A->get_no_of_virtual_clocks() + 1);