Intermediate (#3)

very first working version

.github/workflows/build-and-test.yml

@@ -12,7 +12,7 @@ jobs:
         intsize: ["all:int16:memcheck", "all:int32:memcheck", "all:int64:memcheck"]
         compiler: ["gcc", "clang"]
     runs-on: ubuntu-latest
-    container: alzeha/echtzeitsysteme-tchecker-${{ matrix.compiler }}:v0.1
+    container: alzeha/echtzeitsysteme-tchecker-${{ matrix.compiler }}:latest
     env:
       CONFNAME: ${{ matrix.intsize }}
       INSTALL_DIR: "install"

CppCheckSuppressions.txt

@@ -4,16 +4,5 @@ nullPointer:*/tchecker/src/refzg/refzg.cc:[181, 176, 189, 190, 197, 203, 208]
 uninitdata:*/include/tchecker/utils/shared_objects.hh
 nullPointer:*/src/refzg/refzg.cc
 
-// TODO: fix the following
-rethrowNoCurrentException:*/include/tchecker/variables/variables.hh
-assertWithSideEffect:*/include/tchecker/variables/variables.hh
-funcArgOrderDifferent:*/src/clockbounds/solver.cc
-assertWithSideEffect:*/include/tchecker/waiting/waiting.hh
-uninitMemberVar:*/src/algorithms/covreach/stats.cc
-
-// TODO: decide whether to fix the following
-operatorEqVarError:*/include/tchecker/utils/shared_objects.hh
-missingMemberCopy:*/include/tchecker/utils/shared_objects.hh
-
 // the following is a known cppcheck bug
 internalAstError:*/include/tchecker/graph/directed_graph.hh

ci-scripts/Dockerfile

@@ -4,7 +4,7 @@ ARG CXX
 RUN apt update && \
     apt install -y \
     git cmake bison flex doxygen wget \
-    valgrind graphviz
+    valgrind graphviz cppcheck
 
 
 FROM base as gcc-image

examples/Lieb_et_al_1.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/A1.txt"
+

examples/Lieb_et_al_1_diff_invariant.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/A1_different_invariant.txt"
+

examples/Lieb_et_al_1_non_determ_bisim.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/A1_non_determ_bisim.txt"
+

examples/Lieb_et_al_2.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/A2.txt"
+

examples/Lieb_et_al_2_determ_split_bisim.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/A2_determ_split_bisim.txt"
+

examples/Lieb_et_al_2_determ_split_non_bisim.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/A2_determ_split_non_bisim.txt"
+

examples/Lieb_et_al_2_non_determ_bisim.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/A2_non_determ_bisim.txt"
+

examples/Lieb_et_al_3.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/A3.txt"
+

examples/Lieb_et_al_4.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/A4.txt"
+

examples/Lieb_et_al_5.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/A5.txt"
+

examples/count_to_inf.sh

@@ -0,0 +1 @@
+cat "$(dirname $0)/count_to_inf.txt"

examples/count_to_inf.txt

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

examples/easy-ad94-added-transition.sh

@@ -0,0 +1,9 @@
+#!/bin/bash
+
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+echo "# labels=green"
+
+cat "$(dirname $0)/strong_timed_bisim_system_tests/easy_ad94/easy_ad94_added_transition.txt"

examples/easy-ad94-different-guard.sh

@@ -0,0 +1,9 @@
+#!/bin/bash
+
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+echo "# labels=green"
+
+cat "$(dirname $0)/strong_timed_bisim_system_tests/easy_ad94/easy_ad94_different_guard.txt"

examples/easy-ad94.sh

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

examples/strong_timed_bisim_system_tests/Lieb_et_al/A1.txt

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

examples/strong_timed_bisim_system_tests/Lieb_et_al/A1_different_invariant.txt

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

examples/strong_timed_bisim_system_tests/Lieb_et_al/A1_non_determ_bisim.txt

@@ -0,0 +1,22 @@
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+system:Lieb_et_al_A1
+
+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:CPrime{}
+edge:P:A:B:a{provided: x<=0}
+edge:P:B:C:b{provided: x<=1}
+edge:P:B:CPrime:b{provided:x>1}
+edge:P:C:A:c{provided: x>3 : do: x=0}
+edge:P:CPrime:A:c{provided: x>3 : do: x=0}

examples/strong_timed_bisim_system_tests/Lieb_et_al/A2.txt

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

examples/strong_timed_bisim_system_tests/Lieb_et_al/A2_determ_split_bisim.txt

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

examples/strong_timed_bisim_system_tests/Lieb_et_al/A2_determ_split_non_bisim.txt

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

examples/strong_timed_bisim_system_tests/Lieb_et_al/A2_non_determ_bisim.txt

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

examples/strong_timed_bisim_system_tests/Lieb_et_al/A3.txt

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

examples/strong_timed_bisim_system_tests/Lieb_et_al/A4.txt

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

examples/strong_timed_bisim_system_tests/Lieb_et_al/A5.txt

@@ -0,0 +1,27 @@
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+system:Lieb_et_al_A1
+
+clock:1:x
+clock:1:y
+
+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{do: x=0}
+edge:P:B:C:b{do: y=0}
+edge:P:C:A:c{provided: y>3 : do: x=0;y=0}
+
+edge:P:A:BPrime:a{do: x=0;y=0}
+edge:P:BPrime:CPrime:b{}
+edge:P:CPrime:A:c{provided: y>3 : do: x=0;y=0}

examples/strong_timed_bisim_system_tests/easy_ad94/easy-ad94-different-guard.txt

@@ -0,0 +1,21 @@
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+system:easy_ad94_different_guard_fig10
+
+clock:1:x
+clock:1:y
+
+event:a
+event:b
+event:c
+event:d
+
+process:P
+location:P:l0{initial:}
+location:P:l1{}
+location:P:l2{}
+location:P:l3{labels: green}
+edge:P:l0:l1:a{do: x=0; y=0}
+edge:P:l1:l2:b{provided: y==2 && x<=2 }

examples/strong_timed_bisim_system_tests/easy_ad94/easy_ad94.txt

@@ -0,0 +1,21 @@
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+system:easy_ad94_fig10
+
+clock:1:x
+clock:1:y
+
+event:a
+event:b
+event:c
+event:d
+
+process:P
+location:P:l0{initial:}
+location:P:l1{}
+location:P:l2{}
+location:P:l3{labels: green}
+edge:P:l0:l1:a{do: x=0; y=0}
+edge:P:l1:l2:b{provided: y==1 && x<=2 }

examples/strong_timed_bisim_system_tests/easy_ad94/easy_ad94_added_transition.txt

@@ -0,0 +1,22 @@
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+system:easy_ad94_added_transition_fig10
+
+clock:1:x
+clock:1:y
+
+event:a
+event:b
+event:c
+event:d
+
+process:P
+location:P:l0{initial:}
+location:P:l1{}
+location:P:l2{}
+location:P:l3{labels: green}
+edge:P:l0:l1:a{do: x=0; y=0}
+edge:P:l1:l2:b{provided: y==1 && x<=2 }
+edge:P:l1:l2:c{ }

examples/strong_timed_bisim_system_tests/easy_ad94/easy_ad94_different_guard.txt

@@ -0,0 +1,21 @@
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+system:easy_ad94_different_guard_fig10
+
+clock:1:x
+clock:1:y
+
+event:a
+event:b
+event:c
+event:d
+
+process:P
+location:P:l0{initial:}
+location:P:l1{}
+location:P:l2{}
+location:P:l3{labels: green}
+edge:P:l0:l1:a{do: x=0; y=0}
+edge:P:l1:l2:b{provided: y==2 && x<=2 }

include/tchecker/dbm/dbm.hh

@@ -999,6 +999,29 @@ enum clock_position_t {
 enum tchecker::dbm::clock_position_t clock_position(tchecker::dbm::db_t const * dbm, tchecker::clock_id_t dim,
                                                     tchecker::clock_id_t x1, tchecker::clock_id_t x2);
 
+/*
+ \brief Return value of convex-union
+*/
+enum union_convex_t {
+  UNION_IS_CONVEX,      /*!< the union of two dbm can be represented as a dbm */
+  UNION_IS_NOT_CONVEX   /*!< the union of two dbm cannot be represented as a dbm */
+};
+
+/*!
+ \brief tries to union two dbms
+ \param result : where the result will be stored (must be allocated!)
+ \param dbm1 : a dbm
+ \param dbm2 : a dbm to be unioned with dbm1
+ \param dim : the dimension (must be the same for all dbm!)
+ \pre none of the dbm is nullptr (checked by assertion)
+ dbm1 and dbm1 are consistent and tight (checked by assertion)
+ dim >= 1 (checked by assertion)
+ \return UNION_IS_CONVEX if the union of dbm1 and dbm2 can be represented by a dbm. UNION_IS_NOT_CONVEX otherwise
+ \post if UNION_IS_CONVEX is returned, result contains the union.
+ \note This function implements the convex-union algorithm from the dissertation "Rokicki, Tomas Gerhard: Representing and modeling digital circuits, Stanford University, 1994"
+ */
+enum tchecker::dbm::union_convex_t convex_union(tchecker::dbm::db_t *result, tchecker::dbm::db_t const * dbm1, tchecker::dbm::db_t const * dbm2, tchecker::clock_id_t dim);
+
 } // end of namespace dbm
 
 } // end of namespace tchecker

include/tchecker/dbm/details/db_safe.hh

@@ -95,8 +95,13 @@ static_assert(tchecker::dbm::LE_ZERO != tchecker::dbm::LT_INFINITY, "");
  */
 inline tchecker::dbm::db_t db(enum tchecker::ineq_cmp_t cmp, tchecker::integer_t value)
 {
-  if ((value < tchecker::dbm::MIN_VALUE) || (value > tchecker::dbm::MAX_VALUE))
+  if (value == INF_VALUE && cmp == tchecker::LT)
+  {
+    return tchecker::dbm::LT_INFINITY;
+  }
+  if ((value < tchecker::dbm::MIN_VALUE) || (value > tchecker::dbm::MAX_VALUE)) {
     throw std::invalid_argument("value out of bounds");
+  }
   return db_t{cmp, value};
 }
 
@@ -151,6 +156,12 @@ inline int db_cmp(tchecker::dbm::db_t const & db1, tchecker::dbm::db_t const & d
   return db1.cmp - db2.cmp;
 }
 
+inline tchecker::dbm::db_t invert(tchecker::dbm::db_t const & to_invert)
+{
+  return tchecker::dbm::db(to_invert.cmp==tchecker::LE ? tchecker::LT : tchecker::LE, (-1)*to_invert.value);
+}
+
+
 /*!
  \brief Less-than operator on difference bounds
  \param db1 : a difference bound

include/tchecker/dbm/details/db_unsafe.hh

@@ -99,6 +99,11 @@ inline tchecker::dbm::db_t add(tchecker::dbm::db_t db, tchecker::integer_t value
   return (db + (value << 1));
 }
 
+inline tchecker::dbm::db_t invert(tchecker::dbm::db_t const & to_invert)
+{
+  return tchecker::dbm::db(to_invert.cmp==tchecker::LE ? tchecker::LT : tchecker::LE, to_invert.value);
+}
+
 /*!
  \note Standard comparison operators <, <=, ==, !=, >= and > on integers carry on difference bounds
  */

include/tchecker/extrapolation/extrapolation_factory.hh

@@ -34,7 +34,6 @@ enum extrapolation_type_t {
   EXTRA_M_LOCAL,        /*!< see tchecker::zg::local_extra_m_t */
   EXTRA_M_PLUS_GLOBAL,  /*!< see tchecker::zg::global_extra_m_plus_t */
   EXTRA_M_PLUS_LOCAL,   /*!< see tchecker::zg::local_extra_m_plus_t */
-  EXTRA_K_NORM          /* see tchecker::zg::k_norm */
 };
 
 /*!
@@ -69,8 +68,8 @@ namespace vcg {
 /*!
  \brief Zone extrapolation factory
  \param extrapolation_type : type of extrapolation
- \param orig_system_first : first system of timed processes
- \param orig_system_secpmd : second system of timed processes
+ \param system_first : first system of timed processes
+ \param system_second : second system of timed processes
  \param first_not_second : true iff this vcg is the left hand side of the comparison
  \return a zone extrapolation of type extrapolation_type using clock bounds
  inferred from the systems, nullptr if clock bounds cannot be inferred from system (see
@@ -80,8 +79,8 @@ namespace vcg {
  */
 tchecker::zg::extrapolation_t * extrapolation_factory(
                   enum tchecker::zg::extrapolation_type_t type,
-                  std::shared_ptr<tchecker::ta::system_t const> const & orig_system_first,
-                  std::shared_ptr<tchecker::ta::system_t const> const & orig_system_second,
+                  std::shared_ptr<const tchecker::ta::system_t> system_first,
+                  std::shared_ptr<const tchecker::ta::system_t> system_second,
                   bool first_not_second);
 
 } // end of namespace vcg

include/tchecker/extrapolation/k_norm.hh

@@ -1,67 +0,0 @@
-/*
- * This file is a part of the TChecker project.
- *
- * See files AUTHORS and LICENSE for copyright details.
- *
- */
-
-#ifndef TCHECKER_ZG_EXTRAPOLATION_K_NORM_HH
-#define TCHECKER_ZG_EXTRAPOLATION_K_NORM_HH
-
-#include "tchecker/extrapolation/extrapolation.hh"
-#include "tchecker/extrapolation/global_lu_extrapolation.hh"
-
-namespace tchecker {
-
-namespace zg {
-
-/*!
- \class k_norm
- \brief K-Normalization for zone extrapolation
- */
-class k_norm final : public tchecker::zg::global_extra_lu_t {
-public:
-
-  /*!
-   \brief Constructor
-   \param clock_bounds : global LU clock bounds map
-   \note WARNING: we change the clock bounds, ignoring the const statement
-  */
-  k_norm(std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> const & clock_bounds);
-
-  /*!
-  \brief Destructor
-  */
-  virtual ~k_norm() = default;
-
-  using tchecker::zg::global_extra_lu_t::extrapolate;
-
-};
-
-} // end of namespace zg
-
-namespace vcg {
-
-class k_norm_virtual final : public tchecker::zg::global_extra_lu_t {
-public:
-  /*!
-   \brief Constructor
-   \param clock_bounds : global LU clock bounds map
-   \note WARNING: we change the clock bounds, ignoring the const statement
-  */
-  k_norm_virtual(std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> const & clock_bounds);
-
-  /*!
-  \brief Destructor
-  */
-  virtual ~k_norm_virtual() = default;
-
-  using tchecker::zg::global_extra_lu_t::extrapolate;
-
-};
-
-} // end of namespace vcg
-
-} // end of namespace tchecker
-
-#endif

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

@@ -8,7 +8,10 @@
 #ifndef TCHECKER_ALGORITHMS_COMPARE_STATS_HH
 #define TCHECKER_ALGORITHMS_COMPARE_STATS_HH
 
+#include <unordered_set>
+
 #include "tchecker/algorithms/stats.hh"
+#include "tchecker/zg/state.hh"
 
 /*!
  \file stats.hh
@@ -35,20 +38,13 @@ public:
    \brief Accessor
    \return A reference to the number of visited pair of states
   */
-  unsigned long visited_pair_of_states() const;
+  long visited_pair_of_states() const;
 
   /*!
-  \brief Accessor
-  \return Number of visited transitions
-  */
-  unsigned long visited_transitions() const;
-
-  /*!
-  \brief Accessor
-  \return The deepest path checked
-  */
-
-  unsigned long deepest_path() const;
+   \brief setter for the number of visited pair of states
+   \post visited_pair_of_states is set to the given value
+   */
+  void set_visited_pair_of_states(long visited_pair_of_states);
 
   /*!
   \brief Accessor
@@ -56,6 +52,12 @@ public:
   */
   bool relationship_fulfilled() const;
 
+  /*!
+   \brief setter for relationship_fulfilled
+   \post relationship_fulfilled is set to the given value
+   */
+  void set_relationship_fulfilled(bool relationship_fulfilled);
+
   /*!
    \brief Extract statistics as attributes (key, value)
    \param m : attributes map
@@ -64,9 +66,7 @@ public:
   void attributes(std::map<std::string, std::string> & m) const;
 
 private:
-  unsigned long _visited_pair_of_states;      /*!< Number of visited pairs of states */
-  unsigned long _visited_transitions; /*!< Number of visited transitions */
-  unsigned long _deepest_path; /*!< Number of visited transitions */
+  long _visited_pair_of_states;  /*!< Number of visited pairs of states */
   bool _relationship_fulfilled;  /*< Whether the relationship is fulfilled */
 };
 

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

@@ -5,8 +5,16 @@
  *
  */
 
-#ifndef TCHECKER_ALGORITHMS_REACH_ALGORITHM_HH
-#define TCHECKER_ALGORITHMS_REACH_ALGORITHM_HH
+#ifndef TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH
+#define TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH
+
+#define TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH_SEED 0xDEADBEEF
+
+#if BOOST_VERSION <= 106600
+#include <boost/functional/hash.hpp>
+#else
+#include <boost/container_hash/hash.hpp>
+#endif
 
 #include "tchecker/strong-timed-bisim/stats.hh"
 #include "tchecker/vcg/vcg.hh"
@@ -42,52 +50,62 @@ public:
 
 private:
 
+  struct custom_hash {
+    size_t operator()(const std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t> &to_hash) const {
+      std::size_t h1 = tchecker::zg::hash_value(*(to_hash.first));
+      std::size_t h2 = tchecker::zg::hash_value(*(to_hash.second));
+
+      // https://stackoverflow.com/questions/2590677/how-do-i-combine-hash-values-in-c0x
+      std::size_t h = (h1 + 0x9e3779b9 + (TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH_SEED <<6) + (TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH_SEED>>2));
+      h ^= (h2 + 0x9e3779b9 + + (TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH_SEED <<6) + (TCHECKER_STRONG_TIMED_BISIM_VIRTUAL_CLOCK_ALGORITHM_HH_SEED>>2));
+      return h;
+    }
+  };
+
+  struct custom_equal {
+    bool operator() (const std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t> &p1, const std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t> &p2) const {
+      return (*(p1.first) == *(p2.first)) && (*(p1.second) == *(p2.second));
+    }
+  };
+
+  /*!
+   \brief check-for-virt-bisim function of Lieb et al.
+   \param symb_state_first : the symbolic state that belongs to the first vcg
+   \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);
+
   /*!
    \brief check-for-outgoing-transitions-impl function of Lieb et al.
    \param symb_state_first : the symbolic state that belongs to the first vcg
    \param vcg_first : the first vcg
    \param symb_state_second : the symbolic state that belongs to the second vcg
    \param vcg_second : the second vcg
-   \param func : a function that takes two symbolic states and returns a list of virtual constraint
+   \param A_is_first : whether the outgoing transitions of A or B shall be checked
    \return a list of virtual constraints that cannot be simulated.
    \note the result is allocated at the heap and must be freed.
    */
-
   std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
-  check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t symb_state_first,
-                                  std::shared_ptr<tchecker::vcg::vcg_t> vcg_first,
-                                  tchecker::zg::const_state_sptr_t symb_state_second,
-                                  std::shared_ptr<tchecker::vcg::vcg_t> vcg_second,
-                                  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
-                                    (*func)(tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t));
-
-  /*
-   \brief calling check_for_outgoing_transitions with first = A
-   */
-  inline std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
-  check_for_outgoing_transitions_of_A( tchecker::zg::const_state_sptr_t symb_state_A,
-                                      tchecker::zg::const_state_sptr_t symb_state_B,
-                                       std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
-                                         (*func)(tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t))
-  {
-    return check_for_outgoing_transitions(symb_state_A, _A, symb_state_B, _B, func);
-  }
-
-  /*
-   \brief calling check_for_outgoing_transitions with first = B
-   */
-  inline std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
-  check_for_outgoing_transitions_of_B( tchecker::zg::const_state_sptr_t symb_state_A,
-                                       tchecker::zg::const_state_sptr_t symb_state_B,
-                                       std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
-                                         (*func)(tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t))
-  {
-    return check_for_outgoing_transitions(symb_state_B, _B, symb_state_A, _A, func);
-  }
+  check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t A_state,
+                                  tchecker::zg::const_state_sptr_t B_state,
+                                  std::unordered_set<std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t>, custom_hash, custom_equal> & visited);
 
   const std::shared_ptr<tchecker::vcg::vcg_t> _A;
   const std::shared_ptr<tchecker::vcg::vcg_t> _B;
 
