new version of algorithm

include/tchecker/dbm/dbm.hh

@@ -584,6 +584,21 @@ void open_down(tchecker::dbm::db_t * dbm, tchecker::clock_id_t dim);
 enum tchecker::dbm::status_t intersection(tchecker::dbm::db_t * dbm, tchecker::dbm::db_t const * dbm1,
                                           tchecker::dbm::db_t const * dbm2, tchecker::clock_id_t dim);
 
+
+/*!
+ \brief disjoint
+ \param dbm1 : a dbm
+ \param dbm2 : a dbm
+ \param dim : dimension of dbm1 and dbm2
+ \pre dbm1 and dbm2 are not nullptr (checked by assertion)
+ dbm1 and dbm2 are dim*dim arrays of difference bounds
+ dbm1 and dbm2 are consistent (checked by assertion)
+ dbm1 and dbm2 are tight (checked by assertion)
+ dim >= 1 (checked by assertion).
+ \return [dbm1 && dbm2] == emptyset
+ */
+bool disjoint(tchecker::dbm::db_t * dbm_1, tchecker::dbm::db_t * dbm2, tchecker::clock_id_t dim);
+
 /*!
  \brief revert-multiple-reset function (see the TR of Lieb et al.)
  \param result : where the result will be stored (must be allocated)

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

@@ -18,7 +18,7 @@
 
 #include "tchecker/strong-timed-bisim/stats.hh"
 #include "tchecker/vcg/vcg.hh"
-#include "tchecker/utils/zone_container.hh"
+#include "tchecker/zg/zone_container.hh"
 
 namespace tchecker {
 
@@ -68,32 +68,75 @@ private:
     }
   };
 
+  /*!
+   \brief checks whether we need to do an epsilon transition
+   \param A_state : first state
+   \param B_state : second state
+   \Return true if the states are either not synced or the result of a delay is different than the original symbolic states
+  */
+  bool do_an_epsilon_transition(tchecker::zg::state_sptr_t A_state, tchecker::zg::transition_sptr_t A_trans,
+                                tchecker::zg::state_sptr_t B_state, tchecker::zg::transition_sptr_t B_trans);
+
   /*!
    \brief check-for-virt-bisim function of Lieb et al.
    \param symb_state_first : the symbolic state that belongs to the first vcg
    \param A_trans : the transition with which we reached the first symbolic state
    \param symb_state_second : the symbolic state that belongs to the second vcg
    \param B_trans : the transition with which we reached the second symbolic state
+   \param last_was_epsilon : whether the last transition was an epsilon transition
+   \param visited : a set of assumptions
    \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 A_state, tchecker::zg::transition_sptr_t A_trans,
                        tchecker::zg::const_state_sptr_t B_state, tchecker::zg::transition_sptr_t B_trans,
                        std::unordered_set<std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t>, custom_hash, custom_equal> & visited);
 
+  /*!
+   \brief helping function for check-for-outgoing-transitions. Is called if the other side has no transitions.
+   \param zone : the zone of the starting symbolic states that has some transitions.
+   \param trans : the corresponding transitions
+   \return the virtual constraints that represent the part of zone that has any of the given outgoing transitions.
+   */
+  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
+  check_for_outgoing_transitions_single_empty(tchecker::zg::zone_t const & zone, std::vector<tchecker::vcg::vcg_t::sst_t *> & trans);
+
+  /*!
+   \brief : removes found contradictions from a zone
+   \param zone : the zone to constraint
+   \param contradictions : the virtual constraints that shall be removed from zone
+   \return zone && (! && of all elements in contradictions)
+   */
+  std::shared_ptr<tchecker::zone_container_t<tchecker::zg::zone_t>>
+  extract_zone_without_contradictions(tchecker::zg::zone_t const & zone, std::shared_ptr<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> contradictions);
+
+  /*!
+   \brief : takes two transitions and splits of the target zones. Returns a contradiction if one is found.
+   \param : zones-A : the splits of the target zones of trans_A
+   \param : trans_A : the first transition
+   \param : zones_B : the splits of the target zones of trans_B
+   \param : trans_B : the second transition
+   \param : visted : the assumptions.
+   \return a contradiction if there is one. Otherwise an empty list of virtual constraints.
+   */
+  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
+  check_splitted_transitions(std::shared_ptr<tchecker::zone_container_t<tchecker::zg::zone_t>> zones_A, tchecker::zg::transition_sptr_t trans_A, tchecker::zg::state_sptr_t state_A,
+                             std::shared_ptr<tchecker::zone_container_t<tchecker::zg::zone_t>> zones_B, tchecker::zg::transition_sptr_t trans_B, tchecker::zg::state_sptr_t state_B,
+                             std::unordered_set<std::pair<tchecker::zg::state_sptr_t, tchecker::zg::state_sptr_t>, custom_hash, custom_equal> & visited);
+
   /*!
    \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 A_is_first : whether the outgoing transitions of A or B shall be checked
+   \param zone_A : the zone of the symbolic state that belongs to the first vcg
+   \param zone_B : the zone of the symbolic state that belongs to the second vcg
+   \param trans_A : the list of transitions that belongs to the first vcg
+   \param trans_B : the list of transitions that belongs to the second vcg
+   \param visited : the assumptions
    \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 A_state,
-                                  tchecker::zg::const_state_sptr_t B_state,
+  check_for_outgoing_transitions( tchecker::zg::zone_t const & zone_A, tchecker::zg::zone_t const & zone_B,
+                                  std::vector<tchecker::vcg::vcg_t::sst_t *> & trans_A, std::vector<tchecker::vcg::vcg_t::sst_t *> & trans_B,
                                   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;

include/tchecker/syncprod/vedge.hh

@@ -162,16 +162,34 @@ public:
    */
   const_array_iterator_t end_array() const;
 
