From f5dac3a567a05045d3d228529d7f0f4ca2dca542 Mon Sep 17 00:00:00 2001 From: alzeha Date: Thu, 29 Aug 2024 11:44:31 +0200 Subject: [PATCH] Improved non-determ cases --- include/tchecker/zg/zone_container.hh | 46 +++++++++++++------ .../search_contradiction.cc | 5 +- .../virtual_clock_algorithm.cc | 41 +++++++++++++++-- 3 files changed, 71 insertions(+), 21 deletions(-) diff --git a/include/tchecker/zg/zone_container.hh b/include/tchecker/zg/zone_container.hh index bb87a622..137424c9 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,34 +330,34 @@ 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 \return the dimension of the virtual constraints */ - size_t get_dim() const { return _dim; } + tchecker::clock_id_t get_dim() const { return _dim; } 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/search_contradiction.cc b/src/strong-timed-bisim/search_contradiction.cc index 86b6c5a3..67688c14 100644 --- a/src/strong-timed-bisim/search_contradiction.cc +++ b/src/strong-timed-bisim/search_contradiction.cc @@ -28,8 +28,9 @@ std::shared_ptr> find_contradiction(tchecker::zg::zone_t const & zone, std::vector & trans, - std::vector>> & vcs, tchecker::clock_id_t no_of_virt_clks) +std::shared_ptr> +find_contradiction(tchecker::zg::zone_t const & zone, std::vector & trans, + std::vector>> & vcs, tchecker::clock_id_t no_of_virt_clks) { assert(0 != trans.size()); diff --git a/src/strong-timed-bisim/virtual_clock_algorithm.cc b/src/strong-timed-bisim/virtual_clock_algorithm.cc index e4672356..74120dfe 100644 --- a/src/strong-timed-bisim/virtual_clock_algorithm.cc +++ b/src/strong-timed-bisim/virtual_clock_algorithm.cc @@ -405,6 +405,39 @@ Lieb_et_al::check_target_pair(tchecker::zg::state_sptr_t target_state_A, tchecke } +bool contradiction_still_possible(tchecker::zg::zone_t const & zone_A, tchecker::zg::zone_t const & zone_B, + std::vector & trans_A, std::vector & trans_B, + 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()); } ); + + tchecker::zone_matrix_t new_cont{found_cont.get_no_of_rows(), found_cont.get_no_of_columns(), found_cont.get_dim()}; + + 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]) { + new_cont.get(i, j)->append_container(found_cont.get(i, j)); + } else { + auto vc_true = tchecker::virtual_constraint::factory(found_cont.get_dim() - 1); + vc_true->make_universal(); + new_cont.get(i, j)->append_zone(vc_true); + } + } + } + + auto cont_possible = search_contradiction(zone_A, zone_B, trans_A, trans_B, new_cont, found_cont.get_dim() - 1); + cont_possible->compress(); + + return !cont_possible->is_empty(); + +} + 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 +472,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 +490,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 +511,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 +525,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(zone_A, zone_B, trans_A, trans_B, found_cont, finished)); return std::make_shared>(_A->get_no_of_virtual_clocks() + 1);