package grenier
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=e5362e6ad0e888526517415e78b9e8243bb0cc1b0c952201884148832ac4442f
sha512=4e2f16b52b3c2786a1b8e93156184fd69d448cea571ca839b6cb88ab73f380994d1561fe24c1523c43ed8fc42d2ac01b673a13b6151fff4af4f009923d3aaf37
doc/grenier.valmari/Valmari/Minimize/argument-2-In/index.html
Parameter Minimize.In
include DFA with type label := Label.t
val states : states Strong.Finite.setThe set of DFA nodes
val transitions : transitions Strong.Finite.setThe set of DFA transitions
val label : transitions Strong.Finite.elt -> Label.tGet the label associated with a transition
val source : transitions Strong.Finite.elt -> states Strong.Finite.eltGet the source state of the transition
val target : transitions Strong.Finite.elt -> states Strong.Finite.eltGet the target state of the transition
val initials : (states Strong.Finite.elt -> unit) -> unitIterate on initial states
val finals : (states Strong.Finite.elt -> unit) -> unitIterate final states
val refinements :
refine:(iter:((states Strong.Finite.elt -> unit) -> unit) -> unit) ->
unitThe minimization algorithms operate on a DFA plus an optional initial refinement (state that must be distinguished, because of some external properties not observable from the labelled transitions alone).
If no refinements are needed, the minimum implementation is just: let refinements ~refine:_ = ()
Otherwise, the refinements function should invoke the refine function for each set of equivalent states and call the iter for each equivalent state.
E.g if our automata has 5 states, and states 2 and 3 have tag A while states 4 and 5 have tag B, we will do:
let refinements ~refine = refine (fun ~iter -> iter 2; 3); refine (fun ~iter -> iter 4; 5)