[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

On 02.06.20 03:58, dp.simplexum@xxxxxxxxx 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 ?


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, ...)?


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/01f21669-b186-1d03-48a6-4abe802e3c1c%40lemmster.de.