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

*From*: tal...@xxxxxxxxx*Date*: Mon, 19 Feb 2018 04:11:47 -0800 (PST)*References*: <e4aa2889-9cc4-4ce6-99ad-521f8291a998@googlegroups.com> <FD739EB0-2D0E-49DE-8FDB-E28AD51C01A7@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, On Monday, February 19, 2018 at 11:02:04 AM UTC, Stephan Merz wrote: > 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 > > > > On 19 Feb 2018, at 11:39, talex5 wrote: > > > > 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!

**Follow-Ups**:**Re: [tlaplus] TypeOK => TypeOK' with no other assumptions***From:*Stephan Merz

**References**:**TypeOK => TypeOK' with no other assumptions***From:*tal . . .

**Re: [tlaplus] TypeOK => TypeOK' with no other assumptions***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] TypeOK => TypeOK' with no other assumptions** - Next by Date:
**Re: [tlaplus] TypeOK => TypeOK' with no other assumptions** - Previous by thread:
**Re: [tlaplus] TypeOK => TypeOK' with no other assumptions** - Next by thread:
**Re: [tlaplus] TypeOK => TypeOK' with no other assumptions** - Index(es):