Model-checking environment for state-transition systems (aka. Mist)

erneute Transplantation des Quell-Repositoriums (13. Sept. 2000): neuer Ort: swprakt@aristoteles.informatik.uni-kiel.de:/home/swprakt/cvsroot
Mist-Endbesprechung : 20. Juli 2000, 10 Uhr, Preußerstr. 1-9
Schließung der Accounts im GA-Pool: 24. Juli 2000

Entwurfs & Prototypphase (für 8stündige Teilnehmer)

Dieser erste Teil ist für die 8stündigen Gruppen gedacht. In einer ersten Phase eines Projektes geht es um den Entwurf und hier bereits einen Prototypen, d.h., einen ersten, teillauffähiges Programm, mit Hilfe dessen man einschätzen kann, wie umfangreich man das Endprodukt gestalten will, welche Features es haben soll, welche man besser wegläßt etc. Es ist in diesem Teil möglich, daß sich je 2 2er-Gruppen zu einer Vierer-Arbeitsgemeinschaft zusammentun um Arbeit zu sparen. Die Initiative muß aber von Euch ausgehen, wir teilen das nicht zwingend ein. (bei Bedarf: ich habe alle Mailadressen). Wenn man sich unter der Woche nicht trifft, kann man in der ersten Woche die Planung machen, was man sich vorstellt, dann in der nächsten Woche sich mit einer 2ten Gruppe abgleichen und besprechen, und die zweite Woche auf die Realisierung verwenden.

Hier die genauere Beschreibung des Prototyps.

Pflichtenheft

Folgende Liste enthält das Pflichtenheft. Die erste Eintrag ist jeweils der aktuelle.

5.	Pflichtenheft 5	Typen hinzugefügt, nach der Projektbesprechung am 10. Juli
4.	Pflichtenheft 4	kleine Anpassungen nach der Besprechung vom 27. Juni.
3.	Pflichtenheft 3	Positionen in Zuständern, Änderung der Klasse `Process`.
2.	Pflichtenheft 2	geringe Änderungen an der abstrakten Syntax, Einteilung der Teams
1.	orig. Version, 22. Mai

Baselines

Die Baselines sind hier zur schnelleren Referenz als Javaarchiv mist_v[x].jar festgehalten, wobei [x] die Nummber der Baseline ist). Als Entwickler mit Zugriff auf das Quellcoderepositorium kann man die Entwicklungsschritte sie natürlich mittels cvs wieder zurückholen. Zum Ausführen der Archivs speichere man die Datei mist_v[x].jar an einen geeigneten Platz, und setze export CLASSPATH=[geeigneter_platz]/mist_v[x].jar

4.	Endbesprechung	20. Juli, nach der Endbesprechung
3.	Baseline 3 unwesentliche Fortschritte	17. Juli, vormittags
2.	Baseline 2 keine wesentlichen Fortschritte in der Gesamtintegration	10. Juli, vormittags
1.	Baseline 1 (gif-Bilder noch nicht richtig referenziert im Archiv, Grund: unbekannt)	5. Juli.

HTML-Dokumentation

Zur schnelleren Orientierung wird die mit javadoc dokumentierte Implementierung im Netz bereitgestellt. Die Seiten werden bei größeren Entwicklungsschritten aufgefrischt.

Dokumentation Mist: Stand: 28. Juli, morgens

Arbeitsgruppen

Jede der Arbeitsgruppen bearbeitet i.d.R. ein Java-Paket. Die Beschreibung der Aufgabenstellung findet sich im Pflichtenheft.

1.	Gui	Helge Kraas/ Broder Schümann	unix22
2.	Editor	Finn Jacobs/ Alexander Eckloff	unix18
3.	Model-Checker	Frank Neumann/Aneta Kümper/Eike Schulz	unix19
4.	Parser	Andreas Scott/Alexander Hegegner	unix??
5.1	Graphlazierung	Daniel Dietrich/Moritz Zahorsky/ Christian Buck	unix25
5.2	Graphlazierung	Ralf Thöhle/Paul Mallach	unix11
6.1	Checking	André Nitsche
6.2	[Checking]	[Jonas Dageförde/Andreas Lukosch]	unix11
7	Utilities: Pretty-Printer	Oliver Kraus, Holger Labenda

Die Mailadressen der Teilnehmner finden sich intern unter

[Arbeitsverzeichnis]/Mist/src/Org/gruppen.txt

Das Repositorium

Vorraussetzungen

Man benötigt zwei Dinge, um von Ferne auf das gemeinsame Repositorium zugreifen zu können:

ssh (secure shell) als sicherer Zugriff und
cvs + rcs als Versionskontrolle

Für den ersten Punkt bzw. ssh: so geht man vor: Den ssh-Schlüssel an unix01@ap.informatik.uni-kiel.de mailen. Der Schlüssel liegt typischerweise unter ~/.ssh/identity.pub, wer ihn bereits hat, soll mir dieses File schicken. Wer einen solchen Schlüssel nicht hat, muß ihn sich generieren und zwar mittels ssh-keygen Für das das korrekte Funktionieren braucht man noch Folgendes (bash-Syntax):

