Сплав: определить отношение только к положительным целым числам

Question

У меня есть модель с этим сигналом:

sig Thing {}
sig World {
    quantities: Thing ->one Int,
}

Я хочу определить ограничение для отношения quantities так, чтобы количество каждой вещи было положительным целым числом.

Я абсолютный новичок в Alloy (и у меня нет теоретических знаний, я просто программист на Python).Я прошел весь урок, но не нашел рецепт того, что хочу сделать.

Я знаю, как:

fact {
    all w: World | w.quantities <something>
}

... но мне не ясно, как обратитьсячлены правой стороны отношения при написании факта.

Я определил его как отношение (а не свойство quantity на сигнатуре Thing), потому что я понял изУчебник, что это было необходимо в динамической модели, где я хочу обновить количество вещей с помощью предикатов.

Я попытался определить:

sig PositiveInt extends Int {}

... но это не разрешено.

Answer 1

обновлено Этот вид подтипа работает (imho) лучше всего с заданным перечислением:

 let PositiveInt = { i : Int | i > 0 }
 sig Thing {}
 sig World { quantities : Thing -> one PositiveInt }

┌──────────┬──────────┐
│this/World│quantities│
├──────────┼──────┬───┤
│World⁰    │Thing⁰│7  │
│          ├──────┼───┤
│          │Thing¹│6  │
│          ├──────┼───┤
│          │Thing²│4  │
└──────────┴──────┴───┘