This notebook implements a full version of Milner's value-passing Calculus of Communicating Systems (CCS)
It also serves as a gentle introduction to CCS and a short exposition of the concept of monad comprehensions which are defined, added to Mathematica syntax and subsequently used for many of definitions.
Some considerable time ago I spent a very long weekend developing an implementation of Milner’s Calculus of Communicating Systems and I would like to present it here as a notebook. It contains a fair bit of syntax using the `Notations` package. I think it represents a good example of using monad comprehensions in concert with other Wolfram Language constructs.
​
Your comments and/or corrections would be gratefully received. If I have omitted citations to help I’ve had from SX Mathematica I apologise: it’s been a while!
​
My notebook is attached (not every element is accurately rendered in the preview, but I have tested it with a recent version of Mathematica (14.0))

How to use this notebook

This notebook contains a number of dynamic objects (simulations) which will not operate or display correctly until the notation section and the initialisation cells have been evaluated. Dynamic updating should therefore be initially disabled. To use the simulations, first evaluate the notation section and then the initialisation cells and then finally turn on dynamic updating in the Evaluation menu. There is no need to re-evaluate the cells that generate the simulations unless you wish to start them afresh.

Front matter

Matthew Fairtlough
Murtwell Farm,
Diptford, Devon, TQ9 7NQ
United Kingdom
​matthew@fairflow.co.uk
Matthew Fairtlough is a computer scientist and a freelance researcher, lecturer and tutor who also worked for South Devon College, the Open University and Plymouth University. He holds a PhD in mathematical logic from Leeds University and has over 25 years of experience of lecturing and research in theoretical computer science and mathematics.
Copyright © Matthew Fairtlough, 2007-2024. This notebook is ultimately intended for release with a GPL-style license.

Abstract

CCS (Calculus of Communicating Systems) is a process calculus developed and published by Robin Milner in the 1980's [1]. It is a highly expressive yet very compact formal language for describing concurrent systems, having a formal semantics based on labelled transition systems and bisimulations and a satisfying equational theory. This notebook implements the transitional semantics of the language and utilizes special notations and the dynamic capabilities of Mathematica versions
>=
6 to illustrate its key features while adhering (reasonably) closely to standard notation and specification techniques. A full version of value-passing CCS is implemented, along with SCCS. The CCS agents are defined using an added language feature of monad comprehensions and are animated using a simple but effective interface. Several illustrative examples are developed including the precise version of the Alternating Bit protocol defined and analysed in [1].

Introductory remarks

Explanation of the purpose of the notebook

The main purpose is to explore the possibility of using Mathematica to bring new life to concepts from the theory of concurrency, which I once taught to Computer Science Undergraduates. This notebook shows that possibility is a very real one. The notebook concentrates on implementing a rich set of CCS language features, incorporating value-passing and parameterised recursive agents, and on simulation rather than analysis. However the symbolic features of Mathematica would also readily lend themselves to implementing many of the theoretical tools from the study and analysis of concurrent systems, for example minimization and bisimulations. A small example of the benefits of integration with Mathematica’s language features is the use of random bit generators in the implementation of the Alternating Bit Protocol (see below for details).

Ease of use and understanding

The theory supporting the simulator built here is complex and challenging and has progressed hugely since
[1]
was written. However, the examples are designed to introduce the reader gently to the CCS language and its behaviour and a lot can be learned simply by running the simulations set up below without being too concerned with the precise syntax of the agents involved. I particularly recommend studying the examples using the Fibonacci sequence; the
last example in the series
computes successive approximations to
1
GoldenRatio
by feeding the output from one agent (which generates the sequence in pairs) into the input of another (which simply takes two numbers and calculates a numerical approximation to their ratio).

Philosophy behind the notation and language features

