Parse Error

[reza parvizi <parvizi....@xxxxxxxxx>]

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