Using the VMTL Web Application
The web interface is an easy to use front end for the VMTL laboratory. It features graphic strategy manipulation, dynamic addition of custom dependency pair processors as well as TRS transformations (used for instance to transform conditional to standard TRSs) and convenient proof layouting. Figure 1 shows a screenshot of the web application.
Item 2 in Figure 1 points to the main input area, where standard, context-sensitive and conditional term rewriting systems can be entered using the tpdb syntax described here. Item 1 points to 3 links that will load syntactically correct examples into the text area. Three examples, a standard, a context-sensitive and a conditional one are available.
Alternatively, input systems can be specified directly from within files. To do this, select the input file using the file upload field (item 3 in Figure 1). Note that specifying a file and entering a system into the input text area (item 2) are alternative. In case you specify both, VMTL will use the system from the input field which was changed most recently.
To start the actual proof search use the button at item 6. At item 7 one can specify a transformation / preprocessing step that is performed on the input system before the termination analysis using dependency pairs starts. In case the input system is conditional, a transformation is mandatory. The value Default means that no transformation / preprocessing is applied, unless the input system is conditional in which case a simple context-sensitive unraveling transformation is used.
Items 8, 9 and 10 in Figure 1 point to the strategy configuration area. The input field at item 9 lets the user specify an overall time limit (in milliseconds) for the proof search. Note that the time limit may not exceed 120 seconds due to limited server-side resources. The link at item 10 can be used to reset the strategy to the default one in case it has been modified.
Items 4 and 5 point to fields allowing a user to upload custom dependency pair processors and transformations. For details how this can be done see below.VMTL Output
There are three possible results that VMTL can produce.- A successful termination proof
- An unsuccessful termination proof attempt
- A termination disproof
Figure 2 shows a screenshot of VMTL after a successful proof. Item 1 points to the info area informing the user which of the 3 possible results was produced. The next information area (item 2) lists the dependency pair problems that occurred during the proof together with the (successfully) applied dependency pair processors in a tree like structure. A problem is the child of another one if it was obtained by processing the first problem. In case termination cannot be proved also processors that failed (i.e. that could not simplify the problem) are enlisted here.
Finally, the output generated by each successfully applied dependency pair processor is listed (item 3) and can be viewed by clicking on the Show Details button (item 4).
If termination can not be proved there is an additional output indicating which termination problem(s) could not be processed and remained open. Moreover, if termination can be disproved additional information regarding the infinite computation is given.
Strategy Configuration
In VMTL a strategy is a tree that determines the order of dependency pair processor application through a preorder traversal. However, the tree structure yields processor groups for which parameters such as time limits and repetitions can be set instead of setting them for each single processor.
Figure 3 shows an example of a strategy tree. There, an overall time limit of 10 seconds (10000 ms) is used (item 1). The proof search is started with the dependency graph processor indicated by the value of the selection box at item 2. This selection box contains all available dependency graph processors. The user can select a different processor when customizing the strategy. Note that also custom processors added by the user before are available through this selection.
The next two processors, one for searching for polynomial interpretations yielding suitable orderings and again the dependency graph, are grouped together (another processor group is pointed to by item 3). Through the New Processor button (item 4) additional processors can be added to the strategy. Such buttons are located in each processor group of the strategy, so that processors can be added to each group. If the Processor Group (item 5) box is checked when using the New Processor button a new processor group is added instead of a new processor.
For each processor and each group individual timeouts and cycles can be specified. If several timeouts apply, i.e. for instance if a processor is given a timeout of 10 seconds, but the surrounding processor group has a timeout of only 5 seconds then the shorter timeout is used. A value of 0 means no timeout. Item 9 points to the field specifying a timeout of 2 seconds for the polynomial ordering processor.
Additionally, each processor can be used repeatedly. The field Cycles (item 9) specifies how many times a processor or processor group is applied. In the strategy of figure one the combination of polynomial ordering- and dependency graph processor is executed 10 times in a row (item 9).
Processor groups have an additional attribute specifying whether their "child" processors (resp. groups) are to be executed in parallel. If so the child processors are all given the same input (as compared to feeding them the output of the preceeding one in the non-parallel case) and if none of them actually finds a termination proof the termination problem does not get altered by any of them.
Finally, processors and groups can be deleted by using the red "close" button (item 6).
Adding new processors / transformations / evaluation functions
VMTL provides public interfaces that enable the user to specify custom dependency pair processors and transformations / preprocessings for term rewriting systems. In addition custum evaluation functions can be added to VMTL, which VMTL uses to select problems in the proof search when parallel branches in the strategy tree are rejoined. 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, which can be uploaded through the web interface via the input field of Figure 1, item 4. 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 files may be uploaded (e.g. to use libraries). After the upload the new processors will be available through the processor selection in the strategy area (Figure 3, item 2).
Technically, the implementation of custom transformations and evalution functions is basically analogous to the implementation of custom dependency pair processors, but the relevant interfaces here are TrsToTrsTransformation and ProblemEvaluator.
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 invokingjava -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:
|
| -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
For details on the implementation of custom components please refer to the corresponding section of the VMTL web application help. 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>]{parameter-list}
|| [<processor-class-name>,<time-in-ms>,<cycles>]
|| [Group,<time-in-ms>,<cycles>]{parameter-list}(<processor_def_list>)
|| [Group,<time-in-ms>,<cycles>,parallel]]{parameter-list}(<processor_def_list>)
<processor-def-list> ::= <processor-def>
|| <processor-def>,<processor-def-list>
<parameter-list> ::= <EMPTY>
|| <parameter-name>=<parameter-value>,<parameter-list>
An example of this strategy format can be obtained by using the "-showstrat" option.