User:Philipp Koerner: Difference between revisions

Distributed Model Checking

jasper ProB

TODO: test 64 bit architecture (64 bit build .so files) //test required libraries

1. Minimalistic Jasper Implementation

required files (cant run ProB, see below for more information)

tree ./lib/

lib

├── libspnative.so

├── libsprt4-2-0.so

├── sicstus-4.2.0

│ └── bin

│ ├── jasper.jar

│ └── sprt.sav

└── sp-4.2.0 -> .

classpath: .../lib/sicstus-4.2.0/bin/jasper.jar

The SICStus tries to load the library libspnative.so if not loaded yet. These files have to be located two subdirectories underneath the .jar file.

see: SICStus.java ll. 540 - 544

• // jasper.jar is

• // <installpath>/lib/sicstus-<version>/bin/jasper.jar

• // lib path is <installpath>/lib

• // This does the trick:

• File libPath = jarFile.getParentFile().getParentFile().getParentFile();

The library file spnative requires the file libsprt4-2-0.so.

ldd -v libspnative.so

• linux-gate.so.1 => (0x0018d000)

• libsprt4-2-0.so => /path/to/libspnative.so/./sp-4.2.0/libsprt4-2-0.so (0x00e4e000)

• libc.so.6 => /lib/libc.so.6 (0x00389000)

• libdl.so.2 => /lib/libdl.so.2 (0x0055a000)

• libm.so.6 => /lib/libm.so.6 (0x00110000)

• libpthread.so.0 => /lib/libpthread.so.0 (0x0095e000)

• librt.so.1 => /lib/librt.so.1 (0x00310000)

• /lib/ld-linux.so.2 (0x4cf5b000)

Hence the link to the directory itself, so spnative may find sprt4-2-0. The libraries may also depend on the architecture since a 64 bit ubuntu doesn't run a 32 bit package.

Creating a SICStus object requires the sprt.sav file, the SICStus Runtime Library or bootfile.

2. Running ProB.sav via Jasper // WARNING! Unstable yet. Requires testing. // Warning was caused by extra libraries. May be solved now? (META INF of probcli.sav)

Trying to run the ProB file by calling SICStus.restore() fails because some libraries aren't in the minimalistic Jasper configuration.

[philipp@netbook prolog]$ java ProBTest error(existence_error(source_sink,library(system(codesio))),existence_error(restore(probcli.sav),1,file,library(system(codesio)),0)) at se.sics.jasper.SICStus.handleQueryResult(SICStus.java:1292) at se.sics.jasper.SICStus.restore(SICStus.java:1040) at ProBTest.main(ProBTest.java:25)

It requires some glibc2.7 libraries located in /path/to/spnative/sicstus<version>/library/x86-linux-glibc2.7/ (probably other libraries for a 64 bit system (other path, too?))

• 1. META_INFO 1

• 1. FILE: "probcli.sav"

• 1. FR: "fastrw"

• 1. FR: "random"

• 1. FR: "clpfd"

• 1. FR: "timeout"

• 1. FR: "codesio"

• 1. META_INFO END

tree ./newlib/

├── libspnative.so

├── libsprt4-2-0.so

├── sicstus-4.2.0

│ ├── bin

│ │ ├── jasper.jar

│ │ └── sprt.sav

│ └── library

│ └── x86-linux-glibc2.7

│ ├── clpfd.so

│ ├── codesio.so

│ ├── fastrw.so

│ ├── random.so

│ └── timeout.so

└── sp-4.2.0 -> .

To ensure everything is working smoothly, one should copy every single library.

Running ProB via Jasper requires the environmental variable $PROB_HOME. This should be set to the path where the probcli.sav file is located (may require to run 'make' first to generate it).

Next thing to do is to write a basic Java code. Imports should look like this:

import se.sics.jasper.SICStus; import se.sics.jasper.Query; import java.util.HashMap;

We need an instance of a SICStus, a Query and a Map object. A useful code fragment:

try sp = new SICStus(String[] args, null); sp.restore("file.sav"); query = sp.openPrologQuery("predicate(...).", map); query.nextSolution() <=> solution in map catch Exception e.

The second argument of creating a new SICStus object is a String and it is (was?) used to set up the bootpath to sprt.sav. Since our sprt.sav is in the correct place anyway, we don't need one.

A query that should be made like this: set_search_pathes(A,B). This may be done via sp.query("set_search_pathes(A,B)"); or query = sp.openPrologQuery("set_search_pathes(A,B)"); query.nextSolution();

Note that openPrologQuery does NOT execute the query until a solution is called.