Viewing the SMT Encoding from TLAPM

48 views
Skip to first unread message

Willy Schultz

unread,
Dec 20, 2020, 12:43:11 AM12/20/20
to tlaplus
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. 

Stephan Merz

unread,
Dec 20, 2020, 3:26:25 AM12/20/20
to tla...@googlegroups.com
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...@gmail.com> 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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9ce526bb-8566-4514-be39-c65bb26a58fdn%40googlegroups.com.

Willy Schultz

unread,
Dec 20, 2020, 10:45:41 AM12/20/20
to tlaplus
Excellent, thank you!

Willy Schultz

unread,
Oct 29, 2021, 12:13:06 AM10/29/21
to tlaplus
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

Stephan Merz

unread,
Oct 29, 2021, 2:52:27 AM10/29/21
to tla...@googlegroups.com
Hi Will,

I do not think that this is currently implemented. The `-N' option directs the PM not to run any backend verifiers but if I recall correctly it only produces proof obligations and checks them against the stored fingerprints, without generating encodings for the backend provers.

Stephan

Reply all
Reply to author
Forward
0 new messages