ProB can store the values of constants and operations in a cache file. Compared to 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. (It thus may make sense to activate both of these features.)
In the command-line version probcli the cache can be activated using the option
This means that cache results will be stored in that directory. The directory may contain multiple files, namely one file per B machine. The files contain a hash to detect whether they are still up-to-date.
The same option has to be used to activate the caching for ProB Tcl/Tk, i.e., you need to launch ProB Tcl/Tk from the command-line with the -cache option:
Caching is currently only available for classical B machines without refinement, and when symmetry reduction is off (which it is by default). (Note to developers: the conditions are checked in the Prolog predicate cache_is_applicable in the module value_persistance.pl). The cache feature can, however, deal with composed machines (e.g., with INCLUDES, USES, SEES) and stores constant values for individual sub-machines.
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,...) If the cache cannot be re-used a message will be displayed:
value caching: general computations parameters have changed, no re-use of stored operations
In the command-line version probcli a summary of the cache can be displayed using this option (together with the -cache option mentioned above).
In verbose mode (-v flag) more details are displayed, but the additional information is probably only useful for ProB developers.
probcli CrewAllocationConstants.mch -cache cache/ -show-cache
Contents of cache file cache/CrewAllocationConstants.probcst of type constants for machine CrewAllocationConstants:
( male={(tom|->TRUE),(david|->TRUE),(jeremy|->TRUE),(carol|->FALSE),(janet|->FALSE),(tracy|->FALSE)} &
speaks={(tom|->german),(david|->french),(jeremy|->german),(carol|->spanish),(janet|->french),(tracy|->spanish)} &
assign={(1|->tom),(1|->david),(1|->jeremy),(1|->carol),(1|->janet),(1|->tracy),(2|->tom),(2|->david),(2|->carol),(3|->jeremy),(3|->janet),(3|->tracy)} )