Minimize (p.grenier.0.15.doc.grenier.valmari.Valmari.Minimize)

Parameters

module Label : Map.OrderedType

module In : INPUT with type label := Label.t

include DFA with type label = Label.t

Sourcetype states

Sourceval states : states Strong.Finite.set

The set of DFA nodes

Sourcetype transitions

Sourceval transitions : transitions Strong.Finite.set

The set of DFA transitions

Sourcetype label = Label.t

The type of labels that annotate transitions

Sourceval label : transitions Strong.Finite.elt -> label

Get the label associated with a transition

Sourceval source : transitions Strong.Finite.elt -> states Strong.Finite.elt

Get the source state of the transition

Sourceval target : transitions Strong.Finite.elt -> states Strong.Finite.elt

Get the target state of the transition

Sourceval initials : states Strong.Finite.elt array

Sourceval finals : states Strong.Finite.elt array

val transport_state : 
  In.states Strong.Finite.elt ->
  states Strong.Finite.elt option

val transport_transition : 
  In.transitions Strong.Finite.elt ->
  transitions Strong.Finite.elt option

Sourceval represent_state : states Strong.Finite.elt -> In.states Strong.Finite.elt

val represent_transition : 
  transitions Strong.Finite.elt ->
  In.transitions Strong.Finite.elt