package grenier
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=dec7f84b9e93d5825f10c7dea84d5a74d7365ede45664ae63c26b5e8045c1c44
sha512=b8aa1569c2e24b89674d1b34de34cd1798896bb6a53aa5a1287f68cee880125e6b687f66ad73da9069a01cc3ece1f0684f48328b099d43529bff736b772c8fd8
doc/grenier.valmari/Valmari/module-type-INPUT/index.html
Module type Valmari.INPUT
Source
include DFA
The set of DFA nodes
The set of DFA transitions
The type of labels that annotate transitions
Get the label associated with a transition
Get the source state of the transition
Get the target state of the transition
Iterate on initial states
Iterate final states
The 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
)