Published 3Jan2013, updated 20Nov2018
This page is in group Technology.

In this blog I will jot down some experience with installation and use of the FDR2 tool [1] which analyses CSP (Communicating Sequential Processes) specifications [5].

My experience is that I try to avoid Unix, OSX, Terminal and bash scripting. But here is my last journey into it.

Important notice about a future FDR version

The Oxford team (see Epilogue), in a mail to me (that I was allowed to quote) on 4Feb2013 stated that:

A new version of FDR is in the works with native OSX (and hopefully Windows) support which includes probe style exploration of CSP processes. However, we cannot make any promises on release dates or features.

April 2013: I learn from a mail that it’s called FDR3. August 2013: More starting to appear on FDR3, see [14]. June 2015: FDR has gone to [15] and FDR4. Feb2017: Bill Roscoe has an interesting description of FDR at http://www.cs.ox.ac.uk/bill.roscoe/. He must know, since he’s the designer of it. Like «Thus refinement essentially coincides with reduction of nondeterminism».

Observe that «probe style exploration» points to the ProBE graphical tool! So, maybe before the snow has melted in Trondheim, parts of this blog note will have been obsoleted? I will update here when it arrives!

All this being said, in July2013 I discovered the The ASD:Suite®. See [13]

Installing FDR2 on Mac OSX

I downloaded to OSX 10.8.2 (Mountain Lion).

For academic use the tool may be downloaded from Oxford University Computing Laboratory [2]. You don’t need any licence to install or run it, provided it is for academic use.

Also download the fdr2manual-2.94.pdf and read it. It’s entitled «Failures-Divergence Refinement. Formal Systems (Europe) Ltd. FDR2 User Manual 17 May 2012» [10]. It is very instructive, and also tells some of what I say here.

The file fdr-2.94-academic-osx.tar.gz is downloaded and when you double-click it in downloads, it is unpacked to a directory called fdr-2.94-academic-osx

Move this directory to somewhere. I moved it to Programmer/Verktøy which are aliases of the two first of /Applications/Utilities/FDR2/fdr-2.94-academic-osx. I was asked for the system password to place it there. At the moment I don’t know if this was smart or not.

Then I started Terminal and tried «open .profile«. It complained, there was no such file. This is the batch script file that Terminal tries to run when it starts. So I opened TextEdit instead and started a new file with this contents. It took me a couple of hours of research ([3], [4] plus the manual) to get to this introducery batch script file :

# .profile (introducery)
export FDRHOME=/Applications/Utilities/FDR2/fdr-2.94-academic-osx
export DISPLAY=:0

Then I saved it as «.profile» at «my user», that is where the picture of the house is in Finder. It has standard directories Bilder, Dokumenter etc.. If you run «ls» in terminal it will show you Desktop Downloads Movies Pictures Sites Documents Library Music Public. So this is where terminal also starts. Then quit TextEdit.

Observe that .profile is invisible. It’s not necessary to do any tricks to make invisible files visible. Once in Terminal now do «open .profile» again. TextEdit should up with the new file! Yess!

Now, open the FDR2 directory and find the scripts directory. Start fdr2 by double-clicking it. This will open the fdr2 file. If X11 (the windowing system used by FDR2 if we don’t want to run in batch mode) is not running (Mountain Lion does not come with it) then you get an error message. Have a look inside the fdr2 file, right-click on it and open with TextEdit. It starts like this:

#!/bin/sh
if [ "xbatch" != "x$1" -a "x" = "x$DISPLAY" ]; then
  echo "FDR requires DISPLAY to be set unless running in batch mode."
  exit 1
fi

I deschiffered some by inspecting it. Since I did not have X11 installed, a dialogue window from OSX told me to go to http://support.apple.com/kb/HT5293 («About X11 and OS X Mountain Lion»). I read what was there and downloaded and installed X11. I then had an installable called XQuartz-2.7.4.dmg on my machine. I double-clicked it the usual way and it installed it.

Then I started XQuartz. Fiddled around with it, but nothing more than having it run was needed.

Then I went to the fdr2 script again. I double-clicked it and FDR2 started! Yess!

A better .profile

But OSX will start XQuartz on demand by default if it isn’t already running!

XQuartz uses the standard OSX launchd interface to bring up the X11(XQuartz) server on demand when a program tries to connect to the socket named in $DISPLAY. If there is no $DISPLAY then the FDR2 does it. So, without having XQuartz running, here is a next best .profile. In the optional last line it queries XQuartz state:

