[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Optimizing for model checking


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.


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.