import { type Spec, type World } from "../spec/index.ts";
import type { Bounds, Root, StopReason, Watch } from "./explore.ts";
import { type Graph, type LassoStep } from "./liveness.ts";
import { type Choice } from "./steps.ts";
/** One thing the explored states differ in, and in how many ways (see `IntegerSearch.variety`). */
export interface Variety {
    /** `Actor.field`, or `message name` for the messages of that name in flight. */
    what: string;
    values: number;
}
/** A step of a lasso, replayed: its choice, and the world it was taken in, when asked for. */
export interface Resolved {
    choice: Choice;
    world?: World;
}
/** The search, with what `reportOf` (explore.ts) reads of it. */
export declare class IntegerSearch {
    private readonly spec;
    private readonly b;
    readonly roots: Root[];
    private readonly watch;
    private readonly started;
    readonly failures: Map<string, number>;
    readonly errors: Map<string, number>;
    stuckAt: number | undefined;
    states: number;
    stoppedBy: StopReason | undefined;
    /** A symmetry claim turned out false: the search stopped, to be run again without it. */
    refuted: boolean;
    depthReached: number;
    /** Every path of up to this many events, from each root, was explored; the rest only if not stopped. */
    completeDepth: number;
    /** The most messages in flight at once in any explored world. */
    mostInFlight: number;
    /** Stop once every property has broken: nothing is left to learn (a rule's claim, RFD0010). */
    untilBroken: boolean;
    /** Whether it stopped because every property had broken. */
    allBroken: boolean;
    readonly root: number[];
    private parent;
    /** How each node was reached from its parent: a `ChoiceName` id, found again in any world. */
    private named;
    private faults;
    private depth;
    /** Each node's last event, as a `TraceStep` id: a path's events go up its parents, oldest last. */
    private eventOf;
    private readonly broken;
    private instanceStates;
    private pendings;
    /** By `actor.step`: whether the step is tagged `fault`. */
    private freshes;
    private stepArgs;
    private stepNames;
    private readsWorld;
    /** The world's variables, by their key; 0 is none set, so a spec without variables keeps 0. */
    private worldVariables;
    /** `takers`, by pending entry and then by its receiver's state. */
    /** By instance state id: whether a `when` of its actor reads the world's variables (whenReadsWorld). */
    private readsWorldIn;
    private fires;
    /** By step index: a step that has run apart from its instance's state (Effect.apart). */
    private runsApart;
    private timerLists;
    private names;
    private stepKeys;
    private traceSteps;
    private memories;
    private nevers;
    private everySteps;
    private reachedSteps;
    /** Key lines (keys.ts), named by integers: what symmetric fingerprints are made of. */
    private lines;
    private renamedBy;
    /** For nodes from roots with symmetry: the fingerprint of the world without renaming, which renamed twins do not share. */
    private plains;
    private twinChecks;
    /**
     * For choices that do not name a pending entry (actions, guards), which are shared objects
     * (`planOf`): the step cache's argument, and the choice's name, worked out once.
     */
    private facts;
    /** Choices of actions whose inputs come from `examples`, by (tuple, instance, action). */
    private examples;
    /** While twin checks remain: each state's vector, so a twin's world need not be replayed. */
    private twinWorlds;
    private seen;
    /** For liveness: edges out of each expanded node, the fair steps possible there, and which predicates hold. */
    private readonly keepsEdges;
    private readonly predicates;
    /**
     * Properties see a world's instances and whether anything is pending, nothing else: its
     * tuple, interned. Their answers are kept by tuple, and by pairs of tuples for step
     * properties: most states differ from others only in what is in flight.
     */
    private tuples;
    /** By tuple: the `always` properties that fail there, and which liveness predicates hold. */
    private alwaysFailing;
    private truthsByTuple;
    /** Each node's tuple, for liveness; -1 for shadow nodes. */
    private tupleOfNode;
    /** By (tuple before, tuple after, trace step): each step property's answer, HOLDS or BREAKS, if known. */
    private stepAnswers;
    private expanded;
    private shadow;
    private option;
    private edges;
    private enabled;
    /** One per set of instances the roots have, by their sorted ids. */
    private layouts;
    private always;
    constructor(spec: Spec, b: Bounds, roots: Root[], watch: Watch, started: number);
    /** Steps that ran, as `actor.key`. */
    get stats(): {
        reached: Set<string>;
    };
    /**
     * The layout for a root's instances. World keys sort instances (keys.ts), so a set of them is one
     * layout, in the order of the first root that has it (which the choices follow).
     */
    private layoutOf;
    run(): void;
    /** One node per distinct root: judged, and the frontier to start from. */
    private start;
    /** A new state at a depth: expanded in the next round, or (for liveness) closed at the end. */
    private queue;
    /** Every step from a frontier entry, in the order `branches` gives them. False when the search must stop. */
    private expand;
    /**
     * A step that fails: a spec error, which goes nowhere. The first time an error is met, a node
     * of its own (a shadow, not a state) ends its counterexample. False if it refutes symmetry.
     */
    private failed;
    /**
     * Where a step lands (see Search.land). On a known state, it adds an edge, and its world is
     * tested against a renamed twin's; if it breaks a step property, a shadow node ends that
     * counterexample. On a new state, a node, judged and queued. False when the search must stop.
     */
    private land;
    /** A symmetry claim turned out false: the search stops, to be run again without it. */
    private refutes;
    private faultsAfter;
    /** A node at the depth bound: its edges, if every step from it lands on a known state; else it stays open. */
    private close;
    /** A world as properties see it: its layout, instance states, the world's variables, and whether anything is pending. */
    private tupleOf;
    /** Which liveness predicates hold in a new state: worked out once per tuple. */
    private judgeTruths;
    /**
     * The step properties a step breaks, of those not yet broken: from what is known of the same
     * step between the same tuples, else judged (judge.ts stepBreaks). A predicate that cannot be
     * evaluated holds. One that reads the event's place in the path is not kept: the place is
     * not in the key.
     */
    private stepBreaks;
    /** The search as a graph, for liveness (liveness.ts). */
    /**
     * What the states differ in, most first: for each actor's state field, how many values it
     * took across the explored worlds, and for each message, how many different ones were in
     * flight. A search too big to finish is usually one or two of these growing without bound.
     */
    variety(): Variety[];
    graph(): Graph;
    /** Steps as choices, with the world each is taken in when asked for (see Search.resolve). */
    resolve(steps: LassoStep[], worlds: boolean): Promise<Map<string, Resolved>>;
    /**
     * Whether a world that landed on a known state up to symmetry behaves as that state's world
     * does: the same next worlds, up to symmetry. Tested on the first `symmetryChecks` renamed
     * twins met (not on the very same world), in the order met.
     */
    private sameAsTwin;
    /**
     * The worlds one step away, each up to symmetry: renamed twins must agree on them.
     */
    private successorsKey;
    /** A new state from a root with symmetry: its plain fingerprint, and its vector while twin checks remain. */
    private keepForTwins;
    /** A node's world, replayed from its root. */
    private worldAt;
    /**
     * A fingerprint up to symmetry: the least, over the renamings, of the renamed world's
     * (instances and pending entries as renamed key lines, keys.ts), with the budget and memory
     * as they are, as world keys have them (keys.ts). Renamed twins have the same set of renamed
     * worlds, so the same least one. Also the world's own fingerprint (no renaming, no budget),
     * and its least without the budget, for twin checks.
     */
    private symmetricPrint;
    private renamed;
    private renamedState;
    private renamedPending;
    private lineId;
    /** The trace steps on the way to a node, from its root. */
    private trailOf;
    /** What `never` properties remember after a step on a trail: into the step, and which of them the path breaks. */
    private remember;
    /** A trace step as an event at a place in its path. Only the order of places is promised (TraceEvent.index). */
    private eventAt;
    /** The choices from each node's root to it, found again in real worlds. */
    paths(gids: number[]): Promise<Map<number, Choice[]>>;
    private pathTo;
    /** A named choice in a world: the same step, on the same message or timer. */
    private choiceIn;
    /** A choice's name: worked out once for shared choices, by its pending entry for the others. */
    private nameIn;
    private nameOf;
    private node;
    /** A node that stands only for a counterexample's last step (an error, a step property broken on the way to a known state): not a state. */
    private shadowNode;
    private breaks;
    /** The `always` properties a new state breaks: which fail is worked out once per tuple. */
    private judge;
    /**
     * Whether nothing can happen in a new world: only possible with nothing pending, so its
     * instances are all there is to it. Fewest faults, then first found.
     */
    private judgeStuck;
    /**
     * A world with just the instances, and as many (empty) pending entries as there are: all a
     * property sees of a world (worldView: the instances, and whether anything is pending).
     */
    private instancesOf;
    /** What the search's watcher sees of a state besides its world: what `never` properties remember. */
    private memoryText;
    private factsOf;
    /** What a choice does, to apply to the vector. */
    private step;
    /** A reset's effect in this vector: the messages in flight to the instance that its `drops` picks, removed as well. */
    private withDrops;
    /** A local step's effect: from the cache, or by running it through the engine once. */
    private effectOf;
    /** A step's name as a small number, for the step cache's key. */
    private stepIndex;
    /**
     * The steps that can take pending entry `id` (interned) when its receiver is in state `state`
     * (and the world's variables, when its `when`s read them; the plan is for both): a timer's own;
     * for a message, the steps on it whose `when` holds there (stepsTaking).
     */
    private takers;
    private argOf;
    /** The integers a step changed, from the worlds before and after it. */
    private effectFrom;
    /**
     * A vector with a step applied: the instance's new state, the budget, and what is pending.
     * The message chosen goes from where it is; any other removed message, its first copy
     * (copies are alike, but where they are decides the order of choices). New ones go last.
     */
    private applied;
    /** A root world's vector, with nothing spent. */
    private vectorOf;
    /** The world a vector stands for, for the engine: each pending entry's id is its place in the vector's pending part, from 1. */
    private materialize;
    private here;
    /** Each instance's own timers, oldest first, as a list id (from 1; 0 for none). */
    private timersOf;
    /**
     * Every choice from a vector, as `branches` gives them from its world, in the same order:
     * actions (with their inputs), then guards, instance by instance; then everything pending,
     * messages before timers, oldest first (pendingInOrder, which the vector keeps), each to
     * every step that can take it.
     */
    private choicesOf;
    /**
     * What an instance in one state can do: its actions whose `when` holds (with their inputs, if
     * those do not come from `examples`) and its guards that hold. Both read only its state and
     * its own variables, unless a `when` of its actor reads the world's (`variables`, interned).
     */
    private planOf;
    private readsWorldAt;
    /** Choices on pending entry `k`, shared: they name it by its place, and the step that takes it (`stepIndex`). */
    private fireAt;
    /** Whether a `when` of this actor's steps reads a variable of the world's, not only its instance's. */
    private whenReadsWorld;
    /** An action's choices when its inputs come from `examples`, which read the world: kept by its tuple. */
    private exampleChoices;
    /** An instance in one state, shared by every world it is in that way. */
    private stateId;
    /** As keys.ts pendingText writes it: symmetric fingerprints rename it. */
    private pendingId;
    /** The world's variables, interned: 0 for none set. */
    private variablesId;
    private variablesOf;
    private freshId;
}