+  long _visited_pair_of_states;
+
+  long _delete_me;
+
+
 };
 
 } // end of namespace strong_timed_bisim

include/tchecker/utils/zone_container.hh

@@ -9,6 +9,7 @@
 #define TCHECKER_ZG_ZONE_CONTAINER_HH
 
 #include <iterator>
+#include <memory>
 
 #include "tchecker/zg/zone.hh"
 #include "tchecker/vcg/virtual_constraint.hh"
@@ -34,13 +35,13 @@ public:
    \brief Constructor
    \param dim : dimension
    */
-  zone_container_t(tchecker::clock_id_t dim) : _dim(dim){ }
+  zone_container_t<T>(tchecker::clock_id_t dim) : _dim(dim), _storage(std::make_shared<std::vector<std::shared_ptr<T>>>(0)) { }
 
   /*!
    \brief Copy Constructor
    \param container : the container to copy
    */
-  zone_container_t(zone_container_t &t) : _dim(t.dim()), _storage(0)
+  zone_container_t<T>(zone_container_t<T> &t) : _dim(t.dim()), _storage(std::make_shared<std::vector<std::shared_ptr<T>>>(0))
   {
     for(auto iter = t.begin(); iter < t.end(); iter++) {
       this->append_zone(*(*iter));
@@ -60,23 +61,13 @@ public:
 
   std::shared_ptr<T> create_element(T const &zone);
 
-  /*!
-   \brief destructor of zone. Calling the destructor of tchecker::zg::zone_t
-   \note If T extends tchecker::zg::zone_t by a datastructure, there is a need for 
-   specialisation here!
-  */
-  void destruct_element(std::shared_ptr<T> zone)
-  {
-    tchecker::zg::zone_destruct_and_deallocate(&(*zone));
-  }
-
   /*
    \brief check for emptiness of the container
    \return true if and only if the container is empty
    */
   bool is_empty()
   {
-    return 0 == _storage.size();
+    return 0 == _storage->size();
   }
 
   /*!
@@ -84,7 +75,7 @@ public:
    */
   void append_zone()
   {
-    _storage.emplace_back(create_element());
+    _storage->emplace_back(create_element());
   }
 
   /*!
@@ -92,7 +83,8 @@ public:
    */
   void append_zone(T const & zone)
   {
-    _storage.emplace_back(create_element(zone));
+    assert(_dim == zone.dim());
+    _storage->emplace_back(create_element(zone));
   }
 
 
@@ -103,16 +95,55 @@ public:
    */
   void append_zone(std::shared_ptr<T> zone)
   {
-    _storage.emplace_back(zone);
+    assert(_dim == zone->dim());
+    _storage->emplace_back(zone);
+  }
+
+  /*!
+   \brief adds the elements of other to this
+   \param other: the container to append
+   \post other is appended to the container
+   */
+  void append_container(std::shared_ptr<zone_container_t<T>> other)
+  {
+    assert(other->_dim == this->_dim);
+    for(auto iter = other->begin(); iter < other->end(); iter++) {
+      this->append_zone(*iter);
+    }
+  }
+
+  /*!
+   \brief adds the elements of other to this. The elements that can be accessed are the same!
+   \param other: the container to append
+   \post other is appended to the container
+   */
+  void append_container(zone_container_t<T> &other)
+  {
+    assert(other._dim == this->_dim);
+    for(auto iter = other.begin(); iter < other.end(); iter++) {
+      this->append_zone(*iter);
+    }
   }
 
   /*!
    \brief removes the last zone and deletes the content
    */
-  void remove_back()
+  void remove_first()
   {
     destruct_element(*(_storage.begin()));
-    _storage.erase(_storage.begin());
+    _storage->erase(_storage.begin());
+  }
+
+  /*!
+   \brief removes all empty zones
+   */
+  void remove_empty()
+  {
+    for(auto iter = this->begin(); iter < this->end(); iter++) {
+      if(iter->empty()) {
+        _storage->erase(iter);
+      }
+    }
   }
 
   /*!
@@ -121,7 +152,7 @@ public:
    */
   std::shared_ptr<T> back()
   {
-    return _storage.back();
+    return _storage->back();
   }
 
   /*!
@@ -131,7 +162,7 @@ public:
    */
   std::shared_ptr<T> operator[](typename std::vector<std::shared_ptr<T>>::size_type i)
   {
-    return _storage[i];
+    return (*_storage)[i];
   }
 
   /*!
@@ -140,7 +171,7 @@ public:
    */
   typename std::vector<std::shared_ptr<T>>::size_type size()
   {
-    return _storage.size();
+    return _storage->size();
   }
 
   /*!
@@ -148,7 +179,7 @@ public:
    */
   typename std::vector<std::shared_ptr<T>>::iterator begin()
   {
-    return _storage.begin();
+    return _storage->begin();
   }
 
   /*!
@@ -156,22 +187,63 @@ public:
    */
   typename std::vector<std::shared_ptr<T>>::iterator end()
   {
-    return _storage.end();
+    return _storage->end();
   }
 
   /*!
-   \brief Destructor
+   \brief compresses the zone container if possible
+   \post let zc_prev be the zone container before the call and zc_after the zone container after. The following conditions hold:
+           - 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
    */
-  ~zone_container_t()
+
+  void compress()
   {
-    for(auto iter = begin(); iter < end(); ++iter) {
-      destruct_element(*iter);
-    }
+
+    std::shared_ptr<std::vector<std::shared_ptr<T>>> result = _storage;
+
+    bool reduced;
+
+    do {
+      auto prev = result->size();
+      result = find_union_partner(*result);
+      reduced = (result->size() < prev);
+    } while (reduced);
+
+    assert(result->size() <= _storage->size());
+
+    _storage = result;
+
   }
 
 private:
+
+  std::shared_ptr<std::vector<std::shared_ptr<T>>> find_union_partner(std::vector<std::shared_ptr<T>> const cur)
+  {
+    std::shared_ptr<std::vector<std::shared_ptr<T>>> result = std::make_shared<std::vector<std::shared_ptr<T>>>();
+
+    for(auto to_add = cur.begin(); to_add < cur.end(); ++to_add) {
+      bool found = false;
+      for(auto in_result = result->begin(); in_result < result->end(); ++in_result) {
+        tchecker::dbm::db_t cur_union[this->dim() * this->dim()];
+        if(tchecker::dbm::union_convex_t::UNION_IS_CONVEX == tchecker::dbm::convex_union(cur_union, (*to_add)->dbm(), (*in_result)->dbm(), this->dim())) {
+          found = true;
+          tchecker::dbm::copy((*in_result)->dbm(), cur_union, this->dim());
+          break;
+        }
+      }
+
+      if(!found) {
+        result->emplace_back(*to_add);
+      }
+    }
+
+    return result;
+  }
+
   const tchecker::clock_id_t _dim;
-  std::vector<std::shared_ptr<T>> _storage;
+  std::shared_ptr<std::vector<std::shared_ptr<T>>> _storage;
 
 };
 
@@ -188,13 +260,6 @@ std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> zone_contain
 template<>
 std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>::create_element(tchecker::virtual_constraint::virtual_constraint_t const & zone);
 
-/*!
- \brief contained-in-all function (see the TR of Lieb et al.)
- \param a vector of vector of zones
- \return a vector of zones
- */
-zone_container_t<tchecker::zg::zone_t> contained_in_all(std::vector<zone_container_t<tchecker::zg::zone_t>> & zones, tchecker::clock_id_t dim);
-
 
 } // end of namespace tchecker
 

include/tchecker/vcg/revert_transitions.hh

@@ -11,6 +11,10 @@
 #include "tchecker/vcg/virtual_constraint.hh"
 #include "tchecker/zg/zone.hh"
 
+namespace tchecker {
+
+namespace vcg {
+
 /*!
  \brief revert-action-trans function (see the TR of Lieb et al.)
  \param zone : the original zone
@@ -36,4 +40,8 @@ revert_action_trans(const tchecker::zg::zone_t & zone,
 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);
 
+} // end of namespace vcg
+
+} // end of namespace tchecker
+
 #endif

include/tchecker/vcg/sync.hh

@@ -8,6 +8,7 @@
 #ifndef TCHECKER_VCG_SYNC_HH
 #define TCHECKER_VCG_SYNC_HH
 
+#include "tchecker/dbm/dbm.hh"
 #include "virtual_constraint.hh"
 
 namespace tchecker {
@@ -18,7 +19,8 @@ namespace vcg {
  \brief sync function (see the TR of Lieb et al.)
  \param dbm1 : a dbm
  \param dbm2 : a dbm
- \param dim : dimension of dbm1 and dbm2
+ \param dim1 : dimension of dbm1
+ \param dim2 : dimension of 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 orig_reset1 : the resets of the transition of the first TA
@@ -32,11 +34,26 @@ namespace vcg {
  \note the change happens inplace
  */
 
-void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, tchecker::clock_id_t dim, 
-          tchecker::clock_id_t lowest_virt_clk_id, tchecker::clock_id_t no_of_orig_clocks_1,
+void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2,
+          tchecker::clock_id_t dim1, tchecker::clock_id_t dim2,
+          tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2,
           tchecker::clock_reset_container_t const & orig_reset1,
           tchecker::clock_reset_container_t const & orig_reset2);
 
+/*!
+ \brief checks whether the following dbm are synced
+ \param dbm1 : the DBM of A
+ \param dbm2 : the DBM of B
+ \param dim1 : the dim of dbm1
+ \param dim2 : the dim of dbm2
+ \param no_of_original_clocks_1 : the number of non virt (and non ref) clocks of A
+ \param no_of_original_clocks_2 : the number of non virt (and non ref) clocks of B
+ */
+
+bool are_dbm_synced(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2,
+                    tchecker::clock_id_t dim1, tchecker::clock_id_t dim2,
+                    tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2);
+
 /*!
  \brief revert-sync function (see the TR of Lieb et al.)
  \param dbm1 : a dbm
@@ -53,10 +70,11 @@ void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, tchecker::clock_
  \note the change happens inplace. this function works if and only if only
  resets to zero are allowed!
  */
-std::tuple<std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>, std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>>
-revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2, tchecker::clock_id_t dim,
-            const tchecker::virtual_constraint::virtual_constraint_t & phi_e, tchecker::clock_id_t lowest_virt_clk_id,
-            tchecker::clock_id_t no_of_orig_clocks_1);
+std::pair<std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>, std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>>
+revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2,
+            tchecker::clock_id_t dim1, tchecker::clock_id_t dim2,
+            tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2,
+            const tchecker::virtual_constraint::virtual_constraint_t & phi_e);
 
 
 } // end of namespace vcg

include/tchecker/vcg/vcg.hh

@@ -36,10 +36,11 @@ public:
    \param sharing_type : type of state/transition sharing
    \param semantics : a zone semantics
    \param no_of_virtual_clocks : number of virtual clocks
-   \param extrapolation : a zone extrapolation 
+   \param extrapolation : a zone extrapolation
    \param block_size : number of objects allocated in a block
    \param table_size : size of hash tables
-   \note all states and transitions are pool allocated and deallocated automatically
+   \note all states and transitions are pool allocated and deallocated automatically.
+         enable_extrapolation is set to false, since the current bisimulation algorithm does the extrapolation by itself
    */
   vcg_t(std::shared_ptr<tchecker::ta::system_t const> const & system, enum tchecker::ts::sharing_type_t sharing_type,
        std::shared_ptr<tchecker::zg::semantics_t> const & semantics, tchecker::clock_id_t no_of_virtual_clocks,
@@ -51,6 +52,8 @@ public:
    */
   tchecker::clock_id_t get_no_of_virtual_clocks() const;
 
+  inline tchecker::clock_id_t get_no_of_original_clocks() const { return _system->clocks_count(tchecker::variable_kind_t::VK_FLATTENED) - _no_of_virtual_clocks;}
+
 private:
 
   tchecker::clock_id_t _no_of_virtual_clocks;

include/tchecker/vcg/virtual_constraint.hh

@@ -52,13 +52,13 @@ public:
    \brief Accessor
    \return no of virtual clocks
    */
-  const tchecker::clock_id_t get_no_of_virt_clocks() const;
+  tchecker::clock_id_t get_no_of_virt_clocks() const;
 
   /*!
    \brief return the virtual constraint as list of clock constraints
-   \param sum_of_orig_clocks : the sum of the original clocks of both TA
+   \param no_of_orig_clocks : the number of orig clocks, used as offset
    */
-  clock_constraint_container_t get_vc(tchecker::clock_id_t orig_clocks_offset) const;
+  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
@@ -66,20 +66,58 @@ public:
    *  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.
    */
-  tchecker::zone_container_t<virtual_constraint_t> * neg() const;
+  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!
+   \param other : the other vc not this shall be anded with
+   */
+  void neg_logic_and(std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> result, const virtual_constraint_t & other) const;
+
+ /*
+  \brief returns (this and zone)
+  \param result : the pointer in which the result will be stored. Has to be allocated!
+  \param zone : the zone this shall be anded with
+  \return EMPTY if the resulting DBM is empty, NON_EMPTY otherwise
+  */
+  enum tchecker::dbm::status_t logic_and(std::shared_ptr<virtual_constraint_t> result, const virtual_constraint_t & other) const;
+
+ /*
+  \brief returns (this and zone)
+  \param result : the pointer in which the result will be stored. Has to be allocated!
+  \param zone : the zone this shall be anded with
+  \return EMPTY if the resulting DBM is empty, NON_EMPTY otherwise
+  */
+  enum tchecker::dbm::status_t logic_and(std::shared_ptr<tchecker::zg::zone_t> result, const tchecker::zg::zone_t & zone) const;
+
+ /*
+  \brief returns (this and zone)
+  \param result : the ref in which the result will be stored.
+  \param zone : the zone this shall be anded with
+  \return EMPTY if the resulting DBM is empty, NON_EMPTY otherwise
+  */
+  enum tchecker::dbm::status_t logic_and(tchecker::zg::zone_t & result, const tchecker::zg::zone_t & zone) const;
 
  /*
   \brief iterates through the container and logically ands each element with this
+  \param result : the pointer in which the result will be stored. Has to be allocated!
   \param container : the container to and with
-  \return a copy of container with each element being logically anded with this.
+  \return a container with each element of container being logically anded with this.
   */
-  tchecker::zone_container_t<virtual_constraint_t> logic_and(tchecker::zone_container_t<virtual_constraint_t> *container);
+  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;
+
+private:
+
+  std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> neg_helper(tchecker::dbm::db_t *upper_bounds) const;
 
 };
 
 // factories
-std::shared_ptr<virtual_constraint_t> factory(tchecker::clock_id_t dim);
+std::shared_ptr<virtual_constraint_t> factory(tchecker::clock_id_t no_of_virtual_clocks);
 
 std::shared_ptr<virtual_constraint_t> factory(tchecker::virtual_constraint::virtual_constraint_t const & virtual_constraint);
 
@@ -91,6 +129,14 @@ std::shared_ptr<virtual_constraint_t> factory(tchecker::virtual_constraint::virt
  */
 std::shared_ptr<virtual_constraint_t> factory(std::shared_ptr<tchecker::zg::zone_t const> zone, tchecker::clock_id_t no_of_virtual_clocks);
 
+/*!
+ \brief extract the virtual constraint from a zone
+ \param zone : the zone from which the virtual constraint should be extracted
+ \param virtual_clocks : the number of virtual clocks
+ \return the virtual constraint of zone
+ */
+std::shared_ptr<virtual_constraint_t> factory(tchecker::zg::zone_t const & zone, tchecker::clock_id_t no_of_virtual_clocks);
+
 /*!
  \brief extract the virtual constraint from a dbm
  \param dbm : the dbm from which the virtual constraint should be extracted
@@ -100,16 +146,20 @@ std::shared_ptr<virtual_constraint_t> factory(std::shared_ptr<tchecker::zg::zone
  */
 std::shared_ptr<virtual_constraint_t> factory(const tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::clock_id_t no_of_virtual_clocks);
 
-// destruction
-
-void destruct(virtual_constraint_t *to_destruct);
-
 /*!
  \brief combine operator (see the TR of Lieb et al.)
- \param a vector of vector of virtual constraints
- \return a vector of virtual constraints
+ \param a container of virtual constraints
+ \return a container of virtual constraints
  */
-tchecker::zone_container_t<virtual_constraint_t> *combine(std::vector<tchecker::zone_container_t<virtual_constraint_t>> & lo_lo_vc, tchecker::clock_id_t dim);
+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 contained-in-all function (see the TR of Lieb et al.)
+ \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);
+
 
 } // end of namespace virtual_constraint
 

include/tchecker/zg/semantics.hh

@@ -101,6 +101,20 @@ public:
                                         tchecker::clock_constraint_container_t const & guard,
                                         tchecker::clock_reset_container_t const & clkreset, bool tgt_delay_allowed,
                                         tchecker::clock_constraint_container_t const & tgt_invariant) = 0;
+
+  /*!
+  \brief Compute next zone when epsilon transition is used
+  \param dbm : a DBM
+  \param dim : dimension of dbm
+  \param invariant : invariant of current state
+  \post dbm has been delayed (if allowed), then intersected with src_invariant,
+  \return tchecker::STATE_OK if the resulting DBM is not empty. Otherwise,
+  tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED if intersection with src_invariant
+  result in an empty zone
+  */
+  tchecker::state_status_t delay( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim,
+                                  tchecker::clock_constraint_container_t const & invariant);
+
 };
 
 /*!
@@ -340,19 +354,6 @@ public:
   virtual tchecker::state_status_t final(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
                                          tchecker::clock_constraint_container_t const & invariant);
 
-  /*!
-  \brief Compute next zone when epsilon transition is used
-  \param dbm : a DBM
-  \param dim : dimension of dbm
-  \param invariant : invariant of current state
-  \post dbm has been delayed (if allowed), then intersected with src_invariant,
-  \return tchecker::STATE_OK if the resulting DBM is not empty. Otherwise,
-  tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED if intersection with src_invariant
-  result in an empty zone
-  */
-  tchecker::state_status_t delay( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim,
-                                  tchecker::clock_constraint_container_t const & invariant);
-
   /*!
   \brief Compute next zone when action transition is used
   \param dbm : a DBM

include/tchecker/zg/state.hh

@@ -101,6 +101,13 @@ public:
   */
   constexpr inline tchecker::zg::zone_t const & zone() const { return *_zone; }
 
+
+  /*!
+  \brief Accessor
+  \return zone in this state
+  */
+  constexpr inline tchecker::zg::zone_t & zone() { return *_zone; }
+
   /*!
   \brief Accessor
   \return reference to pointer to the zone in this state

include/tchecker/zg/zg.hh

@@ -169,12 +169,14 @@ public:
    */
   zg_t(std::shared_ptr<tchecker::ta::system_t const> const & system, enum tchecker::ts::sharing_type_t sharing_type,
        std::shared_ptr<tchecker::zg::semantics_t> const & semantics,
-       std::shared_ptr<tchecker::zg::extrapolation_t> const & extrapolation, std::size_t block_size, std::size_t table_size)
+       std::shared_ptr<tchecker::zg::extrapolation_t> const & extrapolation, std::size_t block_size, std::size_t table_size,
+       bool enable_extrapolation = true)
     : _system(system), _sharing_type(sharing_type), _semantics(semantics), _extrapolation(extrapolation),
       _state_allocator(block_size, block_size, _system->processes_count(), block_size,
                        _system->intvars_count(tchecker::VK_FLATTENED), block_size,
                        _system->clocks_count(tchecker::VK_FLATTENED) + 1, table_size),
