# 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'
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))