import { type Fields, type Shaped, type TypeOf } from "./schema.ts";
import type { Fairness, Spec } from "./spec.ts";
/** Code a step stands for: `path#symbol` or `path:start-end`. */
export type Source = `${string}#${string}` | `${string}:${number}-${number}`;
export type Tone = "request" | "reply" | "refused" | "stream";
/** What an actor is drawn as. */
export type Icon = "person" | "people" | "phone" | "laptop" | "desktop" | "browser" | "server" | "cloud" | "database" | "shield" | "key" | "lock" | "terminal" | "robot" | "queue" | "folder" | "file" | "sheet" | "globe" | "gear" | "camera" | "video" | "mail" | "bell" | "clock" | "cpu" | "box" | "plug" | "wifi" | "chat" | "router" | "storage" | "code" | "pipeline" | "eye" | "card";
/**
 * Where a zone sits on the playground's map. Positions are still computed; these say what
 * matters to the picture: left to right, which zone is the region everything hangs off, and
 * how its instances line up.
 */
export interface ZonePlace {
    /** Left to right, from 0. Zones without one follow the direction messages flow. */
    column?: number;
    /** Draw it as a tinted region, as for a service. By default, a zone holding a singleton is one. */
    region?: boolean;
    /** Where its instances sit in the column: at the top, the middle (default), or the bottom. A region's start at the top. */
    align?: "start" | "center" | "end";
    /** How its instances line up: one under another (default), side by side, in a grid, or around a ring (peers in a cluster). */
    arrange?: "stack" | "row" | "grid" | "ring";
}
/** Where an actor's instances sit within their zone. */
export interface ActorPlace {
    /** Instances of actors with a lower order come first; within an order, by label, so "Studio app" and "Studio daemon" sit together. */
    order?: number;
    /** Sit on the zone's border rather than inside it, like a gate everything passes through. */
    edge?: "left" | "right";
}
/**
 * What a node is drawn as. By default it follows the icon: a service (cloud, server,
 * database…) is a circle with its name inside, a device (phone, laptop…) a rounded square,
 * and an actor on a zone's edge a gate.
 */
export type Shape = "circle" | "device" | "gate" | "card";
/** How things are going: colours a node, a row, or a link. */
export type Mood = "ok" | "warn" | "bad" | "busy" | "off" | "info";
/** One line of an actor's state, shown as structure: a host, an account, a file. */
export interface Row {
    label: string;
    detail?: string;
    mood?: Mood;
    /** Rows with the same group are boxed together under it: "Alice's account". */
    group?: string;
    /** An instance (id or label) this row belongs to; its group, and the row if it has no mood, take its colour. */
    owner?: string;
}
/**
 * Something an instance holds that a person can pick up and drop on another node, such as a
 * pairing code or a signed-in person. Dropping it runs the target's action whose input
 * `accepts` this kind, with `value` as that input.
 */
