Modul 10, Folie 10

k_b
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 213
Registriert: 15. Mär 2009 12:06

Modul 10, Folie 10

Beitrag von k_b »

Hallo,

mir ist grad nicht mehr ganz klar wo man an dem Modell von Folie 10 sieht, dass keine Nachrichten verloren gehen und alle die empfangenw erden auch gesendet werden. Und zum anderen warum es keine Garantie gibt, dass gesendete Nachrichten auch empfangen werden.

Kann mir das grad jemand nochmal sagen bitte?


Danke schonmal ;)

The One and Only Markus
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 169
Registriert: 10. Nov 2005 19:28
Wohnort: Darmstadt

Re: Modul 10, Folie 10

Beitrag von The One and Only Markus »

Also verloren gehen können schonmal keine, weil ja die einzige Möglichkeit, dass Nachrichten aus dem Status entfernt werden, dass Empfangen (modelliert durch die Funktion recv(u,v,m)) ist.

Alle die empfangen wurden wurden auch gesendet, weil der Startzustand keine Nachrichten enthält und die einzige Möglichkeit, dass Nachrichten "empfangbar" werden durch das Senden modelliert ist. Also wenn mit recv(u,v,m) eine Nachricht empfangen wird muss sie vorher mit send(u,v,m) gesendet worden sein, sonst wär sie nicht in dem Staus enthalten.

Und eine Garantie, dass alle empfangen werden hast du nicht, weil dass System ja an einer beliebigen Stelle stoppen kann. Also es gilt ja nicht für alle Traces(TS) dass der Status s = () ist.

k_b
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 213
Registriert: 15. Mär 2009 12:06

Re: Modul 10, Folie 10

Beitrag von k_b »

Hallo,

super! Danke für die schnelle Antwort ;)

Mit deiner Aussage zu "alle, die empfangen werden, müssen auch gesendet worden sein" bestätigst du meine Vermutung. Mit dem dass es keine Empfangsgarantie gibt hab ich völlig in die falsche Richtung gedacht. Ich hab das mit dem Fakt des Verlorengehens von Nachrichten in Verbindung gebracht und war dann verwirrt.

Antworten

Zurück zu „Archiv“