export CVSROOT=unix01@gimli.ap.informatik.uni-kiel.de:/home/unix01/cvsroot export CVS_RSH=ssh export CVSEDITOR=emacsclient export CLASSPATH=[workingdirectory]/Mist/src:

wobei [workingdirectory] ein Platzhalter für das Verzeichnis ist, in dem man arbeiten will. Die ersten drei Zeilen sind zum korrekten Steuern von cvs gedacht. (man kann cvs auch anders steuern, z.B. über .cvsrc, bei Bedarf bitte selbst im Manual nachschlagen). Anstelle emacs kann man auch emacsclient oder den editor seiner Wahl nehmen. emacsclient sollte man dann nehmen, wenn man ohnehin emacs verwendet und beim starten des emacs' ein (server-start) ausgeführt wird. Die letzte Zeile hat mit ssh/cvs nichts zu tun, sondern hat mit dem Java-Projekt selbst zu tun.

Beispiel

Im Beispiel findet alles im Verzeichnis ~/Projekt statt, d.h. [workingdirectory] = ~/Projekt).

Auschecken: So bekommt man zum ersten Mal seine Arbeitskopie des Mist-Projektes:
cd ~ mkdir Projekt cd Projekt cvs checkout Mist/src
Macht man
cvs checkout Mist/Org
bekommt man die Gruppeneinteilung. Macht man nur
cvs checkout Mist
so bekommt man alles zum Mist-Projekt, einschließlich der Quellen des Pflichtenheftes und der Web-seite.
Zurückspeichern: Wenn man mit den Änderungen durch ist, kann man den gesamten Verzeichnisbaum zurückspeichern:
cd [workingdirectory]/Mist cvs commit
Danach wird man aufgefordert, einen Kommentar bezüglich seiner Änderungen anzugeben. Falls der Kommentar nur kurz ist, kann man schneller auch
cvs commit -m"Anmerkungen zu den Änderungen"
verwenden.
Updaten: Den Baum seines Arbeitsverzeichnisses auf den neuesten Stand bringen, geht auf zweierlei Weise:
cd [workingdirectory]/Mist cvs update
oder
cd [workingdirectory] cvs checkout Mist
mit den Variante, wie oben geschildert. Man beachte den Unterschied der Verzeichnisse bei beiden Varianten! Das checkout geht weiter als ein bloßes Update, da es einem auch neu hinzugekommene Verzeichnisse gibt.
Neue Dateien + Verzeichnisse: Das geht mit
cvs add [filename]
entfernen mit cvs remove [filename]. Anstelle eines Filenames kann man auch ein Verzeichnis hinzufügen, oder auch alle neuen java-files mit cvs add *.java.

Strategie und Spielregeln

Versionskontrolle garantiert kein reibungsloses Arbeiten, es unterstützt dies, wenn man gewisse Disziplin wahrt. Folgende Daumenregeln:

Änderen von globalen Paketen/Paketen von anderen Gruppen: nur nach reiflicher Überlegung/Rücksprache mit der betroffenen Gruppe.
Nur kompilierbare Versionen einchecken, d.h. der eigene Teil muß mittel make all ohne Fehlermeldungen sich kompilieren lassen (dies gilt noch nicht für die Anlaufphase, bis es zum ersten Mal integriert ist). Änderung, die die Schnittstelle mit einem anderen Pakte betreffen (insbesondere mit der GUI) sollten angekündigt werden, zum Beispiel in den Besprechungen. Daneben sind die Mailadressen der einzelnen Gruppen unter Org/gruppen.txt vorhanden.
Makefiles und Readmes sind hilfreich (im Paket absynt finden sich Beispiele)
bitte den Code sinnvoll mittels Javadoc kommentieren. Zumindest der Author/die Autoren soll dokumentiert sein. In Paket absynt kann man sich anschauen, wie man, wenn man will, auch cvs-logs documentieren lassen kann (z.B. in dem man das File absynt/template.txt verwendet/anpaßt.)

Information zu im Kurs verwendeter Software

Die primären Information finden sich auf der Startseite des Kurses. Weitere für die Projektarbeit wichtige Links hier:

Lexer und Yaccer:
- JLex, CLASSPATH muß /home/unix01/jlex: (im A-Pool) enthalten!
- CUP, CLASSPATH muß /home/unix01/cup: (im A-Pool) enthalten!
  Beachte: zum kompilieren daheim: bitte die neueste Version cup1.0k installieren!
Concurrent version control: die Verwendung von CVS ist im zweiten Teil für alle verpflichtend! Eine gute, lokale Informationsquelle sind die Info-Seiten im emacs.
- CVS
- eine Referenzliste, eine gute Kurzeinführung
Informationen zu gnu make (und weitere gnu-software hier, beides ist wiederum auch innerhalb des Info-Systems des Emacs zugänglich)

Bei Fragen, email an {mky|kst|ms}@informatik.uni-kiel.de

Maintained by: Martin Steffen

Last modified: Wed Sep 13 14:54:51 MET DST 2000