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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 24 Oct 2019 18:18:20 +0200*References*: <730a0c57-4a45-4205-817b-fa06a5852f0b@googlegroups.com> <247BE5EB-9628-4E7A-958A-48DEB3004CEE@gmail.com> <CAHeFUE8DXzp0yb53G85bHBkVa1EvkogePYhC=npTdRa6Grz5TA@mail.gmail.com>

So what you are saying is that when you find out that some assumption that you asserted was actually wrong, you'd like to know where it was used in the proof. We advise users to thoroughly model check their specifications before embarking on any proof. In our experience, using the model checker is a great way for validating a spec. (It could certainly detect the fallacy in the example that you give.) Doing so helps you avoid the problem in the first place. Second, the proof system has an approximation for the functionality that you request: when you modify the assertion of some fact (or change a definition), you can relaunch the prover. Since all previous results of proof attempts are cached, steps that do not syntactically depend on the definition or fact will not be rechecked, and you quickly see which steps fail. Of course, if your assumption appears in a global USE, all steps will need to be reproved. 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/85FC19AF-DD4C-479F-B36B-1DF1F3D53F47%40gmail.com. |

**Follow-Ups**:

**References**:**[tlaplus] [TLAPS] Is there a way to see the steps taken by the automated prover to prove a goal ?***From:*Saswata Paul

**Re: [tlaplus] [TLAPS] Is there a way to see the steps taken by the automated prover to prove a goal ?***From:*Stephan Merz

**Re: [tlaplus] [TLAPS] Is there a way to see the steps taken by the automated prover to prove a goal ?***From:*Saswata Paul

- Prev by Date:
**Re: [tlaplus] [TLAPS] Is there a way to see the steps taken by the automated prover to prove a goal ?** - Next by Date:
- Previous by thread:
- Next by thread:
- Index(es):