Alloy中如何实现支持谓词多态的模块？

Alloy原生模块参数仅支持签名（sig）类型，无法直接传入谓词作为参数，结合Alloy的关系语义，有两种可落地的实现方式，都能通过原生类型检查：

方案1：用集合/关系模拟谓词参数（推荐，轻量无冗余） #

Alloy中谓词的本质是「所有满足谓词约束的参数元组构成的集合/关系」：一元谓词对应目标类型的子集，多元谓词对应对应阶数的多元关系，直接把这个关系作为模块参数传入即可。
示例模块定义：

// predAParam为sigA的子集，对应所有满足predA谓词的sigA元素
module mymodule[sigA, predAParam]
sig B extends sigA {}

pred predB[b : B] {
  // 此处编写B类型相关的固定谓词逻辑
  // ...
}

// 原约束逻辑直接通过集合判断实现
fact { all b : B | b in predAParam => predB[b] }

实例化模块时，只需要提前定义好对应谓词的外延集合，直接作为参数传入即可：

// 定义具体业务签名
sig ConcreteSigA {
  score: Int
}

// 定义自定义predA的逻辑：所有score大于0的ConcreteSigA元素
fun customPredA: set ConcreteSigA {
  {s: ConcreteSigA | s.score > 0}
}

// 传入自定义谓词对应的集合完成模块实例化
open mymodule[ConcreteSigA, customPredA]

如果需要传入多参数谓词，只需要把参数替换为对应阶数的关系即可，比如二元谓词就传入sigA->sigB类型的二元关系，判断逻辑改为(a,b) in predAParam即可。

方案2：用单例签名封装谓词（适合复杂约束场景） #

如果谓词需要关联多组逻辑、或者附带额外约束，可以用抽象单例签名封装谓词接口，实例化时替换单例的实现逻辑。
示例模块定义：

module mymodule[sigA, PredA]
// 定义谓词容器的抽象签名，约束为单例
abstract sig PredA {
  check: sigA -> lone Bool
}
one sig DefaultPredA extends PredA {}

sig B extends sigA {}
pred predB[b : B] {
  // B的固定谓词逻辑
  // ...
}

fact {
  all b : B | DefaultPredA.check[b] = True => predB[b]
}

实例化时只需要扩展对应单例签名，写入自定义的谓词判定逻辑：

open mymodule[ConcreteSigA, MyCustomPred]
one sig MyCustomPred extends PredA {}
fact {
  all s: ConcreteSigA | MyCustomPred.check[s] = True <=> s.score > 0
}

两种方案都完全符合Alloy的语法规则，不会触发类型检查错误，日常使用优先选第一种轻量方案即可。

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