Merge branch 'main' of github.com:unibas-marcelluethi/software-engine…

…ering

docs/exercises/alloy.md

@@ -0,0 +1,96 @@
+---
+layout: default
+title : Alloy
+---
+
+# Modellieren mit Alloy
+
+
+## Aufgabe 1
+
+Erstellen Sie ein Alloy-Modell des unten beschriebenen Systems:
+
+- Es gibt Bachelor-Studenten und Master-Studenten, kein Student ist gleichzeitig Bachelor- und Master-Student;
+- ein Student muss sich an einer Universität einschreiben, und nur eingeschriebene Studenten sind legale Studenten;
+- jeder Student hat eine eindeutige Studenten-ID und genau ein Hauptfach;
+- Studenten mit demselben Hauptfach, die an derselben Universität eingeschrieben sind, gelten als Kommilitonen; ein Student kann mehrere Kommilitonen haben;
+- Bachelor- und Master-Studenten sind niemals Kommilitonen;
+- die Kommilitonen-Beziehung ist nicht reflexiv (ein Student kann nicht sein/ihr eigener Kommilitone sein).
+
+Versuchen Sie sich grob an folgendem UML-Diagramm zu orientieren:
+![UML](./images/student_class_diag.svg)
+
+
+## Aufgabe 2
+
+*(Exercise A.3.3 auf Seite 243 von Software Abstractions von Daniel Jackson)*
+
+Betrachten Sie die Menge aller Mengen, die sich selbst nicht als Element enthalten. Enthält sie sich selbst?
+
+In dieser Übung werden Sie ein kleines Modell ändern, das auf Russells berühmter Variation dieses Problems basiert – dem Barbier-Paradoxon: In einem Dorf, in dem der Barbier jeden Mann rasiert, der sich nicht selbst rasiert, wer rasiert den Barbier?
+
+1. Verwenden Sie den Analyzer, um zu zeigen, dass das Modell tatsächlich inkonsistent ist, zumindest für Dörfer kleiner Größe.
+2. Einige Experten haben darauf hingewiesen, dass das Paradoxon verschwindet, wenn die Existenz von Frauen anerkannt wird. Erstellen Sie eine neue Version des Modells, die die Dorfbewohner in Männer (die rasiert werden müssen) und Frauen (die das nicht müssen) einteilt, und zeigen Sie, dass es nun eine Lösung gibt.
+3. Eine drastischere Lösung, die Edsger Dijkstra vorgeschlagen hat, besteht darin, die Möglichkeit zuzulassen, dass es keinen Barbier gibt. Ändern Sie das ursprüngliche Modell entsprechend und zeigen Sie, dass es nun eine Lösung gibt.
+4. Erstellen Sie schließlich eine Variante des ursprünglichen Modells, die mehrere Barbiere erlaubt. Zeigen Sie, dass es wieder eine Lösung gibt./
+
+Nutzen Sie dazu folgende Code als Startpunkt: 
+
+```alloy
+sig Man {shaves: set Man}
+
+one sig Barber extends Man {}
+
+fact {
+   Barber.shaves = {m: Man | m not in m.shaves}
+}
+
+run { }
+```
+
+## Aufgabe 3
+
+
+*(Exercise A.3.1 auf Seite 243 von Software Abstractions von Daniel Jackson)*
+
+
+Ein Lied von Doris Day hat folgenden Text:
+
+> Everybody loves my baby but my baby don’t love nobody but me
+
+Von einem strikt logischen Standpunkt aus bedeutet dies „Ich bin mein Baby“.
+
+Überprüfen Sie dies indem Sie das Lied mittels Constraints ausdrücken und eine entsprechende Assertion schreiben. 
+
+Modifizieren Sie dann die Constraints, um auszudrücken, was Doris Day wahrscheinlich gemeint hat, und zeigen Sie, dass die Assertion nun ein Gegenbeispiel hat.
+
+Nutzen Sie dazu folgenden Code als Startpunkt:
+```alloy
+
+sig Person {
+  loves: set Person
+}
+
+one sig Me extends Person {}
+```
+
+
+### Aufgabe 4
+
+# Traffic Lights
+
+Schreiben Sie ein dynamisches Modell für Ampeln in Alloy.
+
+Die Ampeln sollten die folgenden Eigenschaften haben:
+
+- Jede Ampel kann die Farben $\text{Rot}$, $\text{Grün}$ und $\text{Gelb}$ anzeigen.
+- Alle Ampeln beginnen mit ${\text{Rot}}$.
+- Zu jedem Zeitpunkt kann eine Ampel unverändert bleiben oder einen der folgenden Übergänge machen:
+    - ${\text{Rot}} \rightarrow {\text{Rot}, \text{Gelb}}$,
+    - ${\text{Rot}, \text{Gelb}} \rightarrow {\text{Grün}}$,
+    - ${\text{Grün}} \rightarrow {\text{Gelb}}$,
+    - ${\text{Gelb}} \rightarrow {\text{Rot}}$.
+- Zu jedem Zeitpunkt darf nur eine Ampel etwas anderes als ${\text{Rot}}$ anzeigen.
+- Jede Ampel muss irgendwann ein grünes Licht gezeigt haben.
+
+Simulieren Sie Ihr Modell für mindestens 2 Ampeln. Funktioniert es auch für mehr?

