Module type Learner.T

Shared interface satisfied by both SWAL and Angluin.

type aut
type teacher
type t
val mk : teacher -> seed:Base.int -> logic:Base.bool -> inc:Base.bool -> exts:(Automata.Word.t -> Automata.Word.set) -> t

mk teacher ~seed ~logic ~inc ~exts initializes a learner.

  • seed: SMT solver random seed (for reproducibility).
  • logic: if true, pass the semiring-specific SMT logic to the solver (tighter than Logic.ALL, may speed up solving).
  • inc: use incremental SMT mode (push/pop instead of re-asserting).
  • exts: counterexample extension function; maps a counterexample word to the set of words whose membership values are added to the observation set. Choices are Id (just the cex), Prefixes, or Suffixes (controlled by --exts).
val learn : t -> aut

Run the learning loop and return the minimal WFA for the target language.