Module traffic_flow 

Traffic FLOW / capacity analysis as model checking.

An approach’s queue is a bit-vector counter; “can it JAM (overflow capacity)?” is a reachability question — exactly what our BMC engine answers, no new mathematics. Each model is synthesizable Verilog, so it rides the existing RTL path (parse_transition_system → bmc / prove_invariant) and the queue level renders straight into the waveform.

• An approach whose service keeps up with demand only ever drains → prove_invariant certifies it never jams (for all time).
• An approach that is under-served (green only part of the cycle while demand keeps arriving) grows without bound until it jams → bmc finds the exact cycle (the jam trace).

capacity here is the queue width’s range; the jam threshold is the level we forbid.

Functions

balanced_approach

A queue with a starting backlog and service that exceeds arrivals: it only ever drains, so it provably never reaches jam — for all reachable states (k-induction).

congested_approach

A queue served only every other cycle while one vehicle arrives each cycle: net inflow is positive, so the queue climbs to jam. BMC finds the cycle it overflows.