Hello,
there is a bit of misunderstanding here about how TLC works.
———
By the way, since I don't know what module GCD contains, I'm using the following definitions:
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 \geq y
GCD(p,q) == Maximum(Divisors(p) \cap Divisors(q))
If you want to check if Inv is an invariant — i.e., if it holds in all reachable states — you verify Inv as an "invariant" over specification Spec. You should see that this works.
If you'd rather want to check if Inv is an inductive invariant, you can verify if Inv is an invariant of specification
SpecI2 == Inv /\ [][Next]_vars
that is, take Inv as your initial condition rather than Init (the fairness condition doesn't matter for invariants so I didn't bother specifying it). Change Spec to SpecI2 in the sub-pane "What is the behavior spec" and check Inv as an invariant over this modified behavior specification.
Now, you'll see that TLC complains that
Attempted to enumerate S \ T when S:
Nat
is not enumerable.
and this comes from the formula TypeOK, which restricts x and y to be in Nat \ {0}, which is an infinite set, and TLC cannot evaluate such expressions.
In order to avoid this problem, I suggest redefining TypeOK as follows:
TypeOK == /\ x \in 1 .. M
/\ y \in 1 .. N
After all, x and y start from M and N, respectively, and can only decrease. (You could alternatively override the meaning of Nat but that's advanced magic and IMHO rather confusing.)
We are now back to
In evaluation, the identifier pc is either undefined or not an operator.
line 69, col 12 to line 69, col 13 of module ExtraSimpleEuclid
(where line 69 is the last conjunct of Inv). I think now you understand the problem: TLC cannot check Inv because pc is not constrained by the initial condition Inv: it could take any value. So we'll redefine TypeOK as
TypeOK == /\ x \in 1 .. M
/\ y \in 1 .. N
/\ pc \in {"loop", "antanaresis", "Done"}
… and now TLC runs for a longer while and then reports a counter-example showing that the invariant is violated: starting from x=y=3 and pc="antanaresis", we reach a state where x=0.
Ah, so that's why Inv is not inductive! We must rule out this case and use InductiveInv. So let's redefine
SpecI2 == InductiveInv /\ [][Next]_vars
and verify InductiveInv over this specification. Eureka!
Your conditions I1, I2, and I3 would be the proof obligations in a TLA+ proof that you could check with TLAPS. With the model checker, you (usually) verify properties over executions of system specifications.
Hope this helps.
Best regards,
Stephan
Working through the Inductive invariants for Euclid, I've encoded them as follows:
\* PC means `PartialCorrectness,' but it's a lot easier to write and read.
PC == (pc = "Done") => (x = y) /\ (x = GCD(M, N))
TypeOK == /\ x \in Nat \ {0}
/\ y \in Nat \ {0}
Inv == /\ TypeOK
/\ GCD(x, y) = GCD(M, N)
/\ (pc = "Done") => (x = y)
InductiveInv == /\ Inv
/\ (pc = "antanaresis") => (x /= y)
I1 == Init => Inv
I2 == Inv /\ Next => Inv'
I3 == Inv => PC
In the model checker, I can check them all except I2, which generates the following error (I labeled my while loop "loop"):
In evaluation, the identifier pc is either undefined or not an operator.
line 32, col 23 to line 32, col 24 of module ExtraSimpleEuclid
While working on the initial state:
/\ x = 30
/\ y = 18
/\ pc = "loop"
Which I interpreted as the checker trying to evaluate Inv /\ Next in when state Init is TRUE and getting undefined pc.
Fair enough, I modified I2 to be
I2 == ~Init /\ Inv /\ Next => Inv'
and I check in the model to ONLY verify the ivariant I2 (PC, Inv, InductiveInv, I1 and I3) are unchecked lest I get other more mysterious errors).
I get the error that "Invariant PC failed." But I didn't ask it to check PC? And if I uncheck I2 and check PC, it succeeds. I'm stumped, and I'd be grateful for advice.
My entire model is as follows:
------------------------- MODULE ExtraSimpleEuclid -------------------------
EXTENDS Integers, GCD
CONSTANTS M, N
ASSUME {M, N} \subseteq Nat \ {0} \* `subset' doesn't seem to work
(***************************************************************************
--fair algorithm Euclid
{ variables x = M, y = N;
{ loop: while (x /= y)
\* The Greek word for the following process of repeated subtraction
\* is `antanaresis.'
{ antanaresis: if (x < y) { y := y - x; }
else { x := x - y; }
}
} }
***************************************************************************)
\* BEGIN TRANSLATION
VARIABLES x, y, pc
vars == << x, y, pc >>
Init == (* Global variables *)
/\ x = M
/\ y = N
/\ pc = "loop"
loop == /\ pc = "loop"
/\ IF x /= y
THEN /\ pc' = "antanaresis"
ELSE /\ pc' = "Done"
/\ UNCHANGED << x, y >>
antanaresis == /\ pc = "antanaresis"
/\ IF x < y
THEN /\ y' = y - x
/\ x' = x
ELSE /\ x' = x - y
/\ y' = y
/\ pc' = "loop"
Next == loop \/ antanaresis
\/ (* Disjunct to prevent deadlock on termination *)
(pc = "Done" /\ UNCHANGED vars)
Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(Next)
Termination == <>(pc = "Done")
\* END TRANSLATION
\* PC means `PartialCorrectness,' but it's a lot easier to write and read.
PC == (pc = "Done") => (x = y) /\ (x = GCD(M, N))
TypeOK == /\ x \in Nat \ {0}
/\ y \in Nat \ {0}
Inv == /\ TypeOK
/\ GCD(x, y) = GCD(M, N)
/\ (pc = "Done") => (x = y)
InductiveInv == /\ Inv
/\ (pc = "antanaresis") => (x /= y)
I1 == Init => Inv
I2 == (~Init) /\ Inv /\ Next => Inv'
I3 == Inv => PC
=============================================================================
--
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...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.