Die Suche ergab 271 Treffer

von dschneid
14. Nov 2013 10:22
Forum: Type Systems of Programming Languages
Thema: Assignment 4.3, Specification Tests
Antworten: 6
Zugriffe: 667

Assignment 4.3, Specification Tests

Hi,

a group of us have worked on the third exercise of the current assignment. All of us only manage to satisfy only 16 of the 19 specification tests, even though we strongly think our implementations are correct.

Is there anyone else with this problem? Could this be a problem with the tests?
von dschneid
23. Mai 2013 17:14
Forum: Archiv
Thema: ConcurrentModificationException() P3
Antworten: 4
Zugriffe: 383

Re: ConcurrentModificationException() P3

Das kann aber auch auftreten, wenn man durch eine HashSet (eigentlich irgendeine Collection) iteriert und in der Schleife den Inhalt ändert, z.B. bei so was: HashSet<String> set = new HashSet<String>(); // fill set... for (String str : set) { if (str.equals("I want more!") set.add("more"); } Wenn du...
von dschneid
18. Apr 2013 13:27
Forum: Archiv
Thema: Klausur: Wie lief's
Antworten: 12
Zugriffe: 2113

Re: Klausur: Wie lief's

Bild
von dschneid
30. Mär 2013 13:39
Forum: Archiv
Thema: Exercise 1 - Ungenauigkeit?
Antworten: 6
Zugriffe: 631

Re: Exercise 1 - Ungenauigkeit?

LTL-Formeln werden in Büchi-Automaten übersetzt. Wenn wir nur über asserts reden, spielen sie also keine Rolle. Unabhängig davon widerspricht meine Aussage aber der Verwendung von Büchi-Automaten nicht. Der grundsätzliche Ansatz beim Model Checking ist immer derselbe, nämlich in irgendeiner Art und ...
von dschneid
30. Mär 2013 13:14
Forum: Archiv
Thema: Exercise 1 - Ungenauigkeit?
Antworten: 6
Zugriffe: 631

Re: Exercise 1 - Ungenauigkeit?

Bei der Verifikation wird das Modell gar nicht simuliert, sondern (vereinfacht gesprochen) die Menge aller möglichen Zustände aufgespannt und durchgegangen. Auf diese Weise wird jegliches mögliche Verhalten des Modells betrachtet.
von dschneid
30. Mär 2013 13:04
Forum: Archiv
Thema: or_left nachvollziehen
Antworten: 7
Zugriffe: 810

Re: or_left nachvollziehen

Um auf deine erste Frage einzugehen: Man kann sich einen Sequenten ja als Zustand eines Beweises vorstellen, in dem wir alles links des Pfeiles annehmen und eine der Formeln rechts davon beweisen wollen. Wenn man nun \phi \vee \psi annimmt, dann weiß man deswegen noch nicht, ob \phi oder \psi gilt. ...
von dschneid
6. Mär 2013 11:51
Forum: Archiv
Thema: Übung 3 , Aufgabe 2.4
Antworten: 2
Zugriffe: 461

Re: Übung 3 , Aufgabe 2.4

Ja, streng genommen hast du Recht. Du wirst dich aber sicher nicht daran stören, dass ähnliche Ungenauigkeiten in der Klausur nicht zu deinen Lasten gewertet werden. :wink:
von dschneid
5. Mär 2013 16:22
Forum: Archiv
Thema: Menge Tr von Prozessen
Antworten: 3
Zugriffe: 593

Re: Menge Tr von Prozessen

Ich beziehe mich auf die erste Aufgabe auf dem 12. Übungsblatt. Meinst du dann den letzten Lauf: (right, up, right, right) als "Prozess am Ende angekommen", wegen dem Stop? Ja. Allgemeiner: Eine Spur modelliert die Aktionen eines zu Ende durchgelaufenen Prozesses, wenn sie kein Präfix irgendeiner an...
von dschneid
4. Mär 2013 12:45
Forum: Archiv
Thema: Übung 6 Aufgabe 1.2
Antworten: 2
Zugriffe: 582

Re: Übung 6 Aufgabe 1.2

Weil die Regel rwhf angewendet wird, nicht die Regel rwht, die du anscheinend im Kopf hast.

Unabhängig davon sollte dir klar sein, dass die Namen von Zuständen in tatsächlichen Ableitungen nicht immer den Namen, die in den Regeln verwendet werden, entsprechen müssen.
von dschneid
6. Feb 2013 11:13
Forum: Archiv
Thema: rigide Funktionssymbole und Updates
Antworten: 3
Zugriffe: 241

Re: rigide Funktionssymbole

Konstanten werden als Funktionen mit 0 Argumenten aufgefasst. Das wurde im Foliensatz über FO-Logik so eingeführt.
von dschneid
30. Jan 2013 14:13
Forum: Archiv
Thema: Menge Tr von Prozessen
Antworten: 3
Zugriffe: 593

Re: Menge Tr von Prozessen

Die Menge der Spuren eines Prozesses enthält nicht nur die Spuren, die bis zu Ende durchgelaufen sind, sondern (siehe z.B. die aktuelle Übung über Abgeschlossenheit unter Präfixbildung) auch alle Spuren, bei denen der Prozess noch nicht "am Ende angekommen" ist. Daher muss man ein Symbol einführen, ...
von dschneid
13. Dez 2012 19:23
Forum: Archiv
Thema: Aufgabe 8.2.1: "Primitive Berechnungsschritte" und While
Antworten: 1
Zugriffe: 476

Re: Aufgabe 8.2.1: "Primitive Berechnungsschritte" und While

Versuch mal folgenden Denkansatz: Wenn die Bedingung einer Schleife zu true auswertet, dann soll intuitiv gesehen eine neue Iteration der Schleife beginnen. Anders gesprochen: Es wird in die Schleife gesprungen, um den Body der Schleife noch einmal auszuführen. Jetzt kannst du dir überlegen, wie du ...
von dschneid
10. Dez 2012 10:04
Forum: Archiv
Thema: Unterschied von Pan mit oder ohne -a
Antworten: 1
Zugriffe: 205

Re: Unterschied von Pan mit oder ohne -a

Ganz grob gesprochen: Ohne -a werden keine LTL-Formeln betrachtet. Das heißt, wenn du diese Flag weglässt, dann können Modelle verifiziert werden obwohl sie eine angegebene LTL-Formel verletzen.
von dschneid
3. Dez 2012 22:12
Forum: Archiv
Thema: Übung 4 - Aufgabe 2
Antworten: 3
Zugriffe: 545

Re: Übung 4 - Aufgabe 2

Genau.
von dschneid
3. Dez 2012 16:35
Forum: Archiv
Thema: Übung 4 - Aufgabe 2
Antworten: 3
Zugriffe: 545

Re: Übung 4 - Aufgabe 2

Weil an manchen Zuständen nicht für jedes Symbol des Alphabets ein Folgezustand spezifiziert wird. Das ist nur bei NDFAs möglich.

Zur erweiterten Suche