import { type Event, type Spec, type World } from "../spec/index.ts";
import { type Counterexample } from "./explore.ts";
/** What a log line says happened: an instance appearing, or one taking a step. */
export type LogEvent = LogSpawn | LogStep;
export interface LogSpawn {
    /** Its place in the log, from 1. */
    line: number;
    /** Where it came from, when not a line of a file: a span, for a trace (trace.ts). */
    at?: string;
    kind: "spawn";
    actor: string;
    label: string;
}
export interface LogStep {
    line: number;
    at?: string;
    /** What kind of step, if the log says: an action, a delivery, a timer or a guarded step. */
    kind?: "action" | "deliver" | "timer" | "guard";
    /** Who took it: an instance's id or label. */
    instance: string;
    /** The action's or step's name. */
    key: string;
    /** An action's inputs; left out, any it can take. */
    inputs?: Record<string, unknown>;
    /** A delivery's message, by key (`message:Buy`); left out, any the step is on. */
    message?: string;
    /** A delivery's sender, by id or label. */
    from?: string;
    payload?: unknown;
    /** Fields of the instance's state after the step, which must be as given. */
    state?: Record<string, unknown>;
    /**
     * The lines of the steps that must come before it, when the log is a partial order (a trace,
     * whose machines' clocks disagree). When no step says, the log is in order: each line after
     * the one before.
     */
    after?: number[];
}
export interface ConformOptions {
    /**
     * Instances besides the singletons, as `check --instances` makes them, before the log's own
     * spawns. An actor left out has none: a log says who is there.
     */
    instances?: Record<string, number>;
    /** Unlogged steps allowed between two logged ones (and before the first). */
    gap?: number;
    /** Whether faults are logged; by default not: a lost message leaves no line. */
    logsFaults?: boolean;
    /** Actors whose steps the log does not record. */
    unlogged?: string[];
    /** Worlds the search may visit before it gives up. */
    maxStates?: number;
}
export declare const DEFAULT_GAP = 4;
/** A property the log's run breaks: the event that breaks it, by its place on the run. */
export interface LogBreak {
    id: string;
    description: string;
    /** Its place in `run.events`. */
    at: number;
}
export type Conformance = {
    conforms: true;
    /** The run the log is, with the unlogged steps it needed. */
    run: Counterexample;
    /** For each event of the run, the log line it matched; undefined for an unlogged step. */
    lines: (number | undefined)[];
    broken: LogBreak[];
    states: number;
} | {
    conforms: false;
    /** Why: the line no reading can match, or the search gave up first. */
    stop: {
        kind: "mismatch";
        line: LogStep;
        could: string[];
        near: string[];
        errors: string[];
    } | {
        kind: "limit";
        states: number;
    };
    /** The longest reading: the run as far as it fits, and its lines. */
    run: Counterexample;
    lines: (number | undefined)[];
    states: number;
};
/** A log's lines, as JSON Lines: each one an object for one event, blank lines skipped. */
export declare function parseLog(text: string, spec: Spec): LogEvent[];
/** One event, from a log line or (trace.ts) a span, `at` saying where it came from. */
export declare function parseEvent(v: Record<string, unknown>, line: number, spec: Spec, at?: string): LogEvent;
/** A log the spec cannot read: at a line (`line 3 …`), at a span, or (`at` empty) about the whole. */
export declare class LogError extends Error {
    readonly line: number;
    readonly what: string;
    constructor(line: number, what: string, at?: string);
}
/** Whether a log is a run of the spec, and the reading that says so, or where it leaves the spec. */
export declare function conform(spec: Spec, log: LogEvent[], options?: ConformOptions): Conformance;
/** An event as a log line would put it: who, what, and with which message, inputs or payload. */
export declare function describeEvent(before: World, e: Event, after?: World): string;