Die Suche ergab 681 Treffer
- 28. Jun 2013 22:53
- Forum: Archiv
- Thema: Exc10 Scala Option
- Antworten: 3
- Zugriffe: 634
Re: Exc10 Scala Option
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...
- 3. Apr 2013 02:04
- Forum: Archiv
- Thema: Mutual Exclusion
- Antworten: 1
- Zugriffe: 459
Re: Mutual Exclusion
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...
- 1. Apr 2013 21:21
- Forum: Archiv
- Thema: Exercise 6 - Partial Correctness vs. total correctness
- Antworten: 1
- Zugriffe: 390
Re: Exercise 6 - Partial Correctness vs. total correctness
Du verstehst das völlig richtig.
- 30. Mär 2013 14:26
- Forum: Archiv
- Thema: Liveness -> Warum wird das verifiziert?
- Antworten: 5
- Zugriffe: 847
Re: Liveness -> Warum wird das verifiziert?
Du musst bei der Verifikation "acceptance cycles" aktivieren, um die Liveness-Eigenschaft zu prüfen:null hat geschrieben: spin -a ltlverification.pml
gcc -o pan pan.c
./pan -N liveness
Code: Alles auswählen
./pan -a
- 29. Mär 2013 14:57
- Forum: Archiv
- Thema: Liveness -> Warum wird das verifiziert?
- Antworten: 5
- Zugriffe: 847
Re: Liveness -> Warum wird das verifiziert?
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.
- 27. Mär 2013 16:58
- Forum: Archiv
- Thema: Keine Gleichverteilung bei select?
- Antworten: 3
- Zugriffe: 507
Re: Keine Gleichverteilung bei select?
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...
- 20. Feb 2013 17:34
- Forum: Archiv
- Thema: Lab4 - Probleme mit HighscoreSorted Invariante und insertAt
- Antworten: 11
- Zugriffe: 759
Re: Lab4 - Probleme mit HighscoreSorted Invariante und inser
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...
- 6. Feb 2013 15:27
- Forum: Archiv
- Thema: Frage zur Kalkülerstellung (KeY)
- Antworten: 1
- Zugriffe: 155
Re: Frage zur Kalkülerstellung (KeY)
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...
- 9. Jan 2013 16:27
- Forum: Archiv
- Thema: Lab 3 - Sequenzenkalkül
- Antworten: 9
- Zugriffe: 1075
Re: Lab 3 - Sequenzenkalkül
"Valid" heißt "allgemeingültig". Erfüllbarkeit heißt auf Englisch "satisfiability".
- 19. Dez 2012 18:09
- Forum: Archiv
- Thema: Sprechstunden/Übungen vom 12. - 21.12
- Antworten: 1
- Zugriffe: 248
Re: Sprechstunden/Übungen vom 12. - 21.12
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.
- 13. Dez 2012 13:47
- Forum: Archiv
- Thema: Frage zur Temporallogik
- Antworten: 5
- Zugriffe: 729
Re: Frage zur Temporallogik
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'
- 13. Dez 2012 10:58
- Forum: Archiv
- Thema: Frage zur Temporallogik
- Antworten: 5
- Zugriffe: 729
Re: Frage zur Temporallogik
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...
- 12. Dez 2012 14:54
- Forum: Archiv
- Thema: Verifizierung von claims
- Antworten: 8
- Zugriffe: 1064
Re: Verifizierung von claims
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?
- 11. Dez 2012 16:39
- Forum: Archiv
- Thema: Verifizierung von claims
- Antworten: 8
- Zugriffe: 1064
Re: Verifizierung von claims
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,...
- 9. Dez 2012 20:39
- Forum: Archiv
- Thema: Lab2 Task 5
- Antworten: 12
- Zugriffe: 1258
Re: Lab2 Task 5
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 ...