Re: [tlaplus] Optimizing for model checking

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 24.12.19 03:16, jack.vanlightly@xxxxxxxxx wrote:
> 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
> 

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b192b1e3-04e0-e039-693f-f5fc4877fb93%40lemmster.de.