-      _transition_allocator(block_size, block_size, _system->processes_count(), table_size)
+      _transition_allocator(block_size, block_size, _system->processes_count(), table_size),
+      _enable_extrapolation(enable_extrapolation)
   {
   }
 
@@ -402,6 +404,14 @@ public:
   void split(tchecker::zg::const_state_sptr_t const & s, tchecker::clock_constraint_container_t const & constraints,
              std::vector<tchecker::zg::state_sptr_t> & v);
 
+  /*!
+   \brief runs the extrapolation on the given dbm
+   \param dbm : the dbm to extrapolate
+   \param dim : the dimension of the dbm
+   \param vloc : a set of locations
+   \post the dbm is extrapolated
+   */
+  inline void run_extrapolation(tchecker::dbm::db_t *dbm, tchecker::clock_id_t dim, tchecker::vloc_t const & vloc) const { _extrapolation->extrapolate(dbm, dim, vloc); }
 
   // Inspector
 
@@ -472,6 +482,12 @@ public:
    */
   inline tchecker::ta::system_t const & system() const { return *_system; }
 
+  /*!
+   \brief Accessor
+   \return Underlying semantics
+   */
+  inline std::shared_ptr<tchecker::zg::semantics_t> const & semantics() const { return _semantics; }
+
   /*!
    \brief Accessor
    \return sharing type of this synchronized product
@@ -482,9 +498,13 @@ public:
    \brief Accessor
    \return number of clocks
    */
-  inline tchecker::clock_id_t clocks_count()  { return _system->clocks_count(tchecker::VK_FLATTENED);  }
+  inline tchecker::clock_id_t clocks_count() const { return _system->clocks_count(tchecker::VK_FLATTENED);  }
 
-private:
+  inline tchecker::zg::state_sptr_t create_state() {return _state_allocator.construct();}
+  inline tchecker::zg::state_sptr_t clone_state(tchecker::zg::const_state_sptr_t const & to_clone) {return _state_allocator.clone(*to_clone);}
+  inline tchecker::zg::state_sptr_t clone_state(tchecker::zg::state_sptr_t const & to_clone) {return _state_allocator.clone(*to_clone);}
+
+protected:
 
   /*!
    \brief High-Order function to shorten the handling of states and transitions
@@ -511,7 +531,7 @@ private:
                                                          tchecker::zg::state_sptr_t &,
                                                         tchecker::zg::transition_sptr_t &,
                                                          helping_hand_t *),
-                  tchecker::zg::const_state_sptr_t const & to_clone, bool clone
+                  tchecker::zg::const_state_sptr_t const & to_clone, bool clone, bool enable_extrapolation = true
                   );
   /*!
    \brief Clone and constrain a state
@@ -537,6 +557,7 @@ private:
   std::shared_ptr<tchecker::zg::extrapolation_t> _extrapolation;   /*!< Zone extrapolation */
   tchecker::zg::state_pool_allocator_t _state_allocator;           /*!< Pool allocator of states */
   tchecker::zg::transition_pool_allocator_t _transition_allocator; /*! Pool allocator of transitions */
+  bool _enable_extrapolation;
 };
 
 /* tools */
@@ -571,13 +592,13 @@ next(tchecker::zg::zg_t &zg,
 std::shared_ptr<zg_t> factory(std::shared_ptr<tchecker::ta::system_t const> const & system,
                              enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type,
                              enum tchecker::zg::extrapolation_type_t extrapolation_type, std::size_t block_size,
-                             std::size_t table_size);
+                             std::size_t table_size, bool enable_extrapolation = true);
 
 std::shared_ptr<zg_t> factory(std::shared_ptr<tchecker::ta::system_t const> const & system,
                              enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type,
                              enum tchecker::zg::extrapolation_type_t extrapolation_type,
                              tchecker::clockbounds::clockbounds_t const & clock_bounds, std::size_t block_size,
-                             std::size_t table_size);
+                             std::size_t table_size, bool enable_extrapolation = true);
 
 } // end of namespace zg
 

src/dbm/dbm.cc