The rule mechanism of Mathematica is not directly suitable for specifying and animating the operational semantics of a concurrent calculus such as CCS. We can however use syntax to specify labelled transitions in a standard way. Since non-determinism is not a built-in feature of the Mathematica programming language, I specify the transitions as a set (represented by a list). This is a reasonable alternative and is a specification technique widely used in the theoretical computer science community.
​
As far as I have been able, consistent with the existing meaning of symbols and my own tastes, I have stuck to a conventional notation for process calculi. This is defined in the Notation section below. The symbol
⋀
is used to denote parallel composition and
⋁
to denote non-deterministic choice of alternatives.  denotes prefix, ∖ restriction and ≀ denotes relabelling. nil is the deadlocked agent and
μ
x
pdenotes
a recursive agent where every occurrence of x in p has the same behaviour as
μ
x
p.
I use
a
+
todenoteapositive
or output action named a and
a
-
to denote a negative or input action with the same name. As usual τ denotes a silent action which usually marks a synchronisation on a pair of complementary ports
a
+
,
a
-
of two agents running in parallel (τ can also be used as a prefix in its own right, in which case it denotes action arising from internal structure that is left unspecified). When such an action does arise from internal talk, I tag the τ with the names of the ports and any bindings involved so as to make the simulation more comprehensible.
​
I have implemented a programming feature (monad comprehensions [5]) which is close to and generalises Haskell's list comprehensions. These are inspired by the comprehensions used in set theory which are heavily used in specification languages such as Z. I introduce a special notation for list comprehensions which is similar to that of Haskell and shares a feature of Clean [3, 4] in allowing parallel generators. The code is not optimised but it works well and was easy to write from the published definition of Haskell98 [2]. The general code is less than twenty lines long, including the notation. Syntax inspired by the records of Haskell is also defined; records are here called structures since Record is a built in symbol.

Notes on implementation tools and techniques

GUIKit had previously been used to build an interactive simulator for the language but this was made redundant by the interface tools now available. The main user interface was built with the following code:
simulateVP[agent_]:=DynamicModule[{bar=agent},​​Dynamic[PopupMenu[Dynamic[bar],setupTransitionsVP[bar],Short[bar],Framed[Row[{Column[{"simulating","(Value Passing)"}],Panel@Short[bar]},Invisible[p]],FrameStyle{Thickness[0.05],Blue}]]]]

Palettes and tools

Declare variables to be constant so they no longer appear to be undefined

(yes, we could use strings instead; I prefer symbols here)
mkConst[f_]:=(ClearAll[f];f[]:=f)(*thisseemsmostlyharmless*)
In[]:=
mkConst/@{generator,zipgen,nil,choice,precede,label,coLabel,choice,restrict,par,rvar,relabel,concrete,param,ifAg,tag,binding,sccs,ccs,release,harmless};
In[]:=
harmless[][][][]
Out[]=
harmless

A tool to count and extract initialization cells from any notebook

I found it useful to be able to extract the initialisation cells and comments from a large notebook without looking at package files. The code is clunky but effective.
Before running the following code, make sure you have a reference to the notebook from which you wish to extract initialization cells, for example by opening the notebook and executing
nbToExtract=SelectedNotebook[]
as below. Next, place the cursor at the point in the notebook from which you wish to extract initialization cells. On subsequently running
extractInitializationCells[nbToExtract]
, all initialization cells following the current insertion point will be extracted into a new document.
In[]:=
nbToExtract=SelectedNotebook[]
In[]:=
extractInitializationCells[nb_]:=​​Block[{nbNew=CreateDocument[],count=0},​​(SelectionMove[nb,Next,Cell];​​While[NotebookRead[nb]=!={},(If[InitializationCell/.Options[NotebookSelection[nb],InitializationCell],​​((*Print["found an initialization cell!"];*)​​count++;​​NotebookWrite[nbNew,NotebookRead[nb]]),{}];SelectionMove[nb,Next,Cell])];​​Print[ToString[count]<>" initialization cell(s) found"];​​Clear[nbNew](*justincase*))]
extractInitializationCells[nbToExtract]

Setting up a palette of symbols to aid in construction of CCS agents

We cannot use PasteButton for parts of expressions that require more input to be correctly parsed, such as infix symbols, so we create a function that will do this and add an optional argument for a tooltip.
In[]:=
symbolButton[s_]:=Button[s,NotebookApply[SelectedNotebook[],s],Appearance"Palette"]​​SetAttributes[symbolButton,HoldAll]​​symbolButton[s_,tt_]:=Tooltip[symbolButton[s],tt]

Concurrency palette

Mouse over the buttons to have an indication of what these symbols mean.
〈,⊲〉
⊲
⊲
〈
〉
⊕
⊖
⊕
⊖
⋄
⋄




∖
≀{}
∖
≀




+

-
{}
⋀
⋁
⋀
⋁

μ

[]


μ

x

y
λ
μ
[]
[]


·{}
·{}
·
nil


⟶

τ
α
β
γ
⋃
⋂
∧
∨
¬

