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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 15 Apr 2020 18:18:57 +0200*References*: <a70545cd-37a0-430a-aad5-bc303a0f33e0@googlegroups.com> <3F9142EF-641E-4A04-8650-DFE1CAC46592@gmail.com> <01d5937b-63df-4723-96c7-14153a75b529@googlegroups.com>

The reason the formula only talks about the initial state is that it does not contain any temporal operator. If you want to prove that it holds for all states, you should write THEOREM Spec => [](diag = tdiag) This is an invariant, and from a quick glance at the algorithm it appears that it is inductive. You can prove it as follows: <1>1. Init => (diag = tdiag) <1>2. (diag = tdiag) /\ [Next]_vars => (diag = tdiag)' <1>. QED BY <1>1, <1>2, PTL DEF Spec (You'll have to write proofs for the steps <1>1 and <1>2 in order to complete the proof.) If this doesn't make sense to you, please have a look at the TLAPS tutorial [1]. Stephan [1] http://proofs.tlapl.us/doc/web/content/Documentation/Tutorial/The_example.html
--
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/730D2F51-FD92-4F40-BB2E-57E5CE211791%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Proving a Matrix Transpose***From:*c . burge . glasgow

**References**:**[tlaplus] Proving a Matrix Transpose***From:*christina . a . burge

**Re: [tlaplus] Proving a Matrix Transpose***From:*Stephan Merz

**Re: [tlaplus] Proving a Matrix Transpose***From:*christina . a . burge

- Prev by Date:
**Re: [tlaplus] Proving a Matrix Transpose** - Next by Date:
**Re: [tlaplus] How do you list possible next steps?** - Previous by thread:
**Re: [tlaplus] Proving a Matrix Transpose** - Next by thread:
**Re: [tlaplus] Proving a Matrix Transpose** - Index(es):