another alignment

include/tchecker/strong-timed-bisim/search_contradiction.hh

@@ -0,0 +1,34 @@
+/*
+ * This file is a part of the TChecker project.
+ *
+ * See files AUTHORS and LICENSE for copyright details.
+ *
+ */
+
+#ifndef TCHECKER_STRONG_TIMED_BISIM_SEARCH_CONTRADICTION_HH
+#define TCHECKER_STRONG_TIMED_BISIM_SEARCH_CONTRADICTION_HH
+
+#include "tchecker/vcg/virtual_constraint.hh"
+
+namespace tchecker {
+
+namespace strong_timed_bisim {
+
+/*!
+ \brief finds a contradiction to timed bisimulation
+ \param zone_A : the zone of the first symbolic state
+ \param zone_B : the zone of the second symbolic state
+ \param trans_A : the outgoing transitions of the first symbolic state
+ \param trans_B : the outgoing transitions of the second symbolic state
+ \param found_cont : the matrix where the already found contradictions of the outgoing transitions are stored
+ */
+
+std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
+search_contradiction(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, tchecker::clock_id_t no_of_virt_clks);
+
+} // end of namespace strong_timed_bisim
+
+} // end of namespace tchecker
+#endif

include/tchecker/strong-timed-bisim/virtual_clock_algorithm.hh

@@ -92,23 +92,14 @@ private:
                        tchecker::zg::const_state_sptr_t B_state, tchecker::zg::transition_sptr_t B_trans,
                        std::unordered_set<std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t>, custom_hash, custom_equal> & visited);
 
-  /*!
-   \brief helping function for check-for-outgoing-transitions. Is called if the other side has no transitions.
-   \param zone : the zone of the starting symbolic states that has some transitions.
-   \param trans : the corresponding transitions
-   \return the virtual constraints that represent the part of zone that has any of the given outgoing transitions.
-   */
-  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
-  check_for_outgoing_transitions_single_empty(tchecker::zg::zone_t const & zone, std::vector<tchecker::vcg::vcg_t::sst_t *> & trans);
-
   /*!
    \brief : removes found contradictions from a zone
    \param zone : the zone to constraint
    \param contradictions : the virtual constraints that shall be removed from zone
-   \return zone && (! && of all elements in contradictions)
+   \return virtual_constraint of zone && (! && of all elements in contradictions)
    */
-  std::shared_ptr<tchecker::zone_container_t<tchecker::zg::zone_t>>
-  extract_zone_without_contradictions(tchecker::zg::zone_t const & zone, std::shared_ptr<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> contradictions);
+  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
+  extract_vc_without_contradictions(tchecker::zg::zone_t const & zone, std::shared_ptr<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> contradictions);
 
   /*!
    \brief : takes two transitions and splits of the target zones. Returns a contradiction if one is found.
@@ -120,9 +111,10 @@ private:
    \return a contradiction if there is one. Otherwise an empty list of virtual constraints.
    */
   std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
