The program FORKLIFT is an inclusion checker for Büchi automata. It takes two automata as input, presented the format described here: http://languageinclusion.org/doku.php?id=tools#the_ba_format Let us call the first given automaton A and B the second one. Upon termination, FORKLIFT exit code is: 0 if L(A) is subset of L(B) 1 if L(A) is NOT subset of L(B) 127 when the inclusion have not been computed
The compilation is performed thanks to the command:
make
Note that, the makefile will simply call another one located in the folder program.
The slave makefile will:
compile the source code (using javac)
then construct the java archive (using jar)
and finally print the usage of FORKLIFT
To run FORKLIFT without options execute the command:
java -jar forklift.jar sub.ba sup.ba
where both sub.ba and sup.ba encode some Büchi automaton.
Please find several encoding of Büchi automata in the folder samples.
For intance running
java -jar forklift.jar ./samples/example_SUPERSET.ba ./samples/example_SUBSET.ba
checks whether L(A) is included in L(B) where A and B are given in Fig.1 in the paper.
Since this inclusion does not holds, FORKLIFT provides an non-inclusion witness u cycle {v}.
Options can be inserted anywhere after forklift.jar in the run command.
For intance running
java -jar forklift.jar -t ./samples/example_SUPERSET.ba -o ./samples/example_SUBSET.ba -v
enables the options optimization, the option verbose and the option time.
For further information about options use the command:
java -jar forklift.jar -h