# Re: [tlaplus] Question on Inductive Invariants (page 44)?

Very clear!  TYVM.

On Sunday, February 16, 2014 4:36:52 PM UTC-8, Stephan Merz wrote:
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

On 16 Feb 2014, at 20:54, Brian Beckman <bc.b...@xxxxxxxxx> wrote:

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.