Skip to content

Commit

Permalink
Improved non-determ cases
Browse files Browse the repository at this point in the history
  • Loading branch information
@alzeha
alzeha committed Aug 29, 2024
1 parent 992467d commit f5dac3a
Show file tree
Hide file tree
Showing 3 changed files with 71 additions and 21 deletions.
46 changes: 31 additions & 15 deletions include/tchecker/zg/zone_container.hh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -284,6 +284,22 @@ std::shared_ptr<zone_container_t<T>> logical_and_container(zone_container_t<T> &
return result;

}

template<typename T>
std::shared_ptr<zone_container_t<T>> logical_and_container(std::vector<std::shared_ptr<zone_container_t<T>>> & lo_container,
std::shared_ptr<T> (*factory)(tchecker::clock_id_t))
{
assert(!lo_container.empty());

auto iter = lo_container.begin();
auto result = std::make_shared<zone_container_t<T>>(**iter);
iter++;
for( ; iter < lo_container.end(); iter++) {
result = logical_and_container<T>(*result, **iter, factory);
}
return result;
}

/*
\brief a matrix of container for all subtypes of zone
*/
Expand All @@ -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<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<std::shared_ptr<zone_container_t<T>>>(row_size * column_size)) {
zone_matrix_t<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<std::shared_ptr<zone_container_t<T>>>(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<zone_container_t<T>>(dim);
}
};
Expand All @@ -314,34 +330,34 @@ public:
\return pointer to the element
*/
std::shared_ptr<zone_container_t<T>> 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<std::vector<std::shared_ptr<zone_container_t<T>>>> get_row(size_t row)
{
auto result = std::make_shared<std::vector<std::shared_ptr<zone_container_t<T>>>>();
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;
Expand All @@ -350,15 +366,15 @@ public:
std::shared_ptr<std::vector<std::shared_ptr<zone_container_t<T>>>> get_column(size_t column)
{
auto result = std::make_shared<std::vector<std::shared_ptr<zone_container_t<T>>>>();
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;
}

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);
Expand All @@ -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<std::shared_ptr<zone_container_t<T>>> _matrix;

};
Expand Down
5 changes: 3 additions & 2 deletions src/strong-timed-bisim/search_contradiction.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,9 @@ std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual

}

std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> find_contradiction(tchecker::zg::zone_t const & zone, std::vector<tchecker::vcg::vcg_t::sst_t *> & trans,
std::vector<std::shared_ptr<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>> & vcs, tchecker::clock_id_t no_of_virt_clks)
std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
find_contradiction(tchecker::zg::zone_t const & zone, std::vector<tchecker::vcg::vcg_t::sst_t *> & trans,
std::vector<std::shared_ptr<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>> & vcs, tchecker::clock_id_t no_of_virt_clks)
{

assert(0 != trans.size());
Expand Down
41 changes: 37 additions & 4 deletions src/strong-timed-bisim/virtual_clock_algorithm.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<tchecker::vcg::vcg_t::sst_t *> & trans_A, std::vector<tchecker::vcg::vcg_t::sst_t *> & trans_B,
tchecker::zone_matrix_t<tchecker::virtual_constraint::virtual_constraint_t> & found_cont,
std::vector< std::vector<bool> > 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<bool> cur) { assert(cur.size() == found_cont.get_no_of_columns()); } );

tchecker::zone_matrix_t<tchecker::virtual_constraint::virtual_constraint_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<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::zone_t const & zone_A, tchecker::zg::zone_t const & zone_B,
std::vector<tchecker::vcg::vcg_t::sst_t *> & trans_A, std::vector<tchecker::vcg::vcg_t::sst_t *> & trans_B,
Expand Down Expand Up @@ -439,7 +472,7 @@ Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::zone_t const & zone_A,
}

tchecker::zone_matrix_t<tchecker::virtual_constraint::virtual_constraint_t> found_cont{trans_A.size(), trans_B.size(), _A->get_no_of_virtual_clocks() + 1};
std::vector<bool> finished(trans_A.size() * trans_B.size(), false);
std::vector<std::vector<bool>> finished(trans_A.size(), std::vector<bool>(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.
Expand All @@ -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]);
Expand All @@ -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();
Expand All @@ -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<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(_A->get_no_of_virtual_clocks() + 1);

Expand Down

0 comments on commit f5dac3a

Please sign in to comment.