Module Swal.Stats

Global statistics accumulator, written to SWAL-<uuid>.json at end of run.

type total = {
  1. teacher : Teacher.stats;
    (*

    Cumulative membership / equivalence query counts.

    *)
  2. time : Utils.Profiler.t;
    (*

    Cumulative wall-clock time per phase.

    *)
}

Accumulated statistics for the entire learning run, written to the output JSON.

val pp_total : Ppx_deriving_runtime.Format.formatter -> total -> Ppx_deriving_runtime.unit
val show_total : total -> Ppx_deriving_runtime.string
val yojson_of_total : total -> Ppx_yojson_conv_lib.Yojson.Safe.t
type round = {
  1. teacher : Teacher.stats;
    (*

    Query counts for this round.

    *)
  2. time : Utils.Profiler.t;
    (*

    Wall-clock time for this round.

    *)
  3. hyp : Automata.WFA.stats;
    (*

    Size and structure of the hypothesis WFA.

    *)
  4. smt : Solver.stats Base.option;
    (*

    SMT solver internal statistics (SWAL only).

    *)
}

Per-round statistics (one entry per equivalence query / hypothesis).

val pp_round : Ppx_deriving_runtime.Format.formatter -> round -> Ppx_deriving_runtime.unit
val show_round : round -> Ppx_deriving_runtime.string
val yojson_of_round : round -> Ppx_yojson_conv_lib.Yojson.Safe.t
type t = {
  1. timestamp : Utils.Time.t;
    (*

    Wall-clock time at the start of the run.

    *)
  2. rounds : round Base.list;
    (*

    One entry per learning round (equivalence query).

    *)
  3. total : total;
}

Top-level stats record written to SWAL-<uuid>.json.

val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val stats : t option Base.ref

Global mutable stats cell, initialized once by mk and mutated by add.

val get : unit -> t
val set : t -> Base.unit
val mk : unit -> Base.unit

Initialize the stats cell. Must be called once before the learning loop.

val add : Automata.WFA.stats -> Solver.stats Base.option -> Teacher.stats -> round

add hyp smt teacher snapshots the profiler lap and teacher stats, appends a new round record, and accumulates into the totals. Returns the new round for immediate logging.