FDR Manual
User Manual:
Open the PDF directly: View PDF
.
Page Count: 174
| Download | |
| Open PDF In Browser | View PDF |
FDR Manual
Release 4.2.0
University of Oxford
December 20, 2016
CONTENTS
1
Introduction
1.1 Citing FDR . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2
The FDR User Interface
2.1 Getting Started . . . . . . . .
2.2 Session Window . . . . . . .
2.3 Debug Viewer . . . . . . . .
2.4 Process Graph Viewer . . . .
2.5 Probe . . . . . . . . . . . . .
2.6 Node Inspector . . . . . . . .
2.7 Communication Graph Viewer
2.8 Machine Structure Viewer . .
2.9 Options . . . . . . . . . . . .
1
1
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
3
3
8
15
20
23
24
26
28
29
The FDR Command-Line Interface
3.1 Command-Line Flags . . . . .
3.2 Examples . . . . . . . . . . . .
3.3 Using a Cluster . . . . . . . . .
3.4 Machine-Readable Formats . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
35
35
37
38
41
CSPM
4.1 Definitions . . . . .
4.2 Functional Syntax .
4.3 Defining Processes .
4.4 Type System . . . .
4.5 Built-In Definitions .
4.6 Profiling . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
49
49
59
68
75
77
86
5
Integrating FDR into Other Tools
5.1 The FDR API . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.2 API Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
89
89
93
6
Optimising
105
6.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
6.2 Compression . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
7
Implementation Notes
7.1 Semantic Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.2 Compilation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.3 Refinement Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3
4
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
109
109
109
110
i
7.4
8
9
Type Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
Release Notes
8.1 4.2.0 (20/12/2016) . . . .
8.2 3.4.0 (09/03/2016) . . . .
8.3 3.3.1 (17/06/2015) . . . .
8.4 3.3.0 (15/06/2015) . . . .
8.5 3.2.1 – 3.2.3 (06/01/2015)
8.6 3.2.0 (30/01/2015) . . . .
8.7 3.1.0 (11/08/2014) . . . .
8.8 3.0.0 (09/12/2013) . . . .
.
.
.
.
.
.
.
.
115
115
115
115
116
116
117
117
118
Example Files
9.1 FDR4 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
9.2 Dining Philosophers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
9.3 Inductive Compression . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
125
125
128
130
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
10 References
11 Licenses
11.1 boost . . . . . . .
11.2 boost.nowide . . .
11.3 CityHash . . . . .
11.4 google-sparsehash
11.5 graphviz . . . . .
11.6 libcspm . . . . . .
11.7 LLVM . . . . . .
11.8 lz4 . . . . . . . .
11.9 popcount.h . . . .
11.10 QT . . . . . . . .
11.11 zlib . . . . . . . .
11.12 Haskell . . . . . .
135
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
137
137
137
138
138
139
140
141
142
143
143
152
153
Bibliography
165
Index
167
ii
CHAPTER
ONE
INTRODUCTION
FDR is a tool for analysing programs written in Hoare’s CSP notation, in particular machine-readable CSP namely
CSPM, which combines the operators of CSP with a functional programming language. The original FDR was written
in 1991 by Formal Systems (Europe) Ltd, and a completely revised version FDR2 was released in the mid-1990s by
the same organisation. The current version of the tool is FDR4, first released in October 2016 following FDR3 which
was first released in 2013. Both of these versions were released by the University of Oxford, which also released
FDR2 versions 2.90 and above in the period 2008-12.
FDR4.0 has extremely similar functionality to FDR2.94, but is completely re-written. The main differences are:
1. The user interface has been completely revised.
2. The debugger has been completely revised and gives simultaneous information about all components of a system, rather than one at a time.
3. There is an integrated type checker for CSPM .
4. It now uses multi-core parallelism to speed up its operation.
5. A version of the ProBE CSP animator has been integrated.
6. There is a utility for drawing graphical representations of the labelled transition systems that represent processes
within FDR.
The only significant functionality of FDR2.94 that FDR4.0 lacks is support for the revivals and refusal testing models
of CSP and their divergence-strict versions (i.e. [V=, [VD=, [R= and [RD=). Note that the batch mode of FDR2.94
has been replaced by a new machine-readable interface based on standard formats (JSON, XML and YAML are
supported).
FDR uses many algorithms and data structures. The ones used in FDR4 are in some cases the same, in some cases
mildly modified, and in other cases completely new. Papers about FDR4 and its development can be found in References. Many books and papers have been written about CSP and earlier versions of FDR.
1.1 Citing FDR
When citing FDR, please refer to the following paper:
@inproceedings{fdr,
title={{FDR3 --- A Modern Refinement Checker for CSP}},
author={Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov, A.W. Roscoe},
booktitle={Tools and Algorithms for the Construction and Analysis of Systems},
year = {2014},
pages = {187-201},
volume={8413},
series={Lecture Notes in Computer Science},
1
FDR Manual, Release 4.2.0
editor={Ábrahám, Erika and Havelund, Klaus},
}
The manual may be cited as:
@manual{fdrmanual,
title={{Failures Divergences Refinement (FDR) Version 3}},
author={Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov, A.W. Roscoe},
year={2013},
url={https://www.cs.ox.ac.uk/projects/fdr/},
}
2
Chapter 1. Introduction
CHAPTER
TWO
THE FDR USER INTERFACE
To launch FDR on Mac OS X simply open the FDR application that you have downloaded (normally this will be
inside Downloads in your home folder). To launch FDR under Linux simply type fdr4 from a command prompt
(providing the installation instructions have been followed). Alternatively, a particular file can be loaded by typing
fdr4 file.csp into a command prompt.
However FDR is launched, the main window that is presented is known as the session window, and is documented
further in Session Window.
2.1 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 .
2.1.1 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/download
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:
3
FDR Manual, Release 4.2.0
sudo
wget
sudo
sudo
sh -c ’echo "deb http://www.cs.ox.ac.uk/projects/fdr/downloads/debian/ fdr release\n" > /etc/apt
-qO - http://www.cs.ox.ac.uk/projects/fdr/downloads/linux_deploy.key | sudo apt-key add apt-get update
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’.
2.1.2 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
4
Chapter 2. The FDR User Interface
FDR Manual, Release 4.2.0
1
2
-- Introducing FDR4.0
-- Bill Roscoe, November 2013
3
4
-- A file to illustrate the functionality of FDR4.0.
5
6
7
-- Note that this file is necessarily basic and does not stretch the
-- capabilities of the tool.
8
9
10
11
-- 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.
12
13
-- Alternatively run FDR4 and enter the command ":load intro.csp".
14
15
16
-- 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.
17
18
19
-- This file contains some examples based on playing a game of tennis between A
-- and B.
20
21
channel pointA, pointB, gameA, gameB
22
23
Scorepairs = {(x,y) | x
<- {0,15,30,40}, y <- {0,15,30,40}, (x,y) != (40,40)}
24
25
datatype scores = NUM.Scorepairs | Deuce | AdvantageA | AdvantageB
26
27
28
Game(p) = pointA -> IncA(p)
[] pointB -> IncB(p)
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
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))
45
46
47
48
next(0) = 15
next(15) = 30
next(30) = 40
49
50
51
-- Note that you can check on non-process functions you have written. Try typing
-- next(15) at the command prompt of FDR4.
52
53
54
-- Game(NUM.(0,0)) thus represents a game which records when A and B win
-- successive games, we can abbreviate it as
55
56
Scorer = Game(NUM.(0,0))
57
58
-- Type ":probe Scorer" to animate this process.
2.1. Getting Started
5
FDR Manual, Release 4.2.0
59
-- Type ":graph Scorer" to show the transition system of this process
60
61
-- We can compare this process with some others:
62
63
64
65
assert Scorer [T= STOP
assert Scorer [F= Scorer
assert STOP [T= Scorer
66
67
-- The results of all these are all obvious.
68
69
-- Also, compare the states of this process
70
71
72
assert Scorer [T= Game(NUM.(15,0))
assert Game(NUM.(30,30)) [FD= Game(Deuce)
73
74
75
-- The second of these gives a result you might not expect: can you explain why?
-- (Answer below....)
76
77
78
79
80
81
------
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:
82
83
84
85
86
87
88
ND = pointA -> ND |~| pointB -> ND
89
90
-- We can imagine one where B gets at least one point every time A gets one:
91
92
Bgood = pointA -> pointB -> Bgood |~| pointB -> Bgood
93
94
95
-- and one where B gets two points for every two that A get, so allowing A to
-- get two consecutive points:
96
97
Bg = pointA -> Bg1 |~| pointB -> Bg
98
99
Bg1 = pointA -> pointB ->
Bg1 |~| pointB -> Bg
100
101
102
assert Bg [FD= Bgood
assert Bgood [FD= Bg
103
104
105
-- 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?
106
107
108
BgoodS = Bgood [|{pointA,pointB}|] Scorer
BgS = Bg [|{pointA,pointB}|] Scorer
109
110
111
assert STOP [T= BgoodS \diff(Events,{gameA})
assert STOP [T= BgS \diff(Events,{gameA})
112
113
114
115
-- 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.
116
6
Chapter 2. The FDR User Interface
FDR Manual, Release 4.2.0
117
118
119
-- 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:
120
121
122
Level = gameA -> Awinning(1)
[] gameB -> Bwinning(1)
123
124
Awinning(1) = gameB -> Level -- A not permitted to win here
125
126
127
128
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)
129
130
assert Level [T= BgS \{pointA,pointB}
131
132
133
-- 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.
134
135
-- Games of tennis can of course go on for ever, as is illustrated by the check
136
137
assert BgS\{pointA,pointB} :[divergence-free]
138
139
140
-- Notice that here, for the infinite behaviour that is a divergence, the
-- debugger shows you a loop.
141
142
143
-- Finally, the answer to the question above about the similarity of
-- Game(NUM.(30,30)) and Game(Deuce).
144
145
146
147
148
149
150
-------
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
151
152
153
154
155
156
157
transparent sbisim, wbisim, diamond
158
159
BScorer = sbisim(Scorer)
160
161
-- Note that FDR automatically applies bisimulation in various places.
162
163
164
-- To see how effective compressions can sometimes be, but that
-- sometimes one compression is better than another compare
165
166
NDS = (ND [|{pointA,pointB}|] Scorer)\{pointA,pointB}
167
168
169
170
wbNDS = wbisim(NDS)
sbNDS = sbisim(NDS)
nNDS = sbisim(diamond(NDS))
2.1. Getting Started
7
FDR Manual, Release 4.2.0
2.2 Session Window
The main window of the GUI is the session window, and is illustrated above. The session window provides the main
interface to CSP files, and allows them to be loaded (see load), expressions to be evaluated (see Available Statements)
and assertions run (see The Assertion List). Below, we give an overview of the three main components of the session
window; the Interactive Prompt, the Assertion List and the Task List.
2.2.1 The Interactive Prompt
The GUI is structured around an interactive prompt, in which expressions may be evaluated, new definitions given,
and assertions specified. For example, if FDR was started with Dining Philosophers loaded (i.e. by typing fdr4
phils6.csp from a command prompt), then the following session is possible:
phils6.csp>
1
phils6.csp>
phils6.csp>
24
phils6.csp>
Assertion 5
8
head(<1..>)
let f(x) = 24
f(1)
assert not PHIL(1) [F= PHIL(2)
created (run using :run 5).
Chapter 2. The FDR User Interface
FDR Manual, Release 4.2.0
The command prompt also exposes a number of commands which are prefixed with :. For example, the type of an
expression can be pretty printed using :type:
phils6.csp> :type head
head :: () -> a
In addition, the command prompt has intelligent (at least in some sense) tab completion. For example:
phils6.csp> c
card
concat
phils6.csp> :
assertions debug
processes
quit
graph
reload
help
run
load
type
options
version
The interactive prompt will also indicate when a file has been modified on disk, but has not yet been reloaded, by
suffixing the file name at the prompt with a *.
Available Statements
Expressions can be evaluated by simply typing them in at the prompt. For example, typing 1+1 would print 2. In
order to create a new definition, let can be used as follows:
phils6.csp> let f(x) = x + 1
phils6.csp> let (z, y) = (1, 2)
As with interactive prompts for other languages, each let statement overrides any previous definitions of the same
variables, but does not change the version that previous definitions refer to. For example, consider the following:
phils6.csp>
phils6.csp>
phils6.csp>
phils6.csp>
2
let f = 1
let g = f
let f(x) = g + x
f(1)
In the above, even though f has been re-bound to a function, g still refers to the previous version.
Transparent and external functions can be imported by typing transparent x, y at the prompt:
phils6.csp> normal(STOP)
:1:1-7:
normal is not in scope
Did you mean: normal (import using ’transparent normal’)
phils6.csp> transparent normal
phils6.csp> normal(STOP)
...
New assertions can be created exactly as they would be in a CSP file, by typing assert X [T= Y, or assert
STOP :[deadlock free [F]]. For example:
phils6.csp> assert not PHIL(1) [F= PHIL(2)
Assertion 5 created (run using :run 5).
Available Commands
There are a number commands available at the command prompt that expose various pieces of functionality. Note that
all commands below may be abbreviated, providing the abbreviation is unambiguous. For example, :assertions
may be abbreviated to :a, but :reload cannot be abbreviated to :r as this could refer to :run.
2.2. Session Window
9
FDR Manual, Release 4.2.0
command :assertions
Lists all of the currently defined assertions. For example, assuming that Dining Philosophers is loaded:
phils6.csp> :assertions
0: SYSTEM :[deadlock free [F]]
1: SYSTEMs :[deadlock free [F]]
2: BSYSTEM :[deadlock free [F]]
3: ASSYSTEM :[deadlock free [F]]
4: ASSYSTEMs :[deadlock free [F]]
The index displayed on the left is the index that should be used for other commands that act on assertions (such
as debug).
command :communication_graph
Given a CSP expression that evaluates to a process, displays the communication graph of the process, as per
Communication Graph Viewer.
command :counterexample
Assuming that the given assertion has been checked and fails, pretty prints a textual represenation of the counterexamples to the specified assertion.
command :cd
Changes the current directory that files are loaded from. This will affect subsequent calls to load.
command :debug
Assuming that the given assertion has been checked and fails, opens the Debug Viewer on the counterexample
to the specified assertion.
command :graph
Given a CSP expression that evaluates to a process, displays a graph of the process in the Process Graph Viewer.
By default, the process will be compiled in the failures-divergences model but a specific model can be specified,
for example, by typing :graph [Model] P, where the model is specified as per assertions. For example,
:graph [F] P will cause the failures model to be used.
command :help
Displays the list of available commands and gives a short description for each.
command :help
Displays more verbose help about the given command, which should be given without a :. For example :help
type displays the help about the type command.
command :load
Loads the specified file, discarding any definitions or assertions that were given at the prompt.
command :options
See options list.
command :options get Source Exif Data:
File Type : PDF File Type Extension : pdf MIME Type : application/pdf PDF Version : 1.5 Linearized : No Page Count : 174 Page Mode : UseOutlines Warning : Duplicate 'Author' entry in dictionary (ignored) Author : University of Oxford Title : FDR Manual Subject : Creator : LaTeX with hyperref package Producer : pdfTeX-1.40.16 Create Date : 2016:12:20 13:53:05Z Modify Date : 2016:12:20 13:53:05Z Trapped : False PTEX Fullbanner : This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015) kpathsea version 6.2.1EXIF Metadata provided by EXIF.tools