Count the time spent on the check of an invariant or a property with TLC

[Rivers Xiao]

Hi all! I want to compare the efficiency of two different invariants or properties. But TLC reports the time spent on both calculating states space and checking invariant/property. Can I get the time spent on the check of invariant/property separately?

For example, the spec DieHard has an invariant TypeOK. We can ask TLC to check this invariant when running the model check. TLC will report the elapsed time, which adds up the time spent on calculating states space and the time spent on checking TypeOK for every state. Can we use some configuration/option to tell TLC to report the time spent on checking TypeOK separately? Or do we have to modify the source code of TLC?

thx

[Stephan Merz]

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.

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/48cbb2d6-e797-4a9e-8b70-fb7de86a4025n%40googlegroups.com.

[Markus Kuppe]

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.

Markus

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

[Rivers Xiao]

Thanks! I tried to use profiler on my spec. But all the four kinds of result - invocations, cost, states and distinct states, are not time cost. They can certainly provide guidance for optimizing specs but I still need time statistics. Does anyone know where TLC invokes invariant checker in its code? So I can add some code for calculating elapsed time.

Rivers