Module DFA

Function dfa_to_pre


pub  fn dfa_to_pre
[
N : Nat,
$S,
@D
]
(   dfa : DFA[N, $S, @D] $pre @public
) 
-> DFA[N, $pre, @D] $pre @public

Conversion of the given DFA to the stage $pre.

Function dfa_to_prover


pub  fn dfa_to_prover
[
N : Nat,
$S,
@D
]
(   dfa : DFA[N, $S, @D] $pre @public
) 
-> DFA[N, $S, @prover] $pre @public

Conversion of the given DFA to the domain @prover.

Function init_dfa


pub  fn init_dfa
[
N : Nat,
$S,
@D
]
(   numStates : uint[18446744073709551616] $pre @public,
   alphabetSize : uint[18446744073709551616] $pre @public,
   trans : list[list[uint[N] $S @D] $pre @public] $pre @public,
   init : uint[N] $S @D,
   finals : list[uint[N] $S @D] $pre @public
) 
-> DFA[N, $S, @D] $pre @public

The DFA object with given fields.

Function runDFA


unchecked eff [,,[[*]],*,[*]] -> [*] -> * ! <@public>

pub  fn runDFA
[
N : Nat,
$S,
@D
]
(   dfa : DFA[N, $S, @D] $pre @public,
   w : list[uint[N] $S @D] $pre @public
) 
-> bool[N] $S @D

where

  Field[N]

Test if the DFA given as the first argument recognizes the word given as the second argument.