@@ -185,8 +185,9 @@ enum tchecker::dbm::status_t tighten(tchecker::dbm::db_t * dbm, tchecker::clock_
     for (tchecker::clock_id_t i = 0; i < dim; ++i) {
       if ((i == k) || (DBM(i, k) == tchecker::dbm::LT_INFINITY)) // optimization
         continue;
-      for (tchecker::clock_id_t j = 0; j < dim; ++j)
+      for (tchecker::clock_id_t j = 0; j < dim; ++j) {
         DBM(i, j) = tchecker::dbm::min(tchecker::dbm::sum(DBM(i, k), DBM(k, j)), DBM(i, j));
+      }
       if (DBM(i, i) < tchecker::dbm::LE_ZERO) {
         DBM(0, 0) = tchecker::dbm::LT_ZERO;
         return tchecker::dbm::EMPTY;
@@ -524,12 +525,61 @@ enum tchecker::dbm::status_t intersection(tchecker::dbm::db_t * dbm, tchecker::d
   return tchecker::dbm::tighten(dbm, dim);
 }
 
+// used for assertion only
+bool split_is_subset_of_R_orig(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::dbm::db_t r_orig[dim*dim];
+  tchecker::dbm::copy(r_orig, orig_zone, dim);
+
+  // resets to zero allowed, only
+  for(const tchecker::clock_reset_t & r : reset) {
+    reset_to_value(r_orig, dim, r.left_id() + 1, 0);
+  }
+
+  assert(tchecker::dbm::is_tight(r_orig, dim));
+  assert(tchecker::dbm::is_consistent(r_orig, dim));
+
+  if(!tchecker::dbm::is_le(zone_split, r_orig, dim)) {
+    std::cout << __FILE__ << ": " << __LINE__ << ": orig_zone:" << std::endl;
+    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);
+
+
+    std::cout << __FILE__ << ": " << __LINE__ << ": resets:" << std::endl;
+
+    for(const tchecker::clock_reset_t & r : reset) {
+      std::cout << r << std::endl;
+    }
+
+    std::cout << __FILE__ << ": " << __LINE__ << ": R(orig_zone):" << std::endl;
+    tchecker::dbm::output_matrix(std::cout, r_orig, dim);
+
+    return false;
+  }
+
+  return true;
+
+}
+
 tchecker::dbm::db_t * revert_multiple_reset(const tchecker::dbm::db_t * orig_zone,
                                             tchecker::clock_id_t dim, tchecker::dbm::db_t * zone_split,
                                             tchecker::clock_reset_container_t reset)
 {
 
-  // TODO: add assertions
+  assert(dim >= 1);
+  assert(orig_zone != nullptr);
+  assert(zone_split != nullptr);
+  assert(tchecker::dbm::is_consistent(orig_zone, dim));
+  assert(tchecker::dbm::is_consistent(zone_split, dim));
+  assert(tchecker::dbm::is_tight(orig_zone, dim));
+  assert(tchecker::dbm::is_tight(zone_split, dim));
+
+  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
@@ -1264,6 +1314,61 @@ enum tchecker::dbm::clock_position_t clock_position(tchecker::dbm::db_t const *
   return tchecker::dbm::CLK_SYNCHRONIZABLE;
 }
 
+enum tchecker::dbm::union_convex_t convex_union(tchecker::dbm::db_t *result, tchecker::dbm::db_t const * dbm1, tchecker::dbm::db_t const * dbm2, tchecker::clock_id_t dim)
+{
+  assert(result != nullptr);
+  assert(dbm1 != nullptr);
+  assert(dbm2 != nullptr);
+
+  assert(dim >= 1);
+
+  assert(tchecker::dbm::is_consistent(dbm1, dim));
+  assert(tchecker::dbm::is_tight(dbm1, dim));
+
+  assert(tchecker::dbm::is_consistent(dbm2, dim));
+  assert(tchecker::dbm::is_tight(dbm2, dim));
+
+  tchecker::dbm::copy(result, dbm1, dim);
+
+  std::vector<std::tuple<tchecker::clock_id_t, tchecker::clock_id_t, tchecker::dbm::db_t>> dbm1_tight;
+  std::vector<std::tuple<tchecker::clock_id_t, tchecker::clock_id_t, tchecker::dbm::db_t>> dbm2_tight;
+
+  for(tchecker::clock_id_t i = 0; i < dim; ++i) {
+    for(tchecker::clock_id_t j = 0; j < dim; ++j) {
+      if(DBM1(i, j) <  DBM2(i, j) ) {
+        result[i*dim + j] = DBM2(i, j);
+        dbm1_tight.emplace_back(std::make_tuple<tchecker::clock_id_t, tchecker::clock_id_t, tchecker::dbm::db_t>(std::move(i), std::move(j), tchecker::dbm::db_t(DBM1(i, j))));
+      } else if (DBM2(i, j) < DBM1(i, j)) {
+        dbm2_tight.emplace_back(std::make_tuple<tchecker::clock_id_t, tchecker::clock_id_t, tchecker::dbm::db_t>(std::move(i), std::move(j), tchecker::dbm::db_t(DBM2(i, j))));
+      }
+    }
+  }
+
+  if(dbm2_tight.empty()) {
+    return tchecker::dbm::union_convex_t::UNION_IS_CONVEX;
+  }
+
+  if (dbm1_tight.empty()) {
+    tchecker::dbm::copy(result, dbm2, dim);
+    return tchecker::dbm::union_convex_t::UNION_IS_CONVEX;
+  }
+
+  for(auto iter = dbm1_tight.begin(); iter < dbm1_tight.end(); iter++) {
+    tchecker::dbm::db_t diff_dbm[dim*dim];
+    tchecker::dbm::copy(diff_dbm, result, dim);
+    diff_dbm[std::get<1>(*iter) * dim + std::get<0>(*iter)] = tchecker::dbm::invert(std::get<2>(*iter));
+    tchecker::dbm::tighten(diff_dbm, dim);
+    for(auto iter2 = dbm2_tight.begin(); iter2 < dbm2_tight.end(); iter2++) {
+      if(diff_dbm[std::get<0>(*iter2) * dim + std::get<1>(*iter2)] > std::get<2>(*iter2)) {
+        return tchecker::dbm::union_convex_t::UNION_IS_NOT_CONVEX;
+      }
+    }
+  }
+
+  return tchecker::dbm::union_convex_t::UNION_IS_CONVEX;
+
+}
+
 } // end of namespace dbm
 
 } // end of namespace tchecker

src/extrapolation/CMakeLists.txt

@@ -7,14 +7,12 @@ ${CMAKE_CURRENT_SOURCE_DIR}/extrapolation.cc
 ${CMAKE_CURRENT_SOURCE_DIR}/extrapolation_factory.cc
 ${CMAKE_CURRENT_SOURCE_DIR}/global_lu_extrapolation.cc
 ${CMAKE_CURRENT_SOURCE_DIR}/global_m_extrapolation.cc
-${CMAKE_CURRENT_SOURCE_DIR}/k_norm.cc
 ${CMAKE_CURRENT_SOURCE_DIR}/local_lu_extrapolation.cc
 ${CMAKE_CURRENT_SOURCE_DIR}/local_m_extrapolation.cc
 ${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/extrapolation.hh
 ${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/extrapolation_factory.hh
 ${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/global_lu_extrapolation.hh
 ${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/global_m_extrapolation.hh
-${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/k_norm.hh
 ${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/local_lu_extrapolation.hh
 ${TCHECKER_INCLUDE_DIR}/tchecker/extrapolation/local_m_extrapolation.hh
 PARENT_SCOPE)

src/extrapolation/extrapolation_factory.cc

@@ -16,7 +16,6 @@
 #include "tchecker/extrapolation/extrapolation.hh"
 #include "tchecker/extrapolation/global_lu_extrapolation.hh"
 #include "tchecker/extrapolation/global_m_extrapolation.hh"
-#include "tchecker/extrapolation/k_norm.hh"
 #include "tchecker/extrapolation/local_lu_extrapolation.hh"
 #include "tchecker/extrapolation/local_m_extrapolation.hh"
 
@@ -62,8 +61,6 @@ tchecker::zg::extrapolation_t * extrapolation_factory(enum extrapolation_type_t
     return new tchecker::zg::global_extra_m_plus_t{clock_bounds.global_m_map()};
   case tchecker::zg::EXTRA_M_PLUS_LOCAL:
     return new tchecker::zg::local_extra_m_plus_t{clock_bounds.local_m_map()};
-  case tchecker::zg::EXTRA_K_NORM:
-    return new tchecker::zg::k_norm{clock_bounds.global_lu_map()};
   default:
     throw std::invalid_argument("Unknown zone extrapolation");
   }
@@ -75,70 +72,51 @@ namespace vcg {
 
 tchecker::zg::extrapolation_t * extrapolation_factory(
                   enum tchecker::zg::extrapolation_type_t type,
-                  std::shared_ptr<tchecker::ta::system_t const> const & orig_system_first,
-                  std::shared_ptr<tchecker::ta::system_t const> const & orig_system_second,
+                  std::shared_ptr<const tchecker::ta::system_t> system_first,
+                  std::shared_ptr<const tchecker::ta::system_t> system_second,
                   bool first_not_second)
 {
-  if(tchecker::zg::EXTRA_K_NORM != type)
-    throw std::invalid_argument("vcg currently supports k normalization only.");
 
-  std::vector<std::vector<tchecker::clockbounds::bound_t>> bounds;
-  bounds.push_back(std::vector<tchecker::clockbounds::bound_t>());
-  bounds.push_back(std::vector<tchecker::clockbounds::bound_t>());
-
-  for(std::size_t i = 0; i < 2; ++i) {
-    std::unique_ptr<tchecker::clockbounds::clockbounds_t> clock_bounds{
-      tchecker::clockbounds::compute_clockbounds(0 == i ? *orig_system_first : *orig_system_second)};
-
-    if (clock_bounds.get() == nullptr)
-      return nullptr;
-
-    std::shared_ptr<tchecker::clockbounds::global_lu_map_t> lu_map = clock_bounds->global_lu_map();
-
-      // we set the upper and lower clock bound to the same value to receive k-norm.
-    tchecker::clockbounds::map_t *U = const_cast<tchecker::clockbounds::map_t*>(&(lu_map->U()));
-    tchecker::clockbounds::map_t *L = const_cast<tchecker::clockbounds::map_t*>(& (lu_map->L()));
-
-    tchecker::clockbounds::update(*U, *L);
-
-    for(tchecker::clock_id_t j = 0; j < clock_bounds->clock_number(); ++j) {
-      bounds[i].push_back(U[0][j]);
-    }
+  if(tchecker::zg::EXTRA_M_GLOBAL != type) { // vcg currently support k norm (m_global) only
+    throw std::invalid_argument("Unknown zone extrapolation");
   }
 
-  tchecker::clock_id_t no_of_virtual_clocks = orig_system_first->clocks_count(VK_FLATTENED) + orig_system_second->clocks_count(VK_FLATTENED);
-  tchecker::clock_id_t no_of_original_clocks = first_not_second ? orig_system_first->clocks_count(VK_FLATTENED) : orig_system_second->clocks_count(VK_FLATTENED);
-  tchecker::clock_id_t no_of_clocks = no_of_original_clocks + no_of_virtual_clocks;
+  std::unique_ptr<tchecker::clockbounds::clockbounds_t> clock_bounds_first{tchecker::clockbounds::compute_clockbounds(*system_first)};
+  if (clock_bounds_first.get() == nullptr)
+    return nullptr;
 
-  std::shared_ptr<tchecker::clockbounds::global_lu_map_t> resulting_clock_bounds = std::make_shared<tchecker::clockbounds::global_lu_map_t>(no_of_clocks);
+  std::unique_ptr<tchecker::clockbounds::clockbounds_t> clock_bounds_second{tchecker::clockbounds::compute_clockbounds(*system_second)};
+  if (clock_bounds_second.get() == nullptr)
+    return nullptr;
 
-  /* set the bounds */
 
-  // original
-  for(tchecker::clock_id_t i = 0; i < no_of_original_clocks; ++i) {
+  std::shared_ptr<const tchecker::clockbounds::global_m_map_t> M_first = clock_bounds_first->global_m_map();
+  std::shared_ptr<const tchecker::clockbounds::global_m_map_t> M_second = clock_bounds_second->global_m_map();
 
-    tchecker::clockbounds::bound_t bound = first_not_second ? bounds[0][i] : bounds[1][i];
 
-    tchecker::clockbounds::update(resulting_clock_bounds->L(), i, bound);
-    tchecker::clockbounds::update(resulting_clock_bounds->U(), i, bound);
+  tchecker::clock_id_t no_orig_clocks = (first_not_second) ? clock_bounds_first->clocks_number() : clock_bounds_second->clocks_number();
+
+  tchecker::clockbounds::global_m_map_t m_map_with_virt_clks{no_orig_clocks + clock_bounds_first->clocks_number() + clock_bounds_second->clocks_number()};
+
+  tchecker::clockbounds::clear(m_map_with_virt_clks.M());
+
+  for(clock_id_t i = 0; i < no_orig_clocks; ++i) {
+    tchecker::clockbounds::update(m_map_with_virt_clks.M(), i, (first_not_second) ? M_first->M()[i] : M_second->M()[i]);
   }
 
-
-  // first virtual
-  for(tchecker::clock_id_t i = no_of_original_clocks; i < no_of_original_clocks + orig_system_first->clocks_count(VK_FLATTENED); ++i) {
-    tchecker::clockbounds::update(resulting_clock_bounds->L(), i, bounds[0][i - no_of_original_clocks]);
-    tchecker::clockbounds::update(resulting_clock_bounds->U(), i, bounds[0][i - no_of_original_clocks]);
+  for(clock_id_t i = 0; i < clock_bounds_first->clocks_number(); ++i) {
+    tchecker::clockbounds::update(m_map_with_virt_clks.M(), i + no_orig_clocks, M_first->M()[i]);
   }
 
-  // second virtual
-  tchecker::clock_id_t offset_second_virtual = no_of_original_clocks + orig_system_first->clocks_count(VK_FLATTENED);
-
-  for(tchecker::clock_id_t i = offset_second_virtual; i < no_of_clocks; ++i) {
-    tchecker::clockbounds::update(resulting_clock_bounds->L(), i, bounds[1][i - offset_second_virtual]);
-    tchecker::clockbounds::update(resulting_clock_bounds->U(), i, bounds[1][i - offset_second_virtual]);
+  for(clock_id_t i = 0; i < clock_bounds_second->clocks_number(); ++i) {
+    tchecker::clockbounds::update(m_map_with_virt_clks.M(), i + no_orig_clocks + clock_bounds_first->clocks_number(), M_second->M()[i]);
   }
 
-  return new tchecker::vcg::k_norm_virtual{resulting_clock_bounds};
+  //std::cout << __FILE__ << ": " << __LINE__ << ": " << m_map_with_virt_clks << std::endl;
+
+  std::shared_ptr<tchecker::clockbounds::global_m_map_t const> final_map = std::make_shared<tchecker::clockbounds::global_m_map_t const>(m_map_with_virt_clks);
+
+  return new tchecker::zg::global_extra_m_t{final_map};
 
 }
 

src/extrapolation/k_norm.cc

@@ -1,39 +0,0 @@
-/*
- * This file is a part of the TChecker project.
- *
- * See files AUTHORS and LICENSE for copyright details.
- *
- */
-
-#include "tchecker/extrapolation/k_norm.hh"
-
-namespace tchecker {
-
-namespace zg {
-
-k_norm::k_norm(
-    std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> const & clock_bounds)
-    :tchecker::zg::global_extra_lu_t(clock_bounds)
-{
-  // k-norm is equivalent to global_extra_lu_t, if we always choose the maximum value of U(i) and L(i) for all checks.
-  tchecker::clockbounds::map_t *U = const_cast<tchecker::clockbounds::map_t*>(&(_clock_bounds->U()));
-  tchecker::clockbounds::map_t *L = const_cast<tchecker::clockbounds::map_t*>(& (_clock_bounds->L()));
-  
-
-  tchecker::clockbounds::update(*U, *L);
-  tchecker::clockbounds::update(*L, *U);
-}
-
-} // end of namespace zg
-
-namespace vcg {
-
-k_norm_virtual::k_norm_virtual(
-    std::shared_ptr<tchecker::clockbounds::global_lu_map_t const> const & clock_bounds)
-    :tchecker::zg::global_extra_lu_t(clock_bounds)
-{
-}
-
-} // end of namespace vcg
-
-} // end of namespace tchecker

src/strong-timed-bisim/stats.cc

@@ -13,15 +13,26 @@ namespace tchecker {
 
 namespace strong_timed_bisim {
 
-stats_t::stats_t() : _visited_pair_of_states(0), _visited_transitions(0), _deepest_path(0), _relationship_fulfilled(true) {}
+stats_t::stats_t() : _visited_pair_of_states(0), _relationship_fulfilled(true) {}
 
-unsigned long stats_t::visited_pair_of_states() const { return _visited_pair_of_states; }
+long stats_t::visited_pair_of_states() const
+{
+  return _visited_pair_of_states;
+}
 
-unsigned long stats_t::visited_transitions() const { return _visited_transitions; }
+void stats_t::set_visited_pair_of_states(long visited_pair_of_states)
+{
+  _visited_pair_of_states = visited_pair_of_states;
+}
 
-unsigned long stats_t::deepest_path() const { return _deepest_path; }
+bool stats_t::relationship_fulfilled() const {
+  return _relationship_fulfilled;
+}
 
-bool stats_t::relationship_fulfilled() const { return _relationship_fulfilled; }
+void stats_t::set_relationship_fulfilled(bool relationship_fulfilled)
+{
+  _relationship_fulfilled = relationship_fulfilled;
+}
 
 void stats_t::attributes(std::map<std::string, std::string> & m) const {
   tchecker::algorithms::stats_t::attributes(m);
@@ -29,18 +40,10 @@ void stats_t::attributes(std::map<std::string, std::string> & m) const {
   std::stringstream sstream;
 
   sstream << _visited_pair_of_states;
-  m["VISITED_PAIR_OF_STATES_STATES"] = sstream.str();
+  m["VISITED_PAIR_OF_STATES"] = sstream.str();
 
   sstream.str("");
-  sstream << _visited_transitions;
-  m["VISITED_TRANSITIONS"] = sstream.str();
-
-  sstream.str("");
-  sstream << _deepest_path;
-  m["DEEPEST_PATH"] = sstream.str();
-
-  sstream.str("");
-  sstream << std::boolalpha << _relationship_fulfilled;
+  sstream << (_relationship_fulfilled ? "true" : "false");
   m["RELATIONSHIP_FULFILLED"] = sstream.str();
 }
 

src/strong-timed-bisim/virtual_clock_algorithm.cc

@@ -7,24 +7,29 @@
 
 #include "tchecker/strong-timed-bisim/virtual_clock_algorithm.hh"
 #include "tchecker/vcg/virtual_constraint.hh"
+#include "tchecker/vcg/revert_transitions.hh"
+#include "tchecker/vcg/sync.hh"
+#include "tchecker/dbm/dbm.hh"
 
 namespace tchecker {
 
 namespace strong_timed_bisim {
 
-Lieb_et_al::Lieb_et_al(std::shared_ptr<tchecker::vcg::vcg_t> input_first, std::shared_ptr<tchecker::vcg::vcg_t> input_second) : _A(input_first), _B(input_first) {}
+Lieb_et_al::Lieb_et_al(std::shared_ptr<tchecker::vcg::vcg_t> input_first, std::shared_ptr<tchecker::vcg::vcg_t> input_second)
+  : _A(input_first), _B(input_second), _visited_pair_of_states(0), _delete_me(0)
+{
+  assert(_A->get_no_of_virtual_clocks() == _B->get_no_of_virtual_clocks());
+}
 
 tchecker::strong_timed_bisim::stats_t Lieb_et_al::run() {
 
-  std::cout << "run algorithm" << std::endl;
+//  std::cout << __FILE__ << ": " << __LINE__ << ": no of orig clocks is " << _A->get_no_of_original_clocks() << " and " << _B->get_no_of_original_clocks() << std::endl;
+//  std::cout << __FILE__ << ": " << __LINE__ << ": no of virt clocks is " << _A->get_no_of_virtual_clocks() << " and " << _B->get_no_of_virtual_clocks() << std::endl;
+
+  tchecker::strong_timed_bisim::stats_t stats;
 
-  stats_t stats;
-#if 0
   stats.set_start_time();
 
-  // sst is a tuple (tchecker::state_status_t, state_t, transition_t)
-  // state_status_t : see basictypes.hh
-
   std::vector<tchecker::zg::zg_t::sst_t> sst_first;
   std::vector<tchecker::zg::zg_t::sst_t> sst_second;
 
@@ -34,74 +39,432 @@ tchecker::strong_timed_bisim::stats_t Lieb_et_al::run() {
   if(STATE_OK != std::get<0>(sst_first[0]) || STATE_OK != std::get<0>(sst_second[0])) 
     throw std::runtime_error("problems with initial state");
 
-  std::size_t dim = std::get<1>(sst_first[0])->zone().dim();
-  auto dbm = std::get<1>(sst_first[0])->zone().dbm();
+  tchecker::zg::const_state_sptr_t const_first{std::get<1>(sst_first[0])};
+  tchecker::zg::const_state_sptr_t const_second{std::get<1>(sst_second[0])};
 
-  for(std::size_t i = 0; i < dim; ++i) {
-      for(std::size_t j = 0; j < dim; ++j) {
-        std::size_t index = i*dim + j;
-        std::cout << "(" << dbm[index].cmp << ", " << dbm[index].value << ") ";
-      }
-      std::cout << std::endl;
-  }
+//  std::cout << __FILE__ << ": " << __LINE__ << ": start algorithm" << std::endl;
 
-  tchecker::virtual_constraint::virtual_constraint_t *vc = tchecker::virtual_constraint::factory(&(std::get<1>(sst_first[0])->zone()), this->_A->get_no_of_virtual_clocks());
+  std::unordered_set<std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t>, custom_hash, custom_equal> empty;
 
-  const clock_constraint_container_t & virt_cons = vc->get_vc(this->_A->clocks_count() - this->_A->get_no_of_virtual_clocks());
-
-  for(auto iter = virt_cons.begin(); iter < virt_cons.end(); iter++) {
-    std::cout << *iter << std::endl;
-  }
-/*
-  for(std::size_t i = 0; i <= input_first->get_no_of_virtual_clocks(); ++i) {
-      for(std::size_t j = 0; j < input_first->get_no_of_virtual_clocks(); ++j) {
-        std::size_t index = i*input_first->get_no_of_virtual_clocks() + i + j;
-        std::cout << "(" << (vc->get_dbm())[index].cmp << ", " << (vc->get_dbm())[index].value << ") ";
-      }
-      std::cout << std::endl;
-  }
-*/
-  delete vc;
+  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> result 
+    = this->check_for_virt_bisim(const_first, std::get<2>(sst_first[0]), const_second, std::get<2>(sst_second[0]), empty, false);
 
   stats.set_end_time();
-#endif
+
+  stats.set_visited_pair_of_states(_visited_pair_of_states);
+  stats.set_relationship_fulfilled(result->is_empty());
+
   return stats;
 
 }
 
-std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
-Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t symb_state_first,
-                                            std::shared_ptr<tchecker::vcg::vcg_t> vcg_first,
-                                            tchecker::zg::const_state_sptr_t symb_state_second,
-                                            std::shared_ptr<tchecker::vcg::vcg_t> vcg_second,
-                                            std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
-                                              (*func)(tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t))
+// used for assertion only
+bool check_for_virt_bisim_preconditions_check(tchecker::zg::const_state_sptr_t symb_state, tchecker::zg::transition_sptr_t symb_trans)
 {
 
-  std::vector<tchecker::vcg::vcg_t::sst_t> v_first;
-  vcg_first->next(symb_state_first, v_first);
+  assert(tchecker::dbm::is_consistent(symb_state->zone().dbm(), symb_state->zone().dim()));
+  assert(tchecker::dbm::is_tight(symb_state->zone().dbm(), symb_state->zone().dim()));
 
-  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> result
-     = std::make_shared<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(vcg_first->get_no_of_virtual_clocks());
+  // we check whether the resets of the zones are matching the resets of the transitions. WARNING: This works for reset to zero only!
+  for(auto iter = symb_trans->reset_container().begin(); iter < symb_trans->reset_container().end(); iter++) {
 
-  for (auto && [status_first, s_first, t_first] : v_first) {
+    if(!iter->reset_to_zero()) {
+      std::cerr << __FILE__ << ": " << __LINE__ << ": the reset " << *iter << " is not a reset to zero" << std::endl;
+      return false;
+    }
 
-    std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> lo_result;
+    tchecker::clock_constraint_t orig_min_ref{iter->left_id(), tchecker::REFCLOCK_ID, tchecker::LE, 0};
+    tchecker::clock_constraint_t ref_min_orig{tchecker::REFCLOCK_ID, iter->left_id(), tchecker::LE, 0};
 
-    std::vector<tchecker::vcg::vcg_t::sst_t> v_second;
-    vcg_second->next(symb_state_second, v_second);
-
-    for (auto && [status_second, s_second, t_second] : v_first) {
-
-      if(t_first->vedge().event_equal(vcg_first->system(), t_second->vedge(), vcg_second->system())) {
-        std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> inter = func(s_first, s_second);
-        for(auto iter = inter->begin(); iter < inter->end(); iter++) {
-          // TODO
-        }
-      }
+    if(!tchecker::dbm::satisfies(symb_state->zone().dbm(), symb_state->zone().dim(), orig_min_ref)) {
+      std::cerr << __FILE__ << ": " << __LINE__ << ": the reset " << orig_min_ref << " is not fulfilled by" << std::endl;
+      std::cerr << __FILE__ << ": " << __LINE__ << ": vloc: "<< symb_state->vloc() << std::endl;
+      tchecker::dbm::output_matrix(std::cerr, symb_state->zone().dbm(), symb_state->zone().dim());
+      return false;
+    }
 
+    if(!tchecker::dbm::satisfies(symb_state->zone().dbm(), symb_state->zone().dim(), ref_min_orig)) {
+      std::cerr << __FILE__ << ": " << __LINE__ << ": the reset " << ref_min_orig << " is not fulfilled by" << std::endl;
+      std::cerr << __FILE__ << ": " << __LINE__ << ": vloc: "<< symb_state->vloc() << std::endl;
+      tchecker::dbm::output_matrix(std::cerr, symb_state->zone().dbm(), symb_state->zone().dim());
+      return false;
     }
   }
+  return true;
+}
+
+// used for assertion only
+bool all_vc_are_sub_vc_of_phi_a_or_phi_b(tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t> & lo_vc, 
+                                         tchecker::zg::const_state_sptr_t first, tchecker::zg::const_state_sptr_t second, tchecker::clock_id_t no_of_virt_clocks)
+{
+  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> phi_A = tchecker::virtual_constraint::factory(first->zone(), no_of_virt_clocks);
+  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> phi_B = tchecker::virtual_constraint::factory(second->zone(), no_of_virt_clocks);
+  bool result = true;
+
+  for(auto iter = lo_vc.begin(); iter < lo_vc.end(); iter++) {
+
+    assert(tchecker::dbm::is_tight((*iter)->dbm(), (*iter)->dim()));
+    assert(tchecker::dbm::is_consistent((*iter)->dbm(), (*iter)->dim()));
+
+    result &= ((*iter)->dim() == no_of_virt_clocks + 1);
+    result &= (tchecker::dbm::is_le((*iter)->dbm(), phi_A->dbm(), phi_A->dim()) || tchecker::dbm::is_le((*iter)->dbm(), phi_B->dbm(), phi_B->dim()));
+
+    if(!result) {
+      std::cout << __FILE__ << ": " << __LINE__ << ": problems with the return of check_for_virt_bisim" << std::endl << "phi_A is " << std::endl;
+      tchecker::dbm::output_matrix(std::cout, phi_A->dbm(), phi_A->dim());
+
+      std::cout << __FILE__ << ": " << __LINE__ << ": phi_B is " << std::endl;
+      tchecker::dbm::output_matrix(std::cout, phi_B->dbm(), phi_B->dim());
+
+      std::cout << __FILE__ << ": " << __LINE__ << ": returned vc is " << std::endl;
+      tchecker::dbm::output_matrix(std::cout, (*iter)->dbm(), (*iter)->dim());
+      return result;
+    }
+  }
+  return result;
+}
+
+// used for assertion only
+bool is_phi_subset_of_a_zone(const tchecker::dbm::db_t *dbm, tchecker::clock_id_t dim, tchecker::clock_id_t no_of_virt_clocks,
+                             const tchecker::virtual_constraint::virtual_constraint_t & phi_e)
+{
+  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> phi = tchecker::virtual_constraint::factory(dbm, dim, no_of_virt_clocks);
+
+  return tchecker::dbm::is_le(phi_e.dbm(), phi->dbm(), phi_e.dim());
+}
+
+std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
+Lieb_et_al::check_for_virt_bisim(tchecker::zg::const_state_sptr_t symb_state_first, tchecker::zg::transition_sptr_t symb_trans_first,
+                                 tchecker::zg::const_state_sptr_t symb_state_second, tchecker::zg::transition_sptr_t symb_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)
+{
+
+  if(!last_was_epsilon) {
+    assert(check_for_virt_bisim_preconditions_check(symb_state_first, symb_trans_first));
+    assert(check_for_virt_bisim_preconditions_check(symb_state_second, symb_trans_second));
+  }
+
+  _visited_pair_of_states++;
+
+  //std::cout << __FILE__ << ": " << __LINE__ << ": _visited_pair_of_states: " << _visited_pair_of_states << std::endl;
+  //std::cout << __FILE__ << ": " << __LINE__ << ": check-for-virt-bisim" << std::endl;
+  //std::cout << __FILE__ << ": " << __LINE__ << ": " << symb_state_first->vloc() << std::endl;
+  //tchecker::dbm::output_matrix(std::cout, symb_state_first->zone().dbm(), symb_state_first->zone().dim());
+
+  //std::cout << __FILE__ << ": " << __LINE__ << ": " << symb_state_second->vloc() << std::endl;
+  //tchecker::dbm::output_matrix(std::cout, symb_state_second->zone().dbm(), symb_state_second->zone().dim());
+
+  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>>(_A->get_no_of_virtual_clocks() + 1);
+
+  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> phi_A = tchecker::virtual_constraint::factory(symb_state_first->zone(), _A->get_no_of_virtual_clocks());
+  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> phi_B = tchecker::virtual_constraint::factory(symb_state_second->zone(), _A->get_no_of_virtual_clocks());
+
+  tchecker::zg::state_sptr_t A_synced = _A->clone_state(symb_state_first);
+  tchecker::zg::state_sptr_t B_synced = _B->clone_state(symb_state_second);
+
+  // Before we sync them, we have to ensure virtual equivalence
+  if(
+    tchecker::dbm::status_t::EMPTY == phi_B->logic_and(A_synced->zone(), symb_state_first->zone()) ||
+    tchecker::dbm::status_t::EMPTY == phi_A->logic_and(B_synced->zone(), symb_state_second->zone())
+    )
+  {
+    // this is a difference to the original function, done for efficiency reasons.
+    result->append_zone(phi_A);
+    result->append_zone(phi_B);
+    assert(all_vc_are_sub_vc_of_phi_a_or_phi_b(*result, symb_state_first, symb_state_second, _A->get_no_of_virtual_clocks()));
+    _delete_me++;
+    //std::cout << __FILE__ << ": " << __LINE__ << ": _delete_me: " << _delete_me << std::endl;
+    result->compress();
+    return result;
+  }
+
+  //std::cout << __FILE__ << ": " << __LINE__ << ": " << "virt_equiv A:" << std::endl;
+  //tchecker::dbm::output_matrix(std::cout, A_synced->zone().dbm(), A_synced->zone().dim());
+  //std::cout << __FILE__ << ": " << __LINE__ << ": " << "virt_equiv B:" << std::endl;
+  //tchecker::dbm::output_matrix(std::cout, B_synced->zone().dbm(), B_synced->zone().dim());
+
+  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> to_append_A 
+    = std::make_shared<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(_A->get_no_of_virtual_clocks() + 1);
+  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> to_append_B 
+    = std::make_shared<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(_B->get_no_of_virtual_clocks() + 1);
+
+  phi_B->neg_logic_and(to_append_A, *phi_A);
+  phi_A->neg_logic_and(to_append_B, *phi_B);
+
+  result->append_container(to_append_A);
+  result->append_container(to_append_B);
+
+  assert(all_vc_are_sub_vc_of_phi_a_or_phi_b(*result, symb_state_first, symb_state_second, _A->get_no_of_virtual_clocks()));
+
+  // now we can sync them. As we know: the targets of delay transitions are already synced!
+  if(!last_was_epsilon) {
+    tchecker::vcg::sync( A_synced->zone_ptr()->dbm(), B_synced->zone_ptr()->dbm(),
+                         A_synced->zone_ptr()->dim(), B_synced->zone_ptr()->dim(),
+                         _A->get_no_of_original_clocks(), _B->get_no_of_original_clocks(),
+                         symb_trans_first->reset_container(), symb_trans_second->reset_container());
+
+    //std::cout << __FILE__ << ": " << __LINE__ << ": " << "synced A:" << std::endl;
+    //tchecker::dbm::output_matrix(std::cout, A_synced->zone().dbm(), A_synced->zone().dim());
+    //std::cout << __FILE__ << ": " << __LINE__ << ": " << "synced B:" << std::endl;
+    //tchecker::dbm::output_matrix(std::cout, B_synced->zone().dbm(), B_synced->zone().dim());
+  }
+
+  assert(tchecker::vcg::are_dbm_synced(A_synced->zone_ptr()->dbm(), B_synced->zone_ptr()->dbm(),
+                                       A_synced->zone_ptr()->dim(), B_synced->zone_ptr()->dim(),
+                                       _A->get_no_of_original_clocks(), _B->get_no_of_original_clocks()));
+
+  // normalizing, checking whether we have already seen this pair.
+  tchecker::zg::state_sptr_t A_normed = _A->clone_state(A_synced);
+  tchecker::zg::state_sptr_t B_normed = _B->clone_state(B_synced);
+
+  _A->run_extrapolation(A_normed->zone().dbm(), A_normed->zone().dim(), *(A_normed->vloc_ptr()));
+  _B->run_extrapolation(B_normed->zone().dbm(), B_normed->zone().dim(), *(B_normed->vloc_ptr()));
+
+  std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t> normalized_pair{A_normed, B_normed};
+
+  if(visited.count(normalized_pair)) {
+    assert(all_vc_are_sub_vc_of_phi_a_or_phi_b(*result, symb_state_first, symb_state_second, _A->get_no_of_virtual_clocks()));
+    _delete_me++;
+    //std::cout << __FILE__ << ": " << __LINE__ << ": _delete_me: " << _delete_me << std::endl;
+    result->compress();
+    return result;
+  }
+
+  // If we haven't seen this pair, yet, add it to visited
+  visited.insert(normalized_pair);
+
+  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> lo_not_simulatable
+    = std::make_shared<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(_A->get_no_of_virtual_clocks() + 1);
+
+  if(!last_was_epsilon) {
+    // we check the outgoing epsilon transition
+    tchecker::zg::state_sptr_t A_epsilon = _A->clone_state(A_normed);
+    tchecker::zg::state_sptr_t B_epsilon = _B->clone_state(B_normed);
+
+    _A->semantics()->delay(A_epsilon->zone_ptr()->dbm(), A_epsilon->zone_ptr()->dim(), symb_trans_first->tgt_invariant_container());
+    _B->semantics()->delay(B_epsilon->zone_ptr()->dbm(), B_epsilon->zone_ptr()->dim(), symb_trans_second->tgt_invariant_container());
+
+    tchecker::zg::const_state_sptr_t const_A_epsilon{A_epsilon};
+    tchecker::zg::const_state_sptr_t const_B_epsilon{B_epsilon};
+
+    std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> result_epsilon
+      = check_for_virt_bisim(const_A_epsilon, symb_trans_first, const_B_epsilon, symb_trans_second, visited, true);
+
+    // 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));
+    }
+
+  }
+ else {
+
+    tchecker::zg::const_state_sptr_t const_A_normed{A_normed};
+    tchecker::zg::const_state_sptr_t const_B_normed{B_normed};
+
+    // now that we have checked the epsilon transition, we check the outgoing action transitions
+    lo_not_simulatable->append_container(check_for_outgoing_transitions(const_A_normed, const_B_normed, visited));
+  }
+
+  lo_not_simulatable->compress();
+
+  // now we have to revert the extrapolation
+
+  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> reverted_extrapolation
+    = std::make_shared<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(_A->get_no_of_virtual_clocks() + 1);
+
+  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> phi_synced = tchecker::virtual_constraint::factory(A_synced->zone(), _A->get_no_of_virtual_clocks()); // vc of A_synced and B_synced are the same
+
+  for(auto iter = lo_not_simulatable->begin(); iter < lo_not_simulatable->end(); iter++) {
+    std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> to_Add = tchecker::virtual_constraint::factory(_A->get_no_of_virtual_clocks());
+    if(tchecker::dbm::NON_EMPTY == tchecker::dbm::intersection(to_Add->dbm(), (*iter)->dbm(), phi_synced->dbm(), _A->get_no_of_virtual_clocks() + 1)) {
+      reverted_extrapolation->append_zone(to_Add);
+    }
+  }
+
+  reverted_extrapolation->compress();
+
+  // finally, we revert the sync
+
+  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> another_phi_A = tchecker::virtual_constraint::factory(symb_state_first->zone(), _A->get_no_of_virtual_clocks());
+  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> another_phi_B = tchecker::virtual_constraint::factory(symb_state_second->zone(), _B->get_no_of_virtual_clocks());
+
+  tchecker::zg::state_sptr_t A_clone = _A->clone_state(symb_state_first);
+  tchecker::zg::state_sptr_t B_clone = _B->clone_state(symb_state_second);
+
+  another_phi_A->logic_and(B_clone->zone(), symb_state_second->zone());
+  another_phi_B->logic_and(A_clone->zone(), symb_state_first->zone());
+
+  tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t> inter{_A->get_no_of_virtual_clocks() + 1};
+
+  for(auto iter = reverted_extrapolation->begin(); iter < reverted_extrapolation->end(); iter++) {
+    std::pair<std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>, std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>> sync_reverted
+      = 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)));
+  }
+
+  inter.compress();
+
+  assert(all_vc_are_sub_vc_of_phi_a_or_phi_b(inter, symb_state_first, symb_state_second, _A->get_no_of_virtual_clocks()));
+
+  result->append_container(tchecker::virtual_constraint::combine(inter, _A->get_no_of_virtual_clocks()));
+
+  assert(all_vc_are_sub_vc_of_phi_a_or_phi_b(*result, symb_state_first, symb_state_second, _A->get_no_of_virtual_clocks()));
+
+  _delete_me++;
+  //std::cout << __FILE__ << ": " << __LINE__ << ": _delete_me: " << _delete_me << std::endl;
+
+  result->compress();
+
+  return result;
+}
+
+
+std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
+Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t A_state,
+                                            tchecker::zg::const_state_sptr_t B_state,
+                                            std::unordered_set<std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t>, custom_hash, custom_equal> & visited)
+{
+
+  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> result
+     = std::make_shared<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(_A->get_no_of_virtual_clocks() + 1);
+
+  std::vector<tchecker::vcg::vcg_t::sst_t> v_first, v_second;
+  _A->next(A_state, v_first);
+  _B->next(B_state, v_second);
+
+  // vector of pointer to zone_container to store the return values regarding an outgoing transition
+  typedef std::vector<std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>> return_values;
+
+  // vector with an entry for each outgoing transition. For each outgoing trans, a vector of zone container is stored
+  typedef std::vector<return_values> lo_return_values; 
+
+  lo_return_values A_return_values;
+
+  lo_return_values B_return_values;
+
+
+  std::tuple<std::vector<tchecker::vcg::vcg_t::sst_t> *, lo_return_values *, tchecker::zg::const_state_sptr_t *> A_v_ret_val_pair
+                      = std::make_tuple<std::vector<tchecker::vcg::vcg_t::sst_t> *, lo_return_values *, tchecker::zg::const_state_sptr_t *>(&v_first, &A_return_values, &A_state);
+
+  std::tuple<std::vector<tchecker::vcg::vcg_t::sst_t> *, lo_return_values *, tchecker::zg::const_state_sptr_t *> B_v_ret_val_pair
+                      = std::make_tuple<std::vector<tchecker::vcg::vcg_t::sst_t> *, lo_return_values *, tchecker::zg::const_state_sptr_t *>(&v_second, &B_return_values, &B_state);
+
+  auto together = {&A_v_ret_val_pair, &B_v_ret_val_pair};
+
+  // init the return values of each outgoing transition.
+  // for A and B
+  for(auto iter : together) {
+    auto ret_val = std::get<1>(*iter);
+    // and for each outgoing transition
+    for(auto && [status, s, t] : *(std::get<0>(*iter))) {
+      // create a zone container
+      tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t> tmp{_A->get_no_of_virtual_clocks() + 1};
+      // that contains the target vc only
+      tmp.append_zone(tchecker::virtual_constraint::factory(s->zone(), _A->get_no_of_virtual_clocks()));
+      // add it to the vector of returned results
+      return_values init_returned_values;
+      init_returned_values.emplace_back(std::make_shared<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(tmp));
+      // and place it at the return values vector
+      ret_val->emplace_back(init_returned_values);
+    }
+  }
+
+  assert(A_return_values.size() == v_first.size());
+  assert(B_return_values.size() == v_second.size());
+
+  for (long unsigned int i = 0; i < v_first.size(); ++i) {
+
+    auto && [status_first, s_first, t_first] = v_first[i];
+    tchecker::zg::const_state_sptr_t const_s_first{s_first};
+
+    for(long unsigned int j = 0; j < v_second.size(); ++j) {
+      auto && [status_second, s_second, t_second] = v_second[j];
+            // the action has to be the same
+      if(!t_first->vedge().event_equal(_A->system(), t_second->vedge(), _B->system())) {
+        continue;
+      }
+
+      tchecker::zg::const_state_sptr_t const_s_second{s_second};
+      std::unordered_set<std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t>, custom_hash, custom_equal> copy(visited);
+
+      std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> inter
+        = this->check_for_virt_bisim(const_s_first, t_first, const_s_second, t_second, copy, false);
+
+      auto A_s_ret_val_idx = std::make_tuple<tchecker::intrusive_shared_ptr_t<tchecker::make_shared_t<tchecker::zg::state_t> >*, 
+                                             lo_return_values *,
+                                             long unsigned int *>(&s_first, &A_return_values, &i);
+
+
+      auto B_s_ret_val_idx = std::make_tuple<tchecker::intrusive_shared_ptr_t<tchecker::make_shared_t<tchecker::zg::state_t> >*, 
+                                             lo_return_values *,
+                                             long unsigned int *>(&s_second, &B_return_values, &j);
+
+      auto s_ret_val_idx_together = {&A_s_ret_val_idx, &B_s_ret_val_idx};
+
+      for(auto iter : s_ret_val_idx_together) {
+        auto s_cur = *(std::get<0>(*iter));
+        auto ret_val_cur = std::get<1>(*iter);
+        auto index_cur = std::get<2>(*iter);
+        tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t> to_add{_A->get_no_of_virtual_clocks() + 1};
+        for(auto iter = inter->begin(); iter < inter->end(); iter++) {
+          std::shared_ptr<tchecker::zg::zone_t> tmp = tchecker::zg::factory(s_cur->zone().dim());
+          if(tchecker::dbm::status_t::NON_EMPTY == (*iter)->logic_and(tmp, s_cur->zone())) {
+            to_add.append_zone(tchecker::virtual_constraint::factory(tmp, _A->get_no_of_virtual_clocks()));
+          }
+        }
+        to_add.compress();
+       (*ret_val_cur)[*index_cur].emplace_back(std::make_shared<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(to_add));
+      }
+    }
+  }
+
+  //std::cout << __FILE__ << ": " << __LINE__ << ": start revert_action_trans" << std::endl;
+
+  for(auto iter : together) {
+    auto v_cur = std::get<0>(*iter);
+    auto ret_val = std::get<1>(*iter);
+    for (long unsigned int i = 0; i < v_cur->size(); ++i) {
+      auto && [status_cur, s_cur, t_cur] = (*v_cur)[i];
+      std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> in_all =
+        tchecker::virtual_constraint::contained_in_all( std::ref((*ret_val)[i]), _A->get_no_of_virtual_clocks());
+
+      for(auto iter_in_all = in_all->begin(); iter_in_all < in_all->end(); iter_in_all++) {
+        if(!((*iter_in_all)->is_empty())) {
+            assert(is_phi_subset_of_a_zone(s_cur->zone().dbm(), s_cur->zone().dim(), (*iter_in_all)->get_no_of_virt_clocks(), **iter_in_all));
+            result->append_zone(tchecker::vcg::revert_action_trans((*(std::get<2>(*iter)))->zone(), t_cur->guard_container(), t_cur->reset_container(), t_cur->tgt_invariant_container(), **iter_in_all));
+        }
+      }
+    }
+
+  }
+
+  //std::cout << __FILE__ << ": " << __LINE__ << ": end revert_action_trans" << std::endl;
+
+  assert(
+    std::all_of(result->begin(), result->end(),
+                [A_state, B_state](std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> vc)
+                {
+                  return (is_phi_subset_of_a_zone(A_state->zone().dbm(), A_state->zone().dim(), vc->get_no_of_virt_clocks(), *vc)) ||
+                         (is_phi_subset_of_a_zone(B_state->zone().dbm(), B_state->zone().dim(), vc->get_no_of_virt_clocks(), *vc));
+                }
+    )
+  );
+
+  result->compress();
+
+  //std::cout << __FILE__ << ": " << __LINE__ << ": return from check-outgoing-trans" << std::endl;
+
+  return result;
+
 }
 
 } // end of namespace strong_timed_bisim

src/tck-compare/tck-compare.cc

@@ -123,9 +123,9 @@ int parse_command_line(int argc, char * argv[])
  of errors
  \post all errors have been reported to std::cerr
  */
-tchecker::parsing::system_declaration_t * load_system_declaration(std::string const & filename)
+std::shared_ptr<tchecker::parsing::system_declaration_t> load_system_declaration(std::string const & filename)
 {
-  tchecker::parsing::system_declaration_t * sysdecl = nullptr;
+  std::shared_ptr<tchecker::parsing::system_declaration_t> sysdecl = nullptr;
   try {
     sysdecl = tchecker::parsing::parse_system_declaration(filename);
     if (sysdecl == nullptr)
@@ -147,12 +147,8 @@ tchecker::parsing::system_declaration_t * load_system_declaration(std::string co
 void strong_timed_bisim(std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl_first, std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl_second)
 {
 
-  std::cout << "tck-compare.cc: run" << std::endl;
-
   auto stats = tchecker::tck_compare::vcg_timed_bisim::run(sysdecl_first, sysdecl_second, os, block_size, table_size);
 
-  std::cerr << "tck-compare.cc : print stats" << std::endl;
-
   // stats
   std::map<std::string, std::string> m;
   stats.attributes(m);

src/tck-compare/vcg-timed-bisim.cc

@@ -73,8 +73,6 @@ run(std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl_fir
 
   std::vector<std::shared_ptr<tchecker::ta::system_t>> systems;
 
-  std::cout << "vcg-timed-bisim.cc : run" << std::endl;
-
   for(size_t i = 0; i < 2; ++i) {
     std::shared_ptr<tchecker::ta::system_t> cur_system{new tchecker::ta::system_t{ (i == 0) ? *sysdecl_first : *sysdecl_second}};
     std::shared_ptr<tchecker::syncprod::system_t const> system_syncprod = std::make_shared<tchecker::syncprod::system_t const>(cur_system->as_syncprod_system());
@@ -90,99 +88,16 @@ run(std::shared_ptr<tchecker::parsing::system_declaration_t> const & sysdecl_fir
   for(size_t i = 0; i < 2; ++i) {
     std::shared_ptr<tchecker::strong_timed_bisim::system_virtual_clocks_t const> extended_system{new tchecker::strong_timed_bisim::system_virtual_clocks_t{*(systems[i]), no_of_virt_clocks, 0 == i}};
     std::shared_ptr<tchecker::vcg::vcg_t> vcg{tchecker::vcg::factory(extended_system, 0 == i, systems[0], systems[1], tchecker::ts::SHARING, tchecker::zg::DISTINGUISHED_SEMANTICS,
-                                                               tchecker::zg::EXTRA_K_NORM, block_size, table_size)};
+                                                               tchecker::zg::EXTRA_M_GLOBAL, block_size, table_size)};
     vcgs.push_back(vcg);
   }
 
-  std::cout << "vcg-timed-bisim.cc : created vcgs" << std::endl;
+//  std::cout << __FILE__ << ": " << __LINE__ << ": created vcgs" << std::endl;
 
   auto algorithm = new tchecker::strong_timed_bisim::Lieb_et_al(vcgs[0], vcgs[1]);
 
   return algorithm->run();
 
-
-  /* DELETE ME!
-
-  std::cout << "no. of processes: " << system_first->processes_count() << std::endl;
-  std::cout << "no. of processes of product: " << product_first->processes_count() << std::endl;
-
-  auto r = system_first->attributes().range();
-  auto begin = r.begin(), end = r.end();
-
-  std::cout << "loop system attributes" << std::endl;
-
-  for(auto it = begin; it != end; ++it) {
-    std::cout << "found attribute: " << (*it).key() << ":" << (*it).value() << std::endl;
-  }
-
-  auto p = product_first->attributes().range();
-  auto pbegin = p.begin(), pend = p.end();
-
-  std::cout << "loop product attributes" << std::endl;
-
-  for(auto it = pbegin; it != pend; ++it) {
-    std::cout << "found attribute: " << (*it).key() << ":" << (*it).value() << std::endl;
-  }
-
-  auto r_l = system_first->locations();
-  auto begin_l = r_l.begin(), end_l = r_l.end();
-
-  std::cout << "loop system locations" << std::endl;
-
-  for(auto it = begin_l; it != end_l; ++it) {
-    std::cout << "found location: " << (*it)->name() << std::endl;
-  }
-
-  auto p_l = product_first->locations();
-  auto begin_p_l = p_l.begin(), end_p_l = p_l.end();
-
-  std::cout << "loop product locations" << std::endl;
-
-  for(auto it = begin_p_l; it != end_p_l; ++it) {
-    std::cout << "found location: " << (*it)->name() << std::endl;
-  }
-
-  std::cout << "initial system locations" << std::endl;
-
-  for(std::size_t i = 0; i < system_first->processes_count(); ++i) {
-      auto r_init = system_first->initial_locations(i);
-      auto begin_init = r_init.begin(), end_init = r_init.end();
-
-    for(auto it = begin_init; it != end_init; ++it) {
-      std::cout << "found initial location for process " << i << "(" << system_first->process_name(i) << "): " << (*it)->name() << std::endl;
-    }
-  }
-
-  std::cout << "initial product locations" << std::endl;
-
-  auto p_init = product_first->initial_locations(0);
-  auto begin_init = p_init.begin(), end_init = p_init.end();
-
-  for(auto it = begin_init; it != end_init; ++it) {
-      std::cout << "found initial location for process " << 0 << "(" << product_first->process_name(0) << "): " << (*it)->name() << std::endl;
-  }
-
-  auto r_c = system_first->clock_variables().identifiers();
-  auto begin_c = r_c.begin(), end_c = r_c.end();
-
-  std::cout << "loop system clocks" << std::endl;
-
-  for(auto it = begin_c; it != end_c; ++it) {
-    std::cout << "found clock: " << it << ": " << system_first->clock_name(it) << std::endl;
-  }
-
-  auto p_c = product_first->clock_variables().identifiers();
-  auto begin_p_c = p_c.begin(), end_p_c = p_c.end();
-
-  std::cout << "loop product clocks" << std::endl;
-
-    for(auto it = begin_p_c; it != end_p_c; ++it) {
-    std::cout << "found clock: " << it << ": " << product_first->clock_name(it) << std::endl;
-  }
-
-
-  /* UNTIL ME! */
-
 }
 
 } // end of namespace vcg_timed_bisim

src/utils/zone_container.cc

@@ -9,39 +9,6 @@
 
 namespace tchecker {
 
-zone_container_t<tchecker::zg::zone_t> contained_in_all(std::vector<zone_container_t<tchecker::zg::zone_t>> & zones, tchecker::clock_id_t dim)
-{
-
-  if (zones.empty()) {
-    zone_container_t<tchecker::zg::zone_t> result(dim);
-    return result;
-  }
-
-  if (1 == zones.size()) {
-    return zones[0];
-  }
-
-  zone_container_t<tchecker::zg::zone_t> cur = zones.back();
-  zones.pop_back();
-
-  zone_container_t<tchecker::zg::zone_t> inter = contained_in_all(zones, dim);
-
-  zone_container_t<tchecker::zg::zone_t> result{dim};
-
-  for(auto iter_cur = cur.begin(); iter_cur < cur.end(); iter_cur++) {
-    for(auto iter_inter = inter.begin(); iter_inter < inter.end(); iter_inter++) {
-      std::shared_ptr<tchecker::zg::zone_t> tmp = tchecker::zg::factory(dim);
-      if(tchecker::dbm::NON_EMPTY == tchecker::dbm::intersection(tmp->dbm(), (**iter_cur).dbm(), (**iter_inter).dbm(), (**iter_cur).dim())) {
-        result.append_zone(tmp);
-      }
-      else {
-        tchecker::zg::zone_t::destruct(&(*tmp));
-      }
-    }
-  }
-  return result;
-}
-
 // specializations
 template<>
 std::shared_ptr<tchecker::zg::zone_t> zone_container_t<tchecker::zg::zone_t>::create_element()
@@ -58,7 +25,7 @@ std::shared_ptr<tchecker::zg::zone_t> zone_container_t<tchecker::zg::zone_t>::cr
 template<>
 std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>::create_element()
 {
-  return tchecker::virtual_constraint::factory(_dim);
+  return tchecker::virtual_constraint::factory(_dim - 1);
 }
 
 template<>

src/vcg/revert_transitions.cc

@@ -7,6 +7,53 @@
 
 #include "tchecker/vcg/revert_transitions.hh"
 
+
+namespace tchecker {
+
+namespace vcg {
+
+bool check_whether_phi_is_subset_of_target(
+                    const tchecker::zg::zone_t & zone,
+                    const tchecker::clock_constraint_container_t & guard,
+                    const tchecker::clock_reset_container_t & reset,
+                    const tchecker::clock_constraint_container_t & tgt_invariant,
+                    const tchecker::virtual_constraint::virtual_constraint_t & phi_split)
+{
+  tchecker::dbm::db_t target_dbm[zone.dim()*zone.dim()];
+  zone.to_dbm(target_dbm);
+
+  tchecker::dbm::constrain(target_dbm, zone.dim(), guard);
+
+  if(!tchecker::dbm::is_tight(target_dbm, zone.dim())) {
+    std::cerr << __FILE__ << ": " << __LINE__ << ": target_dbm is not tight" << std::endl;
+    return false;
+  }
+
+  if(!tchecker::dbm::is_consistent(target_dbm, zone.dim())) {
+    std::cerr << __FILE__ << ": " << __LINE__ << ": target_dbm is not consistent" << std::endl;
+    return false;
+  }
+
+  tchecker::dbm::reset(target_dbm, zone.dim(), reset);
+  tchecker::dbm::constrain(target_dbm, zone.dim(), tgt_invariant);
+
+  if(!tchecker::dbm::is_tight(target_dbm, zone.dim())) {
+    std::cerr << __FILE__ << ": " << __LINE__ << ": target_dbm is not tight" << std::endl;
+    return false;
+  }
+
+  if(!tchecker::dbm::is_consistent(target_dbm, zone.dim())) {
+    std::cerr << __FILE__ << ": " << __LINE__ << ": target_dbm is not consistent" << std::endl;
+    return false;
+  }
+
+  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> target_vc 
+    = tchecker::virtual_constraint::factory(target_dbm, zone.dim(), phi_split.get_no_of_virt_clocks());
+
+  return tchecker::dbm::is_le(phi_split.dbm(), target_vc->dbm(), target_vc->dim());
+
+}
+
 std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>
 revert_action_trans(const tchecker::zg::zone_t & zone,
                     const tchecker::clock_constraint_container_t & guard,
@@ -14,39 +61,59 @@ revert_action_trans(const tchecker::zg::zone_t & zone,
                     const tchecker::clock_constraint_container_t & tgt_invariant,
                     const tchecker::virtual_constraint::virtual_constraint_t & phi_split)
 {
+  assert(!zone.is_empty());
+  assert(!phi_split.is_empty());
 
-  tchecker::clock_reset_container_t reset_copy;
+  assert(tchecker::dbm::is_tight(zone.dbm(), zone.dim()));
+  assert(tchecker::dbm::is_consistent(zone.dbm(), zone.dim()));
 
-  reset_copy.reserve(reset.size());
+  assert(tchecker::dbm::is_tight(phi_split.dbm(), phi_split.dim()));
+  assert(tchecker::dbm::is_consistent(phi_split.dbm(), phi_split.dim()));
 
-  std::copy(reset.begin(), reset.end(), reset_copy.begin());
-
-  tchecker::dbm::db_t zone_clone[zone.dim()*zone.dim()];
-  zone.to_dbm(zone_clone);
+  assert(check_whether_phi_is_subset_of_target(zone, guard, reset, tgt_invariant, phi_split));
 
+  // 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).
   tchecker::dbm::db_t d_land_g[zone.dim()*zone.dim()];
   zone.to_dbm(d_land_g);
 
-  tchecker::dbm::constrain(d_land_g, zone.dim(), guard);
+  assert(tchecker::dbm::is_tight(d_land_g, zone.dim()));
+  assert(tchecker::dbm::is_consistent(d_land_g, zone.dim()));
 
+  tchecker::dbm::constrain(d_land_g, zone.dim(), guard);
 
   tchecker::dbm::db_t r_d_land_g_land_phi[zone.dim()*zone.dim()];
   tchecker::dbm::copy(r_d_land_g_land_phi, d_land_g, zone.dim());
 
   tchecker::dbm::reset(r_d_land_g_land_phi, zone.dim(), reset);
-  tchecker::dbm::constrain(r_d_land_g_land_phi, zone.dim(), phi_split.get_vc(zone.dim() - phi_split.dim()));
+
+  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()));
+
+  // now we have calculated R(zone && g) and we have to land this with the given virtual constrain
+  tchecker::dbm::constrain(r_d_land_g_land_phi, zone.dim(), phi_split.get_vc(zone.dim() - phi_split.dim(), true));
+
+  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);
 
   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::constrain(zone_clone, zone.dim(), virt_mult_reset->get_vc(zone.dim() - phi_split.dim()));
+
+  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;
 }
 
@@ -60,14 +127,15 @@ revert_epsilon_trans(const tchecker::zg::zone_t & zone, const tchecker::virtual_
 
   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()));
+  tchecker::dbm::constrain(zone_copy->dbm(), zone_copy->dim(), phi_copy->get_vc(zone_copy->dim() - phi_copy->dim(), true));
 
   std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> result
     = tchecker::virtual_constraint::factory(zone_copy, phi_split.get_no_of_virt_clocks());
 
-  tchecker::zg::zone_destruct_and_deallocate(&(*phi_copy));
-  tchecker::zg::zone_destruct_and_deallocate(&(*phi_copy));
-
   return result;
 }
 
+} // end of namespace vcg
+
+} // end of namespace tchecker
+

src/vcg/sync.cc

@@ -6,18 +6,103 @@
  */
 
 #include "tchecker/vcg/sync.hh"
-#include "tchecker/dbm/dbm.hh"
+
+namespace tchecker {
+
+namespace vcg {
+
+bool is_virtually_equivalent(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2,
+                                tchecker::clock_id_t dim1, tchecker::clock_id_t dim2,
+                                tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2)
+{
+  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> vc1 
+    = tchecker::virtual_constraint::factory(dbm1, dim1, dim1 - no_of_orig_clocks_1 - 1);
+
+  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> vc2 
+    = tchecker::virtual_constraint::factory(dbm2, dim2, dim2 - no_of_orig_clocks_2 - 1);
+
+  return (*vc1 == *vc2);
+}
 
 
-void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, tchecker::clock_id_t dim, 
-          tchecker::clock_id_t lowest_virt_clk_id, tchecker::clock_id_t no_of_orig_clocks_1,
+bool are_dbm_synced(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2,
+                    tchecker::clock_id_t dim1, tchecker::clock_id_t dim2,
+                    tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2)
+{
+
+  assert(dbm1 != nullptr);
+  assert(dbm2 != nullptr);
+
+  assert(dim1 >= 1);
+  assert(dim2 >= 1);
+
+  assert(tchecker::dbm::is_consistent(dbm1, dim1));
+  assert(tchecker::dbm::is_consistent(dbm2, dim2));
+  assert(tchecker::dbm::is_tight(dbm1, dim1));
+  assert(tchecker::dbm::is_tight(dbm2, dim2));
+
+  assert(no_of_orig_clocks_1 >= 1);
+  assert(no_of_orig_clocks_2 >= 1);
+
+  assert(dim1 == no_of_orig_clocks_1 + no_of_orig_clocks_1 + no_of_orig_clocks_2 + 1);
+  assert(dim2 == no_of_orig_clocks_1 + no_of_orig_clocks_2 + no_of_orig_clocks_2 + 1);
+
+  bool result = is_virtually_equivalent(dbm1, dbm2, dim1, dim2, no_of_orig_clocks_1, no_of_orig_clocks_2);
+
+  if(!result) {
+    std::cout << __FILE__ << ": " << __LINE__ << ": the dbm are not virtually equivalent." << std::endl;
+    tchecker::dbm::output_matrix(std::cout, dbm1, dim1);
+    tchecker::dbm::output_matrix(std::cout, dbm2, dim2);
+    return result;
+  }
+
+  for(tchecker::clock_id_t i = 1; i <= no_of_orig_clocks_1; ++i) {
+    tchecker::dbm::db_t * orig_min_virt = tchecker::dbm::access(dbm1, dim1, i, i + no_of_orig_clocks_1);
+    tchecker::dbm::db_t * virt_min_orig = tchecker::dbm::access(dbm1, dim1, i + no_of_orig_clocks_1, i);
+
+    result &= (*orig_min_virt == *virt_min_orig);
+    result &= (orig_min_virt->cmp == tchecker::LE);
+    result &= (orig_min_virt->value == 0);
+    if(!result) {
+      std::cout << __FILE__ << ": " << __LINE__ << ": " << i << " virtual and original clock of first dbm are not equivalent" << std::endl;
+      tchecker::dbm::output_matrix(std::cout, dbm1, dim1);
+      return result;
+    }
+  }
+
+  for(tchecker::clock_id_t i = 1; i <= no_of_orig_clocks_2; ++i) {
+    tchecker::dbm::db_t * orig_min_virt = tchecker::dbm::access(dbm2, dim2, i, i + no_of_orig_clocks_1 + no_of_orig_clocks_2);
+    tchecker::dbm::db_t * virt_min_orig = tchecker::dbm::access(dbm2, dim2, i + no_of_orig_clocks_1 + no_of_orig_clocks_2, i);
+
+    result &= (*orig_min_virt == *virt_min_orig);
+    result &= (orig_min_virt->cmp == tchecker::LE);
+    result &=(orig_min_virt->value == 0);
+    if(!result) {
+      std::cout << __FILE__ << ": " << __LINE__ << ": " << i << " virtual and original clock of second dbm are not equivalent" << std::endl;
+      tchecker::dbm::output_matrix(std::cout, dbm2, dim2);
+      return result;
+    }
+  }
+
+  return result;
+}
+
+bool is_phi_subset_of_a_zone(const tchecker::dbm::db_t *dbm, tchecker::clock_id_t dim, tchecker::clock_id_t no_of_orig_clocks,
+                             const tchecker::virtual_constraint::virtual_constraint_t & phi_e)
+{
+  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());
+}
+
+void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2,
+          tchecker::clock_id_t dim1, tchecker::clock_id_t dim2,
+          tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2,
           tchecker::clock_reset_container_t const & orig_reset1,
           tchecker::clock_reset_container_t const & orig_reset2)
 {
 
-  // TODO: add assertions
-
-  tchecker::clock_reset_container_t virt_resets;
+  assert(is_virtually_equivalent(dbm1, dbm2, dim1, dim2, no_of_orig_clocks_1, no_of_orig_clocks_2));
 
   for(const tchecker::clock_reset_t & r : orig_reset1) {
 
@@ -25,77 +110,115 @@ void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, tchecker::clock_
       throw std::runtime_error("when checking for timed bisim, only resets to value zero are allowed");
     }
 
-    reset_to_value(dbm1, dim, r.left_id() + 1 + lowest_virt_clk_id, 0);
-    reset_to_value(dbm2, dim, r.left_id() + 1 + lowest_virt_clk_id, 0);
+    reset_to_value(dbm1, dim1, r.left_id() + 1 + no_of_orig_clocks_1, 0);
+    reset_to_value(dbm2, dim2, r.left_id() + 1 + no_of_orig_clocks_2, 0);
   }
 
-  tchecker::clock_id_t border = lowest_virt_clk_id + no_of_orig_clocks_1;
-
   for(const tchecker::clock_reset_t & r : orig_reset2) {
 
     if(r.right_id() != tchecker::REFCLOCK_ID || r.value() != 0) {
       throw std::runtime_error("when checking for timed bisim, only resets to value zero are allowed");
     }
 
-    reset_to_value(dbm1, dim, r.left_id() + 1 + border, 0);
-    reset_to_value(dbm2, dim, r.left_id() + 1 + border, 0);
+    reset_to_value(dbm1, dim1, r.left_id() + 1 + no_of_orig_clocks_1 + no_of_orig_clocks_1, 0);
+    reset_to_value(dbm2, dim2, r.left_id() + 1 + no_of_orig_clocks_2 + no_of_orig_clocks_1, 0);
   }
 
-  virt_resets.clear();
-
+  assert(are_dbm_synced(dbm1, dbm2, dim1, dim2, no_of_orig_clocks_1, no_of_orig_clocks_2));
 }
 
-std::tuple<std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>, std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>>
-revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2, tchecker::clock_id_t dim, 
-            const tchecker::virtual_constraint::virtual_constraint_t & phi_e, tchecker::clock_id_t lowest_virt_clk_id,
-            tchecker::clock_id_t no_of_orig_clocks_1)
+
+
+std::pair<std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>, std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t>>
+revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2,
+            tchecker::clock_id_t dim1, tchecker::clock_id_t dim2,
+            tchecker::clock_id_t no_of_orig_clocks_1, tchecker::clock_id_t no_of_orig_clocks_2,
+            const tchecker::virtual_constraint::virtual_constraint_t & phi_e)
 {
 
-  // TODO add assertions
+  assert(is_virtually_equivalent(const_cast<tchecker::dbm::db_t *>(dbm1), const_cast<tchecker::dbm::db_t *>(dbm2), dim1, dim2, no_of_orig_clocks_1, no_of_orig_clocks_2));
 
-  tchecker::dbm::db_t zero_value = tchecker::dbm::db(tchecker::LT, 0);
-  tchecker::clock_reset_container_t reset_set;
+  // due to the fact that the number of original clocks might differ, we need to build two reset sets
+  tchecker::clock_reset_container_t orig_reset_set_A;
+  tchecker::clock_reset_container_t orig_reset_set_B;
 
-  for(tchecker::clock_id_t i = 1; i < (dim - lowest_virt_clk_id); ++i) {
-    if(zero_value == *tchecker::dbm::access(dbm1, dim, i, 0) && zero_value == *tchecker::dbm::access(dbm1, dim, 0, i)) {
-        tchecker::clock_reset_t tmp{i + lowest_virt_clk_id - 1, tchecker::REFCLOCK_ID, 0};
-        reset_set.emplace_back(tmp);
+  tchecker::clock_reset_container_t virt_reset_set_A;
+  tchecker::clock_reset_container_t virt_reset_set_B;
+
+  for(tchecker::clock_id_t i = 0; i < no_of_orig_clocks_1; ++i) {
+    if(tchecker::dbm::LE_ZERO == *tchecker::dbm::access(dbm1, dim1, i+1, 0) && tchecker::dbm::LE_ZERO == *tchecker::dbm::access(dbm1, dim1, 0, i+1)) {
+
+        tchecker::clock_reset_t orig_tmp{i, tchecker::REFCLOCK_ID, 0};
+
+        tchecker::clock_reset_t virt_tmp_A{i + no_of_orig_clocks_1, tchecker::REFCLOCK_ID, 0};
+        tchecker::clock_reset_t virt_tmp_B{i + no_of_orig_clocks_2, tchecker::REFCLOCK_ID, 0};
+
+        orig_reset_set_A.emplace_back(orig_tmp);
+
+        virt_reset_set_A.emplace_back(virt_tmp_A);
+        virt_reset_set_B.emplace_back(virt_tmp_B);
     }
   }
 
-  for(tchecker::clock_id_t i = 1; i < (dim - lowest_virt_clk_id); ++i) {
-    if(zero_value == *tchecker::dbm::access(dbm2, dim, i, 0) && zero_value == *tchecker::dbm::access(dbm2, dim, 0, i)) {
-        tchecker::clock_reset_t tmp{i + lowest_virt_clk_id + no_of_orig_clocks_1 - 1, tchecker::REFCLOCK_ID, 0};
-        reset_set.emplace_back(tmp);
+  for(tchecker::clock_id_t i = 0; i < no_of_orig_clocks_2; ++i) {
+    if(tchecker::dbm::LE_ZERO == *tchecker::dbm::access(dbm2, dim2, i+1, 0) && tchecker::dbm::LE_ZERO == *tchecker::dbm::access(dbm2, dim2, 0, i+1)) {
+
+        tchecker::clock_reset_t orig_tmp{i, tchecker::REFCLOCK_ID, 0};
+
+        tchecker::clock_reset_t virt_tmp_A{i + no_of_orig_clocks_1 + no_of_orig_clocks_1, tchecker::REFCLOCK_ID, 0};
+        tchecker::clock_reset_t virt_tmp_B{i + no_of_orig_clocks_1 + no_of_orig_clocks_2, tchecker::REFCLOCK_ID, 0};
+
+        orig_reset_set_B.emplace_back(orig_tmp);
+
+        virt_reset_set_A.emplace_back(virt_tmp_A);
+        virt_reset_set_B.emplace_back(virt_tmp_B);
     }
   }
 
-  tchecker::dbm::db_t dbm1_clone[dim*dim];
-  tchecker::dbm::copy(dbm1_clone, dbm1, dim);
+  tchecker::dbm::db_t dbm1_synced[dim1*dim1];
+  tchecker::dbm::copy(dbm1_synced, dbm1, dim1);
+  tchecker::dbm::db_t dbm2_synced[dim2*dim2];
+  tchecker::dbm::copy(dbm2_synced, dbm2, dim2);
 
-  tchecker::dbm::constrain(dbm1_clone, dim, phi_e.get_vc(lowest_virt_clk_id - 1));
+  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);
 
-  tchecker::dbm::db_t dbm2_clone[dim*dim];
-  tchecker::dbm::copy(dbm2_clone, dbm2, dim);
+  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));
 
-  tchecker::dbm::constrain(dbm2_clone, dim, phi_e.get_vc(lowest_virt_clk_id - 1));
+  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
+  }
 
-  tchecker::dbm::db_t * multiple_reset = revert_multiple_reset(dbm1, dim, dbm1_clone, reset_set);
+  if(tchecker::dbm::status_t::EMPTY == tchecker::dbm::constrain(dbm2_synced, dim2, phi_e.get_vc(no_of_orig_clocks_2, true))) {
+    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);
 
   std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> first
-    = tchecker::virtual_constraint::factory(multiple_reset, dim, dim - lowest_virt_clk_id);
+    = 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, dim, dbm2_clone, reset_set);
+  multiple_reset = revert_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, dim, dim - lowest_virt_clk_id);
+    = tchecker::virtual_constraint::factory(multiple_reset, dim2, no_of_orig_clocks_1 + no_of_orig_clocks_2);
 
   free(multiple_reset);
 
-  reset_set.clear();
+  orig_reset_set_A.clear();
+  orig_reset_set_B.clear();
 
-  return std::make_tuple(first, second);
+
+  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));
+
+  return std::make_pair(first, second);
 }
 
+} // end of namespace vcg
+
+} // end of namespace tchecker

src/vcg/vcg.cc

@@ -14,7 +14,7 @@ namespace vcg {
 vcg_t::vcg_t(std::shared_ptr<tchecker::ta::system_t const> const & system, enum tchecker::ts::sharing_type_t sharing_type,
               std::shared_ptr<tchecker::zg::semantics_t> const & semantics, tchecker::clock_id_t no_of_virtual_clocks,
               std::shared_ptr<tchecker::zg::extrapolation_t> const & extrapolation, std::size_t block_size, std::size_t table_size)
-  : tchecker::zg::zg_t(system, sharing_type, semantics, extrapolation, block_size, table_size),
+  : tchecker::zg::zg_t(system, sharing_type, semantics, extrapolation, block_size, table_size, false),
     _no_of_virtual_clocks(no_of_virtual_clocks)
 {
 }

src/vcg/virtual_constraint.cc

@@ -11,116 +11,172 @@ namespace tchecker {
 
 namespace virtual_constraint {
 
-const tchecker::clock_id_t virtual_constraint_t::get_no_of_virt_clocks() const
+tchecker::clock_id_t virtual_constraint_t::get_no_of_virt_clocks() const
 {
   return this->dim() - 1;
 }
 
-// WARNING: above might not be tight after this call
-void insert_values(std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> to_change, tchecker::clock_id_t i, tchecker::clock_id_t j)
-{
-
-  tchecker::dbm::db_t * j_minus_i = tchecker::dbm::access(to_change->dbm(), to_change->dim(), j, i);
-  tchecker::dbm::db_t * i_minus_j = tchecker::dbm::access(to_change->dbm(), to_change->dim(), i, j);
-
-  tchecker::dbm::db_t db_above{
-                        (tchecker::LE == tchecker::dbm::comparator(*i_minus_j)) ? tchecker::LT : tchecker::LE,
-                        tchecker::dbm::value(*i_minus_j)};
-
-  *j_minus_i = db_above;
-  *i_minus_j = tchecker::dbm::LT_INFINITY;
-}
-
 // WARNING: The vitrual constraints placed at result are NOT tight!
-void add_neg(tchecker::zone_container_t<virtual_constraint_t> *result, const virtual_constraint_t *cur, tchecker::clock_id_t i, tchecker::clock_id_t j)
+void add_neg_single(tchecker::zone_container_t<virtual_constraint_t> *result, const virtual_constraint_t & cur, tchecker::clock_id_t i, tchecker::clock_id_t j, tchecker::dbm::db_t *max_value)
 {
-    // we first insert all clock valuations for which chi_i - chi_j is to high
-  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> above = tchecker::virtual_constraint::factory(*cur);
-  insert_values(above, i, j);
-  result->append_zone(above);
 
-  // now we insert all clocks for which chi_i - chi_j is to low
-  std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> below = tchecker::virtual_constraint::factory(*cur);
-  insert_values(below, j, i);
-  result->append_zone(below);
+  // the first line is a special case since the value of 0 - c cannot become larger than zero.
+  tchecker::dbm::db_t upper_bound = ((0 == i) && (tchecker::dbm::LE_ZERO < *max_value)) ? tchecker::dbm::LE_ZERO : *max_value;
+
+  // if the upper constraint is larger than the upper bound, the inverse is empty anyway.
+  if(*tchecker::dbm::access(cur.dbm(), cur.dim(), i, j) < upper_bound) {
+
+    tchecker::dbm::db_t copy{tchecker::dbm::invert(*tchecker::dbm::access(cur.dbm(), cur.dim(), i, j))};
+    std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> to_insert = tchecker::virtual_constraint::factory(cur);
+
+    // we remove what is allowed by cur, by setting the entry j - i to the inverse of cur[i][j], and add what is not allowed, by setting i - j to LT_INFINITY
+
+    tchecker::dbm::db_t * j_minus_i = tchecker::dbm::access(to_insert->dbm(), to_insert->dim(), j, i);
+    tchecker::dbm::db_t * i_minus_j = tchecker::dbm::access(to_insert->dbm(), to_insert->dim(), i, j);
+
+    *j_minus_i = copy;
+    *i_minus_j = upper_bound;
+
+    result->append_zone(to_insert);
+  }
 }
 
-tchecker::zone_container_t<virtual_constraint_t> * virtual_constraint_t::neg() const
+void 
+add_neg(tchecker::zone_container_t<virtual_constraint_t> *result, const virtual_constraint_t & cur, 
+        tchecker::clock_id_t i, tchecker::clock_id_t j, 
+        tchecker::dbm::db_t *max_i_minus_j, tchecker::dbm::db_t *max_j_minus_i)
+{
+
+  // we first add the neg breaking the upper bound of i-j
+  add_neg_single(result, cur, i, j, max_i_minus_j);
+  // we afterwards add the neg breaking the upper bound of j - i
+  add_neg_single(result, cur, j, i, max_j_minus_i);
+}
+
+std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> virtual_constraint_t::neg_helper(tchecker::dbm::db_t *upper_bounds) const
 {
   tchecker::zone_container_t<virtual_constraint_t> inter{this->dim()};
 
   for(tchecker::clock_id_t i = 0; i < this->dim(); ++i) {
     for(tchecker::clock_id_t j = i+1; j < this->dim(); ++j) {
 
-      tchecker::clock_id_t size_before = inter.size();
+      tchecker::zone_container_t<virtual_constraint_t> helper{this->dim()};
+      helper.append_container(inter); // this way, only the pointers are copied.
 
-      add_neg(&inter, this, i, j);
+      tchecker::dbm::db_t * i_minus_j = tchecker::dbm::access(upper_bounds, this->dim(), i, j);
+      tchecker::dbm::db_t * j_minus_i = tchecker::dbm::access(upper_bounds, this->dim(), j, i);
+
+      add_neg(&inter, *this, i, j, i_minus_j, j_minus_i);
 
       // do the same for all already added virtual constraints.
-      for(tchecker::clock_id_t iter = 0; iter < size_before; ++iter) {
-        add_neg(&inter, &(*(inter[iter])), i, j);
+      for(auto iter = helper.begin(); iter < helper.end(); iter++) {
+        add_neg(&inter, **iter, i, j, i_minus_j, j_minus_i);
       }
     }
   }
 
-  tchecker::zone_container_t<virtual_constraint_t> * result = new tchecker::zone_container_t<virtual_constraint_t>(this->dim());
+  std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> result = std::make_shared<tchecker::zone_container_t<virtual_constraint_t>>(this->dim());
 
   for(auto iter = inter.begin(); iter < inter.end(); iter++) {
-    if(tchecker::dbm::NON_EMPTY == tchecker::dbm::tighten((*iter)->dbm(), (*iter)->dim())) {
+    if(tchecker::dbm::NON_EMPTY ==tchecker::dbm::tighten((*iter)->dbm(), (*iter)->dim()) &&
+       tchecker::dbm::NON_EMPTY == tchecker::dbm::intersection((*iter)->dbm(), (*iter)->dbm(), upper_bounds, (*iter)->dim())) {
       result->append_zone(*iter);
-    } else {
-      tchecker::virtual_constraint::destruct(&(**iter));
     }
   }
 
   return result;
 }
 
-clock_constraint_container_t virtual_constraint_t::get_vc(tchecker::clock_id_t orig_clocks_offset) const
+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);
+}
+
+clock_constraint_container_t virtual_constraint_t::get_vc(tchecker::clock_id_t no_of_orig_clocks, bool system_clocks) const
+{
+
+  tchecker::clock_id_t ref_clk = system_clocks ? tchecker::REFCLOCK_ID : 0;
   clock_constraint_container_t result;
 
-  for(tchecker::clock_id_t i = 1; i < get_no_of_virt_clocks(); ++i) {
-    tchecker::clock_id_t cur = i + orig_clocks_offset;
-    result.emplace_back(0, cur, tchecker::dbm::access(this->dbm(), this->dim(), 0, i)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), 0, i)->value);
-    result.emplace_back(cur, 0, tchecker::dbm::access(this->dbm(), this->dim(), i, 0)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), i, 0)->value);
+  for(tchecker::clock_id_t i = 1; i <= get_no_of_virt_clocks(); ++i) {
+    tchecker::clock_id_t cur = i + no_of_orig_clocks;
+
+    if(system_clocks) {
+      cur--;
+    }
+
+    result.emplace_back(ref_clk, cur, tchecker::dbm::access(this->dbm(), this->dim(), 0, i)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), 0, i)->value);
+    result.emplace_back(cur, ref_clk, tchecker::dbm::access(this->dbm(), this->dim(), i, 0)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), i, 0)->value);
+
+    for(tchecker::clock_id_t j = i+1; j <= get_no_of_virt_clocks(); ++j) {
+      tchecker::clock_id_t second_cur = j + no_of_orig_clocks;
+
+    if(system_clocks) {
+      second_cur--;
+    }
 
-    for(tchecker::clock_id_t j = i+1; j < get_no_of_virt_clocks(); ++j) {
-      tchecker::clock_id_t second_cur = j + orig_clocks_offset;
       result.emplace_back(second_cur, cur, tchecker::dbm::access(this->dbm(), this->dim(), j, i)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), j, i)->value);
       result.emplace_back(cur, second_cur, tchecker::dbm::access(this->dbm(), this->dim(), i, j)->cmp, tchecker::dbm::access(this->dbm(), this->dim(), i, j)->value);
     }
   }
