diff --git a/examples/Lieb_et_al_6.sh b/examples/Lieb_et_al_6.sh new file mode 100755 index 00000000..4cb3eb97 --- /dev/null +++ b/examples/Lieb_et_al_6.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +cat "$(dirname $0)/strong_timed_bisim_system_tests/Lieb_et_al/A6.txt" + diff --git a/examples/strong_timed_bisim_system_tests/Lieb_et_al/A6.txt b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A6.txt new file mode 100644 index 00000000..aa4d414d --- /dev/null +++ b/examples/strong_timed_bisim_system_tests/Lieb_et_al/A6.txt @@ -0,0 +1,26 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A6 + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +location:P:BPrime{invariant: x<2} +location:P:CPrime{} + +edge:P:A:B:a{provided: x >= 1 : do: x=0} +edge:P:B:C:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} + +edge:P:A:BPrime:a{provided: x <= 1 : do: x=0} +edge:P:BPrime:CPrime:b{} +edge:P:CPrime:A:c{provided: x>3 : do: x=0} diff --git a/include/tchecker/dbm/dbm.hh b/include/tchecker/dbm/dbm.hh index 5fdab570..25d870c0 100644 --- a/include/tchecker/dbm/dbm.hh +++ b/include/tchecker/dbm/dbm.hh @@ -586,15 +586,15 @@ enum tchecker::dbm::status_t intersection(tchecker::dbm::db_t * dbm, tchecker::d /*! \brief revert-multiple-reset function (see the TR of Lieb et al.) - \param orig_zone the previous zone + \param result : where the result will be stored (must be allocated) + \param orig_zone : the previous zone \param zone_split : the split of reset(orig_zone) \param reset : the used reset set - \return the dbm with reverted resets (same dim as orig_zone) - \note the returned dbm is allocated on the heap. You have to free it! + \return void */ enum tchecker::dbm::status_t revert_multiple_reset(tchecker::dbm::db_t *result, const tchecker::dbm::db_t * orig_zone, - tchecker::clock_id_t dim, tchecker::dbm::db_t * zone_split, - tchecker::clock_reset_container_t reset); + tchecker::clock_id_t dim, tchecker::dbm::db_t * zone_split, + tchecker::clock_reset_container_t reset); /*! \brief ExtraM extrapolation diff --git a/include/tchecker/strong-timed-bisim/virtual_clock_algorithm.hh b/include/tchecker/strong-timed-bisim/virtual_clock_algorithm.hh index 02f83768..ae2139d7 100644 --- a/include/tchecker/strong-timed-bisim/virtual_clock_algorithm.hh +++ b/include/tchecker/strong-timed-bisim/virtual_clock_algorithm.hh @@ -74,14 +74,12 @@ private: \param symbolic_trans_first : the transition with which we reached the first symbolic state \param symb_state_second : the symbolic state that belongs to the second vcg \param symbolic_trans_second : the transition with which we reached the second symbolic state - \param last_was_epsilon : whether the last transition was a delay transition \return a list of virtual constraints that are not bisimilar */ std::shared_ptr> 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, custom_hash, custom_equal> & visited, - bool last_was_epsilon); + std::unordered_set, custom_hash, custom_equal> & visited); /*! \brief check-for-outgoing-transitions-impl function of Lieb et al. diff --git a/include/tchecker/utils/zone_container.hh b/include/tchecker/utils/zone_container.hh index 69a4c86a..eeb295cf 100644 --- a/include/tchecker/utils/zone_container.hh +++ b/include/tchecker/utils/zone_container.hh @@ -196,6 +196,7 @@ public: - zc_prev._dim = zc_after._dim - for all zone_prev in zc_prev : for all u in zone_prev : exists zone_after in zc_after : u in zone_after - for all zone_after in zc_after : for all u in zone_after : exists zone_prev in zc_prev : u in zone_prev + \note see chapter 7.6 of Rokicki "Representing and modeling digital circuits" (PhD thesis) */ void compress() diff --git a/include/tchecker/vcg/sync.hh b/include/tchecker/vcg/sync.hh index ae4e2bba..390228b9 100644 --- a/include/tchecker/vcg/sync.hh +++ b/include/tchecker/vcg/sync.hh @@ -59,8 +59,9 @@ bool are_dbm_synced(tchecker::dbm::db_t *dbm1, tchecker::dbm::db_t *dbm2, \param dbm1 : a dbm \param dbm2 : a dbm \param dim : dimension of dbm1 and dbm2 - \param lowest_virt_clk_id : the clk id of chi_0 \param no_of_orig_clocks_1 : the number of orig clocks in the first TA + \param no_of_orig_clocks_1 : the number of orig clocks in the first TA + \param phi_e : the vc to revert \pre dbm1 and dbm2 are not nullptr (checked by assertion) dbm, dbm1 and dbm2 are dim*dim arrays of difference bounds dbm1 and dbm2 are consistent (checked by assertion) diff --git a/src/dbm/dbm.cc b/src/dbm/dbm.cc index 0cc3edd2..d9ab5a77 100644 --- a/src/dbm/dbm.cc +++ b/src/dbm/dbm.cc @@ -1349,11 +1349,15 @@ enum tchecker::dbm::union_convex_t convex_union(tchecker::dbm::db_t *result, tch } if(dbm2_tight.empty()) { + assert(tchecker::dbm::is_consistent(result, dim)); + assert(tchecker::dbm::is_tight(result, dim)); return tchecker::dbm::union_convex_t::UNION_IS_CONVEX; } if (dbm1_tight.empty()) { tchecker::dbm::copy(result, dbm2, dim); + assert(tchecker::dbm::is_consistent(result, dim)); + assert(tchecker::dbm::is_tight(result, dim)); return tchecker::dbm::union_convex_t::UNION_IS_CONVEX; } @@ -1369,6 +1373,8 @@ enum tchecker::dbm::union_convex_t convex_union(tchecker::dbm::db_t *result, tch } } + assert(tchecker::dbm::is_consistent(result, dim)); + assert(tchecker::dbm::is_tight(result, dim)); return tchecker::dbm::union_convex_t::UNION_IS_CONVEX; } diff --git a/src/strong-timed-bisim/virtual_clock_algorithm.cc b/src/strong-timed-bisim/virtual_clock_algorithm.cc index 1f084025..9b7162f1 100644 --- a/src/strong-timed-bisim/virtual_clock_algorithm.cc +++ b/src/strong-timed-bisim/virtual_clock_algorithm.cc @@ -47,7 +47,7 @@ tchecker::strong_timed_bisim::stats_t Lieb_et_al::run() { std::unordered_set, custom_hash, custom_equal> empty; std::shared_ptr> result - = this->check_for_virt_bisim(const_first, std::get<2>(sst_first[0]), const_second, std::get<2>(sst_second[0]), empty, false); + = this->check_for_virt_bisim(const_first, std::get<2>(sst_first[0]), const_second, std::get<2>(sst_second[0]), empty); stats.set_end_time(); @@ -136,193 +136,187 @@ bool is_phi_subset_of_a_zone(const tchecker::dbm::db_t *dbm, tchecker::clock_id_ std::shared_ptr> 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, custom_hash, custom_equal> & visited, - bool last_was_epsilon) + std::unordered_set, custom_hash, custom_equal> & visited) { - 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)); - } + 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> result +/* + 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()); +*/ + + // the following is a difference to the original function, done for efficiency reasons. + // before we do anything, we check whether there even exist an overlap between the symbolic states + // to do so, we build zone_A \land virtual_constraint(zone_B) and vice versa first and check whether they are empty + std::shared_ptr> overhang = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); + tchecker::zg::state_sptr_t A_constrained = _A->clone_state(symb_state_first); + tchecker::zg::state_sptr_t B_constrained = _B->clone_state(symb_state_second); + std::shared_ptr phi_A = tchecker::virtual_constraint::factory(symb_state_first->zone(), _A->get_no_of_virtual_clocks()); std::shared_ptr 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()) + tchecker::dbm::status_t::EMPTY == phi_B->logic_and(A_constrained->zone(), A_constrained->zone()) || + tchecker::dbm::status_t::EMPTY == phi_A->logic_and(B_constrained->zone(), B_constrained->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())); + + std::shared_ptr A_helper = tchecker::virtual_constraint::factory(symb_state_first->zone(), _A->get_no_of_virtual_clocks()); + std::shared_ptr B_helper = tchecker::virtual_constraint::factory(symb_state_second->zone(), _A->get_no_of_virtual_clocks()); + + overhang->append_zone(A_helper); + overhang->append_zone(B_helper); + assert(all_vc_are_sub_vc_of_phi_a_or_phi_b(*overhang, 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; + overhang->compress(); + return overhang; } - //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> to_append_A + // we calculate the overhang + std::shared_ptr> overhang_A = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); - std::shared_ptr> to_append_B + std::shared_ptr> overhang_B = std::make_shared>(_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); + phi_B->neg_logic_and(overhang_A, *phi_A); + phi_A->neg_logic_and(overhang_B, *phi_B); - result->append_container(to_append_A); - result->append_container(to_append_B); + overhang->append_container(overhang_A); + overhang->append_container(overhang_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())); + assert(all_vc_are_sub_vc_of_phi_a_or_phi_b(*overhang, 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()); - } + + // now that we have calculated the overhang, we can go on with our algorithm + tchecker::zg::state_sptr_t A_synced = _A->clone_state(A_constrained); + tchecker::zg::state_sptr_t B_synced = _B->clone_state(B_constrained); + + // we sync the symbolic states + 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()); 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 normalized_pair{A_normed, B_normed}; + //calculating the future + tchecker::zg::state_sptr_t A_epsilon = _A->clone_state(A_synced); + tchecker::zg::state_sptr_t B_epsilon = _B->clone_state(B_synced); + _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()); - 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; - } + assert(tchecker::dbm::is_tight(A_epsilon->zone().dbm(), A_epsilon->zone().dim())); + assert(tchecker::dbm::is_tight(B_epsilon->zone().dbm(), B_epsilon->zone().dim())); - // If we haven't seen this pair, yet, add it to visited - visited.insert(normalized_pair); - std::shared_ptr> lo_not_simulatable + //calculating the overhang of the future + std::shared_ptr> epsilon_overhang = std::make_shared>(_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()); + std::shared_ptr phi_A_epsilon = tchecker::virtual_constraint::factory(A_epsilon->zone(), _A->get_no_of_virtual_clocks()); + std::shared_ptr phi_B_epsilon = tchecker::virtual_constraint::factory(B_epsilon->zone(), _A->get_no_of_virtual_clocks()); - tchecker::zg::const_state_sptr_t const_A_epsilon{A_epsilon}; - tchecker::zg::const_state_sptr_t const_B_epsilon{B_epsilon}; + overhang_A = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); + overhang_B = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); - std::shared_ptr> 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 + phi_B_epsilon->neg_logic_and(overhang_A, *phi_A_epsilon); + phi_A_epsilon->neg_logic_and(overhang_B, *phi_B_epsilon); - for(auto iter = result_epsilon->begin(); iter < result_epsilon->end(); 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)); - } + epsilon_overhang->append_container(overhang_A); + epsilon_overhang->append_container(overhang_B); - } - else { - tchecker::zg::const_state_sptr_t const_A_normed{A_normed}; - tchecker::zg::const_state_sptr_t const_B_normed{B_normed}; + // normalizing, to check whether we have already seen this pair. + tchecker::zg::state_sptr_t A_normed = _A->clone_state(A_epsilon); + tchecker::zg::state_sptr_t B_normed = _B->clone_state(B_epsilon); - // 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)); - } + _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())); - lo_not_simulatable->compress(); + tchecker::dbm::tighten(A_normed->zone().dbm(), A_normed->zone().dim()); + tchecker::dbm::tighten(B_normed->zone().dbm(), B_normed->zone().dim()); - // now we have to revert the extrapolation + std::pair normalized_pair{A_normed, B_normed}; - std::shared_ptr> reverted_extrapolation + std::shared_ptr> check_trans = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); - std::shared_ptr 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 + // only go into the recursion if we have not seen this pair yet + if(0 == visited.count(normalized_pair)) { + // add the pair to visited + visited.insert(normalized_pair); - for(auto iter = lo_not_simulatable->begin(); iter < lo_not_simulatable->end(); iter++) { - std::shared_ptr 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); - } + // check the outgoing action transitions + tchecker::zg::const_state_sptr_t const_A_normed{A_normed}; + tchecker::zg::const_state_sptr_t const_B_normed{B_normed}; + + check_trans->append_container(check_for_outgoing_transitions(const_A_normed, const_B_normed, visited)); } - reverted_extrapolation->compress(); - // finally, we revert the sync + // collect all results for the epsilon transition + std::shared_ptr> epsilon_result + = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); - std::shared_ptr another_phi_A = tchecker::virtual_constraint::factory(symb_state_first->zone(), _A->get_no_of_virtual_clocks()); - std::shared_ptr another_phi_B = tchecker::virtual_constraint::factory(symb_state_second->zone(), _B->get_no_of_virtual_clocks()); + epsilon_result->append_container(check_trans); + epsilon_result->append_container(epsilon_overhang); - 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); + epsilon_result->compress(); - another_phi_A->logic_and(B_clone->zone(), symb_state_second->zone()); - another_phi_B->logic_and(A_clone->zone(), symb_state_first->zone()); + // now revert them + std::shared_ptr> epsilon_rev_not_comb + = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); + for(auto iter = epsilon_result->begin(); iter < epsilon_result->end(); iter++) { + std::shared_ptr A_helper = tchecker::virtual_constraint::factory(A_epsilon->zone(), _A->get_no_of_virtual_clocks()); + std::shared_ptr B_helper = tchecker::virtual_constraint::factory(B_epsilon->zone(), _A->get_no_of_virtual_clocks()); + (*iter)->logic_and(A_helper, *A_helper); + (*iter)->logic_and(B_helper, *B_helper); + + epsilon_rev_not_comb->append_zone(tchecker::vcg::revert_epsilon_trans(A_synced->zone(), A_epsilon->zone(), *A_helper)); + epsilon_rev_not_comb->append_zone(tchecker::vcg::revert_epsilon_trans(B_synced->zone(), B_epsilon->zone(), *B_helper)); + } - tchecker::zone_container_t inter{_A->get_no_of_virtual_clocks() + 1}; + std::shared_ptr> epsilon_rev = tchecker::virtual_constraint::combine(*epsilon_rev_not_comb, _A->get_no_of_virtual_clocks()); - for(auto iter = reverted_extrapolation->begin(); iter < reverted_extrapolation->end(); iter++) { - std::pair, std::shared_ptr> 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); + epsilon_rev->compress(); - 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))); - } + // in the technical report, we rename overhang to sync-reverted. this is not necessary here. Therefore, we proceed to use the variable overhang instead. + for(auto iter = epsilon_rev->begin(); iter < epsilon_rev->end(); iter++) { + std::pair, std::shared_ptr> sync_reverted + = tchecker::vcg::revert_sync(A_constrained->zone_ptr()->dbm(), B_constrained->zone_ptr()->dbm(), A_constrained->zone_ptr()->dim(), B_constrained->zone_ptr()->dim(), + _A->get_no_of_original_clocks(), _B->get_no_of_original_clocks(), + **iter); - 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))); - } + overhang->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))); + overhang->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(); + overhang->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())); + std::shared_ptr> result + = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); - result->append_container(tchecker::virtual_constraint::combine(inter, _A->get_no_of_virtual_clocks())); + result->append_container(tchecker::virtual_constraint::combine(*overhang, _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())); @@ -330,7 +324,16 @@ Lieb_et_al::check_for_virt_bisim(tchecker::zg::const_state_sptr_t symb_state_fir //std::cout << __FILE__ << ": " << __LINE__ << ": _delete_me: " << _delete_me << std::endl; result->compress(); +/* + std::cout << __FILE__ << ": " << __LINE__ << ": _visited_pair_of_states: " << _visited_pair_of_states << std::endl; + std::cout << __FILE__ << ": " << __LINE__ << ": check-for-virt-bisim return value" << std::endl; + std::cout << __FILE__ << ": " << __LINE__ << ": " << symb_state_first->vloc() << symb_state_second->vloc() << std::endl; + for(auto iter = result->begin(); iter < result->end(); iter++) { + std::cout << std::endl; + tchecker::dbm::output_matrix(std::cout, (*iter)->dbm(), (*iter)->dim()); + } +*/ return result; } @@ -340,10 +343,6 @@ Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t A_s tchecker::zg::const_state_sptr_t B_state, std::unordered_set, custom_hash, custom_equal> & visited) { - - std::shared_ptr> result - = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); - std::vector v_first, v_second; _A->next(A_state, v_first); _B->next(B_state, v_second); @@ -404,38 +403,42 @@ Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t A_s std::unordered_set, custom_hash, custom_equal> copy(visited); std::shared_ptr> inter - = this->check_for_virt_bisim(const_s_first, t_first, const_s_second, t_second, copy, false); + = this->check_for_virt_bisim(const_s_first, t_first, const_s_second, t_second, copy); - auto A_s_ret_val_idx = std::make_tuple >*, - lo_return_values *, - long unsigned int *>(&s_first, &A_return_values, &i); + std::shared_ptr> to_append_A + = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); + std::shared_ptr> to_append_B + = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); - auto B_s_ret_val_idx = std::make_tuple >*, - lo_return_values *, - long unsigned int *>(&s_second, &B_return_values, &j); + for(auto iter = inter->begin(); iter < inter->end(); iter++) { + std::shared_ptr tmp_first = tchecker::zg::factory(s_first->zone().dim()); + std::shared_ptr tmp_second = tchecker::zg::factory(s_second->zone().dim()); - auto s_ret_val_idx_together = {&A_s_ret_val_idx, &B_s_ret_val_idx}; + + if(tchecker::dbm::NON_EMPTY == (*iter)->logic_and(tmp_first, s_first->zone()) ) { + to_append_A->append_zone(tchecker::virtual_constraint::factory(tmp_first, _A->get_no_of_virtual_clocks())); + } - 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 to_add{_A->get_no_of_virtual_clocks() + 1}; - for(auto iter = inter->begin(); iter < inter->end(); iter++) { - std::shared_ptr 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())); - } + if(tchecker::dbm::NON_EMPTY == (*iter)->logic_and(tmp_second, s_second->zone()) ) { + to_append_B->append_zone(tchecker::virtual_constraint::factory(tmp_second, _A->get_no_of_virtual_clocks())); } - to_add.compress(); - (*ret_val_cur)[*index_cur].emplace_back(std::make_shared>(to_add)); } + + to_append_A->compress(); + to_append_B->compress(); + + A_return_values[i].emplace_back(to_append_A); + B_return_values[j].emplace_back(to_append_B); + } } //std::cout << __FILE__ << ": " << __LINE__ << ": start revert_action_trans" << std::endl; + std::shared_ptr> collapsed + = std::make_shared>(_A->get_no_of_virtual_clocks() + 1); + for(auto iter : together) { auto v_cur = std::get<0>(*iter); auto ret_val = std::get<1>(*iter); @@ -447,7 +450,7 @@ Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t A_s 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)); + collapsed->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)); } } } @@ -457,7 +460,7 @@ Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t A_s //std::cout << __FILE__ << ": " << __LINE__ << ": end revert_action_trans" << std::endl; assert( - std::all_of(result->begin(), result->end(), + std::all_of(collapsed->begin(), collapsed->end(), [A_state, B_state](std::shared_ptr vc) { return (is_phi_subset_of_a_zone(A_state->zone().dbm(), A_state->zone().dim(), vc->get_no_of_virt_clocks(), *vc)) || @@ -466,12 +469,11 @@ Lieb_et_al::check_for_outgoing_transitions( tchecker::zg::const_state_sptr_t A_s ) ); - result->compress(); + collapsed->compress(); //std::cout << __FILE__ << ": " << __LINE__ << ": return from check-outgoing-trans" << std::endl; - return result; - + return combine(*collapsed, collapsed->dim() - 1); } } // end of namespace strong_timed_bisim diff --git a/src/vcg/virtual_constraint.cc b/src/vcg/virtual_constraint.cc index 4e930964..62917b3f 100644 --- a/src/vcg/virtual_constraint.cc +++ b/src/vcg/virtual_constraint.cc @@ -213,17 +213,11 @@ std::shared_ptr factory(const tchecker::dbm::db_t * dbm, t std::shared_ptr> combine(tchecker::zone_container_t & lo_vc, tchecker::clock_id_t no_of_virtual_clocks) { - tchecker::zone_container_t lo_of_non_empty_vc{no_of_virtual_clocks + 1}; - - for(auto phi = lo_vc.begin(); phi < lo_vc.end(); phi++) { - if(!(*phi)->is_empty()) { - lo_of_non_empty_vc.append_zone(*phi); - } - } + lo_vc.compress(); std::shared_ptr> result = std::make_shared>(no_of_virtual_clocks + 1); - for(auto iter = lo_of_non_empty_vc.begin(); iter < lo_of_non_empty_vc.end(); iter++) { + for(auto iter = lo_vc.begin(); iter < lo_vc.end(); iter++) { std::shared_ptr> inter = std::make_shared>(no_of_virtual_clocks + 1); std::shared_ptr> helper; @@ -248,11 +242,9 @@ std::shared_ptr> combine(tcheck result->append_zone(**phi); } } - + result->compress(); } - result->compress(); - return result; } diff --git a/test/tck-compare/CMakeLists.txt b/test/tck-compare/CMakeLists.txt index 17ad3bfe..1b0927d0 100644 --- a/test/tck-compare/CMakeLists.txt +++ b/test/tck-compare/CMakeLists.txt @@ -53,6 +53,7 @@ set(INPUTS 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: + Lieb_et_al_6.sh: corsso.sh:2:2:10:1:2 critical-region-async.sh:2:10 csmacd.sh:3 @@ -94,6 +95,7 @@ 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) +list(GET TCK_COMPARE_INPUT_FILES 16 Lieb6) # check whether the no_initial_check works create_testcase(no_initial_first ${no_initial} ${ad} strong-timed-bisim) @@ -124,6 +126,7 @@ 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) +create_testcase(Lieb-et-al-1-Lieb-et-al-6 ${Lieb1} ${Lieb6} strong-timed-bisim) # Lieb2 create_testcase(Lieb-et-al-2-self ${Lieb2} ${Lieb2} strong-timed-bisim) @@ -135,20 +138,27 @@ create_testcase(Lieb-et-al-2-Lieb-et-al-2-determ-split-non-bisim ${Lieb2} ${Lieb 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) +create_testcase(Lieb-et-al-2-Lieb-et-al-6 ${Lieb2} ${Lieb6} 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) +create_testcase(Lieb-et-al-3-Lieb-et-al-6 ${Lieb3} ${Lieb6} 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) +create_testcase(Lieb-et-al-4-Lieb-et-al-6 ${Lieb4} ${Lieb6} strong-timed-bisim) #Lieb 5 create_testcase(Lieb-et-al-5-self ${Lieb5} ${Lieb5} strong-timed-bisim) +create_testcase(Lieb-et-al-5-Lieb-et-al-6 ${Lieb5} ${Lieb6} strong-timed-bisim) + +# Lieb 6 +create_testcase(Lieb-et-al-6-self ${Lieb6} ${Lieb6} strong-timed-bisim) # some self test take to long #foreach(cur ${TCK_COMPARE_INPUT_FILES}) diff --git a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-diff-inv.out-expected b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-diff-inv.out-expected index a8111856..d241142a 100644 --- a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-diff-inv.out-expected +++ b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-diff-inv.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 7 +VISITED_PAIR_OF_STATES 4 diff --git a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-non-determ-bisim.out-expected b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-non-determ-bisim.out-expected index 31efe2e6..ab728476 100644 --- a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-non-determ-bisim.out-expected +++ b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-1-non-determ-bisim.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 10 +VISITED_PAIR_OF_STATES 6 diff --git a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-2.out-expected b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-2.out-expected index a8111856..d241142a 100644 --- a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-2.out-expected +++ b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-2.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 7 +VISITED_PAIR_OF_STATES 4 diff --git a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-3.out-expected b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-3.out-expected index a8111856..d241142a 100644 --- a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-3.out-expected +++ b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-3.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 7 +VISITED_PAIR_OF_STATES 4 diff --git a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-4.out-expected b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-4.out-expected index a8111856..d241142a 100644 --- a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-4.out-expected +++ b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-4.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 7 +VISITED_PAIR_OF_STATES 4 diff --git a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-5.out-expected b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-5.out-expected index 781e1138..a8111856 100644 --- a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-5.out-expected +++ b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-5.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 12 +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-1-Lieb-et-al-6.out-expected b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-6.out-expected new file mode 100644 index 00000000..b4177db5 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-1-Lieb-et-al-6.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 5 diff --git a/test/tck-compare/Lieb-et-al-1-non-determ-bisim.out-expected b/test/tck-compare/Lieb-et-al-1-non-determ-bisim.out-expected index 31efe2e6..ab728476 100644 --- a/test/tck-compare/Lieb-et-al-1-non-determ-bisim.out-expected +++ b/test/tck-compare/Lieb-et-al-1-non-determ-bisim.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 10 +VISITED_PAIR_OF_STATES 6 diff --git a/test/tck-compare/Lieb-et-al-1-self.out-expected b/test/tck-compare/Lieb-et-al-1-self.out-expected index 24975b2e..15098ad2 100644 --- a/test/tck-compare/Lieb-et-al-1-self.out-expected +++ b/test/tck-compare/Lieb-et-al-1-self.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 7 +VISITED_PAIR_OF_STATES 4 diff --git a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-bisim.out-expected b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-bisim.out-expected index 5e696d23..24975b2e 100644 --- a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-bisim.out-expected +++ b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-bisim.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 12 +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-non-bisim.out-expected b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-non-bisim.out-expected index 781e1138..a8111856 100644 --- a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-non-bisim.out-expected +++ b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-determ-split-non-bisim.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 12 +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-non-determ-bisim.out-expected b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-non-determ-bisim.out-expected index 5e696d23..24975b2e 100644 --- a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-non-determ-bisim.out-expected +++ b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-2-non-determ-bisim.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 12 +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-3.out-expected b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-3.out-expected index 24975b2e..15098ad2 100644 --- a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-3.out-expected +++ b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-3.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 7 +VISITED_PAIR_OF_STATES 4 diff --git a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-4.out-expected b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-4.out-expected index a8111856..d241142a 100644 --- a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-4.out-expected +++ b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-4.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 7 +VISITED_PAIR_OF_STATES 4 diff --git a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-5.out-expected b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-5.out-expected index 781e1138..a8111856 100644 --- a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-5.out-expected +++ b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-5.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 12 +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-2-Lieb-et-al-6.out-expected b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-6.out-expected new file mode 100644 index 00000000..24975b2e --- /dev/null +++ b/test/tck-compare/Lieb-et-al-2-Lieb-et-al-6.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-2-self.out-expected b/test/tck-compare/Lieb-et-al-2-self.out-expected index 24975b2e..15098ad2 100644 --- a/test/tck-compare/Lieb-et-al-2-self.out-expected +++ b/test/tck-compare/Lieb-et-al-2-self.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 7 +VISITED_PAIR_OF_STATES 4 diff --git a/test/tck-compare/Lieb-et-al-3-Lieb-et-al-4.out-expected b/test/tck-compare/Lieb-et-al-3-Lieb-et-al-4.out-expected index a8111856..d241142a 100644 --- a/test/tck-compare/Lieb-et-al-3-Lieb-et-al-4.out-expected +++ b/test/tck-compare/Lieb-et-al-3-Lieb-et-al-4.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 7 +VISITED_PAIR_OF_STATES 4 diff --git a/test/tck-compare/Lieb-et-al-3-Lieb-et-al-5.out-expected b/test/tck-compare/Lieb-et-al-3-Lieb-et-al-5.out-expected index 781e1138..a8111856 100644 --- a/test/tck-compare/Lieb-et-al-3-Lieb-et-al-5.out-expected +++ b/test/tck-compare/Lieb-et-al-3-Lieb-et-al-5.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 12 +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-3-Lieb-et-al-6.out-expected b/test/tck-compare/Lieb-et-al-3-Lieb-et-al-6.out-expected new file mode 100644 index 00000000..24975b2e --- /dev/null +++ b/test/tck-compare/Lieb-et-al-3-Lieb-et-al-6.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-3-self.out-expected b/test/tck-compare/Lieb-et-al-3-self.out-expected index 24975b2e..15098ad2 100644 --- a/test/tck-compare/Lieb-et-al-3-self.out-expected +++ b/test/tck-compare/Lieb-et-al-3-self.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 7 +VISITED_PAIR_OF_STATES 4 diff --git a/test/tck-compare/Lieb-et-al-4-Lieb-et-al-5.out-expected b/test/tck-compare/Lieb-et-al-4-Lieb-et-al-5.out-expected index 781e1138..a8111856 100644 --- a/test/tck-compare/Lieb-et-al-4-Lieb-et-al-5.out-expected +++ b/test/tck-compare/Lieb-et-al-4-Lieb-et-al-5.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 12 +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-4-Lieb-et-al-6.out-expected b/test/tck-compare/Lieb-et-al-4-Lieb-et-al-6.out-expected new file mode 100644 index 00000000..a8111856 --- /dev/null +++ b/test/tck-compare/Lieb-et-al-4-Lieb-et-al-6.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 7 diff --git a/test/tck-compare/Lieb-et-al-4-self.out-expected b/test/tck-compare/Lieb-et-al-4-self.out-expected index 24975b2e..15098ad2 100644 --- a/test/tck-compare/Lieb-et-al-4-self.out-expected +++ b/test/tck-compare/Lieb-et-al-4-self.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 7 +VISITED_PAIR_OF_STATES 4 diff --git a/test/tck-compare/Lieb-et-al-5-Lieb-et-al-6.out-expected b/test/tck-compare/Lieb-et-al-5-Lieb-et-al-6.out-expected new file mode 100644 index 00000000..868655bd --- /dev/null +++ b/test/tck-compare/Lieb-et-al-5-Lieb-et-al-6.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED false +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 13 diff --git a/test/tck-compare/Lieb-et-al-5-self.out-expected b/test/tck-compare/Lieb-et-al-5-self.out-expected index 97a2aae4..118dcbdd 100644 --- a/test/tck-compare/Lieb-et-al-5-self.out-expected +++ b/test/tck-compare/Lieb-et-al-5-self.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 22 +VISITED_PAIR_OF_STATES 13 diff --git a/test/tck-compare/Lieb-et-al-6-self.out-expected b/test/tck-compare/Lieb-et-al-6-self.out-expected new file mode 100644 index 00000000..118dcbdd --- /dev/null +++ b/test/tck-compare/Lieb-et-al-6-self.out-expected @@ -0,0 +1,4 @@ +MEMORY_MAX_RSS xxxx +RELATIONSHIP_FULFILLED true +RUNNING_TIME_SECONDS xxxx +VISITED_PAIR_OF_STATES 13 diff --git a/test/tck-compare/easy-ad94-added-transition-easy-ad94.out-expected b/test/tck-compare/easy-ad94-added-transition-easy-ad94.out-expected index 99d08c5e..515b85d0 100644 --- a/test/tck-compare/easy-ad94-added-transition-easy-ad94.out-expected +++ b/test/tck-compare/easy-ad94-added-transition-easy-ad94.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 6 +VISITED_PAIR_OF_STATES 3 diff --git a/test/tck-compare/easy-ad94-different-guard-easy-ad94-added-transition.out-expected b/test/tck-compare/easy-ad94-different-guard-easy-ad94-added-transition.out-expected index b4177db5..515b85d0 100644 --- a/test/tck-compare/easy-ad94-different-guard-easy-ad94-added-transition.out-expected +++ b/test/tck-compare/easy-ad94-different-guard-easy-ad94-added-transition.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 5 +VISITED_PAIR_OF_STATES 3 diff --git a/test/tck-compare/easy-ad94-different-guard-easy-ad94.out-expected b/test/tck-compare/easy-ad94-different-guard-easy-ad94.out-expected index b4177db5..515b85d0 100644 --- a/test/tck-compare/easy-ad94-different-guard-easy-ad94.out-expected +++ b/test/tck-compare/easy-ad94-different-guard-easy-ad94.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 5 +VISITED_PAIR_OF_STATES 3 diff --git a/test/tck-compare/easy-ad94-easy-ad94-added-transition.out-expected b/test/tck-compare/easy-ad94-easy-ad94-added-transition.out-expected index 99d08c5e..515b85d0 100644 --- a/test/tck-compare/easy-ad94-easy-ad94-added-transition.out-expected +++ b/test/tck-compare/easy-ad94-easy-ad94-added-transition.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED false RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 6 +VISITED_PAIR_OF_STATES 3 diff --git a/test/tck-compare/easy-ad94-self-added-transition.out-expected b/test/tck-compare/easy-ad94-self-added-transition.out-expected index 03a58315..15098ad2 100644 --- a/test/tck-compare/easy-ad94-self-added-transition.out-expected +++ b/test/tck-compare/easy-ad94-self-added-transition.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 8 +VISITED_PAIR_OF_STATES 4 diff --git a/test/tck-compare/easy-ad94-self-different-guard.out-expected b/test/tck-compare/easy-ad94-self-different-guard.out-expected index ab728476..6926dc3f 100644 --- a/test/tck-compare/easy-ad94-self-different-guard.out-expected +++ b/test/tck-compare/easy-ad94-self-different-guard.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 6 +VISITED_PAIR_OF_STATES 3 diff --git a/test/tck-compare/easy-ad94-self.out-expected b/test/tck-compare/easy-ad94-self.out-expected index ab728476..6926dc3f 100644 --- a/test/tck-compare/easy-ad94-self.out-expected +++ b/test/tck-compare/easy-ad94-self.out-expected @@ -1,4 +1,4 @@ MEMORY_MAX_RSS xxxx RELATIONSHIP_FULFILLED true RUNNING_TIME_SECONDS xxxx -VISITED_PAIR_OF_STATES 6 +VISITED_PAIR_OF_STATES 3 diff --git a/test/tck-compare/tck-compare-Lieb_et_al_6.out-expected b/test/tck-compare/tck-compare-Lieb_et_al_6.out-expected new file mode 100644 index 00000000..aa4d414d --- /dev/null +++ b/test/tck-compare/tck-compare-Lieb_et_al_6.out-expected @@ -0,0 +1,26 @@ +# This file is a part of the TChecker project. +# +# See files AUTHORS and LICENSE for copyright details. + +system:Lieb_et_al_A6 + +clock:1:x + +event:a +event:b +event:c + +process:P +location:P:A{initial:} +location:P:B{invariant: x<2} +location:P:C{} +location:P:BPrime{invariant: x<2} +location:P:CPrime{} + +edge:P:A:B:a{provided: x >= 1 : do: x=0} +edge:P:B:C:b{} +edge:P:C:A:c{provided: x>3 : do: x=0} + +edge:P:A:BPrime:a{provided: x <= 1 : do: x=0} +edge:P:BPrime:CPrime:b{} +edge:P:CPrime:A:c{provided: x>3 : do: x=0}