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. There is also a specific subsection about installing Tcl/Tk and setting the SP_TCL_DSO environment variable to help SICStus Prolog find the Tcl/Tk installation.
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.
Build instructions for Windows (and other systems) are now found in the ProB source distribution in the file doc/building.md.
The ProB sources consist of ...
Integer value:
int(Nr)
where Nr is an integer
Booleans:
pred_true pred_false
Enumerated or deferred set elements:
fd(Nr,Type)
where Nr is an integer >= 1 and Type is an atom representing the type of enumerated/deferred set
Strings
string(S)
where S is an atom
Pairs/couples
(Val1,Val2)
where Val1 and Val2 are values
Records
rec(Fields)
where Fields is a list of terms:
field(Name,Val)
where Name is atom representing the field name and Val is a value.
The fields are sorted by name!
Sets Here is an overview of the set representations:
[] [Val|Set] avl_set(AVL) closure(P,T,B) global_set(GS) freetype(T)
The empty set is encoded as the empty list.
[]
This represents a set containing at least the value Val and the rest:
[Val|Set]
Note that Set can in principle be any other form (e.g., avl_set(.)). The predicate expand_custom_set_to_list can be used to transform a set into a form using only the empty list and the [.|.] functor.
The next are called custom explicit sets, they always represent a fully known set.
A set can be represented by a non-empty AVL tree:
avl_set(AVL)
Given a list of parameter identifiers, a list of types and a predicate AST B, we can represent the set {P| P:T & B} as follows:
closure(P,T,B)
There are custom representations for complete types, these may be phased out in the future and replaced by the closure(.,.,.) representation:
global_set(GS) freetype(T)
Freetype values
freeval(Id,Case,Value)
Constructor for denoting special values (undefined values, experimental support for reals,..)
term(Term)
term(undefined) is used for uninitialised variables (e.g., when using the B VAR construct). term(floating(Nr) is currently used for floating numbers, but this will probably change in the future.
An AST node has the form:
b(Expr,Type,Infos)
Expr generally has the form Functor(AST1,...,ASTk). Below we list possible cases. The predicate syntaxelement in bsyntaxtree.pl lists all allowed forms of Expr. Type is either pred for predicates, subst for substitutions or the value type for expressions, see below. Infos contains information about the AST node and is explained next.
Infos should be a ground list of informations. Some important information fields are:
contains_wd_condition used_ids(Ids) nodeid(PositionInfo) refers_to_old_state(References)
Possible types are:
pred subst integer real boolean string global(G) couple(Type1,Type2) record(FieldTypes) set(Type) seq(Type) freetype(F)
where FieldTypes is a list containing:
field(Name,Type)
The real type has been added in version 1.10 of ProB.
boolean_false boolean_true bool_set
...
card(AST) domain(AST) front(AST)
...
cartesian_product(AST1,AST2) composition(AST1,AST2) concat(AST1,AST2) conjunct(AST1,AST2)
...
general_sum(Ids,AST,AST) general_product(Ids,AST,AST) lambda(Ids,AST,AST) quantified_union(Ids,AST,AST) quantified_intersection(Ids,AST,AST) set_extension(ListOfASTs) sequence_extension(ListOfASTs)
...
The ProB Tcl/Tk contains a mixture of Prolog and Tcl/Tk source code. The core (i.e., the constraint solver, the animation engine, the model checker, ...) are all written in Prolog (which in turn may call some C external functions, e.g., for LTL model checking).
We use the SICStus library(tcltk) (see chapter 10.40 of SICStus manual)
Overall, the communication works as follows:
The library(tcltk) puts restrictions on what can be transferred from Prolog to Tcl/Tk and then extracted using $prolog_variables(VAR):
You need to add an entry in the ProB Tcl/Tk menu. The menus are defined at the top of the file main_prob_tcltk_gui.tcl
.frmMenu.mnuAnalyse.mnuCoverage add command -label "Number of Values for all Variables" -command {procNrVariableValuesOverStatespace}
You also need to define the Tcl/Tk part of your command (probably inside main_prob_tcltk_gui.tcl):
proc procNrVariableValuesOverStatespace {} { if [prolog “tcltk_compute_nr_covered_values_for_all_variables(Res)"] { procShowErrors procShowTable $prolog_variables(Res) "Coverage Table" "Number of Covered Values for Variables" "CoverageVariablesTable" "" "" } else { procShowErrors } }
Observe the use of prolog to call Prolog predicates and $prolog_variables to extract return values obtained from Prolog (which should instantiate the corresponding variable/argument). Also observer that we call procShowErrors, a Tcl/Tk procedure, which extracts all pending error messages and displays them to the user. procShowTable is a utility to display a dialog box containing a table.
Finally, we need to define the called Prolog predicate somewhere in the Prolog code:
tcltk_compute_nr_covered_values_for_all_variables(list([list(['Variable', 'Number of Values'])|VL])) :- state_space:get_state_space_stats(NrNodes,_,_), format('Computing all values in ~w states for all variables~n',[NrNodes]), findall(list([ID,Count]),number_of_values_for_variable(ID,Count),VL), format('Finished computing all values for all variables~n',[]).
The use of format is more for debugging (the output will not be seen by ProB Tcl/Tk, just on the console (if any) used to launch ProB Tcl/Tk).
The command is now available and ready to use:
Note: the Tcl/Tk code is mostly state-less, almost everything is stored inside Prolog:
Please ensure that there are no compilation errors or warnings when checking in. Also, try to ensure that there are no errors when loading the files in Spider (Eclipse). Ideally, try to get rid of warnings as well.
Have a look at the paper by Covington et al. on Prolog coding guidelines.
Concerning naming of identifiers: try to use names for constants, functors and predicates that are unique and not a prefix of other names. This ensures that one can quickly find all uses/definitions with grep or BBEdit.
Use the boy scout rule: "Always leave the code you are editing a little better than you found it". In particular, the second time around is often a good time for adding comments.
Every module should be annotated with module information. This is used by our coverage analysis tool.
:- module(MYMODULE, [ exported_predicate/arity, ... ]). :- use_module(tools). :- module_info(group,kernel). :- module_info(description,'This module does wonderful things').
Unit tests should be setup using the self_check module.
:- use_module(self_check).
Afterwards you can use the following to add new unit tests:
:- assert_must_succeed((bsets_clp:empty_sequence([]))). :- assert_must_fail((bsets_clp:empty_sequence([int(1)]))).
These tests can be run manually from the ProB Tcl/Tk version, from the command-line using the -self_check command. They will also be automatically run on our jenkins server after committing.
Errors should be raised using one of the add_error predicates in the error_manager module. This will ensure that the errors are brought to the attention of the user in an appropriate way, depending on whether the Rodin, the Tcl/Tk, the command-line version is run and also depending on whether the tool is in testing and/or batch mode.
Note: for internal errors that should never occur use the add_internal_error predicate. This ensures that the coverage information is shown accordingly (in blue rather than red in the highlighting and this also affects coverage statistics).
Preferences should be declared in the preferences module. Each preference must have a default value, a textual description, a type and category. Optionally, a short string for setting the preference from the command-line can be given (using the -p PREF VALUE switch).
To run probcli from sources:
alias probsli='rlwrap sicstus -l $PROB_SOURCE_DIR/prob_cli.pl --goal "go_cli." -a'
To run probcli with the REPL from sources:
alias seval='rlwrap sicstus -l $PROB_SOURCE_DIR/prob_cli.pl --goal "go_cli." -a -repl -init -p WARN_WHEN_EXPANDING_INFINITE_CLOSURES 0 -p CLPFD TRUE'
To run ProB Tcl/Tk from sources:
alias prob='unlimit; sics -Dprob_profile=true -l $PROB_SOURCE_DIR/prob_tcltk.pl --goal "go."'
To run the ProB Test REPL from sources:
alias test='cd $PROB_SOURCE_DIR/..; rlwrap sicstus -Dprob_safe_mode=true -l $PROB_SOURCE_DIR/test_runner.pl --goal "test_repl."'
In this chapter we try to answer the question: why did we use Prolog to develop the core of ProB, and in particular why do we use the commercial SICStus Prolog rather than an open-source alternative.
The short answer is that Prolog allows us to flexibly implement various specification formalisms as well as the analysis and verification tools that go along with it. At the same time, Prolog is very fast and SICStus Prolog is one of the fastest and most stable Prolog systems, allows access to more than 256 MB of heap even on 32 bit systems (important for model checking), and is easy to interate with other programming languages (so that the GUI does not have to be developed in Prolog).
cspm_trans('|'(X,_Y),tau,X). cspm_trans('|'(_X,Y),tau,Y).
:- block less_than_equal(-,?), less_than_equal(?,-). less_than_equal(X,Y) :- X=<Y.
I believe this to be one of the "killer" features of modern Prolog systems. We heavily use this in the ProB kernel to delay enumeration of values and to implement our own constraint solver over sets and relations. In my experience, this feature allows one to write much more declarative code than with traditional Prolog systems (an example is the transcription of Roscoe's operational semantics mentioned above), while often obtaining a dramatic increase in performance in generate-and-test scenarios.
In summary, Prolog gives us both a flexible way to encode both the operational semantics of many high-level formalisms (B, Z, CSP, ...) and various flexible tools on top such as animation, type checking, model checking and refinement checking.
All of this comes with a respectable performance, despite the flexibility of the approach.
There are of course still aspects with Prolog that, despite many years of research and development, are not ideal. Standardisation of Prolog and the libraries is not ideal (the ISO standard does not cover the module system for one). There is no standard static type checking tool.
See my Prolog vs Java Comparison on some sample code from ProB2-UI
Below is a short summary of some of the Prolog systems that to my knowledge are still being actively maintained (please email me corrections and additions).
SICStus:
SWI
Ciao
Gnu Prolog
XSB Prolog:
Yap
LPA
BinProlog
B Prolog
Other Prologs with which I have not directly experimented are: Visual Prolog and IF Prolog.
It seems that maybe Yap and SWI are merging efforts. It would be nice to have a Prolog system with the features of SWI and the speed of YAP. This would be a serious (free) alternative to SICStus Prolog.
Below I have conducted a small experiment to gauge the performance of various Prolog systems. I do not claim that this example is representative; it tests only a few aspects of performance (e.g., speed of recursive calls). I don't have the time to do a more extensive evaluation at the moment.
The benchmark is the Fibonacci function written in the naive recursive way so as to quickly obtain a large number of recursive calls. The advantage is that the code can be easily transcribed into other programming languages. Below, I give you also a Python, a Haskell, and a Java version using BigInts. The benchmarks were run on a MacBook Pro Core2 Duo with 2.33 GHz. BinProlog does not have a demo licence for Mac; hence I had to run the Windows version in Parallels. LPA Prolog only runs on Windows; so it was also run using Parallels. Note: the purpose of the benchmark was to measure the performance of recursion. As such, I was trying to use the same types of data on all platforms (BigInts). Also note that this is actually not a typical Prolog "application" as no use is made of unification or non-determinism. But it is a good application for a functional programming language such as Haskell since Fibonacci is a pure function without side-effects.
Also, I do not claim that the benchmark shows that Prolog is faster than Java in general. My only claim is that if an application is well suited to Prolog, its performance can be surprisingly good. I also have the feeling that Haskell has made great strides in performance recently, and that the Prolog community should be on its guard (so as not to be left behind).
System BigInts Fib(30) Fib(35) Java 1.5.0_16 NO (long) 0.020 0.231 GHC 6.10.1 yes 0.082 0.878 Yap 5.1.3 NO 0.193 2.112 SICStus 4.0.4 yes 0.240 2.640 Ciao 1.13.0 yes 0.312 3.461 BinProlog 11.38 NO 0.361 3.725 Java 1.5.0_16 yes 0.445 4.898 XSB 3.1 NO 0.456 5.064 Python 2.5.1 yes 0.760 8.350 Gnu 1.3.1 NO 1.183 13.139 SWI 5.6.52 yes 1.900 20.990 LPA 4.710 yes 1.736 36.250
The same table with only the BigInteger versions is:
System BigInts Fib(30) Fib(35) GHC 6.10.1 yes 0.082 0.878 SICStus 4.0.4 yes 0.240 2.640 Ciao 1.13.0 yes 0.312 3.461 Java 1.5.0_16 yes 0.445 4.898 Python 2.5.1 yes 0.760 8.350 SWI 5.6.52 yes 1.900 20.990 LPA 4.710 yes 1.736 36.250
I have also recently tested B Prolog 7.4. It seems to perform marginally faster than SICStus (3 %), but does not support BigInts. Note, that Gnu is the only system requiring tweaking of parameters:
export TRAILSZ=200000 export GLOBALSZ=1500000
Java with int rather than BigIntegers takes 0.016 s for Fib(30) and 0.163 s for Fib(35). Note that GHC Haskell seems to have received a big performance boost on this particular example (earlier versions of Haskell were on par with SICStus Prolog).
I also wanted to experiment with a Mercury version, but for the moment Mercury does not compile/install on my machine. Marc Fontaine has also written various Haskell versions of Fibonacci
Here are the various versions of Fibonacci:
Prolog Version:
fib(0,1) :- !. fib(1,1) :- !. fib(N,R) :- N1 is N-1, N2 is N1-1, fib(N1,R1), fib(N2,R2), R is R1+R2.
Python Version:
def Fib(x): if x<2: return 1 else: return Fib(x-1)+Fib(x-2)
Java Version with BigInteger:
private static BigInteger ZERO = BigInteger.ZERO; private static BigInteger ONE = BigInteger.ONE; private static BigInteger TWO = new BigInteger("2"); public static BigInteger naiveFib(BigInteger x) { if (x.equals(ZERO) ) return ONE; if (x.equals(ONE) ) return BigInteger.ONE; return naiveFib(x.subtract(ONE)).add(naiveFib(x.subtract(TWO))); }
Haskell Version:
fib :: Integer -> Integer fib n | n == 0 = 1 | n == 1 = 1 | otherwise = fib(n-1) + fib(n-2)
Java Version with long rather than BigIntegers:
public static long fib(long xx) { if (xx<2) return 1; else return fib(xx-1)+fib(xx-2); }
Below we test the startup times of some of the Prolog systems. Unfortunately, not all Prolog systems can easily be started as easily from the command-line as SICStus Prolog (e.g., --goal "GOAL." parameter and -l FILE parameter).
First, the following command takes 0.026 s real time (0.015 s user time) with SICStus Prolog 4.0.5 on the same system as above:
time sicstus --goal "halt."
For SWI Prolog 5.6.64, we get 0.015 s real time (0.008 s user time):
time swipl -g "halt."
For Ciao Prolog 1.13.0-8334, we get 0.271 s user time for "time ciao" and then typing halt (I found no easy way to provide goals on the command-line).
Now, take the file halt.pl with contents:
main :- print(hello),nl,halt. :- main.
The following takes 0.028 seconds real time and 0.015 seconds user time.
time sicstus -l halt.pl
The following takes 0.204 seconds real time the first time and 0.015 seconds real time the second time:
time swipl -c halt.pl
The following takes 0.726 seconds real time and 0.648 seconds user time (after commenting out :- main.), i.e., 25 times slower than SICStus:
time ciao -c halt.pl