ShotTx.Prover.SessionSupervisor (ShotTx v0.0.1)

Copy Markdown View Source

OTP supervisor owning the per-session proof-search tree.

Started once per ShotTx.Prover.prove/* call and torn down when the caller returns. Uses :rest_for_one so that if the Manager or an agent crashes, its dependents restart in the correct order — the ETS keeper stays alive and preserves stats/traces for post-mortem inspection.

Children (in start order):

  • EtsKeeper — owns the per-session tables (:stats, :tombs, :work_queue, :idle_queue, :traces).
  • Task.Supervisor — supervises async CSP dispatches from ContradictionAgent.
  • Manager — orchestrates workers and iterative deepening.
  • ContradictionAgent, SuggestionAgent, ModelAgent — peer agents on the shared branch_evidence_<session> PubSub topic.
  • A DynamicSupervisor for the worker pool.

Summary

Functions

child_spec(init_arg)

Returns a specification to start this module under a supervisor.

start_link(init_arg)

Starts a per-session supervision tree.

Functions

child_spec(init_arg)

Returns a specification to start this module under a supervisor.

See Supervisor.

start_link(init_arg)

Starts a per-session supervision tree.

init_arg is {session_id, formulas, defs, params} where session_id is the unique reference for this proof, formulas are the initial branch formulas (assumptions plus the negated conclusion), defs a definition map, and params a ShotTx.Data.Parameters struct.