Learner.AngluinWL* algorithm (van Heerdt et al.), adapted to weighted automata.
Uses an observation table whose rows and columns contain semiring-valued vectors. The *closed* criterion checks whether every successor row is in the linear span of the current basis rows; when it is not, the offending row is promoted to a basis row. A hypothesis WFA is extracted from the closed table by solving a linear system for the transition coefficients.
This module serves as a baseline for comparison with SWAL in the paper's experiments.
module S : Algebra.Semiring.Ttype aut = Automata.WFA.Make(S).ttype teacher = Teacher.Make(S).tval mk :
teacher ->
seed:Base.int ->
logic:Base.bool ->
inc:Base.bool ->
exts:(Automata.Word.t -> Automata.Word.set) ->
tmk 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).