Module Lang.Rand_tropical

Random tropical WFA benchmark — unbounded tropical semiring (QF_LIA).

Generates a random WFA with q states over a s-symbol alphabet. Uses the unbounded tropical semiring ({∞} ∪ ℕ, min, +, ∞, 0) via Tropical_lia.get None.

Transition density heuristic: for each (state, character) pair, each outgoing transition is non-zero independently with probability 1.5 / q. This keeps the average out-degree near 1.5 regardless of the number of states, producing automata with realistic sparsity.

module Log : sig ... end
module S : sig ... end
module Matrix : sig ... end
module Aut : sig ... end
val alpha : int -> (Automata.Char.t, Automata.Char.comparator_witness) Base.Set.t
val aut : Base.Int.t -> int -> Aut.t

aut q s constructs a random q-state WFA over a s-symbol alphabet. The initial vector has weight one at state 0 and zero elsewhere. Each transition matrix and the output vector are generated with the sparsity heuristic non_zero = 1.5 / q.

val get : Base.Int.t -> Base__Int.t -> (module Intf.T)