Caching Constants and Operations: Difference between revisions

No edit summary
Line 19: Line 19:
* -show_cache
* -show_cache
In verbose mode (-v flag) more details are displayed.
In verbose mode (-v flag) more details are displayed.
<pre>
probcli CrewAllocationConstants.mch -t  -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)} )
</pre>

Revision as of 06:34, 15 May 2021

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

Activating Caching

In the command-line version probcli the cache can be activated using the option

  • -cache DIRECTORY

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.

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

Inspecting the Cache

In the command-line version probcli a summary of the cache can be displayed using this option (together with the -cache option mentioned above).

  • -show_cache

In verbose mode (-v flag) more details are displayed.

probcli CrewAllocationConstants.mch -t  -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)} )