# .profile (next best)
export FDRHOME=/Applications/Utilities/FDR2/fdr-2.94-academic-osx
$echo $DISPLAY

Now, just double-click the  fdr2 script and you will see XQuartz start (bouncing icon). Then FDR2 starts (but not as fast as with the first .profile).

The optional query in the last .profile above yields this result on my machine:

-bash: /tmp/launch-m6KQIS/org.macosforge.xquartz:0: Permission denied

Still it works!

Running FDR2 in batch mode

Here’s a cut and paste from a mail from Oxford (see below):

You don’t have to double click on the fdr2 script, you can also run

$FDRHOME/bin/fdr2

at the terminal prompt (and put any csp script as an argument on the command line). Alternatively you can add

$FDRHOME/bin

to your PATH (see the bash manpages) and then you can just type fdr2 directly.

The best .profile

So, here’s the most versatile .profile:

# .profile (most versatile)
export FDRHOME=/Applications/Utilities/FDR2/fdr-2.94-academic-osx
export FDREDIT="open -t"
PATH=${PATH}:$FDRHOME/bin
export PATH
$echo $DISPLAY

The FDREDIT tells FDR2 to have OSX open a file in the default editor. This is TextEdit. If you omit that line, the vi editor will be used.

Log from FDR2 running

This FDR release is for academic teaching and research purposes only.
For any other use, please contact Formal Systems (Europe) Ltd at
enquiries@fsel.com to obtain a commercial licence.
Fontconfig warning: ignoring UTF-8: not a valid region tag
Fontconfig warning: ignoring UTF-8: not a valid region tag
Fontconfig warning: ignoring UTF-8: not a valid region tag
Fontconfig warning: ignoring UTF-8: not a valid region tag
Fontconfig warning: ignoring UTF-8: not a valid region tag
Fontconfig warning: ignoring UTF-8: not a valid region tag
Welcome to FDR 2.94 Academic teaching and research release

Epilogue

P.A. at the Oxford team did respond to this blog note and helped me understand, and filled in quute a few holes. This may also trigger an update on their install notes.

But why couldn’t they just do it all for me in the .dmg download? This is a real threshold for some of us (I think even also for some of my fellow students at [6] this fall). The users in the nineties (when FDR2 was conceived) were perhaps more fluent in Unix details. And when I now will start to use it, I have a feeling that I will long for what might come next!

Graphical tool to visualize channel handling etc

[1] points to ProBE, which is «an animator for CSP processes allowing the user to explore the behaviour of models interactively. ProBE is available for download without charge.» It sems to be rather outdated, for «Windows NT / ’95 (and later), FreeBSD, Solaris (Sparc), Solaris (x86), Linux». I thought that perhaps I could try running the Windows95 version under WineApp.app (see note 060, [4] there). But then, the fsel url is «forbidden», as all the download urls there (but see Update2 below)

So these are at the moment not downloadable: «probe-1.30-windows.zip», «probe-1.30-freebsd4.tar.gz», «probe-1.30-solaris.tar.gz» and «probe-1.30-linux6.tar.gz». Since they are so old, there was nothing for OSX on that round..

Update1, I queried the Oxford team, and in a mail they replied that they will «resurrect the download links from known good binaries (the server host was compromised at the end of last year (2012) unfortunately).» I’ll update when it’s there. Also see Important note about a future version here. Update2: On 1Mar2013 the binaries have been restored and are now available! I downloaded the Windows 95 version and ran it under WineApp. No setup required. And discoved some misunderstandings in my understanding of CSPm..

Scratchpad

IMPLEMENTATION deadlock free [FD]

only means what it seems to say if there is a green check point to the left. However, if there is a red X there it means «deadlock». The text simply says this line has been compiled (I think):

assert IMPLEMENTATION :[deadlock free]

CSP questions

Q1 – SKIP in choice

How is the below occam fragment coded in CSP?

ALT
  channel ? data
    ... Handle it
  Expression & SKIP
    ... Handle it

CSP has the ‘&’, but I have seen no example of a SKIP in this case. FDR2 complains that it misses an arrow after my suggestion, and if I put it in (like below), then it also seems to complain:

let
  SERV (thedata, state, ready) =
    in_xchan_ready ? any ->
      SERV (thedata, state, is_ready)
    |~|
    (ready == is_ready) & SKIP ->
      out_xchan_s ! thedata ->
      SERV (no_data, state_no_data, is_not_ready)
