having a check command as a complete model in Alloy

Question

In the Alloy book (Software Abstractions) at page 132, it is said that the following command is a complete alloy model:

check {all p,q: univ -> univ, s: set S | (p.s).q = p.(s.q)}

I put this to alloy tool and execute, but the alloy complains about the S. Is this a mistake in the book?

Answer 1

It does look like it. If one replaces 'S' with 'univ', the expressions make sense and the Analyzer accepts the model.