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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 28 Oct 2021 08:36:53 +0200*References*: <61176d59-aab7-462f-ab73-d711b470fba3n@googlegroups.com> <A8D783A1-DE61-4349-874E-D1C16D893228@gmail.com> <CAEJ64taoPJKxucG5QDN5jrUKxhuMXq8JFVh0QowbHc61xeeqEA@mail.gmail.com> <16f4ac23-7f35-004c-920a-a0e997b69fec@lemmster.de> <121ff5a5-5dcc-479a-8f8c-ecbd9d1e1606n@googlegroups.com> <E3422E8F-6EA5-4307-A2C8-0658F349AB5B@gmail.com> <a9fc145a-ce80-4e46-9ff3-efe4f7a5c9cfn@googlegroups.com> <CABW84KyUdUDSHjCbL0AKuZ83JiG0z4FiMeki-wqpUQ5d6UicsA@mail.gmail.com>

It is completely within the spirit of TLA+ to first write a high-level spec and then check that an algorithm refines that spec. For example, you may have a look at the module SyncTerminationDetected at [1] that provides a high-level spec of termination detection for nodes on a ring with synchronous communication, and for which TLC can check that Dijkstra's algorithm from EWD 840 is a refinement. Stephan
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/B0ED6E04-E15F-470C-B3DB-6C3053FEBD3D%40gmail.com. |

**Follow-Ups**:

**References**:**[tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties***From:*Jones Martins

**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties***From:*Stephan Merz

**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties***From:*Travis Allison

**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties***From:*Markus Kuppe

**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties***From:*Jones Martins

**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties***From:*Stephan Merz

**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties***From:*Andrew Helwer

**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties***From:*Jones Martins

- Prev by Date:
**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties** - Next by Date:
**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties** - Previous by thread:
**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties** - Next by thread:
**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties** - Index(es):