Tutorial Tuning Model Checking - Revision history

Michael Leuschel: /* Operation Caching (Reuse) */

2021-09-10T15:19:04Z

Operation Caching (Reuse)

← Older revision		Revision as of 15:19, 10 September 2021
Line 338:		Line 338:
	You can inspect statistics of the operation caching using the <tt>-op-cache-statistics</tt> command:		You can inspect statistics of the operation caching using the <tt>-op-cache-statistics</tt> command:
	<pre>		<pre>
	probcli IncrementalStatePackingTestLargeSlow.mch --model-check -memory -p COMPRESSION TRUE -p OPERATION_REUSE full -disable-time-out -op-cache-~~statistics~~		probcli IncrementalStatePackingTestLargeSlow.mch --model-check -memory -p COMPRESSION TRUE -p OPERATION_REUSE full -disable-time-out -op-cache-profile
	...		...
	PROB OPERATION_REUSE (full) STATISTICS		PROB OPERATION_REUSE (full) STATISTICS
Line 355:		Line 355:
	----------		----------
	</pre>		</pre>

			A shorter summary can be obtained using the <tt>-op_cache_stats</tt> command.

	=== Partial Order Reduction ===		=== Partial Order Reduction ===

Michael Leuschel: /* Operation Caching (Reuse) */

2021-09-06T08:52:36Z

Operation Caching (Reuse)

@@ Line 333: / Line 333: @@
 ...
 LTSMin found no counter example
 </pre>

Michael Leuschel: /* Operation Caching (Reuse) */

2021-09-06T08:49:59Z

Operation Caching (Reuse)

← Older revision		Revision as of 08:49, 6 September 2021
Line 296:		Line 296:
	ALL OPERATIONS COVERED		ALL OPERATIONS COVERED
	% All open nodes visited		% All open nodes visited
	Model checking time: ~~8752~~ ms (~~9730~~ ms walltime)		Model checking time: 8267 ms (9234 ms walltime)
	States analysed: 9000		States analysed: 9000
	Transitions fired: 44992		Transitions fired: 44992
	No counter example found. ALL nodes visited.		No counter example found. ALL nodes visited.
	ProB memory used: ~~179~~.~~969~~ MB ( 75.~~111~~ MB program)		ProB memory used: 181.807 MB ( 76.949 MB program)
	</pre>		</pre>

	Note: on this example [[TLC\|TLC]] ~~does fare better then ProB in default settings, but~~ is slower than ProB with operation reuse:		Note that setting COMPRESSION to TRUE typically speeds up model checking with operation reuse (the compression typically simplifies the hashing that is done by the operation reuse).
			In the above case the model checking walltime is 10.85 seconds without COMPRESSION.
			With <tt>-disable-time-out</tt> (see above) and with COMPRESSION the walltime is 8.35 seconds

			Note: on this example [[TLC\|TLC]] is slower than ProB with operation reuse enabled:
	<pre>		<pre>
	probcli ~~IncrementalStatePackingTestLarge~~.mch -mc_with_tlc		probcli IncrementalStatePackingTestLargeSlow.mch -mc_with_tlc
	...		...
	Parsing time: ~~199~~ ms		Parsing time: 195 ms
	Translation time: 29 ms		Translation time: 30 ms
	Model checking time: 32 sec		Model checking time: 31 sec
	States analysed: 9000		States analysed: 9000
	Transitions fired: 44992		Transitions fired: 44992
	Result: NoError		Result: NoError
	exit : exit(0) walltime: ~~33551~~ ms		exit : exit(0) walltime: 31930 ms
	</pre>		</pre>

Line 319:		Line 323:
	probcli IncrementalStatePackingTestLargeSlow.mch -mc_with_tlc -p TLC_WORKERS 3		probcli IncrementalStatePackingTestLargeSlow.mch -mc_with_tlc -p TLC_WORKERS 3
	...		...
	exit : exit(0) walltime: ~~26501~~ ms		exit : exit(0) walltime: 25332 ms
	</pre>		</pre>

Michael Leuschel: /* Using other model checking backends (TLC and LTSmin) */

2021-05-29T08:57:16Z

Using other model checking backends (TLC and LTSmin)

← Older revision		Revision as of 08:57, 29 May 2021
Line 219:		Line 219:
	In general you can try and use [[ParB\|ParB]] to parallelize ProB.		In general you can try and use [[ParB\|ParB]] to parallelize ProB.
	However, for this model unfortunately the use of parB actually slows down		However, for this model unfortunately the use of parB actually slows down
	the model checking.		the model checking (we are investigating why).

Michael Leuschel: /* Symmetry Reduction */

2021-05-29T08:56:30Z

Symmetry Reduction

@@ Line 364: / Line 364: @@
 === Symmetry Reduction ===
-Symmetry can achieve considerable reduction, but requires rewriting the model, e.g., to use a deferred set rather than an enumerate set.
+[[Symmetry_Reduction|The use of symmetry]] can lead to as considerable reduction, but requires rewriting the model, e.g., to use a deferred set rather than an enumerate set.
 However, one can also force symmetry, by declaring to ProB that an enumerated set should be treated as a symmetric set:
@@ Line 373: / Line 373: @@
 </pre>
-You can see that this reduces the number of nodes from 9001 to 2001, but unfortunately increases runtime (possibly because compression does not work properly with symmetry):
+You can see that this reduces the number of nodes from 9000 to 2000, and decreases runtime almost by half:
 <pre>
@@ Line 388: / Line 402: @@
 No counter example found. ALL nodes visited.
 ProB memory used:  423.656 MB ( 318.799 MB program)
 </pre>

Michael Leuschel: /* Symmetry Reduction */

