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

Re: [tlaplus] Viewing the SMT Encoding from TLAPM

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 <will62794@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+unsubscribe@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/A77BF16D-579C-484C-B45A-B97BBF630E4C%40gmail.com.