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

Re: [tlaplus] Count the time spent on the check of an invariant or a property with TLC

On 2/10/23 7:15 AM, Stephan Merz wrote:
Invariants are evaluated concurrently with state space generation: by default, TLC stops generating new states when an invariant evaluates to false. One could certainly measure the time that TLC spends on evaluating the invariants but currently this is not done.

The TLC Profiler [1] provides insights into the evaluation frequency of an invariant and its constituent formulas, as well as their memory usage. Overriding certain parts of an invariant with a Java module override can be beneficial, and the CommunityModules repository on GitHub [2] is a great starting point for discovering operators with overrides.


[1] https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/profiling.html, [2] https://github.com/tlaplus/CommunityModules

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/0eadf8c9-f310-cbe9-b767-cc22971b4725%40lemmster.de.