import { type AnyMessage, type Message, type ModelView, type Part, type Variable } from "../spec/dsl.ts";
import type { Fields, TypeOf } from "../spec/schema.ts";
/** What reports count: a step tagged `fault` is one. */
export declare const FAULT = "fault";
/** What a call's failure carries: the payload of the call that failed, and whom it was to. */
export interface Failure<P> {
    readonly payload: P;
    readonly to: {
        readonly id: string;
    };
}
/** A call: a message whose loss, or its reply's, reaches the caller as `failed(call)`. */
export interface Call<Id extends string = string, P = unknown> extends Message<Id, P> {
    /** Phantom: marks a call, so `failed` takes only calls. */
    readonly __call?: true;
}
/** A call's failure: a plain message, `Charge.failed`, the caller has a step on. */
export type Failed<Id extends string, P> = Message<`${Id}.failed`, Failure<P>>;
/**
 * A call (RFD0009), as a message and its failure: `lose` on the call, or on its reply, sends
 * the caller `failed(Charge)`, as an RPC or a `fetch` throws. Its replies carry the request
 * they answer, so a lost reply knows which call it fails.
 */
export declare function defineCall<const Id extends string, F extends Fields = {}>(id: Id, schema?: F, options?: {
    name?: string;
    over?: string;
}): Call<Id, TypeOf<F>>;
/** The failure of a call from `defineCall`: what the caller's step is `on`. */
export declare function failed<Id extends string, P>(call: Call<Id, P>): Failed<Id, P>;
/** A budget: a model variable a fault spends. `--set faults=2` raises it. */
export type Budget = Variable<number>;
/** `budget("faults", 1)`: at most one fault on any path, across every step that spends it. */
export declare function budget(name: string, n: number): Budget;
/** A part that spends a budget: the step is possible only while it is above zero, and takes one. */
export declare function spend(budget: Budget): Part;
/**
 * A part bounding a step to at most `limit` times per instance on any path: an action a person
 * might take forever, bounded for the checker as TLA+ bounds it with a counter. Each instance
 * counts its own, in a model variable named after the step (`Client.pay`). The limit is a
 * number, or a variable several steps share, so `--set repeats=3` raises them all.
 */
export declare function atMost(limit: number | Variable<number>): Part;
interface FaultOptions {
    /** The budget it spends; without one, it may happen on every path, any number of times. */
    spend?: Budget;
    /** In everyday words, instead of the default. */
    description?: string;
}
/** What a fault step is: unfair (it may never happen), on a message or on nothing, tagged `fault`. */
interface FaultStep<On> {
    on?: On;
    fair: false;
    tags: readonly string[];
    with: readonly Part[];
    sends?: readonly AnyMessage[];
    when?: (state: any, model: ModelView) => boolean;
    description: string;
    run(state: any, received: any, ctx: any): void;
}
/**
 * The receiver loses `message` on the way: a step on it that does nothing with it. For a call,
 * the caller's call fails; for a reply, pass `fails` with the call it answers (or the calls it
 * may answer), and the caller's call fails when the reply is lost: the callee did the work, and
 * the caller cannot tell.
 */
export declare function lose<M extends AnyMessage>(message: M, options?: FaultOptions & {
    fails?: Call<string, any> | readonly Call<string, any>[];
}): FaultStep<M>;
/** The network delivers `message` twice: a step on it that puts it back in flight twice. */
export declare function duplicate<M extends AnyMessage>(message: M, options?: FaultOptions): FaultStep<M>;
/**
 * The instance crashes and starts again: its state is its initial state but for the fields in
 * `keeps` (what it wrote to disk), its timers are gone, and so are the failures on their way
 * to it, which would have thrown in code that is no longer running.
 */
export declare function crash(options?: FaultOptions & {
    keeps?: readonly string[];
}): FaultStep<undefined>;
export {};