ProB Documentation - User contributions [en]

Distributed Model Checking

2018-01-26T13:19:46Z

Philipp Koerner: add new preference

Distributed Model Checking allows to check invariants and deadlock-freedom (and assertions) with additional computational power. The distributed version of ProB is named ''distb''. In the following, we will document how to run it.

== Overview ==

''distb'' consists of three components.

* A master which coordinates the model checking process. Per distributed model checking, it must run exactly once.
* A proxy which coordinates workers on its machine. It should run (at least, but usually) once per participating machine.
* A worker which does the actual work. A good number of workers usually is close to the amount of available (physical) CPU cores of a participating machine.

== Setting up shared memory ==

It might be necessary to increase the limits of how much shared memory may be allocated, both per segment and overall. This is, to our knowledge, required for Mac OS X and older versions of Ubuntu. You can view the limits by running:

<nowiki>sysctl -a | grep shm</nowiki>

Per default, recent versions of Ubuntu set the following values:

<nowiki>kernel.shmall = 18446744073692774399
kernel.shmmax = 18446744073692774399
kernel.shmmni = 4096</nowiki>

On Mac OS X, the keys might be different and you can set them by executing:

<nowiki>sudo sysctl -w kern.sysv.shmmax=18446744073692774399
sudo sysctl -w kern.sysv.shmseg=4096
sudo sysctl -w kern.sysv.shmall=18446744073692774399</nowiki>

== Running ''distb'' ==

Run once per machine:

<nowiki>/path/to/prob/lib/proxy $MASTER_IP 5000 $IP 30 $LOGFILE_PROXY $PROXY_NUMBER</nowiki>

Note that on Linux systems you might need to set the LD_LIBRARY_PATH variable to find the ZeroMQ libraries beforehand (for all components):

<nowiki>export LD_LIBRARY_PATH=/path/to/prob/lib</nowiki>

Run once per model checking:

<nowiki>/path/to/prob/probcli -bf -zmq_master <unique identifier> $MODEL</nowiki>

Run as many workers as you want:

<nowiki>/path/to/prob/probcli -zmq_worker <unique identifier> &</nowiki>

== Additional Preferences ==

You can fine-tune the following parameters by adding -p NAME VALUE to the corresponding call (e.g., ./probcli -zmq_worker worker1 -p port 5010 -p max_states_in_memory 100) :

{| class="wikitable"
! Parameter !! Default !! Description !! Applicable for...
|-
|port || 5000 || TCP ports should be used starting at... || master, worker
|-
| ip || localhost || IP of the master component || master
|-
| max_states || 0 || how many states should be checked at most (0 means all) || master
|-
| tmpdir || /tmp/ || directory for temporary files || master, worker
|-
| logdir || ./distb-logs || directory for log output (must exist) || master, worker
|-
| proxynumber || 0 || which proxy should the component connect to (if multiple run on the same machine) || worker
|-
| max_states_in_memory || 1000 || how many states may be kept in memory before written into a database || worker
|-
| hash_cycle || 25 || minimum amount of milliseconds that has to pass between hash code updates from the master || master
|}

Distributed Model Checking

2018-01-26T10:35:39Z

Philipp Koerner: fix table

Distributed Model Checking allows to check invariants and deadlock-freedom (and assertions) with additional computational power. The distributed version of ProB is named ''distb''. In the following, we will document how to run it.

== Overview ==

''distb'' consists of three components.

* A master which coordinates the model checking process. Per distributed model checking, it must run exactly once.
* A proxy which coordinates workers on its machine. It should run (at least, but usually) once per participating machine.
* A worker which does the actual work. A good number of workers usually is close to the amount of available (physical) CPU cores of a participating machine.

== Setting up shared memory ==

It might be necessary to increase the limits of how much shared memory may be allocated, both per segment and overall. This is, to our knowledge, required for Mac OS X and older versions of Ubuntu. You can view the limits by running:

<nowiki>sysctl -a | grep shm</nowiki>

Per default, recent versions of Ubuntu set the following values:

<nowiki>kernel.shmall = 18446744073692774399
kernel.shmmax = 18446744073692774399
kernel.shmmni = 4096</nowiki>

On Mac OS X, the keys might be different and you can set them by executing:

<nowiki>sudo sysctl -w kern.sysv.shmmax=18446744073692774399
sudo sysctl -w kern.sysv.shmseg=4096
sudo sysctl -w kern.sysv.shmall=18446744073692774399</nowiki>

== Running ''distb'' ==

Run once per machine:

<nowiki>/path/to/prob/lib/proxy $MASTER_IP 5000 $IP 30 $LOGFILE_PROXY $PROXY_NUMBER</nowiki>

Note that on Linux systems you might need to set the LD_LIBRARY_PATH variable to find the ZeroMQ libraries beforehand (for all components):

<nowiki>export LD_LIBRARY_PATH=/path/to/prob/lib</nowiki>

Run once per model checking:

<nowiki>/path/to/prob/probcli -bf -zmq_master <unique identifier> $MODEL</nowiki>

Run as many workers as you want:

