Warum timeout?

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

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]

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]

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.