[
Top
]
[
Contents
]
[Index]
[
?
]
Table of Contents
Acknowledgements
1. Introduction
1.1 What is
FDR
?
1.2 The CSP View of the World
1.3 CSP Refinement
1.3.1 Using refinement
1.3.2 Simple buffer example
1.3.3 Checking refinement
1.4 Specification Example
1.4.1 Multiplexed buffer example
2. Using
FDR
2.1 The Main Window
2.2 On-line Help
2.3 File and Model Commands
2.3.1 The
Load
command
2.3.2 The
Reload
command
2.3.3 The
Edit
command
2.3.4 The
All Asserts
command
2.3.5 The
Exit
command
2.4 The Assertion List
2.5 The Process List
2.6 The Tab Pane
2.7 Options
2.8 Tab Bar Commands
2.9 The
FDR
Process Debugger
2.9.1 Debugger menu commands
2.9.2 Viewing process behaviours
2.9.2.1 The process structure
2.9.2.2 The behaviour information
2.10 Interface Conventions
2.10.1 GUI conventions
2.10.2 Keyboard short-cuts
3. Tutorial
3.1 Describing Processes
3.1.1 Sample script for
FDR2
3.2 Using the Checker
3.2.1 Environment
3.2.2 Getting started
3.2.3 Debugging
4. Intermediate
FDR
4.1 Building a Model
4.1.1 Abstract model
4.1.2 Use components
4.2 Tuning for
FDR
4.2.1 Share components
4.2.2 Factor state
4.2.3 Use local definitions
4.3 Choice of Model
5. Advanced Topics
5.1 Using Compressions
5.1.1 Methods of compression
5.1.2 Compressions in context
5.1.3 Hiding and safety properties
5.1.4 Hiding and deadlock
5.2 External Operators
5.2.1 Chase
5.2.2 Prioritise
5.3 Technical Details
5.3.1 Generalised Transition Systems
5.3.2 State-space Reduction
5.3.2.1 Computing semantic equivalence
5.3.2.2 Diamond elimination
5.3.2.3 Combining techniques
A. Syntax Reference
A.1 Expressions
A.1.1 Identifiers
A.1.2 Numbers
A.1.3 Sequences
A.1.4 Sets
A.1.5 Booleans
A.1.6 Tuples
A.1.7 Local definitions
A.1.8 Lambda terms
A.2 Pattern Matching
A.3 Types
A.3.1 Simple types
A.3.2 Named types
A.3.3 Datatypes
A.3.4 Subtypes
A.3.5 Channels
A.3.6 Closure operations
A.4 Processes
A.5 Operator Precedence
A.6 Special Definitions
A.6.1 External
A.6.2 Transparent
A.6.3 Assert
A.6.4 Print
A.7 Mechanics
A.8 Missing Features
B. Changes to FDR
B.1 Changes from FDR1 to FDR2
B.2 Changes from 2.0 to 2.1
B.3 Changes from 2.1 to 2.20
B.4 Changes from 2.20 to 2.22
B.5 Changes from 2.22 to 2.23
B.6 Changes from 2.23 to 2.24
B.7 Changes from 2.24 to 2.25
B.8 Changes from 2.25 to 2.26
B.9 Changes from 2.26 to 2.27
B.10 Changes from 2.27 to 2.28
B.11 Changes from 2.28 to 2.64
B.12 Changes from 2.64 to 2.68
B.13 Changes from 2.68 to 2.69
B.14 Changes from 2.69 to 2.76
B.15 Changes from 2.76 to 2.77
B.16 Changes from 2.77 to 2.78
B.17 Changes from 2.78 to 2.80
B.18 Changes from 2.80 to 2.81
B.19 Changes from 2.81 to 2.82
B.20 Changes from 2.82 to 2.83
B.21 Changes from 2.83 to 2.90
B.22 Changes from 2.90 to 2.91
B.23 Changes from 2.91 to 2.94
C. Direct control of
FDR
C.1 Batch interface
C.2 Script interface
C.3 Object model
C.3.1 Notes on the object model
C.3.2 Session objects
C.3.3 Ism objects
C.3.4 Hypothesis objects
C.3.5 FDRSet objects
D. Configuration
D.1 Environment variables
D.1.1 Location
D.1.2 Tools
D.1.3 Paging
D.2 Performance
E. Multiplexed Buffer Script
F. Bibliography
[
Top
]
[
Contents
]
[Index]
[
?
]
This document was generated by
Phil Armstrong
on
May 17, 2012
using
texi2html 1.82
.