using dd package properly

I want to see how many combinations of XX00 to XX11 would be possible, where X represents don't care of either '1' or '0'? I assume there would be a total of 16 possibilities.

If "A= XX00 to B=XX11", I mean all possible ways to go from state "A=XX00" to "B=XX11". XX={00, 01, 10, 11}. So, $A={0000, 0100, 1000, 1100}$ and $B={0011, 0111, 1011, 1111}$. Finally, as there are 4 unique candidates of A, and B, there are 16 possible ways $A -> B$ can happen, e.g., $0000 -> 0011, 0000 -> 0111$,....$1100 -> 1111$.

Another example can be A="X001" to B="X11X". There are 8 possible ways, e.g., 0001 ->0110, 0001 ->0111... ... 1001->1111. Please let me know if the dd package can handle "don't care" examples like this and I can get the final count of 16 and 8 respectively.

An example that computes the result described above:

"""How to count transitions between two sets of states."""
import dd.autoref as _bdd

def setup_bdd(n_vars):
    """Declare variables in a new BDD instance."""
    bdd = _bdd.BDD()
    vrs = [f'x{i}' for i in range(n_vars)]
    primed_vrs = [f"{var}'" for var in vrs]
    bdd.declare(*vrs)
    bdd.declare(*primed_vrs)
    return bdd

def example_1():
    n_vars = 4
    bdd = setup_bdd(n_vars=n_vars)
    start = r'~ x2 /\ ~ x3'
    end = r" x2' /\ x3' "
    n = count_transitions(
        start, end, n_vars, bdd)
    print(f'{n} transitions in the first example')

def example_2():
    n_vars = 4
    bdd = setup_bdd(n_vars=n_vars)
    start = r'~ x1 /\ ~ x2 /\ x3'
    end = r" x1' /\ x2' "
    n = count_transitions(
        start, end, n_vars, bdd)
    print(f'{n} transitions in the second example')

def count_transitions(
        start, end, n_vars, bdd):
    action = f'{start} /\ {end}'
    u = bdd.add_expr(action)
    return bdd.count(u, nvars=2 * n_vars)

if __name__ == '__main__':
    example_1()
    example_2()

The method BDD.pick_iter is relevant, for example:

list(bdd.pick_iter(u, care_vars=vrs))

The example https://github.com/tulip-control/dd/blob/main/examples/reachability.py is about transitions of state machines.

Regarding care sets, the method omega.symbolic.fol.Context.to_expr (https://github.com/tulip-control/omega/blob/main/omega/symbolic/fol.py) takes a care set (as BDD) as optional argument.

Representing and reasoning about state machines using primed and unprimed identifiers is supported by the module https://github.com/tulip-control/omega/blob/main/omega/symbolic/temporal.py.

tulip-control / dd

using dd package properly #83