Module Lang.Probs

Probs benchmark — probabilistic WFA.

A 2-state Markov chain over the single-letter alphabet {a} using the probabilistic semiring (Prob, QF_NIA). The transition matrix encodes a random walk between two states: State 0 → State 0 with prob 2/3, State 1 with prob 1/3. State 1 → State 0 with prob 1/2, State 1 with prob 1/2. Output: State 0 accepts with weight 1, State 1 with weight 0. The language computes the probability of being in state 0 after reading a word.

module S = Algebra.Prob
module Matrix : sig ... end
module Aut : sig ... end
val bound : int
val aut : Aut.t
val out : Automata.Word.t -> Aut.s