D120.de/forum

Note that the Option type implements map and foreach that are executed only if the Option is-a Some. Using that, you can get rid of a lot if if-else/match code. Also, if you have Lists of Option, you can use flatten to remove all appearances of None and get all Somes. Here are the examples: scala> v...

Meiner Meinung nach sind diese Variablen nicht als Semaphoren, sondern in diesem ersten Ansatz von MutEx eher als Zustandsvariablen der Prozesse gemeint, die dann genutzt werden, den wechselseitigen Ausschluss zu implementieren. Du siehst in den Folien also die Evolution von "die Prozesse machen, wa...

Du verstehst das völlig richtig.

null hat geschrieben: spin -a ltlverification.pml
gcc -o pan pan.c
./pan -N liveness

Du musst bei der Verifikation "acceptance cycles" aktivieren, um die Liveness-Eigenschaft zu prüfen:

Die Frage ist: Was verifizierst du denn? Das Programm verstößt ja beispielsweise auch nicht gegen Assertions (mangels Assertions) und der Deadlock ist dank des end-Labels zulässig.

Wichtig wäre jetzt nur noch zu wissen ob select, obwohl diese nicht richtig funktioniert in der Klausur als nicht-deterministischer Zufallsgenerator angenommen werden darf!? Wer hat denn gesagt, dass select nicht funktioniert? Es erzeugt lediglich keine Gleichverteilung. Für die Verifikation des Mo...

Ich glaube, mmi1991 hat dich schon richtig verstanden. Um EnsuresPost für eine Methode zu beweisen brauchst du doch die Nachbedingung einer Schleife. Wenn du die Invariante da auf true setzt, mag das nie false sein, es generiert aber auch keine sinnvolle Nachbedingung, die für den Rest der Methode v...

KeY gibt die Semantik des Inkrement-Operators wieder: Der Ausdruck x++ bedeutet: erhöhe den Wert einer Variable x um 1 und gib den ursprünglichen/alten Wert zurück. Wenn das jetzt Teil einer Zuweisung ist, wird anschließend zugewiesen. Das macht KeY: Sich den Wert merken, damit er später zurückgegeb...

"Valid" heißt "allgemeingültig". Erfüllbarkeit heißt auf Englisch "satisfiability".

Für die Leute, die letzte Woche nicht in meiner Übung waren, hier nochmal der Hinweis: meine Sprechstunde findet morgen (am 20.12.2012) um 8:00 Uhr in Raum S113/118 nicht statt.

Du musst pan mit '-a' aufrufen. Die Ausgabe sagt dir das auch ganz oben, wenn du es nicht tust. "Technischer" Hinweis: Spin akzeptiert nicht das aneinanderketten von Parameter, man muss also schreiben './pan -a -f'. Es geht nicht: './pan -af'

Problem 3 in Übung 3 ist recht vage gehalten, in sofern würde ich nicht zu viel Hirnschmalz in das Suchen einer "perfekten" Lösung investieren. Dienen Ansatz verstehe ich allerdings nicht so ganz. Es gibt ja den Request, ein Acknowledgement und den Progress des Prozesses. Das sind schon recht unters...

Ich habe den Verdacht, dass das okay und normal ist, dass der Endzustand im Claim nicht erreicht wird. Kann irgendwer das bestätigen oder widerlegen?

Kann es sein, dass spin ltl-Blöcke erst in Never-Claims umschreibt, die dann auch in eventuellen Fehlermeldungen auftauchen (und nicht die LTLs). Sieht hier aber tatsächlich so aus, als sei irgendwas in deiner LTL generell unzutreffend (daher "unreached"). Prüf mal die Semantik von Programm und LTL,...

Die Vergleichen-Frage verstehe ich nicht. Der Intruder kann nicht mit Daten vergleichen, die er nicht kennt. Er kann mit Daten vergleichen, die er kennt. Er kann nicht Inhalte einer Nachricht lesen, wenn sie mit einem fremden geheimen Schlüssel verschlüsselt ist. Er kann die Inhalte von Nachrichten ...