Graphs, trees, and state transitions

A file dependency, a friendship, a road, and a program transition can all be drawn as dots joined by lines. Their lines mean different things. Dependencies have direction; friendship might be symmetric; a road may have travel cost; a transition depends on the whole program state. An attractive drawing alone does not establish the mathematical model needed for a correct conclusion.

This module starts with finite graphs and declared conventions. You will count incidences, prove a tree theorem, explain traversal certificates, order prerequisites, and check a bounded retry protocol. Each result states what it guarantees and what information it needs. The same ideas later describe computation graphs, graph data, finite automata, and dependency systems.

Retrieval check: describe a relation as ordered pairs, separate an invariant from termination, and explain a linear operation count. Review Module 03, Module 04, and Module 06. Lists and dictionaries in the labs represent finite objects; the mathematical claims do not require a particular Python container.

A finite simple undirected graph consists of a finite vertex set V and an edge set E whose elements are two-element subsets of V. The edge {u,v} has two distinct endpoints and no orientation. Simple means there are no self-loops and no parallel copies of an edge. Edges AB and BA denote the same unordered pair under this convention, so storing both as separate edges would double-count.

A directed graph uses ordered pairs (u,v), often written u→v. The edge u→v does not imply v→u. We exclude loops and repeated pairs in our examples, although other graph conventions allow them. A loop, a repeated edge, and a weighted edge can each be useful in a different model. State those choices before applying a theorem whose proof counts endpoints or distinct neighbours.

Vertices are labels, not necessarily numbers or positions. A graph drawing assigns coordinates only to make the structure visible; crossing lines do not create a vertex unless one is declared. Moving a dot preserves the graph when the vertex and edge sets are unchanged. By contrast, deleting an isolated vertex changes V even though none of the visible edges change. This distinction matters when counting states or reporting unreachable objects.

An undirected vertex’s degree is its number of incident edges. In a simple graph this equals the number of neighbours. In a directed graph, indegree counts incoming edges and outdegree counts outgoing edges. A vertex can have high outdegree and zero indegree; treating those numbers as interchangeable could reverse a dependency interpretation. A directed loop, if allowed, contributes one to each directed degree.

A walk is a sequence of vertices with an appropriate edge between consecutive vertices. Its length is the number of edges traversed, one less than its vertex count. A path here is a walk with no repeated vertex. A cycle closes a walk without repeating other vertices; a simple undirected cycle has at least three edges under our conventions. A zero-length path consists of one vertex and establishes its reachability from itself.

An adjacency list stores each vertex’s neighbours. Include an empty list for F. For an undirected graph, each edge appears in two lists; for a directed graph, a list normally records outgoing neighbours only. The distinction affects both interpretation and storage counts. Sorted neighbour lists make our traces reproducible, but sorting is an implementation choice and not part of the graph’s mathematical definition.

An adjacency matrix uses a declared vertex order and entries Aᵢⱼ=1 when the corresponding edge exists, otherwise zero. For a simple undirected graph it is symmetric and its diagonal is zero. Row sums are degrees. With directed outgoing-edge conventions, row sums are outdegrees and column sums are indegrees. A matrix without its row and column labels leaves the represented relation ambiguous.

For v vertices and e edges, lists occupy O(v+e) entries; an undirected list has 2e neighbour incidences. A dense matrix has v² entries even when almost all are zero. Scanning all neighbours takes degree-dependent work in a list and v entry checks in a matrix. A matrix gives direct indexed edge lookup; an ordinary unsorted list may require scanning neighbours. Choose the representation for the operation and sparsity, rather than declaring one universally faster.

These costs assume small fixed-size labels and constant-cost indexing, with dictionary operations treated under the stated implementation model. They do not prove every hash table lookup has deterministic constant worst-case cost. Graphs with variable-size labels or enormous integer identifiers may incur extra representation work. As in Module 06, an O(v+e) conclusion belongs to a cost model, not to every possible encoding of the same abstract graph.

For every finite undirected graph without loops, the degree-sum identity is $\sum_{v\in V}\deg(v)=2|E|$. Count the same incidences in two ways. Grouping by vertices gives the left side; grouping by edges gives two endpoints per edge. This is a double-counting proof for all finite graphs under the convention, not an inference from a few computed degree sequences. If loops are allowed, assigning two incidences to each loop preserves the identity.

