SWAL is an active automata learning algorithm parametric in a commutative semiring, presented in the CAV 2026 paper of the same name. Given a teacher holding a target weighted finite automaton (WFA), it builds an SMT constraint system whose solutions are WFAs consistent with observed membership queries, then calls an SMT solver (Z3, CVC5, or Bitwuzla) to find one. On termination it is guaranteed to produce a minimal WFA.
Swal.Learner — The two learning algorithms: Learner.SWAL (Algorithm 1 of the paper) and Learner.Angluin (WL* baseline).Swal.Teacher — Membership and equivalence oracle. Wraps the target language function in a memoising cache and enumerates Σ* by BFS for equivalence checking.Swal.Stats — Per-round and total statistics written to the output JSON file SWAL-<uuid>.json.Swal.Solver — Thin wrapper selecting a concrete SMT backend (Z3, CVC5, Bitwuzla) via Smtml.Swal.Config — Cmdliner term for all CLI arguments.algebra — Semiring implementations and SMT lifting.automata — WFA data structure and word type.encoding — SMT encoding strategies (naive and gen).lang — Benchmark target languages.utils — Logging, profiling, and utilities.# Build
dune build
# Learn a random 5-state tropical WFA over 3 symbols
dune exec swal -- --algo swal --lang rand_tropical:5:3 --smt z3Results are written to SWAL-<uuid>.json containing configuration, per-round statistics (query counts, wall-clock times, hypothesis sizes), and the final learned WFA.