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

*From*: Brian Beckman <bc.be...@xxxxxxxxx>*Date*: Sun, 16 Feb 2014 17:08:19 -0800 (PST)*References*: <8184289d-5408-4eac-b2e5-aee70f207eea@googlegroups.com> <D3C91322-29A0-44AF-A631-3AE352DBB563@gmail.com>

Very clear! TYVM.

On Sunday, February 16, 2014 4:36:52 PM UTC-8, Stephan Merz wrote:

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 * 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 aninductiveinvariant, 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 <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.

Visit this group at http://groups.google.com/group/tlaplus .

For more options, visit https://groups.google.com/groups/opt_out .

**References**:**Question on Inductive Invariants (page 44)?***From:*Brian Beckman

**Re: [tlaplus] Question on Inductive Invariants (page 44)?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Question on Inductive Invariants (page 44)?** - Next by Date:
**Re: position of PlusCal assert in Euclid from Hyperbook?** - Previous by thread:
**Re: [tlaplus] Question on Inductive Invariants (page 44)?** - Next by thread:
**A typo in hyperbook** - Index(es):