5. Explore a directed graph

Starting at node 0, which nodes can we reach by following directed edges?

Use one Boolean indicator per node. A state means exactly one indicator is true:

S_i(x₀, …, x₁₅) = x_i ∧ ⋀_{j ≠ i} ¬x_j.

A second set of indicators describes the next state. The transition relation is

T(x, x′) = ⋁_{(i,j) ∈ E} (S_i(x) ∧ S_j(x′)).

5.1. Name the variables

The edge list describes the graph. Each current and next indicator gets its own variable in one shared vtree.

const size_t edges[][2] = {
    {0,1}, {1,2}, {3,2}, {4,5}, {5,6}, {6,7}, {8,9}, {9,10}, {10,11},
    {0,4}, {1,5}, {2,6}, {3,7}, {4,8}, {5,9}, {6,10}, {7,11},
    {4,0}, {5,1}, {10,6}, {11,7}, {12,13}, {13,15}, {15,14}, {14,12}
};
TididiVtree *vtree = NULL;
check(tididi_vtree_balanced(32, &vtree));
uint32_t current_vars[16], next_vars[16];
for (uint32_t i = 0; i < 16; ++i) {
    current_vars[i] = i + 1;
    next_vars[i] = i + 17;
}

The helper constructs one state as a conjunction of sixteen signed literals.

static TididiCircuit *state(const TididiVtree *vtree, const uint32_t vars[16], size_t node) {
    int64_t indicators[16];
    for (size_t i = 0; i < 16; ++i)
        indicators[i] = i == node ? (int64_t)vars[i] : -(int64_t)vars[i];
    TididiCircuit *result = NULL;
    check(tididi_cube(vtree, indicators, 16, &result, NULL));
    return result;
}

5.2. Compile the relation

For each edge, conjoin its source state with its destination state, then union all edges. The initial reachable set contains only node 0.

enum { EDGE_COUNT = sizeof(edges) / sizeof(edges[0]) };
TididiCircuit *terms[EDGE_COUNT] = {NULL}, *transition = NULL;
for (size_t i = 0; i < EDGE_COUNT; ++i) {
    TididiCircuit *source = state(vtree, current_vars, edges[i][0]);
    TididiCircuit *target = state(vtree, next_vars, edges[i][1]);
    check(tididi_and(source, target, &terms[i], NULL));
    release(source); release(target);
}
check(tididi_or_many(terms, EDGE_COUNT, &transition, NULL));
for (size_t i = 0; i < EDGE_COUNT; ++i) release(terms[i]);
TididiCircuit *reached = state(vtree, current_vars, 0);

5.3. Take one step

Conjoin the current set with the transition relation. Quantify the current variables to leave possible destinations, then rename next indicators to current indicators. Count only the current variables; next variables are free after renaming and should not multiply the number of states.

TididiCircuit *r = copy(reached), *t = copy(transition);
TididiCircuit *joined = NULL, *projected = NULL, *image = NULL;
check(tididi_and(r, t, &joined, NULL));
check(tididi_exists(joined, current_vars, 16, &projected, NULL));
check(tididi_rename(projected, next_vars, current_vars, 16, &image, NULL));
uint64_t states = 0;
check(tididi_projected_model_count(image, current_vars, 16, &states, NULL));
printf("States after one step: %" PRIu64 "\n", states);

Output:

States after one step: 2

5.4. Reach a fixed point

tididi_and_exists performs the AND followed by existential quantification from the preceding step in one call. It can avoid constructing the full intermediate conjunction. Union the image with the states already reached, minimize, and compare Boolean functions to detect convergence.

for (unsigned step = 1; ; ++step) {
    r = copy(reached); t = copy(transition);
    TididiCircuit *next = NULL, *renamed = NULL, *candidate = NULL, *smaller = NULL;
    check(tididi_and_exists(r, t, current_vars, 16, &next, NULL));
    check(tididi_rename(next, next_vars, current_vars, 16, &renamed, NULL));
    TididiCircuit *old_copy = copy(reached);
    check(tididi_or(old_copy, renamed, &candidate, NULL));
    check(tididi_minimize(candidate, &smaller, NULL));
    bool done = false;
    check(tididi_equivalent(reached, smaller, &done, NULL));
    size_t nodes = 0, pairs = 0;
    check(tididi_size(smaller, &nodes, &pairs));
    check(tididi_projected_model_count(smaller, current_vars, 16, &states, NULL));
    printf("Step %u: %" PRIu64 " states, %zu nodes, %zu pairs%s\n",
           step, states, nodes, pairs, done ? " (fixed point)" : "");
    release(reached); reached = smaller;
    release(r); release(t); release(next); release(renamed);
    release(old_copy); release(candidate);
    if (done) break;
}

Output:

Step 1: 3 states, 35 nodes, 37 pairs
Step 2: 6 states, 40 nodes, 45 pairs
Step 3: 8 states, 41 nodes, 48 pairs
Step 4: 10 states, 42 nodes, 51 pairs
Step 5: 11 states, 42 nodes, 52 pairs
Step 6: 11 states, 42 nodes, 52 pairs (fixed point)

5.5. Inspect the result

Node 3 has edges leading into the reachable region but no directed path from node 0 reaches it. Nodes 12 through 15 form a separate component. Test each state by intersecting it with the final reachable set.

for (size_t node = 0; node < 16; ++node) {
    TididiCircuit *at_node = state(vtree, current_vars, node);
    TididiCircuit *reached_copy = copy(reached), *overlap = NULL;
    check(tididi_and(reached_copy, at_node, &overlap, NULL));
    bool reachable = false;
    check(tididi_is_sat(overlap, &reachable, NULL));
    if (!reachable) printf("Unreachable: %zu\n", node);
    release(at_node); release(reached_copy); release(overlap);
}

Output:

Unreachable: 3
Unreachable: 12
Unreachable: 13
Unreachable: 14
Unreachable: 15

5.6. Complete program

Download reachability.c and the shared helper. The source includes cleanup for all handles. Both files are included in the source checkout.