Examples (follow instructions above to see and use simulations)

These examples were designed to test the features of the simulator as it was being developed. They are not "real-world" examples but are still challenging to understand and animate. With some changes to notation to make the symbolism more accessible, school students would be able to appreciate many the models developed here. Read in conjunction with [1], the simulation of the Alternating Bit Protocol would be comprehensible to undergraduate students of concurrency and aid their understanding of Milner's analysis.

Examples 0 (introduction to CCS)

Consider the processes of making breakfast and doing the washing. Each process executes a number of actions, which for the sake of simplicity we will assume take place in a fixed order and are never repeated. However, the two processes can run together, in which case their respective actions may be interleaved. They can also be alternatives, in which case only one set of actions can be observed.
In[]:=
MakeBreakfast=
"makeTea"
+
(
"layTable"
+
(
"makeToast"
+
nil));​​DoWashing=​​
"fillWasher"
+
(
"addDetergent"
+
(
"startWasher"
+
nil));
MakeBreakfast⋀DoWashing//FullForm
par[precede[label["makeTea"],precede[label["layTable"],precede[label["makeToast"],nil]]],precede[label["fillWasher"],precede[label["addDetergent"],precede[label["startWasher"],nil]]]]
A transition of an agent
p
is a pair
{α,q}
such that
p
α
⟶
q
. That means that agent
p
can do action
α
and thereby evolve into agent
q
. We call
q
a derivative of
p
. After carrying out action
"makeTea"
+
,
MakeBreakfast
still has two more actions before becoming inactive. So, for example,
"layTable"
+
(
"makeToast"
+
nil)
is a derivative of
MakeBreakfast
.
In[]:=
{transVP[MakeBreakfast],transVP[DoWashing]}
Out[]=
{{{
makeTea
+
,
layTable
+
(
makeToast
+
nil)}},{{
fillWasher
+
,
addDetergent
+
(
startWasher
+
nil)}}}
We see that the transitions of the choice
MakeBreakfast⋁DoWashing
just consist of the union of their independent transitions:
transVP[MakeBreakfast⋁DoWashing]
transVP[
fillWasher
+
(
addDetergent
+
(
startWasher
+
nil)),
makeTea
+
(
layTable
+
(
makeToast
+
nil))]
However, when they are run in parallel, each can run independently of the other and the components persist.
transVP[MakeBreakfast⋀DoWashing]
{{
fillWasher
+
,(
makeTea
+
(
layTable
+
(
makeToast
+
nil)))⋀(
addDetergent
+
(
startWasher
+
nil))},{
makeTea
+
,(
layTable
+
(
makeToast
+
nil))⋀(
fillWasher
+
(
addDetergent
+
(
startWasher
+
nil)))}}
In[]:=
simulateVP[MakeBreakfast⋀DoWashing]
When previewed, the interaface appears without special syntax: below is an image of the result. This has been done repeatedly below to avoid wasting screen space. The interfaces have been folded up but should still be functioning.
There is however no synchronisation between the components because they do not share complementary ports. On the other hand, the parallel composition of two agents such as
"a"
+
nil
and
"a"
-
nil
does yield a synchronisation; the action is silent (indicated by the notation
τ
) and both components evolve together.
transVP[(
"a"
+
nil)⋀(
"a"
-
nil)]
{{
a
-
,(
a
+
nil)⋀nil},{
a
+
,nil⋀(
a
-
nil)},{tag[τ,
a
+
],nil⋀nil}}
Since
"makeTea"
and
"fillWasher"
are different names, they cannot synchronise even though they have opposite polarities, and this is tested for by the function
conamed
.
{conamed[
"makeTea"
-
,
"fillWasher"
+
],conamed[
"a"
+
,
"a"
-
]}
{False,True}

Examples 1 (in which recursion is introduced)

Simple test agents

Examples 2 (approximations to GoldenRatio - 1)

Switching parameters

The agent tested below simply alternates between emitting 0 and emitting 1; this is the basic behaviour of the active components of the Alternating Bit Protocol (see below). Note that even though it uses parameters, it is still finite state so its state set can be computed.

A simple set of agents originally designed to test the substitution process within the transition function

