Debugging - Revision history

Michael Leuschel: /* Debugging individual operation executions */

2026-03-27T10:18:36Z

Debugging individual operation executions

← Older revision		Revision as of 10:18, 27 March 2026
Line 308:		Line 308:
	</pre>		</pre>

	== Debugging ~~individual operation executions~~ ==		== Debugging Operation Executions ==

	After setting the preference <tt>STORE_DETAILED_TRANSITION_INFOS</tt> to TRUE, ProB will store additional execution information about operations. You can see this info by right-clicking in the operations view of ProB Tcl/Tk or ProB2-UI.		After setting the preference <tt>STORE_DETAILED_TRANSITION_INFOS</tt> to TRUE, ProB will store additional execution information about operations. You can see this info by right-clicking in the operations view of ProB Tcl/Tk or ProB2-UI.

Michael Leuschel: /* Debugging Animation or Execution */

2026-03-27T10:18:14Z

Debugging Animation or Execution

← Older revision		Revision as of 10:18, 27 March 2026
Line 307:		Line 307:
	% Runtime for -execute: 116 ms (with gc: 116 ms, walltime: 119 ms); time since start: 1132 ms		% Runtime for -execute: 116 ms (with gc: 116 ms, walltime: 119 ms); time since start: 1132 ms
	</pre>		</pre>

			== Debugging individual operation executions ==

			After setting the preference <tt>STORE_DETAILED_TRANSITION_INFOS</tt> to TRUE, ProB will store additional execution information about operations. You can see this info by right-clicking in the operations view of ProB Tcl/Tk or ProB2-UI.
			When setting this preference, the same transition can be added multiple times to the state space, namely if the execution details differ.
			This feature can be useful to debug unexpected non-determinism:
			* you can inspect the transition infos of two executions and compare them (you can also put them into a file and use diff)

	== Profiling ==		== Profiling ==

Michael Leuschel: /* TRACE_INFO preference */

2025-03-06T17:27:06Z

TRACE_INFO preference

← Older revision		Revision as of 17:27, 6 March 2025
Line 84:		Line 84:
	With this feature you can observe how constants get bound to values and can sometimes spot expensive predicates and large values.		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]].		Some additional information about debugging the PROPERTIES can be found in the [[Tutorial Troubleshooting the Setup]].
			The preference also helps debugging the <tt>INITIALISATION</tt> clause of a B machine.

	Let us take the following machine		Let us take the following machine

Michael Leuschel at 07:04, 7 October 2024

2024-10-07T07:04:41Z

← Older revision		Revision as of 07:04, 7 October 2024
Line 78:		Line 78:

	== Debugging Constants Setup ==		== Debugging Constants Setup ==

			=== TRACE_INFO preference ===

	By setting the preference <tt>TRACE_INFO</tt> to <tt>TRUE</tt> ProB will print additional messages when evaluating certain predicates, in particular the <tt>PROPERTIES</tt> clause of a B machine.		By setting the preference <tt>TRACE_INFO</tt> to <tt>TRUE</tt> ProB will print additional messages when evaluating certain predicates, in particular the <tt>PROPERTIES</tt> clause of a B machine.
Line 132:		Line 134:
	</pre>		</pre>

	ProB now also supports profiling the computation of constants defined by equations in the PROPERTIES.		=== Profiling Constants Computation Time ===
	~~This~~ can be achieved using the following table command <tt>-csv prob_constants_profile_info FILE</tt>.		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 <tt>-csv prob_constants_profile_info FILE</tt>:
	<pre>		<pre>
	probsli DebugSymbolicConstants.mch -csv prob_constants_profile_info user_output -init -p PROFILING_INFO TRUE -p PERFORMANCE_INFO TRUE		probsli DebugSymbolicConstants.mch -csv prob_constants_profile_info user_output -init -p PROFILING_INFO TRUE -p PERFORMANCE_INFO TRUE

Michael Leuschel: /* Debugging Constants Setup */

2024-10-07T07:00:44Z

Debugging Constants Setup

@@ Line 100: / Line 100: @@
 </pre>
-Here is how we can debug the constants setup:
+Here is how we can debug the constants setup using the <TT>TRACE_INFO</tt> preference:
 <pre>
@@ Line 131: / Line 131: @@
   [=OK= 0 ms]
 </pre>
 == Debugging Constant Size ==

Michael Leuschel: /* Debugging Constant Size */

2024-09-30T11:36:27Z

Debugging Constant Size

← Older revision		Revision as of 11:36, 30 September 2024
Line 249:		Line 249:
	</pre>		</pre>
	The command is also available by right-clicking on an identifier in the Evaluation View of ProB Tcl/Tk.		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 <pre>-csv constant_expr_analysis FILE</pre> 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 <tt>-lint</tt> command.
			You can also execute <tt>-lint_operations</tt>, which will not generate a CSV table.

	== Debugging Animation or Execution ==		== Debugging Animation or Execution ==

