Caching Constants and Operations: Difference between revisions

ProB can store the values of constants and operations in a cache file. Compared to memoization for functions and 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 memoization and caching.)

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.

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:

• prob -cache DIRECTORY

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. Constants are cached when

• no time-out occurred during SET_UP_CONSTANTS
• all enabled solutions were computed (i.e., the MAX_INITIALISATIONS limit was not reached)
• the machine has no parameters

Operations are cached when

• no time-out occurred
• 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,...) 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, 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)} )

In Tcl/Tk this information can be obtained by choosing the command "Show ProB Cache Info" in the Debug menu.

Example

Take the following B machine

MACHINE PrimeNumbers
// A machine with a slow constant set up to check -cache option
DEFINITIONS SET_PREF_TIME_OUT == 10000
CONSTANTS n, primes, maxprime
PROPERTIES
 n:NATURAL1 &
 primes = {x|x:2..n & !y.(y>1 & y*y<=x => x mod y /= 0)} &
 (n = 10000 or n=1000) &
 maxprime = max(primes)
ASSERTIONS
 (n = 10000 => card(primes) = 1229)
VARIABLES x
INVARIANT
 x:2..n & x:primes
INITIALISATION x:=2
OPERATIONS
  NextPrime(nxt) = SELECT x<maxprime & 
                         nxt:primes & nxt = min(primes /\ (x+1)..n) THEN
       x:=nxt
  END
END

Without caching we have this behaviour:

$ time probcli PrimeNumbers.mch -init
% Runtime for SOLUTION for SETUP_CONSTANTS: 137 ms (walltime: 140 ms)
% Runtime for SOLUTION for SETUP_CONSTANTS: 1176 ms (walltime: 1187 ms)
% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)

real	0m2.549s
user	0m2.341s
sys	0m0.125s

With cache, we obviously do not yet see a benefit the first time around:

$ time probcli PrimeNumbers.mch -init -cache ./cache/
% Runtime for SOLUTION for SETUP_CONSTANTS: 134 ms (walltime: 136 ms)
% Runtime for SOLUTION for SETUP_CONSTANTS: 1161 ms (walltime: 1169 ms)
% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)

real	0m2.536s
user	0m2.311s
sys	0m0.134s

The second time around we get a much faster performance; the values of the constants are simply restored from disk:

$ time probcli PrimeNumbers.mch -init -cache ./cache/

real	0m1.210s
user	0m1.010s
sys	0m0.117s

We can inspect the cache contents either using probcli or inspecting the directory:

$ probcli PrimeNumbers.mch -init -cache ./cache/ -show_cache

Contents of cache file ./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 )

$ ls -l cache/
total 48
-rw-r--r--  1 leuschel  staff      0 15 May 16:25 PrimeNumbers.opdata
-rw-r--r--  1 leuschel  staff  14988 15 May 16:25 PrimeNumbers.probcst
-rw-r--r--  1 leuschel  staff   5831 15 May 16:26 PrimeNumbers.probops

The cache option is worthwhile for constants and operations which are computation intensive. For example, it is not really worthwhile for the operation NextPrime. 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. Take for example:

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

Then you see that the cache of the included machine is re-used straight away:

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