within SERV (no_data, state_no_data, is_not_ready)

The snippet above has no real meaning, I have just taken out an example from the top of my head from something that failed yesterday. Please help!

Here’s the reply I got from P.A. to whom I mailed this question. (I hope i got indenting ok):

Oh, I see. Just elide the SKIP then: It’s unnecessary.

ALT = in ? data ->
          DOSTUFF1(data)
      []
      guard1 & in2 ? data ->
          DOSTUFF2(data)
      []
      guard2 & DOSTUFF3

It’s only written like that in Occam because the ALT alternatives have to be guarded by event prefixes. CSP [] is more general than ALT and doesn’t care whether its arguments are guarded in this fashion. See Bill Roscoe’s book for the gory details.

Q2 – Which parallel?

1. Synchronous parallel
2. Alphabetized parallel (CSPm)
3. Interleaving / unsynchronized parallel (CSPm)
4. Generalized parallel / interface parallel / sharing (CSPm)
5. Linked parallel (CSPm)
6. occam PAR

The reason for this chapter is that when I started to write FDR2 models I began with one parallel operator, copy and pasted from an example, and found things to perhaps work – until I tried other parallel operators and saw that then things seemed to work or not work. I needed to befriend the terms. Then I discovered that different people had different friends here. The goal is to understand why I would use any one of the four possible to describe as machine-readable CSP. Honestly I optimistically wanted to discover which of them was the occam PAR. The answer was: well.. (wrong question!)

CSP describes several parallel operators, but not necessarily the same flavours in each book. The reason that this is possible is that one type of parallel with one set of «dependencies» between the processes may be described as several other types of parallel with other sets of dependecies – with a little bit of this and a little bit of that (example in point 4). Since it’s hard to describe a rose as a specialised tulip, the wise seem to have landed on – roses and tulips.

 CSPm means machine-readable CSP (as understood by FDR2), see [12]

«The various different syntaxes exist mostly because different people like to write the same process in different ways: there’s no particular reason to prefer one over another.» (P.A.)

The ‘alphabet’ (the set of communication: events and channels) used to control a parallel combination will have semantic significance in CSPm. In [7] (Roscoe) alphabets are explicit, as oppose to [9] (Hoare). ([7] chapter «2.7 On alphabets»)

In the CSP literature I have seen so far there are some 5 parallel composition operators plus the occam PAR. First the four in the textbook part of Roscoe [7]:

1. Synchronous parallel
   Not in CSPm:

   P || Q

   All events are synchronized upon. This is not described in the Schneider book [8].

   It may be described using by f.ex. Sharing (below) like this [7] chapter «2.6 Tools»:

   P || Q == P [|Events|] Q

