Entries by Tristram Brelstaff (3025)

Wednesday
Dec202006

Reflections

Windows within Windows

Over the past few months the photographs I have taken have tended more and more to be of reflections, both in water or in windows. I find that reflections are a good way of making mundane things interesting.  I often notice opportunities for interesting pictures when I don't have my camera with me and then I make a mental note to return at a later date when I think the conditions will be the same. For the above picture I was lucky and had my camera with me in my bag. Western Tower was already one of my favorite subjects in Reading and when I caught a glimpse of it reflected in the windows of Greyfriars house I immediately wanted to take a picture of it. I had to move around and cross the road several times before I got one that satisfied me.

Saturday
Dec162006

When Palaeontologists send Christmas Cards...

 

happy-christmas.jpg

Via Darren Naish at Tetrapod Zoology

Tuesday
Dec122006

Fox

When I opened the bedroom curtain at 6:30 this morning there was a fox running along the other side of the fence that separates our flats from the neighboring property.  Keeping low and holding its tail straight out behind, it ran over the road and into the grounds of the Reading School.

Saturday
Dec092006

Falcon by Helen Macdonald

falcon.jpgHelen Macdonald, a research fellow at Cambridge University, is a poet, historian and falcon-lover.   Her blog contains some of the most interesting and poetical ornithological writing available on the web. Her latest book 'Falcon' is not so much a natural history book as a history of the relationship between falcons and man.  A deceptively small book, its 208 pages are densely packed with stories and illustrations.  Since having read it, I often find myself scanning the skies longingly.  However, the only raptors we get here are red kites and the occasional buzzard or kestrel.  Maybe if I keep looking...

Friday
Dec082006

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