-  check_splitted_transitions(std::shared_ptr<tchecker::zone_container_t<tchecker::zg::zone_t>> zones_A, tchecker::zg::transition_sptr_t trans_A, tchecker::zg::state_sptr_t state_A,
-                             std::shared_ptr<tchecker::zone_container_t<tchecker::zg::zone_t>> zones_B, tchecker::zg::transition_sptr_t trans_B, tchecker::zg::state_sptr_t state_B,
-                             std::unordered_set<std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t>, custom_hash, custom_equal> & visited);
+  check_target_pair(tchecker::zg::state_sptr_t target_state_A, tchecker::zg::transition_sptr_t trans_A,
+                    tchecker::zg::state_sptr_t target_state_B, tchecker::zg::transition_sptr_t trans_B,
+                    std::shared_ptr<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> already_found_contradictions,
+                    std::unordered_set<std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t>, custom_hash, custom_equal> & visited);
 
   /*!
    \brief check-for-outgoing-transitions-impl function of Lieb et al.

include/tchecker/vcg/virtual_constraint.hh

@@ -30,9 +30,8 @@ namespace virtual_constraint {
  \class virtual_constraint_t
  \brief Implementation of virtual constraints
  \note We model the virtual constraint as zone
- * using the virtual clocks, only. This is
- * fine since a zone always corresponds to a
- * clock constraint
+ * using the virtual clocks, only. Do not add
+ * any fields to this class (or change the factory)
  */
 
 class virtual_constraint_t : public tchecker::zg::zone_t {
@@ -150,19 +149,6 @@ std::shared_ptr<virtual_constraint_t> factory(const tchecker::dbm::db_t * dbm, t
  */
 std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> combine(tchecker::zone_container_t<virtual_constraint_t> & lo_vc, tchecker::clock_id_t no_of_virtual_clocks);
 
-/*!
- \brief find_contradiction operator (see the TR of Lieb et al.)
- \param zone_A : the base zone of all transitions of trans_A
- \param zone_B : the base zone of all transisions of trans_B
- \param trans_A : a reference to a vector of transitions
- \param trans_B : a reference to a vector of transitions
- \param vcs : a matrix of container of virtual constraints
- */
-std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> find_contradiction(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<virtual_constraint_t> & vcs);
-
-
 /*!
  \brief contained-in-all function (see the TR of Lieb et al.)
  \param a vector of container of virtual constraints

include/tchecker/zg/zone_container.hh

@@ -221,6 +221,13 @@ public:
 
   }
 
+  void print_zone_container(std::ostream & os)
+  {
+    for(auto cur : _storage) {
+      os << *cur << " ";
+    }
+  }
+
 private:
 
   std::shared_ptr<std::vector<std::shared_ptr<T>>> find_union_partner(std::vector<std::shared_ptr<T>> const cur)
@@ -251,6 +258,30 @@ private:
 
 };
 
+template<typename T>
+std::shared_ptr<zone_container_t<T>> logical_and_container(zone_container_t<T> & first, zone_container_t<T> & second,
+                                                           std::shared_ptr<T> (*factory)(tchecker::clock_id_t))
+{
+  assert(first.dim() == second.dim());
+
+  first.compress();
+  second.compress();
+  auto result = std::make_shared<zone_container_t<T>>(first.dim());
+
+  for(auto cur_first : first) {
+    assert(tchecker::dbm::is_tight(cur_first->dbm(), cur_first->dim()));
+    for(auto cur_second : second) {
+      assert(tchecker::dbm::is_tight(cur_second->dbm(), cur_second->dim()));
+      auto inter = factory(first.dim());
+      cur_first->logic_and(inter, *cur_second);
+      result->append_zone(inter);
+    }
+    result->compress();
+  }
+
+  return result;
+
+}
 /*
  \brief a matrix of container for all subtypes of zone
  */
@@ -262,36 +293,36 @@ public:
 
   /*!
    \brief Constructor
-   \param line_size : number of lines in matrix
+   \param row_size : number of rows in matrix
    \param column_size : number of columns in matrix
    \param dim : the dimension of the zones
    */
-  zone_matrix_t<T>(size_t line_size, size_t column_size, tchecker::clock_id_t dim) :
-    _dim(dim), _line_size(line_size), _column_size(column_size), _matrix(std::vector<std::shared_ptr<zone_container_t<T>>>(line_size * column_size)) {
+  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)) {
 
-    for(std::size_t i = 0; i < line_size*column_size; ++i) {
+    for(std::size_t i = 0; i < row_size*column_size; ++i) {
       _matrix[i] = std::make_shared<zone_container_t<T>>(dim);
     }
   };
 
   /*!
    \brief Getter for matrix element
-   \param line : line of the element
+   \param row : row of the element
    \param column : column of the element
    \return pointer to the element
   */
-  std::shared_ptr<zone_container_t<T>> get(size_t line, size_t column) {
-    assert(line < _line_size);
+  std::shared_ptr<zone_container_t<T>> get(size_t row, size_t column) {
+    assert(row < _row_size);
     assert(column < _column_size);
 
-    return _matrix[line*_column_size + column];
+    return _matrix[row*_column_size + column];
   }
 
   /*!
-   \brief Accessor for the line size
-   \return the line size
+   \brief Accessor for the row size
+   \return the row size
   */
-  size_t get_line_size() const { return _line_size; }
+  size_t get_row_size() const { return _row_size; }
 
   /*!
    \brief Accessor for the column size
@@ -305,29 +336,41 @@ public:
   */
   size_t get_dim() const { return _dim; }
 
-  std::shared_ptr<std::vector<std::shared_ptr<zone_container_t<T>>>>  get_line(size_t line)
+  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++) {
-      result->emplace_back(this->get(line, i));
+      result->emplace_back(this->get(row, i));
     }
     return result;
   }
 
   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_line_size(); i++) {
+    for(size_t i = 0; i < this->get_row_size(); 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) {
+      auto row = get_row(i);
+      for(auto cur : row) {
+        row->print_container(os);
+        os << "    ";
+      }
+      os << std::endl;
+    }
+  }
+
   private:
 
     const tchecker::clock_id_t _dim;
 
