Getting Started

In this section we give a brief overview of the basics of operating FDR4. Firstly, we give recommended installation instructions before giving a short tutorial introduction to FDR4. If FDR4 is already installed, simply skip ahead to A Short Tutorial Introduction.

Warning

It is strongly recommended that when using FDR you have at least a basic knowledge of CSP, or are acquiring this by studying it. Roscoe’s books The Theory and Practice of Concurrency and Understanding Concurrent Systems each contains an introduction to CSP that covers the use of FDR and, in particular, covers CSPM.

Installation

To install FDR4 simply follow the installation instructions below for your platform.

Linux

The recommended method of installing FDR is to add the FDR repository using the software manager for your Linux distribution. This makes it extremely easy to update to new FDR releases, whilst also ensuring that FDR is correctly installed and accessible.

If your distribution uses yum (e.g. RHEL, CentOS or Fedora) as its package manager, the following commands can be used to install FDR:

sudo sh -c 'echo -e "[fdr]\nname=FDR Repository\nbaseurl=http://www.cs.ox.ac.uk/projects/fdr/downloads/yum/\nenabled=1\ngpgcheck=1\ngpgkey=http://www.cs.ox.ac.uk/projects/fdr/downloads/linux_deploy.key" > /etc/yum.repos.d/fdr.repo'
sudo yum install fdr

The first of the above commands adds the FDR software repository to yum, whilst the second command installs fdr. If your distribution uses apt-get (e.g. Debian or Ubuntu), then the following commands can be used to install FDR:

sudo sh -c 'echo "deb http://www.cs.ox.ac.uk/projects/fdr/downloads/debian/ fdr release\n" > /etc/apt/sources.list.d/fdr.list'
wget -qO - http://www.cs.ox.ac.uk/projects/fdr/downloads/linux_deploy.key | sudo apt-key add -
sudo apt-get update
sudo apt-get install fdr

The first of these adds the FDR software repository to apt-get, the second installs the GPG key that is used to sign FDR releases, the third fetches new software from all repositories, whilst the last command actually installs FDR.

Alternatively, if your system does not use apt-get or yum, FDR can also be installed simply by downloading the tar.gz package. To install FDR from such a package, firstly extract it. For example, if you downloaded FDR4 to ~/Downloads/fdr-linux-x86_64.tar.gz, then it can be extracted by running the following commands in a terminal:

cd ~/Downloads
tar xzvf fdr-linux-x86_64.tar.gz

This will create a folder ~/Downloads/fdr4, that contains FDR4.

Next, pick an installation location and copy the FDR4 files to the location. For example, you may wish to install FDR4 in /usr/local and can do so as follows:

mv ~/Downloads/fdr4 /usr/local/fdr4

At this point FDR4 can be run be executing /usr/local/fdr4/bin/fdr4. In order to make it accessible from the command line simply as fdr4, a symbolic link needs to be created from a location on $PATH to /usr/local/fdr4/bin/fdr4. For example, on most distributions /usr/local/bin is on $PATH and therefore running:

ln -s /usr/local/fdr4/bin/fdr4 /usr/local/bin/fdr4

The above command may have to be run using sudo, i.e. sudo ln -s /usr/local/fdr4/bin/fdr4 /usr/local/bin/fdr4. At this point you should be able to run FDR4 by simply typing fdr4 into the command prompt.

Mac OS X

To install FDR4 on Mac OS X, simply open the downloaded application, which is named FDR4. On the first run, FDR4 will offer to move itself to the Applications folder. FDR4 can now be opened like any other program, by double clicking on FDR4 within Applications.

Warning

When running Mac OS X 10.8 or later with Gatekeeper enabled, in order to open FDR4 you need to right-click on FDR4, and select ‘Open’.

A Short Tutorial Introduction

It is strongly recommended that when using FDR you have at least a basic knowledge of CSP, or are acquiring this by studying it. Roscoe’s books Understanding Concurrent Systems and Theory and Practice of Concurrency each contains an introduction to CSP that covers the use of FDR and particular covers CSPM. This introduction therefore does not attempt to give a detailed introduction to CSP.

As a quick introduction to FDR, including many of the new features in FDR4, we recommend downloading and completing the simple exercises in the following file.

Download intro.csp

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
-- Introducing FDR4.0
-- Bill Roscoe, November 2013

-- A file to illustrate the functionality of FDR4.0.

-- Note that this file is necessarily basic and does not stretch the
-- capabilities of the tool.

-- To run FDR4 with this file just type "fdr4 intro.csp" in the directory
-- containing intro.csp, assuming that fdr4 is in your $PATH or has been aliased
-- to run the tool.

-- Alternatively run FDR4 and enter the command ":load intro.csp".

-- You will see that all the assertions included in this file appear on the RHS
-- of the window as prompts. This allows you to run them.

-- This file contains some examples based on playing a game of tennis between A
-- and B.

channel pointA, pointB, gameA, gameB

Scorepairs = {(x,y) | x  <- {0,15,30,40}, y <- {0,15,30,40}, (x,y) != (40,40)}

datatype scores = NUM.Scorepairs | Deuce | AdvantageA | AdvantageB

Game(p) = pointA -> IncA(p)
         [] pointB -> IncB(p)

