Running ProB from source: Difference between revisions

(Created page with " Starting ProB Tcl/Tk: sicstus -Dprob_profile=true -l src/prob_tcltk.pl --goal "go."' Starting probcli from source: alias probsli='rlwrap $SICSTUSDIR/bin/sicstus -l src/pro...")
 
No edit summary
Line 1: Line 1:


Starting ProB Tcl/Tk:
== Starting ProB Tcl/Tk ==
Go into the prob_prolog directory and type:
  sicstus -Dprob_profile=true -l src/prob_tcltk.pl --goal "go."'
  sicstus -Dprob_profile=true -l src/prob_tcltk.pl --goal "go."'


Starting probcli from source:
== 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'
  alias probsli='rlwrap $SICSTUSDIR/bin/sicstus -l src/prob_cli.pl --goal "go_cli." -a'
probsli ...
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:
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." -- '
  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
  tests last




ProB Prolog compile time flags:
== ProB Prolog compile time flags ==
  prob_profile (enables B operation profiling to be displayed in ProB Tcl/Tk in Debug menu)
  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_safe_mode (performs additional checking, in particular that ASTs are well-formed)

Revision as of 10:04, 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:

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)