Running ProB from source: Difference between revisions

No edit summary
Line 5: Line 5:


== Starting probcli command-line version ==
== Starting probcli command-line version ==
To start probcli from source define this alias:
To start probcli from source define this alias, where <tt>SICSTUSDIR</tt> must be defined:
  alias probsli='rlwrap $SICSTUSDIR/bin/sicstus -l src/prob_cli.pl --goal "go_cli." -a'
  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.,
You can now use probsli just like probcli, e.g.,
Line 12: Line 12:
== Running ProB tests from source ==
== Running ProB tests from source ==
Starting test runner from source:
Starting test runner from source:
First define the alias, where <tt>PROBDIR</tt> and <tt>SICSTUSDIR</tt> are defined:
First define the alias, where <tt>PROBDIR</tt> and <tt>SICSTUSDIR</tt> must be defined:
  alias tests='cd $PROBDIR; rlwrap $SICSTUSDIR/bin/sicstus -Dprob_safe_mode=true -l $PROBDIR/src/test_runner.pl --goal "test_repl." -- '
  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:
Now you can start the test runner like this:

Revision as of 10:06, 12 January 2018

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)