TLV is based on the SMV model checker , however, all the code implementing model checking has been replaced by a layer that implements a scripting language called TLV-Basic. Users of the system can then write procedures in TLV-Basic for implementing either model checking or deductive verification rules. TLV is a byproduct of Elad Shahar's M.Sc. thesis.
Compressed executables are available for Sun/Solaris, Linux, and win32. To use them, save the file to your disk. Use the following command to uncompress the file:
or
(Make sure you get the filename right)
You can use the source files to compile TLV on other systems. However, we have only checked Solaris, Linux, Windows XP (MinGW and Cygwin), and Mac OS X. It is easier to compile if you have flex, bison, gcc, and gnu readline. To use the source files, create a new directory, put the file in that directory. Then type
If you want to put the rule files in a separate directory, you have to tell TLV where the rule files are. To do this set the environment variable TLV_PATH to point to the directory where the rule files are. For example, in cshell I use the command:
In bash use something like the following:
Currently the compiler from SPL to SMV is not available, thus you cannot use tlv to load programs written in SPL.
An updated tutorial is not yet available.
Note for Windows users:
Note: this version is unsupported and, to be honest, rather old.
A mailing list is available for discussion by both users and (potential) developers. To subscribe, go here.
The Analysis of Computer Systems web site
An SMV Mode interface for Emacs. See the file itself for instructions how to set it up.