alloy

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
Solution

  • 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