affirmation alliage ne fonctionne pas comme prévu

Question

Voici mon code alliage:

one sig Library { 
    books: set Book, // set of the library's books 
    patrons: set Patron, // set of the library's patrons 
    circulation: Patron lone -> some Book // books in circulation 
} 

// set of books in the Library 
sig Book { 
} 

// set of patrons 
sig Patron { 
    curbooks: set Book // books currently checked out by a patron 
} 

Je veux ajouter une assertion que deux Patron ne peut pas avoir actuellement le même livre. Voici l'affirmation que je suis venu avec:

assert sameBook2Patrons { 
    all disj p, p': Patron | all b: p.curbooks | b not in p'.curbooks 
} 

Alors, quand vérifier l'assertion:

check sameBook2Patrons{} for exactly 2 Book, exactly 2 Patron 

alliage ne trouve aucun contre-exemple. Mais quand j'utilise la commande d'exécution, en alliage me donne beaucoup de contre-exemple:

run{} for exactly 2 Book, exactly 2 Patron 

Aussi, je lis que l'ajout d'un fait avec la négation d'une affirmation valable est censée donner aucune instance. J'ai ajouté que:

fact sameBook2Patrons { 
    not (all disj p, p': Patron | all b: p.curbooks | b not in p'.curbooks) 
} 

Lorsque j'exécute le modèle, Alloy trouve une instance valide.

Qu'est-ce que je fais mal? Je vous remercie.

Answer 1

Vous utilisez la commande de vérification à tort. Pour vérifier l'affirmation sameBook2Patrons vous devriez plutôt utiliser

check sameBook2Patrons for exactly 2 Book, exactly 2 Patron 

i.e., sans accolades. Si vous placez les accolades, l'assertion à vérifier est l'expression à l'intérieur des accolades (dans votre cas, vide, ce qui équivaut à vrai) et sameBook2Patrons est juste le nom de la commande.