Caching Constants and Operations - Revision history

Michael Leuschel: /* Other Useful CLI commands */

2026-04-15T06:43:22Z

Other Useful CLI commands

← Older revision		Revision as of 06:43, 15 April 2026
Line 190:		Line 190:
	* -clear_cache to clear the cache		* -clear_cache to clear the cache
	* -clear_cache_for M to clear the cache for the machine M		* -clear_cache_for M to clear the cache for the machine M
			* -ignore_cache_for P to ignore the cache for all machines whose name starts with P
	* -show_inclusion_hierarchy to display the list of included subsidiary machines and a minimal cover		* -show_inclusion_hierarchy to display the list of included subsidiary machines and a minimal cover

Line 197:		Line 198:
	for all machines in that list you can pre-populate the cache with all		for all machines in that list you can pre-populate the cache with all
	the necessary constants.		the necessary constants.


	=== Useful Preferences ===		=== Useful Preferences ===

Michael Leuschel: /* Example */

2026-01-29T15:05:22Z

Example

← Older revision		Revision as of 15:05, 29 January 2026
Line 183:		Line 183:


	=== ~~Example~~ ===		=== Other Useful CLI commands ===

	The following commands can also be useful:		The following commands can also be useful:
Line 197:		Line 197:
	for all machines in that list you can pre-populate the cache with all		for all machines in that list you can pre-populate the cache with all
	the necessary constants.		the necessary constants.


			=== Useful Preferences ===

			* CACHE_CONSTANTS (default true): Cache constant values when -cache is activated
			* CACHE_OPERATIONS (default true): Cache operations/events when -cache is activated
			* CACHE_OPERATIONS_RUNTIME_LIMIT (default 0): Minimal runtime for operations to be stored in -cache

Michael Leuschel at 15:03, 29 January 2026

2026-01-29T15:03:00Z

← Older revision		Revision as of 15:03, 29 January 2026
Line 180:		Line 180:
	maxprime=9973 )		maxprime=9973 )
	</pre>		</pre>



			=== Example ===

			The following commands can also be useful:
			* -ccache DIR works like -cache DIR but creates the directory if it does not exist
			* -cache_statistics to print statistics about cache re-use
			* -clear_cache to clear the cache
			* -clear_cache_for M to clear the cache for the machine M
			* -show_inclusion_hierarchy to display the list of included subsidiary machines and a minimal cover

			The latter command produces a list of sufficient includes to cover all machines.
			By performing
			probcli FILE.mch -init -cache DIR
			for all machines in that list you can pre-populate the cache with all
			the necessary constants.

Michael Leuschel: /* Inspecting the Cache */

2026-01-29T14:55:52Z

Inspecting the Cache

← Older revision		Revision as of 14:55, 29 January 2026
Line 36:		Line 36:
	In the [[Using_the_Command-Line_Version_of_ProB\|command-line version probcli]] a summary of the cache can be displayed using this option (together with the -cache option mentioned above).		In the [[Using_the_Command-Line_Version_of_ProB\|command-line version probcli]] a summary of the cache can be displayed using this option (together with the -cache option mentioned above).
	* -show_cache		* -show_cache
	In verbose mode (-v flag) more details are displayed, but the additional information is probably only useful for ProB developers.		In verbose mode (-v flag) more details are displayed, but the additional information is probably only useful for ProB developers. You can also use -show_cache_verbose to this effect.

	<pre>		<pre>

Michael Leuschel: /* Example */

2022-06-23T11:31:33Z

Example

