合金：定义关系只正整数(Alloy: define relation to only positiv

我有这个签名的模型：

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

我想定义的约束quantities关系，使得每一件事情的数量必须是正INT。

我与合金总初学者（我没有理论背景上绘制，只是一个Python程序员）。 我也跟着通过教程，但我没有看到什么我希望做一个配方。

我知道如何：

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

......但我不清楚如何写一个事实时需要解决的关系，右手边的成员。

我已经将它定义为一种关系（而不是一个quantity上的财产Thing SIG），因为我从教程了解，这是必要的，在这里我想通过谓词更新的东西的量的动态模型。

我试着定义：

sig PositiveInt extends Int {}

......但是这是不允许的。

Answer 1:

更新这种亚型的作品（恕我直言）最好组枚举的：

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

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

文章来源: Alloy: define relation to only positive integers