Wer ist hier der Chef von wem?
Alloy ist eine Sprache, in der man Dinge und ihre Beziehungen als Mengen und Relationen beschreibt, und zugleich ein Werkzeug, das nach Gegenbeispielen sucht. Es zeigt sie als kleine Instanz mit Personen und Pfeilen.
In einer Firma hat jede Person höchstens einen Chef, und niemand ist sein eigener. Folgt daraus, dass es keinen Kreis von Chefs gibt? Alloy antwortet mit einem Kreis aus drei Personen.
Am Ende dieser Lektion
Notiz
Ich kann ein Gegenbeispiel von Alloy aus Personen und Beziehungen lesen.
Schlüsselwörter
| Begriff | Was er bedeutet | Beispiel |
|---|---|---|
| Menge | eine Sammlung gleichartiger Dinge | Mitarbeiter |
| Relation | eine Menge von Paaren, die Beziehungen angeben | chef |
| Fakt (fact) | eine Regel, die im Modell immer gilt | |
| Behauptung (assert) | eine Aussage, die aus den Fakten folgen soll | |
| Instanz | ein kleines Beispiel, das zum Modell passt | |
| Bereich (scope) | die größte Zahl von Dingen, die Alloy durchprobiert | for 4 |
Die Zellen, die Lernende ausfüllen, bleiben in dieser Vorschau leer.
Eine Menge und eine Relation beschreiben die Firma
In Alloy legt sig Mitarbeiter eine Menge von Personen an. Die Relation chef ordnet jeder Person höchstens einen Vorgesetzten zu. lone heißt: keine oder eine.
m.chef ist der Chef von m. ^chef ist die Kette: der Chef, der Chef des Chefs und so weiter. no heißt: keiner.
So liest man die Schreibweise von Alloy
| In Alloy | Bedeutung |
|---|---|
| m.chef | der Chef von m |
| m.^chef | alle Chefs über m, auch die Chefs der Chefs |
| no m: Mitarbeiter | A | für keine Person m gilt A |
| m in m.^chef | m ist sein eigener Chef, über einen Umweg |
Die Zellen, die Lernende ausfüllen, bleiben in dieser Vorschau leer.
Das Modell der Firma in Alloy
sig Mitarbeiter { chef: lone Mitarbeiter }
fact keinSelbstChef { no m: Mitarbeiter | m.chef = m }
assert KeinKreis { no m: Mitarbeiter | m in m.^chef }
check KeinKreis for 4
run Beispiel { some chef } for 3
Mit check sucht Alloy nach einem Gegenbeispiel
Der Befehl check KeinKreis for 4 sucht in allen Firmen mit bis zu 4 Personen nach einem Gegenbeispiel zur Behauptung. Findet er eines, steht in der Ausgabe SAT. Findet er keines, steht dort UNSAT.
run Beispiel sucht dagegen nur irgendeine Firma, die zum Modell passt. Die Befehle unten schreiben das Modell und zeigen beide Ergebnisse.
Einen Ordner anlegen
mkdir -p ~/firmaHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Das Modell schreiben
printf '%s\n' 'sig Mitarbeiter { chef: lone Mitarbeiter }' 'fact keinSelbstChef { no m: Mitarbeiter | m.chef = m }' 'assert KeinKreis { no m: Mitarbeiter | m in m.^chef }' 'check KeinKreis for 4' 'run Beispiel { some chef } for 3' > ~/firma/firma.alsHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Gibt es ein Gegenbeispiel?
alloy ~/firma/firma.als | grep -E "check +KeinKreis" | grep -o -w -E "UNSAT|SAT"Hier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Die Chef-Pfeile der gefundenen Instanzen
alloy ~/firma/firma.als | grep "^this/Mitarbeiter<:chef"Hier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Ein Pfeil heißt: hat als Chef
Jede Zeile des letzten Befehls ist eine Instanz. Mitarbeiter$0->Mitarbeiter$2 heißt: Person 0 hat Person 2 als Chef.
Die erste Zeile gehört zu run Beispiel, eine einfache Firma. Die zweite gehört zu check KeinKreis: Ihre Pfeile laufen im Kreis. Jede Person hat einen Chef, und trotzdem ist keine ganz oben.
Ein häufiger Fehler
Warnung
Viele denken: Findet check kein Gegenbeispiel, gilt die Aussage für jede Firma. Alloy sucht nur bis zur Größe im Befehl, hier 4 Personen. Ein Gegenbeispiel mit mehr Personen ist möglich, nur meist selten.
Eine Reparatur ist ein neuer Fakt
Die Firma braucht eine Regel, die Kreise verbietet. Sie wird ein Fakt: no m: Mitarbeiter | m in m.^chef. Die Behauptung wird zum Fakt, und eine andere Aussage, die daraus folgt, wird geprüft.
Prüfen Sie auch, dass das Modell noch Firmen zulässt. Ein Modell ohne Personen hat keine Gegenbeispiele und beweist daher nichts.
Das reparierte Modell schreiben
printf '%s\n' 'sig Mitarbeiter { chef: lone Mitarbeiter }' 'fact keinKreis { no m: Mitarbeiter | m in m.^chef }' 'assert KeinSelbstChef { no m: Mitarbeiter | m.chef = m }' 'check KeinSelbstChef for 4' 'run Beispiel { some chef } for 3' > ~/firma/firma2.alsHier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Gibt es jetzt ein Gegenbeispiel?
alloy ~/firma/firma2.als | grep -E "check +KeinSelbstChef" | grep -o -w -E "UNSAT|SAT"Hier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Gibt es noch eine passende Firma?
alloy ~/firma/firma2.als | grep -E "run +Beispiel" | grep -o -w -E "UNSAT|SAT"Hier angezeigt, nicht ausgeführt. Erstellen Sie ein kostenloses Konto, um „Ausführen“ zu drücken und ihn im Terminal Ihres eigenen Labs einzugeben.
Weiterführend
Das Lab hat einen eigenen Teil mit Alloy und einem Modell, das eine Behauptung verletzt. Lesen Sie dort das Gegenbeispiel, bevor Sie etwas ändern.
Schreiben Sie für Ihr eigenes Modell zwei Behauptungen, eine, die aus den Fakten folgt, und eine, die es nicht tut. Prüfen Sie beide mit check.