Gerco (SWAL.Lang.Gerco)

Gerco benchmark — unbounded natural-number WFA.

A small 2-state WFA from 10.1007/978-3-030-45231-5_31 over the single-letter alphabet {a}, used as a simple functional smoke-test. The WFA computes an arithmetic series, making it easy to verify correctness by hand. Uses the unbounded natural-number semiring (Nat.get None, QF_NIA).

module S : sig ... end

module Matrix : sig ... end

module Aut : sig ... end

val alpha : (Automata.Char.t, Automata.Char.comparator_witness) Base.Set.t

val bound : int

val aut : Aut.t

The target automaton: init = 0; 1, delta_a = [1;0];[1;2], out = 1; 0. Computes: on word aⁿ the output grows without bound.

val out : Automata.Word.t -> Aut.s