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

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

 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 * dDivisors(q) == {d \in 1..q : d | q}Maximum(S) == CHOOSE x \in S : \A y \in S : x \geq yGCD(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 specificationSpecI2 == Inv /\ [][Next]_varsthat 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 thatAttempted to enumerate S \ T when S:Natis 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 .. NAfter 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 toIn 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 asTypeOK == /\ 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 redefineSpecI2 == InductiveInv /\ [][Next]_varsand 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,StephanOn 16 Feb 2014, at 20:54, Brian Beckman 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 => InvI2 == Inv /\ Next => Inv'I3 == Inv => PCIn 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 ExtraSimpleEuclidWhile 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 beI2 == ~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, GCDCONSTANTS M, NASSUME {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 TRANSLATIONVARIABLES x, y, pcvars == << 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 => InvI2 == (~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...@xxxxxxxxxxxxxxxx. 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.