Quelle  fsa_4   Sprache: Isabelle

fsa_4 := rec (
# This is the word-acceptor for the free group on two generators a,b
# A and B are the inverses of a and b respectively.
# The accepted language consists of all strings that do not have
# aA, Aa, bB or Bb as a substring.
           isFSA := true,
        alphabet := rec (
              type := "identifiers",
              size := 4,
            format := "dense",
             names := [a,A,b,B]
               ),
          states := rec (
 # This is a contrived example to illustrate the list of integers type.
              type := "list of integers",
              size := 5,
              format := "dense",
       names:= [ [1,3], [2], [-3,0,-3,5], [], [0] ]
               ),
           flags := ["DFA","minimized","BFS"],
         initial := [1],
       accepting := [1..5],
           table := rec(
  format := "dense deterministic",
    transitions := [
        [2,3,4,5],
                      [2,0,4,5],
                      [0,3,4,5],
                      [2,3,4,0],
                      [2,3,0,5]
                     ]
        )
);