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

Well Google Groups doesn't seem to let me reply using my other email address so I'll switch over to this one.

Indeed you are correct that somehow the default SMT solver (cvc3 right?) is somehow not working well. Using BY Z3 works quite nicely (Z3 is already installed on my machine).

I am using a rather niche distribution of Linux (NixOS) to do this so it's possible the TLA+ Toolbox is packaged rather oddly in a way that interferes with TLAPS.

Is there any way to retrieve the error message that shows up when it says a backend failed? I had previously seen error messages saying it was unable to find a given process name (e.g. for Isabelle), but I've fixed those and those error messages were more informative than what I see now (which is just "failed").

In other words it seems like the Toolbox is able to find the executable cvc3 and ls4, since I'm not getting the same error message as when e.g. I try to run BY Yices (Executable "yices" not found in this PATH), but there's some other error happening.

在 2019年7月31日星期三 UTC-4上午3:06:58，Stephan Merz写道：

Hello,

I'm sorry for the problems you ran into. I copied and pasted the module as given in the Web page and ran the prover on it, and it worked for me. From what you write and from the axioms that you introduced, it looks like the Toolbox does not have access to all components of the prover.

1. In order for the Toolbox to find the library modules such as TLAPS, you have to add it to the library search path of the Toolbox, as indicated on the installation pages, e.g. https://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries/Windows.html.

2. You say that the PTL method (ls4 backend) doesn't work for you, and quite obviously the SMT backend doesn't work correctly either. (You can check that this is the case by trying to prove LEMMA TRUE BY SMT.) This seems to indicate that the Toolbox's search path doesn't include the locations where these binaries are installed (typically /usr/local/bin or the equivalent in Windows / cygwin). Depending on your operating system and initialization scripts, the Toolbox search path need not be the same that you get in a shell. You can check if things change if you launch the Toolbox from a shell window rather than from your GUI, and if so change the environment that applies to GUI applications, depending on your OS.

Hope this helps,
Stephan

On 31 Jul 2019, at 03:05, Changlin Li <ma...@xxxxxxxxxxxxxx> wrote:

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 tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ee434bd4-83cd-0d61-498c-2fc24a984cb6%40changlinli.com.