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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Thu, 17 Jun 2021 05:35:17 -0700 (PDT)*Ironport-hdrordr*: A9a23:9jWfJKiRFOOZ8Hwc7G7kagOb+nBQXgMji2hC6mlwRA09TyX4rayTdZEgviMc5wx/ZJheo7690cW7IE8036QU3WBpB8bAYOC+ghrLEGgA1/qG/9SfIVybygcH79YGT0EWMrSZMbEdt7ed3ODSKbsdKbe8mpxBcY3lvg5QpHlRGtldB4wTMHfhLqX9LzM2f6bQrfGnl7d6mwY=*References*: <ad1c98a5-728c-4d3c-a077-ea7040f34e9dn@googlegroups.com>

Yes, see my prior thread here: https://groups.google.com/g/tlaplus/c/JZaBcIhA1UY/m/olfrUJ5xCQAJ

And Leslie's paper *Real Time is Really Simple, *which you found.

You are correct it is implemented with the VIEW _expression_, assuming your counter values don't "contaminate" any of the other variable's values.

Andrew

On Wednesday, June 16, 2021 at 8:44:09 PM UTC-4 will...@xxxxxxxxx wrote:

Is anyone familiar with any prior work on exploiting types of "translational" symmetry during model checking? For protocols that maintain, say, a counter, it often seems that the safety of the protocol is, to some extent, "translation invariant". That is, if the set of states reachable from a state <<counter, v1, ..., vn>> is safe, then the set of states reachable from <<counter + T, v1, ..., vn>> for T > 0 should also be safe, assuming that the safety property and algorithm behavior doesn't depend on the specific (i.e. concrete) value of the counter. The closest mention of it that I've encountered is in Section 3.5 of [1], where it discusses "Symmetry Under Time Translation" in the context of model checking real time specifications.I imagine you may be able to implement something like this using a clever VIEW _expression_ in TLC.

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/75f4d42c-c0c5-42db-97bf-e18a87253451n%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: Translational Symmetry for Model Checking***From:*Willy Schultz

**References**:**[tlaplus] Translational Symmetry for Model Checking***From:*Willy Schultz

- Prev by Date:
**[tlaplus] Translational Symmetry for Model Checking** - Next by Date:
**[tlaplus] Re: Translational Symmetry for Model Checking** - Previous by thread:
**[tlaplus] Translational Symmetry for Model Checking** - Next by thread:
**[tlaplus] Re: Translational Symmetry for Model Checking** - Index(es):