import type { Trace, WorldView } from "./spec.ts";
import type { ActorInfo, Change, Event, InstanceState, Pending, Spec, StepInfo, World } from "./spec.ts";
import type { Delivery } from "./dsl.ts";
export interface Step {
    world: World;
    event: Event;
}
/** A spec bug found while running a step: an undeclared send, a missing actor. */
export declare class SpecError extends Error {
}
/**
 * How much a step works out besides the next world. A reader needs everything; the checker,
 * exploring, skips what it never reads and replays a counterexample in full afterwards.
 */
export interface StepOptions {
    /** The event's changes and sentence (true). */
    explain?: boolean;
    /** Which `always` invariants the world after it breaks (true). */
    invariants?: boolean;
    /** Filled in with what the step depended on, for the checker's step cache (integer.ts). */
    observe?: Observation;
}
/** What a step depended on and touched, besides its argument: what decides whether its effect can be reused. */
export interface Observation {
    /** It read another instance's state (`the`, `all`, `from`). */
    others: boolean;
    /** It used a counter every instance shares (`fresh`, `random`). */
    counters: boolean;
    /** It read or set one of the world's model variables. */
    variables: boolean;
    /** It reset its instance, dropping the messages on their way to it that this picks. */
    drops?: (delivery: Delivery) => boolean;
    /** It read or changed its own instance: its state, its own variables or its timers. */
    own: boolean;
}
export declare function observation(): Observation;
/** A message in flight as a step sees it (`ctx.delivery`, a reset's `drops`); `onRead` hears whose state is read. */
export declare function deliveryIn(spec: Spec, world: World, p: Extract<Pending, {
    kind: "deliver";
}>, onRead?: (id: string) => void): Delivery;
/** A world with every singleton spawned. */
export declare function startWorld(spec: Spec, seed?: number): Step[];
export declare function emptyWorld(seed?: number): World;
export declare function actorNamed(spec: Spec, name: string): ActorInfo;
export declare function instanceById(world: World, id: string): InstanceState;
/**
 * What is pending, in the order the system takes it when nobody interferes: messages in the
 * order they were sent, then timers in the order they were set. Left alone, timeouts are
 * slower than the network (RFD0004). Any of them may still go next.
 */
export declare function pendingInOrder(world: World): Pending[];
/** What the system does next when nobody interferes: the first of pendingInOrder. */
export declare function nextLeftAlone(world: World): Pending | undefined;
/** What can happen next: actions people can take, guarded transitions that hold, and what is pending. */
export declare function choices(spec: Spec, world: World): {
    actions: {
        instance: string;
        key: string;
        inputs: string[];
    }[];
    guards: {
        instance: string;
        key: string;
    }[];
    pending: Pending[];
};
/**
 * Whether a step's `when` holds for an instance in a world: it reads the instance's state and
 * the model variables the step uses. One that throws does not hold, except for reading a
 * variable the step does not list in `uses`, which is a spec error.
 */
export declare function whenHolds(spec: Spec, world: World, instance: InstanceState, step: StepInfo, own?: boolean): boolean;
/** A variable's value for an instance: its own for an `each` variable, else the world's; absent, its initial value. */
export declare function variableIn(spec: Spec, world: World, instance: InstanceState | undefined, name: string): unknown;
export declare function spawn(spec: Spec, world: World, actorName: string, label: string): Step;
/** A person takes an action on an instance. */
export declare function act(spec: Spec, world: World, instanceId: string, key: string, inputs?: Record<string, unknown>, how?: StepOptions): Step;
/**
 * The steps that can take a pending entry now: a timer's own step; for a message, each step on
 * it whose `when` holds, in the order declared (RFD0012).
 */
export declare function stepsTaking(spec: Spec, world: World, pending: Pending): string[];
/** The step a message goes to when the system is left alone: the fair one of the steps on it. */
export declare function leftAloneStep(actor: ActorInfo, message: string): string | undefined;
/** Deliver a pending message to one of the steps on it (the one left alone takes, unless named), or fire a pending timer. */
export declare function fire(spec: Spec, world: World, pendingId: number, step?: string, how?: StepOptions): Step;
/** Run an internal transition whose `when` guard holds. */
export declare function guard(spec: Spec, world: World, instanceId: string, key: string, how?: StepOptions): Step;
/** The world as predicates and examples see it; `onRead` hears whose state they read. */
export declare function worldView(spec: Spec, world: World, onRead?: (id: string) => void): WorldView & {
    instance: (i: InstanceState) => {
        id: string;
        label: string;
        state: unknown;
    };
};
export declare function violatedAlways(spec: Spec, world: World): string[];
export declare function holdsIn(spec: Spec, world: World, predicate: (world: WorldView) => boolean): boolean;
export declare function traceView(events: readonly Event[]): Trace;
/** Whether a delivery went to the step the message goes to left alone, rather than to another step on it. */
export declare function tookLeftAlone(spec: Spec, event: Pick<Event, "actor" | "key" | "message">): boolean;
/** A delivery in words: its message's name, and the step that took it when that is not the one left alone ("charge → chargeLost"). */
export declare function deliveryName(spec: Spec, event: Pick<Event, "actor" | "key" | "message">): string;
export declare function messageName(spec: Spec, key: string): string;
/** A deterministic, readable stand-in for a hash. */
export declare function hashOf(value: string): string;
/**
 * A deep copy. States and payloads are plain data, so plain objects, arrays, sets, maps and
 * dates are copied by hand, which is much faster than structuredClone; anything else falls
 * back to it.
 */
export declare function clone<T>(value: T): T;
/** Deep-freeze a value the engine is done changing; it may then be shared between worlds. */
export declare function freeze<T>(value: T): T;
export declare function notPlain(where: string): string;
/** Changes from `before` to `after`, by path. Arrays and leaves are compared whole. */
export declare function diff(instance: string, before: unknown, after: unknown, path?: string): Change[];