Das sind Hausaufgaben und ich habe viel Ärger damit. Ich verwende Legierung , um eine Bibliothek zu modellieren. Hier sind die Definitionen der Objekte:
%Vor%Dann müssen wir eine Tatsache haben, die besagt, dass jedes Buch entweder im Regal steht oder von einem Kunden herausgenommen wird. Sie können jedoch nicht an beiden Orten sein.
%Vor%Ich habe das versucht ...
%Vor%Aber es funktioniert nicht ... die Bücher sind immer in den Regalen. möchte sagen: "Für jedes Buch, wenn es nicht ausgeliehen wird, ist es im Regal. Ansonsten ist es out."
Korrekturen, Beispiele und Hinweise werden sehr geschätzt.
Wenn jedes Buch entweder an jemanden oder in den Regalen ausgeliehen werden muss, dann (a) wird kein Buch sowohl ausgeliehen als auch in den Regalen sein (vorausgesetzt, Sie meinen "oder" als exklusiv), also die Schnittmenge der Onloan-Set und das On-Shelf-Set werden leer sein, und (b) das Set von Büchern wird gleich der Vereinigung der Onloan- und On-Shelf-Sets sein.
Die Menge der ausgeliehenen Bücher ist die Domäne der loaned_to -Beziehung. Die Büchergruppe im Regal in einer bestimmten Bibliothek L ist der Wert von L.onshelves ; das Bücherset in den Regalen aller bekannten Bibliotheken ist Library.onshelves .
Sie könnten also sagen
%Vor%Oder Sie müssen vielleicht etwas anderes sagen, je nachdem, was Sie meinen. Beachten Sie, dass diese Einschränkungen nicht sagen, dass ein Buch auf Kredit an einen einzelnen Kreditnehmer ausgeliehen werden muss.
Ok, korrigieren Sie mich, wenn ich falsch liege, aber ich glaube, das ist die Tatsache, die Sie suchen:
%Vor% Und eine kleine Erklärung. Library.on_shelves ist der Satz Bücher auf der rechten Seite der Beziehung on_shelves , d. h. alle Bücher, die in den Regalen stehen. ~loaned_to ist die umgekehrte Beziehung vom Typ Person -> Book und Person.~loaned_to ist die Menge der Bücher, die an irgendeine Person ausgeliehen werden.
Das Prädikat disj erklärt, dass die zwei Mengen keine gemeinsamen Atome haben (disjunkte Mengen).
Ich bin mit Alloy nicht sehr vertraut. Aber ich denke, das oder etwas Ähnliches würde funktionieren.
Jedes Buch ist entweder in den Regalen oder wird einem Patron ausgeliehen.
%Vor%Tags und Links alloy