CODEWITHSUNDEEP
alloy
qartal
qartal

Reputation: 2064

having a check command as a complete model in Alloy

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?

Upvotes: 1

Views: 58

Answers (1)

C. M. Sperberg-McQueen
C. M. Sperberg-McQueen

Reputation: 25034

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

Upvotes: 2

Related Questions