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

*From*: Andreas Recke <Andreas.Recke@xxxxxxx>*Date*: Sat, 17 Sep 2022 12:09:10 -0700 (PDT)*References*: <37114691-5b42-42ce-a506-73ed0f5a4ea4n@googlegroups.com>

Some additional weird stuff: when decomposing the proof into

THEOREM SmallTest == ASSUME

NEW TEMPORAL System,

NEW VARIABLE j,

NEW CONSTANT d \in S,

NEW CONSTANT e \in S,

e = d-1,

System => j=d ~> j=d-1

PROVE

System => j=d ~> j=e

<1>1. SUFFICES ASSUME System

PROVE j=d ~> j=e

OBVIOUS

<1>2. QED BY <1>1

NEW TEMPORAL System,

NEW VARIABLE j,

NEW CONSTANT d \in S,

NEW CONSTANT e \in S,

e = d-1,

System => j=d ~> j=d-1

PROVE

System => j=d ~> j=e

<1>1. SUFFICES ASSUME System

PROVE j=d ~> j=e

OBVIOUS

<1>2. QED BY <1>1

TLAPS proves the SUFFICES construct <1>1 successfully!! But the outer proof failed. I can even prove that

j=d-1 <=> j=e OBVIOUS

but it does not help. Playing the the proof tactics, e.g. putting PTL into the BY clause or not did not change the situation.

Moreover, writing the proof like

THEOREM SmallTest == ASSUME

NEW TEMPORAL System,

NEW VARIABLE j,

NEW CONSTANT d \in S,

NEW CONSTANT e \in S,

e = d-1,

System => j=d ~> j=d-1,

System

PROVE

j=d ~> j=e

OBVIOUS

NEW TEMPORAL System,

NEW VARIABLE j,

NEW CONSTANT d \in S,

NEW CONSTANT e \in S,

e = d-1,

System => j=d ~> j=d-1,

System

PROVE

j=d ~> j=e

OBVIOUS

Fails, although this is the same as the SUFFICES proof above.

Seems like a bug.

Kind regards

Andreas

Andreas Recke schrieb am Donnerstag, 15. September 2022 um 21:37:36 UTC+2:

Hi,I am trying to set up a liveness proof.I was able to use the WF1 rule successfully, but going farther did not work.I have just a simple "count down from N to 0 then stop" spec.I know there is an example that uses NatInduction, but I want to specificallyuse the LATTICE rule because I would like to set up a framework for a morecomplicated spec.But now I am stuck at this:ASSUME d \in S /\ d > 0[]TypeOk /\ [][Next]_vars /\ WF_vars(Next) => (G(d) ~> G(d-1))But reformulating this to[]TypeOk /\ [][Next]_vars /\ WF_vars(Next) => (G(d) ~> \E e \in S: e < d /\ G(e))does not work.Moreover, another toy example with somehow similar also failedTHEOREM SmallTest == ASSUME

NEW TEMPORAL System,

NEW VARIABLE j,

NEW CONSTANT d \in S,

NEW CONSTANT e \in S,

e = d-1,

System => j=d ~> j=d-1

PROVE

System => j=d ~> j=e

BY

PTLAs if there is a bug. Or am I making a strange mistake?Anyway: does LATTICE work with this new branch?Thank you again in advance!Andreas

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/4a6834b7-b851-4b82-9a7b-4759e173a434n%40googlegroups.com.

**References**:**[tlaplus] Does LATTICE rule work with the branch updated_enabled_cdot?***From:*Andreas Recke

- Prev by Date:
**Re: [tlaplus] Re: Where is the code for the state space traversal algorithm in TLC?** - Next by Date:
**[tlaplus] TLA+ / PlusCalc Cookbook ?** - Previous by thread:
**[tlaplus] Does LATTICE rule work with the branch updated_enabled_cdot?** - Next by thread:
**Re: [tlaplus] Does LATTICE rule work with the branch updated_enabled_cdot?** - Index(es):