(Created page with "Category:User Manual Category: Advanced Feature There are various ways in which you can debug your model. We focus here on debugging performance issues == Debugging...") |
|||
| Line 16: | Line 16: | ||
</pre> | </pre> | ||
With the external predicate < | With the external predicate <tt>printf</tt> 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 printf predicate uses the format from SICStus Prolog for the format string. | ||
The most important are < | The most important are <tt>~w</tt> for printing an argument and <tt>~n</tt> | ||
for a newline. There must be exactly as many < | for a newline. There must be exactly as many <tt>~w</tt> in the format string as there | ||
are aguments. | are aguments. | ||
Below is a small example, to inspect in which order ProB enumerates values. | Below is a small example, to inspect in which order ProB enumerates values. | ||
The example is typed in the REPL of [[Using_the_Command-Line_Version_of_ProB|probcli]] | The example is typed in the REPL of [[Using_the_Command-Line_Version_of_ProB|probcli]] | ||
(started using the command < | (started using the command <tt>probcli -repl File.mch</tt> where <tt>File.mch</tt> includes the definitions section above): | ||
<pre> | <pre> | ||
There are various ways in which you can debug your model.
We focus here on debugging performance issues
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)}