Running ProB from source: Difference between revisions

ProB Source Code

The kernel of ProB is written in Prolog and you can download the latest Prolog sourcecode snapshot from: https://stups.hhu-hosting.de/downloads/prob/source/

You may also wish to obtain related Java sources:

• The source code for the ProB parsers (B, LTL, ...) can be obtained from: https://github.com/hhu-stups/probparsers.
• The ProB2-Java-API (also known as ProB2) source code can be obtained from: https://github.com/hhu-stups/prob2_kernel.
• The ProB2-Java-FX UI source code can be obtained from: https://github.com/hhu-stups/prob2_ui.
• The B to Java value translator can also be useful and is a separate project: https://github.com/hhu-stups/value-translator.
• The Plugin for Rodin is also a separate project: https://gitlab.cs.uni-duesseldorf.de/general/stups/prob_rodin_plugin.
• The Alloy to B translator is here: https://github.com/hhu-stups/alloy2b.
• The TLC4B B to TLA+ translator is here: https://gitlab.cs.uni-duesseldorf.de/general/stups/tlc4b.
• The TLA2B TLA+ to B translator is her: https://gitlab.cs.uni-duesseldorf.de/general/stups/tla2bAST.

Running ProB from Prolog

You first need to download and install SICStus Prolog. Evaluation licenses (30-days) are available. We currently compile with SICStus 4.6.0 (as of January 2021).

You need the password to download SICStus then run sudo ./InstallSICStus and provide the site name, license code and expiration date. Be sure to add the SICStus binaries to your PATH.

Probably you should also install a recent Active Tcl distribution, in particular on macOS.

Now, you need the ProB Prolog sources.

Now, add the following to your .bash_login file (at least on Mac OS; supposing you cloned the Git repository into ~/git_root):

export PROBDIR=~/git_root/prob_prolog
export PROB_SOURCE_DIR=$PROBDIR/src
alias prob='cd $PROB_SOURCE_DIR; sicstus -Dprob_profile=true -l $PROB_SOURCE_DIR/prob_tcltk.pl --goal "go."'

Now, you can simply start ProB from the command-line and from source with prob.

To start the Unit Test REPL, add the following to your .bash_login file (at least on Mac OS):

alias test='cd $PROBDIR; rlwrap sicstus -Dprob_safe_mode=true -l $PROB_SOURCE_DIR/test_runner.pl --goal "test_repl."'

(It is recommended to install rlwrap so that you get a history of your commands. If you don't want to install rlwrap just remove it from the line above.)

Before using ProB for the first time from source you should build the extensions. The minimal extensions are counter and user_signal. You can build them using

cd extensions/counter
make
cd ../user_signal
make

You could also build all extensions at once by going to the top of the prob_prolog tree (i.e., the directory containing src and lib as sub-directories) and then type

make

On Mac you may have to add a symbolic link to gawk in order to build the ProZ fuzz extension:

sudo ln -s /usr/bin/awk /usr/bin/gawk

Now you can start the testing console using test. You can e.g. type the number of a unit test to run it, or a test category such as tickets to run all tests in that category.

Running the Prolog Tests

All Prolog tests are stored as facts in the file test cases.pl. Every test has

• an identifier (a number); the last test added has the highest number
• a non-empty list of categories (such as unit, tickets,...)
• the test itself: the parameters to probcli needed to run the test
• a textual description of the test

There is a specific test_runner.pl file for running all Prolog unit and integration tests. The test_runner also provides a REPL (read-eval-print-loop) for running tests and collection of tests.

Supposing you have set the variable PROBDIR (see above) and have the rlwrap tool, you can define the following alias (e.g., in your .bash_login file on Mac OS X):

alias test='cd $PROBDIR; rlwrap sicstus -Dprob_safe_mode=true -l $PROBDIR/src/test_runner.pl --goal "test_repl."'

Now you can start the test runner:

$ test
...
SICStus 4.2.3 (x86_64-darwin-11.4.2): Fri Oct  5 15:58:35 CEST 2012
Licensed to SP4phil-fak.uni-duesseldorf.de
TEST ==> last.
...
All tests successful.
Walltime: 100 ms

Some useful commands are:

• last to run the last test added to testcases.pl
• all to run all tests
• cat to list all categories of tests (e.g., cbc, cbc_deadlock,...)
• cbc, cbc_deadlock, tickets, ... : to run all tests in that category
• type in a number to run the specific test with that number (see testcases.pl)
• type in a range m-n to run all tests in that range
• v or vv to switch to verbose or very verbose mode
• q to quit the test runner (and stay in Prolog)
• x to quit the test runner and Prolog
• debug to switch on Prolog debug mode
• trace to force Prolog to start tracing as soon as an error occurs (if you have switched to debug above then you will be able to inspect the Prolog goal stack)

Starting ProB Tcl/Tk

Go into the prob_prolog directory and type:

sicstus -Dprob_profile=true -l src/prob_tcltk.pl --goal "go."'

Starting probcli command-line version

To start probcli from source define this alias, where SICSTUSDIR must be defined:

alias probsli='rlwrap $SICSTUSDIR/bin/sicstus -l src/prob_cli.pl --goal "go_cli." -a'

You can now use probsli just like probcli, e.g.,

probsli M.mch --model-check

Running ProB tests from source

Starting test runner from source: First define the alias, where PROBDIR and SICSTUSDIR must be defined:

alias tests='cd $PROBDIR; rlwrap $SICSTUSDIR/bin/sicstus -Dprob_safe_mode=true -l $PROBDIR/src/test_runner.pl --goal "test_repl." -- '

Now you can start the test runner like this:

tests

or you can already specify tests to be run:

tests last

ProB Prolog compile time flags

By giving sicstus a command-line option -Dflag=true you can set certain compile time flags, namely:

prob_profile (enables B operation profiling to be displayed in ProB Tcl/Tk in Debug menu)
prob_safe_mode (performs additional checking, in particular that ASTs are well-formed)
prob_data_validation_mode  (deprecated, replaced by DATA_VALIDATION preference)
prob_release (removes certain tests from the code)
no_terminal_colors (disable terminal colors)
debug_kodkod (write dot files for kodkod interval analysis)
no_wd_checking (disable WD checking for function application)