Debugging: Difference between revisions

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

As you can see, ProB has enumerated y before x, as its domain was smaller.

You can use the external function observe to inspect a list of identifiers:

>>> {x,y | x:1..5 & y:1..2 & x+y=6 & observe((x,y))}
 observing x
 observing y
 y = 1  (walltime: 562188 ms)
. x = 5  (walltime: 562188 ms)
..* Value complete: x |-> y = (5|->1)  (walltime: 562188 ms)
------
 y = 2  (walltime: 562188 ms)
. x = 4  (walltime: 562188 ms)
..* Value complete: x |-> y = (4|->2)  (walltime: 562188 ms)
------
Expression Value = 
{(4|->2),(5|->1)}

With the external function TIME you can get the current time in seconds:

>>> TIME("sec")
Expression Value = 
11
>>> TIME("now")
Expression Value = 
1581432376
>>> TIME("now")
Expression Value = 
1581432377

With the external function DELTA_WALLTIME you can get the time in milliseconds since the last call to DELTA_WALLTIME.

Performance Messages

By setting the preference PERFORMANCE_INFO to TRUE ProB will print various performance messages. For example it may print messages when the evaluation of comprehension sets has exceeded a threshold. This threshold (in ms) can be influenced by setting the preference PERFORMANCE_INFO_LIMIT.

Debugging Constants Setup

TRACE_INFO preference

By setting the preference TRACE_INFO to TRUE ProB will print additional messages when evaluating certain predicates, in particular the PROPERTIES clause of a B machine. With this feature you can observe how constants get bound to values and can sometimes spot expensive predicates and large values. Some additional information about debugging the PROPERTIES can be found in the Tutorial Troubleshooting the Setup.

Let us take the following machine

MACHINE Debug
CONSTANTS a,b,c
PROPERTIES
  a = card(b) &
  b = %x.(x:1..c|x*x) &
  c : 1000..1001 & c < 1001
VARIABLES x
INVARIANT x:NATURAL
INITIALISATION x:=2
OPERATIONS
  Sqr = SELECT x:dom(b) THEN x := b(x) END;
  Finished = SELECT x /: dom(b) THEN skip END
END

Here is how we can debug the constants setup using the TRACE_INFO preference:

$ probcli Debug.mch -p TRACE_INFO TRUE -init
% unused_constants(2,[a,c])
nr_of_components(1)

 ====> (1) c < 1001

 ====> (1) a = card(b)

 ====> (1) b = %x.(x : 1 .. c|x * x)

 ====> (1) c : 1000 .. 1001
finished_processing_component_predicates
grounding_wait_flags
 :?: a int(?:0..sup)
 :?: b VARIABLE: _31319 : GRVAL-CHECK
 :?: c int(?:inf..1000)
--1-->> a
     int(1000)
--1-->> b
     AVL.size=1000
--1-->> c
     int(1000)
% Runtime for SOLUTION for SETUP_CONSTANTS: 107 ms (walltime: 110 ms)
% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)

 =INIT=> x := 2
 [=OK= 0 ms]

Profiling Constants Computation Time

ProB now also supports profiling the computation of constants defined by equations in the PROPERTIES, when profiling is active (see section below). The profiling can be achieved using the following table command -csv prob_constants_profile_info FILE:

probsli DebugSymbolicConstants.mch -csv prob_constants_profile_info user_output -init -p PROFILING_INFO TRUE -p PERFORMANCE_INFO TRUE
% Runtime for SOLUTION for SETUP_CONSTANTS: 22 ms (walltime: 22 ms)
% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
Calling table command prob_constants_profile_info
Constant Kind @desc Computation Runtime (ms) Computation Walltime (ms) Propagation Walltime (ms) # Calls Other Infos Valued Det.Value Instantiates
c1 concrete  20 20 0 1 [] yes AVL-Set:10000 []
c2 concrete  2 2 0 1 [] yes AVL-Set:100 []
c3 concrete  0 0 0 1 [] yes AVL-Set:100 []
a3 abstract  0 0 0 1 [] yes SYMBOLIC-Set []
a2 abstract  0 0 0 1 [] yes SYMBOLIC-Set []
a1 abstract  0 0 0 1 [] yes SYMBOLIC-Set []
Finished exporting prob_constants_profile_info to user_output

In ProB Tcl/Tk this is available in the Debug -> Statistics menu, while in ProB2-UI it is available in the Graph and Table visualisation dialog. In probcli you can obtain a list of all available commands (callable via -csv CMD FILE) using probcli --help.

Debugging Constant Size

Indeed, for performance it can be much more efficient to expand a value (such as a function or relation) once, rather than keeping it symbolic. On the other, expanding a very large set can be costly in terms of memory. A useful feature to analyse these issues is the constants_analysis command. It generates a CSV table which can be inspected in an editor or a spreadsheet program. The table provides an overview of the constants, in particular their size and whether they are kept symbolic or expanded.

