User:Philipp Koerner: Difference between revisions

m (adding information of probcli.sav)
No edit summary
 
(One intermediate revision by the same user not shown)
Line 1: Line 1:
[[Distributed Model Checking]]
jasper ProB
jasper ProB


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


--------------
--------------
Line 11: Line 14:
1. Minimalistic Jasper Implementation
1. Minimalistic Jasper Implementation


required files
required files (cant run ProB, see below for more information)
--------------
--------------
tree ./lib/
tree ./lib/
Line 96: Line 99:


2. Running ProB.sav via Jasper
2. Running ProB.sav via Jasper
WARNING! Unstable yet. Requires testing.
// 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 due to a library that isn't in the minimalistic configuration.
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
[philipp@netbook prolog]$ java ProBTest
Line 108: Line 112:




It requires some glibc2.7 libraries located in /path/to/spnative/sicstus<version>/library/x86-linux-glibc2.7/
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?))


--------------
--------------
Line 114: Line 118:
*# META_INFO 1
*# META_INFO 1


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


*# FR: "fastrw"
*# FR: "fastrw"
Line 164: Line 168:
--------------
--------------


To ensure everythings working smoothly, one should copy every single library.
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).
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:
Next thing to do is to write a basic Java code. Imports should look like this:
Line 182: Line 186:
sp.restore("file.sav");
sp.restore("file.sav");
query = sp.openPrologQuery("predicate(...).", map);
query = sp.openPrologQuery("predicate(...).", map);
-> query.nextSolution() <=> solution in map
query.nextSolution() <=> solution in map
catch Exception e.
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.
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:
A query that should be made like this:
set_search_pathes(A,B).
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.

Latest revision as of 10:16, 26 January 2018

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.