Optimizing for model checking

[jack.va...@gmail.com]

Hi,

Is there guidance or any in depth write ups about optimizing specifications for model checking runtime?

I already use state constraints in my model as the primary way of limiting TLC runtime and resource usage. Also I turn off profiling and use symmetry sets where possible.

I would love to know of any useful state space limiting techniques people have used (beyond simple state constraints).

After that I am thinking that choice of data structure matters. For example, looking up a value in a function would be more efficient than scanning a set or sequence.

Any guidance or write-ups on this subject would be greatly appreciated.

Jack

[Markus Kuppe]

Hi Jack,

"Large Scale Model Checking 101" [5] discusses how to speed up TLC. In
addition, you might want to profile a smaller model to identify
operators that are bottlenecks ("The TLA+ Toolbox" [6] has a section
about the profiler). Afterwards, redefine those operators in the model
with more efficient ones. If this is still not good enough, consider to
implement your TLA+ operators in Java. The CommunityModules [1] have
several examples [2][3] how this can be done and recent TLC nightly
builds comes with annotations that make this easier [7].

Symmetry sets and state constraints indicates that you primarily check
safety properties. If you don't mind running an early prototype, I can
share a version of TLC that scales better with more cores (on a machine
with 16 cores, it doubles throughput [4]).

Hope this helps,
Markus

[1] https://github.com/tlaplus/CommunityModules/
[2]
https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.java
[3]
https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/TLCExt.java
[4] https://twitter.com/lemmster/status/1209277186416361472
[5] https://vimeo.com/264959035/
[6] https://arxiv.org/abs/1912.10633
[7]
https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/tlc2/overrides/TLAPlusOperator.java

[jack.va...@gmail.com]

Hi Markus,

Thanks very much, I will start with profiling for bottlenecks and optimizing those and see how far I get with that.

I run TLC on a 16 core machine so I would be very interested in that build thanks.

Jack