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?