Hello! I went through the Alloy tutorial today, but was surprised to see syntax errors in the tutorial examples: thing' is no longer a legal name in Alloy 6 syntax. I replaced every ' character with "_after", and carried on.
Further digging showed that the syntax error occurred because. with Alloy 6, the humble apostrophe character has been upgraded to a token in the parser. Temporal logic is now a first-class citizen!
While this is extremely exciting now that I’ve more-or-less learned Alloy, it does mean we should update the tutorial so newcomers like me aren’t dissuaded.
I learned about Alloy from @hwayne, and he says on his blog that he’s the one in charge of the tutorial nowadays, so I am invoking his name in the hopes he sees this.
As part of rewriting the tutorial, here is the River Crossing puzzle, rewritten to use first-class temporal operators!
/* Farmer and his possessions are objects. */
abstract sig Object { eats: set Object }
one sig Farmer, Fox, Chicken, Grain extends Object {}
/* Defines what eats what when the farmer is not around. */
fact { eats = Fox->Chicken + Chicken->Grain }
/* Stores the objects at near and far side of river. */
var sig Near in Object {}
var sig Far in Object {}
/* An Object cannot be on both sides of the river at the same time */
fact always { disj [Near, Far] }
/* In the initial state, all objects are on the near side. */
fact { Near = Object && no Far }
/* Move the Farmer and at most one other Object from 'from' to 'to' */
pred crossRiver [from, to: set Object] {
one x: from | {
from' = from - x - Farmer - from'.eats
to' = to + x + Farmer
}
}
/* crossRiver takes the Farmer from one side to the other */
fact {
always {
Farmer in Near =>
crossRiver [Near, Far]
else
crossRiver [Far, Near]
}
}
/* the farmer moves everything to the far side of the river. */
run { eventually Far = Object }
This version plays nicer with Alloy’s graph visualization. It represents the near and far side of the river as Riverside sigs, with a here relation from a Riverside to each Object. Then it replaces the eats relation with predicate functions, purely so I could remove them from the graph and clean the graph up visually.
/* Farmer and his possessions are objects. */
abstract sig Object { }
one sig Farmer, Fox, Chicken, Grain extends Object {}
pred fox_can_eat_chicken [place: set Object] {
Fox in place && Chicken in place
}
pred chicken_can_eat_grain [place: set Object] {
Chicken in place && Grain in place
}
/**
* Make sure this predicate is never true
*/
pred chaos_reigns [place: set Object] {
Farmer not in place
fox_can_eat_chicken[place] || chicken_can_eat_grain[place]
}
/**
* The river has two sides: Near and Far
*/
sig Riverside {
var here: set Object
} {
always { not chaos_reigns[here] }
}
one sig Near extends Riverside { }
one sig Far extends Riverside { }
fact objects_must_be_on_one_side_or_the_other {
/* An Object can't be on both sides of the river at the same time */
always { disj [Near.here, Far.here] }
/* Every object must be on one side of the river or the other */
always { Near.here + Far.here = Object }
}
fact all_objects_initially_on_near_side {
/* All objects are initially on the near side */
Near.here = Object && no Far.here
}
/* Move the Farmer and at most one other Object from 'from' to 'to' */
pred crossRiver [from, to: set Object] {
one x: from | {
from' = from - x - Farmer
to' = to + x + Farmer
}
}
/* Move the Farmer from one side of the River to the other at each time step */
fact farmer_crosses_the_river {
always {
Farmer in Near.here =>
crossRiver[Near.here, Far.here]
else
crossRiver[Far.here, Near.here]
}
}
/* The farmer can move everything to the far side of the river. */
run move_everything_to_the_far_side_of_the_river {
eventually Far.here = Object
}
The Alloy homepage also directly links to these notes to learn Alloy 6. But you may also propose an updated version of the tutorial you linked to, if you’re willing to do it?
Thank you for the pointer! It looks like two PRs which fix minor issues have been sitting in review since November. I’ll start working on a PR once I see someone merge those in!
Looking at this more… I think my main issue with the website isn’t necessarily with any one tutorial, and is more with how the website is laid out. As a newcomer, I was kind of lost as to where to go:
The homepage has a picture of the cover of a book. Do I need that book? Is there a tutorial I can try first?
I also see
Formal Software Design with Alloy 6 is a completely new book (work in progress) specifically dedicated to learning Alloy, including the new Alloy 6 features.
Is that the book I can order? It has a different title than the picture…
Then I clicked on “book” at the top, and learned that I could order the book online. I didn’t click the link to “Formal Software Design with Alloy 6”, because I assumed I had already seen the book. How many books can there be?
I was still wandering in search of a quick tutorial, so I clicked “docs” and found a hodgepodge of resources. The only resource with “tutorial” in the name was the out-of-date Alloy 4 tutorial, so that’s how I learned Alloy.
I completely skipped over Formal Software Design with Alloy 6, because I was hopelessly confused by the disorganized plethora of learning options and was more-or-less breadth-first searching for the first line that says “tutorial”.
All of which is to say that, maybe what we need isn’t a better Alloy 4 6 tutorial so much as a website layout that guides users towards our newest and best resources, and away from the outdated resources.
Thanks for these relevant remarks. Indeed, there is some ambiguity between the cover of @DanielJackson’s book (addressing Alloy 4 “only”, but quite influential on a lot of us) and the Alloy 6 tutorial-style book advertised below which is work in progress.