From a66daebad548f042e5d1143ba3501a190f9fc90a Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Tue, 12 Jul 2022 15:34:53 +0200 Subject: [PATCH 01/18] Add cdd_predt function Co-authored-by: Florian Lorber Co-authored-by: Florian Lorber --- include/cdd/cdd.h | 1 + src/cppext.cpp | 30 ++++++++++++++++++++++++++++++ 2 files changed, 31 insertions(+) diff --git a/include/cdd/cdd.h b/include/cdd/cdd.h index 51c485f..e9d0304 100644 --- a/include/cdd/cdd.h +++ b/include/cdd/cdd.h @@ -881,6 +881,7 @@ class cdd int32_t num_clock_resets, int32_t* bool_resets, int32_t num_bool_resets); friend cdd cdd_transition_back_past(const cdd& state, const cdd& guard, const cdd& update, int32_t* clock_resets, int32_t num_clock_resets, int32_t* bool_resets, int32_t num_bool_resets); + friend cdd cdd_predt(const cdd& target, const cdd& safe); friend cdd cdd_reduce2(const cdd&); friend bool cdd_contains(const cdd&, raw_t* dbm, int32_t dim); friend cdd cdd_extract_dbm(const cdd&, raw_t* dbm, int32_t dim); diff --git a/src/cppext.cpp b/src/cppext.cpp index 13ae89e..d34ac4d 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -114,6 +114,36 @@ cdd cdd_delay(const cdd& state) return res; } +cdd cdd_predt(const cdd& target, const cdd& safe) +{ + cdd allThatKillsUs = cdd_false(); + uint32_t size = cdd_clocknum; + cdd copy = target; + ADBM(dbm); + while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) { + extraction_result res = cdd_extract_bdd_and_dbm(copy); + copy = cdd_reduce(cdd_remove_negative(res.CDD_part)); + dbm = res.dbm; + cdd bdd = res.BDD_part; + cdd bdd_intersect = bdd & safe; + if ( bdd_intersect != cdd_false()) + { + dbm_down(dbm, size); + cdd past = cdd(dbm,size); + past &= bdd; + cdd escape = safe & past; + allThatKillsUs |= (past - escape); + } + else + { + dbm_down(dbm,size); + cdd past = cdd (dbm, size) & bdd; + allThatKillsUs |= past; + } + } + return allThatKillsUs; +} + /** * Perform the delay operation on a CDD taking an invariant into account. * From 04a7caebef991fe2fb5ca9dab5d4393f931a8ed4 Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Tue, 12 Jul 2022 15:44:04 +0200 Subject: [PATCH 02/18] Add first part of the cdd_predt fix Co-authored-by: Florian Lorber --- src/cppext.cpp | 55 +++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 43 insertions(+), 12 deletions(-) diff --git a/src/cppext.cpp b/src/cppext.cpp index d34ac4d..1d72460 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -10,6 +10,7 @@ /////////////////////////////////////////////////////////////////////////////// #include "cdd/kernel.h" +#include "dbm/fed.h" #define ADBM(NAME) raw_t* NAME = allocDBM(size) @@ -114,30 +115,60 @@ cdd cdd_delay(const cdd& state) return res; } +cdd cdd_from_fed(dbm::fed_t& fed) +{ + uint32_t size = cdd_clocknum; + cdd res= cdd_false(); + while (fed.size()>0) + { + dbm::dbm_t current = fed.const_dbmt(); + res |= cdd(current.dbm(),size); + fed.removeThisDBM(current); + } + return res; +} + cdd cdd_predt(const cdd& target, const cdd& safe) { cdd allThatKillsUs = cdd_false(); uint32_t size = cdd_clocknum; cdd copy = target; - ADBM(dbm); + ADBM(dbm_target); + // split target into DBMs while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) { extraction_result res = cdd_extract_bdd_and_dbm(copy); copy = cdd_reduce(cdd_remove_negative(res.CDD_part)); - dbm = res.dbm; - cdd bdd = res.BDD_part; - cdd bdd_intersect = bdd & safe; - if ( bdd_intersect != cdd_false()) + dbm_target = res.dbm; + cdd bdd_target = res.BDD_part; + cdd good_part_with_fitting_bools = bdd_target & safe; + if (good_part_with_fitting_bools != cdd_false()) { - dbm_down(dbm, size); - cdd past = cdd(dbm,size); - past &= bdd; - cdd escape = safe & past; - allThatKillsUs |= (past - escape); + + dbm::fed_t* bad_fed = new dbm::fed_t(dbm_target,cdd_clocknum); + cdd good_copy = good_part_with_fitting_bools; + ADBM(dbm_good); + cdd bdd_parts_reached = cdd_false(); + while (!cdd_isterminal(good_copy.handle()) && cdd_info(good_copy.handle())->type != TYPE_BDD) { + extraction_result res_good = cdd_extract_bdd_and_dbm(good_copy); + good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part)); + dbm_good = res_good.dbm; + cdd bdd_good = res_good.BDD_part; + dbm::fed_t* good_fed = new dbm::fed_t(dbm_good,cdd_clocknum); + dbm::fed_t pred_fed = bad_fed->predt(*good_fed); + allThatKillsUs |= (cdd_from_fed(pred_fed)& bdd_good & bdd_target); + bdd_parts_reached |= bdd_good & bdd_target; + } + // for all boolean valuations we did not reach with our safe CDD, we take the past of the current target DBM + cdd bdd_parts_not_reached = cdd_true() - bdd_parts_reached; + dbm_down(dbm_target,size); + cdd past = cdd (dbm_target, size) & bdd_parts_not_reached; + allThatKillsUs |= past; + } else { - dbm_down(dbm,size); - cdd past = cdd (dbm, size) & bdd; + dbm_down(dbm_target,size); + cdd past = cdd (dbm_target, size) & bdd_target; allThatKillsUs |= past; } } From 6ca2eede1e270ea747920e663816fee2b9b0000a Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Tue, 12 Jul 2022 15:45:00 +0200 Subject: [PATCH 03/18] Trying to fix the predt operation, second version Co-authored-by: Florian Lorber --- src/cppext.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/cppext.cpp b/src/cppext.cpp index 1d72460..6522368 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -9,6 +9,7 @@ // /////////////////////////////////////////////////////////////////////////////// +#include #include "cdd/kernel.h" #include "dbm/fed.h" @@ -130,6 +131,7 @@ cdd cdd_from_fed(dbm::fed_t& fed) cdd cdd_predt(const cdd& target, const cdd& safe) { + printf("Version: 2022-07-04:11:08\n"); cdd allThatKillsUs = cdd_false(); uint32_t size = cdd_clocknum; cdd copy = target; @@ -139,6 +141,8 @@ cdd cdd_predt(const cdd& target, const cdd& safe) extraction_result res = cdd_extract_bdd_and_dbm(copy); copy = cdd_reduce(cdd_remove_negative(res.CDD_part)); dbm_target = res.dbm; + printf("current dbm_target \n"); + dbm_print(stdout, dbm_target, size); cdd bdd_target = res.BDD_part; cdd good_part_with_fitting_bools = bdd_target & safe; if (good_part_with_fitting_bools != cdd_false()) @@ -152,9 +156,12 @@ cdd cdd_predt(const cdd& target, const cdd& safe) extraction_result res_good = cdd_extract_bdd_and_dbm(good_copy); good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part)); dbm_good = res_good.dbm; + printf("current dbm_good \n"); + dbm_print(stdout, dbm_good, size); cdd bdd_good = res_good.BDD_part; dbm::fed_t* good_fed = new dbm::fed_t(dbm_good,cdd_clocknum); dbm::fed_t pred_fed = bad_fed->predt(*good_fed); + cdd_printdot(cdd_from_fed(pred_fed),true); allThatKillsUs |= (cdd_from_fed(pred_fed)& bdd_good & bdd_target); bdd_parts_reached |= bdd_good & bdd_target; } From 452b1b08601eb8c04b9f3d4471e32e65385e6609 Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Tue, 12 Jul 2022 15:47:57 +0200 Subject: [PATCH 04/18] Trying to fix the predt operation, debug version Co-authored-by: Florian Lorber --- src/cppext.cpp | 33 +++++++++++++++++++-------------- 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/src/cppext.cpp b/src/cppext.cpp index 6522368..ff6de64 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -116,22 +116,23 @@ cdd cdd_delay(const cdd& state) return res; } -cdd cdd_from_fed(dbm::fed_t& fed) +cdd cdd_from_fed(const dbm::fed_t& fed) { + dbm::fed_t copy = dbm::fed_t(fed); uint32_t size = cdd_clocknum; cdd res= cdd_false(); - while (fed.size()>0) + while (copy.size()>0) { - dbm::dbm_t current = fed.const_dbmt(); + dbm::dbm_t current = copy.const_dbmt(); res |= cdd(current.dbm(),size); - fed.removeThisDBM(current); + copy.removeThisDBM(current); } return res; } cdd cdd_predt(const cdd& target, const cdd& safe) { - printf("Version: 2022-07-04:11:08\n"); + printf("Version: 2022-07-04 12:01\n"); cdd allThatKillsUs = cdd_false(); uint32_t size = cdd_clocknum; cdd copy = target; @@ -152,6 +153,8 @@ cdd cdd_predt(const cdd& target, const cdd& safe) cdd good_copy = good_part_with_fitting_bools; ADBM(dbm_good); cdd bdd_parts_reached = cdd_false(); + + dbm::fed_t* good_fed = new dbm::fed_t(cdd_clocknum); while (!cdd_isterminal(good_copy.handle()) && cdd_info(good_copy.handle())->type != TYPE_BDD) { extraction_result res_good = cdd_extract_bdd_and_dbm(good_copy); good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part)); @@ -159,21 +162,23 @@ cdd cdd_predt(const cdd& target, const cdd& safe) printf("current dbm_good \n"); dbm_print(stdout, dbm_good, size); cdd bdd_good = res_good.BDD_part; - dbm::fed_t* good_fed = new dbm::fed_t(dbm_good,cdd_clocknum); - dbm::fed_t pred_fed = bad_fed->predt(*good_fed); - cdd_printdot(cdd_from_fed(pred_fed),true); - allThatKillsUs |= (cdd_from_fed(pred_fed)& bdd_good & bdd_target); - bdd_parts_reached |= bdd_good & bdd_target; + good_fed->add(dbm_good, size); } + + dbm::fed_t pred_fed = bad_fed->predt(*good_fed); + cdd_printdot(cdd_from_fed(pred_fed),true); + + cdd_printdot(bdd_target,true); + allThatKillsUs |= cdd_from_fed(pred_fed);//& bdd_target); + cdd_printdot(allThatKillsUs,true); + + bdd_parts_reached |= bdd_target; // for all boolean valuations we did not reach with our safe CDD, we take the past of the current target DBM - cdd bdd_parts_not_reached = cdd_true() - bdd_parts_reached; - dbm_down(dbm_target,size); - cdd past = cdd (dbm_target, size) & bdd_parts_not_reached; - allThatKillsUs |= past; } else { + printf("reached the else part"); dbm_down(dbm_target,size); cdd past = cdd (dbm_target, size) & bdd_target; allThatKillsUs |= past; From 133cfae6683bcff73e0cfb892d7f421b2146b6c5 Mon Sep 17 00:00:00 2001 From: florber Date: Mon, 4 Jul 2022 14:14:00 +0200 Subject: [PATCH 05/18] Trying to fix the predt operation, third version Co-authored-by: Florian Lorber --- src/cppext.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/cppext.cpp b/src/cppext.cpp index ff6de64..0da1183 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -163,6 +163,7 @@ cdd cdd_predt(const cdd& target, const cdd& safe) dbm_print(stdout, dbm_good, size); cdd bdd_good = res_good.BDD_part; good_fed->add(dbm_good, size); + bdd_parts_reached |=bdd_good&bdd_target; } dbm::fed_t pred_fed = bad_fed->predt(*good_fed); @@ -172,8 +173,11 @@ cdd cdd_predt(const cdd& target, const cdd& safe) allThatKillsUs |= cdd_from_fed(pred_fed);//& bdd_target); cdd_printdot(allThatKillsUs,true); - bdd_parts_reached |= bdd_target; // for all boolean valuations we did not reach with our safe CDD, we take the past of the current target DBM + cdd bdd_parts_not_reached = cdd_true() - bdd_parts_reached; + dbm_down(dbm_target,size); + cdd past = cdd (dbm_target, size) & bdd_parts_not_reached; + allThatKillsUs |= past; } else From 860656b92827d38b63023dd4f319da462c9fa51d Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Tue, 12 Jul 2022 15:56:39 +0200 Subject: [PATCH 06/18] Fix the predt operation, simple enumeration approach Co-authored-by: Florian Lorber --- src/cppext.cpp | 93 ++++++++++++++++++++++++++++++++++---------------- 1 file changed, 64 insertions(+), 29 deletions(-) diff --git a/src/cppext.cpp b/src/cppext.cpp index 0da1183..d6c3b1b 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -9,6 +9,7 @@ // /////////////////////////////////////////////////////////////////////////////// +#include #include #include "cdd/kernel.h" #include "dbm/fed.h" @@ -148,41 +149,75 @@ cdd cdd_predt(const cdd& target, const cdd& safe) cdd good_part_with_fitting_bools = bdd_target & safe; if (good_part_with_fitting_bools != cdd_false()) { + printf("before the big for \n"); + for (int i=0; i< pow(2,cdd_varnum); i++) + { + cdd all_booleans = cdd_true(); + printf("in the big for \n"); + for (int j=0; j< cdd_varnum; j++) { + bool current = (i & 1 << j) != 0; + if (current) { + all_booleans &= cdd_bddvarpp(bdd_start_level+j); + printf("1"); + } + else { + all_booleans &= cdd_bddnvarpp(bdd_start_level+j); + printf("0"); + } + } + printf("\n"); + + // for each possible combination of boolean variables, + // compute the part of safe that overlaps with it. + + // no need to test combinations that dont satisfy the bad part + if (!cdd_equiv((all_booleans & bdd_target), cdd_false()) ) + { + dbm::fed_t* bad_fed = new dbm::fed_t(dbm_target,cdd_clocknum); + ADBM(dbm_good); + assert(!cdd_eval_false((all_booleans & bdd_target))); + cdd good_copy = good_part_with_fitting_bools & all_booleans; + + if (!cdd_eval_false(good_copy)) { + printf("found a combination satisfying both CDDs\n"); + dbm::fed_t* good_fed = new dbm::fed_t(cdd_clocknum); + while (!cdd_isterminal(good_copy.handle()) && cdd_info(good_copy.handle())->type != TYPE_BDD) { + extraction_result res_good = cdd_extract_bdd_and_dbm(good_copy); + good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part)); + dbm_good = res_good.dbm; + cdd bdd_good = res_good.BDD_part; + good_fed->add(dbm_good, size); + printf("extracting a BDM from good\n"); + } + + dbm::fed_t pred_fed = bad_fed->predt(*good_fed); + printf("bad fed\n"); + cdd_printdot(cdd_from_fed(*bad_fed), true); + printf("good fed\n"); + cdd_printdot(cdd_from_fed(*good_fed), true); + printf("predt fed\n"); + cdd_printdot(cdd_from_fed(pred_fed), true); + allThatKillsUs |= cdd_from_fed(pred_fed) & all_booleans; + } + else + { + printf("reached the inner else\n"); + // for all boolean valuations we did not reach with our safe CDD, we take the past of the current target DBM + ADBM(local); + dbm_copy(local,dbm_target,size); + dbm_down(local,size); + cdd past = cdd (local, size) & all_booleans; + allThatKillsUs |= past; + } + } - dbm::fed_t* bad_fed = new dbm::fed_t(dbm_target,cdd_clocknum); - cdd good_copy = good_part_with_fitting_bools; - ADBM(dbm_good); - cdd bdd_parts_reached = cdd_false(); - - dbm::fed_t* good_fed = new dbm::fed_t(cdd_clocknum); - while (!cdd_isterminal(good_copy.handle()) && cdd_info(good_copy.handle())->type != TYPE_BDD) { - extraction_result res_good = cdd_extract_bdd_and_dbm(good_copy); - good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part)); - dbm_good = res_good.dbm; - printf("current dbm_good \n"); - dbm_print(stdout, dbm_good, size); - cdd bdd_good = res_good.BDD_part; - good_fed->add(dbm_good, size); - bdd_parts_reached |=bdd_good&bdd_target; - } - - dbm::fed_t pred_fed = bad_fed->predt(*good_fed); - cdd_printdot(cdd_from_fed(pred_fed),true); - - cdd_printdot(bdd_target,true); - allThatKillsUs |= cdd_from_fed(pred_fed);//& bdd_target); - cdd_printdot(allThatKillsUs,true); - // for all boolean valuations we did not reach with our safe CDD, we take the past of the current target DBM - cdd bdd_parts_not_reached = cdd_true() - bdd_parts_reached; - dbm_down(dbm_target,size); - cdd past = cdd (dbm_target, size) & bdd_parts_not_reached; - allThatKillsUs |= past; + } } else { - printf("reached the else part"); + printf("reached the else part\n"); dbm_down(dbm_target,size); cdd past = cdd (dbm_target, size) & bdd_target; allThatKillsUs |= past; From 12fd7ee886534aaefbbcb7a90c943e60962bca77 Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Wed, 13 Jul 2022 14:34:57 +0200 Subject: [PATCH 07/18] Add documentation to the function --- src/cppext.cpp | 158 +++++++++++++++++++++++-------------------------- 1 file changed, 74 insertions(+), 84 deletions(-) diff --git a/src/cppext.cpp b/src/cppext.cpp index d6c3b1b..cef4f76 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -9,10 +9,12 @@ // /////////////////////////////////////////////////////////////////////////////// +#include "dbm/fed.h" +#include "cdd/kernel.h" + #include + #include -#include "cdd/kernel.h" -#include "dbm/fed.h" #define ADBM(NAME) raw_t* NAME = allocDBM(size) @@ -96,15 +98,15 @@ extraction_result cdd_extract_bdd_and_dbm(const cdd& state) */ cdd cdd_delay(const cdd& state) { - if (cdd_isterminal(state.root)) + if (cdd_isterminal(state.handle())) return state; - if (cdd_info(state.root)->type == TYPE_BDD) + if (cdd_info(state.handle())->type == TYPE_BDD) return state; uint32_t size = cdd_clocknum; cdd copy = state; cdd res = cdd_false(); ADBM(dbm); - while (!cdd_isterminal(copy.root) && cdd_info(copy.root)->type != TYPE_BDD) { + while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) { copy = cdd_reduce(copy); cdd bottom = cdd_extract_bdd(copy, size); copy = cdd_extract_dbm(copy, dbm, size); @@ -121,105 +123,93 @@ cdd cdd_from_fed(const dbm::fed_t& fed) { dbm::fed_t copy = dbm::fed_t(fed); uint32_t size = cdd_clocknum; - cdd res= cdd_false(); - while (copy.size()>0) - { + cdd res = cdd_false(); + while (copy.size() > 0) { dbm::dbm_t current = copy.const_dbmt(); - res |= cdd(current.dbm(),size); + res |= cdd(current.dbm(), size); copy.removeThisDBM(current); } return res; } -cdd cdd_predt(const cdd& target, const cdd& safe) +/** + * Get the timed predecessor of the given (bad) \a target state that cannot be + * saved (i.e. reached) by delaying into \a safe. + * @param target the target cdd + * @param safe the safe cdd + * @return a cdd containing states that can delay into \a target without reaching \a safe. + */ +cdd cdd_predt(const cdd& target, const cdd& safe) { - printf("Version: 2022-07-04 12:01\n"); cdd allThatKillsUs = cdd_false(); uint32_t size = cdd_clocknum; cdd copy = target; ADBM(dbm_target); - // split target into DBMs + + // Split target into DBMs. while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) { extraction_result res = cdd_extract_bdd_and_dbm(copy); copy = cdd_reduce(cdd_remove_negative(res.CDD_part)); dbm_target = res.dbm; - printf("current dbm_target \n"); - dbm_print(stdout, dbm_target, size); cdd bdd_target = res.BDD_part; + + // Check whether the safe has an overlapping BDD part with the target. cdd good_part_with_fitting_bools = bdd_target & safe; - if (good_part_with_fitting_bools != cdd_false()) - { - printf("before the big for \n"); - for (int i=0; i< pow(2,cdd_varnum); i++) - { + if (good_part_with_fitting_bools != cdd_false()) { + // For each possible combination of boolean valuations, + // compute the part of safe that overlaps with it. + for (int i = 0; i < pow(2, cdd_varnum); i++) { cdd all_booleans = cdd_true(); - printf("in the big for \n"); - for (int j=0; j< cdd_varnum; j++) { + for (int j = 0; j < cdd_varnum; j++) { bool current = (i & 1 << j) != 0; if (current) { - all_booleans &= cdd_bddvarpp(bdd_start_level+j); - printf("1"); - } - else { - all_booleans &= cdd_bddnvarpp(bdd_start_level+j); - printf("0"); + all_booleans &= cdd_bddvarpp(bdd_start_level + j); + } else { + all_booleans &= cdd_bddnvarpp(bdd_start_level + j); } } - printf("\n"); - - // for each possible combination of boolean variables, - // compute the part of safe that overlaps with it. - - // no need to test combinations that dont satisfy the bad part - if (!cdd_equiv((all_booleans & bdd_target), cdd_false()) ) - { - dbm::fed_t* bad_fed = new dbm::fed_t(dbm_target,cdd_clocknum); - ADBM(dbm_good); - assert(!cdd_eval_false((all_booleans & bdd_target))); - cdd good_copy = good_part_with_fitting_bools & all_booleans; - - if (!cdd_eval_false(good_copy)) { - printf("found a combination satisfying both CDDs\n"); - dbm::fed_t* good_fed = new dbm::fed_t(cdd_clocknum); - while (!cdd_isterminal(good_copy.handle()) && cdd_info(good_copy.handle())->type != TYPE_BDD) { - extraction_result res_good = cdd_extract_bdd_and_dbm(good_copy); - good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part)); - dbm_good = res_good.dbm; - cdd bdd_good = res_good.BDD_part; - good_fed->add(dbm_good, size); - printf("extracting a BDM from good\n"); - } - - dbm::fed_t pred_fed = bad_fed->predt(*good_fed); - printf("bad fed\n"); - cdd_printdot(cdd_from_fed(*bad_fed), true); - printf("good fed\n"); - cdd_printdot(cdd_from_fed(*good_fed), true); - printf("predt fed\n"); - cdd_printdot(cdd_from_fed(pred_fed), true); - allThatKillsUs |= cdd_from_fed(pred_fed) & all_booleans; - } - else - { - printf("reached the inner else\n"); - // for all boolean valuations we did not reach with our safe CDD, we take the past of the current target DBM - ADBM(local); - dbm_copy(local,dbm_target,size); - dbm_down(local,size); - cdd past = cdd (local, size) & all_booleans; - allThatKillsUs |= past; - } + + // No need to test combinations that don't satisfy the bad part. + if (!cdd_equiv(all_booleans & bdd_target, cdd_false())) { + continue; } + // Paranoia check. + assert(!cdd_eval_false(all_booleans & bdd_target)); + + dbm::fed_t* bad_fed = new dbm::fed_t(dbm_target, cdd_clocknum); + ADBM(dbm_good); + cdd good_copy = good_part_with_fitting_bools & all_booleans; + + if (!cdd_eval_false(good_copy)) { + dbm::fed_t* good_fed = new dbm::fed_t(cdd_clocknum); + while (!cdd_isterminal(good_copy.handle()) && cdd_info(good_copy.handle())->type != TYPE_BDD) { + extraction_result res_good = cdd_extract_bdd_and_dbm(good_copy); + good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part)); + dbm_good = res_good.dbm; + cdd bdd_good = res_good.BDD_part; + good_fed->add(dbm_good, size); + } + dbm::fed_t pred_fed = bad_fed->predt(*good_fed); + allThatKillsUs |= cdd_from_fed(pred_fed) & all_booleans; + + } else { + // For all boolean valuations we did not reach with our safe CDD, we take the past of the + // current target DBM. + ADBM(local); + dbm_copy(local, dbm_target, size); + dbm_down(local, size); + cdd past = cdd(local, size) & all_booleans; + allThatKillsUs |= past; + } } - } - else - { - printf("reached the else part\n"); - dbm_down(dbm_target,size); - cdd past = cdd (dbm_target, size) & bdd_target; + } else { + // Safe does not have an overlapping part with the target BDD. + // So the complete past of this DBM is bad. + dbm_down(dbm_target, size); + cdd past = cdd(dbm_target, size) & bdd_target; allThatKillsUs |= past; } } @@ -254,9 +244,9 @@ cdd cdd_delay_invariant(const cdd& state, const cdd& invar) */ cdd cdd_past(const cdd& state) { - if (cdd_isterminal(state.root)) + if (cdd_isterminal(state.handle())) return state; - if (cdd_info(state.root)->type == TYPE_BDD) + if (cdd_info(state.handle())->type == TYPE_BDD) return state; uint32_t size = cdd_clocknum; cdd copy = state; @@ -308,14 +298,14 @@ cdd cdd_apply_reset(const cdd& state, int32_t* clock_resets, int32_t* clock_valu // Special cases when we are already done. if (num_clock_resets == 0) return copy; - if (cdd_isterminal(copy.root)) + if (cdd_isterminal(copy.handle())) return copy; - if (cdd_info(copy.root)->type == TYPE_BDD) + if (cdd_info(copy.handle())->type == TYPE_BDD) return copy; // Apply the clock resets. cdd res = cdd_false(); - while (!cdd_isterminal(copy.root) && cdd_info(copy.root)->type != TYPE_BDD) { + while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) { copy = cdd_reduce(copy); extraction_result exres = cdd_extract_bdd_and_dbm(copy); cdd bottom = exres.BDD_part; @@ -388,13 +378,13 @@ cdd cdd_transition_back(const cdd& state, const cdd& guard, const cdd& update, i // Special cases when we are already done. if (num_clock_resets == 0) return copy & guard; - if (!cdd_isterminal(copy.root) && cdd_info(copy.root)->type == TYPE_BDD) + if (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type == TYPE_BDD) return copy & guard; // Apply the clock resets. cdd res = cdd_false(); copy = cdd_remove_negative(copy); - while (!cdd_isterminal(copy.root) && cdd_info(copy.root)->type != TYPE_BDD) { + while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) { copy = cdd_reduce(copy); extraction_result exres = cdd_extract_bdd_and_dbm(copy); cdd bottom = exres.BDD_part; From cd14ea3efc6e03b7711cf8be39d761e56aacf7a2 Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Wed, 13 Jul 2022 14:50:24 +0200 Subject: [PATCH 08/18] Fix predt for terminals and pure BDDs --- src/cppext.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/cppext.cpp b/src/cppext.cpp index cef4f76..83573d6 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -98,10 +98,12 @@ extraction_result cdd_extract_bdd_and_dbm(const cdd& state) */ cdd cdd_delay(const cdd& state) { + // First some trivial cases. if (cdd_isterminal(state.handle())) return state; if (cdd_info(state.handle())->type == TYPE_BDD) return state; + uint32_t size = cdd_clocknum; cdd copy = state; cdd res = cdd_false(); @@ -141,6 +143,12 @@ cdd cdd_from_fed(const dbm::fed_t& fed) */ cdd cdd_predt(const cdd& target, const cdd& safe) { + // First some trivial cases. + if (cdd_isterminal(target.handle())) + return target; + if (cdd_info(target.handle())->type == TYPE_BDD) + return target; + cdd allThatKillsUs = cdd_false(); uint32_t size = cdd_clocknum; cdd copy = target; @@ -244,10 +252,12 @@ cdd cdd_delay_invariant(const cdd& state, const cdd& invar) */ cdd cdd_past(const cdd& state) { + // First some trivial cases. if (cdd_isterminal(state.handle())) return state; if (cdd_info(state.handle())->type == TYPE_BDD) return state; + uint32_t size = cdd_clocknum; cdd copy = state; cdd res = cdd_false(); From d7b5dbf03b9a3a50df9ae52835de012f76b0dc8f Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Wed, 13 Jul 2022 16:36:10 +0200 Subject: [PATCH 09/18] Fix cdd_from_fed to use an iterator --- src/cppext.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/cppext.cpp b/src/cppext.cpp index 83573d6..0c3ff95 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -121,15 +121,18 @@ cdd cdd_delay(const cdd& state) return res; } +/** + * Construct a cdd from a federation. + * @param fed a federation + * @return the cdd representing \a fed. + */ cdd cdd_from_fed(const dbm::fed_t& fed) { dbm::fed_t copy = dbm::fed_t(fed); uint32_t size = cdd_clocknum; cdd res = cdd_false(); - while (copy.size() > 0) { - dbm::dbm_t current = copy.const_dbmt(); - res |= cdd(current.dbm(), size); - copy.removeThisDBM(current); + for (dbm::fed_t::const_iterator iter(fed); !iter.null(); ++iter) { + res |= cdd(iter(), size); } return res; } From cce2b703d50fdb1ee49b95b4e36d3c266090a046 Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Thu, 14 Jul 2022 09:19:47 +0200 Subject: [PATCH 10/18] Fix cdd_predt when it is supplied with a pure bdd --- src/cppext.cpp | 160 ++++++++++++++++++++++++++++++------------------- 1 file changed, 98 insertions(+), 62 deletions(-) diff --git a/src/cppext.cpp b/src/cppext.cpp index 0c3ff95..c8e59d7 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -137,9 +137,98 @@ cdd cdd_from_fed(const dbm::fed_t& fed) return res; } +/** + * Get the timed predecessor of the given (bad) target dbm and target bdd that cannot be + * saved (i.e. reached) by delaying into \a safe. + * + *

If there is an overlap between \a target and \a safe, the overlap is considered + * to be saved.

+ * @param dbm_target the target dbm + * @param bdd_target the target bdd + * @param safe the safe cdd + * @return a cdd containing states that can delay into \a target without reaching \a safe. + */ +cdd cdd_predt_dbm(raw_t* dbm_target, cdd bdd_target, const cdd& safe) +{ + uint32_t size = cdd_clocknum; + cdd result = cdd_false(); + + // Check whether the safe has an overlapping BDD part with the target. + cdd good_part_with_fitting_bools = bdd_target & safe; + if (good_part_with_fitting_bools != cdd_false()) { + // For each possible combination of boolean valuations, + // compute the part of safe that overlaps with it. + for (int i = 0; i < pow(2, cdd_varnum); i++) { + cdd all_booleans = cdd_true(); + for (int j = 0; j < cdd_varnum; j++) { + bool current = (i & 1 << j) != 0; + if (current) { + all_booleans &= cdd_bddvarpp(bdd_start_level + j); + } else { + all_booleans &= cdd_bddnvarpp(bdd_start_level + j); + } + } + + // No need to test combinations that don't satisfy the bad part. + if (cdd_equiv(all_booleans & bdd_target, cdd_false())) { + continue; + } + + // Paranoia check. + assert(!cdd_eval_false(all_booleans & bdd_target)); + + dbm::fed_t* bad_fed = new dbm::fed_t(dbm_target, cdd_clocknum); + ADBM(dbm_good); + cdd good_copy = good_part_with_fitting_bools & all_booleans; + + if (!cdd_eval_false(good_copy)) { + dbm::fed_t* good_fed = new dbm::fed_t(cdd_clocknum); + while (!cdd_isterminal(good_copy.handle()) && cdd_info(good_copy.handle())->type != TYPE_BDD) { + extraction_result res_good = cdd_extract_bdd_and_dbm(good_copy); + good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part)); + dbm_good = res_good.dbm; + cdd bdd_good = res_good.BDD_part; + good_fed->add(dbm_good, size); + } + + // If good_fed is empty, good_copy did not contain any DBM. This has the interpretation + // of an unbounded DBM. + if (good_fed->isEmpty()) { + dbm_init(dbm_good, size); + good_fed = new dbm::fed_t(dbm_good, cdd_clocknum); + } + + dbm::fed_t pred_fed = bad_fed->predt(*good_fed); + result |= cdd_from_fed(pred_fed) & all_booleans; + + } else { + // For all boolean valuations we did not reach with our safe CDD, we take the past of the + // current target DBM. + ADBM(local); + dbm_copy(local, dbm_target, size); + dbm_down(local, size); + cdd past = cdd(local, size) & all_booleans; + result |= past; + } + } + + } else { + // Safe does not have an overlapping part with the target BDD. + // So the complete past of this DBM is bad. + dbm_down(dbm_target, size); + cdd past = cdd(dbm_target, size) & bdd_target; + result |= past; + } + + return result; +} + /** * Get the timed predecessor of the given (bad) \a target state that cannot be * saved (i.e. reached) by delaying into \a safe. + * + *

If there is an overlap between \a target and \a safe, the overlap is considered + * to be saved.

* @param target the target cdd * @param safe the safe cdd * @return a cdd containing states that can delay into \a target without reaching \a safe. @@ -147,16 +236,21 @@ cdd cdd_from_fed(const dbm::fed_t& fed) cdd cdd_predt(const cdd& target, const cdd& safe) { // First some trivial cases. - if (cdd_isterminal(target.handle())) - return target; - if (cdd_info(target.handle())->type == TYPE_BDD) + if (target == cdd_false()) return target; + if (safe == cdd_true()) + return cdd_false(); cdd allThatKillsUs = cdd_false(); uint32_t size = cdd_clocknum; cdd copy = target; ADBM(dbm_target); + if (cdd_isterminal(target.handle()) || cdd_info(target.handle())->type == TYPE_BDD) { + dbm_init(dbm_target, size); + return cdd_predt_dbm(dbm_target, target, safe); + } + // Split target into DBMs. while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) { extraction_result res = cdd_extract_bdd_and_dbm(copy); @@ -164,65 +258,7 @@ cdd cdd_predt(const cdd& target, const cdd& safe) dbm_target = res.dbm; cdd bdd_target = res.BDD_part; - // Check whether the safe has an overlapping BDD part with the target. - cdd good_part_with_fitting_bools = bdd_target & safe; - if (good_part_with_fitting_bools != cdd_false()) { - // For each possible combination of boolean valuations, - // compute the part of safe that overlaps with it. - for (int i = 0; i < pow(2, cdd_varnum); i++) { - cdd all_booleans = cdd_true(); - for (int j = 0; j < cdd_varnum; j++) { - bool current = (i & 1 << j) != 0; - if (current) { - all_booleans &= cdd_bddvarpp(bdd_start_level + j); - } else { - all_booleans &= cdd_bddnvarpp(bdd_start_level + j); - } - } - - // No need to test combinations that don't satisfy the bad part. - if (!cdd_equiv(all_booleans & bdd_target, cdd_false())) { - continue; - } - - // Paranoia check. - assert(!cdd_eval_false(all_booleans & bdd_target)); - - dbm::fed_t* bad_fed = new dbm::fed_t(dbm_target, cdd_clocknum); - ADBM(dbm_good); - cdd good_copy = good_part_with_fitting_bools & all_booleans; - - if (!cdd_eval_false(good_copy)) { - dbm::fed_t* good_fed = new dbm::fed_t(cdd_clocknum); - while (!cdd_isterminal(good_copy.handle()) && cdd_info(good_copy.handle())->type != TYPE_BDD) { - extraction_result res_good = cdd_extract_bdd_and_dbm(good_copy); - good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part)); - dbm_good = res_good.dbm; - cdd bdd_good = res_good.BDD_part; - good_fed->add(dbm_good, size); - } - - dbm::fed_t pred_fed = bad_fed->predt(*good_fed); - allThatKillsUs |= cdd_from_fed(pred_fed) & all_booleans; - - } else { - // For all boolean valuations we did not reach with our safe CDD, we take the past of the - // current target DBM. - ADBM(local); - dbm_copy(local, dbm_target, size); - dbm_down(local, size); - cdd past = cdd(local, size) & all_booleans; - allThatKillsUs |= past; - } - } - - } else { - // Safe does not have an overlapping part with the target BDD. - // So the complete past of this DBM is bad. - dbm_down(dbm_target, size); - cdd past = cdd(dbm_target, size) & bdd_target; - allThatKillsUs |= past; - } + allThatKillsUs |= cdd_predt_dbm(dbm_target, bdd_target, safe); } return allThatKillsUs; } From 8859ac9cb02d2c4b2209975053ae07dcaaa60eb7 Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Thu, 14 Jul 2022 09:19:58 +0200 Subject: [PATCH 11/18] Add test case for cdd_predt --- test/test_cdd.cpp | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/test/test_cdd.cpp b/test/test_cdd.cpp index 13e744d..8ed3b77 100644 --- a/test/test_cdd.cpp +++ b/test/test_cdd.cpp @@ -772,6 +772,41 @@ void test_transition_back_past(size_t size) num_bools)) == cdd_false()); } +void test_predt(size_t size) +{ + // First some trivial cases. + REQUIRE(cdd_equiv(cdd_predt(cdd_true(), cdd_true()), cdd_false())); + REQUIRE(cdd_equiv(cdd_predt(cdd_true(), cdd_false()), cdd_remove_negative(cdd_true()))); + REQUIRE(cdd_equiv(cdd_predt(cdd_false(), cdd_true()), cdd_false())); + REQUIRE(cdd_equiv(cdd_predt(cdd_false(), cdd_false()), cdd_false())); + + // Create a CDD containing random DBMs. + cdd cdd_part; + auto dbm = dbm_wrap{size}; + int n_dbms = 8; + + for (uint32_t i = 0; i < n_dbms; i++) { + dbm.generate(); + cdd_part |= cdd(dbm.raw(), dbm.size()); + } + + // Create a random BDD. + cdd bdd_part = generate_bdd(size); + cdd cdd1 = cdd_part & bdd_part; + + // First some checks when nothing can save us. + // cdd_part \subset cdd_predt(cdd_part) <==> cdd_part & !cdd_predt(cdd_part) == false + REQUIRE((!cdd_predt(cdd_part, cdd_false()) & cdd_remove_negative(cdd_part)) == cdd_false()); + // cdd_predt(cdd_part) \subset cdd_past(cdd_part) <==> cdd_predt(cdd_part) & !cdd_past(cdd_part) == false + REQUIRE((!cdd_past(cdd_part) & cdd_predt(cdd_part, cdd_false())) == cdd_false()); + REQUIRE(cdd_equiv(cdd_predt(bdd_part, cdd_false()), cdd_remove_negative(bdd_part))); + // cdd_predt(cdd1) \subset cdd_past(cdd1) <==> cdd_predt(cdd1) & !cdd_past(cdd1) == false + REQUIRE((!cdd_past(cdd1) & cdd_predt(cdd1, cdd_false())) == cdd_false()); + REQUIRE(cdd_equiv(cdd_predt(cdd1, cdd_true()), cdd_false())); + + // TODO: how to check cdd_predt when the safe cdd is a random cdd as well? +} + static void test(const char* name, TestFunction f, size_t size) { cout << name << " size = " << size << endl; @@ -809,6 +844,7 @@ static void big_test(uint32_t n) test("test_transition ", test_transition, i); test("test_transition_back", test_transition_back, i); test("test_transition_back_past", test_transition_back_past, i); + test("test_predt ", test_predt, i); } test("test_remove_negative", test_remove_negative, n); passDBMs = dbm_wrap::get_allDBMs() - DBM_sofar; From 2fbd4177150820a7985973207982637f3259c3ed Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Fri, 15 Jul 2022 09:39:04 +0200 Subject: [PATCH 12/18] Fix a double space --- include/cdd/cdd.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/cdd/cdd.h b/include/cdd/cdd.h index e9d0304..215e222 100644 --- a/include/cdd/cdd.h +++ b/include/cdd/cdd.h @@ -881,7 +881,7 @@ class cdd int32_t num_clock_resets, int32_t* bool_resets, int32_t num_bool_resets); friend cdd cdd_transition_back_past(const cdd& state, const cdd& guard, const cdd& update, int32_t* clock_resets, int32_t num_clock_resets, int32_t* bool_resets, int32_t num_bool_resets); - friend cdd cdd_predt(const cdd& target, const cdd& safe); + friend cdd cdd_predt(const cdd& target, const cdd& safe); friend cdd cdd_reduce2(const cdd&); friend bool cdd_contains(const cdd&, raw_t* dbm, int32_t dim); friend cdd cdd_extract_dbm(const cdd&, raw_t* dbm, int32_t dim); From a1832c5636edd38dc5ed696aff7a9b06e4754b2a Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Tue, 26 Jul 2022 12:47:01 +0200 Subject: [PATCH 13/18] Fix easy comments from review --- src/cppext.cpp | 25 +++++++++++-------------- 1 file changed, 11 insertions(+), 14 deletions(-) diff --git a/src/cppext.cpp b/src/cppext.cpp index c8e59d7..868c2ab 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -10,12 +10,9 @@ /////////////////////////////////////////////////////////////////////////////// #include "dbm/fed.h" +#include "dbm/print.h" #include "cdd/kernel.h" -#include - -#include - #define ADBM(NAME) raw_t* NAME = allocDBM(size) /* Allocate a DBM. */ @@ -131,8 +128,8 @@ cdd cdd_from_fed(const dbm::fed_t& fed) dbm::fed_t copy = dbm::fed_t(fed); uint32_t size = cdd_clocknum; cdd res = cdd_false(); - for (dbm::fed_t::const_iterator iter(fed); !iter.null(); ++iter) { - res |= cdd(iter(), size); + for (auto& zone : fed) { + res |= cdd(zone.const_dbm(), size); } return res; } @@ -158,9 +155,9 @@ cdd cdd_predt_dbm(raw_t* dbm_target, cdd bdd_target, const cdd& safe) if (good_part_with_fitting_bools != cdd_false()) { // For each possible combination of boolean valuations, // compute the part of safe that overlaps with it. - for (int i = 0; i < pow(2, cdd_varnum); i++) { + for (auto i = 0u; i < (1u << cdd_varnum); ++i) { cdd all_booleans = cdd_true(); - for (int j = 0; j < cdd_varnum; j++) { + for (auto j = 0u; j < cdd_varnum; ++j) { bool current = (i & 1 << j) != 0; if (current) { all_booleans &= cdd_bddvarpp(bdd_start_level + j); @@ -177,28 +174,28 @@ cdd cdd_predt_dbm(raw_t* dbm_target, cdd bdd_target, const cdd& safe) // Paranoia check. assert(!cdd_eval_false(all_booleans & bdd_target)); - dbm::fed_t* bad_fed = new dbm::fed_t(dbm_target, cdd_clocknum); + dbm::fed_t bad_fed(dbm_target, cdd_clocknum); ADBM(dbm_good); cdd good_copy = good_part_with_fitting_bools & all_booleans; if (!cdd_eval_false(good_copy)) { - dbm::fed_t* good_fed = new dbm::fed_t(cdd_clocknum); + dbm::fed_t good_fed(cdd_clocknum); while (!cdd_isterminal(good_copy.handle()) && cdd_info(good_copy.handle())->type != TYPE_BDD) { extraction_result res_good = cdd_extract_bdd_and_dbm(good_copy); good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part)); dbm_good = res_good.dbm; cdd bdd_good = res_good.BDD_part; - good_fed->add(dbm_good, size); + good_fed.add(dbm_good, size); } // If good_fed is empty, good_copy did not contain any DBM. This has the interpretation // of an unbounded DBM. - if (good_fed->isEmpty()) { + if (good_fed.isEmpty()) { dbm_init(dbm_good, size); - good_fed = new dbm::fed_t(dbm_good, cdd_clocknum); + good_fed.add(dbm_good, size); } - dbm::fed_t pred_fed = bad_fed->predt(*good_fed); + dbm::fed_t pred_fed = bad_fed.predt(good_fed); result |= cdd_from_fed(pred_fed) & all_booleans; } else { From 80b5cc5329da23bccb8bf82cb547132e6ee57662 Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Tue, 26 Jul 2022 12:50:06 +0200 Subject: [PATCH 14/18] Replace size by cdd_clocknum in ADBM Therefore, all size copy variables can be safely removed. --- src/cppext.cpp | 48 +++++++++++++++++++++--------------------------- 1 file changed, 21 insertions(+), 27 deletions(-) diff --git a/src/cppext.cpp b/src/cppext.cpp index 868c2ab..144c3f8 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -13,7 +13,7 @@ #include "dbm/print.h" #include "cdd/kernel.h" -#define ADBM(NAME) raw_t* NAME = allocDBM(size) +#define ADBM(NAME) raw_t* NAME = allocDBM(cdd_clocknum) /* Allocate a DBM. */ static raw_t* allocDBM(uint32_t dim) { return (raw_t*)malloc(dim * dim * sizeof(raw_t)); } @@ -71,10 +71,9 @@ cdd cdd::operator=(ddNode* node) */ extraction_result cdd_extract_bdd_and_dbm(const cdd& state) { - uint32_t size = cdd_clocknum; ADBM(dbm); - cdd bdd_part = cdd_extract_bdd(state, size); - cdd cdd_part = cdd_extract_dbm(state, dbm, size); + cdd bdd_part = cdd_extract_bdd(state, cdd_clocknum); + cdd cdd_part = cdd_extract_dbm(state, dbm, cdd_clocknum); extraction_result res; res.BDD_part = bdd_part; res.CDD_part = cdd_part; @@ -101,17 +100,16 @@ cdd cdd_delay(const cdd& state) if (cdd_info(state.handle())->type == TYPE_BDD) return state; - uint32_t size = cdd_clocknum; cdd copy = state; cdd res = cdd_false(); ADBM(dbm); while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) { copy = cdd_reduce(copy); - cdd bottom = cdd_extract_bdd(copy, size); - copy = cdd_extract_dbm(copy, dbm, size); + cdd bottom = cdd_extract_bdd(copy, cdd_clocknum); + copy = cdd_extract_dbm(copy, dbm, cdd_clocknum); copy = cdd_reduce(cdd_remove_negative(copy)); - dbm_up(dbm, size); - cdd fixed_cdd = cdd(dbm, size); + dbm_up(dbm, cdd_clocknum); + cdd fixed_cdd = cdd(dbm, cdd_clocknum); fixed_cdd &= bottom; res |= fixed_cdd; } @@ -126,10 +124,9 @@ cdd cdd_delay(const cdd& state) cdd cdd_from_fed(const dbm::fed_t& fed) { dbm::fed_t copy = dbm::fed_t(fed); - uint32_t size = cdd_clocknum; cdd res = cdd_false(); for (auto& zone : fed) { - res |= cdd(zone.const_dbm(), size); + res |= cdd(zone.const_dbm(), cdd_clocknum); } return res; } @@ -147,7 +144,6 @@ cdd cdd_from_fed(const dbm::fed_t& fed) */ cdd cdd_predt_dbm(raw_t* dbm_target, cdd bdd_target, const cdd& safe) { - uint32_t size = cdd_clocknum; cdd result = cdd_false(); // Check whether the safe has an overlapping BDD part with the target. @@ -185,14 +181,14 @@ cdd cdd_predt_dbm(raw_t* dbm_target, cdd bdd_target, const cdd& safe) good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part)); dbm_good = res_good.dbm; cdd bdd_good = res_good.BDD_part; - good_fed.add(dbm_good, size); + good_fed.add(dbm_good, cdd_clocknum); } // If good_fed is empty, good_copy did not contain any DBM. This has the interpretation // of an unbounded DBM. if (good_fed.isEmpty()) { - dbm_init(dbm_good, size); - good_fed.add(dbm_good, size); + dbm_init(dbm_good, cdd_clocknum); + good_fed.add(dbm_good, cdd_clocknum); } dbm::fed_t pred_fed = bad_fed.predt(good_fed); @@ -202,9 +198,9 @@ cdd cdd_predt_dbm(raw_t* dbm_target, cdd bdd_target, const cdd& safe) // For all boolean valuations we did not reach with our safe CDD, we take the past of the // current target DBM. ADBM(local); - dbm_copy(local, dbm_target, size); - dbm_down(local, size); - cdd past = cdd(local, size) & all_booleans; + dbm_copy(local, dbm_target, cdd_clocknum); + dbm_down(local, cdd_clocknum); + cdd past = cdd(local, cdd_clocknum) & all_booleans; result |= past; } } @@ -212,8 +208,8 @@ cdd cdd_predt_dbm(raw_t* dbm_target, cdd bdd_target, const cdd& safe) } else { // Safe does not have an overlapping part with the target BDD. // So the complete past of this DBM is bad. - dbm_down(dbm_target, size); - cdd past = cdd(dbm_target, size) & bdd_target; + dbm_down(dbm_target, cdd_clocknum); + cdd past = cdd(dbm_target, cdd_clocknum) & bdd_target; result |= past; } @@ -239,12 +235,11 @@ cdd cdd_predt(const cdd& target, const cdd& safe) return cdd_false(); cdd allThatKillsUs = cdd_false(); - uint32_t size = cdd_clocknum; cdd copy = target; ADBM(dbm_target); if (cdd_isterminal(target.handle()) || cdd_info(target.handle())->type == TYPE_BDD) { - dbm_init(dbm_target, size); + dbm_init(dbm_target, cdd_clocknum); return cdd_predt_dbm(dbm_target, target, safe); } @@ -294,17 +289,16 @@ cdd cdd_past(const cdd& state) if (cdd_info(state.handle())->type == TYPE_BDD) return state; - uint32_t size = cdd_clocknum; cdd copy = state; cdd res = cdd_false(); ADBM(dbm); while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) { copy = cdd_reduce(copy); - cdd bottom = cdd_extract_bdd(copy, size); - copy = cdd_extract_dbm(copy, dbm, size); + cdd bottom = cdd_extract_bdd(copy, cdd_clocknum); + copy = cdd_extract_dbm(copy, dbm, cdd_clocknum); copy = cdd_reduce(cdd_remove_negative(copy)); - dbm_down(dbm, size); - res |= (cdd(dbm, size) & bottom); + dbm_down(dbm, cdd_clocknum); + res |= (cdd(dbm, cdd_clocknum) & bottom); } return res; } From 1471741d0d4e3e2445dbd5746f6b2d961398959b Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Tue, 26 Jul 2022 12:55:16 +0200 Subject: [PATCH 15/18] Change include order --- src/cppext.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/cppext.cpp b/src/cppext.cpp index 144c3f8..a08fbe1 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -9,10 +9,11 @@ // /////////////////////////////////////////////////////////////////////////////// -#include "dbm/fed.h" -#include "dbm/print.h" #include "cdd/kernel.h" +#include +#include + #define ADBM(NAME) raw_t* NAME = allocDBM(cdd_clocknum) /* Allocate a DBM. */ From b0bf73e52dfdcafe008f5ac2d81df98ebb79b7bc Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Tue, 26 Jul 2022 14:34:35 +0200 Subject: [PATCH 16/18] Add more tests (random and static one) --- test/test_cdd.cpp | 64 ++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 63 insertions(+), 1 deletion(-) diff --git a/test/test_cdd.cpp b/test/test_cdd.cpp index 8ed3b77..00306b8 100644 --- a/test/test_cdd.cpp +++ b/test/test_cdd.cpp @@ -804,7 +804,20 @@ void test_predt(size_t size) REQUIRE((!cdd_past(cdd1) & cdd_predt(cdd1, cdd_false())) == cdd_false()); REQUIRE(cdd_equiv(cdd_predt(cdd1, cdd_true()), cdd_false())); - // TODO: how to check cdd_predt when the safe cdd is a random cdd as well? + // Check timed predecessor for random, but non-overlapping safe cdd. + if (size == 0) + return; + cdd b1 = cdd_bddvarpp(bdd_start_level); + cdd cdd2_part; + for (uint32_t i = 0; i < n_dbms; i++) { + dbm.generate(); + cdd_part |= cdd(dbm.raw(), dbm.size()); + } + + cdd left = cdd_part & b1; + cdd right = cdd2_part & !b1; + cdd test = left | right; + REQUIRE(cdd_equiv(cdd_predt(test, right), cdd_remove_negative(cdd_past(left)))); } static void test(const char* name, TestFunction f, size_t size) @@ -873,6 +886,55 @@ TEST_CASE("CDD intersection with size 3") cdd_done(); } +TEST_CASE("CDD timed predecessor static test") +{ + cdd_init(100000, 10000, 10000); + 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: the bellow test case passes only on 32-bit, need to fix it #if INTPTR_MAX == INT32_MAX TEST_CASE("CDD reduce with size 3") From 2ec42d33dd700ef45ff4074942af01069f99f748 Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Tue, 26 Jul 2022 14:49:49 +0200 Subject: [PATCH 17/18] Change ADBM macro and avoid potential most-vexing parse problem --- src/cppext.cpp | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/cppext.cpp b/src/cppext.cpp index a08fbe1..34df0ce 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -14,7 +14,7 @@ #include #include -#define ADBM(NAME) raw_t* NAME = allocDBM(cdd_clocknum) +#define ADBM(NAME, DIM) raw_t* NAME = allocDBM(DIM) /* Allocate a DBM. */ static raw_t* allocDBM(uint32_t dim) { return (raw_t*)malloc(dim * dim * sizeof(raw_t)); } @@ -72,7 +72,7 @@ cdd cdd::operator=(ddNode* node) */ extraction_result cdd_extract_bdd_and_dbm(const cdd& state) { - ADBM(dbm); + ADBM(dbm, cdd_clocknum); cdd bdd_part = cdd_extract_bdd(state, cdd_clocknum); cdd cdd_part = cdd_extract_dbm(state, dbm, cdd_clocknum); extraction_result res; @@ -103,7 +103,7 @@ cdd cdd_delay(const cdd& state) cdd copy = state; cdd res = cdd_false(); - ADBM(dbm); + ADBM(dbm, cdd_clocknum); while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) { copy = cdd_reduce(copy); cdd bottom = cdd_extract_bdd(copy, cdd_clocknum); @@ -171,12 +171,12 @@ cdd cdd_predt_dbm(raw_t* dbm_target, cdd bdd_target, const cdd& safe) // Paranoia check. assert(!cdd_eval_false(all_booleans & bdd_target)); - dbm::fed_t bad_fed(dbm_target, cdd_clocknum); - ADBM(dbm_good); + auto bad_fed = dbm::fed_t{dbm_target, (uint32_t)cdd_clocknum}; + ADBM(dbm_good, cdd_clocknum); cdd good_copy = good_part_with_fitting_bools & all_booleans; if (!cdd_eval_false(good_copy)) { - dbm::fed_t good_fed(cdd_clocknum); + auto good_fed = dbm::fed_t{(uint32_t)cdd_clocknum}; while (!cdd_isterminal(good_copy.handle()) && cdd_info(good_copy.handle())->type != TYPE_BDD) { extraction_result res_good = cdd_extract_bdd_and_dbm(good_copy); good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part)); @@ -192,13 +192,13 @@ cdd cdd_predt_dbm(raw_t* dbm_target, cdd bdd_target, const cdd& safe) good_fed.add(dbm_good, cdd_clocknum); } - dbm::fed_t pred_fed = bad_fed.predt(good_fed); + auto pred_fed = bad_fed.predt(good_fed); result |= cdd_from_fed(pred_fed) & all_booleans; } else { // For all boolean valuations we did not reach with our safe CDD, we take the past of the // current target DBM. - ADBM(local); + ADBM(local, cdd_clocknum); dbm_copy(local, dbm_target, cdd_clocknum); dbm_down(local, cdd_clocknum); cdd past = cdd(local, cdd_clocknum) & all_booleans; @@ -237,7 +237,7 @@ cdd cdd_predt(const cdd& target, const cdd& safe) cdd allThatKillsUs = cdd_false(); cdd copy = target; - ADBM(dbm_target); + ADBM(dbm_target, cdd_clocknum); if (cdd_isterminal(target.handle()) || cdd_info(target.handle())->type == TYPE_BDD) { dbm_init(dbm_target, cdd_clocknum); @@ -292,7 +292,7 @@ cdd cdd_past(const cdd& state) cdd copy = state; cdd res = cdd_false(); - ADBM(dbm); + ADBM(dbm, cdd_clocknum); while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) { copy = cdd_reduce(copy); cdd bottom = cdd_extract_bdd(copy, cdd_clocknum); @@ -325,7 +325,7 @@ cdd cdd_apply_reset(const cdd& state, int32_t* clock_resets, int32_t* clock_valu // Apply bool resets. if (num_bool_resets > 0) - copy = cdd_exist(copy, bool_resets, NULL, num_bool_resets, 0); + copy = cdd_exist(copy, bool_resets, nullptr, num_bool_resets, 0); for (int i = 0; i < num_bool_resets; i++) { if (bool_values[i] == 1) { @@ -414,7 +414,7 @@ cdd cdd_transition_back(const cdd& state, const cdd& guard, const cdd& update, i // Apply bool resets. if (num_bool_resets > 0) - copy = cdd_exist(copy, bool_resets, NULL, num_bool_resets, 0); + copy = cdd_exist(copy, bool_resets, nullptr, num_bool_resets, 0); // Special cases when we are already done. if (num_clock_resets == 0) From 587b57ac66e55db7e06c39711adee05ee3ae116a Mon Sep 17 00:00:00 2001 From: Martijn Goorden Date: Tue, 26 Jul 2022 15:34:52 +0200 Subject: [PATCH 18/18] Fix memory leakage in cdd_predt --- src/cppext.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/cppext.cpp b/src/cppext.cpp index 34df0ce..4e68e32 100644 --- a/src/cppext.cpp +++ b/src/cppext.cpp @@ -180,6 +180,7 @@ cdd cdd_predt_dbm(raw_t* dbm_target, cdd bdd_target, const cdd& safe) while (!cdd_isterminal(good_copy.handle()) && cdd_info(good_copy.handle())->type != TYPE_BDD) { extraction_result res_good = cdd_extract_bdd_and_dbm(good_copy); good_copy = cdd_reduce(cdd_remove_negative(res_good.CDD_part)); + free(dbm_good); dbm_good = res_good.dbm; cdd bdd_good = res_good.BDD_part; good_fed.add(dbm_good, cdd_clocknum); @@ -203,7 +204,9 @@ cdd cdd_predt_dbm(raw_t* dbm_target, cdd bdd_target, const cdd& safe) dbm_down(local, cdd_clocknum); cdd past = cdd(local, cdd_clocknum) & all_booleans; result |= past; + free(local); } + free(dbm_good); } } else { @@ -241,18 +244,22 @@ cdd cdd_predt(const cdd& target, const cdd& safe) if (cdd_isterminal(target.handle()) || cdd_info(target.handle())->type == TYPE_BDD) { dbm_init(dbm_target, cdd_clocknum); - return cdd_predt_dbm(dbm_target, target, safe); + cdd result = cdd_predt_dbm(dbm_target, target, safe); + free(dbm_target); + return result; } // Split target into DBMs. while (!cdd_isterminal(copy.handle()) && cdd_info(copy.handle())->type != TYPE_BDD) { extraction_result res = cdd_extract_bdd_and_dbm(copy); copy = cdd_reduce(cdd_remove_negative(res.CDD_part)); + free(dbm_target); dbm_target = res.dbm; cdd bdd_target = res.BDD_part; allThatKillsUs |= cdd_predt_dbm(dbm_target, bdd_target, safe); } + free(dbm_target); return allThatKillsUs; }