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

Re: [tlaplus] Viewing the SMT Encoding from TLAPM



To follow up on this question, it is also possible to tell TLAPM to only produce these SMT files, without trying to prove anything? Basically, I am wondering if there's a way to only do the "pre-processing" step that produces the SMT encoding of the proof obligations, without invoking any solvers.

Will

On Sunday, December 20, 2020 at 10:45:41 AM UTC-5 Willy Schultz wrote:
Excellent, thank you!

On Sunday, December 20, 2020 at 3:26:25 AM UTC-5 Stephan Merz wrote:
Launch tlapm with the option `--debug tempfiles' (when you use the Toolbox, use C-G C-P to bring up the PM dialog and enter that option in the line at the bottom). You will probably also want to disable the use of fingerprints for the selected proof obligation. This will leave files with names such as tlapm_XXX.smt in the MMM.tlaps directory (where MMM is the name of the module).

Stephan 

On 20 Dec 2020, at 06:43, Willy Schultz <will...@xxxxxxxxx> wrote:

If my understanding is correct, TLAPM encodes TLA+ expressions into SMT-LIB format [1] and passes this to a backend solver e.g. Z3. I was wondering if it is possible to have the proof manager output the SMT-LIB formulas that it generates for inspection. I ask mostly out of curiosity i.e. I am interested about what this encoding looks like in practice. I have the proof manager set up on the command line. If there are any special debug flags I can pass to do this that would be great. 


--
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/9ce526bb-8566-4514-be39-c65bb26a58fdn%40googlegroups.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/78ca8885-0a21-450e-b23c-a31196e0ca6bn%40googlegroups.com.