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
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 close the application
7. That's it! Write your specification and check it by typing:
> tlv comp-inv.pf <my_specification_file>