This website is under construction.


These instructions are for installing TJT in Windows 7. Instructions for other compatible operating systems may be added in the future.


You will need the following:

Installation guide

Tool guide

The first thing is to active the traces view, by clicking at Window/Show View/Other on the tool bar, and then selecting TJTPlugin/Traces.

If you want to use our tool, you need to have a compiled Java project in Eclipse. You have to create a special file by clicking with the right mouse button over the project folder. In the menu you have to select New/Other/TJT/TJT configuration file. In the next window you must select the project where you want to store that new file. If the file is opened with the default editor you must close it and always open it with our special editor. For that, right mouse button over the created XML file and select Open With/ TJT Configuration Editor.

Once you have opened the configuration with with the editor, you see several different parts divided in tabs. Note that some of them might not be explained but you have them in the configuration files (they are still in experimental process and only hash implementation is currently released). The most important tabs are explained next:

Once we have performed a test with our tool, we will see how the Traces View changes (otherwise try pressing the rescan button of the view), and an item with the project name is added. Depending on the result of the test, we can expand that item and see the different(s) execution(s) trace(s). When we click over a determinate location, we will see the class it belongs and the concrete line remarked in a new window. Following the course of the execution, we can extract conclusions about the behavior of our code and why errors appeared. Besides erroneous traces information you are able to see in real time what is happening during the execution by selecting TJT console in Eclipse console view. A trace file by itself contains useful information, because it stores in order the operations performed in the tested Java program to that concrete trace. We also are able to watch the values of the variables in a proper view.


We provide you the code we have tested. Note that this codes have been slightly modified for performing easily and automatically the different tests. This modification is neccesary only with servers and programs with an infinite execution to save time and to have a stop condition in some cases.

To use anyone of them you must create an Eclipse project, and import the packaged file to it. Each package also contains the configuration files for evaluating the properties we tested in its root directory. Make sure you build the project before launching the test. We recommend you to test first the configuration files as they are, and later try changing some parameters.

To use our tool, you may open the concrete test file by clicking Open With/TJT Configuration Editor. Then you have to proceed as explained in the tool guide.


Download this example project

This code consists of a complete FTP Java server, with an additional part added by us that simulates the behavior of a client according to our purpose.

Java NFS server

Download this example project

This code contains a NFS server with an internal client which performs operations against the server.


Download this example project

It is a code for a http server. As the others servers above exposed, this one contains a small additional code that simulates the behavior of client.


Download this example project

Download this example project

This is a concurrent program, with one elevator and several users that try to access it. The first link is a good implementation and the second is wrong implemented in order to see the errors.

Lists management

Download this example project

This program contains performs operations in lists inside a cycle.

Random numbers

Download this example project

This project contains three different classes that performs method accesses according to random numbers results. They are used as examples in jpf-ltl too.