Warum timeout?

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Warum timeout?

Beitrag von null »

Hallo zusammen,

ich habe den folgenden Code aus der letzetn Vorlesung einfach mal ausprobiert:

Code: Alles auswählen

chan request = [0] of {byte}

active proctype Server() {
	byte num;
	do :: request ? num -> printf("serving client %d\n", num);
	od
}	

active proctype Client0() {
	request ! 0;
}

active proctype Client1() {
	request ! 1;
}
Wenn ich jedoch spin jetzt starte, kommt die folgende Ausgabe:

serving client 0
serving client 1
timeout
#processes: 1
5: proc 0 (Server) clientServer.pml:5 (state 3)
3 processes created

Dazu habe ich zwei Fragen:

1.) Warum kommt ein timeout? Was bedeutet das?

2.) Wo ist meine Schleife? Habe ich nicht eigentlich eine Endlosschleife erzeugt?

Vielen Dank für die Hilfe
Viele Grüße,
null

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Warum timeout?

Beitrag von yourmaninamsterdam »

Dein Server empfängt über den Rendezvous-Channel erst die Nachricht von Client1, dann von Client2, erreicht dann die Anweisung 'request ? num', die aber nie ausgeführt werden kann, weil alle Clients terminiert sind. Daher endet dein Programm mit einem Timeout.

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Re: Warum timeout?

Beitrag von null »

und wie kann ich dieses Problem beheben? Ich kann ja nicht die Sendeoperation der Clienten in eine Schleife stecken, weil das ja eigentlich eine andere Funktion dann hätte.

Vielen Dank für die Hilfe! :)

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Warum timeout?

Beitrag von yourmaninamsterdam »

Naja, eine offensichtliche Variante wäre, nur zwei Nachrichten mit dem Server zu empfangen, wenn du genau weißt, dass nur zwei gesendet werden.

Ansonsten gibt es da noch die end-labels.

Antworten

Zurück zu „Archiv“