Skip to content

Commit

Permalink
Fix pipeline (#9)
Browse files Browse the repository at this point in the history
fixed pipeline
  • Loading branch information
alzeha authored Sep 24, 2024
1 parent fcc5712 commit 661ef25
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 9 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
.vscode/*
2 changes: 2 additions & 0 deletions src/vcg/revert_transitions.cc
Original file line number Diff line number Diff line change
Expand Up @@ -105,6 +105,8 @@ revert_action_trans(const tchecker::zg::zone_t & zone,
std::shared_ptr<tchecker::virtual_constraint::virtual_constraint_t> virt_mult_reset
= tchecker::virtual_constraint::factory(reverted, zone.dim(), phi_split.get_no_of_virtual_clocks());

free(reverted);

return virt_mult_reset;
}

Expand Down
29 changes: 20 additions & 9 deletions test/unit-tests/test-virtual_constraint.hh
Original file line number Diff line number Diff line change
Expand Up @@ -38,16 +38,17 @@ TEST_CASE ("Extract virtual constraint", "[evc]") {

// create container with all clock constraints, 0 = x, 1 = y, 2 = z, 3 = w, for zero clock one has to use tchecker::REFCLOCK_ID
tchecker::clock_constraint_container_t cc_container;
for (int i = 0; i < dim-1; i++)
for (tchecker::clock_id_t i = 0; i < dim-1; i++)
{
tchecker::clock_constraint_t cc_tmp = tchecker::clock_constraint_t(i, tchecker::REFCLOCK_ID, tchecker::LE, i+1);
int32_t i_32bit = (int32_t) i;
tchecker::clock_constraint_t cc_tmp = tchecker::clock_constraint_t(i, tchecker::REFCLOCK_ID, tchecker::LE, i_32bit+1);
cc_container.push_back(cc_tmp);
cc_tmp = tchecker::clock_constraint_t(tchecker::REFCLOCK_ID, i, tchecker::LE, -i-1);
cc_tmp = tchecker::clock_constraint_t(tchecker::REFCLOCK_ID, i, tchecker::LE, -i_32bit-1);
cc_container.push_back(cc_tmp);

for (tchecker::clock_id_t j = 0; j < dim-1; j++)
{
tchecker::clock_constraint_t cc_tmp = tchecker::clock_constraint_t(i, j, tchecker::LE, i-j);
tchecker::clock_constraint_t cc_tmp = tchecker::clock_constraint_t(i, j, tchecker::LE, i_32bit-j);
cc_container.push_back(cc_tmp);
}
}
Expand Down Expand Up @@ -147,6 +148,16 @@ TEST_CASE ("Extract virtual constraint", "[evc]") {


SECTION ("Test for completeness of vc_comp and zone_comp") {
std::string base_string = "zone dbm is ";
std::stringstream info(base_string);
info << std::endl;
tchecker::dbm::output_matrix(info, zone_comp->dbm(), zone_comp->dim());
info << "vc dbm is " << std::endl;
tchecker::dbm::output_matrix(info, vc_comp->dbm(), vc_comp->dim());
info << "clock_val_w_toosmall is " << std::endl;
std::function<std::string(tchecker::clock_id_t)> clk_name {[](tchecker::clock_id_t clk) {return std::to_string(clk);}};
tchecker::output(info, *clockval_w_toosmall, clk_name );
INFO(info.str());
REQUIRE(zone_comp->belongs(*clockval_fitting));
REQUIRE_FALSE(zone_comp->belongs(*clockval_x_toobig));
REQUIRE_FALSE(zone_comp->belongs(*clockval_x_toosmall));
Expand Down Expand Up @@ -270,7 +281,7 @@ TEST_CASE ("Revert Action Trans Operator", "[rato]") {
std::shared_ptr<tchecker::zg::zone_t> zone_D_sigma_A_0 = tchecker::zg::factory(dim);

// Set guard constraints
for (int i = 0; i < dim-1; i++)
for (unsigned int i = 0; i < dim-1; i++)
{
// guard->emplace_back(i, tchecker::REFCLOCK_ID, tchecker::LE, i+1);
guard->emplace_back(tchecker::REFCLOCK_ID, i, tchecker::LE, -i-1);
Expand Down Expand Up @@ -321,7 +332,7 @@ TEST_CASE ("Revert Action Trans Operator", "[rato]") {
std::shared_ptr<tchecker::zg::zone_t> zone_D_sigma_A_1 = tchecker::zg::factory(dim);

// Set guard constraints
for (int i = 0; i < dim-1; i++)
for (unsigned int i = 0; i < dim-1; i++)
{
guard_1->emplace_back(tchecker::REFCLOCK_ID, i, tchecker::LE, -i-1);
}
Expand Down Expand Up @@ -364,7 +375,7 @@ TEST_CASE ("Revert Action Trans Operator", "[rato]") {
std::shared_ptr<tchecker::zg::zone_t> zone_D_sigma_A_2 = tchecker::zg::factory(dim);

// Set guard constraints
for (int i = 0; i < dim-1; i++)
for (unsigned int i = 0; i < dim-1; i++)
{
guard_2->emplace_back(tchecker::REFCLOCK_ID, i, tchecker::LE, -i-1);
}
Expand Down Expand Up @@ -407,7 +418,7 @@ TEST_CASE ("Revert Action Trans Operator", "[rato]") {
std::shared_ptr<tchecker::zg::zone_t> zone_D_sigma_A_3 = tchecker::zg::factory(dim);

// Set guard constraints
for (int i = 0; i < dim-1; i++)
for (unsigned int i = 0; i < dim-1; i++)
{
guard_3->emplace_back(tchecker::REFCLOCK_ID, i, tchecker::LE, -i-1);
}
Expand Down Expand Up @@ -446,7 +457,7 @@ TEST_CASE ("Revert Action Trans Operator", "[rato]") {
std::shared_ptr<tchecker::zg::zone_t> zone_D_sigma_A_4 = tchecker::zg::factory(dim);

// Set guard constraints
for (int i = 0; i < dim-1; i++) {
for (unsigned int i = 0; i < dim-1; i++) {
guard_4->emplace_back(tchecker::REFCLOCK_ID, i, tchecker::LE, -i-1);
}

Expand Down

0 comments on commit 661ef25

Please sign in to comment.