.. DO NOT EDIT. .. THIS FILE WAS AUTOMATICALLY GENERATED BY SPHINX-GALLERY. .. TO MAKE CHANGES, EDIT THE SOURCE PYTHON FILE: .. "tutorials/03_reachability.py" .. LINE NUMBERS ARE GIVEN BELOW. .. only:: html .. note:: :class: sphx-glr-download-link-note :ref:`Go to the end ` to download the full example code. .. rst-class:: sphx-glr-example-title .. _sphx_glr_tutorials_03_reachability.py: Reachability in a directed graph ==================================== Starting at node 0, which nodes of this graph can we reach? .. image:: /_static/reachability.svg :alt: Sixteen nodes. Node 3 points into the reachable grid but has no incoming edges. Nodes 12 through 15 form a separate cycle. :width: 780 We represent a state with one Boolean indicator per node. Exactly one indicator is true. For example, ``A₀(x₀, …, x₁₅) = x₀ ∧ ¬x₁ ∧ ⋯ ∧ ¬x₁₅``. A set of states is the disjunction of their indicators. With current-state variables ``x`` and next-state variables ``x′``, the transition relation is ``T(x, x′) = ⋁_{(i,j)∈E} (Aᵢ(x) ∧ Aⱼ(x′))``. .. GENERATED FROM PYTHON SOURCE LINES 21-32 .. code-block:: Python from tididi import Vtree, and_exists, cube, or_many nodes = 16 edges = [ (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), ] vtree = Vtree.balanced(2 * nodes) current_vars = list(range(1, nodes + 1)) .. GENERATED FROM PYTHON SOURCE LINES 33-37 Build state indicators -------------------------- Variable IDs begin at 1; graph nodes begin at 0. The state function asserts one indicator and negates every other indicator in the supplied group. .. GENERATED FROM PYTHON SOURCE LINES 37-44 .. code-block:: Python def state(vtree, indicators, node): return cube(vtree, (var if i == node else -var for i, var in enumerate(indicators))) at_current = [state(vtree, current_vars, node) for node in range(nodes)] reached = at_current[0].copy() .. GENERATED FROM PYTHON SOURCE LINES 45-47 The second group describes the state after a transition. Each edge contributes one conjunction to the relation; ``or_many`` combines them. .. GENERATED FROM PYTHON SOURCE LINES 47-52 .. code-block:: Python next_vars = list(range(nodes + 1, 2 * nodes + 1)) at_next = [state(vtree, next_vars, node) for node in range(nodes)] transition = or_many(at_current[a].copy() & at_next[b].copy() for a, b in edges) print("Transition pairs:", transition.pair_count()) .. rst-class:: sphx-glr-script-out .. code-block:: none Transition pairs: 176 .. GENERATED FROM PYTHON SOURCE LINES 53-57 Take one step ----------------- Conjoin the current states with the transition relation, then forget the old state: ``∃x. R(x) ∧ T(x, x′)``. .. GENERATED FROM PYTHON SOURCE LINES 57-60 .. code-block:: Python possible_steps = reached.copy() & transition.copy() successors = possible_steps.exists(current_vars) .. GENERATED FROM PYTHON SOURCE LINES 61-63 The result describes next-state variables. Rename those back to current-state variables so it can be used as the input to another step. .. GENERATED FROM PYTHON SOURCE LINES 63-67 .. code-block:: Python next_to_current = dict(zip(next_vars, current_vars)) successors = successors.rename(next_to_current) print("States after one step:", successors.projected_model_count(current_vars)) .. rst-class:: sphx-glr-script-out .. code-block:: none States after one step: 2 .. GENERATED FROM PYTHON SOURCE LINES 68-71 ``and_exists`` performs the conjunction and quantification we just wrote as two separate operations in a single call. It computes the same function and can avoid building parts of the intermediate conjunction. .. GENERATED FROM PYTHON SOURCE LINES 71-78 .. code-block:: Python def image(states, relation): return and_exists(states, relation, current_vars).rename(next_to_current) combined = image(reached.copy(), transition.copy()) print("Combined operation agrees:", combined.equivalent(successors)) .. rst-class:: sphx-glr-script-out .. code-block:: none Combined operation agrees: True .. GENERATED FROM PYTHON SOURCE LINES 79-84 Iterate to a fixed point ---------------------------- Keep the states already reached and add their successors. Semantic equivalence tells us when this adds no new states. We count projections onto current-state variables, since the next-state variables are free here. .. GENERATED FROM PYTHON SOURCE LINES 84-98 .. code-block:: Python iteration = 0 while True: successors = image(reached.copy(), transition.copy()) enlarged = reached.copy() | successors iteration += 1 count = enlarged.projected_model_count(current_vars) print(f"Iteration {iteration}: {count} states, " f"{enlarged.node_count()} circuit nodes, {enlarged.pair_count()} pairs") fixed = enlarged.equivalent(reached) reached = enlarged if fixed: print("Fixed point reached") break .. rst-class:: sphx-glr-script-out .. code-block:: none Iteration 1: 3 states, 35 circuit nodes, 37 pairs Iteration 2: 6 states, 40 circuit nodes, 45 pairs Iteration 3: 8 states, 41 circuit nodes, 48 pairs Iteration 4: 10 states, 42 circuit nodes, 51 pairs Iteration 5: 11 states, 42 circuit nodes, 52 pairs Iteration 6: 11 states, 42 circuit nodes, 52 pairs Fixed point reached .. GENERATED FROM PYTHON SOURCE LINES 99-103 Two reasons for being unreachable ------------------------------------- Node 3 is connected to the grid, but its edges point away from it and there is no path from 0 to 3. Nodes 12–15 form an entirely separate component. .. GENERATED FROM PYTHON SOURCE LINES 103-111 .. code-block:: Python print("Node 3 unreachable:", reached.implies(~at_current[3].copy())) separate_component = or_many(node.copy() for node in at_current[12:]) print("Nodes 12–15 unreachable:", reached.implies(~separate_component)) target = reached & at_current[11].copy() witness = target.satisfying_assignment() active = [node for node, var in enumerate(current_vars) if any(choice.variable == var and choice.sign for choice in witness)] print("Reachable target:", active) .. rst-class:: sphx-glr-script-out .. code-block:: none Node 3 unreachable: True Nodes 12–15 unreachable: True Reachable target: [11] .. _sphx_glr_download_tutorials_03_reachability.py: .. only:: html .. container:: sphx-glr-footer sphx-glr-footer-example .. container:: sphx-glr-download sphx-glr-download-jupyter :download:`Download Jupyter notebook: 03_reachability.ipynb <03_reachability.ipynb>` .. container:: sphx-glr-download sphx-glr-download-python :download:`Download Python source code: 03_reachability.py <03_reachability.py>` .. container:: sphx-glr-download sphx-glr-download-zip :download:`Download zipped: 03_reachability.zip <03_reachability.zip>`