TLV INSTALLATION

(Fabio Patrizi, December, 2008)

0. Create directory <my_path>/TLV/ (or <my_path>\TLV\, if on a Windows platform)

ON A WINDOWS PLATFORM:

1. Download and install Cygwin, available at http://www.cygwin.com/

2. Download TLV executables for Cygwin at http://www.wisdom.weizmann.ac.il/~verify/tlv/tlvcygwin3.2.exe.Z and uncompress them into <my_path>\TLV\;

2b. You can also download (recommended) the TLV manual at http://www.wisdom.weizmann.ac.il/~verify/tlv/tlvmanual.ps.gz

3. Uncompress file rules.zip provided with this distribution (don't use the one from TLV's website!) into <my_path>\TLV\

4. If everything worked fine, dir <my_path>\TLV\ now contains:

- a file: tlvcygwin.exe

- a directory: rules/

5. Set the following environment variables:

- TLV_RULES=<my_path>\TLV\rules\Rules.tlv

- TLV_PATH=<my_path>\TLV\rules\

- We also recommend to set the PATH environment variable so to include <my_path>\TLV\

6. TLV should be now installed. (Re)Start Cygwin and type:

> tlvcygwin.exe

Hopefully, you get (something similar to) this message:

Loading Util.tlv $Revision: 4.3 $

Loading MCTL.tlv $Revision: 4.3 $

Loading MCTLS.tlv $Revision: 4.1 $

Loading TESTER.tlv $Revision: 4.2 $

Loading MCsimple.tlv $Revision: 4.2 $

Loading SIMULATE $Revision: 4.2 $

Loading Floyd.tlv $Revision: 4.1 $

Loading Abstract.tlv $Revision: 4.2 $

Loading deductive.tlv $Revision: 4.2 $

Warning! : No input file has been specified

But you can define program variables yourself, for example:

x : boolean;

y : 1..4;

Loaded rules file /Users/patrizi/Library/Tlv/rules/Rules.tlv.

Your wish is my command ...

8. Type > quit; to exit the application

7. That's it!

Write your specification and check it by typing command: >tlvcygwin.exe comp-inv.pf <my_specification_file>

ON A LINUX or OSX PLATFORM:

1. Download TLV source files for Linux at http://www.wisdom.weizmann.ac.il/~verify/tlv/src.tar.Z and uncompress them in any directory, say <my_src_path>;

1b. You can also download (recommended) the TLV manual at http://www.wisdom.weizmann.ac.il/~verify/tlv/tlvmanual.ps.gz

2. Move to <my_source_path>/src and type: > make

3. If everything worked fine, <my_source_path>/src should now contain (among others) executable file:

- tlv

4. Move (or copy) it to dir <my_path>/TLV/

You can now remove dir <my_src_path>/src

3. Uncompress file rules.zip provided with this distribution (don't use the one from TLV's website!) into <my_path>/TLV

4. Dir <my_path>/TLV/ should contain:

- a (executable) file: tlv

- a directory: rules/

5. Set the following environment variables:

- TLV_RULES=<my_path>/TLV/rules/Rules.tlv

- TLV_PATH=<my_path>/TLV/rules/

- We also recommend to set the PATH environment variable so to include <my_path>/TLV/

6. TLV should be now installed. (Re)Start your shell (to update environment variables) and type:

> tlv