Alloy

Unterpunkte dieser Seite

Installation von Alloy unter Ubuntu
Der Editor von Alloy
Aufbau eines Alloy Modells
Signaturen
Operationen auf Signaturen
Operationen auf Relationen
Operationen auf Mengen
Einschränkungen bzw. Fakten
Funktionen
Prädikate
Assertions
Schlüsselwörter in Alloy 3.0
Relationen und Atome - wie Alloy arbeitet
Der Alloybefehl run
univ

Installation von Alloy unter Ubuntu

Da alloy mit Java programmiert ist, muss auf dem System ein Java Runtime Environment installiert sein. Von der Alloy Homepage http://alloy.mit.edu/ kann man den Alloy Analyzer in der Beta Version 3.0 herunterladen. Im Download Bereich gibt es ein zip-file für GNU Linux. Nachdem man das zip-file heruntergeladen hat, erzeugt man als root im Verzeichnis /usr/share ein Verzeichnis namens alloy und entpackt den Inhalt der zip-file in dieses Verzeichnis.

sudo file-roller /home/bischowg/Download/applications/alloy-i386-linux.zip

Das Programm lässt sich nun mit dem Befehl

java -jar alloy.jar

starten.
Der Tutor hat gesagt, das das erste, was man mit Alloy tun sollte, ist denn Erfüllbarkeitstester für logische Formeln umzustellen. Alloy bringt gleich vier Stück mit. Im Menupunkt File > Preferences auf dem Reiter Main sollte man den SAT-Solver auf ZChaff einstellen.

Der Editor von Alloy

Vielleicht habe nur ich das Problem, aber auf meinem Linux kann ich kein Dach-Zeichen in den Editor von Alloy eingeben. Ein weiteres Problem ist, dass die Tilde die ich im Editor erzeugen kann einen Syntax-Fehler produziert. Daher muss ich das Dach und das Tilde-Zeichen in einem anderen Editor eintippen, kopieren und in den Alloy Editor einfügen. Die gute Nachricht ist, dass Alloy diese beiden Zeichen dann tatsächlich akzeptiert und sich die Alloy Syntax damit formulieren und übersetzen lässt. ^~

Aufbau eines Alloy Modells

Ein Modell wird in einer Datei mit der Endung .als gespeichert. Jedes Modell befindet sich in einem Modul. Dieses Modul muss am Anfang einer .als-Datei deklariert werden. Der Name der .als-Datei sollte gleich dem Modulnamen gewählt werden.

module modulname

Kommentare sind einzeilig und werden mit zwei backslashes begonnen.

// Dies ist ein Kommentar.

Nach der Moduldeklaration folgen die Deklarationen der Signaturen (sig), Fakten. Es ist egal in welcher Reihenfolge man diese Konstrukte in die .als-Datei schreibt. Alloy ist deskriptiv und nicht imperativ. Es interpretiert die gesamte Menge an gegebenen Konstrukten egal in welcher Reihenfolge sie angegeben sind.

Signaturen

Signaturen sind die syntaktischen Konstrukte von Alloy mit denen man Mengen innerhalb des Universums, also Basic Types und Relationen auf diesen Basic Datatypes definiert. Innerhalb des Körpers einer Signatur werden die sogenannten Fields einer Signatur definiert. Die Fields werden verwendet um Relationen zu definieren. Die Relationen in den Fields besitzen implizit immer als erstes Element eines Tupels, ein Atom vom Basic Type der Signatur, in der sie deklariert worden sind.

Signaturen werden mit dem Schlüsselwort sig gebildet und erhalten einen Namen. Hinter dem Namen folgt der Körper der Signatur, der in geschweifte Klammern eingefügt ist. Innerhalb des Körpers werden Relationen deklariert, die sich wie die Attribute einer Klasse verhalten. Signaturen selber sind Mengen von Objekten. Die Relationen, die man in Signaturen deklariert, sind Relationen zwischen einem Objekt vom Typ der Signatur und einem Objekt des Typs den man in der Deklaration der Relation angegeben hat.

