Alloy 6.1.0中参数名加单引号（'）报错的原因及解决

问题场景 #

在Windows 10系统上运行Alloy 6.1.0，跟随《Software Abstractions》一书“Whirlwind Tour”2.2节示例编写代码时，出现指向变量名单引号的语法错误。

原代码 #

module tour/addressBook1

sig Name, Addr {}
sig Book {
  addr: Name -> lone Addr
}

pred show (b: Book) {
#b.addr >1
#Name.(b.addr) > 1
}

pred add (b,b': Book, n: Name, a: Addr) {
b'.addr = b.addr + n -> a
}

run add for 3 but 2 Book

错误信息 #

Syntax error at line 13 column 14:
There are 3 possible tokens that can appear here:
, : =

问题原因 #

Alloy 6.x版本对标识符的语法规则进行了更新：旧版本允许将单引号(')作为变量名的一部分（比如b'），但在6.x中，单引号已被用作特殊语法符号（例如用于字段否定、字符串转义等场景），不再支持直接作为变量名的后缀。

解决办法 #

将带单引号的变量名替换为符合新版本语法的合法标识符，比如用b_prime、bNext这类命名方式替代b'。

修改后的代码 #

module tour/addressBook1

sig Name, Addr {}
sig Book {
  addr: Name -> lone Addr
}

pred show (b: Book) {
#b.addr >1
#Name.(b.addr) > 1
}

pred add (b, b_prime: Book, n: Name, a: Addr) {
b_prime.addr = b.addr + n -> a
}

run add for 3 but 2 Book

内容的提问来源于stack exchange，提问作者Asterion Daedalus