Home Articles

指定合金中关系的属性

Asked
Viewed 790 times
1

我试图在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 Answer

  • 3

    要指定给定关系的域是单例的事实,您的第一次尝试真的很接近 . 唯一的问题是 one ~r 强制r关系的倒数(因而r关系本身)由单个元组组成 . 这不是你想要表达的 . 你想要表达的是,r关系范围内的所有元素通过其反比关系具有相同的(因此只有一个)图像 . 因此,您应该编写以下谓词:

    pred SingletonDomain(r: univ->univ) {
       one univ.~r
    }
    

    对于您的第二个问题,您的谓词不处理案例 e -> e' -> e '' -> e. 要处理这些案例,您可以使用传递闭包 .

Related