import { type Event, type PropertyInfo, type Spec, type World } from "../spec/index.ts";
import { type Symmetry } from "./keys.ts";
import { type Variety } from "./integer.ts";
import type { RuleVerdict } from "./rules.ts";
import { type Counterexample, type ScenarioPlace } from "./steps.ts";
export { apply, branches, placeText, QUIET, replay, type Choice, type Counterexample, type ScenarioPlace } from "./steps.ts";
export interface Bounds {
    /** Instances of each actor that is not a singleton (1 by default). */
    instances: Record<string, number>;
    /**
     * Longest path explored, in events: none by default, so a search goes on until it has every
     * world or meets a limit. With a depth, paths cut off at it leave what held unproved.
     */
    depth: number;
    /** Stop after this many distinct states. */
    maxStates: number;
    /** Stop after this long, in milliseconds. */
    timeLimit: number;
    /** Stop when the process holds more than this many megabytes (50% of the machine's by default). */
    memoryLimit: number;
    /** Random runs to try before the search; they take at most a quarter of the time limit. */
    walks: number;
    /** Longest random run, in events. */
    walkDepth: number;
    /** Treat interchangeable instances of one actor as one (see keys.ts). */
    symmetry: boolean;
    /**
     * How many merged twins to test a symmetry claim on: both must have the same next steps.
     * Each test runs every step from two worlds, so more tests catch a subtly wrong claim more
     * surely, at a cost; 0 trusts the claim.
     */
    symmetryChecks: number;
}
/** Which limit stopped a search early. */
export type StopReason = "maxStates" | "timeLimit" | "memoryLimit";
export declare const DEFAULT_BOUNDS: Bounds;
/** A property's verdict: it held, here is how it breaks, or (a reachable property) no world explored got there. */
export type PropertyResult = PropertyHeld | PropertyBroken | PropertyUnreached;
interface PropertyVerdict {
    id: string;
    kind: PropertyInfo["kind"];
    description: string;
    /** A known bug: why the property is expected to break. */
    known?: string;
    /**
     * For `leadsTo`: in how many explored worlds it was put to the test, `whenever` holding
     * and `then` not. Zero means exploration never got there, so holding says nothing.
     */
    tested?: number;
}
export interface PropertyHeld extends PropertyVerdict {
    holds: true;
    /**
     * Holding among the worlds explored, but not all of them: the search stopped early, or (for
     * liveness) the region it was judged on reaches worlds past the depth bound, where a loop
     * may lie.
     */
    unfinished?: boolean;
    /**
     * When the search stopped early: the length of the paths it had explored in full. A safety
     * property held on every path of up to this many events, from each world it started from.
     */
    upTo?: number;
    /** A reachable property: the way to a world that gets there, and who found it (the search: a shortest one). */
    witness?: Counterexample;
    witnessBy?: "search" | "walk";
}
/**
 * A reachable property no explored world got to. Whether that is a ✗ depends on whether every
 * world within the bounds was explored (verdict.ts): a search that stopped early, or that a
 * depth bound cut off, may not have got there yet.
 */
export interface PropertyUnreached extends PropertyVerdict {
    holds: false;
    unreached: true;
    /** When the search stopped early: no path of up to this many events got there. */
    upTo?: number;
}
export interface PropertyBroken extends PropertyVerdict {
    holds: false;
    unreached?: undefined;
    counterexample: Counterexample;
    /** Who found the counterexample: the search (shortest), or a random run (shrunk, maybe not shortest). */
    foundBy: "search" | "walk";
    /**
     * For liveness: what repeats forever after the counterexample, from where it ends. Empty
     * when the system stays where it ends (nothing fair can happen there).
     */
    loop?: Counterexample;
    /**
     * When the counterexample is not the shortest because a shorter one needs more faults:
     * that one's length and faults (see withFewestFaults).
     */
    shorter?: {
        events: number;
        faults: number;
    };
}
export interface Report {
    spec: string;
    bounds: Bounds;
    states: number;
    /** The scenario worlds explored from, besides the initial world. */
    seeds: ScenarioPlace[];
    /** Whether every state within the bounds was explored. */
    exhaustive: boolean;
    /**
     * Whether the depth bound cut paths off: the search met new worlds at the bound, and did not
     * go on from them. What held, held on every path of up to `bounds.depth` events.
     */
    cutAtDepth?: boolean;
    /** Why the search stopped early, when it did. */
    stoppedBy?: StopReason;
    /** When the search stopped early: what its states differ in, most first (integer engine). */
    variety?: Variety[];
    /** With `variety`: the most messages in flight at once in an explored world. */
    mostInFlight?: number;
    /** Each rule a property needs, checked in the design without it (RFD0010), when asked for (checkRules). */
    rules?: RuleVerdict[];
    depthReached: number;
    durationMs: number;
    properties: PropertyResult[];
    /** Spec bugs met while exploring: an undeclared send, a message nobody handles. */
    errors: {
        message: string;
        counterexample: Counterexample;
    }[];
    /** A world where nothing can happen and the spec does not call it final (the first found). */
    stuck?: {
        counterexample: Counterexample;
        foundBy: "search" | "walk";
    };
    /**
     * Steps that drew `ctx.random()`. The numbers are seeded: each draw got one value, and the
     * paths where it would have got another were not explored. A property that held is not proved.
     */
    chance?: string[];
    /** Steps that ran somewhere, in the search or a random run. */
    coverage: {
        reached: string[];
        missed: string[];
    };
    /** The random runs: how many, how many steps in all, and the longest. */
    walks: {
        runs: number;
        steps: number;
        deepest: number;
    };
    /** Symmetry: the instances taken as interchangeable. */
    reductions: {
        symmetric: string[][];
        /** Actors declared symmetric whose instances turned out not to be; the search was redone without. */
        refuted?: string[];
    };
}
/** A world to explore from besides the initial one: where a scenario's setup leaves it, or where it ends. */
export interface Seed extends ScenarioPlace {
    world: World;
    /** The scenario's events on the way there, which `never` properties judge paths from it with. */
    events?: readonly Event[];
}
/** Callbacks for tools that compare the checker with another: every distinct state, as the search first meets it. */
export interface Watch {
    state?(world: World, memory: string): void;
}
/** How to run a check, besides the bounds. */
export interface CheckOptions {
    /** Every distinct state, as the search first meets it. */
    watch?: Watch;
    /** Stop once every property has broken: for searches that only look for breaks. */
    untilBroken?: boolean;
    /** `never` properties to remember the whole path for: those an earlier search found to vary (nevers.ts). */
    wholePath?: readonly string[];
}
/** Where paths start: the initial world, then each seed, with the symmetry of each. */
export interface Root {
    from?: ScenarioPlace;
    /** The steps that led to it: a scenario's, none for the initial world. */
    events?: readonly Event[];
    world: World;
    symmetry: Symmetry;
}
/**
 * Explore every interleaving within the bounds, from the initial world and from each seed
 * at once, breadth first, after a share of random runs. Seeding with where scenarios end puts
 * the search where the interesting states are, rather than spending its budget getting there.
 */
export declare function check(spec: Spec, bounds?: Partial<Bounds>, seeds?: Seed[], options?: CheckOptions): Promise<Report>;
/** Singletons, plus the configured number of every other actor, labelled by actor: "Mac", or "Mac A", "Mac B"… */
export declare function initialWorld(spec: Spec, bounds: Pick<Bounds, "instances">): World;