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

[tlaplus] The Euclid algorithm and TLAPS 1.4.5


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:

    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,

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.