Hi: Posting it here is fine.
Thank you in advance for helping us improve the tutorials.

Sincerely,
Felix Chang
Alloy4 Lead Developer

These are suggested corrections to the Alloy 4 tutorial.

On page http://alloy.mit.edu/alloy4/tutorial4/frame-FS-3.html :
"exactly 1 FileSystem and up to 4 FileSytemObjects"
should be
"exactly 1 FileSystem and up to 4 FSObject".

On page http://alloy.mit.edu/alloy4/tutorial4/frame-FS-6.html :
"One reflection of this is that functions in Alloy only ever evaluate to true or false...".
But in the side note it says "A predicate returns true or false. A similar construct is a function which returns a value".  So all use of "function" in this paragraph should be "predicate" (or something else like "routine").

"1. pred move [fs, fs': FileSystem, x: FSObject, d: Dir] {
2.     (x + d) in fs.objects
3.     fs'.parent = fs.parent - x->(x.(fs.parent)) + x->d
4. }":
In line 2, "(x + d) in fs.objects" should be "(x + d) in fs.live".

"moveOkay: check {
    all fs, fs': FileSystem, x: FSObject, d:Dir |
      move[fs, fs', x, d] => fs'.objects = fs.objects
  } for 5":
Similarly, "fs'.objects = fs.objects" should be "fs'.live = fs.live".

"assert moveOkay {
    all fs, fs': FileSystem, x: FSObject, d:Dir |
      move[fs, fs', x, d] => fs'.objects = fs.objects
  }":
Similarly, "fs'.objects = fs.objects" should be "fs'.live = fs.live".

"It stipulates that the file system object to be deleted, ... Certainly, it doesn't make sense to delete ...; nor does it make sense to delete ...":
Each "delete" should be "remove" since you named the predicate "remove".

"Our assertions claim that the functions to do not alter the root of the file system; that the rows in the contents relation of the post-state is a subset of the rows in the pre-state; and that they remove exactly the objects they should":
It looks to me like removeOkay and removeAllOkay only do the third check.  That is, I don't see how they check that the predicates do not alter the root or check the contents relation.  If removeOkay and removeAllOkay somehow do this, then more explanation is needed.  If not, then the text needs correction.

On page http://alloy.mit.edu/alloy4/tutorial4/frame-FS-7.html :
"However if delete function"
should be
"However if the remove predicate".

"We can amend our delete functions to stipulate that the root stays the same. The amended delete functions look as follows"
should be
"We can amend our remove predicates to stipulate that the root stays the same. The amended remove predicates look as follows".

"thus further reassuring us that the remove predicates functions were written correctly"
should be
"thus further reassuring us that the remove predicates were written correctly".

On page http://alloy.mit.edu/alloy4/tutorial4/frame-RC-1.html :
"sig Farmer, Fox, Chicken, Grain extends Object {}", but this gives the error "You must specify a scope for sig "this/Object"".   The the code in the upper-right pane is correct:
"one sig Farmer, Fox, Chicken, Grain extends Object {}".
Perhaps the tutorial should explain why "one" is needed.

"In this case, Alloy will assume three are 3 State atoms"
should be
"In this case, Alloy will assume there are 3 State atoms".

On page http://alloy.mit.edu/alloy4/tutorial4/sidenote-OO-paradigm.html :
"Signatures are technically sets, but they can be thought of as objects in the OO paradigm"
should be
"Signatures are technically sets, but they can be thought of as classes in the OO paradigm".

In
"sig S extends E {
    F:T
  }

  fact {
    all s:S | s.F in X
  }",
"s.F in X" should be "s.F in T".

On page http://alloy.mit.edu/alloy4/tutorial4/sidenote-levels-of-understanding.h... :
In
"sig S extends E {
      F: one T
  }

  fact {
      all s:S | s.F in X
  }",
"s.F in X" should be "s.F in T".

Thanks,
- Jeff

Hi Jeff: Thank you very much. I'll check over these suggestions then commit the fixes to the tutorial.
We really appreciate your help!

Sincerely,
Felix Chang
Alloy4 Lead Developer

While you're at it, these are suggested errata for "Software Abstractions" to add to
http://alloy.mit.edu/alloy4/book.html

Page 39, near the middle:
Old:
addrT = {(N0, D0, T0), (N1, D1, T0), (N2, D2, T0)}
New:
addrT = {(N0, D0, T0), (N0, D1, T0), (N2, D2, T0)}

Page 65, near the bottom:
Old:
univ = {(B0), (B1), (N0), (N1), (D0), (D1), (B0), (B1)}
New:
univ = {(B0), (B1), (N0), (N1), (D0), (D1)}

Page 116, near the bottom:
Old:
the expression x.f in the equivalent form f.~x
New:
the expression x.f in the equivalent form (~f).x
[x is unary, so it doesn't make sense to reverse it.]

Page 175, near the middle:
Old:
sig Time {
sig Process {
  ...
}
New:
sig Time {}
sig Process {
  ...
}

Page 204, near the bottom:
  part hidden, showing: set assets,
  [but the part qualifier has been removed in Alloy 4.  Need to fix the example?]

Thank you again so much for your careful reading. I'll forward these errata to Daniel.

Recently I was busy preparing for my thesis defense, so I haven't had time
to gone through the bug reports yet, but I promise I'll get to them as soon as I can.
Thank you!

Sincerely,
Felix Chang
Alloy4 Lead Developer

Jeff,

Many thanks indeed. I am planning a revision of the book soon, so this is very useful.

--Daniel