合金：事實等等關於詮釋

Question

我最近與合金工作。 我可以這樣說：

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

我想說：所有整數合金的用途應該是積極的。 合金不失敗，但也不給我實例。

問候

Answer 1

你目前不能說這個。你可以指定整數的唯一範圍（告訴Alloy整數是「使用」）是位寬（例如4 Int）;合金總是使用該位寬內的所有整數（例如，對於4的位寬，使用的整數是-8, ..., 7）。

如果你在你的模型int類型的字段，可以使用一個事實（像你上面說的）來限制它的值：

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