← Older revision		Revision as of 11:31, 23 June 2022
Line 114:		Line 114:
	$ probcli PrimeNumbers.mch -init -cache ./cache/ -show_cache		$ probcli PrimeNumbers.mch -init -cache ./cache/ -show_cache

	Contents of cache file ~~/Users/leuschel/git_root/prob_prolog~~/cache/PrimeNumbers.probcst of type constants for machine PrimeNumbers:		Contents of cache file ./cache/PrimeNumbers.probcst of type constants for machine PrimeNumbers:
	( n=1000 &		( n=1000 &
	primes=#168:{2,3,...,991,997} &		primes=#168:{2,3,...,991,997} &
Line 162:		Line 162:
	% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)		% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)

	Contents of cache file ~~/Users/leuschel/git_root/prob_prolog~~/cache/PrimeNumberSum.probcst of type constants for machine PrimeNumberSum:		Contents of cache file ./cache/PrimeNumberSum.probcst of type constants for machine PrimeNumberSum:
	( mx=1000 &		( mx=1000 &
	n=1000 &		n=1000 &
Line 172:		Line 172:
	maxprime=9973 )		maxprime=9973 )

	Contents of cache file ~~/Users/leuschel/git_root/prob_prolog~~/cache/PrimeNumbers.probcst of type constants for machine PrimeNumbers:		Contents of cache file ./cache/PrimeNumbers.probcst of type constants for machine PrimeNumbers:
	( n=1000 &		( n=1000 &
	primes=#168:{2,3,...,991,997} &		primes=#168:{2,3,...,991,997} &

Michael Leuschel: /* Example */

2022-06-23T11:30:57Z

Example

← Older revision		Revision as of 11:30, 23 June 2022
Line 78:		Line 78:

	<pre>		<pre>
	$ time probcli ~~/Users/leuschel/git_root/prob_examples/public_examples/B/PerformanceTests/Cache/~~PrimeNumbers.mch -init		$ time probcli PrimeNumbers.mch -init
	% Runtime for SOLUTION for SETUP_CONSTANTS: 137 ms (walltime: 140 ms)		% Runtime for SOLUTION for SETUP_CONSTANTS: 137 ms (walltime: 140 ms)
	% Runtime for SOLUTION for SETUP_CONSTANTS: 1176 ms (walltime: 1187 ms)		% Runtime for SOLUTION for SETUP_CONSTANTS: 1176 ms (walltime: 1187 ms)
Line 102:		Line 102:
	The second time around we get a much faster performance; the values of the constants are simply restored from disk:		The second time around we get a much faster performance; the values of the constants are simply restored from disk:
	<pre>		<pre>
	~~leuschel@Michas-MBA13-LAN prob_prolog (develop *)~~$ time probcli PrimeNumbers.mch -init -cache ./cache/		$ time probcli PrimeNumbers.mch -init -cache ./cache/

	real 0m1.210s		real 0m1.210s

Michael Leuschel at 11:24, 23 June 2022

2022-06-23T11:24:26Z

← Older revision		Revision as of 11:24, 23 June 2022
Line 1:		Line 1:
	ProB can store the values of constants and operations in a cache file.		ProB can store the values of constants and operations in a cache file.
	Compared to [[Memoization_for_Functions\|memoization for functions]] and		Compared to [[Memoization_for_Functions\|memoization for functions]] and
	[[Tutorial_Tuning_Model_Checking#Operation_Caching_.28Reuse.29\|operation reuse during model checking]], this caching is persistent across different runs of probcli or ProB Tcl/Tk and is applicable to the constant setup and operations, not at the level of (constant) functions.		[[Tutorial_Tuning_Model_Checking#Operation_Caching_.28Reuse.29\|operation reuse during model checking]], this caching is persistent across different runs of probcli or ProB Tcl/Tk and is applicable to the constant setup and operations, not at the level of computation of values using (constant) functions.
	(It thus may make sense to activate both ~~of these features~~.)		(It thus may make sense to activate both [[Memoization_for_Functions\|memoization]] and caching.)

	=== Activating Caching ===		=== Activating Caching ===

Michael Leuschel at 16:17, 2 October 2021

2021-10-02T16:17:22Z

← Older revision		Revision as of 16:17, 2 October 2021
Line 1:		Line 1:
	ProB can store the values of constants and operations in a cache file.		ProB can store the values of constants and operations in a cache file.
	Compared to [[Memoization_for_Functions\|memoization for functions]], this caching is persistent across different runs of probcli or ProB Tcl/Tk and is applicable to the constant setup and operations, not at the level of (constant) functions.		Compared to [[Memoization_for_Functions\|memoization for functions]] and
			[[Tutorial_Tuning_Model_Checking#Operation_Caching_.28Reuse.29\|operation reuse during model checking]], this caching is persistent across different runs of probcli or ProB Tcl/Tk and is applicable to the constant setup and operations, not at the level of (constant) functions.
	(It thus may make sense to activate both of these features.)		(It thus may make sense to activate both of these features.)

Michael Leuschel at 06:48, 16 May 2021

2021-05-16T06:48:40Z

← Older revision		Revision as of 06:48, 16 May 2021
Line 25:		Line 25:
	* no time-out occurred		* no time-out occurred
	* all enabled operations were computed (i.e., the MAX_OPERATIONS limit was not reached)		* all enabled operations were computed (i.e., the MAX_OPERATIONS limit was not reached)
			* the preference CACHE_OPERATIONS is true (which it is by default; it is only available as of version 1.11.0)

	The cache file will also contain the values of relevant preferences, which can influence the computation of constants or operation results (e.g., MAXINT, MININT, DEFAULT_SETSIZE,...)		The cache file will also contain the values of relevant preferences, which can influence the computation of constants or operation results (e.g., MAXINT, MININT, DEFAULT_SETSIZE,...)
Line 129:		Line 130:
	The cache option is worthwhile for constants and operations which are computation intensive.		The cache option is worthwhile for constants and operations which are computation intensive.
	For example, it is not really worthwhile for the operation NextPrime.		For example, it is not really worthwhile for the operation NextPrime.
	~~In future we may provide a way~~ to ~~select to which operations cache is applied (ask us if you need this feature)~~.		As of version 1.11.0 you can turn off caching operations by setting the preference CACHE_OPERATIONS to FALSE.

	Note that the cache is also used for when other machines include a cached machine.		Note that the cache is also used for when other machines include a cached machine.

Michael Leuschel: /* Example */

2021-05-16T06:34:06Z

Example

← Older revision		Revision as of 06:34, 16 May 2021
Line 130:		Line 130:
	For example, it is not really worthwhile for the operation NextPrime.		For example, it is not really worthwhile for the operation NextPrime.
	In future we may provide a way to select to which operations cache is applied (ask us if you need this feature).		In future we may provide a way to select to which operations cache is applied (ask us if you need this feature).

			Note that the cache is also used for when other machines include a cached machine.
			Take for example:
			<pre>
			MACHINE PrimeNumberSum
			INCLUDES PrimeNumbers
			CONSTANTS
			mx
			PROPERTIES
			mx = n
			VARIABLES
			sum
			INVARIANT
			sum : 0..mx
			INITIALISATION
			sum := 1
			OPERATIONS
			Next(nxtP) = PRE nxtP:0..mx THEN
			NextPrime(nxtP) \|\| sum := sum + 1
			END
			END
			</pre>

			Then you see that the cache of the included machine is re-used straight away:
			<pre>
			$ probcli PrimeNumbersSum.mch -init -cache ./cache/ -show_cache
			% Runtime for SOLUTION for SETUP_CONSTANTS: 32 ms (walltime: 33 ms)
			% Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
			% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)

			Contents of cache file /Users/leuschel/git_root/prob_prolog/cache/PrimeNumberSum.probcst of type constants for machine PrimeNumberSum:
			( mx=1000 &
			n=1000 &
			primes=#168:{2,3,...,991,997} &
			maxprime=997 )
			( mx=10000 &
			n=10000 &
			primes=#1229:{2,3,...,9967,9973} &
			maxprime=9973 )

			Contents of cache file /Users/leuschel/git_root/prob_prolog/cache/PrimeNumbers.probcst of type constants for machine PrimeNumbers:
			( n=1000 &
			primes=#168:{2,3,...,991,997} &
			maxprime=997 )
			( n=10000 &
			primes=#1229:{2,3,...,9967,9973} &
			maxprime=9973 )
			</pre>