Michael Leuschel: /* Profiling External Function Calls */

2024-09-28T06:12:29Z

Profiling External Function Calls

← Older revision		Revision as of 06:12, 28 September 2024
Line 354:		Line 354:
	Calling table command prob_external_fun_profile_info		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)		Operation/Action Total Runtime (ms) Total Walltime (ms) # Calls Max. Walltime (ms) Max. Witness ID Min. Walltime (ms)
	SHA_HASH~~::external_functions~~ 0 1 16 1 unknown 0		SHA_HASH 0 1 16 1 unknown 0
	SHA_HASH_HEX~~::external_functions~~ 0 1 8 1 unknown 0		SHA_HASH_HEX 0 0 8 0 unknown 0
	Finished exporting prob_external_fun_profile_info to user_output		Finished exporting prob_external_fun_profile_info to user_output
	</pre>		</pre>

Michael Leuschel: /* Profiling External Function Calls */

2024-09-28T06:11:52Z

Profiling External Function Calls

← Older revision		Revision as of 06:11, 28 September 2024
Line 348:		Line 348:
	END		END
	</pre>		</pre>
	~~Then this~~ command generates a CSV table of the called external functions; instead of user_output you should provide the name of a file:		The <tt>-prob-profile</tt> 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:
	<pre>		<pre>
	probcli TestLibraryHash.mch -init -repl -csv prob_external_fun_profile_info user_output -assertions -p PROFILING_INFO TRUE		probcli TestLibraryHash.mch -init -repl -csv prob_external_fun_profile_info user_output -assertions -p PROFILING_INFO TRUE

Michael Leuschel: /* Profiling */

2024-09-27T17:33:40Z

Profiling

← Older revision		Revision as of 17:33, 27 September 2024
Line 284:		Line 284:

	<pre>		<pre>
	$ probcli ../prob_examples/public_examples/B/Tutorial/Debug.mch -execute_all -prob_profile		$ 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 profile info~~ after ~~5685~~ ms walltime (~~5248~~ ms runtime)		PROB PROFILING INFORMATION after 426 ms walltime (268 ms runtime) 168.843 MB
	~~----Source Location Profiler Information----~~		No source profiling information available
	~~----Tracks number of times B statements (aka substitutions) are hit~~		Set preference SOURCE_PROFILING_INFO to TRUE
	~~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 ----		---- ProB Runtime Profiler ----
	---- ~~Tracks time~~ spent in B operations and invariant evaluation		---- Time spent in B operations and invariant evaluation
	$setup_constants : 78 ms (80 ms walltime & 80 ms ~~max.~~ walltime; #calls 1)		Operation : Total Runtime ms (Total ms walltime & Minimum - Maximum ms walltime; #calls Number of Calls)
	Sqr : 9 ms (9 ms walltime & 9 ms ~~max.~~ walltime; #calls 1)		$setup_constants : 2 ms (2 ms walltime & 2 - 2 ms walltime; #calls 1)
	$initialise_machine : 5 ms (5 ms walltime & 5 ms ~~max.~~ walltime; #calls 1)		INVARIANT : 1 ms (0 ms walltime & 0 - 0 ms walltime; #calls 7)
	~~Finished~~ : 3 ms (4 ms walltime & 4 ms ~~max.~~ walltime; #calls 1)		Finished : 0 ms (1 ms walltime & 1 - 1 ms walltime; #calls 1)
	Total Walltime: 98 ms for #calls 4		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
	</pre>		</pre>

Michael Leuschel: /* Profiling */

2024-09-27T17:32:21Z

Profiling

← Older revision		Revision as of 17:32, 27 September 2024
Line 305:		Line 305:
	Note, if you memoize functions you can also inspect time spent in evaluating function calls. E.g., if you set the preference <tt> MEMOIZE_FUNCTIONS</tt> to true then all abstract constants will be memoised and you can inspect number of calls and time.		Note, if you memoize functions you can also inspect time spent in evaluating function calls. E.g., if you set the preference <tt> MEMOIZE_FUNCTIONS</tt> to true then all abstract constants will be memoised and you can inspect number of calls and time.
	See [[Memoization_for_Functions]].		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):
			<pre>
			$ 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
			</pre>

			=== Profiling External Function Calls ===

			You can also generate a profile of the external functions called.
			Take for example this machine:
			<pre>
			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
			</pre>
			Then this command generates a CSV table of the called external functions; instead of user_output you should provide the name of a file:
			<pre>
			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::external_functions 0 1 16 1 unknown 0
			SHA_HASH_HEX::external_functions 0 1 8 1 unknown 0
			Finished exporting prob_external_fun_profile_info to user_output
			</pre>