Kommunikeerivad järjestikprotsessid

Sissejuhatus

CSP ehk communicating sequential process.

Jutt on sisuliselt (operatsioonisüsteemi) protessidest mis suhtlevad sõnumivahetuse (message passing) abil.

A trace is a finite sequence of symbols recording the actual or potential behaviour of a process from its beginning up to some moment in time. A process P is defined by the set of all traces of its possible behaviour. From the definition of a trace, it follows for any process P.

Semantika

STOP on protsess mis ei kommunikeeri midagi. SKIP on protsess mis tähitsab edukat lõpetamist.

Loe kui "a siis Q", kus P ning Q on protsessid ning a on sündmus. Sündmuse a korral protsess P käitub nagu protsess Q:

\begin{equation*} P = a \rightarrow Q \end{equation*}

Mitu prefiksit (prefix):

\begin{align*} Coin = coin \rightarrow Choice \\ Choice = choice \rightarrow Coffee \\ Coffee = coffee \rightarrow STOP \end{align*}

Võib kirjutada kui:

\begin{equation*} CM_0 = coin \rightarrow choice \rightarrow coffee \rightarrow STOP \end{equation*}

Väline valik

Väline valik (external choice) võib kirja panna kui:

\begin{equation*} x \rightarrow P\ \square\ y \rightarrow Q \end{equation*}

Mündi sisestamisel ning kohvi/tee valimisel masin väljastab tassi kohvi/teed ning seejärel lõpetab:

\begin{equation*} CM_1 = coin \rightarrow (choice\_coffee \rightarrow coffee \rightarrow STOP \ \square\ choice\_tea \rightarrow tea \rightarrow STOP) \end{equation*}

QAoES TU Berlin