export interface Token {
    kind: string;
    value: string | number | boolean;
    /** What the chip shows; the value by default. */
    label?: string;
    mood?: Mood;
}
export interface Display<S> {
    icon?: Icon;
    shape?: Shape;
    /** Labels for instances added in the playground, in order: "Alice", "Bob". */
    names?: string[];
    /** A few words under the name: "connected", "not linked", "watching Studio". */
    status?: (state: Readonly<S>) => string;
    mood?: (state: Readonly<S>) => Mood;
    rows?: (state: Readonly<S>) => Row[];
    /**
     * Whose this is, as an instance id or label: a Mac belongs to the person whose account
     * it is linked to. It then wears that instance's colour; with null it stays neutral.
     */
    owner?: (state: Readonly<S>) => string | null;
    /** Things to drag onto other nodes, floating beside this one. */
    tokens?: (state: Readonly<S>, self: {
        id: string;
        label: string;
    }) => Token[];
}
/** A live connection an instance holds: a socket, a session, a subscription. */
export interface Link {
    /** An instance id, an instance label, or the name of a singleton actor. */
    to: string;
    /** What it is: "websocket", "session"; links of one kind share a style. */
    kind?: string;
    label?: string;
    mood?: Mood;
    style?: "solid" | "dashed" | "dotted";
    /** The label of a row on the target to end at, so the line meets what it connects to. */
    row?: string;
}
export interface Message<Id extends string = string, P = unknown> {
    readonly kind: "message";
    /** `Charge`, unique within a spec. */
    readonly id: Id;
    /** The engine's key: `message:Charge`. */
    readonly key: `message:${Id}`;
    /** In everyday words: "charge". */
    readonly name: string;
    /** The protocol it travels over: "https", "websocket", "unix socket". */
    readonly over?: string;
    readonly tone: Tone;
    /** A reply to it carries the request it answers (`ctx.delivery.answers`); see `MessageOptions`. */
    readonly correlate: boolean;
    readonly schema: Fields;
    readonly seq: number;
    /** Phantom: the payload type. */
    readonly __payload?: P;
}
export type AnyMessage = Message<string, any>;
/** A message's payload type. */
export type PayloadOf<M> = M extends Message<string, infer P> ? P : never;
interface MessageOptions {
    /** In everyday words, shown in traces: "pairing code". By default, the id in words. */
    name?: string;
    over?: string;
    tone?: Tone;
    /**
     * A reply to it (`ctx.reply`) carries the request it answers, which the step handling the
     * reply reads as `ctx.delivery.answers`: how a library knows which call a lost reply fails.
     * Replies to different requests are then different messages in flight, even with the same
     * payload.
     */
    correlate?: boolean;
}
/** A message, with its payload's schema: `defineMessage("Charged", { payment: String }, { tone: "reply" })`. */
export declare function defineMessage<const Id extends string, F extends Fields = {}>(id: Id, schema?: F, options?: MessageOptions): Message<Id, TypeOf<F>>;
export interface Actor<S = any, A = any> {
    readonly name: string;
    /** Phantoms. */
    readonly __state?: S;
    readonly __actions?: A;
}
/** An actor's state type. */
export type StateOf<X> = X extends Actor<infer S, any> ? S : never;
/** An actor's actions: each action's key, to its inputs' types. */
export type ActionsOf<X> = X extends Actor<any, infer A> ? A : never;
export interface Instance<S, A> {
    readonly id: string;
    readonly label: string;
    readonly state: Readonly<S>;
    /** Phantom. */
    readonly __actions?: A;
}
/** The world as properties and examples see it. */
export interface World {
    /** Nothing is in flight: no message on its way and no timer set. "Once quiet, …" is how to say "in the end". */
    readonly quiet: boolean;
    all<X extends Actor<any, any>>(actor: X): Instance<StateOf<X>, ActionsOf<X>>[];
    the<X extends Actor<any, any>>(actor: X): Instance<StateOf<X>, ActionsOf<X>>;
    /** A model variable's value (RFD0012); for one defined for each instance of an actor, that instance's. */
    get<T>(variable: Variable<T>, instance?: Instance<any, any>): T;
}
/**
 * What a step can do. A step's `ctx` sends only what its `sends` lists; a helper shared by steps
 * takes a plain `Ctx`, and a step passes its own.
 */
