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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Mon, 24 Feb 2014 13:36:45 -0800 (PST)*References*: <094f0fd5-83b7-4670-acd2-e8c820261355@googlegroups.com>

Hi Brian,

I don't understand what you are doing in this or your previous post.

You write

This passes checks with ISpec as temporal invariant

I don't know what you mean by a temporal invariant. I presume that

"passes checks" means that you have successfully checked something

with the model checker, but I don't know what. In other words, I

don't know what model you have checked. To describe the model, you

need to say what you entered in the various Toolbox fields that

specify the model--that is, "What is the behavior spec?", "What to

check?", and any other things that you told the model checker to use

(I don't think there should be any).

You define

ISpec == Inv /\ [][Next]_<<x, pc>>

whose form suggests that you are taking Inv to be the initial predicate.

But your definition

Inv == /\ Init

/\ TypeOK

/\ MutualExclusion

/\ Fairness

/\ Coordination

/\ DeadlockFreedom

is rather bizarre. First of all, I presume that Init is defined by

the PlusCal translation. In that case, I believe that Init implies

TypeOK /\ MutualExclusion /\ Coordination. (You should make sure you

understand why it does--or find a counterexample if it doesn't.)

Therefore, Inv is equivalent to (since P => Q is equivalent to P /\ Q = P)

/\ Init

/\ Fairness

/\ DeadlockFreedom

which is the conjunction of a state predicate and two temporal

formulas. Moreover, if the algorithm is deadlock free (I haven't

looked closely to see if it is), then the formula

S == Init /\ [][Next]_<<x, pc>> /\ Fairness

should imply DeadlockFreedom, so ISpec should be equivalent to S.

I believe you are confused, but I don't know what the source of your

confusion is. I suspect that you are writing formulas that don't mean

what you want them to mean. You should make sure that you understand

the meaning of each formula you write---that is, what it asserts about

a behavior. You would then see that Init, TypeOK, MutualExclusion,

and Coordination make assertions about the first state of the

behavior, while Fairness and DeadlockFreedom make assertions about the

entire behavior.

Leslie

**Follow-Ups**:**Re: Bikeshedding fun with problem 7.7***From:*Brian Beckman

**References**:**Bikeshedding fun with problem 7.7***From:*Brian Beckman

- Prev by Date:
**Re: importing module into model** - Next by Date:
**Re: Bikeshedding fun with problem 7.7** - Previous by thread:
**Bikeshedding fun with problem 7.7** - Next by thread:
**Re: Bikeshedding fun with problem 7.7** - Index(es):