[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Optimizing for model checking
On 24.12.19 03:16, jack.vanlightly@xxxxxxxxx wrote:
> 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.
"Large Scale Model Checking 101"  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"  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  have
several examples  how this can be done and recent TLC nightly
builds comes with annotations that make this easier .
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 ).
Hope this helps,
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.