[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] "Final" action to check hyperproperties ?
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?
TLC's most recent nightly build  has experimental support  for
your request (has to be refactored if this feature proves useful). The
test case  shows how to configure TLC to make use of the feature.
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.