IncA(AdvantageA) = gameA -> Game(NUM.(0,0))
IncA(NUM.(40,_)) = gameA -> Game(NUM.(0,0))
IncA(AdvantageB) = Game(Deuce)
IncA(Deuce) = Game(AdvantageA)
IncA(NUM.(30,40)) = Game(Deuce)
IncA(NUM.(x,y)) =  Game(NUM.(next(x),y))
IncB(AdvantageB) = gameB -> Game(NUM.(0,0))
IncB(NUM.(_,40)) = gameB -> Game(NUM.(0,0))
IncB(AdvantageA) = Game(Deuce)
IncB(Deuce) = Game(AdvantageB)
IncB(NUM.(40,30)) = Game(Deuce)
IncB(NUM.(x,y)) = Game(NUM.(x,next(y)))
-- If you uncomment the following line it will introduce a type error to
-- illustrate the typechecker.
-- IncB((x,y)) = Game(NUM.(next(x),y))

next(0) = 15
next(15) = 30
next(30) = 40

-- Note that you can check on non-process functions you have written. Try typing
-- next(15) at the command prompt of FDR4.

-- Game(NUM.(0,0)) thus represents a game which records when A and B win
-- successive games, we can abbreviate it as

Scorer = Game(NUM.(0,0))

-- Type ":probe Scorer" to animate this process.    
-- Type ":graph Scorer" to show the transition system of this process

-- We can compare this process with some others:

assert Scorer [T= STOP
assert Scorer [F= Scorer
assert STOP [T= Scorer

-- The results of all these are all obvious.

-- Also, compare the states of this process

assert Scorer [T= Game(NUM.(15,0))
assert Game(NUM.(30,30)) [FD=  Game(Deuce)

-- The second of these gives a result you might not expect: can you explain why?
-- (Answer below....)

-- For the checks that fail, you can run the debugger, which illustrates why the
-- given implementation (right-hand side) of the check can behave in a way that
-- the specification (LHS) cannot.  Because the examples so far are all
-- sequential processes, you cannot subdivide the implementation behaviours into
-- sub-behaviours within the debugger.

-- One way of imagining the above process is as a scorer (hence the name) that
-- keeps track of the results of the points that A and B score.  We could put a
-- choice mechanism in parallel: the most obvious picks the winner of each point
-- nondeterministically:

ND = pointA -> ND |~| pointB -> ND

-- We can imagine one where B gets at least one point every time A gets one:

Bgood = pointA -> pointB -> Bgood |~| pointB -> Bgood

-- and one where B gets two points for every two that A get, so allowing A to
-- get two consecutive points:

Bg = pointA -> Bg1 |~| pointB -> Bg

Bg1 = pointA -> pointB ->  Bg1 |~| pointB -> Bg

assert Bg [FD= Bgood 
assert Bgood [FD= Bg 

-- We might ask what effect these choice mechanisms have on our game of tennis:
-- do you think that B can win a game in these two cases?

BgoodS = Bgood [|{pointA,pointB}|] Scorer
BgS = Bg [|{pointA,pointB}|] Scorer

assert STOP [T= BgoodS \diff(Events,{gameA})
assert STOP [T= BgS \diff(Events,{gameA})

-- You will find that A can in the second case, and in fact can win the very
-- first game.  You can now see how the debugger explains the behaviours inside
-- hiding and of different parallel components.

-- Do you think that in this case A can ever get two games ahead?  In order to
-- avoid an infinite-state specification, the following one actually says that A
-- can't get two games ahead when it has never been as many as 6 games behind:

Level = gameA -> Awinning(1)
        [] gameB -> Bwinning(1)

Awinning(1) = gameB -> Level -- A not permitted to win here

Bwinning(6) = gameA -> Bwinning(6) [] gameB -> Bwinning(6)
Bwinning(1) = gameA -> Level [] gameB -> Bwinning(2)
Bwinning(n) = gameA -> Bwinning(n-1) [] gameB -> Bwinning(n+1)

assert Level [T= BgS \{pointA,pointB}

-- Exercise for the interested: see how this result is affected by changing Bg
-- to become yet more liberal. Try Bgn(n) as n copies of Bgood in ||| parallel.

-- Games of tennis can of course go on for ever, as is illustrated by the check

assert BgS\{pointA,pointB} :[divergence-free]

-- Notice that here, for the infinite behaviour that is a divergence, the
-- debugger shows you a loop.

-- Finally, the answer to the question above about the similarity of
-- Game(NUM.(30,30)) and Game(Deuce).

-- Intuitively these processes represent different states in the game: notice
-- that 4 points have occurred in the first and at least 6 in the second. But
-- actually the meaning (semantics) of a state only depend on behaviour going
-- forward, and both 30-all and deuce are scores from which A or B win just when
-- they get two points ahead.  So these states are, in our formulation,
-- equivalent processes.

-- FDR has compression functions that try to cut the number of states of
-- processes: read the books for why this is a good idea. Perhaps the simplest
-- compression is strong bisimulation, and you can see the effect of this by
-- comparing the graphs of Scorer and

transparent sbisim, wbisim, diamond

BScorer = sbisim(Scorer)

-- Note that FDR automatically applies bisimulation in various places.

-- To see how effective compressions can sometimes be, but that
-- sometimes one compression is better than another compare 

NDS = (ND [|{pointA,pointB}|] Scorer)\{pointA,pointB}

wbNDS = wbisim(NDS)
sbNDS = sbisim(NDS)
nNDS = sbisim(diamond(NDS))