Tested versions

OS / CVC / LP3 Version

Java
OpenJDK

jdk.java.net

Java Version
JDK

Oracle.com/java

Java Version
JDK

Oracle.com/java

Ubuntu 20.0.4 /

cvc4-1.8-x86_64-linux-opt / V1.1

16.0.1

O.K.

11.0.11

O.K.

16.0.1

O.K.

Window 10 /

cvc4-1.8-win64-opt.exe / V1.1

16.0.1

O.K.

11.0.11

O.K.

16.0.1

O.K.

Mac OS 11

Cvc4 / V1.1

16.0.1

O.K.

11.0.11

O.K.

16.0.1

O.K.


Prereq

  1. Get one of the supported java packages (see matrix). You need the jdk Version, the jre does not work.
  2. Download CVC4 (https://cvc4.github.io/downloads.html )and if necessary follow the installation instructions from the user manual (http://cvc4.cs.stanford.edu/wiki/User_Manual).
  3. Download the packages under Releases (right pages side) from github.com/Sinnloshausen/LP3Verif
    LP3Verif.zip (compiled java)
    Source Code (zip, containes protocol examples)
    and unpack into a directory of your choice.
  4. In the unzipped LP3Verif folder edit the tool.config file with the editor of your choice.
    Edit the solver path to the absolute path where your CVC4 binaries are located. If necessary edit the name of the solver, e.g., "cvc4.exe" for windows.

Under Windows you can use the unix path sign / or \\.

Then edit the smt2 path and name to a file of your choice. This file will be used by the smt solver and can contain additional
tracing/debug information for LP3Verif.

Doublecheck that you have all paths ending with a /.
 

Run

Use one of the tested java versions to run LP3Verif with any of the
protocols files.

Depending on your operating system you can now create a shell/batch script to start the executable .jar file:

The command java -jar "LP3Verif.jar" starts LP3Verif in interactive mode where a command line prompt will ask for a path to an .lp3 file.

Calling LP3Verif with the additional argument -lp3 path/file.lp3 directly starts the verification of the specified .lp3 file.

e.g. Unix
jdk-11.0.11/bin/java -jar LP3Verif.jar -lp3 LP3Verif-1.1/Protocols/feelingbased.lp3

e.g. MacOS
jdk-11.0.11/Contents/Home/bin/java -jar LP3Verif.jar -lp3 LP3Verif-1.1/Protocols/feelingbased.lp3

e.g. Windows:
c:\users\elvis\lp3\jdk-11.0.11\bin\java -jar LP3Verif.jar -lp3 LP3Verif-1.1\Protocols\beresford.lp3
 

Protocols