Re: [tlaplus] Expanding PrintT to TRUE in proofs?

Yes, you should comment out PrintT for proofs. Since PrintT is evaluated only for its side effect, expanding the definition would probably be harmless. But this is not the case for other operators defined in the TLC module. For example, TLC evaluates x \in Any to TRUE, for any x, but this could not be proved based on the definition of Any and even worse, adding the axiom "\A x : x \in Any" would make the logic of TLA+ inconsistent. (It is harmless for finite domains that TLC is based on.)

But you are raising an interesting question. We should probably reconsider which operators could and should be supported in proofs.

Regards,

Stephan

On 28 Apr 2020, at 00:34, JosEdu Solsona <josedusolsona@xxxxxxxxx> wrote:

Hello,

According to Unsupported TLA+ features:

TLAPS has no built-in knowledge of (most of) the operators defined in the TLC standard module, and it cannot use their definitions either.

So, when trying to prove an obligation containing PrintT operator (which is defined to be TRUE in TLC module), TLAPS cant prove it unless the same PrintT was already in assumptions.

Should i comment out PrintT statements from specs when doing proofs?, or there is a better way?

Thanks

--
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/e1933e9f-0b9a-4658-a3c3-9fb74b8fdcb0%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/C6794C96-C148-46CB-AC60-43AD200E93B4%40gmail.com.