The second agent is given an initial value (0 in this example), outputs the value on the channel "a" and then increments the value (and stores it) before restarting. The agent thus implements a simple incrementing counter.
This can now be synchronized with an agent which inputs the sequence and does something with it e.g. takes the ratio of the two values output. We first relabel the agent so that another agent uses the same channel. What was an output channel ("out") becomes an input channel to the agent which computes the ratio. As we see, the behaviour is identical apart from the name of the channel.
To get the two agents to play together, we place them in parallel and restrict them on the internal channel, which is now called "in". It would be a simple matter to keep a count of the number of times the calculation has been done, and to terminate the entire process once the ratio had reached a given accuracy.
Snapshot showing rapid convergence:

Example 3 (a larger example): the Alternating Bit Protocol

Since the protocol does not inspect the contents of messages, we follow Milner [1] in abstracting away from the contents of messages, leaving only the passing of the bits that are essential to the functioning of the protocol.
We model the timeouts with silent actions τ.

Treating 1's and 0's as bits

Agents designed to test the sender and replier

ackAny is an agent that tirelessly acknowledges with either bit (0 or 1)
transAny is an agent that tirelessly transmits with either bit

Defining the sender

accept2 is the same agent as accept except that it can appear outside the definition of sender
To simulate the behaviour of the sender it helps to feed the sender with acknowledgement bits. Symbolic simulation is possible only up to the point where a choice (the ifAg part) must be made that depends on the acknowledgement bit.

Defining the replier

Now for the transmission lines

The ack line

The transmission line

Putting it all together to simulate the protocol

A specification weakly equivalent (that is, it shows the same interactions when τ actions are ignored) to the protocol in that it acts as a simple pipe, accepting and delivering messages without delay:

The specification and simulation code with documentation and tests

The definitions are all made without special notations so this notebook can be used to generate a package file.

Supporting definitions and new language features

Comprehensions

Preliminary CCS definitions

Documentation of function usage

Names and conames

eqLabel and others with documentation

The syntactic sort of an agent

Testing synSort

Substitutions

The transition relation defined as a set

Documentation for transVP

Defining the 3-place transition relation

Computing transition graphs for visualisation and simulation

Note that these functions require the agent to be finite-state. To handle parameter passing that causes infinite state, first strip the parameters from the agent and then display.

Core simulation code

The special syntax (important since in FullForm agents become very large)

Conclusion

This notebook illustrates how concurrency theory can be directly implemented in a language with strong symbolic support. The simulation language (value-passing CCS with recursive parameterised constructions) is fully integrated with the huge mathematical toolbox provided by Mathematica, which suggests a number of possible directions for development. A simple idea would be to use the concurrency primitives defined here to implement Gosper's algorithms for continued fraction arithmetic [6]. This would provide a platform for understanding, developing and reasoning about these algorithms.
A large amount of material has been presented here and much of it may be unfamiliar. To do the reader justice, more in the way of documentation and explanation would be needed. However, I hope that the explanations of concurrency and the interactive simulations give a flavour of what can be achieved with this approach. It would be nice to add a graph-based interface to complement one based on formal syntax, useful as that is for specification, verification and implementation. This could be achieved in a number of ways and would have the benefit of being visually attractive and highly interactive. This notebook concentrates on simulation, yet model checking and formal verification are even more important components in a scheme to model concurrent systems operating in the real world. As an interface language and implementation platform for a theorem prover or a model checker Mathematica could prove invaluable, given the high productivity and flexibility it allows.
Using the Notation package has been an interesting exercise. The main issue I found was that if I made definitions using syntax introduced by the package, they were not correctly written to the package file. This is why all definitions have been made using the full form notation, and the help system has been used to re-present the definitions in the declared syntax. I would have liked more control over grammar as the built-in operator precedences do not always match my fondness for a particular symbol.

References

[4] Tom Brus, Marko van Eekelen, Maarten van Leer, Rinus Plasmeijer (1987).
`CLEAN - A Language for Functional Graph Rewriting'. Proc. of the Third International Conference on Functional Programming Languages and Computer Architecture (FPCA `87), Portland, Oregon, USA, LNCS 274, Springer Verlag, 364-384.

Postscripts

Buttons to return from References

Templates

The best way I have found to template a new recursive definition is to create a template manually and then use find-and-replace-all from the front end. Use the following to write a new function over the syntax of CCS agents.

CITE THIS NOTEBOOK

Implementing process algebra: recursive concurrent agents​
by Matthew Fairtlough​
Wolfram Community, STAFF PICKS, September 13, 2024
​https://community.wolfram.com/groups/-/m/t/3273073