Home Articles

合金:仅定义与正整数的关系

Asked
Viewed 275 times
0

我有一个这个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 Answer

  • 1

    updated 这种子类型工作(imho)最好用set枚举:

    let PositiveInt = { i : Int | i > 0 }
     sig Thing {}
     sig World { quantities : Thing -> one PositiveInt }
    
    ┌──────────┬──────────┐
    │this/World│quantities│
    ├──────────┼──────┬───┤
    │World⁰    │Thing⁰│7  │
    │          ├──────┼───┤
    │          │Thing¹│6  │
    │          ├──────┼───┤
    │          │Thing²│4  │
    └──────────┴──────┴───┘
    

Related