Re: [tlaplus] "Final" action to check hyperproperties ?

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 31.05.20 13:52, dp.simplexum@xxxxxxxxx wrote:
> 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?

Hi,

TLC's most recent nightly build [1] has experimental support [2] for
your request (has to be refactored if this feature proves useful).  The
test case [3] shows how to configure TLC to make use of the feature.

Markus

[1] http://nightly.tlapl.us/
[2]
https://github.com/tlaplus/tlaplus/commit/ced9269895aa6b760fa7d7a35fa61b43eb2a9a0a
[3]
https://github.com/tlaplus/tlaplus/commit/ced9269895aa6b760fa7d7a35fa61b43eb2a9a0a#diff-5ef0f0f30e570c3acf482e001e9d87e9

-- 
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/80f5e51a-30dc-2546-fd6d-e8f704ee9863%40lemmster.de.