ex6 Aufgabe 2 (FSM - cold hot)

[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

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

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

[Diablo]

Video gucke ich mir jetzt gleich mal an danke

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

[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

[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??

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

[Gerrit]

Hab es anhand des Papers von Eric endgültig verstanden:
http://www.bodden.de/pubs/bodden10efficient.pdf

[ericbodden]

Hallo. Die Antwort von tgp ist korrekt.

Liebe Grüße,
Eric

[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?

[ericbodden]

Hallo.

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.