Propositional Logic

------------------------------ 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.)              *)
(***************************************************************************)
=============================================================================