Я попробовал следующий фрагмент Alloy4 и обнаружил, что меня смущает поведение модуля util/Natural. Комментарии объясняют более подробно, что было неожиданным. Я надеялся, что кто-то может объяснить, почему это происходит.
module weirdNatural
private open util/natural as nat
//Somehow, using number two obtained from incrementing one works as I expect, (ie, there is no
//number greater than it in {0,1,2}. but using number two obtained from the natrual/add function
//seems to work differently. why is that?
let twoViaAdd = nat/add[nat/One, nat/One]
let twoViaInc = nat/inc[nat/One]
pred biggerAdd {
some x: nat/Natural | nat/gt[x, twoViaAdd]
}
pred biggerInc {
some y: nat/Natural | nat/gt[y, twoViaInc]
}
//run biggerAdd for 10 but 3 Natural //does not work well, it does find a number gt2 in {0,1,2}
run biggerInc for 10 but 3 Natural //works as expected, it finds a number gt2 in {0,1,2,3}, but not in {0,1,2}
