Module Lang.Residual

Residual NFA family from Denis et al. (Boolean semiring).

This benchmark instantiates the hard family of minimal NFAs used to stress-test NFA learning algorithms. The family is parameterized by (n, k): n is the number of states and k is the alphabet size. The alphabet is split into two groups of symbols, a₀,… and b₀,…, each group sharing the same transition structure.

The target automata are the Boolean WFAs (i.e. ordinary NFAs) used as the residual-language example in the paper's evaluation section.

module S = Algebra.Bool
module Matrix : sig ... end
module Aut : sig ... end
val alpha : Base__Int.t -> Base.String.t Base.List.t * Base.String.t Base.List.t

alpha k partitions the alphabet into k/2 "a"-symbols and the remaining "b"-symbols.

val aut : Base__Int.t -> Base__Int.t -> Aut.t

aut n k constructs the target n-state NFA over a k-letter alphabet. All "a"-symbols share one transition relation and all "b"-symbols share another, giving two structurally symmetric transition functions:

  • delta_a: cyclic shift (q → q+1 mod n, wrapping at n-1→0).
  • delta_b: reverse shift (0→0, 1→n-1, q>1 → q-1). Initial states: the first ⌊n/2⌋ states are accepting (true). Final state: only state 0.
val get : Base__Int.t -> Base__Int.t -> (module Intf.T)

get n k returns the (n, k) instance as a first-class Intf.T module. The counterexample bound is set to 5000 · n · k to give the learner enough room to find counterexamples in the large NFA state space.