Help

Handbook/ProB Prolog Guide

Running ProB from source

ProB Source Code

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:


Running ProB from Prolog

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.

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 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 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.

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 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

Running the Prolog Tests

All Prolog tests are stored as facts in the file test cases.pl. 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 probcli needed to run the test
  • a textual description of the test

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:

  • last to run the last test added to testcases.pl
  • 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 testcases.pl)
  • 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

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]

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 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.

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 ./gradlew updateParser. More details are available 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): 

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 )

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): 

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.

Organization of ProB Sources

The ProB sources consist of ...

ProB's Prolog Datastructures

Data Values

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.

AST (Abstract Syntax Tree)

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.

Information list

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)

AST types

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.

Operators without arguments

boolean_false
boolean_true
bool_set

...

Unary operators

card(AST)
domain(AST)
front(AST)

...

Binary operators

cartesian_product(AST1,AST2)
composition(AST1,AST2)
concat(AST1,AST2)
conjunct(AST1,AST2)

...

Special operators

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)

...

ProB Tcl/Tk Architecture


TheProB Tcl/Tk cross-language architecture

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:

  • on startup ProB launches Tcl/Tk; most of the GUI code can be found inside main_prob_tcltk_gui.tcl
  • from then on Tcl/Tk controls the GUI and calls Prolog predicates
  • Tcl/Tk code calls Prolog using 
prolog PRED(…X…Y…)
  • Tcl/Tk then gets result values using
 $prolog_variables(X) or $prolog_variables(Y). There are only limited Prolog datatypes that can be transferred from Prolog to Tcl/Tk in this way; see below.
  • Tcl/Tk code can also check if a Prolog call was successful, e.g.: 
if [prolog tcltk_backtrack] { … }
  • Tcl/Tk code usually calls predicates with tcltk in their name; but there are exception (evaluation_view.tcl calls bvisual2 predicates)

The library(tcltk) puts restrictions on what can be transferred from Prolog to Tcl/Tk and then extracted using $prolog_variables(VAR):

  • integer
  • atoms (which get translated to Tcl strings)
  • lists of integer or atoms
  • nested lists of the above; in this case the Prolog code should not return the list but wrap the list result inside a list(.) constructor

How to add a simple menu command

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:

ProB TclTk CountVarMenu.png

Some useful ProB Tcl/Tk procedures

  • procShowErrors: collect all new errors and warnings from the Prolog error_manager and displays them in a dialog (in batch mode they are printed on the console only)
  • procShowList, procShowTable: pops up dialog boxes to display lists or tables (lists of lists). Parameters are title of dialog box,…
  • procInsertHistoryOptionsState: updates the State, History and Operations (Options) views by calling Prolog and getting information about the current state

Note: the Tcl/Tk code is mostly state-less, almost everything is stored inside Prolog:

  • current animation state
  • animation history and forward history
  • state space (all visited states and transitions)
  • all errors that have occurred (stored by the error_manager.pl)
  • the current specification
  • the state of all the preferences (inside preferences.pl)
  • ...

Prolog Coding Guidelines

General Guidelines

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.

Module Information

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

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

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

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).

Git

  • before committing ensure that probcli can be built (make prob); otherwise git bisect gets annoying to use (one can use git bisect skip to some extent, but it is annoying)
  • run integration tests before pushing your changes (ideally also before committing to avoid later issues with git bisect); ideally you should run as many tests as possible, but at least those affecting the parts you have changed. See alias below to start the test REPL. The command "test" then starts the ProB Test REPL. Type something like "tickets" to run all non-regression tests related to tickets.
  • as a rule of thumb: use rebase before pushing your changes to gitlab, especially when you only have one real commit.
  • avoid merge bombs with many changed files: a Git merge can hide unintended changes, e.g., accidentally reverting previous commits because of editor issues (editor out of sync with file system).
  • provide good commit messages. If a commit is related to a JIRA/Gitlab/Github ticket reference the identifier of the ticket in the commit message. This web page provides the following seven rules:
  • Separate subject from body with a blank line
  • Limit the subject line to 50 characters
  • Capitalize the subject line
  • Do not end the subject line with a period
  • Use the imperative mood in the subject line
  • Wrap the body at 72 characters
  • Use the body to explain what and why vs. how
  • Note: you can use git commit -m "Title" -m "Description" to add descriptions to a commit
  • Ideally: always create a test or ticket (or ideally both) for a bug fix

