CODEWITHSUNDEEP
alloy
Geremia Moretti
Geremia Moretti

Reputation: 53

Problems with Alloy 6

I'm a bit confuse 'cause I really don't know why Alloy Analyzer doesn't find a solution to this simple problem. I just want a unique id for each person ...

abstract sig Person {
id: Int
} {id > 0}

sig Candidato extends Person {
    votiRicevuti: Int
}

sig Elettore extends Person {
    votiDati: set Voto
}

sig Voto {
    votante: Elettore,
    votato: Candidato
}

fact {
    #Candidato > 0
    #Elettore > 0
}

fact {
    all p1, p2: Person |
        p1.id != p2.id
}

    
run {} for 4 but 4 Elettore, 4 Candidato

Upvotes: -1

Views: 51

Answers (1)

Soaib
Soaib

Reputation: 96

You can use id: disj Int to get a unique ID.

Permalink: https://play.formal-methods.net/?check=ALS&p=reflux-casino-dollar-vibes

An Instance

Upvotes: 0

Related Questions