# Alloy 6 tutorial updates

**URL:** <https://alloytools.discourse.group/t/alloy-6-tutorial-updates/432>\
**Category:** Alloy 6\
**Created:** [January 15, 2024, 5:29am UTC](https://alloytools.discourse.group/t/alloy-6-tutorial-updates/432 "2024-01-15T05:29:31Z")\
**Posts on this page:** 11\
**Page:** 1

<div class="post-metadata">

**Author:** ![jthemphill](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/jthemphill/32/220_2.png) [@jthemphill](https://alloytools.discourse.group/u/jthemphill)\
**Post date:** [January 15, 2024, 5:29am UTC](https://alloytools.discourse.group/t/alloy-6-tutorial-updates/432/1 "2024-01-15T05:29:31Z")

</div>

Hello! I went through [the Alloy tutorial](https://alloytools.org/tutorials/online/index.html) 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](https://alloytools.org/tutorials/online/frame-RC-1.html), rewritten to use first-class temporal operators!

```auto
/* 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 }

```

---

<div class="post-metadata">

**Author:** ![jthemphill](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/jthemphill/32/220_2.png) [@jthemphill](https://alloytools.discourse.group/u/jthemphill)\
**Post date:** [January 15, 2024, 6:45am UTC](https://alloytools.discourse.group/t/alloy-6-tutorial-updates/432/2 "2024-01-15T06:45:49Z")

</div>

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.

```auto
/* 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
}

```

---

<div class="post-metadata">

**Author:** ![hwayne](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/hwayne/32/67_2.png) [@hwayne](https://alloytools.discourse.group/u/hwayne)\
**Post date:** [January 15, 2024, 7:06am UTC](https://alloytools.discourse.group/t/alloy-6-tutorial-updates/432/3 "2024-01-15T07:06:33Z")

</div>

I’m actually maintaining reference docs ([alloy.readthedocs.org](http://alloy.readthedocs.org)), not the tutorial D:

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [January 15, 2024, 8:38am UTC](https://alloytools.discourse.group/t/alloy-6-tutorial-updates/432/4 "2024-01-15T08:38:38Z")

</div>

The Alloy homepage also directly links to [these notes](https://haslab.github.io/formal-software-design/) 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?

---

<div class="post-metadata">

**Author:** ![jthemphill](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/jthemphill/32/220_2.png) [@jthemphill](https://alloytools.discourse.group/u/jthemphill)\
**Post date:** [January 15, 2024, 6:50pm UTC](https://alloytools.discourse.group/t/alloy-6-tutorial-updates/432/5 "2024-01-15T18:50:36Z")

</div>

> But you may also propose an updated version of the tutorial you linked to, if you’re willing to do it?

Where should I post it? I would have proposed an edit already if it were, say, a Wiki or on GitHub. Instead, I’m here😉

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [January 16, 2024, 9:24am UTC](https://alloytools.discourse.group/t/alloy-6-tutorial-updates/432/6 "2024-01-16T09:24:34Z")

</div>

Looks like the source is here: [alloytools.github.io/tutorials/online at master · AlloyTools/alloytools.github.io · GitHub](https://github.com/AlloyTools/alloytools.github.io/tree/master/tutorials/online)  
A pull request would be most welcome if you feel so inclined!

---

<div class="post-metadata">

**Author:** ![jthemphill](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/jthemphill/32/220_2.png) [@jthemphill](https://alloytools.discourse.group/u/jthemphill)\
**Post date:** [January 21, 2024, 4:19am UTC](https://alloytools.discourse.group/t/alloy-6-tutorial-updates/432/7 "2024-01-21T04:19:24Z")

</div>

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!

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [January 22, 2024, 8:05am UTC](https://alloytools.discourse.group/t/alloy-6-tutorial-updates/432/8 "2024-01-22T08:05:27Z")

</div>

Thanks, I just made the commit.

---

<div class="post-metadata">

**Author:** ![jthemphill](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/jthemphill/32/220_2.png) [@jthemphill](https://alloytools.discourse.group/u/jthemphill)\
**Post date:** [January 22, 2024, 4:56pm UTC](https://alloytools.discourse.group/t/alloy-6-tutorial-updates/432/9 "2024-01-22T16:56:15Z")

</div>

Brilliant, good to know it’s being maintained! I’ll take a look at updating the tutorial🙂

---

<div class="post-metadata">

**Author:** ![jthemphill](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/jthemphill/32/220_2.png) [@jthemphill](https://alloytools.discourse.group/u/jthemphill)\
**Post date:** [February 13, 2024, 7:10am UTC](https://alloytools.discourse.group/t/alloy-6-tutorial-updates/432/10 "2024-02-13T07:10:52Z")

</div>

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](https://haslab.github.io/formal-software-design/) 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](https://haslab.github.io/formal-software-design/), 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.

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [February 13, 2024, 9:37am UTC](https://alloytools.discourse.group/t/alloy-6-tutorial-updates/432/11 "2024-02-13T09:37:30Z")

</div>

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.