module Petri: sig .. end
Module for Petri Automata.
type Tools.ISet.t * Tools.Trans.t * int * Tools.ISSet.t
Type of an automaton.
val union : t -> t -> t
Union of automata.
val concat : t -> t -> t
Sequential product of automata.
val pstar : t -> t
Iteration of an automaton.
val inter : t -> t -> t
Intersection of automata.
val trad : string Expr.expr -> t
Conversion of an expression into an automaton.
val progress : Tools.ISet.t -> Tools.ptrans -> Tools.ISet.t
Makes a configuration go through a transition.
val read : Tools.readstate -> Tools.ptrans -> Tools.Trans.t -> Tools.MSet.t
Makes an embedding go through a transition.
val simul : t -> t -> int * string * string Expr.ground option
Tries to find a ground term recognised by the first automaton
that is not recognised by the second. In case of success,
returns said term.
Otherwise returns None.
It also returns the number of pairs examined, and a string
representing these pairs.