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

*From*: Brian Beckman <bc.be...@xxxxxxxxx>*Date*: Sun, 16 Feb 2014 15:54:10 -0800 (PST)

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

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

\* 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

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

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

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