Running ProB from source: Difference between revisions

Source Code

You can download the latest Prolog sourcecode snapshot from: http://www3.hhu.de/stups/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 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://github.com/hhu-stups/prob-rodinplugin.

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)