-    const size_t _line_size, _column_size;
+    const size_t _row_size, _column_size;
     std::vector<std::shared_ptr<zone_container_t<T>>> _matrix;
 
 };

src/strong-timed-bisim/CMakeLists.txt

@@ -6,4 +6,5 @@ set(STRONG_TIMED_BISIM_SRC
     ${CMAKE_CURRENT_SOURCE_DIR}/stats.cc
     ${CMAKE_CURRENT_SOURCE_DIR}/virtual_clock_algorithm.cc
     ${CMAKE_CURRENT_SOURCE_DIR}/system.cc
+    ${CMAKE_CURRENT_SOURCE_DIR}/search_contradiction.cc
     PARENT_SCOPE)

src/strong-timed-bisim/search_contradiction.cc

@@ -0,0 +1,94 @@
+/*
+ * This file is a part of the TChecker project.
+ *
+ * See files AUTHORS and LICENSE for copyright details.
+ *
+ */
+
+#include "tchecker/strong-timed-bisim/search_contradiction.hh"
+#include "tchecker/vcg/revert_transitions.hh"
+
+namespace tchecker {
+
+namespace strong_timed_bisim {
+
+std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> find_contradiction_create_fill_up(tchecker::zg::zone_t const & zone, tchecker::virtual_constraint::virtual_constraint_t & other_side,
+                                                                                                    std::shared_ptr<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> vcs)
+{
+
+  auto inter = tchecker::virtual_constraint::factory(zone, vcs->dim() - 1);
+  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> result = std::make_shared<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(vcs->dim());
+  other_side.neg_logic_and(result, *inter);
+
+  result->append_container(vcs);
+
+  result->compress();
+
+  return result;
+
+}
+
+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());
+  assert(vcs.size() == trans.size());
+
+  auto result = std::make_shared<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(no_of_virt_clks + 1);
+
+  auto to_add = tchecker::virtual_constraint::factory(zone, no_of_virt_clks);
+
+  result->append_zone(to_add);
+
+  for(unsigned int i = 0; i < vcs.size(); ++i) {
+    auto && [status, s, t] = *(trans[i]);
+    auto vc_s = tchecker::virtual_constraint::factory(s->zone(), no_of_virt_clks);
+    auto fill_up = find_contradiction_create_fill_up(zone, *vc_s, vcs[i]);
+
+    result = tchecker::logical_and_container<tchecker::virtual_constraint::virtual_constraint_t>(*result, *fill_up, [] (tchecker::clock_id_t dim) {return tchecker::virtual_constraint::factory(dim - 1);} );
+  }
+
+  result->compress();
+  result = tchecker::virtual_constraint::combine(*result, no_of_virt_clks);
+  result->compress();
+
+  return result;
+}
+
+std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
+search_contradiction(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, tchecker::clock_id_t no_of_virt_clks)
+{
+  auto contradiction = std::make_shared<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(no_of_virt_clks + 1);
+
+  for(size_t idx_A = 0; idx_A < trans_A.size(); idx_A++) {
+    auto && [status_A, s_A, t_A] = *(trans_A[idx_A]);
+    auto row = found_cont.get_row(idx_A);
+    auto found = find_contradiction(s_A->zone(), trans_B, *row, no_of_virt_clks);
+    for(auto cur : *found) {
+      contradiction->append_zone(tchecker::vcg::revert_action_trans(zone_A, t_A->guard_container(), t_A->reset_container(), t_A->tgt_invariant_container(), *cur));
+    }
+  }
+
+  for(size_t idx_B = 0; idx_B < trans_B.size(); idx_B++) {
+    auto && [status_B, s_B, t_B] = *(trans_B[idx_B]);
+    auto column = found_cont.get_column(idx_B);
+    auto found = find_contradiction(s_B->zone(), trans_A, *column, no_of_virt_clks);
+    for(auto cur : *found) {
+      contradiction->append_zone(tchecker::vcg::revert_action_trans(zone_B, t_B->guard_container(), t_B->reset_container(), t_B->tgt_invariant_container(), *cur));
+    }
+  }
+
+  contradiction->compress();
+  auto result = tchecker::virtual_constraint::combine(*contradiction, no_of_virt_clks);
+  result->compress();
+
+  return result;
+
+}
+
+} // end of namespace strong_timed_bisim
+
+} // end of namespace tchecker