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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Thu, 30 Mar 2023 09:04:22 -0700 (PDT)*References*: <CABj=xUXEh034sKeX4Tdm21UWZ069Q89hAC9Fb2L9cMFf9oSOjw@mail.gmail.com> <29233EBE-DCFE-40F5-B65A-031F96782E27@gmail.com>

The --line flag has proven helpful. I might whip up a quick rust program that uses the tree-sitter grammar to find all lines with terminal proofs, runs tlapm FileName.tla --line N, measures the wall clock time for each, then prints out a sorted list of the longest-running proofs.

I'm having trouble proving a goal of type \E n \in Nat : P(n). It times out every other solver before Isabelle finally catches it. So I can reduce the time by specifying BY Isa, but I would be interested in knowing whether there's a way to break it down further to speed up checking:

https://github.com/ahelwer/formal-methods-experiments/blob/d6590da7cda489aa1a694ee8805d0dcfb7033ce8/tla/AddTwo.tla#L68

Andrew

On Tuesday, March 28, 2023 at 2:47:55 AM UTC-4 Stephan Merz wrote:

If you send me (off-list) your proofs, I can have a look, and that may help us optimize the encoding for the back-end provers. My hunch is that it's not just arithmetic but rather a combination, such as function application and arithmetic. Breaking down complex proofs into smaller steps will in general help speed up proof checking, as may introducing local definitions for abstracting complex subformulas. A trivial way to reduce wall-clock time is to explicitly indicate the relevant back-end if SMT (which is called first) doesn't succeed so that you don't have to wait for it to time out. But my advice would be not to exaggerate: this is a rabbit hole that's probably not worth exploring.Not sure I understand your last question, but perhaps you systematically invoke the prover on the entire module (from the command line). The Toolbox GUI really helps for launching the prover on individual obligations, but you can also run it from the command line usingtlapm --toolbox m nwhere m and n denote the interval of lines in the module that you'd like the prover to check.StephanOn 27 Mar 2023, at 19:24, Andrew Helwer <andrew...@xxxxxxxxx> wrote:I've written some arithmetic proofs where the prover does eventually validate the proof, albeit after a fairly long wait time. In general, can one reduce proof check time by breaking down a long-running proof into smaller substeps? Is there a way to check which steps are taking a long time so you know where to focus efforts?Thanks!Andrew--

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUXEh034sKeX4Tdm21UWZ069Q89hAC9Fb2L9cMFf9oSOjw%40mail.gmail.com.

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/a754d530-0927-4337-bff3-3e51e7ea5b55n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Optimizing proof check time***From:*Stephan Merz

**References**:**[tlaplus] Optimizing proof check time***From:*Andrew Helwer

**Re: [tlaplus] Optimizing proof check time***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Experience report: teaching TLA+ proofs to ChatGPT** - Next by Date:
**Re: [tlaplus] Optimizing proof check time** - Previous by thread:
**Re: [tlaplus] Optimizing proof check time** - Next by thread:
**Re: [tlaplus] Optimizing proof check time** - Index(es):