排序模块中的 pred/totalOrder 是什么？

Question

[更新] 只是为了好玩，我在Alloy中实现了pred/totalOrder。这是：

sig elem {}

one sig Ord {
    First: elem,
    Next: elem -> elem
} {
    no a: elem | (a -> First) in Next   // First is the first atom in the list
    // Constrain Next to be ordered like Next in the ordering module
    (elem <: iden) & Next = (none -> none)   // Constrain Next to be irreflexive
    Next.Next & Next = none -> none  // Constrain Next to be intransitive 
    (Next & ~Next) = none -> none    // Constrain Next to be asymmetric
    Next + ~Next + (elem <: iden) != (elem -> elem)   // Constrain Next to be non-connected
    #(elem.Next) = #Next   // Constrain Next to be injective
    #(Next.elem) = #Next    // Constrain Next to be functional
    #Next = minus[#elem,1]  // Constraint Next to contain all atoms in elem
}

fun first: one elem { Ord.First }
fun next : elem->elem { Ord.Next }
fun last: one elem { elem - (next.elem) }
fun prevs [e: elem]: set elem { e.^(~(Ord.Next)) }
fun nexts [e: elem]: set elem { e.^(Ord.Next) }

pred Show {
    #elem > 2
}

run Show

订购模块有这个：

private one sig Ord {
   First: set elem,
   Next: elem -> elem
} {
   pred/totalOrder[elem,First,Next]
}

什么是pred/totalOrder？它在哪里定义？它有什么作用？我可以在我的 Alloy 模型中使用它吗？

什么是private？它在哪里定义？它有什么作用？我可以在我的 Alloy 模型中使用它吗？

Answer 1

我猜它的含义是硬编码在工具中的，与 fun/sub 和 fun/add 的定义方式相同。

至于为什么我还不清楚。也许是为了优化？

Answer 2

关键字private使签名在调用模块时不可见，并且可以在任何模型中使用。 pred/foo 模型是内置的，不应在用户级模型中使用。

排序模块中的 pred/totalOrder 是什么？

What is pred/totalOrder in the ordering module?

alloy