Useful Bash Aliases

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."'

Why Prolog?

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).

Why Prolog

  • Prolog is a convenient language in which to express the semantics of other languages.
In particular, high-level languages with non-determinism can be expressed with an ease that is hard to match by other languages. For example, the ProB source code to encode the semantics of the internal choice (encoded internally as '|') from CSP is basically as follows:
cspm_trans('|'(X,_Y),tau,X).
cspm_trans('|'(_X,Y),tau,Y).
The full operational semantics of CSP from Roscoe's book has been translated mostly one-to-one into Prolog rules (adding treatment for source location information,...).
  • Prolog is (one of) the most convenient languages to express program analysis
(e.g., abstract interpretation or even dataflow analysis, see also last chapters of 2nd edition of the Dragon book), program verification (e.g., model checking), and program transformation (e.g., partial evaluation) in. Also, type inference and type checking are a "breeze" thanks to Prolog's unification.
  • Modern Prolog systems support a feature called "co-routining",
also known as flexible computation rules or delay-declarations. These can be implemented by block-declarations or when-statements and they can stipulate conditions under which a Prolog goal should be expanded. For example, the following block declarations say that the goal less_than_equal should only be expanded when both of its arguments are known:
:- block less_than_equal(-,?), less_than_equal(?,-).
less_than_equal(X,Y) :- X=<Y.
A nice aspect is that the block declarations do *not* influence the declarative semantics of a Prolog program because of the theorem which states that the declarative semantics of logic programs is independent of the selection rule.

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.

  • Prolog is fast.
This may be surprising to some as Prolog sometimes has a reputation of being slow. On the laptop used for the experiments below, SICStus Prolog can perfrom 33 Million logical inferences per second (on my very latest laptop in can actually perform 75 Million logical inferences per second in 64-bit mode). As you see below, it can sometimes be faster than Java. Modern Prolog systems are well tuned and developed, and will outperform your own logical inference or unification mechanism by a considerable margin (I observed a factor of 10,000 between SICStus Prolog and the C implementation of a custom rule engine in a commercial product).

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.

  • Prolog is concise

See my Prolog vs Java Comparison on some sample code from ProB2-UI

Why SICStus Prolog

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:

  • + Fast, good support
  • + Standalone binaries
  • + >256 MB Heap on 32 Bit systems
  • + C, Java, TclTk external interfaces,
  • + Good libraries (from Quintus)
  • + fast co-routines and constraint solving
  • - commercial product (with academic site licences available)
  • - no multi-threading

SWI

  • + Actively maintained
  • + Large number of libraries and features
  • + Support for co-routines and constraint solving
  • - still slow

Ciao

  • + comes with CiaoPP analyser for static analysis
  • + good module system
  • + relatively fast
  • + decent support for co-routines and constraint solving
  • - Long startup time

Gnu Prolog

  • + good Constraint solving
  • - No co-routines
  • - limited features and libraries
  • - no BigInts

XSB Prolog:

  • + Tabling
  • + Prolog facts can be used as efficient relational database
  • - non-standard built-ins (no print, ... quite ≠ from SWI, ...)
  • - no co-routines nor constraint solving
  • - no BigInts

Yap

  • + fast
  • - no finite domain constraint solver
  • - no BigInts
  • - only C external language interface

LPA

  • + good graphical tools, GUI generation, ...
  • - runs only Windows
  • - no modules
  • - no co-routines

BinProlog

  • - no Bigints
  • - commercial

B Prolog

  • - no Bigints prior to version 7.6, but now available
  • + constraint-based graphics library
  • - commercial (but free academic license)
  • + has action-rule mechanism (which apparently is a co-routining mechanism; I have not yet been able to experiment with it)


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.

A small benchmark

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);
}

Startup Times

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
Retrieved from "https://prob.hhu.de/w/index.php?title=Handbook/ProB_Prolog_Guide&oldid=5224"