Alloy 6 First Impressions

So a couple of weeks ago I wrote Finding Alloy's Niche, where I said I wasn't expecting the new Alloy 6 release to change all that much. It came out last Tuesday, I tried it out, figuring that I'd update the Alloydocs in mid-December or so.

Totally unrelated: I was planning on uploading a TLA+ post to the blog today, it's 99% finished, but I didn't bother because I need to get an Alloy post out right frickin' now.¹ Because as of last Tuesday all existing Alloy learning material is obsolete.

The online tutorial uses signature cloning and state signatures to emulate a temporal spec. Every example in Daniel Jackson's book at some point has to emulate time. The Alloydocs has an entire section on ways to represent time. Alloy material breaks down to "various tricks to hack time into your spec" and "everything else". But now Alloy 6 has first class time constructs. Instead of writing the river crossing puzzle like this:

-- fox/chicken/corn puzzle
-- from sample modules
module examples/tutorial/farmer

open util/ordering[State] as ord

abstract sig Object { eats: set Object }
one sig Farmer, Fox, Chicken, Grain extends Object {}

fact eating { eats = Fox->Chicken + Chicken->Grain }

sig State {
   near: set Object,
   far: set Object
}

fact initialState {
   let s0 = ord/first |
     s0.near = Object && no s0.far
}

pred crossRiver [from, from", to, to": set Object] {
   // either the Farmer takes no items
   (from" = from - Farmer - from".eats and
    to" = to + Farmer) or
    // or the Farmer takes one item
    (one x : from - Farmer | {
       from" = from - Farmer - x - from".eats
       to" = to + Farmer + x })
}

fact stateTransition {
  all s: State, s": ord/next[s] {
    Farmer in s.near =>
      crossRiver[s.near, s".near, s.far, s".far] else
      crossRiver[s.far, s".far, s.near, s".near]
  }
}

pred solvePuzzle {
    ord/last.far = Object
}

run solvePuzzle for 8 State

assert NoQuantumObjects {
   no s : State | some x : Object | x in s.near and x in s.far
}

check NoQuantumObjects for 8 State

You can just write this:

module examples/tutorial/farmer

abstract sig Object { eats: lone Object }
one sig Farmer, Fox, Chicken, Grain extends Object {}
fact eating { eats = Fox->Chicken + Chicken->Grain }
var sig Crossed in Object {}

pred same_side[o1, o2: Object] {
  (o1 in Crossed <=> o2 in Crossed)
}

pred cross[o: Object] {
  {
    (o + Farmer) in Crossed
    Crossed' = Crossed - Farmer - o
  } or
  {
    (o + Farmer) in Object - Crossed
    Crossed' = Crossed + Farmer' + o'
  }
}

pred safe {
  all o1: Object, o2: o1.eats |
    same_side[o1, o2] implies same_side[Farmer, o1]
}

pred Next {
  some item: Object | --includes Farmer
    cross[item]
}

solvePuzzle: run {
  no Crossed
  always Next
  always safe
  eventually Crossed = Object
}

Also, the visualizer is much nicer. Compare this:

To this:

I'm especially excited about the added "past" temporal operators. Want to check if a certain value was, at some point, in a relation? once {x in y.rel}. And as you can see from how I structured the program, there's really no difference between using temporal operations to describe the behavior of a system and using them to describe its properties. Both are equally valid, which opens up lots of cool uses. Combined with Alloy's model-finding (not just model-checking) capabilities, and you have a solid tool for exploring concurrent systems!

Natch, there's also some problems, many of which stem from this being the first public iteration. For one, while the tooling now has new trace exploration options, it hasn't fully caught up. The big one is that the visualizer layout isn't fixed: the atoms can move around between steps, which makes the trace a lot more confusing.

The other main issue is a footgun: if you don't fully specify the next-state of every mutable value, Alloy will just pick an arbitrary value. This was also a problem in the old way of doing things, but it was unfixable then (because you were emulating time with regular relations). Now, though, it should be possible to raise a compiler warning whenever that happens. That'd be nice to see.

(Another issue is that you can't retrieve the step state. I have no idea if this is something people will eventually need, but it's worth noting.)

Overall, though, this is a major update and I'm incredibly excited about it. But, as I said before, this also means a lot of work. Here's roughly what I'm seeing as my tasks:

1. Write an Alloy 6 blog post that explains to existing users the new features and why they're interesting. Something that at least gets them to experiment. I'm working on this right now.
2. Fix the Pygments and GitHub syntax highlighters. Not only is there new syntax, there's also a backwards incompatible syntax change. Legacy specs would often write some x, x': Foo, but now ' is an operator, so now we're supposed to write some x, x": Foo, which the highlighters think starts a string. You can already see the issue in the farmer crossing spec up above.
3. Update AlloyDocs. I'll need to add all of the new syntax, which means thoroughly documenting all the edge cases.
4. Find extant Alloy resources and talk to their owners about making them Alloy6 compatible. This mostly means replacing foo' with foo"; maybe some people would be up to modernize their specs too.
5. Write a new tutorial. The old one has been showing its age anyway.
6. Write a guide to linear temporal logic, because it's actually pretty unintuitive and people will need help with that. Like what eventually(p and after always q) means or how □∀p.x = ∀p.□x while you can't do the same with □∃.
7. New book??!?!?!?!?!?!?!

Then there's the revising the workshop. I don't know whether it's better to cover all the static Alloy and then dynamics or to thread temporal logic through the usual route. The temporal stuff opens a lot more interesting examples that don't require transitive closure or multirelations, so I don't have to build up to them as quickly and can order the content in a different way.

Anyway, I should get back to the blog post. Lots to talk about, lots to draw. Have a good week!

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.