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

[dp.simplexum@xxxxxxxxx]

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 написал:

 

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/6843748f-2f9f-4f9d-9710-644a56342383%40googlegroups.com.