Some other information.
------------------------------ MODULE DieHard ------------------------------- (***************************************************************************) (* In the movie Die Hard J1, the heros must obtain exactly 4 gallons of *) (* water using a J2 gallon jug, a J1 gallon jug, and a water faucet. Our *) (* goal: to get TLC to solve the problem for us. *) (* *) (* First, we write a spec that describes all allowable behaviors of our *) (* heros. *) (***************************************************************************) EXTENDS Integers (*************************************************************************) (* This statement imports the definitions of the ordinary operators on *) (* integers, such as +. *) (*************************************************************************) CONSTANTS J1, J2, G (***************************************************************************) (* We next declare the specification's variables. *) (***************************************************************************) VARIABLES big, \* The number of gallons of water in the J2 gallon jug. small \* The number of gallons of water in the J1 gallon jug. (***************************************************************************) (* Now we define of the initial predicate, that specifies the initial *) (* values of the variables. I like to name this predicate Init, but the *) (* name doesn't matter. *) (* *) (* Note: TLA+ uses the convention that a list of formulas bulleted by /\ *) (* or \/ denotes the conjunction or disjunction of those formulas. *) (* Indentation of subitems is significant, allowing one to eliminate lots *) (* of parentheses. This makes a large formula much easier to read. *) (* However, it does mean that you have to be careful with your indentation.*) (***************************************************************************) Init == /\ big = 0 /\ small = 0 (***************************************************************************) (* Now we define the actions that our hero can perform. There are three *) (* things they can do: *) (* *) (* - Pour water from the faucet into a jug. *) (* *) (* - Pour water from a jug onto the ground. *) (* *) (* - Pour water from one jug into another *) (* *) (* We now consider the first two. Since the jugs are not calibrated, *) (* partially filling or partially emptying a jug accomplishes nothing. *) (* So, the first two possibilities yield the following four possible *) (* actions. *) (***************************************************************************) FillSmall == /\ small' = J1 /\ big' = big FillBig == /\ big' = J2 /\ small' = small EmptySmall == /\ small' = 0 /\ big' = big EmptyBig == /\ big' = 0 /\ small' = small (***************************************************************************) (* We now consider pouring water from one jug into another. Again, since *) (* the jugs are not callibrated, when pouring from jug A to jug B, it *) (* makes sense only to either fill B or empty A. And there's no point in *) (* emptying A if this will cause B to overflow, since that could be *) (* accomplished by the two actions of first filling B and then emptying A. *) (* So, pouring water from A to B leaves B with the lesser of (i) the water *) (* contained in both jugs and (ii) the volume of B. To express this *) (* mathematically, we first define Min(m,n) to equal the minimum of the *) (* numbers m and n. *) (***************************************************************************) Min(m, n) == IF m < n THEN m ELSE n (***************************************************************************) (* Now we define the last two pouring actions. From the observation *) (* above, these definitions should be clear. *) (***************************************************************************) SmallToBig == LET poured == Min(big + small, J2) - big \* The amount of water poured. IN /\ big' = big + poured /\ small' = small - poured BigToSmall == LET poured == Min(big + small, J1) - small IN /\ big' = big - poured /\ small' = small + poured (***************************************************************************) (* We define the next-state relation, which I like to call Next. A Next *) (* step is a step of one of the six actions defined above. Hence, Next is *) (* the disjunction of those actions. *) (***************************************************************************) Next == \/ FillSmall \/ FillBig \/ EmptySmall \/ EmptyBig \/ SmallToBig \/ BigToSmall ---------------------------------------------------------------------------- (***************************************************************************) (* We now define TypeOK to be the type invariant, asserting that the value *) (* of each variable is an element of the appropriate set. A type *) (* invariant like this is not part of the specification, but it's *) (* generally a good idea to include it because it helps the reader *) (* understand the spec. Moreover, having TLC check that it is an *) (* invariant of the spec catches errors that, in a typed language, are *) (* caught by type checking. *) (***************************************************************************) TypeOK == /\ small \in 0..J1 /\ big \in 0..J2 ----------------------------------------------------------------------------- (***************************************************************************) (* Remember that our heros must measure out 4 gallons of water. *) (* Obviously, those 4 gallons must be in the J2 gallon jug. So, they have *) (* solved their problem when they reach a state with big = 4. We find a *) (* solution by having TLC check if big # 4 is an invariant, which will *) (* cause it to print out an "error trace" consisting of a behavior ending *) (* in a states where big # 4 is false--that is, ending in a state in which *) (* big = 4. Such a behavior is the desired solution. (Because TLC uses a *) (* breadth-first search, it will find the shortest solution.) *) (***************************************************************************) =============================================================================
Left-click to open it in a new window,
or right-click
and select
Save as ...
to download it.