@nrailgun 2015-09-29T15:52:32.000000Z 字数 1118 阅读 1477

Modeling Distributed Systems with spin chan

强力软件

Distributed systems consist of:

Spin simulates distributed systems with processes and chans.

Declaration

A variable of channel type is declared by initializer.

chan c = [ capacity ] of { type_1, type_2, ..., type_n };

If capacity $\ge 1$ , channel is called "buffered", else "rendezvous" (直连，无缓冲).

Send statement has the form:

c ! expr_1, expr_2, ..., expr_n;

Receive statement has the form:

c ? var_1, var_2, ..., var_n;

Attension: Rendezvous chan ! and chan ? pairs can't be interleaved. But interleavings occur in buffered chan.

chan can also be sent through chan, setting up a private connection between server and client.

chan a = [0] of { int };
chan b = [0] of { chan };
b ! a;

Also, you can check channels for full / empty with full, nfull, empty, and nempty. Don't use the negative operator !

Syntax for receiving messages without removing it:

ch ? <v1, v2, ..., vn>

Receive statement admits values as arguments. Receive statement is executable if and only if matching succeeds.

c ? 'D', 'E', 'A', v;