处理多重关系( arity ~10)

Question

我有一个模型，它有一个类似于这个的sig：

sig State {
  ps: set P,
  cs: set C,
  o: set C -> set P,
  m: set M
}

像这样的谓词，处理两个State：

pred my_pred [s, s': State] {
  ...
}

我正在尝试创建我的模型的参数化版本，其中我没有State签名，而是在函数和谓词中显式地传递这些字段。这意味着谓词看起来像这样

pred my_pred [(M -> P -> C -> (C -> P)) ->
              (M -> P -> C -> (C -> P))] {
  ...
}

我的问题是，如何轻松地处理相对较大的数量关系，比如my_pred中的关系？例如，我试图使用util/relation中的dom，但dom是在二元关系上定义的，不幸的是，似乎合金看到了这一点

  (M -> P -> C -> (C -> P))
  ->
  (M -> P -> C -> (C -> P))

作为一个10而不是2的关系；这意味着忽略括号。因此，使用dom将返回M类型的内容，而不是所需类型的(M -> P -> C -> (C -> P))。

还有一个相关的问题，我想知道是否/如何在这样的关系上使用传递闭包运算符。

Answer 1

通常情况下，数量关系大于3是不好的做法。

为什么不简单地声明谓词，如下所示：

pred my_pred [m,m':M , ps,ps':P , cs,cs':C , o,o':(C -> P)] {
  ...
}