Man kann eine Signatur von einer anderen ableiten. Dazu verwendet man das extends Schlüsselwort, das nach dem Namen einer Signatur angewendet wird. Hinter extends schreibt man den Namen der Signatur von der abgeleitet werden soll. Ableitung bedeutet, folgendes. Wenn die Signaturen S2 und S3 von der Signatur S1 abgeleitet sind, so sind S2 und S3 disjunkte Teilmengen von S1 und alles was mit S1 getan werden kann, kann auch mit S2 und S3 getan werden. Es wird durch das Ableiten allerdings nicht ausgesagt, das S2 und S3 eine Partition von S1 bilden, es könnte auch noch ein S4 geben, das aus S1 abgeleitet ist. Um Partitionen zu erstellen muss ein extra Fakt eingeführt werden. Der obige Satz ist falsch. In dem Onlinetutorial zu alloy kann man nachlesen, das durch das extends Schlüsselwort eine Partition erzeugt wird. In dem Onlinetutorial kann man auch nachlesen, das durch ein extend zwar disjunkte Mengen gebildet werden, aber diese Mengen nicht alle Elemente der Obermenge enthalten müssen. Ich weiß nicht, was richtig und was falsch ist ! Möchte man erreichen, das durch subtypen keine Partition gebildet wird, so verwendet man statt extends einfach das Schlüsselwort in.

Signaturen können direkt nach ihrem Körper noch mal einen Bereich enthalten, der von geschweiften Klammern umgeben ist. Dieser Bereich wird appended fact Bereich genannt. In diesen appended fact bereich lassen sich facts unterbringen, die immer für diese Signatur gelten sollen.

Operationen auf Signaturen

Signaturen sind Mengen von Objekten. Operationen auf Signaturen sind daher Operationen auf Mengen. Die Operation + ist die Mengenvereinigung.

Operationen auf Relationen

.* - Reflexive-Transitive-Hülle. Wenn man sich ein Relation als Graph vorstellt, dann ist die reflexive transitive Hülle, der enstehende Graph indem eine Kante von jedem Knoten zu sich selbst ausgebildet ist (=transitiv) und von jedem Knoten eine Kante zu den Knoten die sich über einen Pfad erreichen lassen (=transitiv)