<nowiki>/path/to/prob/probcli -zmq_worker <unique identifier> &</nowiki>

You can fine-tune the following parameters by adding -p NAME VALUE to the corresponding call (e.g., ./probcli -zmq_worker worker1 -p port 5010 -p max_states_in_memory 100) :

{| class="wikitable"
! Parameter !! Default !! Description !! Applicable for...
|-
|port || 5000 || TCP ports should be used starting at... || master, worker
|-
| ip || localhost || IP of the master component || master
|-
| max_states || 0 || how many states should be checked at most (0 means all) || master
|-
| tmpdir || /tmp/ || directory for temporary files || master, worker
|-
| logdir || ./distb-logs || directory for log output (must exist) || master, worker
|-
| proxynumber || 0 || which proxy should the component connect to (if multiple run on the same machine) || worker
|-
| max_states_in_memory || 1000 || how many states may be kept in memory before written into a database || worker
|}

Distributed Model Checking

2018-01-26T10:35:14Z

Philipp Koerner: startup

Distributed Model Checking allows to check invariants and deadlock-freedom (and assertions) with additional computational power. The distributed version of ProB is named ''distb''. In the following, we will document how to run it.

== Overview ==

''distb'' consists of three components.

* A master which coordinates the model checking process. Per distributed model checking, it must run exactly once.
* A proxy which coordinates workers on its machine. It should run (at least, but usually) once per participating machine.
* A worker which does the actual work. A good number of workers usually is close to the amount of available (physical) CPU cores of a participating machine.

== Setting up shared memory ==

It might be necessary to increase the limits of how much shared memory may be allocated, both per segment and overall. This is, to our knowledge, required for Mac OS X and older versions of Ubuntu. You can view the limits by running:

<nowiki>sysctl -a | grep shm</nowiki>

Per default, recent versions of Ubuntu set the following values:

<nowiki>kernel.shmall = 18446744073692774399
kernel.shmmax = 18446744073692774399
kernel.shmmni = 4096</nowiki>

On Mac OS X, the keys might be different and you can set them by executing:

<nowiki>sudo sysctl -w kern.sysv.shmmax=18446744073692774399
sudo sysctl -w kern.sysv.shmseg=4096
sudo sysctl -w kern.sysv.shmall=18446744073692774399</nowiki>

== Running ''distb'' ==

Run once per machine:

<nowiki>/path/to/prob/lib/proxy $MASTER_IP 5000 $IP 30 $LOGFILE_PROXY $PROXY_NUMBER</nowiki>

Note that on Linux systems you might need to set the LD_LIBRARY_PATH variable to find the ZeroMQ libraries beforehand (for all components):

<nowiki>export LD_LIBRARY_PATH=/path/to/prob/lib</nowiki>

Run once per model checking:

<nowiki>/path/to/prob/probcli -bf -zmq_master <unique identifier> $MODEL</nowiki>

Run as many workers as you want:

<nowiki>/path/to/prob/probcli -zmq_worker <unique identifier> &</nowiki>

You can fine-tune the following parameters by adding -p NAME VALUE to the corresponding call (e.g., ./probcli -zmq_worker worker1 -p port 5010 -p max_states_in_memory 100) :

{| class="wikitable"
! Parameter !! Default !! Description !! Applicable for...
|-
|port || 5000 || TCP ports should be used starting at... || master, worker
|-
| ip || localhost || IP of the master component || master
|-
| max_states || 0 || how many states should be checked at most (0 means all) || master
|-
| tmpdir || /tmp/ || directory for temporary files || master, worker
|-
logdir || ./distb-logs || directory for log output (must exist) || master, worker
|-
proxynumber || 0 || which proxy should the component connect to (if multiple run on the same machine) || worker
|-
max_states_in_memory || 1000 || how many states may be kept in memory before written into a database || worker
|}

Distributed Model Checking

2018-01-26T10:23:20Z

Philipp Koerner: add distributed model checking page

User:Philipp Koerner

2018-01-26T10:16:16Z

Philipp Koerner:

[[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?))

--------------

*# META_INFO 1

*# FILE: "probcli.sav"

*# FR: "fastrw"

*# FR: "random"

*# FR: "clpfd"

*# FR: "timeout"

*# FR: "codesio"

*# 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.

User:Philipp Koerner

2011-11-28T14:46:41Z

Philipp Koerner: added query-handling

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?))

--------------

*# META_INFO 1

*# FILE: "probcli.sav"

*# FR: "fastrw"

*# FR: "random"

*# FR: "clpfd"

*# FR: "timeout"

*# FR: "codesio"

*# 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.

User:Philipp Koerner

2011-11-28T13:03:31Z

Philipp Koerner: adding information of probcli.sav

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/

--------------

*# META_INFO 1

*# FILE: "/home/philipp/Documents/prolog/probcli.sav"

*# FR: "fastrw"

*# FR: "random"

*# FR: "clpfd"

*# FR: "timeout"

*# FR: "codesio"

*# 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 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).

User:Philipp Koerner

2011-11-28T12:53:22Z

Philipp Koerner: Jasper ProB Documentation

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).