import type { Fairness, LivenessProperty, WorldView } from "../spec/index.ts";
/** A fair step's identity, the same wherever it is possible (a hash of its name). */
export type FairId = number;
/** A predicate a liveness property is made of. */
export type Predicate = (w: WorldView) => boolean;
/** The predicates of liveness properties, in a fixed order: owners evaluate them in every world they keep. */
export declare function predicatesOf(properties: LivenessProperty[]): Predicate[];
/** A step on the graph: where it goes, which of its world's options takes it, whether it is a fault, and its fairness identity, if fair. */
export interface Edge {
    to: number;
    option: number;
    fault: boolean;
    fair?: FairId;
}
/** What the search hands over: for each node, whether its successors are known, its edges, the fair steps possible there, and which predicates hold in it. */
export interface Graph {
    size: number;
    /** Whether a predicate holds in each node. A predicate that throws in a world is false there. */
    holds: (predicate: Predicate) => (node: number) => boolean;
    roots: number[];
    /** Root 0's node: where behaviours begin, for `eventually`. */
    initial: number;
    expanded: boolean[];
    /** Nodes that stand only for a counterexample's last step (errors, broken steps): not part of the graph. */
    shadow: boolean[];
    edges: Edge[][];
    /** Fair steps possible in each node, by identity. */
    enabled: Map<FairId, Fairness>[];
    /** A path from a root to each node, as the search found it. */
    parent: number[];
    /** Which of the parent's options leads to each node, and whether it is a fault. */
    optionFrom: number[];
    faultFrom: boolean[];
}
/** A step of a lasso: the node it is taken in, and which of its options. */
export interface LassoStep {
    from: number;
    option: number;
}
export interface Lasso {
    /** The root the way in starts at. */
    root: number;
    prefix: LassoStep[];
    /** Repeated forever; empty when the behaviour stays in the last world. */
    loop: LassoStep[];
}
export type LivenessVerdict = {
    holds: true;
    unfinished: boolean;
    tested?: number;
} | {
    holds: false;
    lasso: Lasso;
    tested?: number;
};
export declare function judgeLiveness(graph: Graph, property: LivenessProperty): LivenessVerdict;