Note that B distinguishes between abstract and concrete constants. By default, concrete constants will be evaluated (unless they are known to be infinite or larger or annotated as symbolic). Abstract constants are more often kept symbolic. You can influence ProB's treatmen of constants by - choosing to put constants into the ABSTRACT_CONSTANTS or CONCRETE_CONSTANTS section - annotating the values with the /*@ symbolic */ pragma - annotating the constant with the /@ desc expand */ pragma to force expansion - annotating the constant with the /@desc memo */ pragma to memoize its evaluation (i.e., cache evaluation results involving the constant)

Let us examine this machine, where the constants a1,a2,a3 are identical to c1,c2,c3 but are located in the abstract rather than the concrete constants section:

MACHINE DebugSymbolicConstants
ABSTRACT_CONSTANTS
  a1, a2, a3
CONCRETE_CONSTANTS
  c1, c2, c3
PROPERTIES
  a1 = %x.(x:1..10000|x+x) &
  a2 = {x | x:1..10000 & x mod 100 = 0} &
  a3 = %x.(x:1..100|x*x) &
  c1 = %x.(x:1..10000|x+x) &
  c2 = {x | x:1..10000 & x mod 100 = 0} &
  c3 = %x.(x:1..100|x*x)
END

The command can now be run as follows. Here the output is written to the console (by providing user_output as file name). The list of constants is sorted according to size.

 probcli DebugSymbolicConstants.mch -init -csv constants_analysis user_output
...
Calling table command constants_analysis

! Message (source: constants_analysis):
! Abstract constant is stored symbolically but can be expanded to a finite set of size 10000 (by moving to ABSTRACT_CONSTANTS or annotating with /*@desc expand */ pragma): a1
! Line: 3 Column: 2 until Line: 3 Column: 4 in file: /Users/leuschel/git_root/prob_examples/public_examples/B/Tester/ConstantsDebug/DebugSymbolicConstants.mch

! Message (source: constants_analysis):
! Abstract constant is stored symbolically but can be expanded to a finite set of size 100 (by moving to ABSTRACT_CONSTANTS or annotating with /*@desc expand */ pragma): a2
! Line: 3 Column: 6 until Line: 3 Column: 8 in file: /Users/leuschel/git_root/prob_examples/public_examples/B/Tester/ConstantsDebug/DebugSymbolicConstants.mch