+
   return result;
 
 }
 
-tchecker::zone_container_t<virtual_constraint_t> virtual_constraint_t::logic_and(tchecker::zone_container_t<virtual_constraint_t> *container)
-{
-  tchecker::zone_container_t<virtual_constraint_t> result{this->dim()};
-  for(auto iter = container->begin(); iter < container->end(); iter++ ) {
+void virtual_constraint_t::neg_logic_and(std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> result, const virtual_constraint_t & other) const {
+  assert(result->is_empty());
+  assert(result->dim() == other.dim());
+  assert(this->dim() == other.dim());
 
-    std::shared_ptr<virtual_constraint_t> to_append = factory(this->dim());
+  result->append_container(this->neg_helper(const_cast<tchecker::dbm::db_t *>(other.dbm())));
+}
+
+enum tchecker::dbm::status_t virtual_constraint_t::logic_and(std::shared_ptr<virtual_constraint_t> result, const virtual_constraint_t & other) const
+{
+  assert(result->dim() == other.dim());
+  assert(this->dim() == result->dim());
+  return tchecker::dbm::intersection(result->dbm(), other.dbm(), this->dbm(), this->dim());
+}
+
+enum tchecker::dbm::status_t virtual_constraint_t::logic_and(std::shared_ptr<tchecker::zg::zone_t> result, const tchecker::zg::zone_t & zone) const
+{
+  return this->logic_and(*result, zone);
+}
+
+enum tchecker::dbm::status_t virtual_constraint_t::logic_and(tchecker::zg::zone_t & result, const tchecker::zg::zone_t & zone) const
+{
+  assert(result.dim() == zone.dim());
+  tchecker::dbm::copy(result.dbm(), zone.dbm(), zone.dim());
+  return tchecker::dbm::constrain(result.dbm(), result.dim(), this->get_vc(result.dim() - this->dim(), true));
+}
+
+void virtual_constraint_t::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
+{
+  assert(result->is_empty());
+  assert(result->dim() == container->dim());
+  assert(this->dim() == container->dim());
+
+  for(auto iter = container->begin(); iter < container->end(); iter++ ) {
+    std::shared_ptr<virtual_constraint_t> to_append = factory(this->get_no_of_virt_clocks());
     if(tchecker::dbm::EMPTY != tchecker::dbm::intersection(to_append->dbm(), (*iter)->dbm(), this->dbm(), this->dim())) {
-      result.append_zone(to_append);
+      result->append_zone(to_append);
     }
   }
-
-  return result;
 }
 
-std::shared_ptr<virtual_constraint_t> factory(tchecker::clock_id_t dim)
+std::shared_ptr<virtual_constraint_t> factory(tchecker::clock_id_t number_of_virtual_clocks)
 {
   return static_pointer_cast<tchecker::virtual_constraint::virtual_constraint_t>(
-                                    tchecker::zg::factory(dim));
+                                    tchecker::zg::factory(number_of_virtual_clocks + 1));
 }
 
 std::shared_ptr<virtual_constraint_t> factory(tchecker::virtual_constraint::virtual_constraint_t const & virtual_constraint)
 {
-  tchecker::zg::zone_t const & reinterpreted_zone = reinterpret_cast<tchecker::zg::zone_t const &>(virtual_constraint);
-  return static_pointer_cast<tchecker::virtual_constraint::virtual_constraint_t>(
-                                    tchecker::zg::factory(reinterpreted_zone)
-        );
+  return factory(virtual_constraint.dbm(), virtual_constraint.dim(), virtual_constraint.get_no_of_virt_clocks());
 }
 
 
@@ -129,10 +185,15 @@ std::shared_ptr<virtual_constraint_t> factory(std::shared_ptr<tchecker::zg::zone
   return factory(zone->dbm(), zone->dim(), no_of_virtual_clocks);
 }
 
+std::shared_ptr<virtual_constraint_t> factory(tchecker::zg::zone_t const & zone, tchecker::clock_id_t no_of_virtual_clocks)
+{
+  return factory(zone.dbm(), zone.dim(), no_of_virtual_clocks);
+}
+
 std::shared_ptr<virtual_constraint_t> factory(const tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, tchecker::clock_id_t no_of_virtual_clocks)
 {
 
-  std::shared_ptr<virtual_constraint_t> result = factory(no_of_virtual_clocks + 1);
+  std::shared_ptr<virtual_constraint_t> result = factory(no_of_virtual_clocks);
 
   std::vector<tchecker::clock_id_t> indices;
   indices.emplace_back(0);
@@ -142,78 +203,123 @@ std::shared_ptr<virtual_constraint_t> factory(const tchecker::dbm::db_t * dbm, t
     indices.emplace_back(i);
   }
 
-  for(std::size_t i = 0; i < indices.size(); ++i)
+  for(tchecker::clock_id_t i = 0; i < indices.size(); ++i)
   {
-    for(std::size_t j = 0; j < indices.size(); ++j)
+    for(tchecker::clock_id_t j = 0; j < indices.size(); ++j)
     {
-      tchecker::dbm::constrain(
-          result->dbm(), result->dim(), i, j, dbm[indices[i]*dim + indices[j]].cmp, dbm[indices[i]*dim + indices[j]].value
-        );
+      tchecker::dbm::db_t * i_minus_j = tchecker::dbm::access(result->dbm(), result->dim(), i, j);
+      *i_minus_j = *(tchecker::dbm::access(dbm, dim, indices[i], indices[j]));
     }
   }
 
   return result;
 }
 
-void destruct(virtual_constraint_t *to_destruct)
+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)
 {
-  tchecker::zg::zone_destruct_and_deallocate(to_destruct);
-}
 
