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.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.
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.
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, "
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.
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.
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.
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.