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

# Question on Inductive Invariants (page 44)?

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

=============================================================================