Forlan Manual


The RFA Module


Synopsis

signature RFA
structure RFA :> RFA

This module defines the abstract type of regular expression finite automata (RFAs).


Interface

type concr = {
               stats : Sym.sym Set.set,
               start : Sym.sym,
               accepting : Sym.sym Set.set,
               trans : TranReg.tran_reg Set.set
             }
type rfa
val valid : concr -> bool
val fromConcr : concr -> rfa
val toConcr : rfa -> concr
val fromString : string -> rfa
val input : string -> rfa
val toPP : rfa -> PP.pp
val toString : rfa -> string
val output : string * rfa -> unit
val states : rfa -> Sym.sym Set.set
val startState : rfa -> Sym.sym
val acceptingStates : rfa -> Sym.sym Set.set
val transitions : rfa -> TranReg.tran_reg Set.set
val compare : rfa Sort.total_ordering
val equal : rfa * rfa -> bool
val numStates : rfa -> int
val numTransitions : rfa -> int
val alphabet : rfa -> Sym.sym Set.set
val sub : rfa * rfa -> bool
val renameStates : rfa * SymRel.sym_rel -> rfa
val renameStatesCanonically : rfa -> rfa
val checkLP : (Str.str * Reg.reg -> bool) * rfa -> LP.lp -> unit
val validLP : (Str.str * Reg.reg -> bool) * rfa -> LP.lp -> bool
val standard : rfa -> bool
val standardize : rfa -> rfa
val fromFA : (Reg.reg -> Reg.reg) -> FA.fa -> rfa
val eliminateState : (Reg.reg -> Reg.reg) -> rfa * Sym.sym -> rfa
val toReg : (Reg.reg -> Reg.reg) -> rfa -> Reg.reg
val faToReg : (Reg.reg -> Reg.reg) -> FA.fa -> Reg.reg
val faToRegPerms : int option * (Reg.reg -> Reg.reg) -> FA.fa -> Reg.reg
val faToRegPermsTrace : int option * (Reg.reg -> Reg.reg) -> FA.fa -> Reg.reg
val jforlanNew : unit -> rfa
val jforlanEdit : rfa -> rfa
val jforlanValidate : string -> unit
val jforlanPretty : string -> unit

Description

type concr = {
               stats : Sym.sym Set.set,
               start : Sym.sym,
               accepting : Sym.sym Set.set,
               trans : TranReg.tran_reg Set.set
             }
The concrete type of pre-regular expression finite automata, records consisting of a finite set stats ("states") of symbols, a symbol start ("start state"), a finite set accepting ("accepting states") of symbols, and a finite set trans ("transitions") of RFA transitions.

type rfa
The abstract type of regular expression finite automata, consisting of those pre-regular expression finite automata concr of type concr such that: We say that concr is valid iff concr satisfies the above conditions.

valid concr
tests whether concr is valid.

fromConcr concr
returns concr. Issues an error message if concr is not valid.

toConcr rfa
returns rfa.

fromString s
inputs an RFA from s.

input fil
inputs an RFA from the file named fil.

toPP rfa
returns a pretty-printing expression for rfa.

toString rfa
pretty-prints rfa to a string.

output(fil, rfa)
pretty-prints rfa to the file fil.

states rfa
returns the states of rfa.

startState rfa
returns the start state of rfa.

acceptingStates rfa
returns the accepting states of rfa.

transitions rfa
returns the transitions of rfa.

compare(rfa1, rfa2)
returns
  case SymSet.compare(states rfa1, states rfa2) of
       LESS    => LESS
     | EQUAL   =>
         (case Sym.compare(startState rfa1, startState rfa2) of
               LESS    => LESS
             | EQUAL   =>
                 (case SymSet.compare(acceptingStates rfa1, acceptingStates rfa2) of
                       LESS    => LESS
                     | EQUAL   =>
                         TranRegSet.compare
                         (transitions rfa1, transitions rfa2)
                     | GREATER => GREATER)
             | GREATER => GREATER)
     | GREATER => GREATER


equal(rfa1, rfa2)
tests whether rfa1 and rfa2 are equal.

numStates rfa
returns the number of states of rfa.

numTransitions rfa
returns the number of transitions of rfa.

alphabet rfa
returns the alphabet of rfa.

sub(rfa1, rfa2)
tests whether rfa1 is a sub-RFA of rfa2.

renameStates(rfa, rel)
renames the states of rfa using the bijection rel. Issues an error message if rel is not a bijection from the states of rfa to some set.

renameStatesCanonically rfa
canonically renames the states of rfa.

checkLP (memb, rfa) lp
checks whether lp is valid for rfa, using memb for testing whether the strings of lp are generated by regular expressions of rfa. checkLP silently returns (), if lp is valid, and explains why it isn't valid, if it's not valid.

checkLP (memb, rfa) lp
tests whether lp is valid for rfa, using memb for testing whether the strings of lp are generated by regular expressions of rfa.

standard rfa
tests whether rfa is standard.

standardize rfa
standardizes rfa.

fromFA simp fa
Converts fa to an RFA, using simp to simplify the regular expressions of transitions.

eliminateState simp (rfa, q)
eliminates the state q from rfa, using simp for regular expression simplification. Issues an error message if q is not a state of rfa, q is the start state of rfa, or q is one of the accepting states of rfa.

toReg simp rfa
converts the standardization of rfa to a regular expression by the state elimination algorithm, using simp for regular expression simplification.

faToReg simp fa
converts the standardization of fromReg simp fa to a regular expression by the state elimination algorithm, using simp for regular expression simplification.

faToRegPerms (NONE, simp) fa
works through all the bijections (permutations) rel on the states of fa, evaluating faToReg simp (FA.renameStates(fa, rel)), and selecting the simplest answer (judged using Reg.compareComplexityTotal).

faToRegPerms (SOME n, simp) fa
works through the first n bijections (ordered by SymRel.compare) rel on the states of fa, evaluating faToReg simp (FA.renameStates(fa, rel)), and selecting the simplest answer (judged using Reg.compareComplexityTotal). Issues an error message if n is negative.

val faToRegPermsTrace : int option * (Reg.reg -> Reg.reg) -> FA.fa -> Reg.reg
is like faToRegPerms, but issues tracing messages, explaining its operation.

jforlanNew()
invokes JForlan, and returns the RFA that the user creates and commits. Issues an error message if the user aborts, instead.

jforlanEdit rfa
invokes JForlan, letting the user edit rfa, and returning the resulting RFA that the user commits. Issues an error message if the user aborts, instead.

jforlanValidate
is a low-level function used by JForlan. See the code for more information.

jforlanPretty
is a low-level function used by JForlan. See the code for more information.


[ Top | Parent | Root | Contents | Index ]

Forlan Version 4.12
Copyright © 2019 Alley Stoughton