Add cdd predt operator

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

src/cppext.cpp

@@ -11,7 +11,10 @@
 
 #include "cdd/kernel.h"
 
-#define ADBM(NAME) raw_t* NAME = allocDBM(size)
+#include <dbm/fed.h>
+#include <dbm/print.h>
+
+#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)); }
@@ -69,10 +72,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);
+    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;
     res.BDD_part = bdd_part;
     res.CDD_part = cdd_part;
@@ -93,27 +95,174 @@ extraction_result cdd_extract_bdd_and_dbm(const cdd& state)
  */
 cdd cdd_delay(const cdd& state)
 {
-    if (cdd_isterminal(state.root))
+    // First some trivial cases.
+    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) {
+    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, 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;
     }
     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);
+    cdd res = cdd_false();
+    for (auto& zone : fed) {
+        res |= cdd(zone.const_dbm(), cdd_clocknum);
+    }
+    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.
+ *
+ * <p>If there is an overlap between \a target and \a safe, the overlap is considered
+ * to be saved.</p>
+ * @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)
+{
+    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 (auto i = 0u; i < (1u << cdd_varnum); ++i) {
+            cdd all_booleans = cdd_true();
+            for (auto j = 0u; 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));
+
+            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)) {
+                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));
+                    free(dbm_good);
+                    dbm_good = res_good.dbm;
+                    cdd bdd_good = res_good.BDD_part;
+                    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, cdd_clocknum);
+                    good_fed.add(dbm_good, cdd_clocknum);
+                }
+
+                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, cdd_clocknum);
+                dbm_copy(local, dbm_target, cdd_clocknum);
+                dbm_down(local, cdd_clocknum);
+                cdd past = cdd(local, cdd_clocknum) & all_booleans;
+                result |= past;
+                free(local);
+            }
+            free(dbm_good);
+        }
+
+    } 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, cdd_clocknum);
+        cdd past = cdd(dbm_target, cdd_clocknum) & 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.
+ *
+ * <p>If there is an overlap between \a target and \a safe, the overlap is considered
+ * to be saved.</p>
+ * @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)
+{
+    // First some trivial cases.
+    if (target == cdd_false())
+        return target;
+    if (safe == cdd_true())
+        return cdd_false();
+
+    cdd allThatKillsUs = cdd_false();
+    cdd copy = target;
+    ADBM(dbm_target, cdd_clocknum);
+
+    if (cdd_isterminal(target.handle()) || cdd_info(target.handle())->type == TYPE_BDD) {
+        dbm_init(dbm_target, cdd_clocknum);
+        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;
+}
+
 /**
  * Perform the delay operation on a CDD taking an invariant into account.
  *
@@ -142,21 +291,22 @@ cdd cdd_delay_invariant(const cdd& state, const cdd& invar)
  */
 cdd cdd_past(const cdd& state)
 {
-    if (cdd_isterminal(state.root))
+    // First some trivial cases.
+    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);
+    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, 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;
 }
@@ -182,7 +332,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) {
@@ -196,14 +346,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;
@@ -271,18 +421,18 @@ 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)
         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;