-tchecker::zone_container_t<virtual_constraint_t> * combine_lhs_land_not_rhs(std::shared_ptr<virtual_constraint_t> lhs, std::shared_ptr<virtual_constraint_t> rhs, tchecker::clock_id_t dim)
-{
-  tchecker::zone_container_t<virtual_constraint_t> *result = new tchecker::zone_container_t<virtual_constraint_t>(dim);
+  tchecker::zone_container_t<virtual_constraint_t> lo_of_non_empty_vc{no_of_virtual_clocks + 1};
 
-  tchecker::zone_container_t<virtual_constraint_t> *neg = rhs->neg();
-
-  for(auto iter = neg->begin(); iter < neg->end(); iter++) {
-    std::shared_ptr<virtual_constraint_t> to_append = factory(dim);
-    if(tchecker::dbm::EMPTY != tchecker::dbm::intersection(to_append->dbm(), (*iter)->dbm(), lhs->dbm(), dim)) {
-      result->append_zone(*to_append); // to_append is copied here
+  for(auto phi = lo_vc.begin(); phi < lo_vc.end(); phi++) {
+    if(!(*phi)->is_empty()) {
+      lo_of_non_empty_vc.append_zone(*phi);
     }
-    destruct(&(*to_append));
   }
 
-  return result;
-}
+  std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> result = std::make_shared<tchecker::zone_container_t<virtual_constraint_t>>(no_of_virtual_clocks + 1);
 
-tchecker::zone_container_t<virtual_constraint_t> * combine_helper(std::shared_ptr<virtual_constraint_t> lhs, tchecker::zone_container_t<virtual_constraint_t> * lo_vc, tchecker::clock_id_t dim)
-{
-  tchecker::zone_container_t<virtual_constraint_t> *result = new tchecker::zone_container_t<virtual_constraint_t>(dim);
-  result->append_zone(*lhs);
-  for(auto iter = lo_vc->begin(); iter < lo_vc->end(); iter++) {
-    tchecker::zone_container_t<virtual_constraint_t> *inter = result;
-    result = new tchecker::zone_container_t<virtual_constraint_t>(dim);
+  for(auto iter = lo_of_non_empty_vc.begin(); iter < lo_of_non_empty_vc.end(); iter++) {
 
-    for(auto inter_iter = inter->begin(); inter_iter < inter->end(); inter_iter++) {
-      tchecker::zone_container_t<virtual_constraint_t> *lhs_land_not_rhs = combine_lhs_land_not_rhs(*inter_iter, *iter, dim);
-      for(auto land_iter = lhs_land_not_rhs->begin(); land_iter < lhs_land_not_rhs->end(); land_iter++) {
-        result->append_zone(*land_iter);
+    std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> inter = std::make_shared<tchecker::zone_container_t<virtual_constraint_t>>(no_of_virtual_clocks + 1);
+    std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> helper;
+    inter->append_zone(*iter);
+
+    for(auto phi_r = result->begin(); phi_r < result->end(); phi_r++) {
+      helper = std::make_shared<tchecker::zone_container_t<virtual_constraint_t>>(no_of_virtual_clocks + 1);
+      for(auto phi_inter = inter->begin(); phi_inter < inter->end(); phi_inter++) {
+        std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> to_append
+          = std::make_shared<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>(no_of_virtual_clocks + 1);
+
+        (*phi_r)->neg_logic_and(to_append, **phi_inter);
+
+        helper->append_container(to_append);
+      }
+      inter = helper;
+    }
+
+    for(auto phi = inter->begin(); phi < inter->end(); phi++) {
+      if(!(*phi)->is_empty()) {
+        assert(tchecker::dbm::is_le((*phi)->dbm(), (*iter)->dbm(), (*iter)->dim()));
+        result->append_zone(**phi);
       }
     }
-    delete inter;
+
   }
 
   return result;
-
 }
 
-tchecker::zone_container_t<virtual_constraint_t> * combine(std::vector<tchecker::zone_container_t<virtual_constraint_t>> & lo_lo_vc, tchecker::clock_id_t dim)
+bool all_elements_are_stronger_than(std::shared_ptr<zone_container_t<virtual_constraint_t>> weaker, 
+                                    std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> stronger, tchecker::clock_id_t no_of_virtual_clocks) {
+  bool result = true;
+  for(auto iter = stronger->begin(); iter < stronger->end(); iter++) {
+    result &= ((*iter)->dim() == (no_of_virtual_clocks + 1));
+    bool inter = false;
+    for(auto second_iter = weaker->begin(); second_iter < weaker->end(); second_iter++) {
+      inter |= tchecker::dbm::is_le((*iter)->dbm(), (*second_iter)->dbm(), no_of_virtual_clocks + 1);
+    }
+    result &= inter;
+  }
+  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)
 {
-  if(lo_lo_vc.empty()) {
-    return new tchecker::zone_container_t<virtual_constraint_t>(dim);
+
+  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]
+    )
+  );
+
+  if (zones.empty()) {
+    return std::make_shared<tchecker::zone_container_t<virtual_constraint_t>>(no_of_virtual_clocks + 1);
   }
 
-  tchecker::zone_container_t<virtual_constraint_t> cur = lo_lo_vc.back();
-  lo_lo_vc.pop_back();
-
-  tchecker::zone_container_t<virtual_constraint_t> *result = combine(lo_lo_vc, dim);
-
-  for(auto cur_iter = cur.begin(); cur_iter < cur.end(); cur_iter++) {
-    tchecker::zone_container_t<virtual_constraint_t> *inter = combine_helper(*cur_iter, result, dim);
-    delete result;
-    result = inter;
+  if (1 == zones.size()) {
+    return (zones[0]);
   }
+
+  std::shared_ptr<zone_container_t<virtual_constraint_t>> cur = zones.back();
+  zones.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>> result = std::make_shared<zone_container_t<virtual_constraint_t>>(no_of_virtual_clocks + 1);
+
+  for(auto iter_cur = cur->begin(); iter_cur < cur->end(); iter_cur++) {
+    for(auto iter_inter = inter->begin(); iter_inter < inter->end(); iter_inter++) {
+      std::shared_ptr<virtual_constraint_t> tmp = factory(no_of_virtual_clocks);
+      if(tchecker::dbm::NON_EMPTY == tchecker::dbm::intersection(tmp->dbm(), (**iter_cur).dbm(), (**iter_inter).dbm(), (**iter_cur).dim())) {
+        result->append_zone(tmp);
+      }
+    }
+  }
+
+  assert(
+    std::all_of(result->begin(), result->end(),
+                [](std::shared_ptr<virtual_constraint_t> res){return tchecker::dbm::is_consistent(res->dbm(), res->dim());} // cppcheck-suppress assertWithSideEffect
+    )
+  );
+
+  assert(
+    std::all_of(result->begin(), result->end(),
+                [](std::shared_ptr<virtual_constraint_t> res){return tchecker::dbm::is_tight(res->dbm(), res->dim());} // cppcheck-suppress assertWithSideEffect
+    )
+  );
+
+  assert(all_elements_are_stronger_than(cur, result, no_of_virtual_clocks));
+
   return result;
 }
 

src/zg/semantics.cc

@@ -42,9 +42,15 @@ tchecker::state_status_t next_helper(tchecker::dbm::db_t * dbm, tchecker::clock_
                                                     tchecker::clock_reset_container_t const & clkreset, bool tgt_delay_allowed,
                                                     tchecker::clock_constraint_container_t const & tgt_invariant)
 {
+  assert(tchecker::dbm::is_tight(dbm, dim));
+  assert(tchecker::dbm::is_consistent(dbm, dim));
+
   if (tchecker::dbm::constrain(dbm, dim, src_invariant) == tchecker::dbm::EMPTY)
     return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED;
 
+  assert(tchecker::dbm::is_tight(dbm, dim));
+  assert(tchecker::dbm::is_consistent(dbm, dim));
+
   if (src_delay_allowed) {
     tchecker::dbm::open_up(dbm, dim);
 
@@ -55,11 +61,21 @@ tchecker::state_status_t next_helper(tchecker::dbm::db_t * dbm, tchecker::clock_
   if (tchecker::dbm::constrain(dbm, dim, guard) == tchecker::dbm::EMPTY)
     return tchecker::STATE_CLOCKS_GUARD_VIOLATED;
 
+
+  assert(tchecker::dbm::is_tight(dbm, dim));
+  assert(tchecker::dbm::is_consistent(dbm, dim));
+
   tchecker::dbm::reset(dbm, dim, clkreset);
 
+  assert(tchecker::dbm::is_tight(dbm, dim));
+  assert(tchecker::dbm::is_consistent(dbm, dim));
+
   if (tchecker::dbm::constrain(dbm, dim, tgt_invariant) == tchecker::dbm::EMPTY)
     return tchecker::STATE_CLOCKS_TGT_INVARIANT_VIOLATED;
 
+  assert(tchecker::dbm::is_tight(dbm, dim));
+  assert(tchecker::dbm::is_consistent(dbm, dim));
+
   return tchecker::STATE_OK;
 }
 
@@ -98,6 +114,23 @@ tchecker::state_status_t prev_helper(tchecker::dbm::db_t * dbm, tchecker::clock_
   return tchecker::STATE_OK;
 }
 
+/* semantics_t */
+
+tchecker::state_status_t semantics_t::delay( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim,
+                                                            tchecker::clock_constraint_container_t const & invariant)
+{
+  if (tchecker::dbm::constrain(dbm, dim, invariant) == tchecker::dbm::EMPTY)
+    return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED;
+
+  tchecker::dbm::open_up(dbm, dim);
+
+  if (tchecker::dbm::constrain(dbm, dim, invariant) == tchecker::dbm::EMPTY)
+    return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED; // should never occur
+
+  return tchecker::STATE_OK;
+}
+
+
 /* standard_semantics_t */
 
 tchecker::state_status_t standard_semantics_t::initial(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
@@ -225,27 +258,13 @@ tchecker::state_status_t elapsed_semantics_t::prev(tchecker::dbm::db_t * dbm, tc
 tchecker::state_status_t distinguished_semantics_t::initial( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
                                                              tchecker::clock_constraint_container_t const & invariant)
 {
-  return initial_helper(dbm, dim, delay_allowed, invariant);
+  return initial_helper(dbm, dim, false, invariant);
 }
 
 tchecker::state_status_t distinguished_semantics_t::final( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool delay_allowed,
                                                            tchecker::clock_constraint_container_t const & invariant)
 {
-  return final_helper(dbm, dim, delay_allowed, invariant);
-}
-
-tchecker::state_status_t distinguished_semantics_t::delay( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim,
-                                                            tchecker::clock_constraint_container_t const & invariant)
-{
-  if (tchecker::dbm::constrain(dbm, dim, invariant) == tchecker::dbm::EMPTY)
-    return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED;
-
-  tchecker::dbm::open_up(dbm, dim);
-
-  if (tchecker::dbm::constrain(dbm, dim, invariant) == tchecker::dbm::EMPTY)
-    return tchecker::STATE_CLOCKS_SRC_INVARIANT_VIOLATED; // should never occur
-
-  return tchecker::STATE_OK;
+  return final_helper(dbm, dim, false, invariant);
 }
 
 tchecker::state_status_t distinguished_semantics_t::next( tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim, bool src_delay_allowed,

src/zg/zg.cc

@@ -63,7 +63,7 @@ void zg_t::next(tchecker::zg::const_state_sptr_t const & s, outgoing_edges_value
                                             t->reset_container(), tgt_delay, t->tgt_invariant_container());
                     };
 
-  sst_handler<outgoing_edges_value_t const, bool>(out_edge, v, mask, ta_func, se_func, s, true);
+  sst_handler<outgoing_edges_value_t const, bool>(out_edge, v, mask, ta_func, se_func, s, true, _enable_extrapolation);
 }
 
 void zg_t::next(tchecker::zg::const_state_sptr_t const & s, std::vector<sst_t> & v,
@@ -248,11 +248,11 @@ void zg_t::sst_handler( edge_t edge, std::vector<sst_t> & v, tchecker::state_sta
                                                          tchecker::zg::state_sptr_t &,
                                                         tchecker::zg::transition_sptr_t &,
                                                          helping_hand_t *),
-                  tchecker::zg::const_state_sptr_t const & to_clone, bool clone
+                  tchecker::zg::const_state_sptr_t const & to_clone, bool clone, bool enable_extrapolation
                   )
 {
   tchecker::zg::state_sptr_t s;
-  if(clone) { // for some crazy reason, I cannot check for null here and, therefore, we need clone
+  if(clone) { // for some crazy reasons, I cannot check for null here and, therefore, we need clone
     s = _state_allocator.clone(*to_clone);
   }
   else {
@@ -271,7 +271,7 @@ void zg_t::sst_handler( edge_t edge, std::vector<sst_t> & v, tchecker::state_sta
 
     status = se_func(*_system, *_semantics, dbm, dim, s, t, &helper);
 
-    if(tchecker::STATE_OK == status) {
+    if(tchecker::STATE_OK == status && enable_extrapolation) {
       _extrapolation->extrapolate(dbm, dim, *(s->vloc_ptr()));
     }
   }
@@ -344,28 +344,28 @@ next(tchecker::zg::zg_t &zg,
 std::shared_ptr<zg_t> factory(std::shared_ptr<tchecker::ta::system_t const> const & system,
                              enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type,
                              enum tchecker::zg::extrapolation_type_t extrapolation_type, std::size_t block_size,
-                             std::size_t table_size)
+                             std::size_t table_size, bool enable_extrapolation)
 {
   std::shared_ptr<tchecker::zg::extrapolation_t> extrapolation{
       tchecker::zg::extrapolation_factory(extrapolation_type, *system)};
   if (extrapolation.get() == nullptr)
     return nullptr;
   std::shared_ptr<tchecker::zg::semantics_t> semantics{tchecker::zg::semantics_factory(semantics_type)};
-  return std::make_shared<zg_t>(system, sharing_type, semantics, extrapolation, block_size, table_size);
+  return std::make_shared<zg_t>(system, sharing_type, semantics, extrapolation, block_size, table_size, enable_extrapolation);
 }
 
 std::shared_ptr<zg_t> factory(std::shared_ptr<tchecker::ta::system_t const> const & system,
                              enum tchecker::ts::sharing_type_t sharing_type, enum tchecker::zg::semantics_type_t semantics_type,
                              enum tchecker::zg::extrapolation_type_t extrapolation_type,
                              tchecker::clockbounds::clockbounds_t const & clock_bounds, std::size_t block_size,
-                             std::size_t table_size)
+                             std::size_t table_size, bool enable_extrapolation)
 {
   std::shared_ptr<tchecker::zg::extrapolation_t> extrapolation{
       tchecker::zg::extrapolation_factory(extrapolation_type, clock_bounds)};
   if (extrapolation.get() == nullptr)
     return nullptr;
   std::shared_ptr<tchecker::zg::semantics_t> semantics{tchecker::zg::semantics_factory(semantics_type)};
-  return std::make_shared<zg_t>(system, sharing_type, semantics, extrapolation, block_size, table_size);
+  return std::make_shared<zg_t>(system, sharing_type, semantics, extrapolation, block_size, table_size, enable_extrapolation);
 }
 
 } // end of namespace zg

test/tck-compare/CMakeLists.txt

@@ -38,7 +38,21 @@ set(DOT_MAX_SIZE 20000)
 # only append to the tail of this list!
 set(INPUTS
     missing_initial.sh:
+    easy-ad94.sh:
+    easy-ad94-added-transition.sh:
+    easy-ad94-different-guard.sh:
     ad94.sh:
+    Lieb_et_al_1.sh:
+    Lieb_et_al_1_diff_invariant.sh:
+    Lieb_et_al_2.sh:
+    Lieb_et_al_3.sh:
+    Lieb_et_al_4.sh:
+    Lieb_et_al_5.sh:
+    count_to_inf.sh:
+    Lieb_et_al_1_non_determ_bisim.sh:
+    Lieb_et_al_2_non_determ_bisim.sh:
+    Lieb_et_al_2_determ_split_bisim.sh:
+    Lieb_et_al_2_determ_split_non_bisim.sh:
     corsso.sh:2:2:10:1:2
     critical-region-async.sh:2:10
     csmacd.sh:3
@@ -64,15 +78,90 @@ file(RELATIVE_PATH here ${CMAKE_BINARY_DIR} ${CMAKE_CURRENT_BINARY_DIR})
 message(STATUS "Generating '${here}' tests. This may take a long time.")
 tck_register_testcases("tck-compare-" CHECK_TESTCASES_ savelist TCK_COMPARE_INPUT_FILES ${INPUTS})
 
-# TODO: Insert real Testcases here. You can find the name of all the available files in TCK_COMPARE_INPUT_FILES or add some to INPUTS
-
 list(GET TCK_COMPARE_INPUT_FILES 0 no_initial)
-list(GET TCK_COMPARE_INPUT_FILES 1 ad)
+list(GET TCK_COMPARE_INPUT_FILES 1 easy-ad)
+list(GET TCK_COMPARE_INPUT_FILES 2 easy-ad-added-transition)
+list(GET TCK_COMPARE_INPUT_FILES 3 easy-ad-different-guard)
+list(GET TCK_COMPARE_INPUT_FILES 4 ad)
+list(GET TCK_COMPARE_INPUT_FILES 5 Lieb1)
+list(GET TCK_COMPARE_INPUT_FILES 6 Lieb1_diff_inv)
+list(GET TCK_COMPARE_INPUT_FILES 7 Lieb2)
+list(GET TCK_COMPARE_INPUT_FILES 8 Lieb3)
+list(GET TCK_COMPARE_INPUT_FILES 9 Lieb4)
+list(GET TCK_COMPARE_INPUT_FILES 10 Lieb5)
+list(GET TCK_COMPARE_INPUT_FILES 11 count_to_inf)
+list(GET TCK_COMPARE_INPUT_FILES 12 Lieb1_non_determ_bisim)
+list(GET TCK_COMPARE_INPUT_FILES 13 Lieb_et_al_2_non_determ_bisim)
+list(GET TCK_COMPARE_INPUT_FILES 14 Lieb_et_al_2_determ_split_bisim)
+list(GET TCK_COMPARE_INPUT_FILES 15 Lieb_et_al_2_determ_split_non_bisim)
 
+# check whether the no_initial_check works
 create_testcase(no_initial_first ${no_initial} ${ad} strong-timed-bisim)
 create_testcase(no_initial_second ${ad} ${no_initial} strong-timed-bisim)
 
+# testcases using easy-ad94
 
+create_testcase(easy-ad94-self ${easy-ad} ${easy-ad} strong-timed-bisim)
+create_testcase(easy-ad94-self-added-transition ${easy-ad-added-transition} ${easy-ad-added-transition} strong-timed-bisim)
+create_testcase(easy-ad94-self-different-guard ${easy-ad-different-guard} ${easy-ad-different-guard} strong-timed-bisim)
 
+create_testcase(easy-ad94-easy-ad94-added-transition ${easy-ad} ${easy-ad-added-transition} strong-timed-bisim)
+create_testcase(easy-ad94-added-transition-easy-ad94 ${easy-ad-added-transition} ${easy-ad} strong-timed-bisim)
+
+create_testcase(easy-ad94-different-guard-easy-ad94 ${easy-ad-different-guard} ${easy-ad} strong-timed-bisim)
+
+create_testcase(easy-ad94-different-guard-easy-ad94-added-transition ${easy-ad-different-guard} ${easy-ad-added-transition} strong-timed-bisim)
+
+# testcases using the examples of Lieb et al.
+
+# Lieb1
+create_testcase(Lieb-et-al-1-self ${Lieb1} ${Lieb1} strong-timed-bisim)
+
+create_testcase(Lieb-et-al-1-Lieb-et-al-1-diff-inv ${Lieb1} ${Lieb1_diff_inv} strong-timed-bisim)
+create_testcase(Lieb-et-al-1-Lieb-et-al-1-non-determ-bisim ${Lieb1} ${Lieb1_non_determ_bisim} strong-timed-bisim)
+
+create_testcase(Lieb-et-al-1-Lieb-et-al-2 ${Lieb1} ${Lieb2} strong-timed-bisim)
+create_testcase(Lieb-et-al-1-Lieb-et-al-3 ${Lieb1} ${Lieb3} strong-timed-bisim)
+create_testcase(Lieb-et-al-1-Lieb-et-al-4 ${Lieb1} ${Lieb4} strong-timed-bisim)
+create_testcase(Lieb-et-al-1-Lieb-et-al-5 ${Lieb1} ${Lieb5} strong-timed-bisim)
+
+# Lieb2
+create_testcase(Lieb-et-al-2-self ${Lieb2} ${Lieb2} strong-timed-bisim)
+
+create_testcase(Lieb-et-al-2-Lieb-et-al-2-non-determ-bisim ${Lieb2} ${Lieb_et_al_2_non_determ_bisim} strong-timed-bisim)
+create_testcase(Lieb-et-al-2-Lieb-et-al-2-determ-split-bisim ${Lieb2} ${Lieb_et_al_2_determ_split_bisim} strong-timed-bisim)
+create_testcase(Lieb-et-al-2-Lieb-et-al-2-determ-split-non-bisim ${Lieb2} ${Lieb_et_al_2_determ_split_non_bisim} strong-timed-bisim)
+
+create_testcase(Lieb-et-al-2-Lieb-et-al-3 ${Lieb2} ${Lieb3} strong-timed-bisim)
+create_testcase(Lieb-et-al-2-Lieb-et-al-4 ${Lieb2} ${Lieb4} strong-timed-bisim)
+create_testcase(Lieb-et-al-2-Lieb-et-al-5 ${Lieb2} ${Lieb5} strong-timed-bisim)
+
+#Lieb 3
+create_testcase(Lieb-et-al-3-self ${Lieb3} ${Lieb3} strong-timed-bisim)
+
+create_testcase(Lieb-et-al-3-Lieb-et-al-4 ${Lieb3} ${Lieb4} strong-timed-bisim)
+create_testcase(Lieb-et-al-3-Lieb-et-al-5 ${Lieb3} ${Lieb5} strong-timed-bisim)
+
+#Lieb 4
+create_testcase(Lieb-et-al-4-self ${Lieb4} ${Lieb4} strong-timed-bisim)
+
+create_testcase(Lieb-et-al-4-Lieb-et-al-5 ${Lieb4} ${Lieb5} strong-timed-bisim)
+
+#Lieb 5
+create_testcase(Lieb-et-al-5-self ${Lieb5} ${Lieb5} strong-timed-bisim)
+
+# some self test take to long
+#foreach(cur ${TCK_COMPARE_INPUT_FILES})
+#
+#  string(FIND ${cur} "/" last_slash REVERSE)
+#  math(EXPR last_slash "${last_slash}+1")
+#  string(SUBSTRING ${cur} ${last_slash} -1 test_name)
+#  string(REPLACE ".out" "-self" test_name ${test_name})
+#
+#  if(NOT ${no_initial} STREQUAL ${cur})
+#    create_testcase(${test_name} ${cur} ${cur} strong-timed-bisim)
+#  endif()
+#
+#endforeach()
 
 tck_add_savelist(save-compare ${savelist})

test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-diff-inv.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 7

test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-non-determ-bisim.out-expected

@@ -1,6 +1,4 @@
-DEEPEST_PATH 0
 MEMORY_MAX_RSS  xxxx
 RELATIONSHIP_FULFILLED true
 RUNNING_TIME_SECONDS  xxxx
-VISITED_PAIR_OF_STATES_STATES 0
-VISITED_TRANSITIONS 0
+VISITED_PAIR_OF_STATES 10

test/tck-compare/Lieb-et-al-1-Lieb-et-al-2.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 7

test/tck-compare/Lieb-et-al-1-Lieb-et-al-3.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 7

test/tck-compare/Lieb-et-al-1-Lieb-et-al-4.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 7

test/tck-compare/Lieb-et-al-1-Lieb-et-al-5.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 12

test/tck-compare/Lieb-et-al-1-non-determ-bisim.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED true
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 10

test/tck-compare/Lieb-et-al-1-self.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED true
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 7

test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-bisim.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED true
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 12

test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-non-bisim.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 12

test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-non-determ-bisim.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED true
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 12

test/tck-compare/Lieb-et-al-2-Lieb-et-al-3.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED true
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 7

test/tck-compare/Lieb-et-al-2-Lieb-et-al-4.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 7

test/tck-compare/Lieb-et-al-2-Lieb-et-al-5.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 12

test/tck-compare/Lieb-et-al-2-self.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED true
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 7

test/tck-compare/Lieb-et-al-3-Lieb-et-al-4.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 7

test/tck-compare/Lieb-et-al-3-Lieb-et-al-5.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 12

test/tck-compare/Lieb-et-al-3-self.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED true
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 7

test/tck-compare/Lieb-et-al-4-Lieb-et-al-5.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 12

test/tck-compare/Lieb-et-al-4-self.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED true
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 7

test/tck-compare/Lieb-et-al-5-self.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED true
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 22

test/tck-compare/easy-ad94-added-transition-easy-ad94.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 6

test/tck-compare/easy-ad94-different-guard-easy-ad94-added-transition.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 5

test/tck-compare/easy-ad94-different-guard-easy-ad94.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 5

test/tck-compare/easy-ad94-easy-ad94-added-transition.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED false
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 6

test/tck-compare/easy-ad94-self-added-transition.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED true
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 8

test/tck-compare/easy-ad94-self-different-guard.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED true
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 6

test/tck-compare/easy-ad94-self.out-expected

@@ -0,0 +1,4 @@
+MEMORY_MAX_RSS  xxxx
+RELATIONSHIP_FULFILLED true
+RUNNING_TIME_SECONDS  xxxx
+VISITED_PAIR_OF_STATES 6

test/tck-compare/no_initial_first.err-expected

@@ -1 +1,2 @@
-WARNING: the first system has no initial state
+ERROR: Currently, strong timed bisim is supported with exactly a single initial location per process, only
+a process of missing_initial has no initial location

test/tck-compare/no_initial_second.err-expected

@@ -1 +1,2 @@
-WARNING: the second system has no initial state
+ERROR: Currently, strong timed bisim is supported with exactly a single initial location per process, only
+a process of missing_initial has no initial location

test/tck-compare/no_initial_second.out-expected

@@ -1,6 +0,0 @@
-DEEPEST_PATH 0
-MEMORY_MAX_RSS  xxxx
-RELATIONSHIP_FULFILLED true
-RUNNING_TIME_SECONDS  xxxx
-VISITED_PAIR_OF_STATES_STATES 0
-VISITED_TRANSITIONS 0

test/tck-compare/tck-compare-Lieb_et_al_1.out-expected

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

test/tck-compare/tck-compare-Lieb_et_al_1_diff_invariant.out-expected

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

test/tck-compare/tck-compare-Lieb_et_al_1_non_determ_bisim.out-expected

@@ -0,0 +1,22 @@
+# This file is a part of the TChecker project.
+#
+# See files AUTHORS and LICENSE for copyright details.
+
+system:Lieb_et_al_A1
+
+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:CPrime{}
+edge:P:A:B:a{provided: x<=0}
+edge:P:B:C:b{provided: x<=1}
+edge:P:B:CPrime:b{provided:x>1}
+edge:P:C:A:c{provided: x>3 : do: x=0}
+edge:P:CPrime:A:c{provided: x>3 : do: x=0}

test/tck-compare/tck-compare-Lieb_et_al_2.out-expected

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

test/tck-compare/tck-compare-Lieb_et_al_2_determ_split_bisim.out-expected

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

test/tck-compare/tck-compare-Lieb_et_al_2_determ_split_non_bisim.out-expected

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