No Instance Found on integer declaration greater than 7

Question

I'm trying to model a problem that about some girls on the pool. There are some premises that must be followed.

• Maiô: amarelo, azul, branco, verde
• Nome: Ana, Bruna, Raquel, Vivian
• Idade: 8, 9, 10, 11
• Suco: laranja, limão, maracujá, morango
• Protetor: FPS 40, FPS 45, FPS 50, FPS 55
• Animal: cachorros, gatos, pássaros, peixes

I'm having trouble building facts using numerical values. Is there any limitation on Interger usage?

I'm trying to model a problem that about some girls on the pool. So far i have the following bunch of code, just some signatures:

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
}

There are only four girls and they must be between 8 and 11 years old. So, i created the following fact:

    #Menina = 4
    // Position
    pos in Menina one -> one (1 + 2 + 3 + 4)
    // Age
    idade in Menina one -> one (8 + 9 + 10 + 11) // Don't Work!! 

When I put the age fact, I can't found any instance.

The same problem happens when I put a fact about the sunscreen (protetor). It can be between 40, 45, 50 or 55. If I put a fact about that, No instance found!

What's the issue with the integer usage?

Answer 1

The use of integers is severely restricted in Alloy.

• By default you only have 16 integers. So >7 or <-8 won't work,
• Math is done by functions like 6.plus[5]
• The - and + operators are set operators
• Handling of overflow is an option, if overflow happens:
  • no solution, or
  • modulo arithmetic
• Increasing the number of integers can be done with the run or check commands: run for 6 but 6 int. In this case the 6 int will refer to 6 bits or 64 integers evenly spread out.

The reason numbers are so crippled in Alloy is that the use of SAT solvers to create an instance encodes the integers as a bitmap. This does scale awfully so that models that use larger integers quickly take forever to solve. Daniel Jackson in his book calls this out explicitly. His recommendation is to not use integers to encode concepts. For example if you have the sunscreen factor, make a sig SunscreenFactor and make sure to order it.

This limitation is one of the major drawbacks of Alloy. First, we're used to so many examples where we use integers as cheap stand-ins, second almost all problems need list like behavior and lists are also limited by the available integers.

That said, looking at your code you seem to lack a basic understanding of how you make Alloy models. Of course reading Daniels book or some of the online tutorials might help. What I nowadays find very helpful is to use ChatGPT to construct a model. It still gets it surprisingly wrong quite often but a lot of the beginners stuff it gets right.