integer - 合金:关于 Int 的事实等

Question

我最近在与 Alloy 合作。
我可以这样说吗:

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

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

你好

Answer 1

你目前不能这么说。您可以为整数指定的唯一范围(告诉 Alloy 要“使用”哪些整数)是位宽(例如， 4 Int )；然后，Alloy 始终使用该位宽内的所有整数(例如，对于 4 位宽，使用的整数是 -8, ..., 7 )。

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

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