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

*From*: Fumin Wang <awaw...@xxxxxxxxx>*Date*: Sun, 24 Aug 2014 19:29:55 +0800*References*: <dc96966e-530b-48f1-a502-45ba1f7f0cb8@googlegroups.com> <5397a425-8203-4597-ba8b-7a4d44906322@googlegroups.com> <af0a91d3-8acf-4760-871e-8773f172e741@googlegroups.com> <1ACE9F5C-47BE-458D-8360-C2A02C9AB102@gmail.com>

Ah, I see, this I believe is indeed what Leslie had in mind when he asked "how could I use TLC to help me figure out what's wrong".

Apparently, I still have a long way to go in internalizing the concepts of specifications and models in the context of TLA+.

While I actually did struggled to let TLC show me some examples of the more 300 million states it found with the buggy spec, including clicking on the headers of the statistics table which showed only a graph with the # of states on the Y axis and execution time on the X axis, but to no avail, I didn't realize I could achieve my goals by adding relevant invariants to my model and checking the resulting error trace like you suggested.

In retrospect, this practice of playing with invariants was a constant theme in the book and actually the way we derived the solution to the DieHard big :> 5 @@ small :> 3 problem, but I just wasn't able to take advantage of it like you suggested.

Thanks a lot for reemphasizing the importance of invariants in TLA+ and the explanation on the notion of functions in TLA+'s context!

On Sun, Aug 24, 2014 at 6:16 PM, Stephan Merz <Stepha...@xxxxxxxxx> wrote:

Such typos are often not so easy to catch, and the longer you stare at your specification the less you notice them. You can try to make your life a little easier by using TLC to check invariants that you'd assume to hold trivially, such as\A j \in Jugs : 0 <= injug[j] /\ injug[j] <= Capacity[j]as Leslie hinted at in item 4 of his answer. TLC would have shown you a counter-example that might have led you to your typo a little faster. Conversely, if TLC finds much fewer states than you expect your model to have, it helps to check predicates that you expect to be false. For example, you could assert predicates such as\A j \in Jugs : injug[j] = 0 or \E j \in Jugs : injug[j] = 0as invariants and letting TLC generate traces to help validate your specification.–––Concerning your question about distinguishing functional values: two functions f and g are equal iff their domains are equal and if for every value in that domain, the functions yield the same result, in symbolsf = g <=> (DOMAIN f = DOMAIN g) /\ (\A x \in DOMAIN f : f[x] = g[x])For those functions that TLC can represent explicitly, it can decide these conditions and thus compare two functions.Best regards,StephanOn 24 Aug 2014, at 11:48, Fumin Wang <awaw...@xxxxxxxxx> wrote:You received this message because you are subscribed to the Google Groups "tlaplus" group.Turns out that it was my bad, a typo by me in the line of Listing 1poured = Min(injug[j]+injug[k], Capacity[k] - injug[k])when it really should bepoured = Min(injug[j]+injug[k], Capacity[k]) - injug[k]Note the position of the closing parenthesis.----------------------------The debugging steps that led to this discovery was to first scrutinize the explanation and ASCII spec as described in the book. After rereading the passage a couple of times, I was pretty convinced that the book was correct.Could there really be some special treatment for function variables in TLC like I wrongly suspected in the previous post? Again after rereading chapter 15 and the paper "Should your specification language be Typed", I was pretty convinced that functions were nothing special under a Set-theoretic treatment. In other words, if the tuple of numbers << big, small >> is conceptually enumerable and distinctable, so could the tuple of an function << injug >>.This leaves the possibility of something wrong in my code. Further scrutiny eventually revealed the bug and typo described above. Fixing it results in the number of distinct states being 6 as expected.----------------------By the way, thanks for the anecdote about the faulty book on Differential Geometry. Although, I am now most excited to be able to proceed on to chapter 6 and begin entering the main topic of analyzing distributed systems, I'd nevertheless be carrying the lesson with me.

On Sunday, August 24, 2014 2:24:41 PM UTC+8, Leslie Lamport wrote:1. If every jug must contain an integral amount of water between 0 and

its capacity, how many possible reachable states are there?2. How many reachable states did TLC find before you stopped it?

3. What can you deduce from your answers to 1 & 2?

4. Does your answer to 3 suggest how you can use TLC to help you

figure out what's wrong?----

Many years ago I read a book on differential geometry. The book was fullof errors. I couldn't believe anything it said. I had to check everythingand, if it was wrong, I had to figure out how to correct it. No other bookever taught me as much as that book.

Leslie

On Saturday, August 23, 2014 9:48:23 PM UTC-7, Fumin Wang wrote:While validating the sentenceTry other models. Start with a model with two jugs of capacity 3 and 6 gallons, having the goal of obtaining 4 gallons of water. TLC will report that the alleged invariant actually is an invariant.

on page 57 of the TLA+ hyperbook, I observed that the DieHarder spec (Listing 1) does not end with the number of distinct states ever increasing (about 300 million after 10 minutes or so). However, the seemingly equivalent PDieHard (Listing 2) ends pretty soon reporting only 6 distinct states. How could this be? If the model-checking goes on infinitely, how do we infer from TLC " that the alleged invariant actually is an invariant"?

My unsatisfying explanation right now is that since in the PDieHard spec, the variables "big" and "small" are Integers, and therefore have an unambiguous definition for their distinctness. In the Dieharder spec, the variable "injug" is a function, which might not possess a notion of distinctness. Obviously, this explanation is confusing and funky.

Is it true that there is some deficiency in the DieHarder version of the spec to the same DieHard problem, or did I misunderstood something and introduced some bug in Listing 1?

------------------------------

-------Listing 1

--algorithm DieHarder {

variable injug = [j \in Jugs |-> 0];

{ while (TRUE)

{ either with (j \in Jugs) \* fill jug j

{ injug[j] := Capacity[j] }

or with (j \in Jugs) \* empty jug j

{ injug[j] := 0 }

or with (j \in Jugs, k \in Jugs \ {j}) \* pour from jug j to jug k

{ with (poured = Min(injug[j]+injug[k], Capacity[k] - injug[k]))

{ injug[k] := injug[k] + poured ||

injug[j] := injug[j] - poured }

}

}

}

}-----------------------

Listing 2

--algorithm DieHard {

variables big = 0, small = 0;

{ while (TRUE)

{ either big := 6

or small := 3

or big := 0

or small := 0

or with (poured = Min (big + small, 6) - big)

{ big := big + poured;

small := small - poured }

or with (poured = Min(big + small, 3) - small)

{ big := big - poured;

small := small + poured }

}

}

}

--

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/d/optout.

--

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.

To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/y4XkKrZy2Tc/unsubscribe.

To unsubscribe from this group and all its topics, 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/d/optout.

**References**:**Why model-checking of DieHarder does not end, but PDieHard does?***From:*awaw . . .

**Re: Why model-checking of DieHarder does not end, but PDieHard does?***From:*Leslie Lamport

**Re: Why model-checking of DieHarder does not end, but PDieHard does?***From:*Fumin Wang

**Re: [tlaplus] Re: Why model-checking of DieHarder does not end, but PDieHard does?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Re: Why model-checking of DieHarder does not end, but PDieHard does?** - Next by Date:
**Re: "Partial" Functions** - Previous by thread:
**Re: [tlaplus] Re: Why model-checking of DieHarder does not end, but PDieHard does?** - Next by thread:
**Termination with multi-processes** - Index(es):