TypeOK => TypeOK' with no other assumptions

[tal...@gmail.com]

Hi. I'm new to TLA+ and just tried my first proof. It appeared to work, and everything went green, but it seemed a bit too easy. After simplifying things, I ended up with this, which also goes all green:

------------------------------- MODULE False -------------------------------

EXTENDS TLAPS

VARIABLE x

TypeOK == x = {}

THEOREM T0 ==
ASSUME TypeOK
PROVE TypeOK'
BY PTL DEF TypeOK

=============================================================================

Oddly, if I replace TypeOK with its definition then it no longer accepts it. It does still accept it if I remove the "DEF TypeOK" bit completely though.

Maybe I shouldn't be using "BY PTL" here, but could someone explain what this means?

This is Version 1.5.6 of 29 January 2018 and includes:
- SANY Version 2.1 of 23 July 2017
- TLC Version 2.12 of 29 January 2018
- PlusCal Version 1.8 of 07 December 2015
- TLATeX Version 1.0 of 20 September 2017

Thanks!

[Stephan Merz]

Hello,

this is a known bug that has been fixed in the development version of TLAPS that is hopefully soon going to give rise to a new release. Indeed, you should not be using PTL for proving non-temporal (i.e., state- or action-level) proof obligations, but only for steps involving operators of temporal logic.

Sorry for the confusion,
Stephan

> --
> 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 post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[tal...@gmail.com]

Ah, OK. Is there a list of known issues somewhere?

I went to the tlaplug GitHub page (https://github.com/tlaplus). That pins the v2-tlapm repository, but it seems it isn't being used yet. Its README suggests https://tlaps.codeplex.com instead, but that has a "Shutdown Announcement". I also found https://github.com/tlaplus/v1-tlapm, but that has no issues (open or closed) and hasn't seen a release since Jan 2016.

(I was just curious to read the log for the fix commit)

Thanks,

[Stephan Merz]

The issue tracker for v2-tlapm is the one to use. Unfortunately, the transition to the new version of the PM has taken us far longer than we anticipated.

Stephan