Installing and running LCT

This page explains how to install and use LCT in the computer rooms of the VUB (tested in room E.1.4).

A VM exists with LCT and other tools pre-installed (http://soft.vub.ac.be/~cderoove/sq/testing-ubuntu-12.10-desktop-i386.zip, username: ubuntu, password: reverse), but there is unfortunately not enough room in the computer rooms (neither on the home directory nor in /tmp) to download it and unzip it. However, the manual installation is not that hard and probably takes less time than downloading the entire VM.

1 Installation

Typing the following commands will install LCT on those rooms (no adaptation of path needed):

cd /tmp
wget http://www.tcs.hut.fi/Software/lime/LimeTB-2.2.0.tar.gz
tar xvf LimeTB-2.2.0.tar.gz
export PATH=$PATH:/tmp/LimeTB-2.2.0/bin
cd LimeTB-2.2.0/dependencies/solvers
wget http://fmv.jku.at/boolector/boolector-1.4-ffc2089-100608.tar.gz
wget http://fmv.jku.at/picosat/picosat-936.tar.gz
export JAVA_HOME=/usr/lib/jvm/java-7-openjdk-amd64
export JRELIBPATH=$JAVA_HOME/jre/lib
make

To test if the installation succeeded, launch limegui. However, don't use limegui to use LCT as there is a bug that prevents you from correctly running LCT with it.

2 Path adaptation

Once LCT is installed, if you open a new terminal you will have to adapt the paths again. To avoid that, you can edit the ~/.bashrc file and add this at the end:

export JAVA_HOME=/usr/lib/jvm/java-7-openjdk-amd64
export JRELIBPATH=$JAVA_HOME/jre/lib
export PATH=$PATH:/tmp/LimeTB-2.2.0/bin

However, you will still need to install LCT at each session as it is stored in a temporary directory.

3 Usage

To use LCT, first launch the server in a terminal:

LCTserver

Then, open another terminal, place yourself in the directory where you have the .java file you want to run with LCT, and type the following:

LCTcompile File.java
LCTinstrument File
cd output
LCTrun File all

You can test it on the following program for example.

import fi.hut.ics.lime.tester.LCT;

public class Foo
{
    public static void main(String[] args) {
        int x = LCT.getInteger();
        System.out.println(x);
    }
}

4 Importing in Eclipse

To import LCT in Eclipse, launch Eclipse and do the following steps.

  1. File -> Import -> General -> Existing Projects into Workspace -> Next.
  2. Choose /tmp/LimeTB-2.2.0/ as root directory and select only LCT in the projects list, then click Finish.
  3. Import the needed dependencies: Right click on LCT -> Properties -> Java Build Path -> Add External JARs
    • add all the JARs in /tmp/LimeTB-2.2.0/lib/external
    • add /usr/share/java/junit.jar

5 Exporting a JAR

If you want to test modifications done on LCT source code, do the following:

  1. File -> Export -> Java -> JAR file -> Next.
  2. Check the LCT box, and set the export destination to /tmp/LimeTB-2.2.0/lib/lime/LCT-2.2.0.jar/
  3. Click Finish. Confirm that you want to override the existing file. You might get a warning that the JAR file was exported with warning, but you can just ignore that.

On the next run of LCT, it will use your modified version. If you modified code in the server, don't forget to relaunch LCTserver as well.

Last update: 2015-10-02T12:58:19+02:00