我有一个这个sig的模型：
sig Thing {}
sig World {
quantities: Thing ->one Int,
}
我想在 quantities 关系上定义一个约束，这样每个Thing的数量必须是一个正整数 .
我是Alloy的初学者（我没有理论背景可供借鉴，我只是一名Python程序员） . 我按照教程进行了操作，但是我没有看到我想要做的配方 .
我知道如何：
fact {
all w: World | w.quantities <something>
}
......但我不清楚如何在撰写事实时如何处理关系右侧的成员 .
我已经将它定义为一种关系（而不是在 Thing sig上有一个 quantity 属性），因为我从教程中了解到这在动态模型中是必要的，我想通过谓词来更新Things的数量 .
我试着定义一个：
sig PositiveInt extends Int {}
......但这是不允许的 .
1 回答
updated 这种子类型工作（imho）最好用set枚举：