aligning code to the TR

include/tchecker/dbm/dbm.hh

@@ -592,7 +592,7 @@ enum tchecker::dbm::status_t intersection(tchecker::dbm::db_t * dbm, tchecker::d
  \return the dbm with reverted resets (same dim as orig_zone)
  \note the returned dbm is allocated on the heap. You have to free it!
  */
-tchecker::dbm::db_t * revert_multiple_reset(const tchecker::dbm::db_t * orig_zone,
+enum tchecker::dbm::status_t revert_multiple_reset(tchecker::dbm::db_t *result, const tchecker::dbm::db_t * orig_zone,
                                             tchecker::clock_id_t dim, tchecker::dbm::db_t * zone_split,
                                             tchecker::clock_reset_container_t reset);
 

include/tchecker/utils/zone_container.hh

@@ -140,7 +140,7 @@ public:
   void remove_empty()
   {
     for(auto iter = this->begin(); iter < this->end(); iter++) {
-      if(iter->empty()) {
+      if((*iter)->is_empty()) {
         _storage->erase(iter);
       }
     }
@@ -201,6 +201,8 @@ public:
   void compress()
   {
 
+    this->remove_empty();
+
     std::shared_ptr<std::vector<std::shared_ptr<T>>> result = _storage;
 
     bool reduced;

include/tchecker/vcg/revert_transitions.hh

@@ -34,11 +34,12 @@ revert_action_trans(const tchecker::zg::zone_t & zone,
 /*!
  \brief revert-epsilon-trans function (see the TR of Lieb et al.)
  \param zone : the original zone
+ \param zone_eps : the original target zone
  \param phi_split : the sub vc of the target
  \return a shared pointer to the resulting virtual constraint
  */
 std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>
-revert_epsilon_trans(const tchecker::zg::zone_t & zone, const tchecker::virtual_constraint::virtual_constraint_t & phi_split);
+revert_epsilon_trans(const tchecker::zg::zone_t & zone, const tchecker::zg::zone_t & zone_eps, const tchecker::virtual_constraint::virtual_constraint_t & phi_split);
 
 } // end of namespace vcg
 

include/tchecker/vcg/virtual_constraint.hh

@@ -60,16 +60,6 @@ public:
    */
   clock_constraint_container_t get_vc(tchecker::clock_id_t no_of_orig_clocks, bool system_clocks) const;
 
-  /*!
-   \brief returns the negated version of this clock constraint
-   \return let result be the return value.
-   *  forall u with u model this and for all vc in result u does not model vc
-   *  forall u with u does not model this exists a vc in result such that u models vc
-   *  (for u in ({\chi_0, ..., \chi_{|C_A| + | C_B| - 1}} \rightarrow T))
-   \note the result can easily become very large. Try to avoid this method and use neg_logic_and instead.
-   */
-  std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> neg() const;
-
   /*
    \brief returns the (not this and other)
    \param result : the pointer in which the result will be stored. Has to be allocated!
@@ -110,6 +100,12 @@ public:
   void logic_and(std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> result,
                  std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> const container) const;
 
+ /*
+  \brief returns, whether there exists any clock valuation that fulfills this
+  \return false, if no clock valuation exists that fulfills this
+  */
+  bool is_fulfillable() {return !this->is_empty();}
+
 private:
 
   std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> neg_helper(tchecker::dbm::db_t *upper_bounds) const;
@@ -158,7 +154,7 @@ std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> combine(tcheck
  \param a vector of container of zones
  \return a container of zones
  */
-std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> contained_in_all(std::vector<std::shared_ptr<zone_container_t<virtual_constraint_t>>> & zones, tchecker::clock_id_t no_of_virtual_clocks);
+std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> contained_in_all(std::vector<std::shared_ptr<zone_container_t<virtual_constraint_t>>> & vc, tchecker::clock_id_t no_of_virtual_clocks);
 
 
 } // end of namespace virtual_constraint

src/dbm/dbm.cc

@@ -523,6 +523,7 @@ enum tchecker::dbm::status_t intersection(tchecker::dbm::db_t * dbm, tchecker::d
       DBM(i, j) = tchecker::dbm::min(DBM1(i, j), DBM2(i, j));
 
   return tchecker::dbm::tighten(dbm, dim);
+
 }
 
 // used for assertion only
@@ -547,7 +548,7 @@ bool split_is_subset_of_R_orig(const tchecker::dbm::db_t * orig_zone,
     tchecker::dbm::output_matrix(std::cout, orig_zone, dim);
 
     std::cout << __FILE__ << ": " << __LINE__ << ": zone_split:" << std::endl;
-    tchecker::dbm::output_matrix(std::cout, orig_zone, dim);
+    tchecker::dbm::output_matrix(std::cout, zone_split, dim);
 
 
     std::cout << __FILE__ << ": " << __LINE__ << ": resets:" << std::endl;
@@ -566,7 +567,7 @@ bool split_is_subset_of_R_orig(const tchecker::dbm::db_t * orig_zone,
 
 }
 
-tchecker::dbm::db_t * revert_multiple_reset(const tchecker::dbm::db_t * orig_zone,
+enum tchecker::dbm::status_t revert_multiple_reset(tchecker::dbm::db_t *result, const tchecker::dbm::db_t * orig_zone,
                                             tchecker::clock_id_t dim, tchecker::dbm::db_t * zone_split,
                                             tchecker::clock_reset_container_t reset)
 {
@@ -582,10 +583,9 @@ tchecker::dbm::db_t * revert_multiple_reset(const tchecker::dbm::db_t * orig_zon
   assert(split_is_subset_of_R_orig(orig_zone, dim, zone_split, reset));
 
   if(reset.empty()) {
-    // place the dbm to return at the heap s.t. it is not destroyed during the returns
-    tchecker::dbm::db_t * result = (tchecker::dbm::db_t *)malloc(dim*dim*sizeof(tchecker::dbm::db_t));
     tchecker::dbm::copy(result, zone_split, dim);
-    return result;
+    tchecker::dbm::tighten(result, dim);
+    return (is_empty_0(result, dim) ? tchecker::dbm::EMPTY : tchecker::dbm::NON_EMPTY);
   }
 
   tchecker::dbm::db_t zone_clone[dim*dim];
@@ -594,19 +594,23 @@ tchecker::dbm::db_t * revert_multiple_reset(const tchecker::dbm::db_t * orig_zon
   tchecker::clock_reset_t cur = reset.back();
   reset.pop_back();
 
-  if(cur.right_id() != tchecker::REFCLOCK_ID || cur.value() != 0) {
+  if(cur.left_id() == tchecker::REFCLOCK_ID || cur.right_id() != tchecker::REFCLOCK_ID || cur.value() != 0) {
     throw std::runtime_error("when checking for timed bisim, only resets to value zero are allowed");
   }
 
-  tchecker::dbm::reset(zone_clone, dim, reset);
+  tchecker::dbm::reset_to_value(zone_clone, dim, cur.left_id() + 1, cur.value());
 
-  tchecker::dbm::free_clock(zone_split, dim, cur);
+  revert_multiple_reset(result, zone_clone, dim, zone_split, reset);
 
-  tchecker::dbm::db_t new_split[dim*dim];
+  tchecker::dbm::free_clock(result, dim, cur.left_id() + 1);
 
-  intersection(new_split, zone_clone, zone_split, dim);
+  enum tchecker::dbm::status_t ret_val = intersection(result, result, orig_zone, dim);
+
+  if(tchecker::dbm::EMPTY != ret_val) {
+    assert(tchecker::dbm::is_tight(result, dim));
+  }
 
-  return revert_multiple_reset(orig_zone, dim, new_split, reset);
+  return ret_val;
 
 }
 

src/strong-timed-bisim/virtual_clock_algorithm.cc

@@ -255,7 +255,8 @@ Lieb_et_al::check_for_virt_bisim(tchecker::zg::const_state_sptr_t symb_state_fir
     // now, we calculate the problematic virtual constraints by using the revert-epsilon function and adding it to lo_not_simulatable
 
     for(auto iter = result_epsilon->begin(); iter < result_epsilon->end(); iter++) {
-      lo_not_simulatable->append_zone(tchecker::vcg::revert_epsilon_trans(A_normed->zone(), **iter));
+      lo_not_simulatable->append_zone(tchecker::vcg::revert_epsilon_trans(A_normed->zone(), A_epsilon->zone(), **iter));
+      lo_not_simulatable->append_zone(tchecker::vcg::revert_epsilon_trans(B_normed->zone(), B_epsilon->zone(), **iter));
     }
 
   }
@@ -304,11 +305,17 @@ Lieb_et_al::check_for_virt_bisim(tchecker::zg::const_state_sptr_t symb_state_fir
       = tchecker::vcg::revert_sync(A_clone->zone_ptr()->dbm(), B_clone->zone_ptr()->dbm(), A_clone->zone_ptr()->dim(), B_clone->zone_ptr()->dim(),
                     _A->get_no_of_original_clocks(), _B->get_no_of_original_clocks(),
                     **iter);
-    inter.append_zone(sync_reverted.first);
-    inter.append_zone(sync_reverted.second);
 
-    assert(is_phi_subset_of_a_zone(symb_state_first->zone().dbm(), symb_state_first->zone().dim(), _A->get_no_of_virtual_clocks(), *(sync_reverted.first)));
-    assert(is_phi_subset_of_a_zone(symb_state_second->zone().dbm(), symb_state_second->zone().dim(), _B->get_no_of_virtual_clocks(), *(sync_reverted.second)));
+    if(sync_reverted.first->is_fulfillable()) {
+      inter.append_zone(sync_reverted.first);
+      assert(is_phi_subset_of_a_zone(symb_state_first->zone().dbm(), symb_state_first->zone().dim(), _A->get_no_of_virtual_clocks(), *(sync_reverted.first)));
+    }
+
+    if(sync_reverted.second->is_fulfillable()) {
+      inter.append_zone(sync_reverted.second);
+      assert(is_phi_subset_of_a_zone(symb_state_second->zone().dbm(), symb_state_second->zone().dim(), _B->get_no_of_virtual_clocks(), *(sync_reverted.second)));
+    }
+
   }
 
   inter.compress();

src/vcg/revert_transitions.cc

@@ -75,7 +75,7 @@ revert_action_trans(const tchecker::zg::zone_t & zone,
   // copy the reset container since revert_multiple_reset will change it
   tchecker::clock_reset_container_t reset_copy(reset);
 
-  // According to the implementation of revert-action-trans, described in Lieb et al., we first have to calculate R(zone && g).
+  // According to the implementation of revert-action-trans, described in Lieb et al., we first have to calculate R(zone && g) && phi_split.
   tchecker::dbm::db_t d_land_g[zone.dim()*zone.dim()];
   zone.to_dbm(d_land_g);
 
@@ -98,36 +98,33 @@ revert_action_trans(const tchecker::zg::zone_t & zone,
   assert(tchecker::dbm::is_tight(r_d_land_g_land_phi, zone.dim()));
   assert(tchecker::dbm::is_consistent(r_d_land_g_land_phi, zone.dim()));
 
-  tchecker::dbm::db_t *reverted = tchecker::dbm::revert_multiple_reset(d_land_g, zone.dim(), r_d_land_g_land_phi, reset_copy);
+  tchecker::dbm::db_t *reverted = (tchecker::dbm::db_t *)malloc(zone.dim()*zone.dim()*sizeof(tchecker::dbm::db_t));
+
+  tchecker::dbm::revert_multiple_reset(reverted, d_land_g, zone.dim(), r_d_land_g_land_phi, reset_copy);
 
   std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> virt_mult_reset 
       = tchecker::virtual_constraint::factory(reverted, zone.dim(), phi_split.get_no_of_virt_clocks());
 
-
-  tchecker::dbm::db_t zone_clone[zone.dim()*zone.dim()];
-  zone.to_dbm(zone_clone);
-
-  tchecker::dbm::constrain(zone_clone, zone.dim(), virt_mult_reset->get_vc(zone.dim() - phi_split.dim(), true));
-
-  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> result
-      = tchecker::virtual_constraint::factory(zone_clone, zone.dim(), phi_split.get_no_of_virt_clocks());
-
-  //std::cout << __FILE__ << ": " << __LINE__ << ": return from revert_action_trans" << std::endl;
-
-  return result;
+  return virt_mult_reset;
 }
 
 std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>
-revert_epsilon_trans(const tchecker::zg::zone_t & zone, const tchecker::virtual_constraint::virtual_constraint_t & phi_split)
+revert_epsilon_trans(const tchecker::zg::zone_t & zone, const tchecker::zg::zone_t & zone_eps, const tchecker::virtual_constraint::virtual_constraint_t & phi_split)
 {
 
-  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> phi_copy = factory(phi_split);
+  std::shared_ptr<tchecker::zg::zone_t> zone_eps_copy = tchecker::zg::factory(zone_eps);
+
+  if(tchecker::dbm::EMPTY == tchecker::dbm::constrain(zone_eps_copy->dbm(), zone_eps_copy->dim(), phi_split.get_vc(zone_eps_copy->dim() - phi_split.dim(), true))) {
+    tchecker::dbm::tighten(zone_eps_copy->dbm(), zone_eps_copy->dim());
+    std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> result = tchecker::virtual_constraint::factory(zone_eps_copy->dbm(), zone_eps_copy->dim(), phi_split.dim() - 1);
+    return result;
+  }
 
-  tchecker::dbm::open_down(phi_copy->dbm(), phi_copy->dim());
+  tchecker::dbm::open_down(zone_eps_copy->dbm(), zone_eps_copy->dim());
 
   std::shared_ptr<tchecker::zg::zone_t> zone_copy = tchecker::zg::factory(zone);
 
-  tchecker::dbm::constrain(zone_copy->dbm(), zone_copy->dim(), phi_copy->get_vc(zone_copy->dim() - phi_copy->dim(), true));
+  intersection(zone_copy->dbm(), zone_copy->dbm(), zone_eps_copy->dbm(), zone_eps_copy->dim());
 
   std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> result
     = tchecker::virtual_constraint::factory(zone_copy, phi_split.get_no_of_virt_clocks());

src/vcg/sync.cc

@@ -92,7 +92,18 @@ bool is_phi_subset_of_a_zone(const tchecker::dbm::db_t *dbm, tchecker::clock_id_
 {
   std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> phi = tchecker::virtual_constraint::factory(dbm, dim, dim - no_of_orig_clocks - 1);
 
-  return tchecker::dbm::is_le(phi_e.dbm(), phi->dbm(), phi_e.dim());
+  if(!tchecker::dbm::is_le(phi_e.dbm(), phi->dbm(), phi_e.dim())) {
+    std::cout << __FILE__ << ": " << __LINE__ << ": phi of zone:" << std::endl;
+    tchecker::dbm::output_matrix(std::cout, phi->dbm(), phi->dim());
+
+    std::cout << __FILE__ << ": " << __LINE__ << ": phi given:" << std::endl;
+    tchecker::dbm::output_matrix(std::cout, phi_e.dbm(), phi_e.dim());
+
+    return false;
+
+  }
+
+  return true;
 }
 
 void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2,
@@ -182,7 +193,7 @@ revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2,
 
   sync(dbm1_synced, dbm2_synced, dim1, dim2, no_of_orig_clocks_1, no_of_orig_clocks_2, orig_reset_set_A, orig_reset_set_B);
 
-  assert(is_phi_subset_of_a_zone(dbm1_synced, dim1, no_of_orig_clocks_1, phi_e) || is_phi_subset_of_a_zone(dbm2_synced, dim2, no_of_orig_clocks_2, phi_e));
+  assert(is_phi_subset_of_a_zone(dbm1_synced, dim1, no_of_orig_clocks_1, phi_e) && is_phi_subset_of_a_zone(dbm2_synced, dim2, no_of_orig_clocks_2, phi_e));
 
   if(tchecker::dbm::status_t::EMPTY == tchecker::dbm::constrain(dbm1_synced, dim1, phi_e.get_vc(no_of_orig_clocks_1, true))) {
     throw std::runtime_error("problems in _A while reverting the sync"); // should NEVER occur
@@ -192,14 +203,18 @@ revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2,
     throw std::runtime_error("problems in _B while reverting the sync"); // should NEVER occur
   }
 
-  tchecker::dbm::db_t * multiple_reset = revert_multiple_reset(dbm1, dim1, dbm1_synced, virt_reset_set_A);
+  tchecker::dbm::db_t *multiple_reset = (tchecker::dbm::db_t *)malloc(dim1*dim1*sizeof(tchecker::dbm::db_t));
+
+  enum tchecker::dbm::status_t stat_1 = revert_multiple_reset(multiple_reset, dbm1, dim1, dbm1_synced, virt_reset_set_A);
 
   std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> first
     = tchecker::virtual_constraint::factory(multiple_reset, dim1, no_of_orig_clocks_1 + no_of_orig_clocks_2);
 
   free(multiple_reset);
 
-  multiple_reset = revert_multiple_reset(dbm2, dim2, dbm2_synced, virt_reset_set_B);
+  multiple_reset = (tchecker::dbm::db_t *)malloc(dim2*dim2*sizeof(tchecker::dbm::db_t));
+
+  enum tchecker::dbm::status_t stat_2 = revert_multiple_reset(multiple_reset, dbm2, dim2, dbm2_synced, virt_reset_set_B);
 
   std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> second
     = tchecker::virtual_constraint::factory(multiple_reset, dim2, no_of_orig_clocks_1 + no_of_orig_clocks_2);
@@ -213,8 +228,17 @@ revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2,
   virt_reset_set_A.clear();
   virt_reset_set_B.clear();
 
-  assert(is_phi_subset_of_a_zone(dbm1, dim1, no_of_orig_clocks_1, *first));
-  assert(is_phi_subset_of_a_zone(dbm2, dim2, no_of_orig_clocks_2, *second));
+  if (tchecker::dbm::EMPTY == stat_1) {
+    tchecker::dbm::empty(first->dbm(), first->dim());
+  } else {
+    assert(is_phi_subset_of_a_zone(dbm1, dim1, no_of_orig_clocks_1, *first));
+  }
+
+  if (tchecker::dbm::EMPTY == stat_2) {
+    tchecker::dbm::empty(second->dbm(), second->dim());
+  } else {
+    assert(is_phi_subset_of_a_zone(dbm2, dim2, no_of_orig_clocks_2, *second));
+  }
 
   return std::make_pair(first, second);
 }

src/vcg/virtual_constraint.cc

@@ -84,14 +84,9 @@ std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> virtual_constr
     }
   }
 
-  return result;
-}
+  result->compress();
 
-std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> virtual_constraint_t::neg() const
-{
-  tchecker::dbm::db_t univ[this->dim()*this->dim()];
-  tchecker::dbm::universal(univ, this->dim());
-  return neg_helper(univ);
+  return result;
 }
 
 clock_constraint_container_t virtual_constraint_t::get_vc(tchecker::clock_id_t no_of_orig_clocks, bool system_clocks) const
@@ -256,6 +251,8 @@ std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> combine(tcheck
 
   }
 
+  result->compress();
+
   return result;
 }
 
@@ -273,27 +270,28 @@ bool all_elements_are_stronger_than(std::shared_ptr<zone_container_t<virtual_con
   return result;
 }
 
-std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> contained_in_all(std::vector<std::shared_ptr<zone_container_t<virtual_constraint_t>>> & zones, tchecker::clock_id_t no_of_virtual_clocks)
+std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> contained_in_all(std::vector<std::shared_ptr<zone_container_t<virtual_constraint_t>>> & vc, tchecker::clock_id_t no_of_virtual_clocks)
 {
 
   assert(
-    std::all_of(zones.begin(), zones.end(),
-                [no_of_virtual_clocks](std::shared_ptr<zone_container_t<virtual_constraint_t>> & lo_zones){return no_of_virtual_clocks + 1 == lo_zones->dim();} // cppcheck-suppress [assertWithSideEffect]
+    std::all_of(vc.begin(), vc.end(),
+                [no_of_virtual_clocks](std::shared_ptr<zone_container_t<virtual_constraint_t>> & lo_vc){return no_of_virtual_clocks + 1 == lo_vc->dim();} // cppcheck-suppress [assertWithSideEffect]
     )
   );
 
-  if (zones.empty()) {
+  if (vc.empty()) {
     return std::make_shared<tchecker::zone_container_t<virtual_constraint_t>>(no_of_virtual_clocks + 1);
   }
 
-  if (1 == zones.size()) {
-    return (zones[0]);
+  if (1 == vc.size()) {
+    (vc[0])->compress();
+    return vc[0];
   }
 
-  std::shared_ptr<zone_container_t<virtual_constraint_t>> cur = zones.back();
-  zones.pop_back();
+  std::shared_ptr<zone_container_t<virtual_constraint_t>> cur = vc.back();
+  vc.pop_back();
 
-  std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> inter = contained_in_all(zones, no_of_virtual_clocks);
+  std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> inter = contained_in_all(vc, no_of_virtual_clocks);
 
   std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> result = std::make_shared<zone_container_t<virtual_constraint_t>>(no_of_virtual_clocks + 1);
 
@@ -320,6 +318,8 @@ std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> contained_in_a
 
   assert(all_elements_are_stronger_than(cur, result, no_of_virtual_clocks));
 
+  result->compress();
+
   return result;
 }