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

*From*: sidorykp@xxxxxxxxx*Date*: Wed, 6 May 2020 13:04:43 -0700 (PDT)

Hi,

I have just upgraded TLAPS from v1.4.3 to v1.4.5. I use TLA+ Toolbox v1.7.0 on Ubuntu.

And unfortunately TLAPS is not able to prove the following part of the Euclid algorithm:

THEOREM GCDProperty3 == ASSUME

NEW p \in Number,

NEW q \in Number,

q > p

PROVE GCD(p, q) = GCD(p, q - p)

<1> USE DEF Divisors, |

<1>1 \A d \in Number: d | p /\ d | q => d | (q - p)

BY DEF Number

<1>2 \A d \in Number: d | p /\ d | (q - p) => d | q

BY DEF Number

<1> QED

BY <1>1, <1>2 DEF GCD

NEW p \in Number,

NEW q \in Number,

q > p

PROVE GCD(p, q) = GCD(p, q - p)

<1> USE DEF Divisors, |

<1>1 \A d \in Number: d | p /\ d | q => d | (q - p)

BY DEF Number

<1>2 \A d \in Number: d | p /\ d | (q - p) => d | q

BY DEF Number

<1> QED

BY <1>1, <1>2 DEF GCD

More precisely, it cannot prove <1>1 and <1>2. I can see timeout after 30 seconds or something.

Downgrading to v1.4.3 solves the issue.

Has anybody encountered a similar issue? Or maybe somebody managed to prove the Euclid algorithm with TLAPS v1.4.5?

Best Regards,

Pawel

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/18bc9f5b-a91b-4553-9e83-7affdf1994c1%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: The Euclid algorithm and TLAPS 1.4.5***From:*sidorykp

- Prev by Date:
**[tlaplus] Re: Supporting Action Composition in TLC** - Next by Date:
**[tlaplus] Re: The Euclid algorithm and TLAPS 1.4.5** - Previous by thread:
**[tlaplus] Re: Supporting Action Composition in TLC** - Next by thread:
**[tlaplus] Re: The Euclid algorithm and TLAPS 1.4.5** - Index(es):