FDR
4.2
Contents
Introduction
Citing FDR
The FDR User Interface
Getting Started
Session Window
Debug Viewer
Process Graph Viewer
Probe
Node Inspector
Communication Graph Viewer
Machine Structure Viewer
Options
The FDR Command-Line Interface
Command-Line Flags
Examples
Using a Cluster
Machine-Readable Formats
CSP
M
Definitions
Functional Syntax
Defining Processes
Type System
Built-In Definitions
Profiling
Integrating FDR into Other Tools
The FDR API
API Examples
Optimising
Overview
Compression
Implementation Notes
Semantic Models
Compilation
Refinement Checking
Type Checking
Release Notes
4.2.7 (11/05/2020)
4.2.6 (10/05/2020)
4.2.5 (27/04/2020)
4.2.4 (19/02/2019)
4.2.3 (26/10/2017)
4.2.2 (09/10/2017)
4.2.1 (19/09/2017)
4.2.0 (20/12/2016)
3.4.0 (09/03/2016)
3.3.1 (17/06/2015)
3.3.0 (15/06/2015)
3.2.1 – 3.2.3 (06/01/2015)
3.2.0 (30/01/2015)
3.1.0 (11/08/2014)
3.0.0 (09/12/2013)
Example Files
FDR4 Introduction
Dining Philosophers
Inductive Compression
References
Licenses
boost
boost.nowide
CityHash
google-sparsehash
graphviz
libcspm
LLVM
lz4
popcount.h
QT
zlib
Haskell
Page
Index
Index
Symbols
|
A
|
B
|
C
|
D
|
E
|
F
|
G
|
H
|
I
|
L
|
M
|
N
|
O
|
P
|
Q
|
R
|
S
|
T
|
U
|
V
|
W
|
Y
Symbols
--archive <output_file>
refines command line option
--brief, -b
refines command line option
--divide, -d
refines command line option
--format <format>, -f <format>
refines command line option
--help, -h
refines command line option
--quiet, -q
refines command line option
--remote <ssh_host>
refines command line option
--remote-path <path>
refines command line option
--reveal-taus
refines command line option
--typecheck, -t
refines command line option
--version, -v
refines command line option
A
a (type)
Alphabetised Parallel (operator)
assert (definition)
:[deadlock free] (definition)
:[deterministic] (definition)
:[divergence free] (definition)
:[has trace] (definition)
:[livelock free] (definition)
not (definition)
refinement (definition)
assertions
deadlock freedom
determinism
divergence
has trace
negated
partial order reduction
refinement
tau priority over
assertions (command)
B
Binary Boolean Function (syntax)
Binary Maths Operation (syntax)
Bool (constant)
(type)
C
card (function)
cd (command)
channel (definition)
CHAOS (function)
Char (constant)
(type)
chase (function)
chase_nocache (function)
Cloud Computing
Cluster
communication_graph (command)
Comparison (syntax)
compiler.check_for_immediate_recursions (option)
compiler.leaf_compression (option)
compiler.recursive_high_level (option)
compiler.reuse_machines (option)
Complete (type constraint)
concat (function)
Concat (syntax)
Concat Pattern (syntax)
constants (definition)
counterexample (command)
cspm.evaluator_heap_size (option)
cspm.profiling.active (option)
cspm.profiling.flatten_recursion (option)
cspm.runtime_range_checks (option)
D
datatype (definition)
Datatype (type)
dbisim (function)
debug (command)
deter (function)
diamond (function)
diff (function)
DIV (function)
Dot (syntax)
(type)
Dot Pattern (syntax)
Dotable (type)
Double Pattern (syntax)
E
EC2
elem (function)
empty (function)
emptyMap (function)
Enumerated Set (syntax)
Enumerated Set Comprehension (syntax)
Eq (type constraint)
Equality Comparison (syntax)
error (function)
Event (type)
Events (constant)
Exception (operator)
explicate (function)
Extendable (type)
extensions (function)
external (definition)
External Choice (operator)
F
failure_watchdog (function)
False (constant)
Function (type)
Function Application (syntax)
functions (definition)
G
Generalised Parallel (operator)
Generator Statement (syntax)
graph (command)
Guarded Expression (operator)
gui.close_windows_on_load (option)
gui.console.history_length (option)
H
head (function)
help (command)
,
[1]
Hide (operator)
I
If (syntax)
include (definition)
Infinite Int List (syntax)
Infinite Int Set (syntax)
Infinite Ranged List Comprehension (syntax)
,
[1]
Int (constant)
(type)
Inter (function)
inter (function)
Interleave (operator)
Internal Choice (operator)
Interrupt (operator)
L
Lambda (syntax)
lazyenumerate (function)
length (function)
Let (syntax)
Linked Parallel (operator)
List (syntax)
List Comprehension (syntax)
List Length (syntax)
List Pattern (syntax)
Literal (syntax)
Literal Pattern (syntax)
load (command)
loop (function)
M
Map (function)
(syntax)
(type)
mapDelete (function)
mapFromList (function)
mapLookup (function)
mapMember (function)
mapToList (function)
mapUpdate (function)
mapUpdateMultiple (function)
member (function)
module (definition)
MPI
mtransclose (function)
N
nametype (definition)
normal (function)
null (function)
O
options (command)
options get (command)
options help (command)
options list (command)
options reset (command)
options set (command)
Ord (type constraint)
P
Parenthesis (syntax)
Parenthesis Pattern (syntax)
partial order reduction
Predicate Statement (syntax)
Prefix (operator)
print (definition)
prioritise (function)
prioritise_nocache (function)
prioritisepo (function)
probe (command)
Proc (constant)
(type)
processes (command)
processes false (command)
productions (function)
profiling_data (command)
Project (operator)
Q
quit (command)
R
Ranged Int List (syntax)
Ranged Int Set (syntax)
Ranged List Comprehension (syntax)
Ranged Set Comprehension (syntax)
refinement.bfs.workers (option)
refinement.cluster.homogeneous (option)
refinement.desired_counterexample_count (option)
refinement.explorer.storage.type (option)
refinement.storage.compressor (option)
refinement.storage.file.cache_size (option)
refinement.storage.file.checksum (option)
refinement.storage.file.compressor (option)
refinement.storage.file.path (option)
refinement.track_history (option)
refines command line option
--archive <output_file>
--brief, -b
--divide, -d
--format <format>, -f <format>
--help, -h
--quiet, -q
--remote <ssh_host>
--remote-path <path>
--reveal-taus
--typecheck, -t
--version, -v
relational_image (function)
relational_inverse_image (function)
reload (command)
Rename (operator)
Replicated Alphabetised Parallel (operator)
Replicated External Choice (operator)
Replicated Generalised Parallel (operator)
Replicated Interleave (operator)
Replicated Internal Choice (operator)
Replicated Linked Parallel (operator)
Replicated Sequential Composition (operator)
Replicated Synchronising Parallel (operator)
run (command)
RUN (function)
S
sbisim (function)
Seq (function)
seq (function)
Sequence (type)
Sequential Composition (operator)
Set (function)
set (function)
Set (syntax)
(type constraint)
(type)
Set Comprehension (syntax)
Set Pattern (syntax)
show (function)
SKIP (constant)
Sliding Choice or Timeout (operator)
statistics (command)
STOP (constant)
structure (command)
subtype (definition)
Supercomputer
Synchronising External Choice (operator)
Synchronising Interrupt (operator)
T
tail (function)
tau_loop_factor (function)
Timed (definition)
timed_priority (function)
trace_watchdog (function)
transparent (definition)
transpose (function)
True (constant)
Tuple (syntax)
(type)
Tuple Pattern (syntax)
type (command)
type annotations (definition)
type expressions
U
Unary Boolean Function (syntax)
Unary Maths Operation (syntax)
Union (function)
union (function)
V
Variable (syntax)
Variable Pattern (syntax)
version (command)
W
WAIT (function)
wbisim (function)
Wildcard Pattern (syntax)
Y
Yieldable (type constraint)