improved non-deterministic

include/tchecker/zg/zone_container.hh

@@ -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
  */
@@ -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);
     }
   };
@@ -314,23 +330,23 @@ 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
@@ -341,7 +357,7 @@ public:
   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;
@@ -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);
@@ -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;
 
 };

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<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()); } );
+
+  // 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<std::shared_ptr<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>> usable 
+      = std::vector<std::shared_ptr<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>>();
+
+    // 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<tchecker::virtual_constraint::virtual_constraint_t>(
+                          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<std::shared_ptr<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>> usable 
+      = std::vector<std::shared_ptr<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>>();
+    // 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<tchecker::virtual_constraint::virtual_constraint_t>(
+                          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<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,
@@ -439,7 +518,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.
@@ -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<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(_A->get_no_of_virtual_clocks() + 1);