sft-example.vtf

# Example of a symbolic finite transducer in the VATA format
@SFT               # symbolic finite transducer
%Name  trans       # name (optional)
%Initial q1        # initial states (required)
%Final q2          # final states (required)
# TODO: restrict the theories?

q1 ("(= x 3)") ("(+ x 3)" "0") q2       # the format is <source> (<input predicate 1> ... <input predicate n>)
                                        # (<output function 1> ... <output function m>) <target>
q1 ("(even x)" "(odd y)") ("y" "x") q2  # here, we use a transition over two
                                        # symbols; note that the free variables
                                        # used in the predicates are used in
                                        # the output functions to refer to the
                                        # position of the symbols
q1 ("(= x x)") ("x") q3                 # this is how to specify the 'true'
                                        # predicate and also bind the symbol to a variable
q1 () ("1") q3                          # epsilon transitions allowed too
q1 ("(in x (list 1 2 3)") ("x") q3      # the input symbol is one of {1,2,3}, the output is the same