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

# Re: [tlaplus] Parse Error

 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,StephanOn 19 Jul 2017, at 08:57, reza parvizi wrote:Was expecting "----MODULE (beginning of module)"Encountered "" al line 68, column 24 in module EuclidResidual 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, TLAPSp | q == \E d \in 1..q : q = p * dDivisors(q) == {d \in 1..q : d | q}Maximum(S) == CHOOSE x \in S : \A y \in S : x >= yGCD(p,q) == Maximum(Divisors(p) \cap Divisors(q))Number == Nat \ {0}CONSTANTS M, NVARIABLES x, yInit == (x = M) /\ (y = N)Next == \/ /\ x < y           /\ y' = y - x           /\ x' = x        \/ /\ y < x           /\ x' = x-y           /\ y' = ySpec == Init /\ [][Next]_<>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 NumberTHEOREM InitProperty == Init => InductiveInvariant  BY NumberAssumption DEF Init, InductiveInvariantAXIOM GCDProperty1 == \A p \in Number : GCD(p, p) = pAXIOM 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>bTHEOREM Correctness == Spec => []ResultCorrect  <1>1 InductiveInvariant /\ UNCHANGED <> => 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-- 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...@xxxxxxxxxxxxxxxx.To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.Visit this group at https://groups.google.com/group/tlaplus.For more options, visit https://groups.google.com/d/optout.