[tlaplus] Optimizing for model checking

[jack.vanlightly@xxxxxxxxx]

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

-- 
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/99e3bafe-d932-4548-a2ab-91f98346a5c6%40googlegroups.com.