+  /*!
+   \brief This functions returns the event names of the transition
+   \param system : the system this transitions belongs to
+   \return the set of events of this transition
+   */
+  std::set<std::string> event_names(const tchecker::system::system_t & system) const;
+
   /*!
    \brief This function checks whether all events of this are also
           contained by other and vice versa.
    \param my_system : the system this belongs to
    \param other : the other transition
    \param other_system: the system other belongs to
+   \return true, if the set of event names is the same
    */
   bool event_equal(tchecker::system::system_t const & my_system, const vedge_t & other, tchecker::system::system_t const & other_system) const
     { return this->contains_events(my_system, other, other_system) && other.contains_events(other_system, *this, my_system); }
 
+  /*!
+   \brief This function checks whether all events of this are also
+          contained by the given set.
+   \param system : the system this belongs to
+   \param event: the other event
+   \return true, if the given set is the same as the event names of this transition
+   */
+  bool event_equal(tchecker::system::system_t const & system, std::set<std::string> const & events) const
+    { return this->event_names(system) == events; }
+
 protected:
 
   /*!

include/tchecker/vcg/sync.hh

@@ -17,31 +17,24 @@ namespace vcg {
 
 /*!
  \brief sync function (see the TR of Lieb et al.)
- \param dbm1 : a dbm
- \param dbm2 : a dbm
- \param dim1 : dimension of dbm1
- \param dim2 : dimension of dbm2
- \param lowest_virt_clk_id : the clk id of chi_0
+ \param zone_1 : a zone
+ \param zone_2 : a zone
  \param  no_of_orig_clocks_1 : the number of orig clocks in the first TA
+ \param  no_of_orig_clocks_2 : the number of orig clocks in the second TA
  \param orig_reset1 : the resets of the transition of the first TA
  \param orig_reset2 : the resets of the transition of the second TA
- \pre dbm1 and dbm2 are not nullptr (checked by assertion)
- dbm, dbm1 and dbm2 are dim*dim arrays of difference bounds
- dbm1 and dbm2 are consistent (checked by assertion)
- dbm1 and dbm2 are tight (checked by assertion)
- dim >= 1 (checked by assertion).
- \post dbm1 and dbm2 are synced, consistent and tight
+ \post zone_1 and zone_2 are synced, consistent and tight
  \note the change happens inplace
+ \note this function works if and only if only resets to zero are allowed!
  */
 
