Wip (#4)

* wip

* aligning to TR

* improved readability and counting each alternating seq only once

* updated doc

* wip

examples/Lieb_et_al_6.sh

@@ -0,0 +1,8 @@
+#!/bin/bash
+
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+cat "$(dirname $0)/strong_timed_bisim_system_tests/Lieb_et_al/A6.txt"
+

examples/strong_timed_bisim_system_tests/Lieb_et_al/A6.txt

@@ -0,0 +1,26 @@
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+system:Lieb_et_al_A6
+
+clock:1:x
+
+event:a
+event:b
+event:c
+
+process:P
+location:P:A{initial:}
+location:P:B{invariant: x<2}
+location:P:C{}
+location:P:BPrime{invariant: x<2}
+location:P:CPrime{}
+
+edge:P:A:B:a{provided: x >= 1 : do: x=0}
+edge:P:B:C:b{}
+edge:P:C:A:c{provided: x>3 : do: x=0}
+
+edge:P:A:BPrime:a{provided: x <= 1 : do: x=0}
+edge:P:BPrime:CPrime:b{}
+edge:P:CPrime:A:c{provided: x>3 : do: x=0}

include/tchecker/dbm/dbm.hh

@@ -586,15 +586,15 @@ enum tchecker::dbm::status_t intersection(tchecker::dbm::db_t * dbm, tchecker::d
 
 /*!
  \brief revert-multiple-reset function (see the TR of Lieb et al.)
- \param orig_zone the previous zone
+ \param result : where the result will be stored (must be allocated)
+ \param orig_zone : the previous zone
  \param zone_split : the split of reset(orig_zone)
  \param reset : the used reset set
- \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!
+ \return void
  */
 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);
+                                                   tchecker::clock_id_t dim, tchecker::dbm::db_t * zone_split,
+                                                   tchecker::clock_reset_container_t reset);
 
 /*!
  \brief ExtraM extrapolation

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

@@ -74,14 +74,12 @@ private:
    \param symbolic_trans_first : the transition with which we reached the first symbolic state
    \param symb_state_second : the symbolic state that belongs to the second vcg
    \param symbolic_trans_second : the transition with which we reached the second symbolic state
-   \param last_was_epsilon : whether the last transition was a delay transition
    \return a list of virtual constraints that are not bisimilar
    */
   std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
   check_for_virt_bisim(tchecker::zg::const_state_sptr_t symb_state_first, tchecker::zg::transition_sptr_t symbolic_trans_first,
                        tchecker::zg::const_state_sptr_t symb_state_second, tchecker::zg::transition_sptr_t symbolic_trans_second,
-                       std::unordered_set<std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t>, custom_hash, custom_equal> & visited,
-                       bool last_was_epsilon);
+                       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/utils/zone_container.hh

@@ -196,6 +196,7 @@ public:
            - zc_prev._dim = zc_after._dim
            - for all zone_prev in zc_prev : for all u in zone_prev : exists zone_after in zc_after : u in zone_after
            - for all zone_after in zc_after : for all u in zone_after : exists zone_prev in zc_prev : u in zone_prev
+   \note see chapter 7.6 of Rokicki "Representing and modeling digital circuits" (PhD thesis)
    */
 
   void compress()

include/tchecker/vcg/sync.hh

@@ -59,8 +59,9 @@ bool are_dbm_synced(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2,
  \param dbm1 : a dbm
  \param dbm2 : a dbm
  \param dim : dimension of dbm1 and dbm2
- \param lowest_virt_clk_id : the clk id of chi_0
  \param  no_of_orig_clocks_1 : the number of orig clocks in the first TA
+ \param  no_of_orig_clocks_1 : the number of orig clocks in the first TA
+ \param phi_e : the vc to revert
  \pre dbm1 and dbm2 are not nullptr (checked by assertion)
  dbm, dbm1 and dbm2 are dim*dim arrays of difference bounds
  dbm1 and dbm2 are consistent (checked by assertion)

src/dbm/dbm.cc

@@ -1349,11 +1349,15 @@ enum tchecker::dbm::union_convex_t convex_union(tchecker::dbm::db_t *result, tch
   }
 
   if(dbm2_tight.empty()) {
+    assert(tchecker::dbm::is_consistent(result, dim));
+    assert(tchecker::dbm::is_tight(result, dim));
     return tchecker::dbm::union_convex_t::UNION_IS_CONVEX;
   }
 
   if (dbm1_tight.empty()) {
     tchecker::dbm::copy(result, dbm2, dim);
+    assert(tchecker::dbm::is_consistent(result, dim));
+    assert(tchecker::dbm::is_tight(result, dim));
     return tchecker::dbm::union_convex_t::UNION_IS_CONVEX;
   }
 
@@ -1369,6 +1373,8 @@ enum tchecker::dbm::union_convex_t convex_union(tchecker::dbm::db_t *result, tch
     }
   }
 
+  assert(tchecker::dbm::is_consistent(result, dim));
+  assert(tchecker::dbm::is_tight(result, dim));
   return tchecker::dbm::union_convex_t::UNION_IS_CONVEX;
 
 }