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

*From*: Brian Beckman <bc.be...@xxxxxxxxx>*Date*: Tue, 25 Feb 2014 10:46:06 -0800 (PST)*References*: <094f0fd5-83b7-4670-acd2-e8c820261355@googlegroups.com> <8094bd59-a130-46d1-a2f3-b9f803ee8300@googlegroups.com>

I appreciate your for taking the time to read so carefully; this is very

helpful to me. Responses inline below.

On Monday, February 24, 2014 1:36:45 PM UTC-8, Leslie Lamport wrote:

Hi Brian,

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

I am trying to make a version of the spec that is more subjectively

understandable to me but equivalent to the one in the hyperbook. This is

admittedly a subjective, stylistic activity.

You write

This passes checks with ISpec as temporal invariant

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

I should have said "Temporal formula." My "Model Overview" has "ISpec"

typed in to the "Temporal formula" box under "What is the behavior

spec?"

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).

Under "What to check?" I chose "Deadlock," not the same as my

user-defined "DeadlockFreedom."

If I had an "Initial predicate and next-state relation" chosen under

"what is the behavior spec?" then I think "Deadlock" under "What to

check?" means that the next-state relation is satisfied by every step in

every behavior. However, I have "Temporal formula" chosen instead of

"Initial predicate and next-state relation," so I don't know what

"Deadlock" under "What to check?" does under this circumstance.

You define

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

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

But your definitionInv == /\ Init

/\ TypeOK

/\ MutualExclusion

/\ Fairness

/\ Coordination

/\ DeadlockFreedomis 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

The "Init" generated by the PlusCal translation is the following:

ProcSet == ({0,1})

Init == (* Global variables *)

/\ x = [i \in {0,1} |-> FALSE]

/\ pc = [self \in ProcSet |-> "ncs"]

which does imply TypeOK, MutualExclusion, and Coordination (I checked).

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 formulaS == Init /\ [][Next]_<<x, pc>> /\ Fairness

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

Abandoning Inv, I changed ISpec to equal Init /\ [][Next]_<<x, pc>> /\

Fairness and checked it in the model checker by choosing "Temporal

Formula" under "What is the behavior spec?" and typing in "ISpec." This

passes. With this chosen, I cannot choose "Initial predicate and

next-state relation."

Here is the MC.tla file

---- MODULE MC ----

EXTENDS OneBitTwoProcesses, TLC

\* SPECIFICATION definition @modelBehaviorSpec:0

spec_139335347329970000 ==

ISpec

----

\* PROPERTY definition @modelCorrectnessProperties:0

prop_139335347330971000 ==

A!ISpec

----

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

\* Modification History

\* Created Tue Feb 25 10:37:53 PST 2014 by bbeckman

I then tried an experiment that heightens my confusion. I would have

expected that the above is equivalent to putting "Init" and "Next" into

the Init and Next slots of "Initial predicate and next-state relation"

of "What is the behavior spec?" and ALSO putting "Fairness" in the

properties box of "What to check?" However, doing so generates an error,

namely that

<Initial predicate> State (num = 1)

x (0 :> FALSE @@ 1 :> FALSE)

pc (0 :> "ncs" @@ 1 :> "ncs")

<Stuttering> State (num = 2)

Fairness asserts that \A i \in {0,1} : WF_vars(Proc(i)), where

Proc(i) == ncs(i) \/ e1(i) \/ e2(i) \/ cs(i) \/ e3(i) \/ e4(i) \/ f(i).

I think WF_vars(P) means that there is no suffix of any behavior in

which P is enabled for every step but there is no P step. For Proc(i) to

be enabled means that there exists a possible assignment of values to

variables that makes Proc(i) true. But I don't see how a stuttering

state can be reached since "ncs(i)" will push pc to e1:

ncs(self) == /\ pc[self] = "ncs"

/\ TRUE

/\ pc' = [pc EXCEPT ![self] = "e1"]

/\ x' = x

At the bottom of this post is my entire spec as it stands now.

Here is the failing MC.tla file

---- MODULE MC ----

EXTENDS OneBitTwoProcesses, TLC

\* INIT definition @modelBehaviorInit:0

init_139335367677776000 ==

Init

----

\* NEXT definition @modelBehaviorNext:0

next_139335367678777000 ==

Next

----

\* PROPERTY definition @modelCorrectnessProperties:0

prop_139335367679878000 ==

A!ISpec

----

\* PROPERTY definition @modelCorrectnessProperties:1

prop_139335367680979000 ==

Fairness

----

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

\* Modification History

\* Created Tue Feb 25 10:41:16 PST 2014 by bbeckman

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

I am definitely confused between assertions about the first state of a

behavior versus assertions about the entire behavior. Suppose, under

"What is the behavior spec?" I choose a "Temporal formula" instead of

"Initial predicate and next-state relation." Section 6.7.2 of the