export interface Ctx<Sends extends AnyMessage = AnyMessage> {
    /** This instance's id and label, and the instance itself, to send to yourself. */
    readonly id: string;
    readonly label: string;
    readonly self: Instance<unknown, unknown>;
    the<X extends Actor<any, any>>(actor: X): Instance<StateOf<X>, ActionsOf<X>>;
    all<X extends Actor<any, any>>(actor: X): Instance<StateOf<X>, ActionsOf<X>>[];
    /**
     * Send a message; `text` says, for this event only, what it means. `answers` marks it as
     * answering a request, as a reply does, so a reset of its receiver drops it in flight.
     */
    send<M extends Sends>(to: Instance<any, any> | {
        id: string;
    }, message: M, payload: PayloadOf<M>, options?: string | SendOptions): void;
    /**
     * Set one of this actor's timers: from now on it may fire at any moment, before or after
     * anything else pending. Setting it again replaces it.
     */
    start(timer: string): void;
    cancel(timer: string): void;
    /** A fresh id: `cred-1`, `cred-2`. */
    fresh(prefix: string): string;
    /** A deterministic, readable stand-in for a hash: `hash:…`. */
    hash(value: string): string;
    /** A seeded random number in [0, 1). */
    random(): number;
    /** Explain this event when the step's description is not enough. */
    note(text: string): void;
    /** A model variable the step lists in `uses`: the world's, or this instance's own for an `each` one. */
    get<T>(variable: Variable<T>): T;
    /** Change a model variable the step lists in `uses`. */
    set<T>(variable: Variable<T>, value: T): void;
    /**
     * Start this instance again, as a crash and restart does: its state becomes its initial
     * state with the fields in `keeps` carried over, and its timers are cancelled. Messages on
     * their way to it stay, but those `drops` picks, which went with its memory (a failure
     * that would have thrown in code that is no longer running).
     */
    reset(options?: {
        keeps?: readonly string[];
        drops?: (delivery: Delivery) => boolean;
    }): void;
}
/** What `send` takes after the payload, besides a text: the request the message answers. */
export interface SendOptions {
    text?: string;
    answers?: {
        message: string;
        payload: unknown;
    };
}
/** The message a step on one is handling, as it was in flight. */
export interface Delivery {
    /** Its key: `message:Charge`. */
    readonly message: string;
    readonly from: Instance<any, any>;
    readonly payload: unknown;
    /** For a reply, or a message sent as answering one: the request it answers. */
    readonly answers?: {
        message: string;
        payload: unknown;
    };
}
/** In a step `on` a message, `reply` answers the sender. */
export interface ReplyCtx<Sends extends AnyMessage = AnyMessage> extends Ctx<Sends> {
    readonly from: Instance<any, any>;
    reply<M extends Sends>(message: M, payload: PayloadOf<M>, text?: string): void;
    /** The message being handled, as it was in flight. */
    readonly delivery: Delivery;
    /**
     * Put the message being handled back in flight as it was; twice, and it is there twice. With
     * `as`, it goes on as another message (declared in `sends`), still from its sender: how a lost
     * reply becomes its call's failure.
     */
    forward<M extends Sends>(as?: {
        message: M;
        payload: PayloadOf<M>;
    }): void;
}
/** What a step receives: a message's payload, or nothing for a timer or a guard. */
type Received<On> = On extends Message<string, infer P> ? P : undefined;
type CtxOn<On, Sends extends AnyMessage> = On extends AnyMessage ? ReplyCtx<Sends> : Ctx<Sends>;
/**
 * A step of an actor, named by its key in `transitions`. It is one of three kinds: `on` a
 * message; a timer of the same name, started with `ctx.start` (say when the
 * code fires it with `after`); or a guarded step, possible whenever `when` holds.
 */
