Line 132: | Line 132: | ||

</pre> | </pre> | ||

== Debugging Constant Size | == 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 <tt>constants_analysis</tt> command. | |||

It generates a CSV table which can be inspected in an editor or a spreadsheet program. | 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. | 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. | 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). | By default, concrete constants will be evaluated (unless they are known to be infinite or larger or annotated as symbolic). | ||

Line 145: | Line 148: | ||

- annotating the constant with the <tt>/@ desc expand */</tt> pragma to force expansion | - annotating the constant with the <tt>/@ desc expand */</tt> pragma to force expansion | ||

- annotating the constant with the <tt>/@desc memo */</tt> pragma to memoize its evaluation (i.e., cache evaluation results involving the constant) | - annotating the constant with the <tt>/@desc memo */</tt> 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: | |||

<pre> | <pre> | ||

Line 159: | Line 164: | ||

c2 = {x | x:1..10000 & x mod 100 = 0} & | c2 = {x | x:1..10000 & x mod 100 = 0} & | ||

c3 = %x.(x:1..100|x*x) | c3 = %x.(x:1..100|x*x) | ||

END | |||

</pre> | |||

The command can now be run as follows: | |||

<pre> | |||

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

</pre> | |||

Let us now add pragmas to study their influence: | |||

<pre> | |||

MACHINE DebugSymbolicConstants_pragmas | |||

ABSTRACT_CONSTANTS | |||

a1 /*@desc expand*/, a2 /*@desc expand*/, a3 /*@desc expand*/ | |||

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 = /*@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 | END | ||

</pre> | </pre> | ||

<pre> | <pre> | ||

probcli | probcli DebugSymbolicConstants.mch -init -csv constants_analysis user_output | ||

... | ... | ||

Calling table command constants_analysis | Calling table command constants_analysis |

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

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

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

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:

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

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:

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

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

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

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

$ probcli ../prob_examples/public_examples/B/Tutorial/Debug.mch -execute_all -prob_profile ... -------------------------- ProB profile info after 5685 ms walltime (5248 ms runtime) ----Source Location Profiler Information---- ----Tracks number of times B statements (aka substitutions) are hit 1 hits at 9:15 -- 9:19 in /Users/leuschel/git_root/prob_examples/public_examples/B/Tutorial/Debug.mch 1 hits at 12:37 -- 12:41 in /Users/leuschel/git_root/prob_examples/public_examples/B/Tutorial/Debug.mch 4 hits at 11:29 -- 11:38 in /Users/leuschel/git_root/prob_examples/public_examples/B/Tutorial/Debug.mch ---- ---- ProB Runtime Profiler ---- ---- Tracks time spent in B operations and invariant evaluation $setup_constants : 78 ms (80 ms walltime & 80 ms max. walltime; #calls 1) Sqr : 9 ms (9 ms walltime & 9 ms max. walltime; #calls 1) $initialise_machine : 5 ms (5 ms walltime & 5 ms max. walltime; #calls 1) Finished : 3 ms (4 ms walltime & 4 ms max. walltime; #calls 1) Total Walltime: 98 ms for #calls 4