这个 Alloy 代码有什么问题？

Question

我收到以下代码的语法错误消息。该消息指定了 addLocal 断言中的标记位置，声明： "Syntax error at line 30 column 9: There are 1 possible tokens that can appear here: )" 我只是看不出这里有什么问题。

abstract sig Target{}

sig Addr extends Target{}
sig Name extends Target{}

sig Book
{
    addr: Name->Target
}

pred add(b, b1:Book, n:Name, t:Target)
{
    b1.addr = b.addr + (n->t)
}

fun lookup (b: Book, n: Name): set Addr 
{
    n.^(b.addr) & Addr
}

assert addLocal 
{
    all 
        b,b1:Book, 
        n,n1:Name, 
        t:Target |
            add(b, b1, n, t) and n != n1 => lookup(b, n1) = lookup(b1, n1)
            //   |- error position   
}

Answer 1

由于我一直不太明白的原因，在某些时候 Alloy 的语法从使用（或允许）围绕谓词和函数的参数的括号更改为需要方括号。所以addLocal的相关行需要重新标点：

    add[b, b1, n, t] and n != n1 => lookup[b, n1] = lookup[b1, n1]

我脑子里的语法不够牢固，无法确定，但快速浏览一下 软件抽象 的附录 B 中的语法表明括号可以包含谓词声明中的参数，但不在谓词引用中；在表达式位置，括号总是包含一个表达式，这可以解释为什么解析器在遇到参数列表中的第一个逗号时停止。

这个 Alloy 代码有什么问题？

What's wrong with this Alloy code?

alloy