Seite 1 von 1

ex6 Aufgabe 2 (FSM - cold hot)

Verfasst: 18. Jan 2012 14:19
von Diablo
Hi,

irgend wie bin ich total verunsichert wie ich nun den rückwerts Ablauf mache und etscheide was cold und was hot ist.

Ich habe die FSM gezeichnet und diese ähnelt ja sehr der in der Vorlesung vorgestellten.

Nun habe ich den Ablauf close, reconnect, write, close, write.
Ich beginne im Fehlerzustand und schaue mir an was in diesem passieren kann?
Wie bereits in der Vorlesung in der FSM habe ich hier zwei hot und einen cold.... dann gehe ich eins weiter raus und gucke wie ich in den Fehlerzustand oder in disconnected komme? .... und dann gehe ich noch eins weiter raus und ????

Also der Ablauf wie ich nun durch die FSM gehe ist mir nicht klar...
Wenn ich den write befehl dann rückwerts ausführe würde ich in disconnected landen... muss ich dann schauen wie ich hierher gekommen bin und welche vorherigen aufrufe somit hot (also zum fehlerzustand führen konnten) und danach gehe ich mit close weiter .. habe aber zwei möglichkeiten für close...

:(
Um so mehr ich mich damit beschäfige um so weniger scheine ich zu verstehen :(

Re: ex6 Aufgabe 2 (FSM - cold hot)

Verfasst: 18. Jan 2012 14:38
von tgp
Eric hat Clara auch vor einiger Zeit in Frankreich vorgestellt. im Video davon erklärt er ab 39:03 Minuten auch nochmal NSA - vielleicht hilft dir das :).

Re: ex6 Aufgabe 2 (FSM - cold hot)

Verfasst: 18. Jan 2012 14:52
von Diablo
Ganz konkret was beudetet hot was cold...

hot = kann error zustand erreiche durch?
cold = ist sicher kann error zustand nicht erreichen ... durch?

Hier fehlt mir einfach die Grundlage zum entscheiden.

Re: ex6 Aufgabe 2 (FSM - cold hot)

Verfasst: 18. Jan 2012 14:53
von Diablo
Video gucke ich mir jetzt gleich mal an danke

Re: ex6 Aufgabe 2 (FSM - cold hot)

Verfasst: 18. Jan 2012 15:47
von Diablo
hmpf... kann es richtig sein dass ich letzlich alle Zustände im hot status erhalte? Das müsste sich ja auch nach oben propagieren wie es das beim cold gemacht hat... und ich ende ja letzlich bei der gegebenen ausführungsreihenfolge im error Status....

Re: ex6 Aufgabe 2 (FSM - cold hot)

Verfasst: 19. Jan 2012 14:03
von ericbodden
Hallo Diablo.

Sorry wegen der späten Antwort. Aus irgend einem Grund bekomme ich manchmal keine Emails über neue Postings, obwohl ich das Forum abonniert habe.

Wenn an einem Statement s ein Zustand q hot ist, dann bedeutet das, dass man, falls man, wenn man s erreicht sich in Zustand q befindet*, und dann dem Programmverlauf weiter folgt, mit Sicherheit einen Fehlerzustand erreichen wird. Wenn ein Zustand cold ist, dann bedeutet das das Gegenteil: man wird ab s von q aus sicherlich keinen Fehlerzustand erreichen. (Bemerkung: Wer weiterdenkt, der fragt sich nun eventuell, ob es nicht Fälle geben kann, in denen man eventuell (aber nicht sicher) den Fehlerzustand erreicht. In der Tat ist das der Fall, allerdings nur, wenn es im Programm Verzweigungen gibt. In einem solchen Fall ist die Zustandsmenge keine Bipartition sondern eine Tripartition mir einer dritten Klasse "unknown".)

(*Ob das tatsächlich der Fall sein kann, sagt einem dann die Vorwärtsanalyse.)

Also der Rückwärts-Algorithmus geht wie folgt:

Man startet immer hinter den Events, die einen direkt in den Fehlerzustand bringen können. Für das Beispiel also direkt hinter allen write-statements. Für das Beispiel sind das zwei an der Zahl, man muss die Rückwärst-Analyse also zweimal durchführen, einmal ab (4) und einmal ab (6). An beiden Positionen ist der Fehlerzustand "hot", alles andere "cold".

Vor sowohl (4) als auch (6) steht nun natürlich eine write-transition. Nun schaut man daher, welche Zustände von den Zuständen die aktuell hot sind (also hier nur der Fehlerzustand) erreichbar sind, wenn man write-Kanten rückwärts folgt. Bei (3) und (5) sind dann entsprechend diese Zustände hot, alle anderen cold.

So macht man das ganze dann weiter, bis zur Position (1), für beide Fälle (ab (4) und ab (6)) getrennt; man bekommt also für die Stellen (1)-(4) zwei verschiedene Analyseinformationen. Entfernen darf man eine Transition natürlich nur dann, wenn sie bezüglich beider Analyseinformationen "äquivalent" ist.

Hilft das?

Gruß,
Eric

P.S. Louvain ist in Belgien :-)