For a directed graph, $\sum_v\operatorname{outdeg}(v)=|E|$ and $\sum_v\operatorname{indeg}(v)=|E|$. Each directed edge has one source and one target. Adding both sums yields 2|E|, but either one separately counts only e. These identities give useful input checks; they do not by themselves prove a graph is connected or acyclic. Many nonisomorphic graphs share the same degree sequence.

Two vertices of an undirected graph are connected when there is a path between them. Reachability by walks gives the same condition: whenever a finite walk repeats a vertex, remove the closed intervening portion until no repetition remains. Connection is reflexive via a zero-length path, symmetric via reversing a path, and transitive via concatenating walks and removing repetition. Thus it is an equivalence relation, connecting this construction to Module 03.

Its equivalence classes are connected components. In our example one component is {A,B,C,D,E} and another is {F}. A graph is connected if all vertices lie in a single component; for trees below we additionally require a nonempty graph. The empty graph requires an explicitly chosen convention and is outside our tree theorem. A graph can contain a cycle and still be disconnected elsewhere, as this example does.

Direction changes reachability. From u there may be a directed path to v without a path back. Strong connection requires both directions and yields strongly connected components. Weak connection ignores orientation before finding components. A one-way chain A→B→C is weakly connected but its three vertices are in separate strongly connected components. The unqualified word connected is inadequate when an application needs directed reachability.

An edge whose removal increases the component count is a bridge. DE is a bridge in the example: deleting it separates E. AB is not a bridge because A can still reach B through C,D. An undirected edge on a cycle is not a bridge: the rest of that cycle provides a replacement route. Conversely, if an edge is not a bridge, an alternate endpoint path together with that edge forms a cycle.

Cycle detection must respect the graph type. In a directed traversal, an edge to an active ancestor witnesses a directed cycle. In an undirected traversal, the reverse appearance of the parent edge is expected and is not a two-edge cycle in a simple graph. A routine that flags every already-seen neighbour as a cycle will misclassify even a single undirected edge unless it handles the parent and discovery status correctly.

Degree identities are necessary checks, not complete recognition rules. A list of proposed degrees may have an even sum and still be impossible in a simple graph; for instance a three-vertex graph cannot give one vertex degree three. Similarly, e=v−1 alone does not imply a tree without connectedness or acyclicity. A triangle plus an isolated vertex has four vertices and three edges but is disconnected and cyclic.

A tree is a finite nonempty connected undirected graph with no cycle. A forest is an undirected graph with no cycle and may have several components, including isolated vertices. Every connected component of a finite forest is a tree. A one-vertex graph with no edges is a tree: it is connected by the zero-length path and has no cycle. Its edge count should be included in any proof claiming all positive sizes.

In a tree there is exactly one path between any two vertices. Connectedness supplies existence. If two distinct paths joined the same endpoints, follow them from the first point where they separate to a point where they meet again; those two different segments form a cycle. Conversely, a connected graph with unique endpoint paths cannot have a cycle, because the two arcs of that cycle would supply two paths between selected cycle vertices.

A leaf in an unrooted tree of at least two vertices has degree one. To prove such a tree has a leaf, take a path of maximum length, which exists because the graph is finite. An endpoint cannot have a neighbour outside the path, as that would extend it. It cannot have another neighbour farther along the path, as that would make a cycle. Therefore its only neighbour is the next vertex of the path. Both endpoints are leaves.

For a forest with v vertices and c components, summing the tree theorem component by component gives e=v−c. Isolated vertices contribute one vertex and zero edges, so the formula handles them correctly. The empty forest has v=e=c=0 and also satisfies the identity, even though it is not a tree under our definition. This extension is a sum over components rather than an unproved substitution into the connected theorem.

A rooted tree chooses one vertex as the root. The root-to-vertex path determines each nonroot vertex’s parent; the other neighbours are its children. Depth is the number of edges from the root. Height here is the maximum depth, so a single-node rooted tree has height zero. Other books sometimes count vertices instead of edges; comparing formulas requires checking that convention. Root choice changes depths and parents while preserving the unrooted tree.

