Running ProB from source: Difference between revisions

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, where PROBDIR and SICSTUSDIR are 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)