合金分析仪 - 仅自然数 - 无整数集

Question

有没有办法像 Alloy 中的 Int 那样声明自然数？

目前我有

util/integer

，如果我运行

run 6 Int

，我会得到：

integers={-32, -31, -30, -29, -28, -27, -26, -25, -24, -23, -22, -21, -20, -19, -18, -17, -16, -15, -14, -13, -12, -11, -10, -9, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31}

我想要的是

util/naturals

和

3 Natural

导致：

naturals={0, 1, 2, 3, 4, 5, 6, 7, 8,...}

而不是：

natural/Natural={natural/Natural$0, natural/Natural$1, natural/Natural$2...}

Answer 1

我会在 Alloy 4.2 中这样做

let Natural = {i : Int | i>=0}


sig A{

 a: disj Natural
}

run {} for 3 Int 

注意在设置中开启“防止溢出”