A rooted leaf is a node with no children. For a tree with at least two vertices, a degree-one root has a child and is not a rooted leaf, although it is an unrooted leaf. This small distinction explains many confused endpoint counts. The single-node root has no children and is a rooted leaf despite having unrooted degree zero. Definitions should resolve these cases before using a formula such as the full-binary-tree identity from Module 04.

A spanning tree uses every vertex of a connected graph and only some of its edges. A traversal’s discovery-parent edges form one: every reachable nonroot vertex gets exactly one parent leading back toward the source, so the parent structure connects the component without a cycle. If the original graph is disconnected, traversing all components yields a spanning forest. A search from A in our graph cannot produce a spanning tree containing F because there is no connecting edge.

The edge theorem helps justify minimality. A tree loses connectedness when any edge is removed; its unique endpoint path used that edge. A connected graph with a cycle can lose a cycle edge without losing connectedness, so repeated deletions eventually leave a spanning tree. Finiteness ensures the deletion process ends. Therefore a connected graph needs at least v−1 edges, and a connected simple graph with exactly v−1 edges is a tree.

Breadth-first search (BFS) maintains a first-in-first-out queue. Mark the source discovered, assign it distance zero, and enqueue it. Repeatedly remove the queue front and examine outgoing neighbours. For each undiscovered neighbour, mark it immediately, assign a parent and distance one greater than the current vertex’s, then enqueue it. Marking at discovery ensures a vertex enters the queue only once, even when several predecessors point to it.

The queue processes discovered vertices in nondecreasing assigned distance. New neighbours get distance d+1 when a distance-d vertex is processed; they join behind all already waiting vertices. The queue’s frontier therefore advances one edge layer at a time. An invariant states that every discovered label is the length of a concrete parent path from the source and that every processed vertex’s outgoing edges have been examined. The parent path supplies an upper bound on the shortest distance.

For a general shortest-path proof, suppose a reachable vertex had a shorter path than its BFS label. Along a shortest path choose the first vertex with a label larger than its path-prefix length. Its predecessor has the correct smaller label and is processed before larger-distance vertices. Examining their connecting edge would discover the next vertex with a label no larger than that prefix length, or it would already have such a label. Either case contradicts the choice. Thus the discovered parent path has minimum edge count.

A returned distance map can also be checked as a certificate. Require source label zero, a valid parent edge for each other labelled vertex with distance increasing by one, and the inequality d(v)≤d(u)+1 on every outgoing edge from a labelled u. Require all successors of labelled vertices to be labelled. Parent chains provide paths of the reported lengths, while chaining the inequalities along any source path shows the reported label cannot exceed its length. Together these conditions establish optimality without repeating BFS’s exact queue trace.

Depth-first search (DFS) explores an undiscovered neighbour recursively before returning to examine the next neighbour. Discovery order is preorder; completion order is postorder. On our alphabetically ordered lists the recursive preorder is A,B,D,C,E, whereas postorder is C,E,D,B,A. Both orders reach the same component as BFS, but the DFS discovery path to C is A,B,D,C even though edge AC exists. DFS parent depth therefore need not be a shortest-path distance.

DFS’s conceptual recursion maintains an active path on the call stack. In a directed graph, an edge to a currently active vertex closes a directed cycle. An edge to an already completed vertex does not establish such a cycle. Distinguish undiscovered, active, and finished states when reasoning about DFS; a single visited Boolean proves reachability but does not capture every cycle-detection claim. The stack or an explicit stack representation also uses memory proportional to the maximum exploration depth.

With adjacency lists, each discovered vertex is processed once and each outgoing neighbour entry is scanned once. A full traversal across every component costs O(v+e) in the declared operation model; searching from one source only scans its reachable part, plus any separately initialised bookkeeping. A matrix scan takes O(v²) for a full traversal. Python’s deque implements queue removal without shifting all remaining elements; repeatedly using list.pop(0) would add work not covered by the simple queue-operation model.

BFS minimises edge count, which is also total cost when every edge has the same positive weight. For unequal weights, a one-edge route costing ten can be worse than a two-edge route costing one plus one. Running ordinary BFS unchanged does not minimise that total. A weighted shortest-path algorithm requires additional assumptions and a different invariant; do not import the unweighted proof merely because both methods use a frontier.