export interface StepDef<S, On, Sends extends AnyMessage> {
    /** The message this step reacts to. */
    on?: On;
    /**
     * For a guarded step: it can run whenever this holds. For a step on a message: it can take
     * the message only while this holds.
     */
    when?: (state: Readonly<S>, model: ModelView) => boolean;
    /** The model variables it reads or writes (its `when` too), as `sends` lists messages (RFD0012). */
    uses?: readonly Variable<any>[];
    /** Strings the core keeps and never reads, for libraries and reports: a fault is tagged `fault`. */
    tags?: readonly string[];
    /** Parts that bound it, from a library: `with: [atMost(repeats)]`. See `Part`. */
    with?: readonly Part[];
    /**
     * For a timer, when the code fires it, in words: "10 minutes", "after three missed
     * heartbeats". Shown to readers; it has no effect on when it can fire.
     */
    after?: string;
    /** In everyday words, what the step does, in general. */
    description: string;
    /**
     * The code this step stands for, as an ordered trail. Leave it out while the code does not
     * exist yet; add it as the code appears.
     */
    sources?: Source[];
    starts?: string[];
    run(state: S, received: Received<On>, ctx: CtxOn<On, Sends>): void;
    /** What happened this time, as the timeline says it, from the state after the step: "Made code 19YP for alice". */
    say?: (state: Readonly<S>, received: Received<On>) => string;
    /** Housekeeping a reader need not watch, such as a heartbeat: views fold it away. The checker still explores it. */
    routine?: boolean;
    /**
     * Fairness (RFD0006). A delivery, timer or guard that stays possible from some point on
     * eventually happens ("weak", the default); "strong": one possible again and again eventually
     * happens; false: it may never happen.
     */
    fair?: Fairness | false;
}
/** What an action input holds: String, Number, Boolean, or `oneOf(…)` for a choice. */
export type InputType = StringConstructor | NumberConstructor | BooleanConstructor | Shaped<string | number | boolean>;
declare const INPUT: unique symbol;
/** Made by `input`: an input's type with examples. */
export interface InputDef<T = InputType> {
    readonly [INPUT]: true;
    type: T;
    examples?: ((world: World) => ValueOf<T>[]) | readonly ValueOf<T>[];
    accepts?: string;
}
type ValueOf<T> = T extends InputDef<infer U> ? ValueOf<U> : TypeOf<T>;
/** The values an action's inputs take, from their declared types. */
export type InputsOf<I> = {
    [K in keyof I]: ValueOf<I[K]>;
};
/**
 * An action input with examples. `examples` are what the playground offers and the checker
 * tries; `accepts` names a token kind that can be dropped on the node to fill this input.
 */
export declare function input<const T extends InputType>(type: T, options?: {
    examples?: ((world: World) => ValueOf<T>[]) | readonly ValueOf<T>[];
    accepts?: string;
}): InputDef<T>;
export interface ActionDef<S, I> {
    /** The button: "Paste a pairing code". */
    label: string;
    description: string;
    sources?: Source[];
    sends?: readonly AnyMessage[];
    starts?: string[];
    /** `{ code: String, vote: oneOf("yes", "no") }`, or `input(type, { examples })` for examples. */
    inputs?: {
        [K in keyof I]: I[K];
    };
    /** When set, the action is offered only while this holds. */
    when?: (state: Readonly<S>, model: ModelView) => boolean;
    /** The model variables it reads or writes (its `when` too), as `sends` lists messages (RFD0012). */
    uses?: readonly Variable<any>[];
    /** Strings the core keeps and never reads, for libraries and reports. */
    tags?: readonly string[];
    /** Parts that bound it, from a library: `with: [atMost(repeats)]`. See `Part`. */
    with?: readonly Part[];
    run(state: S, inputs: InputsOf<I>, ctx: Ctx): void;
    /** What happened this time, as the timeline says it, from the state after the step. */
    say?: (state: Readonly<S>, inputs: InputsOf<I>) => string;
    /** Housekeeping a reader need not watch, such as a heartbeat: views fold it away. The checker still explores it. */
    routine?: boolean;
}
/**
 * What a library adds to a step without knowing its state (RFD0012): the variables it uses, a
 * condition on them, and what it does to them first. A step `with: [atMost(repeats)]` is
 * possible only while every part's `when` and its own hold, and runs every part's `run`, in
 * order, before its own.
 */
