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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Sat, 23 Aug 2014 23:24:41 -0700 (PDT)*References*: <dc96966e-530b-48f1-a502-45ba1f7f0cb8@googlegroups.com>

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?

figure out what's wrong?

----

Many years ago I read a book on differential geometry. The book was full

of errors. I couldn't believe anything it said. I had to check everything

and, if it was wrong, I had to figure out how to correct it. No other book

ever 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 }

}

}

}

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

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

- Prev by Date:
**Re: Why Amazon Chose TLA+** - Next by Date:
**Re: "Partial" Functions** - Previous by thread:
**Why model-checking of DieHarder does not end, but PDieHard does?** - Next by thread:
**Re: Why model-checking of DieHarder does not end, but PDieHard does?** - Index(es):