Module ctl 

Constants

MAX_CTL_STATES

Computation-Tree Logic (CTL) — BRANCHING-time temporal logic over a transition system, distinct from the LINEAR-time temporal_ltl. Transitions are (state →next→ state') edges (predicate == next); a state satisfies a proposition when (state, holds, prop) is present. Bounded, zero-heap. Max states explored by the bounded zero-heap CTL reachability.

Functions

all_finally

AF φ — on ALL paths from start, prop eventually holds. Least-fixpoint labelling: a state is AF if it satisfies prop, or it has ≥1 successor and ALL successors are AF (a prop-free cycle or prop-free deadlock falsifies it). Bounded + zero-heap.

all_until

A[φ U ψ] — on EVERY path from start, phi holds at each state until psi becomes true (and psi is reached on every path). Least-fixpoint labelling. Bounded + zero-heap. Completes the CTL operator set (EX, AX, EF, AF, EG, AG, EU, AU).

always_globally

AG φ — EVERY state reachable from start (including start) satisfies the invariant inv. Zero-heap BFS.

always_next

AX φ — ALL immediate successors of start satisfy prop (vacuously true if none).

exists_finally

EF φ — from start, SOME path eventually reaches a state satisfying prop. Zero-heap BFS over next edges.

exists_globally

EG φ — SOME path from start on which the invariant prop holds forever. Greatest-fixpoint labelling (Emerson-Clarke): keep a prop-state alive while it retains a successor that is also alive; EG holds iff start survives. Bounded + zero-heap.

exists_next

EX φ — SOME immediate successor of start satisfies prop.

exists_until

E[φ U ψ] — SOME path on which phi holds at every state until psi becomes true. Zero-heap BFS constrained to phi-states.

fair_globally

Fair EG φ — an infinite path from start on which prop holds forever AND a fair state is visited infinitely often. The fairness constraint eliminates unrealistic infinite loops that make no progress. True iff some fair state — reachable from start within the prop-states that have an infinite prop-future — lies on a cycle. Bounded + zero-heap.