diff --git a/include/tchecker/dbm/dbm.hh b/include/tchecker/dbm/dbm.hh index 7f3be836..5fdab570 100644 --- a/include/tchecker/dbm/dbm.hh +++ b/include/tchecker/dbm/dbm.hh @@ -592,7 +592,7 @@ enum tchecker::dbm::status_t intersection(tchecker::dbm::db_t * dbm, tchecker::d \return the dbm with reverted resets (same dim as orig_zone) \note the returned dbm is allocated on the heap. You have to free it! */ -tchecker::dbm::db_t * revert_multiple_reset(const tchecker::dbm::db_t * orig_zone, +enum tchecker::dbm::status_t revert_multiple_reset(tchecker::dbm::db_t *result, const tchecker::dbm::db_t * orig_zone, tchecker::clock_id_t dim, tchecker::dbm::db_t * zone_split, tchecker::clock_reset_container_t reset); diff --git a/include/tchecker/utils/zone_container.hh b/include/tchecker/utils/zone_container.hh index e3517cc4..69a4c86a 100644 --- a/include/tchecker/utils/zone_container.hh +++ b/include/tchecker/utils/zone_container.hh @@ -140,7 +140,7 @@ public: void remove_empty() { for(auto iter = this->begin(); iter < this->end(); iter++) { - if(iter->empty()) { + if((*iter)->is_empty()) { _storage->erase(iter); } } @@ -201,6 +201,8 @@ public: void compress() { + this->remove_empty(); + std::shared_ptr>> result = _storage; bool reduced; diff --git a/include/tchecker/vcg/revert_transitions.hh b/include/tchecker/vcg/revert_transitions.hh index 06422a91..031bba23 100644 --- a/include/tchecker/vcg/revert_transitions.hh +++ b/include/tchecker/vcg/revert_transitions.hh @@ -34,11 +34,12 @@ revert_action_trans(const tchecker::zg::zone_t & zone, /*! \brief revert-epsilon-trans function (see the TR of Lieb et al.) \param zone : the original zone + \param zone_eps : the original target zone \param phi_split : the sub vc of the target \return a shared pointer to the resulting virtual constraint */ std::shared_ptr -revert_epsilon_trans(const tchecker::zg::zone_t & zone, const tchecker::virtual_constraint::virtual_constraint_t & phi_split); +revert_epsilon_trans(const tchecker::zg::zone_t & zone, const tchecker::zg::zone_t & zone_eps, const tchecker::virtual_constraint::virtual_constraint_t & phi_split); } // end of namespace vcg diff --git a/include/tchecker/vcg/virtual_constraint.hh b/include/tchecker/vcg/virtual_constraint.hh index b0e5028b..637333a0 100644 --- a/include/tchecker/vcg/virtual_constraint.hh +++ b/include/tchecker/vcg/virtual_constraint.hh @@ -60,16 +60,6 @@ public: */ clock_constraint_container_t get_vc(tchecker::clock_id_t no_of_orig_clocks, bool system_clocks) const; - /*! - \brief returns the negated version of this clock constraint - \return let result be the return value. - * forall u with u model this and for all vc in result u does not model vc - * forall u with u does not model this exists a vc in result such that u models vc - * (for u in ({\chi_0, ..., \chi_{|C_A| + | C_B| - 1}} \rightarrow T)) - \note the result can easily become very large. Try to avoid this method and use neg_logic_and instead. - */ - std::shared_ptr> neg() const; - /* \brief returns the (not this and other) \param result : the pointer in which the result will be stored. Has to be allocated! @@ -110,6 +100,12 @@ public: void logic_and(std::shared_ptr> result, std::shared_ptr> const container) const; + /* + \brief returns, whether there exists any clock valuation that fulfills this + \return false, if no clock valuation exists that fulfills this + */ + bool is_fulfillable() {return !this->is_empty();} + private: std::shared_ptr> neg_helper(tchecker::dbm::db_t *upper_bounds) const; @@ -158,7 +154,7 @@ std::shared_ptr> combine(tcheck \param a vector of container of zones \return a container of zones */ -std::shared_ptr> contained_in_all(std::vector>> & zones, tchecker::clock_id_t no_of_virtual_clocks); +std::shared_ptr> contained_in_all(std::vector>> & vc, tchecker::clock_id_t no_of_virtual_clocks); } // end of namespace virtual_constraint diff --git a/src/dbm/dbm.cc b/src/dbm/dbm.cc index 97ca3ae9..0cc3edd2 100644 --- a/src/dbm/dbm.cc +++ b/src/dbm/dbm.cc @@ -523,6 +523,7 @@ enum tchecker::dbm::status_t intersection(tchecker::dbm::db_t * dbm, tchecker::d DBM(i, j) = tchecker::dbm::min(DBM1(i, j), DBM2(i, j)); return tchecker::dbm::tighten(dbm, dim); + } // used for assertion only @@ -547,7 +548,7 @@ bool split_is_subset_of_R_orig(const tchecker::dbm::db_t * orig_zone, tchecker::dbm::output_matrix(std::cout, orig_zone, dim); std::cout << __FILE__ << ": " << __LINE__ << ": zone_split:" << std::endl; - tchecker::dbm::output_matrix(std::cout, orig_zone, dim); + tchecker::dbm::output_matrix(std::cout, zone_split, dim); std::cout << __FILE__ << ": " << __LINE__ << ": resets:" << std::endl; @@ -566,7 +567,7 @@ bool split_is_subset_of_R_orig(const tchecker::dbm::db_t * orig_zone, } -tchecker::dbm::db_t * revert_multiple_reset(const tchecker::dbm::db_t * orig_zone, +enum tchecker::dbm::status_t revert_multiple_reset(tchecker::dbm::db_t *result, const tchecker::dbm::db_t * orig_zone, tchecker::clock_id_t dim, tchecker::dbm::db_t * zone_split, tchecker::clock_reset_container_t reset) { @@ -582,10 +583,9 @@ tchecker::dbm::db_t * revert_multiple_reset(const tchecker::dbm::db_t * orig_zon assert(split_is_subset_of_R_orig(orig_zone, dim, zone_split, reset)); if(reset.empty()) { - // place the dbm to return at the heap s.t. it is not destroyed during the returns - tchecker::dbm::db_t * result = (tchecker::dbm::db_t *)malloc(dim*dim*sizeof(tchecker::dbm::db_t)); tchecker::dbm::copy(result, zone_split, dim); - return result; + tchecker::dbm::tighten(result, dim); + return (is_empty_0(result, dim) ? tchecker::dbm::EMPTY : tchecker::dbm::NON_EMPTY); } tchecker::dbm::db_t zone_clone[dim*dim]; @@ -594,19 +594,23 @@ tchecker::dbm::db_t * revert_multiple_reset(const tchecker::dbm::db_t * orig_zon tchecker::clock_reset_t cur = reset.back(); reset.pop_back(); - if(cur.right_id() != tchecker::REFCLOCK_ID || cur.value() != 0) { + if(cur.left_id() == tchecker::REFCLOCK_ID || cur.right_id() != tchecker::REFCLOCK_ID || cur.value() != 0) { throw std::runtime_error("when checking for timed bisim, only resets to value zero are allowed"); } - tchecker::dbm::reset(zone_clone, dim, reset); + tchecker::dbm::reset_to_value(zone_clone, dim, cur.left_id() + 1, cur.value()); - tchecker::dbm::free_clock(zone_split, dim, cur); + revert_multiple_reset(result, zone_clone, dim, zone_split, reset); - tchecker::dbm::db_t new_split[dim*dim]; + tchecker::dbm::free_clock(result, dim, cur.left_id() + 1); - intersection(new_split, zone_clone, zone_split, dim); + enum tchecker::dbm::status_t ret_val = intersection(result, result, orig_zone, dim); + + if(tchecker::dbm::EMPTY != ret_val) { + assert(tchecker::dbm::is_tight(result, dim)); + } - return revert_multiple_reset(orig_zone, dim, new_split, reset); + return ret_val; } diff --git a/src/strong-timed-bisim/virtual_clock_algorithm.cc b/src/strong-timed-bisim/virtual_clock_algorithm.cc index 46f54a1e..1f084025 100644 --- a/src/strong-timed-bisim/virtual_clock_algorithm.cc +++ b/src/strong-timed-bisim/virtual_clock_algorithm.cc @@ -255,7 +255,8 @@ Lieb_et_al::check_for_virt_bisim(tchecker::zg::const_state_sptr_t symb_state_fir // now, we calculate the problematic virtual constraints by using the revert-epsilon function and adding it to lo_not_simulatable for(auto iter = result_epsilon->begin(); iter < result_epsilon->end(); iter++) { - lo_not_simulatable->append_zone(tchecker::vcg::revert_epsilon_trans(A_normed->zone(), **iter)); + lo_not_simulatable->append_zone(tchecker::vcg::revert_epsilon_trans(A_normed->zone(), A_epsilon->zone(), **iter)); + lo_not_simulatable->append_zone(tchecker::vcg::revert_epsilon_trans(B_normed->zone(), B_epsilon->zone(), **iter)); } } @@ -304,11 +305,17 @@ Lieb_et_al::check_for_virt_bisim(tchecker::zg::const_state_sptr_t symb_state_fir = tchecker::vcg::revert_sync(A_clone->zone_ptr()->dbm(), B_clone->zone_ptr()->dbm(), A_clone->zone_ptr()->dim(), B_clone->zone_ptr()->dim(), _A->get_no_of_original_clocks(), _B->get_no_of_original_clocks(), **iter); - inter.append_zone(sync_reverted.first); - inter.append_zone(sync_reverted.second); - assert(is_phi_subset_of_a_zone(symb_state_first->zone().dbm(), symb_state_first->zone().dim(), _A->get_no_of_virtual_clocks(), *(sync_reverted.first))); - assert(is_phi_subset_of_a_zone(symb_state_second->zone().dbm(), symb_state_second->zone().dim(), _B->get_no_of_virtual_clocks(), *(sync_reverted.second))); + if(sync_reverted.first->is_fulfillable()) { + inter.append_zone(sync_reverted.first); + assert(is_phi_subset_of_a_zone(symb_state_first->zone().dbm(), symb_state_first->zone().dim(), _A->get_no_of_virtual_clocks(), *(sync_reverted.first))); + } + + if(sync_reverted.second->is_fulfillable()) { + inter.append_zone(sync_reverted.second); + assert(is_phi_subset_of_a_zone(symb_state_second->zone().dbm(), symb_state_second->zone().dim(), _B->get_no_of_virtual_clocks(), *(sync_reverted.second))); + } + } inter.compress(); diff --git a/src/vcg/revert_transitions.cc b/src/vcg/revert_transitions.cc index bc6bbc7e..4e2b0fa1 100644 --- a/src/vcg/revert_transitions.cc +++ b/src/vcg/revert_transitions.cc @@ -75,7 +75,7 @@ revert_action_trans(const tchecker::zg::zone_t & zone, // copy the reset container since revert_multiple_reset will change it tchecker::clock_reset_container_t reset_copy(reset); - // According to the implementation of revert-action-trans, described in Lieb et al., we first have to calculate R(zone && g). + // According to the implementation of revert-action-trans, described in Lieb et al., we first have to calculate R(zone && g) && phi_split. tchecker::dbm::db_t d_land_g[zone.dim()*zone.dim()]; zone.to_dbm(d_land_g); @@ -98,36 +98,33 @@ revert_action_trans(const tchecker::zg::zone_t & zone, assert(tchecker::dbm::is_tight(r_d_land_g_land_phi, zone.dim())); assert(tchecker::dbm::is_consistent(r_d_land_g_land_phi, zone.dim())); - tchecker::dbm::db_t *reverted = tchecker::dbm::revert_multiple_reset(d_land_g, zone.dim(), r_d_land_g_land_phi, reset_copy); + tchecker::dbm::db_t *reverted = (tchecker::dbm::db_t *)malloc(zone.dim()*zone.dim()*sizeof(tchecker::dbm::db_t)); + + tchecker::dbm::revert_multiple_reset(reverted, d_land_g, zone.dim(), r_d_land_g_land_phi, reset_copy); std::shared_ptr virt_mult_reset = tchecker::virtual_constraint::factory(reverted, zone.dim(), phi_split.get_no_of_virt_clocks()); - - tchecker::dbm::db_t zone_clone[zone.dim()*zone.dim()]; - zone.to_dbm(zone_clone); - - tchecker::dbm::constrain(zone_clone, zone.dim(), virt_mult_reset->get_vc(zone.dim() - phi_split.dim(), true)); - - std::shared_ptr result - = tchecker::virtual_constraint::factory(zone_clone, zone.dim(), phi_split.get_no_of_virt_clocks()); - - //std::cout << __FILE__ << ": " << __LINE__ << ": return from revert_action_trans" << std::endl; - - return result; + return virt_mult_reset; } std::shared_ptr -revert_epsilon_trans(const tchecker::zg::zone_t & zone, const tchecker::virtual_constraint::virtual_constraint_t & phi_split) +revert_epsilon_trans(const tchecker::zg::zone_t & zone, const tchecker::zg::zone_t & zone_eps, const tchecker::virtual_constraint::virtual_constraint_t & phi_split) { - std::shared_ptr phi_copy = factory(phi_split); + std::shared_ptr zone_eps_copy = tchecker::zg::factory(zone_eps); + + if(tchecker::dbm::EMPTY == tchecker::dbm::constrain(zone_eps_copy->dbm(), zone_eps_copy->dim(), phi_split.get_vc(zone_eps_copy->dim() - phi_split.dim(), true))) { + tchecker::dbm::tighten(zone_eps_copy->dbm(), zone_eps_copy->dim()); + std::shared_ptr result = tchecker::virtual_constraint::factory(zone_eps_copy->dbm(), zone_eps_copy->dim(), phi_split.dim() - 1); + return result; + } - tchecker::dbm::open_down(phi_copy->dbm(), phi_copy->dim()); + tchecker::dbm::open_down(zone_eps_copy->dbm(), zone_eps_copy->dim()); std::shared_ptr zone_copy = tchecker::zg::factory(zone); - tchecker::dbm::constrain(zone_copy->dbm(), zone_copy->dim(), phi_copy->get_vc(zone_copy->dim() - phi_copy->dim(), true)); + intersection(zone_copy->dbm(), zone_copy->dbm(), zone_eps_copy->dbm(), zone_eps_copy->dim()); std::shared_ptr result = tchecker::virtual_constraint::factory(zone_copy, phi_split.get_no_of_virt_clocks()); diff --git a/src/vcg/sync.cc b/src/vcg/sync.cc index cbdf5727..3f4279b3 100644 --- a/src/vcg/sync.cc +++ b/src/vcg/sync.cc @@ -92,7 +92,18 @@ bool is_phi_subset_of_a_zone(const tchecker::dbm::db_t *dbm, tchecker::clock_id_ { std::shared_ptr phi = tchecker::virtual_constraint::factory(dbm, dim, dim - no_of_orig_clocks - 1); - return tchecker::dbm::is_le(phi_e.dbm(), phi->dbm(), phi_e.dim()); + if(!tchecker::dbm::is_le(phi_e.dbm(), phi->dbm(), phi_e.dim())) { + std::cout << __FILE__ << ": " << __LINE__ << ": phi of zone:" << std::endl; + tchecker::dbm::output_matrix(std::cout, phi->dbm(), phi->dim()); + + std::cout << __FILE__ << ": " << __LINE__ << ": phi given:" << std::endl; + tchecker::dbm::output_matrix(std::cout, phi_e.dbm(), phi_e.dim()); + + return false; + + } + + return true; } void sync(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, @@ -182,7 +193,7 @@ revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2, sync(dbm1_synced, dbm2_synced, dim1, dim2, no_of_orig_clocks_1, no_of_orig_clocks_2, orig_reset_set_A, orig_reset_set_B); - assert(is_phi_subset_of_a_zone(dbm1_synced, dim1, no_of_orig_clocks_1, phi_e) || is_phi_subset_of_a_zone(dbm2_synced, dim2, no_of_orig_clocks_2, phi_e)); + assert(is_phi_subset_of_a_zone(dbm1_synced, dim1, no_of_orig_clocks_1, phi_e) && is_phi_subset_of_a_zone(dbm2_synced, dim2, no_of_orig_clocks_2, phi_e)); if(tchecker::dbm::status_t::EMPTY == tchecker::dbm::constrain(dbm1_synced, dim1, phi_e.get_vc(no_of_orig_clocks_1, true))) { throw std::runtime_error("problems in _A while reverting the sync"); // should NEVER occur @@ -192,14 +203,18 @@ revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2, throw std::runtime_error("problems in _B while reverting the sync"); // should NEVER occur } - tchecker::dbm::db_t * multiple_reset = revert_multiple_reset(dbm1, dim1, dbm1_synced, virt_reset_set_A); + tchecker::dbm::db_t *multiple_reset = (tchecker::dbm::db_t *)malloc(dim1*dim1*sizeof(tchecker::dbm::db_t)); + + enum tchecker::dbm::status_t stat_1 = revert_multiple_reset(multiple_reset, dbm1, dim1, dbm1_synced, virt_reset_set_A); std::shared_ptr first = tchecker::virtual_constraint::factory(multiple_reset, dim1, no_of_orig_clocks_1 + no_of_orig_clocks_2); free(multiple_reset); - multiple_reset = revert_multiple_reset(dbm2, dim2, dbm2_synced, virt_reset_set_B); + multiple_reset = (tchecker::dbm::db_t *)malloc(dim2*dim2*sizeof(tchecker::dbm::db_t)); + + enum tchecker::dbm::status_t stat_2 = revert_multiple_reset(multiple_reset, dbm2, dim2, dbm2_synced, virt_reset_set_B); std::shared_ptr second = tchecker::virtual_constraint::factory(multiple_reset, dim2, no_of_orig_clocks_1 + no_of_orig_clocks_2); @@ -213,8 +228,17 @@ revert_sync(const tchecker::dbm::db_t *dbm1, const tchecker::dbm::db_t *dbm2, virt_reset_set_A.clear(); virt_reset_set_B.clear(); - assert(is_phi_subset_of_a_zone(dbm1, dim1, no_of_orig_clocks_1, *first)); - assert(is_phi_subset_of_a_zone(dbm2, dim2, no_of_orig_clocks_2, *second)); + if (tchecker::dbm::EMPTY == stat_1) { + tchecker::dbm::empty(first->dbm(), first->dim()); + } else { + assert(is_phi_subset_of_a_zone(dbm1, dim1, no_of_orig_clocks_1, *first)); + } + + if (tchecker::dbm::EMPTY == stat_2) { + tchecker::dbm::empty(second->dbm(), second->dim()); + } else { + assert(is_phi_subset_of_a_zone(dbm2, dim2, no_of_orig_clocks_2, *second)); + } return std::make_pair(first, second); } diff --git a/src/vcg/virtual_constraint.cc b/src/vcg/virtual_constraint.cc index c73bbd8e..4e930964 100644 --- a/src/vcg/virtual_constraint.cc +++ b/src/vcg/virtual_constraint.cc @@ -84,14 +84,9 @@ std::shared_ptr> virtual_constr } } - return result; -} + result->compress(); -std::shared_ptr> virtual_constraint_t::neg() const -{ - tchecker::dbm::db_t univ[this->dim()*this->dim()]; - tchecker::dbm::universal(univ, this->dim()); - return neg_helper(univ); + return result; } clock_constraint_container_t virtual_constraint_t::get_vc(tchecker::clock_id_t no_of_orig_clocks, bool system_clocks) const @@ -256,6 +251,8 @@ std::shared_ptr> combine(tcheck } + result->compress(); + return result; } @@ -273,27 +270,28 @@ bool all_elements_are_stronger_than(std::shared_ptr> contained_in_all(std::vector>> & zones, tchecker::clock_id_t no_of_virtual_clocks) +std::shared_ptr> contained_in_all(std::vector>> & vc, tchecker::clock_id_t no_of_virtual_clocks) { assert( - std::all_of(zones.begin(), zones.end(), - [no_of_virtual_clocks](std::shared_ptr> & lo_zones){return no_of_virtual_clocks + 1 == lo_zones->dim();} // cppcheck-suppress [assertWithSideEffect] + std::all_of(vc.begin(), vc.end(), + [no_of_virtual_clocks](std::shared_ptr> & lo_vc){return no_of_virtual_clocks + 1 == lo_vc->dim();} // cppcheck-suppress [assertWithSideEffect] ) ); - if (zones.empty()) { + if (vc.empty()) { return std::make_shared>(no_of_virtual_clocks + 1); } - if (1 == zones.size()) { - return (zones[0]); + if (1 == vc.size()) { + (vc[0])->compress(); + return vc[0]; } - std::shared_ptr> cur = zones.back(); - zones.pop_back(); + std::shared_ptr> cur = vc.back(); + vc.pop_back(); - std::shared_ptr> inter = contained_in_all(zones, no_of_virtual_clocks); + std::shared_ptr> inter = contained_in_all(vc, no_of_virtual_clocks); std::shared_ptr> result = std::make_shared>(no_of_virtual_clocks + 1); @@ -320,6 +318,8 @@ std::shared_ptr> contained_in_a assert(all_elements_are_stronger_than(cur, result, no_of_virtual_clocks)); + result->compress(); + return result; }