Debugging

There are various ways in which you can debug your model. We focus here on debugging performance issues

Debugging with LibraryIO

The standard library "LibraryIO.def" contains various external functions and predicates with which you can instrument your formal model.

To use the library in your model you need to include the following

DEFINITIONS
 "LibraryIO.def"

With the external predicate

printf

you can view values of variables and identifiers. The printf predicate is always true and will print its arguments when all of them have been fully computed.

The printf predicate uses the format from SICStus Prolog for the format string.

The most important are

~w

for printing an argument and

~n

for a newline. There must be exactly as many

~w

in the format string as there

are aguments. Below is a small example, to inspect in which order ProB enumerates values. The example is typed in the REPL of probcli

(started using the command

probcli -repl File.mch

where

File.mch

includes the definitions section above):

>>> {x,y | x:1..5 & y:1..2 & x+y=6 & printf("x=~w~n",[x]) & printf("y=~w~n",[y])}
y=1
x=5
y=2
x=4
Expression Value = 
{(4|->2),(5|->1)}