Re: ex6 Aufgabe 2 (FSM - cold hot)

Verfasst: 25. Feb 2012 18:59
von Gerrit
Ich habe diesbezüglich noch eine Frage, beziehe mich auf folgendes Bild:
http://www.bodden.de/clara/wordpress/wp ... mage_6.png

Wieso ist bei 8 eine Leere Menge angegeben, obwohl ich doch - getreu dem Algortithmus - aus eins beim Rückwärtsgehen der Kanten "close" in 1,2 und 3 gelange? In 5 ist es ja auch die Menge {1,2,3} ..

Grüße, Gerrit

edit: liegt es daran, weil man durch das reconnect in einen Zustand kommt, in dem man mittels write garantiert nicht in einen Fehlerzustand kommen kann und deshalb von 8 bis 1 uns alles nicht interessiert/cold ist??

Re: ex6 Aufgabe 2 (FSM - cold hot)

Verfasst: 25. Feb 2012 21:32
von tgp
Also dieser längere Rückwärts-Durchlauf beginnt m.E. so:

Direkt nach Zeile 10 starten wir, da das dortige write böse ist: In den finalen Zustand (2) führt mindestens eine Transition, die mit write beschriftet ist. Also kommt in die hot-Menge schon mal die 2.

Wenn wir die write-Zeile zurückgehen, also zu direkt nach Zeile 9, gehen wir auch im Automaten die write-Pfeile zurück. Wir wollen ja wissen, wie wir zum bösen 2 gekommen sein könnten. Beim Zurückgehen kommen wir zu den Zuständen 1 und 2, also kommen beide dort in die hot-Menge.

Genauso gehts nun beim reconnect, um direkt hinter Zeile 8 zu kommen: Aus den hot-Zuständen 1 und 2 gehen wir reconnect-Transitionen zurück. Siehe da: Es gibt keine, also können wir durch reconnect gar nicht zu den dann bösen 1 und 2 gekommen sein. Alles gut, also gibt es dort keine hot-Zustände, also steht da eine leere Menge.

Jetzt soweit klar? Die Analyse-Information ist übrigens nicht "bei Zeile 8" oder so, sondern immer zwischen zwei Zeilen - das kommt aber auf den Folien besser raus als im Bild.

Re: ex6 Aufgabe 2 (FSM - cold hot)

Verfasst: 26. Feb 2012 15:06
von Gerrit
Hab es anhand des Papers von Eric endgültig verstanden:
http://www.bodden.de/pubs/bodden10efficient.pdf

Re: ex6 Aufgabe 2 (FSM - cold hot)

Verfasst: 27. Feb 2012 08:44
von ericbodden
Hallo. Die Antwort von tgp ist korrekt.

Liebe Grüße,
Eric

Re: ex6 Aufgabe 2 (FSM - cold hot)

Verfasst: 28. Feb 2012 16:38
von Ambush
Hallo,

Ich hab leider noch nicht ganz verstanden wann ich die statements jetzt rausnehmen kann und wann nicht. Konkret: Bei dem oben genannten Beispiel Bild ist der übergang in der Forward Analysis bei Statement 6: 1->1 . Diese sind in beiden Backwards Analysis equivalent. Ich kann es also rausnehmen, richtig?
wenn ich dann aber überlege, dass ich das close bei statement 6 rausnehme (und das close bei statement 5 ja auch....) dann verpasse ich doch den fehler der durch statement 6 gefolgt von Statement 7 entsteht ?

Weiß jemand was ich da falsch gemacht habe?

Re: ex6 Aufgabe 2 (FSM - cold hot)

Verfasst: 28. Feb 2012 17:47
von ericbodden
Hallo.
Ambush hat geschrieben: Weiß jemand was ich da falsch gemacht habe?
Wie Sie sich vielleicht erinnern, darf man immer nur einen shadow entfernen und muss dann die Analyseinformationen neu berechnen. Die neuen Informationen würden Ihnen dann sagen, dass Sie das zweite close()-Statement nicht entfernen dürfen.