Skip to content

Commit

Permalink
Add cdd_done to test case
Browse files Browse the repository at this point in the history
To prevent memory issues, the actual test case is placed into its own namespace, see UPPAALModelChecker#31 and UPPAALModelChecker#36.
  • Loading branch information
Martijn Goorden committed Jul 27, 2022
1 parent 870e053 commit b917ba1
Showing 1 changed file with 46 additions and 41 deletions.
87 changes: 46 additions & 41 deletions test/test_cdd.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -899,47 +899,52 @@ TEST_CASE("CDD timed predecessor static test")
cdd_add_clocks(4);
cdd_add_bddvar(3);

cdd b6 = cdd_bddvarpp(bdd_start_level + 0);
cdd b7 = cdd_bddvarpp(bdd_start_level + 1);
cdd b8 = cdd_bddvarpp(bdd_start_level + 2);

// Create input cdd.
cdd input = cdd_intervalpp(1, 0, 6, 10);
input &= cdd_intervalpp(2, 0, 5, dbm_LS_INFINITY);
input &= cdd_intervalpp(3, 0, 8, dbm_LS_INFINITY);
input &= b6;
cdd_reduce(input);

// Create safe cdd, which will be safe1 | safe2.
cdd safe1 = cdd_intervalpp(1, 0, 0, 4);
safe1 &= cdd_intervalpp(2, 0, 0, dbm_LS_INFINITY);
safe1 &= cdd_intervalpp(3, 0, 0, dbm_LS_INFINITY);
safe1 &= b7;

cdd safe2 = cdd_intervalpp(1, 0, 7, 9);
safe2 &= cdd_intervalpp(2, 0, 0, 4);
safe2 &= cdd_intervalpp(3, 0, 0, 3);
safe2 &= b8;
cdd safe = safe1 | safe2;
cdd_reduce(safe);

// Perform the timed predecessor operator and remove any negative clock values.
cdd result = cdd_remove_negative(cdd_predt(input, safe));

// Create the expected cdd.
cdd expected1 = cdd_intervalpp(1, 0, 0, 4);
expected1 &= cdd_intervalpp(2, 1, -5, dbm_LS_INFINITY);
expected1 &= cdd_intervalpp(3, 1, -1, dbm_LS_INFINITY);
expected1 &= b6;
expected1 &= !b7;
cdd expected2 = cdd_intervalpp(1, 0, 4, 10);
expected2 &= cdd_intervalpp(2, 1, -5, dbm_LS_INFINITY);
expected2 &= cdd_intervalpp(3, 1, -1, dbm_LS_INFINITY);
expected2 &= b6;
cdd expected = cdd_remove_negative(expected1 | expected2);

// Check whether the result matches the expected one.
REQUIRE(cdd_equiv(result, expected));
// TODO For now, the actual test case has to be in its own name space, otherwise cdd_done() will generate memory
// issues, see issue #36.
{
cdd b6 = cdd_bddvarpp(bdd_start_level + 0);
cdd b7 = cdd_bddvarpp(bdd_start_level + 1);
cdd b8 = cdd_bddvarpp(bdd_start_level + 2);

// Create input cdd.
cdd input = cdd_intervalpp(1, 0, 6, 10);
input &= cdd_intervalpp(2, 0, 5, dbm_LS_INFINITY);
input &= cdd_intervalpp(3, 0, 8, dbm_LS_INFINITY);
input &= b6;
cdd_reduce(input);

// Create safe cdd, which will be safe1 | safe2.
cdd safe1 = cdd_intervalpp(1, 0, 0, 4);
safe1 &= cdd_intervalpp(2, 0, 0, dbm_LS_INFINITY);
safe1 &= cdd_intervalpp(3, 0, 0, dbm_LS_INFINITY);
safe1 &= b7;

cdd safe2 = cdd_intervalpp(1, 0, 7, 9);
safe2 &= cdd_intervalpp(2, 0, 0, 4);
safe2 &= cdd_intervalpp(3, 0, 0, 3);
safe2 &= b8;
cdd safe = safe1 | safe2;
cdd_reduce(safe);

// Perform the timed predecessor operator and remove any negative clock values.
cdd result = cdd_remove_negative(cdd_predt(input, safe));

// Create the expected cdd.
cdd expected1 = cdd_intervalpp(1, 0, 0, 4);
expected1 &= cdd_intervalpp(2, 1, -5, dbm_LS_INFINITY);
expected1 &= cdd_intervalpp(3, 1, -1, dbm_LS_INFINITY);
expected1 &= b6;
expected1 &= !b7;
cdd expected2 = cdd_intervalpp(1, 0, 4, 10);
expected2 &= cdd_intervalpp(2, 1, -5, dbm_LS_INFINITY);
expected2 &= cdd_intervalpp(3, 1, -1, dbm_LS_INFINITY);
expected2 &= b6;
cdd expected = cdd_remove_negative(expected1 | expected2);

// Check whether the result matches the expected one.
REQUIRE(cdd_equiv(result, expected));
}
cdd_done();
}

// TODO: the bellow test case passes only on 32-bit, need to fix it
Expand Down

0 comments on commit b917ba1

Please sign in to comment.