hyperbook states that a formula without temporal operators is a temporal

formula true of an entire behavior if it's true of its first state. I

gather this means that, when looking at a temporal formula that is a

conjunction, TLC picks out the conjuncts that are formulas with no

primes and no temporal operators (the state predicates), and only

ensures them on the first state of any behavior.

Here is my entire spec, including translation, as it stands now.

------------------------- MODULE OneBitTwoProcesses -------------------------

EXTENDS Integers

(******************************************************************

--algorithm OneBit

{ variable x = [i \in {0,1} |-> FALSE] ;

fair process (Proc \in {0,1})

{ ncs: while (TRUE)

\* This is the model for my non-critical processing.

{ skip ;

\* Ok, I'm done with that and I want in to the

\* critical section!

e1: x[self] := TRUE ;

e2: if (~x[1-self])

\* If the other guy isn't in, I'm in!

{ cs: skip (* Model for my critical code! *) }

else

\* Oops, the other guy is in. What do I do?

{ if (self = 0)

\* If I'm process 0, I'll keep trying.

{ goto e2 }

\* But, if I'm process 1, I'll be the nice guy;

\* I'll stop trying and spin while process 0 is in.

else

{ e3: x[1] := FALSE ;

e4: while ( x[0] )

{ skip (* spin *) } ;

goto e1

} } ;

\* Ok, I'm done. I don't need the critical section now.

f: x[self] := FALSE

}

} }

******************************************************************)

\* BEGIN TRANSLATION

VARIABLES x, pc

vars == << x, pc >>

ProcSet == ({0,1})

Init == (* Global variables *)

/\ x = [i \in {0,1} |-> FALSE]

/\ pc = [self \in ProcSet |-> "ncs"]

ncs(self) == /\ pc[self] = "ncs"

/\ TRUE

/\ pc' = [pc EXCEPT ![self] = "e1"]

/\ x' = x

e1(self) == /\ pc[self] = "e1"

/\ x' = [x EXCEPT ![self] = TRUE]

/\ pc' = [pc EXCEPT ![self] = "e2"]

e2(self) == /\ pc[self] = "e2"

/\ IF ~x[1-self]

THEN /\ pc' = [pc EXCEPT ![self] = "cs"]

ELSE /\ IF self = 0

THEN /\ pc' = [pc EXCEPT ![self] = "e2"]

ELSE /\ pc' = [pc EXCEPT ![self] = "e3"]

/\ x' = x

cs(self) == /\ pc[self] = "cs"

/\ TRUE

/\ pc' = [pc EXCEPT ![self] = "f"]

/\ x' = x

e3(self) == /\ pc[self] = "e3"

/\ x' = [x EXCEPT ![1] = FALSE]

/\ pc' = [pc EXCEPT ![self] = "e4"]

e4(self) == /\ pc[self] = "e4"

/\ IF x[0]

THEN /\ TRUE

/\ pc' = [pc EXCEPT ![self] = "e4"]

ELSE /\ pc' = [pc EXCEPT ![self] = "e1"]

/\ x' = x

f(self) == /\ pc[self] = "f"

/\ x' = [x EXCEPT ![self] = FALSE]

/\ pc' = [pc EXCEPT ![self] = "ncs"]

Proc(self) == ncs(self) \/ e1(self) \/ e2(self) \/ cs(self) \/ e3(self)

\/ e4(self) \/ f(self)

Next == (\E self \in {0,1}: Proc(self))

Spec == /\ Init /\ [][Next]_vars

/\ \A self \in {0,1} : WF_vars(Proc(self))

\* END TRANSLATION

PC0Labels == {"ncs", "f", "e1", "e2", "cs"}

ExtraLabels == {"e3", "e4"}

PC1Labels == PC0Labels \cup ExtraLabels

TypeOK == /\ pc \in [{0} -> PC0Labels] \cup [{1} -> PC1Labels]

/\ x \in [{0, 1} -> BOOLEAN]

InCS(i) == pc[i] = "cs"

MutualExclusion == ~(InCS(0) /\ InCS(1))

Fairness == \A i \in {0,1} : WF_vars(Proc(i))

Coordination == \A i \in {0,1} : InCS(i) \/ (pc[i] = "e2") => x[i]

Trying(i) == pc[i] \in {"e1", "e2"}

DeadlockFreedom == (Trying(0) \/ Trying(1)) ~> (InCS(0) \/ InCS(1))

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

A == INSTANCE OneBitProtocol

WITH pc <- [i \in {0, 1} |->

IF pc[i] \in {"ncs", "f", "e3", "e4"} THEN "r" ELSE pc[i]]

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

\* Modification History

\* Last modified Tue Feb 25 08:39:44 PST 2014 by bbeckman

\* Created Thu Feb 20 13:10:58 PST 2014 by bbeckman

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

**Re: Bikeshedding fun with problem 7.7***From:*Leslie Lamport

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