【发布时间】：2014-12-04 23:59:45
【问题描述】：
在Alloy book (Software Abstractions)第132页，据说下面的命令是一个完整的合金模型：
check {all p,q: univ -> univ, s: set S | (p.s).q = p.(s.q)}
我把这个放到合金工具上执行，但是合金抱怨S。这是书中的错误吗？
【问题讨论】：
标签： alloy
【发布时间】：2014-12-04 23:59:45
【问题描述】：
看起来确实如此。如果将 'S' 替换为 'univ'，则表达式有意义，Analyzer 会接受该模型。
【讨论】：