Echtzeitsysteme/tchecker
1
0
Fork 0
mirror of https://github.com/Echtzeitsysteme/tchecker.git synced 2024-05-20 20:00:44 +00:00
Code Issues Packages Projects Releases Wiki Activity

aligning code to the TR

Browse source
This commit is contained in:
alzeha 2024-03-29 10:16:13 +01:00
parent ce49d61b11
commit cd24a58f8b
9 changed files with 101 additions and 70 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
include/tchecker/dbm/dbm.hh
View file

@ -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);

4
include/tchecker/utils/zone_container.hh
View file

@ -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<std::vector<std::shared_ptr<T>>> result = _storage;
bool reduced;

3
include/tchecker/vcg/revert_transitions.hh
View file

@ -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<tchecker::virtual_constraint::virtual_constraint_t>
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

18
include/tchecker/vcg/virtual_constraint.hh
View file

@ -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<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!
@ -110,6 +100,12 @@ public:
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;
/*
\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<tchecker::zone_container_t<virtual_constraint_t>> neg_helper(tchecker::dbm::db_t *upper_bounds) const;
@ -158,7 +154,7 @@ std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> combine(tcheck
\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);
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);
} // end of namespace virtual_constraint

26
src/dbm/dbm.cc
View file

@ -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);
return revert_multiple_reset(orig_zone, dim, new_split, reset);
if(tchecker::dbm::EMPTY != ret_val) {
assert(tchecker::dbm::is_tight(result, dim));
}
return ret_val;
}

17
src/strong-timed-bisim/virtual_clock_algorithm.cc
View file

@ -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();

33
src/vcg/revert_transitions.cc
View file

@ -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<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::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;
return virt_mult_reset;
}
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)
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<tchecker::virtual_constraint::virtual_constraint_t> phi_copy = factory(phi_split);
std::shared_ptr<tchecker::zg::zone_t> zone_eps_copy = tchecker::zg::factory(zone_eps);
tchecker::dbm::open_down(phi_copy->dbm(), phi_copy->dim());
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<tchecker::virtual_constraint::virtual_constraint_t> result = tchecker::virtual_constraint::factory(zone_eps_copy->dbm(), zone_eps_copy->dim(), phi_split.dim() - 1);
return result;
}
tchecker::dbm::open_down(zone_eps_copy->dbm(), zone_eps_copy->dim());
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(), true));
intersection(zone_copy->dbm(), zone_copy->dbm(), zone_eps_copy->dbm(), zone_eps_copy->dim());
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> result
= tchecker::virtual_constraint::factory(zone_copy, phi_split.get_no_of_virt_clocks());

36
src/vcg/sync.cc
View file

@ -92,7 +92,18 @@ bool is_phi_subset_of_a_zone(const tchecker::dbm::db_t *dbm, tchecker::clock_id_
{
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());
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<tchecker::virtual_constraint::virtual_constraint_t> 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<tchecker::virtual_constraint::virtual_constraint_t> 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);
}

32
src/vcg/virtual_constraint.cc
View file

@ -84,14 +84,9 @@ std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> virtual_constr
}
}
return result;
}
result->compress();
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);
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<tchecker::zone_container_t<virtual_constraint_t>> combine(tcheck
}
result->compress();
return result;
}
@ -273,27 +270,28 @@ bool all_elements_are_stronger_than(std::shared_ptr<zone_container_t<virtual_con
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)
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)
{
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]
std::all_of(vc.begin(), vc.end(),
[no_of_virtual_clocks](std::shared_ptr<zone_container_t<virtual_constraint_t>> & lo_vc){return no_of_virtual_clocks + 1 == lo_vc->dim();} // cppcheck-suppress [assertWithSideEffect]
)
);
if (zones.empty()) {
if (vc.empty()) {
return std::make_shared<tchecker::zone_container_t<virtual_constraint_t>>(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<zone_container_t<virtual_constraint_t>> cur = zones.back();
zones.pop_back();
std::shared_ptr<zone_container_t<virtual_constraint_t>> cur = vc.back();
vc.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>> inter = contained_in_all(vc, 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);
@ -320,6 +318,8 @@ std::shared_ptr<tchecker::zone_container_t<virtual_constraint_t>> contained_in_a
assert(all_elements_are_stronger_than(cur, result, no_of_virtual_clocks));
result->compress();
return result;
}