2021-05-29T08:50:20Z

Symmetry Reduction

← Older revision		Revision as of 08:50, 29 May 2021
Line 373:		Line 373:
	</pre>		</pre>

	You can see that this reduces the number of nodes from 9001 to 2001, but unfortunately increases runtime:		You can see that this reduces the number of nodes from 9001 to 2001, but unfortunately increases runtime (possibly because compression does not work properly with symmetry):

	<pre>		<pre>

Michael Leuschel: /* Symmetry Reduction */

2021-05-29T08:48:10Z

Symmetry Reduction

← Older revision		Revision as of 08:48, 29 May 2021
Line 365:		Line 365:

	Symmetry can achieve considerable reduction, but requires rewriting the model, e.g., to use a deferred set rather than an enumerate set.		Symmetry can achieve considerable reduction, but requires rewriting the model, e.g., to use a deferred set rather than an enumerate set.
			However, one can also force symmetry, by declaring to ProB that an enumerated set should be treated as a symmetric set:

			<pre>
			MACHINE IncrementalStatePackingTestLarge_v2
			DEFINITIONS FORCE_SYMMETRY_ID == TRUE
			...
			</pre>

			You can see that this reduces the number of nodes from 9001 to 2001, but unfortunately increases runtime:

			<pre>
			probcli IncrementalStatePackingTestLarge_v2.mch -model-check -p COMPRESSION TRUE -memory -p SYMMETRY_MODE hash
			% unused_constants(1,[zz])
			FORCING SYMMETRY: ID % Runtime for SOLUTION for SETUP_CONSTANTS: 94 ms (walltime: 97 ms)
			% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)

			ALL OPERATIONS COVERED
			% All open nodes visited
			Model checking time: 3255 ms (3352 ms walltime)
			States analysed: 2001
			Transitions fired: 10000
			No counter example found. ALL nodes visited.
			ProB memory used: 423.656 MB ( 318.799 MB program)
			</pre>

Michael Leuschel: /* Operation Caching (Reuse) */

2021-05-29T08:45:37Z

Operation Caching (Reuse)

← Older revision		Revision as of 08:45, 29 May 2021
Line 283:		Line 283:
	probcli IncrementalStatePackingTestLargeSlow.mch --model-check -memory -p COMPRESSION TRUE		probcli IncrementalStatePackingTestLargeSlow.mch --model-check -memory -p COMPRESSION TRUE
	...		...
	* ~~2025~~ states checked (48.6% of total ~~4169~~), ~~10121~~ transitions, ~~168~~.~~719~~ MB		* 5000 states checked (66.3% of total 7540), 24987 transitions, 175.097 MB
	* currently checking 14.52 states/sec, adding 37.02 new states/sec		* currently checking 15.08 states/sec, adding 15.45 new states/sec
	* walltime 2.4 minutes~~, percentage of checked states decreasing from 50.7%~~		* walltime 5.6 minutes
	...		...
	</pre>		</pre>
Line 330:		Line 330:
	LTSMin found no counter example		LTSMin found no counter example
	</pre>		</pre>


	=== Partial Order Reduction ===		=== Partial Order Reduction ===

Michael Leuschel: /* Partial Order Reduction */

2021-05-29T08:36:41Z

Partial Order Reduction

← Older revision		Revision as of 08:36, 29 May 2021
Line 334:		Line 334:
	=== Partial Order Reduction ===		=== Partial Order Reduction ===

	In principle [[~~Tutorial_Various_Optimizati~~\|partial order reduction]] can help, in particular for deadlock checking.		In principle [[Tutorial_Various_Optimizations\|partial order reduction]] can help, in particular for deadlock checking.
	Looking at the original example we get:		Looking at the original example we get:

Michael Leuschel: /* Partial Order Reduction */

2021-05-29T08:36:23Z

Partial Order Reduction

← Older revision		Revision as of 08:36, 29 May 2021
Line 334:		Line 334:
	=== Partial Order Reduction ===		=== Partial Order Reduction ===

	In principle partial order reduction can help.		In principle [[Tutorial_Various_Optimizati\|partial order reduction]] can help, in particular for deadlock checking.
	~~But for this~~ example ~~the optimisation~~ does not pay off		Looking at the original example we get:

			<pre>
			probcli IncrementalStatePackingTestLarge.mch -model-check -p COMPRESSION TRUE -memory -p por ample_sets -noinv -noass

			ALL OPERATIONS COVERED
			% All open nodes visited
			Model checking time: 45 ms (66 ms walltime)
			States analysed: 18
			Transitions fired: 29
			No counter example found. ALL nodes visited.
			ProB memory used: 162.450 MB ( 57.592 MB program)
			</pre>

			For invariant checking it does not pay off, and actually makes runtime worse:

	<pre>		<pre>
	probcli IncrementalStatePackingTestLarge.mch -model-check -p COMPRESSION TRUE -memory -p por ample_sets		probcli IncrementalStatePackingTestLarge.mch -model-check -p COMPRESSION TRUE -memory -p por ample_sets -nodead -noass

	ALL OPERATIONS COVERED		ALL OPERATIONS COVERED
	% All open nodes visited		% All open nodes visited
	Model checking time: ~~13248~~ ms (~~16266~~ ms walltime)		Model checking time: 13935 ms (17163 ms walltime)
	States analysed: 9000		States analysed: 9000
	Transitions fired: ~~36004~~		Transitions fired: 35875
	No counter example found. ALL nodes visited.		No counter example found. ALL nodes visited.
	ProB memory used: 178.~~722~~ MB ( 73.~~865~~ MB program)		ProB memory used: 178.822 MB ( 73.964 MB program)
	</pre>		</pre>