.^ - Transitive-Hülle. Gleich wie Reflexive-Transitive-Hülle bloß ohne reflexivität. (allerdings kann ein Knoten immer noch eine Kante zu sich selbst haben, nämlich genau dann, wenn es einen Pfad über andere Knoten gibt, der wieder bei ihm selbst endet.

-> - relational product operator. Der -> Operator ist überladen für Relationen und speziel auf für Skalare und Mengen. Wenn man ihn auf zwei Skalare Alice = {(ALICE)} und Bob = {(BOB)} anwendet, so erhält man ein Tupel (Alice, Bob). Wenn man ihn auf zwei Mengen anwedet, so wird das kartesische Produkt der beiden Mengen gebildet. D.h. alle Möglichen Tupel aus den Elementen der Mengen werden aufgebaut, wobei die Reihenfolge eine Rolle spielt. Wenn man den Operator auf Relationen anwendet, so werden alle Tupel in der angegebenen Reihenfolge zu neuen Tupeln in allen möglichen Kombinationen kombiniert und es ensteht dadurch eine neue Relation. Sei p eine Realtion und sei q ein Relation. Wenn p das Tupel (p_1,...,p_n) und q das Tupel (q_1,...,q_m) enthält, dann enthält p -> q das Tupel (p_1,...,p_n,q_1,...,q_m). Links und rechts des -> Operator können Multiplizitäten stehen (lone, one, some, gar nichts). Eine Signatur kann in ihrem Körper ein Attribut enthalten, das den relational product operator enthält. Ein relational product operator erzeugt ternäre Relationen. Die Signatur, die das Attribut mit dem Operator enthält, wird abgebildet auf eine binäre Relation aus den beiden Objekten, die links und rechts des Operators stehen.

~ - Inverse einer Relation, die Paare werden einfach alle umgedreht.

Operationen auf Mengen

Relationen sind Mengen von Tupeln, damit lassen sich die folgenden Operatoren auf Relationen anwenden. Skalare sind unäre Relationen, die nur genau ein Tupel enthalten. Ein Skalar ist also eine spezielle Menge. Der Inhalt dieses Kaptiels hätte auch im Kapitel Operationen auf Relationen untergebracht werden können. & - Schnitt zweier Mengen. Der Schnitt enthält ausschließlich die Elemente, die in beiden Mengen enthalten sind. + - Vereinigung zweier Mengen. Die Vereinigung enthält alle Elemente beider Mengen. Wenn man zwei skalare addiert, so entsteht kein skalar mehr sondern eine Menge. Mit dem Plus Operator kann man einer Menge bzw. Relation auch ein neues Tupel hinzufügen. Bsp.: Gegeben sei die binäre Realtion likes und die beiden Atome Alice und Bob. Mit Alice -> Bob wird das Tupel (Alice, Bob) beschrieben. Mit likes + Alice -> Bob wird das Tupel (Alice, Bob) der Menge likes hinzugefügt. - - Mengendifferenz A - B ist die Menge A aus der alle Elemente enfernt worden sind, die auch in B enthalten waren. in - Untermenge/Teilmenge. Falls A in B wahr ist, so ist A eine Untermenge von B, enthält also eine Auswahl an Elementen, die in B enthalten sind. = - Mengengleichheit. A = B ist wahr genau dann wenn A die gleichen Elemente enthält wie B und umgekehrt. none - die leere Menge. Die leere Menge enthält kein einziges Element. iden - die Identische binäre Relation. In der Identischen binären Relation sind nur Paare der Form (a,a) enthalten. Also steht in der identischen Relation jedes Element ausschließlich in Relation zu sich selbst.

Einschränkungen bzw. Fakten

Mit dem Schlüsselwort fact werden Fakten deklariert, die in einem Modell immer gelten müssen. Alloy erzeugt nur Beispielmodelle, die allen angegebenen Fakten entsprechen.

Funktionen

Fakten gelten immer, Funktionen nur unter bestimmten Umständen. Funktionen geben einen Wert zurück. (Dieser Wert ist kein Wahrheitswert wahr oder falsch. Prädikate geben wahr oder falsch zurück, Funktionen geben einen Wert zurück.) Funktionen werden mit dem Schlüsselwort fun deklariert.

Prädikate

Fakten gelten immer, Prädikate nur unter bestimmten Umständen. Prädikate werden mit dem Schlüsselwort pred deklariert. Prädikate werden zu einem Wahrheitswert (= wahr oder falsch) ausgewertet.

Assertions

Mit Fakten stellt man sicher, das jedes Beispiel das Alloy darstellt, diesen Fakten entspricht. Wenn man eine Menge von Fakten formuliert hat, so ergeben sich neben diesen Fakten oft noch weitere Fakten, die immer gelten, obwohl man sie nicht explizit formuliert hat.
Wenn man davon überzeugt ist, dass eine solche Folgerung existiert, kann man testen ob man richtig gedacht hat, indem man eine Assertion formuliert, die genau die eigene Vermutung ausdrückt und diese Assertion mit dem check Schlüsselwort testen lässt. Alloy sucht Gegenbeispiele und sagt, ob es Gegenbeispiele finden konnte oder nicht.
Es ist immer besser eine Folgerung zu provozieren, als den gleichen Effekt durch ein Fakt zu erzwingen.
Bis zu einer bestimmten Grenze findet Alloy, bewiesenermaßen, alle Gegenbeispiele. Die Suche der Gegenbeispiele kann also als Korrektheitsbeweis bis zu einer bestimmten Grenze herangezogen werden.

// The contents path is acyclic
assert acyclic {
  no d: Dir | d in d.^contents
}

check acyclic for 5

Schlüsselwörter in Alloy 3.0

Schlüsselwort	Bedeutung
abstract	Eine abstrakte Signatur enthält nur die Atome, die auch in den von ihr abgeleiteten Signaturen vorhanden sind.
all	All-Quantor
assertion
check	Eine Assertion lässt sich mit dem Befehl check testen
extends	Signature können voneinander abgeleitet werden
fact	Fact, Fakten müssen in Modellen gelten
for	Suche nach Beispielen beschränken
in	Teilmenge
let	Wie ein define in C, wird einfach ersetzt
lone	one or less, eines oder gar keines
module	definiert ein Modell in einer .als-Datei
no
one	Genau eines. Von dieser Signatur gibt es nur genau ein Objekt
pred	Prädikat
run	Alloy Befehl, der versucht eine Lösung des Modells zu finden (Keine Gegenbeispiele)
set	Eine Menge kann kein Element, ein Element oder mehrere Elemente enthalten.
sig	Signature, definiert eine Menge von Objekten

Relationen und Atome - wie Alloy arbeitet

Grundbaussteine

In Alloy besteht alles aus Atomen und Relationen. Der Benutzer von Alloy kann allerdings nur auf Relationen arbeiten, da die Atome intern verwaltet werden.

Atome

Atome sind unteilbar, unveränderlich und zustandslos. Atome können nicht aufgeteilt werden, da sie nicht aus noch kleineren Elementen aufgebaut sind. Atome sind unveränderlich. Wenn man sie erzeugt bleiben sie so wie man sie erzeugt hat. Atome sind zustandslos. Sie bestehen nicht aus Attributen, die sich ändern könnten und sind selbst unveränderlich, wodurch sie genau einen Zustand anzeigen können und damit für eine Zustandsmenge völlig unbrauchbar sind.

Atome werden syntaktisch in Alloy durch ??? deklariert.

Das Universum

Das Universum ist eine endliche Menge, die alle Atome eines Modells enthält. Das Universum ist in disjunkte Teilmengen partitioniert. Diese Teilmengen bilden die Basisdatentypen. z.B. Tag = {Montag, Dienstag, Mittwoch, Donnerstag, Freitag, Samstag, Sonntag} und Personen = {Franz, Klaus, Jong}. Auf derm Universum sind die Relationen ausgebildet.

Relationen

Relationen sind Konstrukte die Atome miteinander in Beziehung setzen. Relationen sind wie Relationen aus der Mathematik realisiert. Relationen sind Mengen. Die Elemente die in der Menge enthalten sind, sind Tupel. Tupel bestehen aus einem, zwei, drei oder mehr Atomen (Tupel sind also ein Liste von Atomen). Eine Relation enthält ausschließlich Tupel mit gleicher Anzahl an Atomen darin. Es gibt also keine Relation die Tupel mit zwei oder drei Atomen besitzt. Alle Tupel einer Relation haben alle genau n Atome. Die Menge der Atome in einem Tupel wird als die Arität einer Relation bezeichnet. Die Anordnung der Atome in einem Tupel ist wichtig. Das Tupel, das das Atom A vor dem Atom B enthält, unterscheidet sich von dem Tupel das zuerst B und dann A enthält. Neben der Reihenfolge und der Anzahl der Atome muss in einer Relation auf der Basisdatentyp, also die Teilmenge des Universums, für jede Stelle des Tupels angegeben werden. Wenn man z.B. ein Relation mit Tupeln vom Typ (Person, Tag) hat, so muss an erster Stelle ein Atom aus der Menge Person und an zweiter Stelle ein Atom aus der Menge Tag stehen. Relationen müssen sozusagen typisiert sein.

Relationen werden syntaktisch in Alloy durch ??? deklariert.

Mengen und Skalare

Eine Menge wird auf der logischen Ebene von Alloy durch eine unäre Relation ausgedrückt, also eine Relation, die nur Tupel enthält, die ein einziges Atom enthalten. Zum Beispiel Tag = {(Montag), (Dienstag), (Mittwoch), (Donnerstag), (Freitag), (Samstag), (Sonntag)}
Ein Skalar wird auf der logischen Ebene von Alloy durch eine unäre Relation dargestellt, die nur genau ein Tupel enthält. Bsp.: Alice = {(ALICE)}
Eine Menge A wird als Atom dargestellt. Die Elemente, die in der Menge enthalten sind, werden alle als einzelne Atome dargestellt. Es gibt dann eine Relation der Arität 2, die ausdrückt welche Elemente in der Menge A sind, indem sie A als erstes Element des Tupels verwendet und alle enthaltenen Element an die zweite Position in die Tupel einsetzt.

Signaturen

Signaturen sind nur syntaktische Konstrukte. Eine Signatur deklariert eine Menge, also ein Atom mit einer Relation, die alle enthaltenen Elemente beschreibt. Im Körper einer Relation kann allerdings nicht nur eine solche Relation definiert werden sondern gleich mehrere. Bsp.:

sig Mensch {
  ehegatte: lone Mensch,
  kind: set Mensch
}

Die obige Signatur erzeugt das Atom Mensch, das zwei Relationen ausbildet nämlich ehegatte und kind. Es werden also auch gleich zwei Mengen definiert, nämlich die Menge aller Ehegatten von Mensch und die Menge aller Kinder von Mensch.

Die join-Operation auf Mengen

Der Alloybefehl run

Der run Befehl veranlasst Alloy eine Instanz zu suchen, die die Wahrheit eines Prädikates in Kombination mit allen angegebenen Signaturen und Fakten aufzeigt. Falls das Prädikat oder die Formel in verbindung mit dem Rest nicht wahr sein kann spuckt Alloy aus, dass es keine Instanz gibt. Alloy sucht nicht unendlich lange, man muss Alloy eine Grenze angeben. Die Grenze bezieht sich hierbei auf die Anzahl der Signaturen, die in einer Instanz verwendet werden sollen. Wenn man z.B. die Signaturen A und B angegeben hat, so kann man folgendes formulieren:

pred example() {}
run example for exactly 4 A, exactly 2 B

Das leere Prädikat ist per Definition immer wahr, es wird also faktisch nur der Rest der Alloy .als-Datei auf eine erfüllende Instanz untersucht.
Man muss eine Grenze fuer alle Signaturen der Datei angeben. Bei vielen Signaturen ist das mühsam man kann daher folgendes schreiben:

univ

univ ist der Obertyp aller Atome.

zum Seitenanfang
zur Hauptseite

Letzte Änderung: 24.05.2006