docs/week10/index.md

@@ -36,7 +36,7 @@ Die Studierenden
 
 ## Übungen
 
-Versuchen Sie die Aufgaben im [Alloy Übungsblatt](../exercises/alloy-static) zu lösen. 
+Versuchen Sie die Aufgaben im [Alloy Übungsblatt](../exercises/alloy) zu lösen. 
 
 - Das Übungsblatt muss nicht abgegeben werden. 
 - Wir werden die Übungen in der letzten Übungsstunde am 17. Dezember besprechen.

docs/week11/index.md

@@ -3,40 +3,46 @@ layout: default
 title : Woche 11
 ---
 
-# Woche 11: Softwareprozesse
+# Woche 11: Modellieren mit Alloy (II)
 
 ## Übersicht
 
-In dieser Woche schauen wir uns an, wie man die verschiedenen Aktivitäten und Phasen
-des Softwareengineering organisiert. Wir besprechen dabei traditionelle Softwareprozessmodelle
-und geben auch eine Einführung in Agile Softwareentwicklungsmethoden.
+In dieser Woche werden wir das Modellierungswerkzeug Alloy vertiefen. Insbesondere werden wir 
+sehen, wie wir dynamische Modelle in Alloy erstellen können. Zudem werden wir anhand von 
+Anwendungsbeispielen sehen, wie wir Alloy für die Modellierung von Software Systemen einsetzen können.
 
-## Theorie
+## Lernziele 
 
-####  Vorbereitung (zu bearbeiten bis 28. November)
+Die Studierenden
 
-* Schritt 1: Softwareprozesse ([Video](https://unibas.cloud.panopto.eu/Panopto/Pages/Viewer.aspx?id=412f9e91-dde8-467a-b3b6-b07c008935ca), [Slides](./slides/Prozesse.pdf))
-* Schritt 2: Lesen Sie den Artikel: Agile Softwareentwicklung  ([Artikel](./agile))
-* Schritt 3: Lesen Sie das Kapitel "Agile!: The Good, the Hype and the Ugly"  ([Artikel](./agile-critic.html))
-* Schritt 4: Bearbeiten Sie den Selbsttest für Woche 11 ([auf Adam)](https://adam.unibas.ch/goto_adam_tst_1646918.html)).
+- kennen die Zeitoperatoren von Alloy und können damit einfache temporale Eigenschaften modellieren.
+- kennen die Grundlegende Strategie um dynamische Modelle in Alloy zu erstellen.
+- können den Visualizer einsetzen um dynamische Aspekte von Modellen zu verstehen.
+- können einfache dymamische Modelle in Alloy erstellen und analysieren.
 
-## Übungsstunde
 
-Während der Übungsstunde können Sie an Ihrem Projekt arbeiten. Die Tutoren stehen Ihnen unterstützend zur Seite.	
 
-## Hausaufgaben
+## Vorlesungsslides
 
-Die folgenden Aufgaben müssen bis zum 5. Dezember erledigt werden. 
-- Arbeiten Sie den [Selbststudiumsteil Woche 12](../week12/index) durch und bearbeiten Sie die dort angegebenen Aufgaben. 
 
+* Modellieren mit Alloy
+    * Slides (Auf Adam): [pdf](https://adam.unibas.ch/goto_adam_file_1932030_download.html) 
 
-## Lernziele
+## Ressourcen
 
-Die Studierenden
+- [Offizielle Seite für Alloy](http://alloytools.org/)
+- [Alloy Dokumentation](https://alloy.readthedocs.io/en/latest/)
+- [Formal software design with Alloy](https://haslab.github.io/formal-software-design/index.html)
+- [Alloy 6 - It's all about time](https://www.hillelwayne.com/post/alloy6/)
+
+## Übungen
+
+Versuchen Sie die Aufgaben im [Alloy Übungsblatt](../exercises/alloy) zu lösen. 
+
+- Das Übungsblatt muss nicht abgegeben werden. 
+- Wir werden die Übungen in der letzten Übungsstunde am 17. Dezember besprechen.
+- Das bearbeiten der Übungen ist freiwillig. Alloy wird aber ein Teil der Prüfung sein.
 
-- können die Ziele nennen, die man mit einem Softwareprozess erreichen möchte
-- kennen die wichtigsten Softwareprozessmodelle und deren Charakteristika
-- können die Hauptmerkmale von agilen Methodologien erklären
-- können agile Methodologien mit traditionellen Softwareprozessen vergleichen 
-- können und Vor- und Nachteile beider Modelle nennen. 
+## Übungsstunde:
 
+Im Praktischen Teil der Vorlesung werden Sie weiter an Ihrem Projekt arbeiten und die Präsentation vorbereiten.