2.  Alphabetized parallel

   P [ a || a' ] Q
   P [interface] Q

   Only those events defined in the alphabet or interface are agreed upon. Also spelt Alphabetised parallel. Interface are events or channels.

   All other parallel composition operators are «variants» of this type (P.A.)

   P [ x || y ] Q \ x ∩ y
   is "close to" occam PAR (point-to-point invisible, see below)

3. Interleaving / unsynchronized parallel

   P ||| Q

   Process P and Q do not interact on any events apart from termination. Each event is performed by exactly one process» [8]. «The parallel operator with no synchronization events in its alphabet is named interleaving parallel» [11]. For some reason the word parallel is often dropped. Also, it’s not interleaved parallel. The interleaving operator represents completely independent concurrent activity for P and Q. Also called Unsynchronized parallel (in FDR2 Manual [10]).

4. Generalized parallel / interface parallel / sharing

   P [| a |] Q
   LEFT [| {|internal_right,internal_left|} |] RIGHT
   
   Wikipedia syntax:? P |[ {a} ]| Q (also accepted by FDR2!)

   Any event in the interface set {a} can only occur when both P and Q are able to engage in that event.

   Also spelt Generalised parallel and called Interface parallel. It does not exist in Hoare’s book [9]. I was rather confused when reading the CSPm descriptions in both [7] (Roscoe) and [10] (FDR2 manual) since when describing this kind of parallel in that context, the word ‘generalized’ is completely gone and ‘shared’ is used instead. I thought them to be unique. But I discovered the connection by reading [7] chapter «2.6 Tools» and «B.5 Processes». Not easy to detect, Roscoe!

   «The |[ or [|  is purely a matter of preference. I think Hoare used one and some other people used the latter. FDR2 accepts either.» (P.A.)

   Here are aspects of generalized parallel described as other types. This shows the expressive power og generalized parallel.

   If there is no interface between two processes (nothing is synchronized), then it’s the same as interleaving:

   P || Q == P ||| Q
     {}

   Since CSPm could not have a syntax like the left part (difficult to write and parse the connection between the two lines), the first line in the code below will say the same:

   P [| {} |] Q    == P ||| Q         (as interleaving)
   P [| x ∩ y |] Q == P [ x || y ] Q  (as alphabetized)
   P |[ x ∪ y ]| Q == P || Q          (as synchronous)

   The second line states that if P and Q never communicate outside x and y, but by the events in the intersection of x and y, then those common events represent the interface alphabet of alphabetized parallel.

   The third line states that if P and Q never communicate outside x and y, but by the events in the union of x and y, then all events, also those not in common, represent synchronous parallel – where all events are synchronized upon.

   P [| z |] Q \ z     Is also
   "close to" occam PAR (point-to-point invisible, see below)

The Wikipedia article only mentions Interleaving and Interface parallel.

Then, when it comes to the CSPm manual part of Roscoe’s book then Synchronous seems to be gone and in come this:

5. Linked parallel

   P [chan_out <-> chan_in] Q
   FORK [right<->left] PHIL

   It is a «generalised version of chaining» [10]. The linked parallel operator generalizes the chaining operator ≫ [12]. Observe that CSPm per se has no «>>» chaining operator. Line 2 makes channels left and right available for FORK and PHIL.

   It is easy to see the similarities between the below occam and CSPm code. The second PAR in the occam code would set up a «linked parallel», if that were an occam term:

   "BUFF" is a one place buffer, not seen here, but see [12]
   
   VAL N IS 4:
   [N + 1] CHAN OF ANY OutIn:
   PAR
     -- Producer at InOut[0] and consumer at InOut[N] in here 
     PAR i = 0 FOR N
       BUFF (OutIn[i],OutIn[i+1])
   
   PIPE (N,in,out) =
     [out<->in] i : @ BUFF (in,out)

So, now – where is the occam PAR operator in this (apart from the example above)?

6. occam PAR
   Not in CSPm:

   PAR
     P
     Q

«Occam PAR infers the synchronisation event sets from the process defintions, rather like the original Hoare ||, so it doesn’t have a direct equivalent in CSPm where specifying the alphabets is always required.» (P.A.)

There are two examples in the alphabetized and generalized chapters above, where occam examples are seen (search for «point-to-point»). They are pasted from book [7] (Roscoe, page 78 in chapter «3.1 Hiding») which states that:

If we want to hide all the communications between a pair of parallel processes we would write P [ x || y ] Q \ x ∩ y or P [| z |] Q \ z. This creates point-to-point, invisible communication, which is arguably closest to the ‘natural’ parallel operator of implementations such as OCCAM.

The paper [11] (Bojan Orlic (B.O.)) has some clarification here (coloured by me):

In occam, a PAR construct defines that all of its subprocesses are executed in parallel, that is by separate flows of control. A PAR construct contains two or more processes – it is not relevant for the construct whether any two processes are intended to be interleaving or to synchronize on some user-defined events. Instead of explicitly specifying events on which processes synchronize per every parallel operator, the concept of a channel is used. A channel is an infrastructure element that encapsulates the point of event synchronization. In this way, event ends are not aware of each other; they communicate by accessing the same channel. The channel implementation mechanism take care that event ends synchronize in a rendezvous manner. The alphabet on which two parallel processes synchronize is in this way implicitly specified in their channel interconnections. For the operational semantics of a parallel construct in occam, explicit enumeration of alphabets on which processes synchronize is thus not needed and not foreseen in its language syntax. In the same way, renaming and hiding operators are superfluous in a channel-based synchronization interconnection infrastructure. A CSP event is symmetric seen from all sides participating in rendezvous synchronization and may or may not have associated a set of data communications in one or both directions. Occam channels assume both rendezvous synchronization and unidirectional communication.

«The key difference regarding the parallel construct is that in CSP one needs to explicitly specify channel/event names on which the processes composed in parallel will synchronize. While in Occam, communication and synchronization (barrier) are always lumped together in notion of rendezvous channels, in CSP focus is on synchronization. Therefore, processes will synchronize on events with same name but only if that is specified in alphabet (interface) of parallel construct. If nothing is specified then synchronization is on all events with same name. [..] Occam and CSP…occam is simple for practical use, CSP is more powerful for expressing subtleties of synchronization patterns» (B.O.)

Credits. Thanks P.A. and B.O. for thorough replies to my mail queries! I have done some copy / paste from them!

Q3 – CSPm operator precedence

Do observe that CSPm has operator precedence, see [10] (FDR2 User Manual). Do like this:

SERV (params..) =
    chan1 ? value ->
    (
      if (some condition) then
        SERV (params..)
      else if (some condition) then
        SERV (params..)
      else (some condition) then
        SERV (params..)
    )
  []
    chan2 ? msg -> SERV (params..)

It wil compile perfectly fine without the brackets, but since [] and the other CSP operators binds tighter than if..then..else then the choice operator [] would start to run at the above else statement. I think the first if and else if clauses will bind to chan1 input. To be honest I don’t understand why it’s broken at that place.. This is not for previous occam people to understand, having been unlearned of operator precedence!

Wish list and comments

1. (This point may be nonsensical) «FDR Status» window does not include a date/time before each log line. This makes it difficult to understand what’s new and not. Right now it took me 15 minutes to understand that a complaint it had after loading a file, was from a loading yesterday! So I restarted FDR2 to restart the log window. Of course, the window does not have any xy-addressing, so it’s always what’s at the bottom that is new! But it’s not as simple as that: Some times the window seems to go full, and it looks like it’s being updated, but it isn’t. «Yesterday’s» sins are just present. It could say something like NEWLINE not expected at line 28, but this is only a past truth.. (I would like to be able to flush the log window and write comments in it!)
2. FDR2 status line (bottom of the screen) seems to disappears in a second, so it’s quite volatile.
3. After the importing syntax check has been passed and I decide to do a FD Check, I get the disappearing «Process requires arguments to be filled in» in the status line. What doe sthis mean, and which line does it point to?
4. I did «File», «All asserts» and then I got an error message into the Status window, like «Identifier …. has not been declared near line xx of file», which surely will help me going on. Is this like standard «compilation» with messages?

References

1. FDR2 at http://www.fsel.com/index.html Formal Systems (Europe) Ltd. FDR = Failures-Divergence Refinement.
2. Oxford University Computing Laboratory at http://www.cs.ox.ac.uk/projects/concurrency-tools/
3. «OS X: Easily edit hidden configuration files with TextEdit» at http://www.tech-recipes.com/rx/2618/os_x_easily_edit_hidden_configuration_files_with_textedit/
4. «Easier use of X11 in bash» at http://hints.macworld.com/article.php?story=20031026091804549
5. CSP at http://en.wikipedia.org/wiki/Communicating_sequential_processes
6. Course «The Theory of Concurrency in Real-Time Systems» TK8112 at NTNU, see http://www.ntnu.edu/studies/courses/TK8112
7. Some of the books at Oxford (download at http://www.cs.ox.ac.uk/activities/concurrency/books/). «The Theory and Practice of Concurrency» by A.W. Roscoe, 1998
8. «Concurrent and Real-time Systems: the CSP Approach» by Steve Schneider, 1999
9. «Communicating Sequential Processes» by C.A.R. Hoare, 1985
10. «FDR2 User Manual», see [2]
11. «Design principles for the (System)CSP software framework» by B. Orlic. et al. at https://www.ce.utwente.nl/aigaion/attachments/single/652. The CPA-2007 paper is present at http://www.wotug.org/paperdb/show_pap.php?f=1&num=522
12. «CSPm : A Reference Manual Bryan Scattergood» by Philip Armstrong, at http://www.cs.ox.ac.uk/ucs/cspm.pdf
13. The The ASD:Suite® at http://www.verum.com/
14. «FDR3: The Future of CSP Model Checking», Thomas GIBSON-ROBINSON, Department of Computer Science, University of Oxford, England. Fringe presentation at CPA-2013, see http://www.wotug.org/cpa2013/programme.shtml
15. FDR3 — The CSP Refinement Checker
    FDR3 analyses programs written in CSPM, which combines the
    operators of Hoare’s CSP with a functional programming language. It also has support for analysing timed systems, via tock CSP, see https://www.cs.ox.ac.uk/projects/fdr/