Die Suche ergab 187 Treffer

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

Re: Exercise 1 - Ungenauigkeit?

Der Nichtdeterminismus ist hier entscheidend. Es könnte ja jedes Arrayelement gewählt werden, sodass dies der for Schleife entspricht. Prüft SPIN dann alle Array-Komponenten (indem das Do mehrfach für die Verifikation ausgeführt wird) oder gibt es sich zufrieden, dass es eines gefunden hat, für das...
von barracuda317
30. Mär 2013 12:52
Forum: Archiv
Thema: Exercise 1 - Ungenauigkeit?
Antworten: 6
Zugriffe: 631

Exercise 1 - Ungenauigkeit?

Hallo, im Lösungsvorschlag zu Exercise 1 - Problem 7 ist mir eine Sache nicht ganz klar: Die Aufgabe ist hier konkret: "The printed value of prod ist, greater-or-equal than each array component" Also mathemtaisch: Für alle i, die einen Index bilden, gilt: prod >= a Im Lösungsvorschlag existieren nun...
von barracuda317
29. Mär 2013 23:02
Forum: Archiv
Thema: or_left nachvollziehen
Antworten: 7
Zugriffe: 831

Re: or_left nachvollziehen

Okay, das hat sich doch schneller geklärt als gedacht. Ich kann ja auch mit "false" schließen. Aber eine weitere Frage habe ich noch: Wie verfahre ich denn mit dem true-Fall. Eine Formel Haken , true \Rightarrow \Delta kann ich ja nicht schließen. Versuche ich dann mir im Sukzedenten auch ein true z...
von barracuda317
29. Mär 2013 22:50
Forum: Archiv
Thema: or_left nachvollziehen
Antworten: 7
Zugriffe: 831

or_left nachvollziehen

Hallo, ich versuche gerade zu verstehen, warum or_left so aufgebaut ist wie in den Folien http://www.abload.de/img/orleftutetg.png Wenn die Formeln ver-OR-t werden, muss nur eine von beiden gelten. Wenn ich sie aber beide im Antezedenten in die Prämisse ziehe, müssen doch beide gelten. Laufe ich dan...
von barracuda317
29. Mär 2013 14:57
Forum: Archiv
Thema: First-Steps KeY
Antworten: 2
Zugriffe: 414

Re: First-Steps KeY

Wie startest du KeY? Wir haben festgestellt, dass in den Folien ein anderer Link ist als auf der FGdI3 Website - und dass dieser Probleme mit manchen Regeln hat. Vielleicht liegt es daran. Welche Version ich auf dem Rechner hatte weiß ich nicht mehr genau. Ich habe es nun mit http://www.key-project...
von barracuda317
29. Mär 2013 13:32
Forum: Archiv
Thema: First-Steps KeY
Antworten: 2
Zugriffe: 414

First-Steps KeY

Hallo, gerade versuche ich mich praktisch an einem KeY-Beweis. Dafür habe ich die relSimple.key geladen. Ich schreibe mal genau wie ich vorgegangen bin und wo ich (bzw. KeY) nicht mehr weiter kommt. 1. Klick auf den Implikationpfeil im Sukzedenten mit ImpRight 2. Klick auf das \exists im Antezedente...
von barracuda317
28. Mär 2013 19:39
Forum: Archiv
Thema: Never Claim - Accept-Label
Antworten: 1
Zugriffe: 317

Never Claim - Accept-Label

Hallo, beim 1. Beispiel für ein Never-Claim (TemporaModelCheckingWithSpin) Folie 18 wird accept_init definiert (das Accept-Label?). Im If-wird aber im "Erfolgsfall" !q zu TO_init und nicht zu accept_init gesprungen. Warum sagt man dennoch, dass das accept_label beliebig oft besucht wird, genau genom...
von barracuda317
28. Mär 2013 16:52
Forum: Archiv
Thema: FGdI Sprechstunden
Antworten: 4
Zugriffe: 648

Re: FGdI Sprechstunden

Nathan Wasser hat geschrieben:Es wird am 3. April Sprechstunden geben.
Danke für die Antwort, ist schon bekannt wo und von wann bis wann diese stattfinden werden?
von barracuda317
27. Mär 2013 12:41
Forum: Archiv
Thema: Endzustand gesucht
Antworten: 5
Zugriffe: 525

Re: Endzustand gesucht

Es sollte "_nr_pr == 2" gelten solange beide Prozesse noch am leben sind Müsste dann nicht _nr_pr == 3 gelten, denn der init Prozess zählt ja mit. Wenn ich ::_nr_pr == 1 -> assert(n == 10 || n == 12); schreibe, kommt es trotzdem zum Timeout. Beide Prozesse müssten doch terminieren können, denn wenn...
von barracuda317
27. Mär 2013 11:14
Forum: Archiv
Thema: Spinspider - Befehl nicht gefunden
Antworten: 2
Zugriffe: 180

Re: Spinspider - Befehl nicht gefunden

Nathan Wasser hat geschrieben:Auf der Webseite gibt es unter Tools einen Link dazu.
Danke, das habe ich wohl übersehen.
von barracuda317
27. Mär 2013 10:46
Forum: Offtopic
Thema: Themen abonnieren
Antworten: 4
Zugriffe: 2413

Re: Themen abonnieren

d_s hat geschrieben:Schau mal ganz unten links auf der Seite. Dort gibt es die Funktion "Thema beobachten".
Genau das habe ich gesucht, danke. Ist aber schon versteckt :mrgreen:
von barracuda317
27. Mär 2013 10:25
Forum: Archiv
Thema: Spinspider - Befehl nicht gefunden
Antworten: 2
Zugriffe: 180

Spinspider - Befehl nicht gefunden

Hallo,

wenn ich ein Spinspider-Beispiel starten will, erhalte ich: spinspider: Befehl nicht gefunden.

Wie kann ich Spinspider installieren?
von barracuda317
27. Mär 2013 10:13
Forum: Offtopic
Thema: Themen abonnieren
Antworten: 4
Zugriffe: 2413

Themen abonnieren

Hallo,

kann man im Forum ein Thema abonnieren damit man bei neuen Nachrichten z.b. per Mail benachrichtigt wird? Ich habe die Funktion leider nicht gefunden.
von barracuda317
27. Mär 2013 10:12
Forum: Offtopic
Thema: Raspberry Pi
Antworten: 1
Zugriffe: 2077

Re: Raspberry Pi

Frag mal http://www.facebook.com/groups/info.tud/ dort.

Ich habe letzten Herbst eine Sammelbestellung angestoßen, und es gab großes Interesse.
von barracuda317
26. Mär 2013 16:16
Forum: Archiv
Thema: Definition Interleaving of independent computations
Antworten: 1
Zugriffe: 186

Definition Interleaving of independent computations

Hallo, leider ist mir die Definition von "Interleaving of indepentend computations" noch nicht so ganz klar. http://www.abload.de/img/defa2ilq.png Wir haben hier n unabhängige Prozesse P_1,..., P_n und einen Prozess i ( ist das dann Prozess P_i mit 1\leq i \leq n ? ) der eine Berechnung c^i = (s_0^i...

Zur erweiterten Suche