Using the VMTL Command Line Frontend

VMTL with command line interfaces (available here) is distributed as a directory containing VMTL itself (VMTL_CLI.jar), a startup script, the satisfiability solver Minisat, and two additional directories tmp used for temporary files produced by VMTL and additional_jars where custom dependency pair processors and/or transformations inside jar files can be placed (see also here). In order to use VMTL you can either start start VMTL directly by invoking

java -jar VMTL_CLI.jar [options] <input-file>

or by using the included bash script.

./VMTL_CLI.sh [options] <input-file>

Command line options

The following options are available

`-?`	Shows a help page.
`-m`	Prints memory usage at start and end of program execution.
`-p <property-file>`	Specify a java property file defining some execution parameters. These parameters are: `tmp`: Specifying the directory where VMTL puts its temporary files; default is `${VMTL_ROOT}/tmp/`. `Minisat`: Specify the location of the Minisat satisifability solver; default is `${VMTL_ROOT}/minisat/MiniSat`. `AdditionalJarsDir`: Specifies the location of the directory where VMTL looks for additional jar files containing user defined dependency pair processors or transformations; default is `${VMTL_ROOT}/additional_jars/`
`-j <jar-file>`	Specify a jar file containing additional user defnied dependency pair processors or transformations. This option can be used as an alternative to put the jar file in the `additional_jars` folder. The given jar file and the ones in the `additional_jars` folder will all be searched for custom processors.
`-t <limit>`	Specify a time limit in milliseconds.
`-o <classname>`	Specify a class for custom output formatting. A fully qualified name is required. The class must be available in one of the provided custom jar files (either in the `additional_jars` directory or with the `j` option).
`-showstrat`	Prints the default strategy plus the available processors, transformations and classes for output formatting.
`-s <strategy-file>`	Specify a custom strategy. An example for the format of strategy files can be obtained by using the `showstrat` option.
`-u <trafo-name>`	Specify the name of a transformation (class) to be used. The class must be available in one of the provided custom jar files (either in the `additional_jars` directory or with the `j` option).

All options are optional.

Adding custom processors, transformations or output formatters

VMTL provides public interfaces that enable the user to specify custom dependency pair processors and transformations / preprocessings for term rewriting systems. For this purpose a Java library containing the necessary interfaces and datastructures is provided here (Javadocs can be found here).

The relevant interfaces for custom dependency pair processors are DPProcessor and ContextSensitiveDPProcessor, where the latter is a subinterface of the former. A custom dependency pair processor is an implementation of one of the two depending whether it works (also) on context-sensitive termination problems or only on standard ones.

According to the dependency pair framework such a processor has to implement a method taking a dependency pair problem as an argument and returning a set of dependency pair problems. It is assumed that specified processors are correct, i.e. that if each one in the resulting set of dependency pair problems is finite, so is the input problem. The processor informs the framework through the method isComplete whether the converse holds, too

Additional methods in the interface concern human readable processor output and cleanup of external resources used by the processor. We refer to the Javadocs for details. Note that for security considerations it is not allowed to access the file system, open network connections, send direct messages to the java vm (System.exit, ...) , etc. when executing custom processors within the web application. When using the command line version of VMTL no such restrictions are imposed.

Once a dependency pair processor has been implemented it needs to be packed into a "jar" file. No meta information is needed inside the file. The VMTL library should not be included. It is also possible to include several processors into one single jar file, all of them will be found by VMTL. In addition, several jar file may be used (see below how this can be done).

Technically, the implementation of custom transformations and output formatters is basically the same as dependency pair processors, but the relevant interface here is TrsToTrsTransformation. The interface for output formatters is OutputWriter.

In order to use custom components within VMTL they need to be packed into a jar file. This file can either be put in the additional_jars folder of VMTL or passed to the program with the "-j" option. In order to use a custom transformation or a custom output formatter the name (either simple or qualified) of the class implementing the corresponding interface has to provided through the "-u" resp. "-t" options (or both). In order to use custom dependency pair processors they (i.e. their simple or qualified class names) need to be specified in a custom strategy file ("-s" option). A strategy file has the following syntax.


<processor-def>      ::= [<processor-class-name>,<time-in-ms>,<cycles>]
                     ||  [Group,<time-in-ms>,<cycles>](<processor_def_list>)
                     ||  [Group,<time-in-ms>,<cycles>,parallel](<processor_def_list>)

<processor-def-list> ::= <processor-def>
                     ||  <processor-def>,<processor-def-list>

An example of this strategy format can be obtained by using the "-showstrat" option.