m (Moved category to bottom) |
|||
(40 intermediate revisions by 2 users not shown) | |||
Line 1: | Line 1: | ||
== ProB Source Code == | |||
{{ProBSourceCode}} | |||
== | == Running ProB from Prolog == | ||
You | You first need to download and install [https://sicstus.sics.se/ SICStus Prolog]. Evaluation licenses (30-days) are available. We currently compile with SICStus 4.6.0 (as of January 2021), but the source code is compatible with older versions as well (SICStus 4.3.2 or later). | ||
You | You need the password to download SICStus then run <tt>sudo ./InstallSICStus</tt> and provide the site name, license code and expiration date. Be sure to add the SICStus binaries to your PATH. | ||
== Starting ProB Tcl/Tk == | |||
Now, you need to clone or download the [http://www3.hhu.de/stups/downloads/prob/source/ ProB Prolog sources]. | |||
=== Building ProB Extensions === | |||
Before using ProB for the first time from source you should build the extensions. The minimal extensions are counter, myheap and user_signal. You can build them using | |||
cd extensions/counter | |||
make | |||
cd ../user_signal | |||
make | |||
cd ../myheap | |||
make | |||
You will also need the ProB parser, which can be downloaded or updated using the command | |||
./gradlew updateParser | |||
You could also build all extensions at once by going to the top of the prob_prolog tree (i.e., the directory containing src and lib as sub-directories) and then type | |||
make | |||
An alternative is to download ProB from the [[Download|download page]], unzip the archive and copy all the files in the lib folder of the archive to the lib folder of your Prolog source code, containing files such as (the file extension of some of these files varies with the operating system: bundle for macOS, dll for Windows and so for Linux): | |||
* probcliparser.jar | |||
* counter.bundle | |||
* user_signal.bundle | |||
* myheap.bundle | |||
* ltlc.bundle | |||
=== Starting ProB Tcl/Tk === | |||
Probably you should first install a recent Active Tcl distribution, in particular on macOS. Check the [[Download|download page]] for which version is required or recommended. | |||
You can then start ProB Tcl/Tk by changing into the prob_prolog directory of the Prolog sources 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 command-line version == | To simplify starting ProB, add the following to your <tt>.bash_login</tt> file (or similar configuration file; supposing you cloned the Git repository into ~/git_root): | ||
To start probcli from source define this alias, where <tt>SICSTUSDIR</tt> must be defined: | |||
alias probsli='rlwrap $SICSTUSDIR/bin/sicstus -l | export PROBDIR=~/git_root/prob_prolog | ||
export PROB_SOURCE_DIR=$PROBDIR/src | |||
alias prob='cd sicstus -Dprob_profile=true -l $PROB_SOURCE_DIR/prob_tcltk.pl --goal "go."' | |||
Now, you can simply start ProB from the command-line and from source with the <tt>prob</tt> alias command. | |||
=== Starting probcli command-line version === | |||
The command-line version of ProB does not require a Tcl/Tk distribution. | |||
To start probcli from source define this alias, where <tt> PROB_SOURCE_DIR </tt> and <tt>SICSTUSDIR</tt> must be defined: | |||
alias probsli='rlwrap $SICSTUSDIR/bin/sicstus -l $PROB_SOURCE_DIR/prob_cli.pl --goal "go_cli." -a' | |||
(It is recommended to install rlwrap so that you get a history of your commands. If you don't want to install rlwrap just remove it from the line above.) | |||
You can now use probsli just like probcli, e.g., | You can now use probsli just like probcli, e.g., | ||
probsli M.mch --model-check | probsli M.mch --model-check | ||
or | |||
probsli --repl | |||
=== Running the Prolog Tests === | |||
All Prolog tests are stored as facts in the file <tt>test cases.pl</tt>. | |||
Every test has | |||
* an identifier (a number); the last test added has the highest number | |||
* a non-empty list of categories (such as unit, tickets,...) | |||
* the test itself: the parameters to <tt>probcli</tt> needed to run the test | |||
* a textual description of the test | |||
There is a specific <tt>test_runner.pl</tt> file for running all Prolog unit and integration tests. The test_runner also provides a REPL (read-eval-print-loop) for running tests and collection of tests. | |||
To start the Unit Test REPL, add the following to your <tt>.bash_login</tt> file (at least on Mac OS): | |||
alias tests='cd $PROBDIR; rlwrap sicstus -Dprob_safe_mode=true -l $PROB_SOURCE_DIR/test_runner.pl --goal "test_repl."' | |||
(It is recommended to install rlwrap so that you get a history of your commands. If you don't want to install rlwrap just remove it from the line above.) | |||
Now you can start the test runner like this: | Now you can start the test runner like this: | ||
tests | tests | ||
or you can already specify tests to be run: | or you can already specify tests to be run: | ||
tests last | tests last | ||
You can also type the number of a unit test to run, or a test category such as <tt>tickets</tt> to run all tests in that category. | |||
Here is a sample sesssion of running the test REPL: | |||
<pre> | |||
$ tests | |||
... | |||
SICStus 4.2.3 (x86_64-darwin-11.4.2): Fri Oct 5 15:58:35 CEST 2012 | |||
Licensed to SP4phil-fak.uni-duesseldorf.de | |||
TEST ==> last. | |||
... | |||
All tests successful. | |||
Walltime: 100 ms | |||
</pre> | |||
Some useful commands in the REPL are: | |||
* last to run the last test added to <tt>testcases.pl</tt> | |||
* all to run all tests | |||
* cat to list all categories of tests (e.g., cbc, cbc_deadlock,...) | |||
* cbc, cbc_deadlock, tickets, ... : to run all tests in that category | |||
* type in a number to run the specific test with that number (see <tt>testcases.pl</tt>) | |||
* type in a range m-n to run all tests in that range | |||
* v or vv to switch to verbose or very verbose mode | |||
* q to quit the test runner (and stay in Prolog) | |||
* x to quit the test runner and Prolog | |||
* debug to switch on Prolog debug mode | |||
* trace to force Prolog to start tracing as soon as an error occurs (if you have switched to debug above then you will be able to inspect the Prolog goal stack) | |||
== ProB Prolog compile time flags == | == ProB Prolog compile time flags == | ||
Line 36: | Line 115: | ||
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) | ||
prob_release (removes certain tests from the code) | prob_release (removes certain tests from the code) | ||
no_terminal_colors (disable terminal colors) | no_terminal_colors (disable terminal colors) | ||
prob_src_profile (perform profiling at B source level in source_profiler.pl) | |||
debug_kodkod (write dot files for kodkod interval analysis) | debug_kodkod (write dot files for kodkod interval analysis) | ||
prob_logging_mode (automatically log probcli (add -ll command-line switch)) | |||
no_wd_checking (disable WD checking for function application) | no_wd_checking (disable WD checking for function application) | ||
no_interrupts (do not treat CTRL-C user_interrupts) | |||
disable_chr (completely disable CHR) | |||
prob_data_validation_mode (deprecated, replaced by DATA_VALIDATION preference) | |||
prob_core_only probcli now only contains core modules, many extensions are not included | |||
prob_myheap do not use C++ priority queue but Prolog version instead | |||
prob_c_counter_false do not use C++ counter extension but Prolog version instead | |||
The full list of flags is now documented in the Prolog file <tt>compile_time_flags.pl</tt>. | |||
When you call probcli with the <tt>-version</tt> command you will get information about the compile-time flags that have been used: | |||
<pre> | |||
$ probcli -version | |||
ProB Command Line Interface | |||
VERSION 1.10.1-nightly (88d012a1d06fdbfdaa5c550492197b0c622a1479) | |||
Sat Jan 9 09:41:02 2021 +0100 | |||
Prolog: SICStus 4.6.0 (x86_64-darwin-17.7.0): Mon Apr 6 18:23:42 CEST 2020 | |||
COMPILE TIME FLAGS: [prob_release,SP_TIMEOUT_IMPLEMENTATON=legacy] | |||
</pre> | |||
== Running ProB with SWI-Prolog == | |||
ProB can also run on recent versions of SWI-Prolog. We recommend using the latest development release of SWI-Prolog (currently 8.5.x). The stable release 8.4.2 also works relatively well. Downloads can be found on [https://www.swi-prolog.org/download/devel the SWI-Prolog website]. You can also compile [https://github.com/SWI-Prolog/swipl-devel the latest SWI-Prolog source code] manually. | |||
Please note that SWI-Prolog support in ProB is still in development and '''there are known bugs'''. In addition, many advanced ProB features are not yet available on SWI-Prolog and performance is sometimes much slower than on SICStus Prolog. | |||
All instructions below assume that you have installed SWI-Prolog and can run it on the command line as <code>swipl</code>. If you have SWI-Prolog installed under a different name/location, you need to adjust the commands appropriately. | |||
=== Obtain Source Code and Parser JAR === | |||
* Download the source code for the development version of ProB: https://www3.hhu.de/stups/downloads/prob/source/ProB_src.tgz | |||
* Ensure the Java parser is available, either by copying it from a pre-compiled release of ProB or by running <tt>./gradlew updateParser</tt>. More details are available [[#Building ProB Extensions|above]]. Note you do not need the other extensions of ProB. | |||
=== Starting ProB with SWI-Prolog === | |||
For convenience declare this alias, where $PROBDIR points to the top-level directory of the ProB source (see above): | |||
<pre> | |||
alias swiprob='PROLOG_SYSTEM=swi "$PROBDIR/probcli_src.sh"' | |||
</pre> | |||
You can now start a REPL for evaluating B expressions and predicates (without a machine context) as follows: | |||
<pre> | |||
$ swiprob -repl | |||
... | |||
ProB Interactive Expression and Predicate Evaluator | |||
Type ":help" for more information. | |||
>>> | |||
</pre> | |||
Note that currently you may still see warnings and various messages appear on the console. | |||
You can now experiment and type in expressions and predicate: | |||
<pre> | |||
>>> 2+2 | |||
Expression Value = | |||
4 | |||
>>> {x,y|x:1..30000 & y:1..3000 & x<y & x * 220 <y} | |||
Expression Value = | |||
#18980:{(1|->221),(1|->222),...,(13|->2999),(13|->3000)} | |||
>>> x*x=100 | |||
Existentially Quantified Predicate over x is TRUE | |||
Solution: | |||
x = -10 | |||
</pre> | |||
You can also provide all of the command-line arguments accepted by probcli, e.g., provide a machine that should be loaded | |||
<pre> | |||
swiprob -repl -init ../prob_examples/public_examples/B/Demo/ACounter.mch | |||
... | |||
>>> :state | |||
Current state id 0 : | |||
( ii=2 & | |||
jj=10 ) | |||
</pre> | |||
=== Running ProB Tests with SWI-Prolog === | |||
For convenience declare this alias, where $PROBDIR points to the top-level directory of the ProB source (see above): | |||
<pre> | |||
alias switests='PROLOG_SYSTEM=swi "$PROBDIR/prolog.sh" --file "$PROBDIR/src/test_runner.pl" --goal "test_repl." -- ' | |||
</pre> | |||
You can now start the testrunner REPL as follows: | |||
<pre> | |||
$switests | |||
... | |||
ProB 1.11.0-nightly | |||
Revision: no revision found | |||
Date: no lastchanged found | |||
TEST ==> | |||
</pre> | |||
You can now for example run individual tests: | |||
<pre> | |||
TEST ==> 11. | |||
Current directory: /Users/leuschel/git_root/prob_prolog/ | |||
Running test 11 | |||
executing: probcli ../prob_examples/public_examples/B/Benchmarks/DSP0.mch -t -mc 100 -noinv -strict -nodead -expcterr model_check_incomplete -strict -p STRICT_RAISE_WARNINGS TRUE | |||
... | |||
All expected errors occurred. | |||
Test 11 completed successfully (in 186 ms) | |||
Test successful. | |||
Walltime: 188 ms | |||
0.000 MB ( 0.000 MB program) | |||
</pre> | |||
The test runner will automatically skip tests that are known to be incompatible with SWI-Prolog, usually because a necessary component of ProB is currently disabled/unavailable on SWI-Prolog. To run a skipped test anyway, enter its number directly into the test REPL - this bypasses any skip declarations/conditions. | |||
[[Category:Developer Manual]] |
The kernel of ProB is written in Prolog and you can download the latest Prolog sourcecode snapshot from: https://stups.hhu-hosting.de/downloads/prob/source/
You may also wish to obtain related Java sources:
You first need to download and install SICStus Prolog. Evaluation licenses (30-days) are available. We currently compile with SICStus 4.6.0 (as of January 2021), but the source code is compatible with older versions as well (SICStus 4.3.2 or later).
You need the password to download SICStus then run sudo ./InstallSICStus and provide the site name, license code and expiration date. Be sure to add the SICStus binaries to your PATH.
Now, you need to clone or download the ProB Prolog sources.
Before using ProB for the first time from source you should build the extensions. The minimal extensions are counter, myheap and user_signal. You can build them using
cd extensions/counter make cd ../user_signal make cd ../myheap make
You will also need the ProB parser, which can be downloaded or updated using the command
./gradlew updateParser
You could also build all extensions at once by going to the top of the prob_prolog tree (i.e., the directory containing src and lib as sub-directories) and then type
make
An alternative is to download ProB from the download page, unzip the archive and copy all the files in the lib folder of the archive to the lib folder of your Prolog source code, containing files such as (the file extension of some of these files varies with the operating system: bundle for macOS, dll for Windows and so for Linux):
Probably you should first install a recent Active Tcl distribution, in particular on macOS. Check the download page for which version is required or recommended.
You can then start ProB Tcl/Tk by changing into the prob_prolog directory of the Prolog sources and type:
sicstus -Dprob_profile=true -l src/prob_tcltk.pl --goal "go."'
To simplify starting ProB, add the following to your .bash_login file (or similar configuration file; supposing you cloned the Git repository into ~/git_root):
export PROBDIR=~/git_root/prob_prolog export PROB_SOURCE_DIR=$PROBDIR/src alias prob='cd sicstus -Dprob_profile=true -l $PROB_SOURCE_DIR/prob_tcltk.pl --goal "go."'
Now, you can simply start ProB from the command-line and from source with the prob alias command.
The command-line version of ProB does not require a Tcl/Tk distribution.
To start probcli from source define this alias, where PROB_SOURCE_DIR and SICSTUSDIR must be defined:
alias probsli='rlwrap $SICSTUSDIR/bin/sicstus -l $PROB_SOURCE_DIR/prob_cli.pl --goal "go_cli." -a'
(It is recommended to install rlwrap so that you get a history of your commands. If you don't want to install rlwrap just remove it from the line above.)
You can now use probsli just like probcli, e.g.,
probsli M.mch --model-check
or
probsli --repl
All Prolog tests are stored as facts in the file test cases.pl. Every test has
There is a specific test_runner.pl file for running all Prolog unit and integration tests. The test_runner also provides a REPL (read-eval-print-loop) for running tests and collection of tests. To start the Unit Test REPL, add the following to your .bash_login file (at least on Mac OS):
alias tests='cd $PROBDIR; rlwrap sicstus -Dprob_safe_mode=true -l $PROB_SOURCE_DIR/test_runner.pl --goal "test_repl."'
(It is recommended to install rlwrap so that you get a history of your commands. If you don't want to install rlwrap just remove it from the line above.)
Now you can start the test runner like this:
tests
or you can already specify tests to be run:
tests last
You can also type the number of a unit test to run, or a test category such as tickets to run all tests in that category.
Here is a sample sesssion of running the test REPL:
$ tests ... SICStus 4.2.3 (x86_64-darwin-11.4.2): Fri Oct 5 15:58:35 CEST 2012 Licensed to SP4phil-fak.uni-duesseldorf.de TEST ==> last. ... All tests successful. Walltime: 100 ms
Some useful commands in the REPL are:
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_release (removes certain tests from the code) no_terminal_colors (disable terminal colors) prob_src_profile (perform profiling at B source level in source_profiler.pl) debug_kodkod (write dot files for kodkod interval analysis) prob_logging_mode (automatically log probcli (add -ll command-line switch)) no_wd_checking (disable WD checking for function application) no_interrupts (do not treat CTRL-C user_interrupts) disable_chr (completely disable CHR) prob_data_validation_mode (deprecated, replaced by DATA_VALIDATION preference) prob_core_only probcli now only contains core modules, many extensions are not included prob_myheap do not use C++ priority queue but Prolog version instead prob_c_counter_false do not use C++ counter extension but Prolog version instead
The full list of flags is now documented in the Prolog file compile_time_flags.pl. When you call probcli with the -version command you will get information about the compile-time flags that have been used:
$ probcli -version ProB Command Line Interface VERSION 1.10.1-nightly (88d012a1d06fdbfdaa5c550492197b0c622a1479) Sat Jan 9 09:41:02 2021 +0100 Prolog: SICStus 4.6.0 (x86_64-darwin-17.7.0): Mon Apr 6 18:23:42 CEST 2020 COMPILE TIME FLAGS: [prob_release,SP_TIMEOUT_IMPLEMENTATON=legacy]
ProB can also run on recent versions of SWI-Prolog. We recommend using the latest development release of SWI-Prolog (currently 8.5.x). The stable release 8.4.2 also works relatively well. Downloads can be found on the SWI-Prolog website. You can also compile the latest SWI-Prolog source code manually.
Please note that SWI-Prolog support in ProB is still in development and there are known bugs. In addition, many advanced ProB features are not yet available on SWI-Prolog and performance is sometimes much slower than on SICStus Prolog.
All instructions below assume that you have installed SWI-Prolog and can run it on the command line as swipl
. If you have SWI-Prolog installed under a different name/location, you need to adjust the commands appropriately.
For convenience declare this alias, where $PROBDIR points to the top-level directory of the ProB source (see above):
alias swiprob='PROLOG_SYSTEM=swi "$PROBDIR/probcli_src.sh"'
You can now start a REPL for evaluating B expressions and predicates (without a machine context) as follows:
$ swiprob -repl ... ProB Interactive Expression and Predicate Evaluator Type ":help" for more information. >>>
Note that currently you may still see warnings and various messages appear on the console.
You can now experiment and type in expressions and predicate:
>>> 2+2 Expression Value = 4 >>> {x,y|x:1..30000 & y:1..3000 & x<y & x * 220 <y} Expression Value = #18980:{(1|->221),(1|->222),...,(13|->2999),(13|->3000)} >>> x*x=100 Existentially Quantified Predicate over x is TRUE Solution: x = -10
You can also provide all of the command-line arguments accepted by probcli, e.g., provide a machine that should be loaded
swiprob -repl -init ../prob_examples/public_examples/B/Demo/ACounter.mch ... >>> :state Current state id 0 : ( ii=2 & jj=10 )
For convenience declare this alias, where $PROBDIR points to the top-level directory of the ProB source (see above):
alias switests='PROLOG_SYSTEM=swi "$PROBDIR/prolog.sh" --file "$PROBDIR/src/test_runner.pl" --goal "test_repl." -- '
You can now start the testrunner REPL as follows:
$switests ... ProB 1.11.0-nightly Revision: no revision found Date: no lastchanged found TEST ==>
You can now for example run individual tests:
TEST ==> 11. Current directory: /Users/leuschel/git_root/prob_prolog/ Running test 11 executing: probcli ../prob_examples/public_examples/B/Benchmarks/DSP0.mch -t -mc 100 -noinv -strict -nodead -expcterr model_check_incomplete -strict -p STRICT_RAISE_WARNINGS TRUE ... All expected errors occurred. Test 11 completed successfully (in 186 ms) Test successful. Walltime: 188 ms 0.000 MB ( 0.000 MB program)
The test runner will automatically skip tests that are known to be incompatible with SWI-Prolog, usually because a necessary component of ProB is currently disabled/unavailable on SWI-Prolog. To run a skipped test anyway, enter its number directly into the test REPL - this bypasses any skip declarations/conditions.