A directed acyclic graph (DAG) has no directed cycle. In a dependency model u→v will mean that u must be completed before v. This orientation is a design decision: another application might store the reverse lookup of what v depends on. Declare the meaning rather than inferring it from an arrow style. A topological order lists each vertex exactly once and places every source u before its target v for every edge u→v.

Every finite nonempty DAG has a vertex of indegree zero. Otherwise start at any vertex and repeatedly choose an incoming predecessor. A finite graph cannot supply endlessly distinct vertices, so a repetition would produce a directed cycle. The contradiction establishes a starting vertex. Notice the role of finiteness: an infinite backward chain could lack both a zero-indegree vertex and a finite cycle, so this proof does not extend automatically to infinite graphs.

Kahn’s algorithm repeatedly chooses an indegree-zero remaining vertex, outputs it, and removes its outgoing edges by decrementing remaining indegrees. Its invariant says output vertices respect all already-output dependencies, and remaining indegrees count exactly the predecessors not yet output. Every selected vertex has no unfinished predecessor. Removing a vertex from a DAG leaves a DAG, so the zero-indegree lemma allows the process to continue until all vertices are output.

If vertices remain but none has indegree zero, the remaining graph contains a directed cycle by that same predecessor argument. The blocked set can also include vertices downstream of a cycle, so it is not itself an exact list of cycle vertices. In the example with D→A, B can be processed, while A,C,D,E remain blocked. E is blocked because of C but lies on no directed cycle. A cycle witness requires an actual closed edge sequence such as A,C,D,A.

Topological order need not be unique. A queue chooses a valid ready task according to its insertion order; a heap gives alphabetic tie-breaking in our lab. That reproducibility has a cost: heap insertion and removal add logarithmic factors, so the heap version is not simply the plain O(v+e) queue implementation. A full validation of an order checks both that it is a permutation of V and that position(u)<position(v) for every edge. Missing isolated vertices fail the permutation condition.

A topological order also supports induction over dependencies. Suppose a value at v is computed only from already completed predecessor values. Prove a property for zero-indegree vertices, then assume it for all predecessors when processing v and show the update preserves it. This is ordinary induction on the position in a valid order, with edges establishing which earlier hypotheses are available. It underlies evaluation of acyclic computation graphs and dynamic programs.

For a simple scheduling example, give each task a nonnegative duration and unlimited parallel workers. Its earliest finish is its duration plus the maximum predecessor finish, with maximum zero when there are no predecessors. In our DAG, durations A=2, B=5, C=3, D=4, E=1 give finishes 2,5,8,12,9. The total makespan is 12. Summing all durations gives 15 and describes serial work, not the unlimited-parallel completion time.

This recurrence assumes tasks start as soon as dependencies finish, durations are fixed, and resources do not conflict. With one worker, memory limits, shared devices, or uncertain durations, that calculation need not describe a feasible schedule. A DAG models precedence, not every scheduling constraint. Keeping the assumptions visible helps a learner transfer the same graph to build systems or AI computation without promising unrealistic throughput.

A state-transition system specifies a state set S, permitted initial states, and a directed transition relation. An event labels an allowed change, but the state must contain enough information to determine its permitted successors. Two situations that look identical at the control-flow level may have different futures because their counters or flags differ. The model’s vertex is the whole state, not merely the line of code currently executing.

A two-control-state retry protocol uses idle and waiting. A send changes idle to waiting; an acknowledgement returns waiting to idle. To discuss a bounded implementation, also record the number of sends and whether an acknowledgement has been seen. These are product states: a state is a tuple of control, count, and flag. With two control values, counts zero through two, and two flag values there are twelve possible tuples, although only a subset are reachable under the declared rules.

To explore a finite model, run BFS or DFS from the initial state, generating exactly the declared successors. Keep a visited set of complete state tuples and a parent event for newly discovered states. BFS’s first path to a bad state is a shortest counterexample in number of model transitions. A trace names a concrete sequence of permitted changes and its violating state; merely reporting that an assertion failed would omit useful evidence for repairing the transition rule.

