Die Suche ergab 681 Treffer

von yourmaninamsterdam
28. Jun 2013 22:53
Forum: Archiv
Thema: Exc10 Scala Option
Antworten: 3
Zugriffe: 529

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...
von yourmaninamsterdam
3. Apr 2013 02:04
Forum: Archiv
Thema: Mutual Exclusion
Antworten: 1
Zugriffe: 380

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...
von yourmaninamsterdam
30. Mär 2013 14:26
Forum: Archiv
Thema: Liveness -> Warum wird das verifiziert?
Antworten: 5
Zugriffe: 722

Re: Liveness -> Warum wird das verifiziert?

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:

Code: Alles auswählen

./pan -a
von yourmaninamsterdam
29. Mär 2013 14:57
Forum: Archiv
Thema: Liveness -> Warum wird das verifiziert?
Antworten: 5
Zugriffe: 722

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.
von yourmaninamsterdam
27. Mär 2013 16:58
Forum: Archiv
Thema: Keine Gleichverteilung bei select?
Antworten: 3
Zugriffe: 400

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...
von yourmaninamsterdam
20. Feb 2013 17:34
Forum: Archiv
Thema: Lab4 - Probleme mit HighscoreSorted Invariante und insertAt
Antworten: 11
Zugriffe: 529

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...
von yourmaninamsterdam
6. Feb 2013 15:27
Forum: Archiv
Thema: Frage zur Kalkülerstellung (KeY)
Antworten: 1
Zugriffe: 130

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...
von yourmaninamsterdam
9. Jan 2013 16:27
Forum: Archiv
Thema: Lab 3 - Sequenzenkalkül
Antworten: 9
Zugriffe: 840

Re: Lab 3 - Sequenzenkalkül

"Valid" heißt "allgemeingültig". Erfüllbarkeit heißt auf Englisch "satisfiability".
von yourmaninamsterdam
19. Dez 2012 18:09
Forum: Archiv
Thema: Sprechstunden/Übungen vom 12. - 21.12
Antworten: 1
Zugriffe: 220

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.
von yourmaninamsterdam
13. Dez 2012 13:47
Forum: Archiv
Thema: Frage zur Temporallogik
Antworten: 5
Zugriffe: 583

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'
von yourmaninamsterdam
13. Dez 2012 10:58
Forum: Archiv
Thema: Frage zur Temporallogik
Antworten: 5
Zugriffe: 583

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...
von yourmaninamsterdam
12. Dez 2012 14:54
Forum: Archiv
Thema: Verifizierung von claims
Antworten: 8
Zugriffe: 871

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?
von yourmaninamsterdam
11. Dez 2012 16:39
Forum: Archiv
Thema: Verifizierung von claims
Antworten: 8
Zugriffe: 871

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,...
von yourmaninamsterdam
9. Dez 2012 20:39
Forum: Archiv
Thema: Lab2 Task 5
Antworten: 12
Zugriffe: 981

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 ...

Zur erweiterten Suche