Parse Error

[reza parvizi]

Was expecting "----MODULE (beginning of module)"
Encountered "<EOF>" al line 68, column 24 in module Euclid

Residual stack trace follows:
Begin module starting at line 68, column 24.
Module definition starting at line 68, column 24.

-----------This is My Code----------

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) \cap 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)

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>a CASE x < y
<2>1 (y - x \in Number) /\ ~(y < x)
BY <1>a DEF Number
<2> QED
BY <1>a, <2>1, GCDProperty3
<1>b CASE y < x
<2>1 (x - y \in Number) /\ ~(x < y)
BY <1>b DEF Number
<2>2 GCD(y', x') = GCD(y, x)
BY <1>b, <2>1, GCDProperty3
<2> QED
BY <1>b, <2>1, <2>2, GCDProperty2
<1>2 QED
BY <1>1, <1>a, <1>b

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

[Martin]

Hello Reza,

Each TLA+ Specification must start with

---- MODULE Name ---

when your file is called name.tla (or Name.tla). It must also end with

====

If I insert these into your file, the proof of Correctness is missing
its QED step. If you add

<1> QED BY <1>1, <1>2, <1>3, PTL

TLAPS should be able to prove everything.

cheers, Martin

[Stephan Merz]

Hello,

difficult to understand what exactly you did since it doesn't look like you included your full TLA+ module, but the parser's error message is pretty explicit: a TLA+ module should start with a line like "---- MODULE Euclid ----". For example, see the code at the bottom of page https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/The_example.html.

It looks like you start with the TLA+ proof system without having experimented with other aspects of TLA+, and in particular the model checker. I'd recommend to get started with some elementary specifications, for example by reading the initial chapters of the hyperbook of reproducing the examples presented in Leslie's video lectures.

Regards,

Stephan

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.