User:Philipp Koerner: Difference between revisions

jasper ProB

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

1. Minimalistic Jasper Implementation

required files

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.

Trying to run the ProB file by calling SICStus.restore() fails due to a library that isn't in the minimalistic 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/

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 everythings 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 is: set_search_pathes(A,B).