The Die Hard Problem in Alloy 3

In the examples included with the TLA+ Tools distribution, Leslie Lamport includes a solution to the so-called Die Hard Problem:

In the movie Die Hard 3, the heros must obtain exactly 4 gallons of water using a 5 gallon jug, a 3 gallon jug and a water faucet.

Today, as an excercise in using the natural numbers in Alloy, I translated the TLA+ solution into Alloy 3:

 module tristram/diehard
   
   open util/natural
   open util/ordering[State] as SO
   
   /* Define names for Natural numbers Two to Five 
      (Zero and One are defined in util/natural):
   */
   lone sig Two in Natural {}
   lone sig Three in Natural {}
   lone sig Four in Natural {}
   lone sig Five in Natural {}
   fact {
     Two = inc(One)
     Three = inc(Two)
     Four = inc(Three)
     Five = inc(Four)
   }
   
   sig State {
     small : Natural,
     big : Natural
   }
   
   pred init(s : State) {
     s.small = Zero
     s.big = Zero
   }
   
   pred emptysmall(s, s' : State) {
     s'.small = Zero
     s'.big = s.big
   }
   
   pred emptybig(s, s' : State) {
     s'.small = s.small
     s'.big = Zero
   }
   
   pred fillsmall(s, s' : State) {
     s'.small = Three
     s'.big = s.big
   }
   
   pred fillbig(s, s' : State) {
     s'.small = s.small
     s'.big = Five
   }
   
   pred smalltobig(s, s' : State) {
     let t = add(s.small,s.big) |
       s'.big = if util/natural/lt(t, Five) then t else Five
     s'.small = sub(s.small, sub(s'.big, s.big))
   }
   
   pred bigtosmall(s, s' : State) {
     let t = add(s.small, s.big) |
       s'.small = if util/natural/lt(t, Three) then t else Three
     s'.big = sub(s.big, sub(s'.small, s.small))
   }
   
   fact Traces {
     init(SO/first())
     all s : State - SO/last() |
       let s' = SO/next(s) |
         emptysmall(s, s') or
         emptybig(s, s') or
         fillsmall(s, s') or
         fillbig(s, s') or
         smalltobig(s, s') or
         bigtosmall(s, s')
   }
   
   pred show() {
     SO/last().small = Four or
     SO/last().big = Four
   }
   
   /* 7 is the smallest scope for States that gives a solution.
      This was found by progressively increasing the scope.
      We need scope 9 for the naturals (0..8) because smalltobig 
      and bigtosmall use the sum of s.small and s.big:
   */
   run show for 7 but 9 Natural
   

The Economics of Colonizing Other Planets

Anthropologist John Hawks has produced what I regard as the definitive refutation of  Stephen Hawking's argument that humans ought to spread to other planets in order to survive catastrophes that strike Earth.  His refutation is based on economic and genetic considerations.

Lisp as an 'Improved XML'

Steve Yegge's old blog, Stevey's Drunken Blog Rants, contains a lot of good reading for anyone interested in programming.  I particularly like his post The Emacs Problem in which he demonstates convincingly that the ancient programming language Lisp is better at representing structured text than the currently fashionable XML.  Here is a sample Java error log in XML:

<?xml version="1.0" encoding="utf-8" standalone="no"?>
 <!DOCTYPE log SYSTEM "logger.dtd">
 <log>
 <record>
   <date>2005-02-21T18:57:39</date>
   <millis>1109041059800</millis>
   <sequence>1</sequence>
   <logger></logger>
   <level>SEVERE</level>
   <class>java.util.logging.LogManager$RootLogger</class>
   <method>log</method>
   <thread>10</thread>
   <message>A very very bad thing has happened!</message>
   <exception>
     <message>java.lang.Exception</message>
     <frame>
       <class>logtest</class>
       <method>main</method>
       <line>30</line>
     </frame>
   </exception>
 </record>
 </log> 

And here is the same in Lisp:

(log
 '(record
   (date "2005-02-21T18:57:39")
   (millis 1109041059800)
   (sequence 1)
   (logger nil)
   (level 'SEVERE)
   (class "java.util.logging.LogManager$RootLogger")
   (method 'log)
   (thread 10)
   (message "A very very bad thing has happened!")
   (exception
     (message "java.lang.Exception")
     (frame
       (class "logtest")
       (method 'main)
       (line 30)))))
 

Not only is the Lisp version shorter, less verbose and clearer, it also doesn't require you to learn another half dozen half-baked programming languages and frameworks in order to be able to write a program to read it and process it.

The older I get, the less patience I seem to have with unnecessary syntactic baggage, and more attractive I find Lisp's simplicity.  However, for the time being I think I will stick with Haskell.

A New Version of Alloy

Beta versions of version 4 of the Alloy Analyzer are available from here.  This version includes some changes to the syntax of the Alloy language (see here), which is unfortunate since it makes Daniel Jackson's new book obsolete only 6 months after it was published.  However, updating models from version 3 to version 4 syntax does seem to be fairly easy. Still, it might be a good idea to have Alloy 3 and Alloy 4 installed alongside each other, at least until you have got used to the new version.

Never Let Me Go by Kazuo Ishiguro

A strange and moving story. Thirty-one year old Kathy H. looks back over her life to her days at Hailsham school and tries to make sense of it.  Initially Hailsham seems like a typical boarding school but gradually the reader becomes aware that the world it exists in has a dark secret, the full nature of which is not revealed till the penultimate chapter.  Mallory Towers meets 1984 is how you might describe it, though Ishiguro is a much better writer than both Blyton or Orwell.  When reading Ishiguro I  continually find myself struck by the power of writing: how a string of simple words describing the lives of ordinairy people can produce such a gripping experience.