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

[tlaplus] "Final" action to check hyperproperties ?

I can collect stats for hyperproperties, like max/min/avg value of some variable throughout all states with TLCGet/TLCSet.

I can show these hyperproperties by printing the collected stats as they are updated.

But I did not find a way to check these collected stats for expected range at the end of TLC run with TLA+ _expression_, as opposed to manual checking or using some external script to parse the output (both options are inconvenient and error-prone)

Is there a way to do these checks robustly and conveniently, that I missed ?

If there is not, what is the possibility for a feature to be added, that would be something like a special 'Final' action that would be evaluated just after TLC finished checking?

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/7433ba81-01a7-4872-bbf4-a7c99ec45b23%40googlegroups.com.