-void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2,
-          tchecker::clock_id_t dim1, tchecker::clock_id_t dim2,
+void sync(tchecker::zg::zone_t & zone_1, tchecker::zg::zone_t & zone_2,
           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
+ \brief checks whether the given dbm are synced
  \param dbm1 : the DBM of A
  \param dbm2 : the DBM of B
  \param dim1 : the dim of dbm1
@@ -50,30 +43,32 @@ void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2,
  \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,
+bool are_dbm_synced(tchecker::dbm::db_t const *dbm1, tchecker::dbm::db_t const *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 checks whether the given zones are synced
+ \param zone_1 : the first zone
+ \param zone_2 : the second zone
+ \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_zones_synced(tchecker::zg::zone_t const & zone_1, tchecker::zg::zone_t const & zone_2,
+                      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
- \param dbm2 : a dbm
- \param dim : dimension of dbm1 and dbm2
+ \param zone_1 : a zone
+ \param zone_2 : a zone
  \param  no_of_orig_clocks_1 : the number of orig clocks in the first TA
  \param  no_of_orig_clocks_1 : the number of orig clocks in the first TA
  \param phi_e : the vc to revert
- \pre dbm1 and dbm2 are not nullptr (checked by assertion)
- dbm, dbm1 and dbm2 are dim*dim arrays of difference bounds
- dbm1 and dbm2 are consistent (checked by assertion)
- dbm1 and dbm2 are tight (checked by assertion)
- dim >= 1 (checked by assertion).
- \post dbm1 and dbm2 are synced, consistent and tight
- \note the change happens inplace. this function works if and only if only
- resets to zero are allowed!
+ \return a pair of virtual constraints
+ \note this function works if and only if only resets to zero are allowed!
  */
 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,
+revert_sync(tchecker::zg::zone_t const & zone_1, tchecker::zg::zone_t const & zone_2,
             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);
 

include/tchecker/vcg/virtual_constraint.hh

@@ -10,7 +10,8 @@
 
 #include "tchecker/zg/zone.hh"
 #include "tchecker/dbm/dbm.hh"
-#include "tchecker/utils/zone_container.hh"
+#include "tchecker/zg/zone_container.hh"
+#include "tchecker/vcg/vcg.hh"
 
 /*
  \file virtual_constraint.hh
@@ -52,7 +53,7 @@ public:
    \brief Accessor
    \return no of virtual clocks
    */
-  tchecker::clock_id_t get_no_of_virt_clocks() const;
+  tchecker::clock_id_t get_no_of_virtual_clocks() const;
 
   /*!
    \brief return the virtual constraint as list of clock constraints
@@ -61,7 +62,7 @@ public:
   clock_constraint_container_t get_vc(tchecker::clock_id_t no_of_orig_clocks, bool system_clocks) const;
 
   /*
-   \brief returns the (not this and other)
+   \brief returns (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
    */
@@ -149,10 +150,23 @@ std::shared_ptr<virtual_constraint_t> factory(const tchecker::dbm::db_t * dbm, t
  */
 std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> combine(tchecker::zone_container_t<virtual_constraint_t> & lo_vc, tchecker::clock_id_t no_of_virtual_clocks);
 
+/*!
+ \brief find_contradiction operator (see the TR of Lieb et al.)
+ \param zone_A : the base zone of all transitions of trans_A
+ \param zone_B : the base zone of all transisions of trans_B
+ \param trans_A : a reference to a vector of transitions
+ \param trans_B : a reference to a vector of transitions
+ \param vcs : a matrix of container of virtual constraints
+ */
+std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> find_contradiction(tchecker::zg::zone_t const & zone_A, tchecker::zg::zone_t const & zone_B, 
+                                                                                     std::vector<tchecker::vcg::vcg_t::sst_t *> & trans_A, std::vector<tchecker::vcg::vcg_t::sst_t *> & trans_B,
+                                                                                     tchecker::zone_matrix_t<virtual_constraint_t> & vcs);
+
+
 /*!
  \brief contained-in-all function (see the TR of Lieb et al.)
- \param a vector of container of zones
- \return a container of zones
+ \param a vector of container of virtual constraints
+ \return a container of virtual constraints
  */
 std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> contained_in_all(std::vector<std::shared_ptr<zone_container_t<virtual_constraint_t>>> & vc, tchecker::clock_id_t no_of_virtual_clocks);
 

include/tchecker/zg/state.hh

@@ -123,6 +123,16 @@ public:
     return tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_zone_t const>(_zone.ptr());
   }
 
+  /*!
+  \brief replaces the zone
+  \param : the new zone of this state
+  */
+  inline void replace_zone(tchecker::zg::zone_t & zone)
+  {
+    assert(zone.dim() == _zone->dim());
+    tchecker::dbm::copy(_zone->dbm(), zone.dbm(), zone.dim());
+  }
+
 private:
   tchecker::intrusive_shared_ptr_t<tchecker::zg::shared_zone_t> _zone; /*!< Zone over clock valuations */
 };

include/tchecker/zg/zone.hh

@@ -10,6 +10,7 @@
 
 #include <string>
 
+#include "tchecker/zg/zone_container.hh"
 #include "tchecker/basictypes.hh"
 #include "tchecker/clockbounds/clockbounds.hh"
 #include "tchecker/dbm/dbm.hh"
@@ -24,6 +25,14 @@
 
 namespace tchecker {
 
+// forward declaration of virtual constraints since we want to be able to check for virtual equivalence
+
+namespace virtual_constraint {
+
+class virtual_constraint_t;
+
+} // end of namespace virtual_constraint
+
 namespace zg {
 
 /*!
@@ -63,6 +72,11 @@ public:
    */
   bool is_universal_positive() const;
 
+  /*!
+   \brief makes this zone universal
+   */
+  void make_universal();
+
   /*!
    \brief Equality predicate
    \param zone : a DBM zone
@@ -167,6 +181,39 @@ public:
   */
   bool belongs(tchecker::clockval_t const & clockval) const;
 
+  /*!
+   \brief Checks whether the zones are virtual equivalent
+   \param zone : the other zone
+   \param no_virt_clocks : the number of virtual clocks
+   \return true, if and only if the zones are virtual equivalent
+  */
+  bool is_virtual_equivalent(tchecker::zg::zone_t const & zone, tchecker::clock_id_t no_of_virt_clocks) const;
+
+  /*!
+   \brief Calculates the set of virtual constraints of (this && not phi)
+   \param phi : the virtual constraint phi
+   \return the virtual constraint of (this && not phi)
+  */
+  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
+  get_virtual_overhang(tchecker::virtual_constraint::virtual_constraint_t const & phi) const;
+
+  /*!
+   \brief Calculates the set of virtual constraints of (this && not virtual_constraint(other))
+   \param other : the other zone
+   \return the virtual constraint of (this && not virtual_constraint(other))
+  */
+  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
+  get_virtual_overhang(tchecker::zg::zone_t const & other, tchecker::clock_id_t no_of_virtual_clocks) const;
+
+  /*!
+   \brief Calculates the set of virtual constraints of (this && not virtual_constraint(other)) concatenated with
+          the set of virtual constraints of (other && not virtual_constraint(this))
+   \param other : the other zone
+   \return (this && not virtual_constraint(other)) concatenated with (other && not virtual_constraint(this))
+  */
+  std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>
+  get_virtual_overhang_in_both_directions(tchecker::zg::zone_t const & other, tchecker::clock_id_t no_of_virtual_clocks) const;
+
   /*!
    \brief Construction
    \tparam ARGS : type of arguments to a constructor of tchecker::zg::zone_t
@@ -315,13 +362,13 @@ template <class... ARGS> tchecker::zg::zone_t * zone_allocate_and_construct(tche
 void zone_destruct_and_deallocate(tchecker::zg::zone_t * zone);
 
 /*!
- \brief factory of zones of a vcg
+ \brief factory
  \param dim : the dimension
  */
 std::shared_ptr<zone_t> factory(tchecker::clock_id_t dim);
 
 /*!
- \brief factory of zones of a vcg
+ \brief factory
  \param zone : the zone to copy
  */
 std::shared_ptr<zone_t> factory(zone_t const & zone);