export interface Part {
    uses?: readonly Variable<any>[];
    tags?: readonly string[];
    when?: (model: ModelView) => boolean;
    run?: (ctx: Ctx) => void;
}
/** Made by `defineVariable`: state of the model rather than of an actor (RFD0012). */
export interface Variable<T> {
    readonly kind: "variable";
    readonly name: string;
    readonly initial: T;
    /** Whether every instance of the actor that uses it has its own value. */
    readonly each: boolean;
}
/** The model's variables as a guard reads them: `when: (state, model) => model.get(faults) > 0`. */
export interface ModelView {
    get<T>(variable: Variable<T>): T;
}
/**
 * State that belongs to the model rather than to an actor, as a TLA+ variable that no process
 * owns: a budget of faults, a bound on retries, ghost history for a property. With `each: true`,
 * every instance of the actor whose steps use it has its own (one actor uses it, then). A step that reads or writes one lists it in `uses`, and
 * reads it with `ctx.get` and writes it with `ctx.set`; properties read it with `w.get`. It is
 * for the model's bookkeeping, not for actors to share what the system does not share.
 */
export declare function defineVariable<T>(name: string, initial: T, options?: {
    each?: boolean;
}): Variable<T>;
/**
 * A variable of one step, named by it when its actor is read: `Client.pay`. For libraries that
 * bound a step without asking for a name (`atMost`); one step uses it.
 */
export declare function stepVariable<T>(initial: T, options?: {
    each?: boolean;
}): Variable<T>;
export interface Zone {
    readonly name: string;
}
export declare function defineZone(def: {
    name: string;
    description?: string;
    place?: ZonePlace;
}): Zone;
export interface Limit {
    readonly name: string;
    readonly value: number;
}
export declare function defineLimit(def: {
    name: string;
    value: number;
    unit?: string;
    sources?: Source[];
}): Limit;
/**
 * Actors shown as one thing: the relay, rather than its Worker and Durable Objects. A list
 * of singletons is one node. A record groups instances of other actors by label: with
 * `{ app: App, daemon: Axod }`, "Studio app" and "Studio daemon" are one "Studio".
 */
export interface GroupDef {
    name: string;
    actors: Actor<any, any>[] | Record<string, Actor<any, any>>;
    description?: string;
    icon?: Icon;
    shape?: Shape;
    /** Shown as one node to begin with (true); it opens on demand. */
    collapsed?: boolean;
    /** Names for instances added in the playground, for a record group: "Studio", "iMac". */
    names?: string[];
}
export interface Group {
    readonly name: string;
}
export declare function defineGroup(def: GroupDef): Group;
/** A link to an actor, or to an instance by id or label. */
export interface ActorLink extends Omit<Link, "to"> {
    /** An actor (a singleton), or an instance id or label. */
    to: Actor<any, any> | string;
}
interface ActorDef<S, A, O, Sn> {
    name: string;
    /** In everyday words, what this is. */
    description?: string;
    zone: Zone;
    /** One instance, spawned with the world. */
    singleton?: boolean;
    /** Where its instances sit within the zone, on the playground's map. */
    place?: ActorPlace;
    initialState: (ctx: {
        id: string;
        label: string;
    }) => S;
    /**
     * Instances are interchangeable: the spec only compares their ids and labels for equality,
     * never orders them or computes with them. The checker then treats "Alice, then Bob" and
     * "Bob, then Alice" as one state. It tests the claim as it goes and says if it is false.
     */
    symmetric?: boolean;
    display?: Display<NoInfer<S>>;
    /** The live connections an instance holds now, from its own state. */
    links?: (state: Readonly<NoInfer<S>>, self: {
        id: string;
        label: string;
    }) => ActorLink[];
    actions?: {
        [K in keyof A]: ActionDef<NoInfer<S>, A[K]>;
    };
    /** Its steps, by name: `charge: { on: Charge, … }`, `retry: { after: "10 seconds", … }`, `drain: { when: …, … }`. */
    transitions?: {
        [K in keyof O]: StepDef<NoInfer<S>, O[K], Sn[K & keyof Sn] & AnyMessage>;
    } & {
        [K in keyof Sn]: {
            sends?: readonly Sn[K][];
        };
    };
}
/** An actor: a kind of process, with its state and its steps. */
export declare function defineActor<S, A = {}, O = {}, Sn = {}>(def: ActorDef<S, A, O, Sn>): Actor<S, A>;
export interface TraceEvent {
    readonly index: number;
    readonly actor: string;
    readonly key: string;
    /** Whether this event is `actor` taking the step or action named `step`. */
    is(actor: Actor<any, any>, step: string): boolean;
    /** Whether this event sent `message`. */
    replied(message: AnyMessage): boolean;
    sent(message: AnyMessage): boolean;
}
export interface Trace {
    readonly events: readonly TraceEvent[];
    count(predicate: (event: TraceEvent) => boolean): number;
    some(predicate: (event: TraceEvent) => boolean): boolean;
}
/** A rule of the design (RFD0010): a part that exists to keep properties true. */
export interface Rule {
    readonly name: string;
    readonly description: string;
    /** Whether the rule is in the design being run: true as written, false in a variant without it. */
    readonly on: boolean;
}
/**
 * A rule of the design: a part that exists to keep properties true (RFD0010). Read `rule.on`
 * where it applies, in steps, guards and properties; properties that need it say so with
 * `needs: [rule]`. It is on in the spec as written, and off in the variant without it
 * (`feynman check --without name`).
 */