For a safety predicate I, an inductive invariant proof checks all initial states satisfy I and every permitted transition from an I-state preserves I. Induction on finite execution length then proves all reachable states satisfy I, including arbitrarily long executions. Exhaustive checking instead computes reachable states and tests I there. On a complete finite model it decides that model’s reachable-state safety; a general symbolic invariant may cover a much larger or unbounded system.

The lab finds six reachable states in the faulty model, including one unsafe tuple, and five in the repaired model. The unreachable tuple (idle,2,false) still belongs to the ambient product domain. It is unreachable because of the repaired rules, not because the tuple is syntactically impossible. Conversely, some unreachable tuples might violate I without affecting reachable-state safety. An inductive proof may strengthen I to exclude such tuples if its transition-preservation obligation otherwise fails.

Safety says a forbidden event or state never occurs. Liveness asks that a desired event eventually occurs. The repaired waiting-timeout self-loop is safe but permits an infinite execution that never receives acknowledgement. Neither finite reachability nor the absence of an unsafe state establishes eventual delivery. A liveness argument would need additional assumptions about the environment, such as a justified fairness condition, and a proof that those assumptions imply progress.

Exhaustiveness is only as complete as the chosen model. We permit at most two sends, one request, no cancellation, and no delayed-message or concurrent behaviour. Checking those states does not prove an unlimited-retry network implementation correct. Omitting a counter from the state can collapse situations with different legal retries; omitting message contents can hide a wrong-recipient acknowledgement. An abstraction requires its own argument about which real behaviours it represents.

The potential number of product states grows quickly when components are combined. Independent-looking flags, counters, and processes multiply the domain size even before transitions are generated. Reachable-state search can remain practical for small educational models while becoming costly for real software. A bounded test offers a useful counterexample or a precisely scoped checked claim; a proof, a sound abstraction, or a different analysis may be needed for a larger conclusion.

Each script uses the Python standard library and runs locally without a GPU. Predict the graph facts and witness first. Downloaded scripts are the exact sources executed for the displayed output.

Lab A Lists matrices and rejected graph inputs

Predict: write F’s list and matrix row; compute the degree sum. Run: execute the script. It builds both representations and rejects a loop, a duplicate undirected edge, and an unknown vertex. Explain: why AB and BA are duplicates under this convention, while the all-zero F row must remain. Change: remove AC, predict which cycle disappears, and rerun after updating the edge count checks.

Download lab1_representations.py

"""Represent one finite simple undirected graph, including an isolated vertex."""
VERTICES = tuple("ABCDEF")
EDGES = ("AB", "AC", "BD", "CD", "DE")

def build_graph(vertices, edges):
    graph = {v: [] for v in vertices}
    seen = set()
    for u, v in edges:
        if u not in graph or v not in graph or u == v:
            raise ValueError("Edges need two distinct declared vertices")
        key = frozenset((u, v))
        if key in seen:
            raise ValueError("Repeated undirected edge")
        seen.add(key)
        graph[u].append(v)
        graph[v].append(u)
    return {v: sorted(neighbours) for v, neighbours in graph.items()}

graph = build_graph(VERTICES, EDGES)
matrix = [[int(v in graph[u]) for v in VERTICES] for u in VERTICES]
print("Adjacency lists:", graph)
print("Matrix order:", " ".join(VERTICES))
for v, row in zip(VERTICES, matrix):
    print(v, " ".join(map(str, row)))
degrees = [len(graph[v]) for v in VERTICES]
assert sum(degrees) == 2 * len(EDGES)
assert all(matrix[i][j] == matrix[j][i] for i in range(6) for j in range(6))
print("Degrees:", degrees, "; sum =", sum(degrees), "; 2|E| =", 2 * len(EDGES))
print("Isolated vertices:", [v for v in VERTICES if not graph[v]])
for label, edges in [("loop", ("AA",)), ("duplicate", ("AB", "BA")), ("unknown", ("AZ",))]:
    try:
        build_graph(VERTICES, edges)
    except ValueError as error:
        print("Rejected", label + ":", error)

