合金:关于Int的事实等

Question

我最近在Alloy工作。我能不能这样说:

fact{
all i: Int | i >= 0 
}

我想说:Alloy使用的所有Integer都应该是正的。Alloy不会失败，但也不会给我实例。

问候

Answer 1

你现在不能这么说。你可以为整数指定的唯一作用域(它告诉Alloy要"使用"哪个整数)是位宽(例如，4 Int);然后Alloy总是使用该位宽内的所有整数(例如，对于位宽为4，使用的整数是-8, ..., 7)。

如果你的模型中有一个Int类型的字段，你可以使用一个事实(就像上面所说的)来限制它的值:

sig S { i: Int }
fact  { all s: S | s.i >= 0 }