! Message (source: constants_analysis):
! Abstract constant is stored symbolically but can be expanded to a finite set of size 100 (by moving to ABSTRACT_CONSTANTS or annotating with /*@desc expand */ pragma): a3
! Line: 3 Column: 10 until Line: 3 Column: 12 in file: /Users/leuschel/git_root/prob_examples/public_examples/B/Tester/ConstantsDebug/DebugSymbolicConstants.mch
CONSTANT class kind termsize value
c1 CONCRETE AVL-Set:10000 90002 #10000:{(1|->2),(2|->4),...,(9999|->19998),(10000|->20000)}
c3 CONCRETE AVL-Set:100 902 {(1|->1),(2|->4),(3|->9),(4|->16),(5|->25),(6|->36),(7|->49),(8|->64),(9|->81),(10|->100),(11|->121)...
a3 ABSTRACT FINITE-SYMBOLIC-Set:100 708 /*@symbolic*/ %x.(x : {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29...
c2 CONCRETE AVL-Set:100 602 {100,200,300,400,500,600,700,800,900,1000,1100,1200,1300,1400,1500,1600,1700,1800,1900,2000,2100,220...
a2 ABSTRACT FINITE-SYMBOLIC-Set:100 162 /*@symbolic*/ {x|x : (1 .. 10000) & x mod 100 = 0}
a1 ABSTRACT FINITE-SYMBOLIC-Set:10000 151 /*@symbolic*/ %x.(x : (1 .. 10000)|x + x)
Finished exporting constants_analysis to user_output

Let us now add pragmas to study their influence:

MACHINE DebugSymbolicConstants_pragmas
ABSTRACT_CONSTANTS
  a1 /*@desc expand*/, a2 /*@desc expand*/, a3 /*@desc expand*/
CONCRETE_CONSTANTS
  c1 /*@desc memo */, c2, c3
PROPERTIES
  a1 = %x.(x:1..10000|x+x) &
  a2 = {x | x:1..10000 & x mod 100 = 0} &
  a3 = %x.(x:1..100|x*x) &
  c1 = /*@symbolic */ %x.(x:1..10000|x+x) &
  c2 = /*@symbolic */ {x | x:1..10000 & x mod 100 = 0} &
  c3 = /*@symbolic */ %x.(x:1..100|x*x)
END

You can see that a1,a2 and a3 are expanded, while c1, c2 and c3 kept symbolic.

 probcli DebugSymbolicConstants_pragmas.mch -init -csv constants_analysis user_output
...
Calling table command constants_analysis

! Message (source: constants_analysis):
! Concrete constant is stored symbolically but can be expanded to a finite set of size 10000 (by annotating with /*@desc expand */ pragma): c1
! Line: 5 Column: 2 until Line: 5 Column: 4 in file: /Users/leuschel/git_root/prob_examples/public_examples/B/Tester/ConstantsDebug/DebugSymbolicConstants_pragmas.mch

! Message (source: constants_analysis):
! Concrete constant is stored symbolically but can be expanded to a finite set of size 100 (by annotating with /*@desc expand */ pragma): c2
! Line: 5 Column: 22 until Line: 5 Column: 24 in file: /Users/leuschel/git_root/prob_examples/public_examples/B/Tester/ConstantsDebug/DebugSymbolicConstants_pragmas.mch

! Message (source: constants_analysis):
! Concrete constant is stored symbolically but can be expanded to a finite set of size 100 (by annotating with /*@desc expand */ pragma): c3
! Line: 5 Column: 26 until Line: 5 Column: 28 in file: /Users/leuschel/git_root/prob_examples/public_examples/B/Tester/ConstantsDebug/DebugSymbolicConstants_pragmas.mch
CONSTANT class kind termsize value
a1 ABSTRACT AVL-Set:10000 90002 #10000:{(1|->2),(2|->4),...,(9999|->19998),(10000|->20000)}
a3 ABSTRACT AVL-Set:100 902 {(1|->1),(2|->4),(3|->9),(4|->16),(5|->25),(6|->36),(7|->49),(8|->64),(9|->81),(10|->100),(11|->121)...
c3 CONCRETE FINITE-SYMBOLIC-Set:100 708 /*@symbolic*/ %x.(x : {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29...
a2 ABSTRACT AVL-Set:100 602 {100,200,300,400,500,600,700,800,900,1000,1100,1200,1300,1400,1500,1600,1700,1800,1900,2000,2100,220...
c2 CONCRETE FINITE-SYMBOLIC-Set:100 162 /*@symbolic*/ {x|x : (1 .. 10000) & x mod 100 = 0}
c1 MEMOIZED FINITE-SYMBOLIC-Set:10000 154 /*@symbolic*/ %x.(x : (1 .. 10000)|x + x)
Finished exporting constants_analysis to user_output

For symbolic constants you can also inspect the value graphically. Using probcli this can be done as follows:

probcli -init DebugSymbolicConstants_pragmas.mch -dot_expr id_value_formula_tree c3 c3.pdf

The command is also available by right-clicking on an identifier in the Evaluation View of ProB Tcl/Tk.

Finding Constant Expressions

Using the command

-csv constant_expr_analysis FILE

you can detect possibly expensive constant expressions used in operation bodies.

It could be interesting to extract these expressions out of operations (e.g., into a constant or variable computed after initialisation), to avoid repeated re-computation of the expression.

Note, this command is also carried out as part of the -lint command. You can also execute -lint_operations, which will not generate a CSV table.

Debugging Animation or Execution

By using the -animate_stats flag, you can see execution times for operations that are executed either using the -execute or -animate commands. In verbose mode (-v flag) you also see the memory consumption.

$ probcli Debug.mch -execute_all -animate_stats
% unused_constants(2,[a,c])
% Runtime for SOLUTION for SETUP_CONSTANTS: 79 ms (walltime: 80 ms)
1    : SETUP_CONSTANTS
       91 ms walltime (89 ms runtime), since start: 1107 ms
2    : INITIALISATION
       5 ms walltime (4 ms runtime), since start: 1112 ms
3    : Sqr
       10 ms walltime (10 ms runtime), since start: 1123 ms
4    : Sqr
       0 ms walltime (0 ms runtime), since start: 1123 ms
5    : Sqr
       1 ms walltime (0 ms runtime), since start: 1124 ms
6    : Sqr
       0 ms walltime (0 ms runtime), since start: 1124 ms
7    : Finished
       3 ms walltime (4 ms runtime), since start: 1127 ms
Infinite loop reached after 8 steps (looping on Finished).
% Runtime for -execute: 116 ms (with gc: 116 ms, walltime: 119 ms); time since start: 1132 ms

Profiling

You can obtain some profiling information using the -prob_profile command. This command unfortunately requires that ProB was compiled using special flags (-Dprob_profile=true and -Dprob_src_profile=true). As of version 1.13.1-nightly September 2024, the profiling can be enabled by setting the preference PROFILING_INFO to TRUE (simply add -p PROFILING_INFO TRUE to the invocation below):

$ probcli ../prob_examples/public_examples/B/Tutorial/Debug.mch -execute_all -prob_profile -p PROFILING_INFO TRUE
% unused_constants(2,[a,c])
% Runtime for SOLUTION for SETUP_CONSTANTS: 2 ms (walltime: 2 ms)
Infinite loop reached after 8 steps (looping on Finished).
% Runtime for -execute: 3 ms (with gc: 3 ms, walltime: 3 ms); since start: 0 sec 426 ms
--------------------------
PROB PROFILING INFORMATION after 426 ms walltime (268 ms runtime)  168.843 MB
No source profiling information available
Set preference SOURCE_PROFILING_INFO to TRUE
---- ProB Runtime Profiler ----
---- Time spent in B operations and invariant evaluation
 Operation : Total Runtime ms (Total ms walltime & Minimum - Maximum ms walltime; #calls Number of Calls)
 $setup_constants : 2 ms (2 ms walltime & 2 - 2 ms walltime; #calls 1)
 INVARIANT : 1 ms (0 ms walltime & 0 - 0 ms walltime; #calls 7)
 Finished : 0 ms (1 ms walltime & 1 - 1 ms walltime; #calls 1)
 Sqr : 0 ms (0 ms walltime & 0 - 0 ms walltime; #calls 5)
 $initialise_machine : 0 ms (0 ms walltime & 0 - 0 ms walltime; #calls 1)
 Total Walltime: 3 ms for #calls 15
---- Time spent evaluating CONSTANTS (defined by equations)
 Operation : Total Runtime ms (Total ms walltime & Minimum - Maximum ms walltime; #calls Number of Calls)
 Total Walltime: 0 ms for #calls 0
Stored 0 AVL sets for state compression

Note, if you memoize functions you can also inspect time spent in evaluating function calls. E.g., if you set the preference MEMOIZE_FUNCTIONS to true then all abstract constants will be memoised and you can inspect number of calls and time. See Memoization_for_Functions.

Exporting Profile to CSV

You can also export the profile information into a CSV file (or on the console when providing "user_output" as special file name):

$ probcli ../prob_examples/public_examples/B/Tutorial/Debug.mch -execute_all -csv prob_profile_info user_output -p PROFILING_INFO TRUE
% unused_constants(2,[a,c])
% Runtime for SOLUTION for SETUP_CONSTANTS: 3 ms (walltime: 2 ms)
Infinite loop reached after 8 steps (looping on Finished).
% Runtime for -execute: 3 ms (with gc: 3 ms, walltime: 3 ms); since start: 0 sec 430 ms
Calling table command prob_profile_info
Operation/Action Total Runtime (ms) Total Walltime (ms) # Calls Max. Walltime (ms) Max. Witness ID Min. Walltime (ms)
$setup_constants 3 2 1 2 unknown 2
Sqr 0 1 5 1 unknown 0
INVARIANT 0 0 7 0 unknown 0
Finished 0 0 1 0 unknown 0
$initialise_machine 0 0 1 0 unknown 0
Finished exporting prob_profile_info to user_output

Profiling External Function Calls

You can also generate a profile of the external functions called. Take for example this machine:

MACHINE TestLibraryHash
DEFINITIONS
 "LibraryHash.def"
ASSERTIONS
  HASH(2+2) = HASH(4);
  SHA_HASH(2**10) = SHA_HASH(1024);
  SHA_HASH(2**10) /= SHA_HASH({1024});
  SHA_HASH({2,3,1,4,5}) = SHA_HASH(1..5);
  SHA_HASH({2,3,1,4,5}*{TRUE}) = SHA_HASH({x,y|x:1..5 & (y=TRUE <=> x<6)});
  SHA_HASH({2,3,1,4,5}) /= SHA_HASH({2,3,1,4});
  SHA_HASH_HEX({2,3,1,4,5}) = SHA_HASH_HEX(1..5);
  SHA_HASH_HEX({2,3,1,4,5}) /= SHA_HASH_HEX({2,3,1,4})
END

The -prob-profile command above will also print out information about calls to external functions. This command generates a CSV table of the called external functions; instead of user_output you should provide the name of a file:

probcli TestLibraryHash.mch -init -repl -csv prob_external_fun_profile_info user_output -assertions -p PROFILING_INFO TRUE
...
Calling table command prob_external_fun_profile_info
Operation/Action Total Runtime (ms) Total Walltime (ms) # Calls Max. Walltime (ms) Max. Witness ID Min. Walltime (ms)
SHA_HASH 0 1 16 1 unknown 0
SHA_HASH_HEX 0 0 8 0 unknown 0
Finished exporting prob_external_fun_profile_info to user_output