Adjacency lists: {'A': ['B', 'C'], 'B': ['A', 'D'], 'C': ['A', 'D'], 'D': ['B', 'C', 'E'], 'E': ['D'], 'F': []}
Matrix order: A B C D E F
A 0 1 1 0 0 0
B 1 0 0 1 0 0
C 1 0 0 1 0 0
D 0 1 1 0 1 0
E 0 0 0 1 0 0
F 0 0 0 0 0 0
Degrees: [2, 2, 2, 3, 1, 0] ; sum = 10 ; 2|E| = 10
Isolated vertices: ['F']
Rejected loop: Edges need two distinct declared vertices
Rejected duplicate: Repeated undirected edge
Rejected unknown: Edges need two distinct declared vertices

Lab B Traversals and topological certificates

Predict: BFS distances from A, recursive DFS preorder, and a valid dependency order. Run: inspect the returned parents and assertions checking local distance inequalities. Explain: why C’s DFS parent route can be longer than its BFS route, and why E can be blocked without lying on a directed cycle. Change: reverse neighbour orders and distinguish changed parent choices from unchanged shortest distances. The heap chooses alphabetic ready tasks and adds its own overhead.

Download lab2_traversals.py

"""Deterministic traversal certificates and dependency orders, not weighted paths."""
from collections import deque
from heapq import heapify, heappop, heappush

GRAPH = {"A": ["B", "C"], "B": ["A", "D"], "C": ["A", "D"],
         "D": ["B", "C", "E"], "E": ["D"], "F": []}

def bfs(graph, source):
    distance, parent, order = {source: 0}, {source: None}, []
    queue = deque([source])
    while queue:
        u = queue.popleft()
        order.append(u)
        for v in graph[u]:
            if v not in distance:  # Mark at discovery, before queueing.
                distance[v], parent[v] = distance[u] + 1, u
                queue.append(v)
    return order, distance, parent

def dfs(graph, source):
    seen, preorder, postorder = set(), [], []
    def visit(u):
        seen.add(u)
        preorder.append(u)
        for v in graph[u]:
            if v not in seen:
                visit(v)
        postorder.append(u)
    visit(source)
    return preorder, postorder

def topological(graph):
    indegree = dict.fromkeys(graph, 0)
    for neighbours in graph.values():
        for v in neighbours:
            indegree[v] += 1
    ready = [v for v in graph if indegree[v] == 0]
    heapify(ready)  # Alphabetic tie-breaking, with heap overhead.
    order = []
    while ready:
        u = heappop(ready)
        order.append(u)
        for v in graph[u]:
            indegree[v] -= 1
            if indegree[v] == 0:
                heappush(ready, v)
    return order, sorted(v for v in graph if indegree[v] > 0)

order, distance, parent = bfs(GRAPH, "A")
assert distance == {"A": 0, "B": 1, "C": 1, "D": 2, "E": 3}
for u, neighbours in GRAPH.items():
    if u in distance:
        for v in neighbours:
            assert v in distance and distance[v] <= distance[u] + 1
for v, p in parent.items():
    if p is not None:
        assert v in GRAPH[p] and distance[v] == distance[p] + 1
print("BFS order:", order)
print("Distances:", distance, "; F is unreachable")
print("Parents:", parent)
print("DFS preorder/postorder:", dfs(GRAPH, "A"))
dag = {"A": ["C"], "B": ["C"], "C": ["D", "E"], "D": [], "E": []}
order, blocked = topological(dag)
position = {v: i for i, v in enumerate(order)}
assert not blocked and all(position[u] < position[v] for u in dag for v in dag[u])
print("DAG topological order:", order)
cyclic = {v: neighbours[:] for v, neighbours in dag.items()}
cyclic["D"].append("A")
print("After adding D->A, processed/blocked:", topological(cyclic))
cycle = ["A", "C", "D", "A"]
assert all(v in cyclic[u] for u, v in zip(cycle, cycle[1:]))
print("Cycle witness:", " -> ".join(cycle))
print("Weighted trap: direct A->E costs 10; A->B->E costs 2. Fewest edges is not cheapest.")

