Alloy建模中整数取值大于7时出现No Instance Found问题求助

建模场景前提 #

• 泳衣：黄色、蓝色、白色、绿色
• 名字：Ana、Bruna、Raquel、Vivian
• 年龄：8、9、10、11
• 果汁：橙子、柠檬、百香果、草莓
• 防晒霜：FPS 40、FPS 45、FPS 50、FPS 55
• 喜爱动物：狗、猫、鸟、鱼

已实现的签名代码 #

abstract sig Maio{} 
one sig maio_amarelo, maio_azul, maio_branco, maio_verde extends Maio{}

abstract sig Nome{}
one sig nome_ana, nome_bruna, nome_raquel, nome_vivian extends Nome{}

abstract sig Suco{}
one sig suco_laranja, suco_limao, suco_maracuja, suco_morango extends Suco{}

abstract sig Animal{}
one sig cachorros, gatos, passaros, peixes extends Animal{}

sig Menina{
    maio: one Maio,
    nome: one Nome,
    suco: one Suco,
    animal: one Animal, 
    protetor: Int,
    idade: Int,
    pos: Int
}

遇到的问题 #

我添加了以下Fact约束场景：

#Menina = 4
// 位置约束
pos in Menina one -> one (1 + 2 + 3 + 4)
// 年龄约束——此处无法生效！
idade in Menina one -> one (8 + 9 + 10 + 11)

添加年龄约束后，Alloy提示「No Instance Found」；给防晒霜设置40、45、50、55的取值范围时，也会出现同样问题。

问题原因与解决办法 #

核心问题：Alloy默认Int的范围限制 #

Alloy默认使用3位有符号整数，数值范围是-4到3。你用到的8、9、10、11以及40、45等数值全超出了这个默认范围，所以找不到符合条件的实例。另外，1 + 2 + 3 + 4这种写法是算术运算，结果是10，不是你想要的集合{1,2,3,4}，这也是错误点之一。

三种解决途径 #

1. 扩展整数位宽
   在模型最开头添加代码，扩大Int的取值范围：

// 覆盖8-11用5位足够（范围-16到15），覆盖40-55需要7位（范围-64到63）
set bitwidth = 7;

同时修正集合写法，把(1+2+3+4)改成{1,2,3,4}，年龄约束改成：

idade in Menina one -> one {8,9,10,11}

2. 改用枚举类型（推荐）
   对于年龄、防晒霜这类固定离散值，像泳衣、名字一样用枚举定义，完全规避整数范围问题，也更贴合Alloy的建模逻辑：

// 新增年龄枚举
abstract sig Idade{}
one sig idade_8, idade_9, idade_10, idade_11 extends Idade{}

// 新增防晒霜枚举
abstract sig Protetor{}
one sig protetor_40, protetor_45, protetor_50, protetor_55 extends Protetor{}

// 修改Menina签名
sig Menina{
    maio: one Maio,
    nome: one Nome,
    suco: one Suco,
    animal: one Animal, 
    protetor: one Protetor,
    idade: one Idade,
    pos: Int
}

然后Fact里直接用：

idade in Menina one -> one Idade
protetor in Menina one -> one Protetor

3. 仅修正集合写法（但仍需扩展位宽）
   如果一定要用Int，除了扩展bitwidth，必须把整数集合的写法改成{x,y,z,...}，而不是用加号相加。比如位置约束正确写法是：

pos in Menina one -> one {1,2,3,4}

内容的提问来源于stack exchange，提问作者George Victor