What's new in the TVT version 3.0?


Four new programs:


The TVT version 3.0 introduces an input language similar to LOTOS that greatly alleviates the creation of system processes. The new tool program tvt.compiler analyzes files written in the TVT input language and compiles them into usual LSTS files.

Instructions for basic use of the compiler as well as a detailed description of the input language can be found from the TVT tutorial document available on the main page.


tvt.ReduceKnsp computes the smallest LSTS that is strongly bisimilar to its input. It is in other words similar to tvt.SBreduction but it uses an efficient implementation of the Kannellakis-Smolka naive algorithm. In some cases it performs significantly better than tvt.SBreduction.


tvt.TauReduction is a new reducer program that looks for set of states that are strongly connected with invisible transitions and constricts each of the sets into a single state.


The last of the new programs, tvt.simulate, is an LSTS simulator with a simple ascii-based user interface. It has been created to allow inspecting LSTSs that are too big for viewing in the usual way with the illustrator program.

Changes regarding on-the-fly verification

The way TVT handles on-the-fly verification has been changed. The syntax of the state proposition section and the file format of parallel composition rules files have been modified. Moreover, two new classes of propositions --permanent propositions and cutting propositions-- are introduced.

Please, take a look at the TVT tutorial document available on the main page to see how the propositions are used in the new version of TVT.

New command line options

Two new command line options have been added to all TVT programs in order to give a user more control of how output files are created.

First one of the options, "--extract-section", allows the user to command a section of an output LSTS file to be written to a file of its own. This can be useful especially with the action names section, since most of the programs don't change its content and can refer to the same section file in their output.

Second one, "--copy-section", allows the user to command a section --in practice the action names section-- to be copied to an output LSTS file instead of just being referred to.

Compilation of the tool made easier

The compilation process of TVT has been under careful examination and as a result, compiling the tool should be easier now. All the UNIX dependencies have been removed as well as the "hidden" Lex and Yacc dependencies. The only auxiliary software required to compile the new version of TVT is GCC (different compilers can be used with little effort), GNU make and GTK.

Windows version available

Now, for the first time, a Windows version of TVT is available. The Windows version is identical to the UNIX version and it has been tested in Windows 98, 2000 and XP. It is distributed as precompiled binaries.

Tested platforms

The TVT version 3.0 has been compiled and tested on the following platforms:

The precompiled TVT 3.0 Windows binaries have been tested in Windows 98, 2000 and XP.

Last modifications to this page: Wed Jan 29 18:16:52 EET 2003