这些“$show”关系的含义是什么？

Question

在下面的简单模型中，一些实例包含标记为“$show_upd”的关系。似乎它们是在 'f1' 中使用 'some' 限定符时创建的。它们分别代表什么？

sig Licence {}

sig UpdateRow { 
    next: lone UpdateRow, 
    licence: one Licence
}

sig UpdateChain { 
    first: one UpdateRow 
}

fact f1 {
    // every licence belongs to one or more updateRows
    all lic: Licence | some upd: UpdateRow | upd.licence = lic
}

pred show {} 
run show

Answer 1

Alloy 分析器以美元符号作为前缀命名 Skolem 常量。更具体地说，Skolem 常量（或 Skolemized 约束的见证）与您正在检查的谓词（在本例中为谓词 show）以及与给定 Skolem 常量（在本例中 some upd: UpdateRow），前缀为美元符号 $.

Skolemization，以及 Alloy 分析器中描述的 Skolemized 约束的见证，在 Alloy quick guide 中简要介绍，在 5.2.2 Skolemization 在《软件抽象》一书中。