export declare function defineRule(name: string, def: {
    description: string;
}): Rule;
export type PropertyDef = ({
    description: string;
    always: (world: World) => boolean;
}
/** Of every step: the world before it, the world after, and the event. */
 | {
    description: string;
    everyStep: (before: World, after: World, event: TraceEvent) => boolean;
} | {
    description: string;
    never: (trace: Trace) => boolean;
}
/** From the start, this happens at least once. */
 | {
    description: string;
    eventually: (world: World) => boolean;
}
/** Every time `whenever` holds, `then` holds then or later. */
 | {
    description: string;
    leadsTo: {
        whenever: (world: World) => boolean;
        then: (world: World) => boolean;
    };
}
/** This keeps happening, forever. */
 | {
    description: string;
    infinitelyOften: (world: World) => boolean;
}
/** From some point on, this always holds. */
 | {
    description: string;
    eventuallyAlways: (world: World) => boolean;
}) & {
    /**
     * The rules of the design this property needs (RFD0010): without any one of them, it should
     * break. `check` checks the design without each rule, and fails when the property still holds.
     */
    needs?: readonly Rule[];
    /**
     * A known bug: the property states what should hold, the system does not do it yet, and
     * `check` expects it broken. Say why, or link the issue. Check reports it, but it does not
     * fail; once the property holds, check fails until `known` is removed.
     */
    known?: string;
};
export interface Property {
    readonly id: string;
}
/**
 * A property: of every state (`always`), every step (`everyStep`), every path so far (`never`),
 * or of every fair infinite behaviour (`eventually`, `leadsTo`, `infinitelyOften`,
 * `eventuallyAlways`). See RFD0006 for what each means, and fairness.
 */
export declare function defineProperty(id: string, def: PropertyDef): Property;
type ActionInputs<A, K extends keyof A> = InputsOf<A[K]>;
type NoInputs<A> = {
    [K in keyof A & string]: keyof A[K] extends never ? K : never;
}[keyof A & string];
type ActionsWithInputs<A> = Exclude<keyof A & string, NoInputs<A>>;
/** Actions that take no inputs; when there are none, a message saying what to do. */
type ActionsWithoutInputs<A> = [NoInputs<A>] extends [never] ? `every action of this actor takes inputs (${ActionsWithInputs<A>}); pass them as the third argument` : NoInputs<A>;
/**
 * The world a scenario starts in, set up rather than reached by events: a repository already
 * pushed to, a cluster with a leader. Each instance starts in its `initialState` with the
 * fields given here laid over it. The flow starts after it. It is a claim that the system
 * gets there; the checker explores from here too, and reports a property this world breaks.
 */
