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

# [tlaplus] Trying to follow along with INRIA's TLAPS tutorial

• From: Changlin Li <mail@xxxxxxxxxxxxxx>
• Date: Tue, 30 Jul 2019 21:05:41 -0400
• User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.7.2

I'm looking at https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Hierarchical_proofs.html and the proofs there don't seem to be working for me.


The non-temporal proofs seem to require a lot more hand-holding (i.e. introducing a lot more axioms) than what's being displayed on the page and I can't seem to prove the temporal proof with ls4 backend at all.

Is there something I'm missing here?


On a separate note the TLAPS module doesn't seem to be found by my TLA+ Toolbox installation and I had to inline it as a module in the same spec as Euclid.


I've included the module I ended up writing here (with the large number of axioms I had to introduce). The Correctness theorem still isn't accepted by tlapm.


------------------------------- MODULE Euclid -------------------------------

EXTENDS Integers, TLAPS

p | q == \E d \in 1..q : q = p * d

Divisors(q) == {d \in 1..q : d | q}

Maximum(S) == CHOOSE x \in S : \A y \in S : x >= y

GCD(p, q) == Maximum(Divisors(p) \intersect Divisors(q))

Number == Nat \ {0}

CONSTANTS M, N

VARIABLES x, y

Init == (x = M) /\ (y = N)

Next ==
\/ /\ x < y
/\ y' = y - x
/\ x' = x
\/ /\ y < x
/\ x ' = x - y
/\ y' = y

Spec == Init /\ [][Next]_<<x, y>>

ResultCorrect == (x = y) => x = GCD(M, N)

InductiveInvariant ==
/\ x \in Number
/\ y \in Number
/\ GCD(x, y) = GCD(M, N)

ASSUME NumberAssumption == M \in Number /\ N \in Number

THEOREM InitProperty == Init => InductiveInvariant
BY NumberAssumption DEF Init, InductiveInvariant

AXIOM GCDProperty1 == \A p \in Number : GCD(p, p) = p
AXIOM GCDProperty2 == \A p, q \in Number : GCD(p, q) = GCD(q, p)

AXIOM GCDProperty3 == \A p, q \in Number : (p < q) => GCD(p, q) = GCD(p, q-p)
AXIOM LessThanIsAntiSymmetric == \A p, q \in Nat : (p < q) => ~(q < p)
AXIOM LessThanImpliesInequality == \A p, q \in Nat : (p < q) => p /= q

AXIOM NatsClosedUnderLessThanSubtraction == \A p, q \in Nat : (p < q) => q - p \in Nat
AXIOM NatIsSuperSetOfNumber == \A p \in Number : p \in Nat
AXIOM NatIsNumberIfNotZero == \A p \in Nat : p /= 0 => p \in Number
AXIOM LessThanRespectsZero == \A p, q \in Nat : q < p => p - q > 0

THEOREM NextProperty == InductiveInvariant /\ Next => InductiveInvariant'
<1> SUFFICES ASSUME InductiveInvariant, Next
PROVE InductiveInvariant'
OBVIOUS
<1> USE DEF InductiveInvariant, Next
<1>1 (x < y) \/ (y < x)
OBVIOUS
<1>2 y \in Nat
BY NatIsSuperSetOfNumber
<1>3 x \in Nat
BY NatIsSuperSetOfNumber
<1>4 CASE x < y
<2>1 ~(y < x)
BY <1>2, <1>3, <1>4, LessThanIsAntiSymmetric
<2>2 (y - x \in Nat)
BY <1>4, NatsClosedUnderLessThanSubtraction, NatIsSuperSetOfNumber
<2>3 (y - x > 0)
BY <1>2, <1>3, <1>4, LessThanRespectsZero
<2>4 (y - x /= 0)
BY <2>3, LessThanImpliesInequality
<2>5 (y - x \in Number)
BY <2>2, NatIsNumberIfNotZero, <2>4
<2>6 (y - x \in Number) /\ ~(y < x)
BY <2>1, <2>5
<2> QED BY <1>4, <2>6, GCDProperty3
<1>5 CASE y < x
<2>1 ~(x < y)
BY <1>2, <1>3, <1>5, LessThanIsAntiSymmetric
<2>2 (x - y \in Nat)
BY <1>5, NatsClosedUnderLessThanSubtraction, NatIsSuperSetOfNumber
<2>3 (x - y > 0)
BY <1>2, <1>3, <1>5, LessThanRespectsZero
<2>4 (x - y /= 0)
BY <2>3, LessThanImpliesInequality
<2>5 (x - y \in Number)
BY <2>2, NatIsNumberIfNotZero, <2>4
<2>6 (x - y \in Number) /\ ~(x < y)
BY <2>1, <2>5
<2>7 GCD(y', x') = GCD(y, x)
BY <1>5, <2>1, GCDProperty3
<2> QED BY <1>5, <2>6, <2>7, GCDProperty2
<1>6 QED BY <1>1, <1>4, <1>5

THEOREM Correctness == Spec => []ResultCorrect

<1>1 InductiveInvariant /\ UNCHANGED <<x,y>> => InductiveInvariant' BY DEF InductiveInvariant <1>2 Spec => []InductiveInvariant BY PTL, InitProperty, NextProperty, <1>1 DEF Spec <1>3 InductiveInvariant => ResultCorrect BY GCDProperty1 DEF InductiveInvariant, ResultCorrect
<1> QED BY PTL, <1>2, <1>3

=============================================================================
\* Modification History
\* Last modified Tue Jul 30 21:04:57 EDT 2019 by changlin
\* Created Mon Jul 29 15:58:58 EDT 2019 by changlin

--
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/ee434bd4-83cd-0d61-498c-2fc24a984cb6%40changlinli.com.