Erfüllung der Erwartungen eines Clients

Nachdem wir im vorangehenden Kapitel das Protokoll eines Servers durch reguläre Typen spezifiziert haben können wir nun aus Sicht des Clients fragen, ob seine Folgen von Anfragen an den Server von diesem akzeptiert werden. Hierbei soll es möglich sein, dass der Client ein System aus mehreren nebenläufigen Clients ist. Dann können zu einem Zeitpunkt mehrere Anfragen an den Server bestehen, und dieser hat jeweils die Wahl, welche er als nächste bedient. Es ist jetzt sinnvoll, die nach Bearbeitung einer Anfragefolge $s$ noch bestehende Menge von Anfragen $R$ zu betrachten.

Definition 6: $offers(c):=\{(s,R)\mid \exists c',c\overset {s}{\Rightarrow }c',R=init(c')\}$

Zusammen mit den Fehlersituationen eines Servers $x$ lässt sich jetzt definieren, wann der Client durch den Server zufriedengestellt wird.

Definition 7: Ein Objekt $x$ erfüllt die Erwartungen eines Clients $c$, geschrieben $x\models c$, genau dann, wenn gilt :

$(s,R)\in failures(x)\cap offers(c)\Rightarrow R=\emptyset$.