我试图在Alloy中表达关系的某些数学属性，但我不确定我是否有正确的方法，因为我只是一个初学者 . 非常感谢来自专家社区的任何见解！
Specifying the fact that domain of a relation as singleton . 例如以下是一种合理而正确的方法吗？
pred SingletonDomain(r: univ->univ) {
one ~r
}
sig S2 {}
sig S1 {
child: set S2
}
fact {
SingletonDomain [child]
}
或者它应该是类似下面的东西
pred SingletonDomain (r: univ->univ) {
#S2.~r = 1
}
这不是非常模块化的，因为S2的使用对特定签名非常具体 .
Specifying the fact that a relation is a total order. 目前我正在使用以下内容，基本上我正在模拟xor
pred total[r: univ->univ] {
all disj e, e': Event | (e.r = e' and e'.r != e) or (e.r != e' and e'.r = e)
}
谢谢
1 回答
要指定给定关系的域是单例的事实，您的第一次尝试真的很接近 . 唯一的问题是
one ~r强制r关系的倒数（因而r关系本身）由单个元组组成 . 这不是你想要表达的 . 你想要表达的是，r关系范围内的所有元素通过其反比关系具有相同的（因此只有一个）图像 . 因此，您应该编写以下谓词：对于您的第二个问题，您的谓词不处理案例
e -> e' -> e '' -> e.要处理这些案例，您可以使用传递闭包 .