export interface Setup {
    /** A singleton's state at the start: these fields, over its `initialState`. */
    set<X extends Actor<any, any>>(actor: X, state: Partial<StateOf<X>>): void;
    /**
     * An instance there from the start, rather than spawned in the flow: its `initialState`,
     * with these fields over it. In `run`, find it with `s.the(Actor)` or `s.all(Actor)`.
     */
    spawn<X extends Actor<any, any>>(actor: X, label: string, state?: Partial<StateOf<X>>): void;
}
/** What a scenario's `setup` receives: a shared setup is a function of it. */
export type SetupWorld = Setup;
export interface Script {
    spawn<X extends Actor<any, any>>(actor: X, label: string): Instance<StateOf<X>, ActionsOf<X>>;
    /** The one instance of an actor (a singleton, or the only one spawned). */
    the<X extends Actor<any, any>>(actor: X): Instance<StateOf<X>, ActionsOf<X>>;
    all<X extends Actor<any, any>>(actor: X): Instance<StateOf<X>, ActionsOf<X>>[];
    /** Take an action that has no inputs. */
    act<S, A>(who: Instance<S, A>, action: ActionsWithoutInputs<A>, inputs?: Record<string, never>): void;
    /** Take an action with its inputs. */
    act<S, A, K extends ActionsWithInputs<A>>(who: Instance<S, A>, action: K, inputs: ActionInputs<A, K>): void;
    /**
     * Leave the system alone until nothing is pending: every message in flight arrives, in the
     * order it was sent, and when none is, the timer set first fires. With `until`, stop as soon
     * as it holds (before anything happens, if it holds already), to step in at that moment:
     * `s.settle({ until: (w) => w.the(Store).state.saved })`, then `s.step(worker, "crash")`. It is an
     * error if the system settles, or runs SETTLE_LIMIT events, without getting there.
     */
    settle(options?: {
        until: (world: World) => boolean;
    }): void;
    /** Fire one of an instance's timers now, ahead of what is in flight. */
    fire(who: Instance<any, any>, timer: string): void;
    /**
     * Deliver a message in flight to `who` now, ahead of the rest: the oldest of `message`, or
     * the oldest carrying `payload` when given, to its fair step. Any message may overtake another.
     */
    deliver<M extends AnyMessage>(who: Instance<any, any>, message: M, payload?: PayloadOf<M>): void;
    /**
     * Take one of `who`'s steps by name: a guarded step whose `when` holds now, or a step on a
     * message, which takes the oldest such message in flight to `who` (the oldest carrying
     * `payload`, if given), as `deliver` picks it.
     */
    step(who: Instance<any, any>, step: string, payload?: unknown): void;
    /** The world now, to read state between steps. */
    readonly world: World;
}
export interface Scenario {
    readonly name: string;
}
/**
 * A flow a reader should see, scripted: `run` replays it event by event. `setup`, when given,
 * sets the world it starts in (see Setup), for a scenario that begins after some history: a
 * second push, a fetch after pushes.
 */
export declare function defineScenario(name: string, def: {
    description?: string;
    setup?(setup: Setup): void;
    run(script: Script): void;
}): Scenario;
export interface SpecParts {
    name: string;
    /** What the spec explains, in a sentence. */
    description?: string;
    actors: Actor<any, any>[];
    groups?: Group[];
    limits?: Limit[];
    /** Rules no property needs yet; rules a property needs are found from it. */
    rules?: Rule[];
    properties?: Property[];
    /**
     * The worlds where the system may stop: finished, not stuck. Any other world where nothing
     * can happen (no action possible, no guard holding, nothing pending) is reported as stuck.
     */
    finalState?: {
        description: string;
        when: (world: World) => boolean;
    };
    scenarios?: Scenario[];
}
/**
 * A spec, assembled from its parts. Messages, zones and rules are found from the actors and
 * properties that use them.
 */
export declare function defineSpec(parts: SpecParts): Spec;
export {};