There is one change that is needed in almost every example, and it would be too numerous to list every occurrence:
function and predicate invocations in Alloy 4 uses [ ] instead of ( ).

Alloy 3		add (3,4)
Alloy 4		add [3,4]

Page 69: The table of logical operators should be changed to this:

not	!	negation
and	&&	conjunction
or	||	disjunction
implies	=>	implication
else		alternative
iff	<=>	bi-implication

Page 69, the example near the bottom:

Alloy 3		Alloy 4
C1=>F1, C2=>F2, C3=>F3		C1=>F1 else C2=>F2 else C3=>F3

Page 70, the example near the top:

Alloy 3		Alloy 4
if C then E1 else E2		C => E1 else E2

Page 70, the example near the middle:

Alloy 3		Alloy 4
some a.workAddress =>   a.address = a.workAddress ,   a.address = a.homeAddress or, using an if-then-else expression a.address =   if some a.workAddress   then a.workAddress   else a.homeAddress		some a.workAddress   => a.address = a.workAddress   else a.address = a.homeAddress or, using an if-then-else expression a.address =   (some a.workAddress   => a.workAddress   else a.homeAddress)

Page 72, the example near the middle:

Alloy 3		all p, q: univ lone->lone univ | p.q : univ lone->lone univ
Alloy 4		all p, q: univ lone->lone univ | p.q in univ lone->lone univ

Page 73, the example at the bottom:

Alloy 3		all a: Alias |   let w = a.workAddress |     a.address = if some w then w else a.homeAddress
Alloy 4		all a: Alias |   let w = a.workAddress |     a.address = (some w => w else a.homeAddress)

Page 74, the example near the top:

Alloy 3		all a: Alias |   a.address =     let w = a.workAddress |       if some w then w else a.homeAddress
Alloy 4		all a: Alias |   a.address =     (let w = a.workAddress | some w => w else a.homeAddress)

Page 75:

Alloy 3		Its meaning is almost -- a caveat soon -- as if
Alloy 4		Its meaning is as if

Page 76:

Alloy 3		In the last section... Now the caveat: the declaration can
Alloy 4		A declaration can

Page 79, section 3.6.4:

Alloy 3		Declarations usually introduce new names... (because of the default multiplicity).
Alloy 4		The subset operator in can also be used to impose constraints on relations that have already been declared, or on arbitrary expressions.

Page 79, section 3.6.4:

Alloy 3		Alias <: address : Alias ->lone Addr
Alloy 4		Alias <: address in Alias ->lone Addr

Page 79, section 3.6.4:

Alloy 3		all b: Book | b.addr : Name lone-> Addr
Alloy 4		all b: Book | b.addr in Name lone-> Addr

Page 79, section 3.6.5:

Alloy 3		all a:A | a.r : B m->n C
Alloy 4		all a:A | a.r in B m->n C

Page 80, section 3.6.5:

Alloy 3		all c:C | r.c : A m->n B
Alloy 4		all c:C | r.c in A m->n B

Page 80, section 3.6.5:

Alloy 3		all b:Book | b.addr : Name lone-> Addr
Alloy 4		all b:Book | b.addr in Name lone-> Addr

Page 82:

Alloy 3		They are easily disambiguated from the context -- in fact, by parsing alone.
Alloy 4		They are easily disambiguated from the context by the typechecker.

Page 95, near the middle:

Alloy 3		as if a fact included the declaration constraint f : A->e
Alloy 4		as if a fact included the constraint f in A->e

Page 95, near the middle:

Alloy 3		all this:A | this.f : e
Alloy 4		all this:A | this.f in e

Page 95, near the bottom:

Alloy 3		all this:A | this.f : m e
Alloy 4		all this:A | this.f in m e

Page 96, near the middle:

Alloy 3		all this:A | this.f : e1 m->n e2
Alloy 4		all this:A | this.f in e1 m->n e2"

Page 98:

The part qualifier has been removed in Alloy 4.

Page 104, at the very bottom of the page:

Alloy 3		all a:A | a.R : B->one C
Alloy 4		all a:A | a.R in B->one C

Page 120:

Alloy 3		sig Book {     homeAddress, workAddress, address: Name->Addr } {     address : homeAddress + workAddress }
Alloy 4		sig Book {     homeAddress, workAddress, address: Name->Addr } {     address in homeAddress + workAddress }

Page 123: there was a typo in fun redLights and pred mostlyRed. It should be as follows:

fun LightState::redLights ( ): set Light { this.color.Red }
pred LightState::mostlyRed ( j: Junction ) {
    lone j.lights - this::redLights
}

The syntax above will still work in Alloy4, but the preferred new syntax is:

fun LightState.redLights : set Light { this.color.Red }
pred LightState.mostlyRed [ j: Junction ] {
    lone j.lights - this.redLights
}

Page 130, section 4.7:

Alloy 3		Paths are interpreted with respect to a collection of root directories, given as preferences in the tool.
Alloy 4		If the module is not one of the library module that comes with the Alloy Analyzer, the analyzer will infer the location of the file based on the location of the main file and the module header of the main file.

Page 131:

Alloy 3		open library/graphs sig Person { parents: set Person } pred Acyclic ( ) { library/graphs/Acyclic (parents) }
Alloy 4		open library/graphs as g sig Person { parents: set Person } pred Acyclic ( ) { g/Acyclic [parents] }

Page 133:

The first question When are module aliases useful? should be deleted.

Page 134:

Alloy 3		Int e denotes the integer atom... int e denotes the sum of the integer values... some w => int w = 0
Alloy 4		Int [e] denotes the integer atom... int [e] denotes the sum of the integer values... some w => int [w] = 0

Page 135:

Alloy 3		How are integers scoped in Alloy? In scope specifications... -31 to +31.
Alloy 4		How are integers scoped in Alloy? In scope specifications, a setting for int gives the maximum bit-width for integers. For example, a command that includes the scope     6 int results in a search limited to exactly 64 Int atoms, and involving integers from -32 to +31.

Page 135:

Alloy 3		Is Alloy's Int like Java's Integer? Yes. The distinction... overload the + and - operators.
Alloy 4		Is Alloy's Int like Java's Integer? Yes. The distinction between Int and int in Alloy is very similar to Java's distinction between primitive integer values and Integer objects.

Page 136:

Alloy 3		{all i, j: Int | int i = int j => i = j }
Alloy 4		{all i, j: Int | int [i] = int [j] => i = j }

Page 164:

The book says "you'll get a compilation error telling you that the scope of 2 is too low".
In Alloy4, we will raise the scope to 3 automatically, and display a warning message (if message verbosity is medium or high).

Page 187, near the top, and one more time near the bottom:

Alloy 3		Room<:keys : Room lone->Key
Alloy 4		Room<:keys in Room lone->Key

Page 199: there was a typo in sig Entry. It should be as follows:

sig Entry extends RoomKeyEvent { } {
    key in guest.keys.pre
    let ck = room.currentKey |
        (key = ck.pre and ck.post = ck.pre) or
        (key = nextKey[ck.pre, room.keys] and ck.post = key)
    currentKey.post = currentKey.pre ++ room->key
    }

Page 231: there was a typo in the ReformulateNonEmptinessOK assertion:

Old		assert ReformulateNonEmptinessOK {   all r: univ->univ |     some r iff (some x, y: univ | x->y)   }
New		assert ReformulateNonEmptinessOK {   all r: univ->univ |     some r iff (some x, y: univ | x->y in r)   }

Pages 253..294:

Appendix B and C are based on Alloy 3.
Please refer to the Alloy 4 quick guide on the Alloy website for the detailed list of changes.