Running ProB from source

Revision as of 10:04, 12 January 2018 by Michael Leuschel (talk | contribs)

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:

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:

alias tests='cd $NEWPROBDIR; rlwrap $SICSTUSDIR/bin/sicstus -Dprob_safe_mode=true -l $NEWPROBDIR/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

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)