[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] "Final" action to check hyperproperties ?
I found it adequate to achieve the goals that I had.
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.
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:
> 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,
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/01f21669-b186-1d03-48a6-4abe802e3c1c%40lemmster.de.
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/CAHjs49yB0GKs0Qzc0OBi0b4c1E0JfA8OiAJrNYYWp1KAZ1tDJA%40mail.gmail.com.