BFS order: ['A', 'B', 'C', 'D', 'E']
Distances: {'A': 0, 'B': 1, 'C': 1, 'D': 2, 'E': 3} ; F is unreachable
Parents: {'A': None, 'B': 'A', 'C': 'A', 'D': 'B', 'E': 'D'}
DFS preorder/postorder: (['A', 'B', 'D', 'C', 'E'], ['C', 'E', 'D', 'B', 'A'])
DAG topological order: ['A', 'B', 'C', 'D', 'E']
After adding D->A, processed/blocked: (['B'], ['A', 'C', 'D', 'E'])
Cycle witness: A -> C -> D -> A
Weighted trap: direct A->E costs 10; A->B->E costs 2. Fewest edges is not cheapest.

Lab C A bounded protocol repair

Predict: trace send, retry, timeout and evaluate the declared safety predicate. Run: compare faulty and repaired reachable states. Explain: the scope of the five-state safety result and the possible infinite timeout execution. Change: permit a third send, expand the count domain and successor rule consistently, and check whether the same repair preserves the intended predicate. Do not describe this toy model as a verified network protocol.

Download lab3_protocol.py

"""Exhaustively explore a deliberately bounded, two-control-state retry model."""
from collections import deque

START = ("idle", 0, False)  # control, number of sends, acknowledgement seen

def successors(state, faulty):
    mode, count, ack = state
    if mode == "idle" and count == 0 and not ack:
        yield "send", ("waiting", 1, False)
    if mode == "waiting":
        if count < 2:
            yield "retry", ("waiting", count + 1, ack)
        yield "ack", ("idle", count, True)
        if count == 2:
            yield "timeout", ("idle", count, ack) if faulty else state

def safe(state):
    mode, count, ack = state
    return mode != "idle" or count == 0 or ack

def explore(faulty):
    queue, paths = deque([START]), {START: []}
    while queue:
        state = queue.popleft()
        for event, target in successors(state, faulty):
            if target not in paths:
                paths[target] = paths[state] + [event]
                queue.append(target)
    return paths

for faulty in (True, False):
    paths = explore(faulty)
    bad = [(state, path) for state, path in paths.items() if not safe(state)]
    print("faulty =", faulty, "; reachable =", len(paths), "; unsafe =", len(bad))
    for state, path in bad:
        print("Witness:", " -> ".join(path), "; state =", state)
    assert bool(bad) == faulty
    if not faulty:
        assert len(paths) == 5 and ("idle", 2, False) not in paths
print("Repair: timeout stays waiting; safety does not guarantee acknowledgement or termination.")
print("Scope: two sends maximum, no cancellation, one request, no delayed messages or concurrency.")

faulty = True ; reachable = 6 ; unsafe = 1
Witness: send -> retry -> timeout ; state = ('idle', 2, False)
faulty = False ; reachable = 5 ; unsafe = 0
Repair: timeout stays waiting; safety does not guarantee acknowledgement or termination.
Scope: two sends maximum, no cancellation, one request, no delayed messages or concurrency.

Exercises 1–12 are required; 13–14 are extensions. Prove claims for the declared graph conventions and give an actual edge sequence for a cycle witness.

The automatic score covers Questions 1–9. Question 10 is written and self-reviewed; the two activities test different kinds of evidence.

Use MIT Mathematics for Computer Science for graph, tree, and state-machine selections. Use MIT’s handshaking, connectivity, and trees notes to compare graph conventions. Read the BFS and DFS/topological sorting selections in MIT 6.006 lecture notes. These are external primary readings; the lesson and required exercises are original.

Treat a reading as a comparison of definitions and arguments. Reconcile any differences in path, leaf, or height conventions before transplanting a formula.

Without notes, define our tree, prove its edge count, describe BFS’s discovery rule, and give both a valid topological order and a cycle witness. Explain why a shortest-edge certificate does not minimise arbitrary weights and why a safe finite protocol need not deliver eventually.

Exit task: add an isolated vertex G to the example. State the new degree sum and component count; explain the unchanged distances from A and the effect on a full spanning forest. For a forest built by traversals, there are now seven vertices and three components, hence four discovery edges. The original graph still has five edges and degree sum ten; its nonforest cycle edge is not a discovery edge.

Ready to move on: you can distinguish the abstract graph, its representation, a traversal witness, and the scope of a correctness claim. The discrete branch next studies modular arithmetic and invertibility. See the course overview for lesson availability.