"Final" action to check hyperproperties ?

[dp.sim...@gmail.com]

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?

[Markus Kuppe]

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

[dp.sim...@gmail.com]

Cool! I've tested it, and it works.

I've added automatic test for 'transactions ever confirmed in some execution path' hyperproperty to the 'succint atomic swap' spec: https://github.com/dgpv/SASwap_TLAplus_spec/blob/38ad074db8a19aa6bf06cbe4a1420fd828a49232/HyperProperties.tla#L51

In the diff you linked to, I see some calls to TLCGet with string arguments. Do I understand correctly that the string arguments to TLCGet/TLCSet reserved only for internal values like number of states, and for ordinary use, integer slot numbers should be used ?

вторник, 2 июня 2020 г., 5:50:31 UTC+5 пользователь Markus Alexander Kuppe написал:

[Markus Kuppe]

On 02.06.20 03:58, dp.sim...@gmail.com wrote:
>
> In the diff you linked to, I see some calls to TLCGet with string
> arguments. Do I understand correctly that the string arguments to
> TLCGet/TLCSet reserved only for internal values like number of states,
> and for ordinary use, integer slot numbers should be used ?

Yes, TLCSet(i,v) only accepts (positive) integers for the i parameter
(see 2.2.2 of [1]).

Markus

[1] https://lamport.azurewebsites.net/tla/current-tools.pdf

[Markus Kuppe]

On 02.06.20 03:58, dp.sim...@gmail.com wrote:

> Cool! I've tested it, and it works.
>
> I've added automatic test for 'transactions ever confirmed in some
> execution path' hyperproperty to the 'succint atomic swap' spec:
> https://github.com/dgpv/SASwap_TLAplus_spec/blob/38ad074db8a19aa6bf06cbe4a1420fd828a49232/HyperProperties.tla#L51
>
> In the diff you linked to, I see some calls to TLCGet with string
> arguments. Do I understand correctly that the string arguments to
> TLCGet/TLCSet reserved only for internal values like number of states,
> and for ordinary use, integer slot numbers should be used ?

Hi,

what's your experience with the feature after a couple of weeks? Do you
have the bandwidth to shepherd this feature to completion (finish impl,
documentation, ...)?

Markus

[Dmitry Petukhov]

I found it adequate to achieve the goals that I had.

I have used this feature in https://github.com/dgpv/SASwap_TLAplus_spec/blob/master/HyperProperties.tla and https://github.com/dgpv/bip32_template_parse_tplaplus_spec/blob/master/HyperProperties.tla

I can say that usage is pretty straightforward and I did not encounter something to complain about. It just worked.

I cannot say that I have enough bandwidth to help on this work, as the lateness of this answer probably shows. If there is a concrete issue where you think that my input could be valuable, please tag me on github @dgpv.

вт, 23 июн. 2020 г. в 03:20, Markus Kuppe <tlaplus-go...@lemmster.de>:

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/o1dRrwyVlrw/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/01f21669-b186-1d03-48a6-4abe802e3c1c%40lemmster.de.