package lascar

  1. Overview
  2. Docs
package lascar
Legend:
Library
Module
Module type
Parameter
Class
Class type

Non-deterministic Finite Automata (NFA)

A NFA is just a Labeled Transition System (LTSA) for which

  • transition labels are taken from an input alphabet
  • the set of initial states is reduced to a singleton
  • state attribute is boolean indicating whether the state is accepting or not
module type SYMBOL = sig ... end
module type T = sig ... end
module Make (S : Ltsa.STATE) (L : SYMBOL) : T with type state = S.t and type symbol = L.t

Functor building an implementation of the NFA structure given an implementation of state identifiers and symbols

module Trans (S1 : T) (S2 : T) : sig ... end

Functor for converting a NFA, with a given implementation of state identifiers and symbols into another one with different respective implementations

module Product (S1 : T) (S2 : T with type symbol = S1.symbol and type Symbols.t = S1.Symbols.t) : sig ... end

Functor for computing the products of two NFAs sharing the same symbol set