import { type Spec, type World } from "../spec/index.ts";
import type { Bounds, Root, StopReason, Watch } from "./explore.ts";
import { type Verdicts } from "./judge.ts";
import { type Graph, type LassoStep } from "./liveness.ts";
import { type Choice } from "./steps.ts";
import { type WalkResult } from "./walk.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;
    /** Whether the search ran out of worlds before the depth bound: it has explored every world reachable. */
    complete: boolean;
    /** Scratch for pick: each option's kind. */
    private kinds;
    /** Each root's vector, where random runs start. */
    private rootVectors;
    /** Whether a new world was found at the depth bound, and not expanded. */
    /** Where `run` goes on from, if it stopped at a deadline. */
    private resume;
    /** For liveness: the nodes at the depth bound, whose edges are added at the end if they can be. */
    private open;
    /** 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;
    /** Whether any message is ordered: only then do vectors have channels (`queueLanes`). */
    private readonly ordered;
    /** By interned message: its channel (sender and receiver), interned, if it is ordered; -1 if not. */
    private channels;
    private channelIds;
    /** By actor, then step index: whether the step may take an ordered message out of order. */
    private outOfOrder;
    /** 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;
    /** What a step adds to `never` properties' memory (remember), by memory and then by trace step. */
    private memorySteps;
    /** Fires' fairness (fairOf), by step index and then by interned message or timer; null for none. */
    private fairFires;
    /** Fires' names (nameIn), by step index and then by interned message or timer. */
    private fireNames;
    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.
     */
    /** 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.
     */
    /** Tuples, interned: for each layout and whether anything is pending, a trie over the instance states, then the variables. */
    private tupleRoots;
    private tupleCount;
    /** By parent tuple: its children's tuples (childTuple). */
    private tupleSteps;
    /** 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;
    /** For each `everyStep` property, what it read and what it answered (`stepAnswer`); undefined for one that is not a function of what it reads. */
    private stepMemos;
    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;
    /** Steps that drew a random number (`ctx.random()`): each got the one value its seed gives, not every value. */
    readonly drew: Set<string>;
    /** `never` properties that remember the whole path (nevers.ts): those found to vary, in an earlier search. */
    wholePath: ReadonlySet<string>;
    /** `never` properties whose shape varied in this search: it stopped, to be run again with them in `wholePath`. */
    readonly varied: Set<string>;
    /** How each `never` property read the first path it was judged on. */
    private shapes;
    /** Each root's steps before it, as traces see them: a scenario's, none for the initial world. */
    private rootTrails;
    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;
    /**
     * Breadth first, until the depth bound, a limit, or `deadline` (the time limit's, by default).
     * Stopped by a deadline, it can be run again, and goes on from where it was.
     */
    run(deadline?: number): void;
    /**
     * Whether a world at the depth bound leads somewhere the search has not been: a step to a new
     * world, an error not met yet, or a step that would break a property. Any of them, and the
     * bound has cut a path off, so what held is not proved.
     */
    private goesFurther;
    /** One node per distinct root: judged, and the frontier to start from. */
    private start;
    /**
     * Random runs (walk.ts) on the search's vectors and caches: the same runs, picked by the same
     * seeds and weights from the same choices in the same order, judged as judge.ts judges them,
     * in a fraction of the time of running each step through the engine. A run records its
     * choices by name, found again in real worlds only for what it reports.
     */
    walk(v: Verdicts, until: number): WalkResult;
    /** A run's next choice (walk.ts pick): mostly the system's fair steps, some people, rarely an unfair step. */
    private pick;
    /** 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;
    /**
     * The tuple of a vector with one instance's state replaced (`slot`, or -1 for none), these
     * variables, and something pending or not. Tuples are interned in a trie of integers, one
     * level for each part: a search makes a tuple for nearly every step, and a key written out
     * as text was a large part of its time.
     */
    private tupleWith;
    /**
     * A child's tuple, from its parent and the step, without making the child: its parent's, but
     * for the stepping instance's state, the variables, and whether anything is pending. Kept by
     * those for each parent tuple.
     */
    private childTuple;
    /** 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;
    /**
     * One `everyStep` property's answer for a step, by what the property reads. Most read a few
     * instances' states before and after, not the whole world: two steps that agree on those have
     * one answer. So each property keeps a tree of what it read, in the order it read it, with
     * the answer at the end of each path: a step is looked up by reading the same things from its
     * vectors, and the property runs only for a path not walked before. `keep` is false for an
     * answer that depends on where in its path the step is (`event.index`), which no step shares.
     */
    private stepAnswer;
    /** 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, and the properties each breaks: renamed twins
     * must agree on them. The claim is about the properties as much as the steps: one that names
     * an instance ("B never wins") tells twins apart, and judged on one of each merged pair it
     * would never be judged on the worlds where it breaks.
     */
    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;
    /**
     * For each renaming, the two lanes of a world's fingerprint but for its timers and memory:
     * the counters and variables as they are, and each state and message as the renaming has it.
     * Sums, so a child's follow from its parent's by what the step changed (`childLanes`).
     */
    private symmetricLanes;
    /** A child's lanes from its parent's: what the step changed, taken out and put back, for each renaming. */
    private childLanes;
    /** What a state adds to lane 1 under a renaming, which also fills what it adds to lane 2 (`r.state2`). */
    private stateLane1;
    /** As `stateLane1`, for a message in flight. */
    private messageLane1;
    private renamed;
    private renamedState;
    private renamedPending;
    private lineId;
    /** The trace steps on the way to a node, from its root. */
    private trailOf;
    /** Notes how each `never` property read a path: one that reads this path another way than the first has varied. */
    private shaped;
    private lazyTrail;
    /**
     * What `never` properties remember after a step: into the step, and which of them the path
     * breaks. Paths that remember the same are one state, so what a step adds depends only on the
     * memory before it and the step: worked out on the trail once for each, then kept.
     */
    private remember;
    /**
     * A choice's fairness (fairness.ts), kept: a fire's depends only on its step and what it takes
     * (interned), a guard's on the choice, which plans share.
     */
    private fairOf;
    /** The fair steps possible in a world, among its options, by identity (fairness.ts fairStepsIn). */
    private fairStepsIn;
    /** 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;
    /** Named choices from a root (nameIn), found again in real worlds. */
    private choicesNamed;
    /** 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;
    /** The `always` properties that fail in a world: worked out once per tuple. */
    private failingAt;
    /**
     * 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: of the messages in flight, those on their way to the
     * instance that its `drops` picks are removed, and those the reset changes (a call the instance
     * made, an answer on its way to it: afterReset) are replaced by what they become.
     */
    private withReset;
    /** 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;
    /** An interned message's channel, if it is ordered: its sender and receiver, interned; -1 if not. */
    private channelOf;
    /** Whether an actor's step (by index) may take an ordered message with others ahead of it. */
    private takesOutOfOrder;
    /**
     * What the order of ordered messages adds to a fingerprint's two lanes: for each channel, a
     * hash of its messages in the order they are in the vector, which is the order they were
     * sent; summed over the channels, which are in no order. `name` is what stands for a message:
     * its intern id, or its renamed key line under symmetry.
     */
    private queueLanes;
    /** A vector's fingerprint from scratch, with its channels' order. */
    private printOf;
    /**
     * A child's fingerprint (childPrint). With ordered messages, from the child's vector, as the
     * order on a channel changes with every step on it.
     */
    private childPrint;
    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;
    /** The slot of the instance an interned message or timer is for. */
    private slotIn;
    /** 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;
}