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> ccard 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