# The FDR Command-Line Interface¶

In addition to the graphical interface, FDR also exposes a command-line interface. Whilst this is not particularly useful as a standalone tool, primarily due to the difficulty in navigating counterexamples, it can be useful for quickly checking if assertions pass. More importantly, the command-line tool can also produce machine-readable output (in either JSON, XML or YAML), providing an easy way of integrating FDR into other tools. The command-line version can also be executed on clusters, enabling massive problems to be tackled.

On Linux the command-line tool can be invoked simply as refines (providing the standard installation instructions have been followed). Under Mac OS X, the command line tool can be invoked by launching /Applications/FDR4.app/Contents/MacOS/refines, assuming that FDR has been installed to /Applications/.

## Command-Line Flags¶

refines takes as input a list of files and will check all assertions in all files. For example:

$refines a.csp b.csp  will cause refines to load a.csp, check all assertions in it, then load b.csp and then check all assertions. If the filename is set to -, then refines will then read from stdin. For instance: $ refines - < a.csp


will cause refines to check assertions in a.csp, since it is piped into stdin.

refines takes various option flags, as follows

--archive <output_file>

If this option is specified then FDR will read in the specified CSP file, calculate all files that it includes, and then save all of these into a single compressed file named output_file. output_file may subsequently be loaded by refines in the normal way. For example:

$refines --archive phils.arch phils6.csp Saved phils8.csp (and all depdendent files) to phils.arch$ refines phils.arch
Log:
Found 50 processes including 7 names
...


This is intended to help running refines on a remote server since only the single combined archive needs to be transferred, rather than all files that the root file includes. For example:

$refines --archive phils.arch phils6.csp$ scp phils.arch server:phils.arch
$ssh server "refines phils.arch"  would execute refines on the computer named server. --brief, -b If this option is included then only the result of each assertion is printed, rather than a description of the counterexample. See also --divide, -d If selected, any counterexample that is generated will be split and the behaviours of component machines will also be output (as per the Debug Viewer). See also --format <format>, -f <format> Specifies the output format, which must be one of: colour This is the default mode. This pretty-prints texts in a human-readable format and uses some colours to highlight text printed to the terminal. plain As per colour, but no colours are used. json Outputs machine-readable JSON, as described below in Machine-Readable Formats. framed_json This is as per the json format, but instead outputs one complete JSON object after each assertion or print statement. See Machine-Readable Formats for further details. xml Outputs machine-readable XML, as described below in Machine-Readable Formats. yaml Outputs machine-readable YAML, as described below in Machine-Readable Formats. --help, -h Prints the list of command-line flags that are available. --quiet, -q This suppresses all the progress logging that FDR normally generates. --remote <ssh_host> This causes refines to check the assertions on the specified remote host, using SSH. refines will connect to the specified server, upload the script (including any scripts it includes), and then invokes refines on the remote server. For example: $ refines --remote myserver phils6.csp


would cause refines to use SSH to connect to myserver and then invoke refines on the remote server in order to check all assertions in phils6.csp.

The --remote option can be used to specify an arbitrary sequence of options to ssh. For instance:

$refines --remote '-o "PubkeyAuthentication=yes" -p 1000 user@remote' phils6.csp  would mean refines invoked ssh as ssh -o "PubkeyAuthentication=yes" -p 1000 user@remote> (along with some other options to start refines on the remote server). In order to use this comand, ssh (or ssh.exe on Windows) must be available on your$PATH, and refines must be available on your $PATH on the remote server. The version of refines does not need to exactly match the version on the remote server, but should be similar. See also refines --remote-path in order to change the path to refines on the remote server. --remote-path <path> This can be used to specify the path to refines on the remote server when using refines --remote. For example: $ refines --remote myserver --remote-path /var/bin/refines phils6.csp


would cause /var/bin/refines to be invoked on the remote server, rather than refines.

refines --remote for further details on how to invoke refines with the --remote option.

--reveal-taus

If selected, will print the top-level trace of the system with all taus revealed. That is, any tau in the counterexample that is a tau that resulted from hiding will be revealed and the event that was hidden given instead.

For example, consider the following CSP script:

channel a, b

P = a -> b -> STOP

assert STOP [T= P \ {a}


Running refines on this file using the above option would print:

Trace: <τ>
Error Event: b
Unhidden trace: <a>


which indicates that the first tau was an a.

--typecheck, -t

Typecheck the file arguments and exit.

--version, -v

Prints the version of the current version of FDR.

Further, any of the options that are available in the GUI, listed in Options can also be specified from the command line by replacing each . or _ in the option name with a -. For example, refinement.storage.compressor can be set to Zip by adding the argument --refinement-storage-compressor Zip.

## Examples¶

The following causes FDR to check all assertions in the file, outputting as much information as possible.

$refines phils6.csp SYSTEM :[deadlock free [F]]: Log: Found 50 processes including 7 names Visited 43 processes and discovered 6 recursive names Constructed 0 of 1 machines Constructed 0 of 2 machines Constructed 0 of 3 machines ...  The next example will cause FDR to check all assertions in the file, but suppresses all logging (due to refines --quiet) and causes only a summary of the results to be produced (due to refines --brief). $ refines --brief --quiet phils6.csp


This example supresses all logging, but will cause FDR to pretty-print counterexamples to any assertions that fail. FDR will also divide the counterexamples to give behaviours for each subprocess of the main process (thus allowing each component’s contribution to the error to be deduced).

$refines --divide --quiet phils6.csp SYSTEM :[deadlock free [F]]: Log: Result: Failed Visited States: 181 Visited Transitions: 493 Visited Plys: 9 Counterexample (Deadlock Counterexample) Implementation Debug: SYSTEM (Failure Behaviour): Trace: <thinks.1, sits.1, thinks.0, thinks.2, sits.2, sits.0, picks.1.1, picks.0.0, picks.2.2> Min Acceptance: {} Component Behaviours: ...  ## Using a Cluster¶ refines can also be executed on clusters using MPI <http://www.mpi-forum.org/> in the standard way. For example: $ mpiexec refines phils6.csp


will execute refines on whatever cluster mpiexec is configured to use. Note that all other options for refines, including those that control machine- readable output, function as normal.

For optimal performance, refines should be executed on a cluster with a high-performance interconnect and consisting of homogeneous compute nodes (i.e. with the same number and speed of cores). Further, exactly one copy of refines should be executed on each physical server. refines will still use all of the cores, but will use a more efficient communication algorithm for communication with other threads on the same physical node.

For example, to execute refine on two homogeneous nodes node001 and node002, the following could be used:

$mpiexec -hosts node001,node002 refines --refinement-cluster-homogeneous true phils6.csp  Note that refinement.cluster.homogeneous has been set to true. This option should always be specified when using a homogeneous cluster, since it makes FDR assume the cluster is homogeneous. If it is not specified there is a small chance FDR may fail to detect the homogeneity of the cluster, leading to suboptimal performance. The required interconnect speed depends on the problem, but in our experience, if each node in the cluster has 8 cores, the interconnect needs to be able to support 750 Mb/s (e.g. gigabit Ethernet), whilst if each node has 16 cores, the interconnect needs to support 1500 Mb/s (e.g. 10-gigabit Ethernet, or InfiniBand). See also refines --archive If your CSPM scripts make use of Include Files, then refines --archive can help when transferring files over to a cluster since it packages all files, including all files that are included, into a single compressed archive. For example: $ refines --archive phils.arch phils6.csp
$scp phils.arch cluster-master:phils.arch$ ssh cluster-master "mpiexec -hosts node001,node002 refines --refinement-cluster-homogeneous true phils.arch"


would execute FDR on the cluster consisting of node001 and node002.

Warning

At the present time, only checks in the traces and failures models will take full advantage of the cluster mode as parallelising divergence checking has not be parallelised to take advantage of multiple machines in an optimal way.

### Supported MPI Versions¶

Currently the cluster version of refines only supports Linux running one of the following MPI distributions:

The usage of MPICH 3.1 (or any other MPI3 compliant distribution) is strongly recommended, particularly on larger clusters.

Further, FDR4 requires that the MPI distribution has support for multi-threaded applications (in particular MPI_THREAD_FUNNELED). When running under mvapich, this requires -env IPATH_NO_CPUAFFINITY 1 -env MV2_ENABLE_AFFINITY 0 to be passed to mpiexec.

### Using Cloud Computing Services¶

Amazon’s EC2 is ideally suited to being used for FDR. In particular, Amazon’s support for Enhanced Networking (i.e. 10-gigabit Ethernet) and the availability of Placement Groups (which guarantee optimal network performance between compute nodes) means that they are ideal hosts for FDR. In particular, the large r3.4xlarge (8 cores) and r3.8xlarge (16 cores) provide an excellent balance of memory and compute power for refines.

Creating and optimally configuring a cluster on Amazon is complex. We recommend the use of StarCluster, which can automatically setup and configure a cluster on EC2. You may use the following starcluster configuration as a starting point for a FDR-compatible cluster. Note the presence of SUBNET_ID and VPC_ID: in order for Enhanced Networking to function correctly, the nodes in the cluster must be part of VPC on Amazon. The StarCluster user guide can provide more help on this point.

[cluster fdr]
CLUSTER_SIZE = ...
NODE_INSTANCE_TYPE = r3.8xlarge
DNS_PREFIX = True
NODE_IMAGE_ID = ami-52a0c53b
SUBNET_ID = ...
VPC_ID = ...
PLUGINS = mpich2, mpich3, pkginstaller, sge
DISABLE_QUEUE = True

[plugin mpich2]
SETUP_CLASS = starcluster.plugins.mpich2.MPICH2Setup

[plugin sge]
# Don't use the default SGE setup because we only want one slot per node
SETUP_CLASS = starcluster.plugins.sge.SGEPlugin
SLOTS_PER_HOST = 1

[plugin pkginstaller]
SETUP_CLASS = starcluster.plugins.pkginstaller.PackageInstaller
PACKAGES = language-pack-en

[plugin mpich3]
SETUP_CLASS = mpich3.MPICH3Setup


This also requires the following plugin, which builds mpich3 from source, to be installed to ~/.starcluster/plugins/mpich3.py:

from starcluster.clustersetup import ClusterSetup
from starcluster.logger import log

class MPICH3Setup(ClusterSetup):
def _configure_node(self, node):
env_file = node.ssh.remote_file('/etc/profile.d/mpich3.sh', 'w')
env_file.close()

def run(self, nodes, master, user, user_shell, volumes):
log.info("Building mpich 3.1.1 from source")
master.ssh.execute("""
tar xzvf mpich-3.1.1.tar.gz
cd mpich-3.1.1
make -j16
make install
""")
log.info("Setting environment on all nodes...")
for node in nodes:
self._configure_node(node)

def on_add_node(self, node, nodes, master, user, user_shell, volumes):
self._configure_node(node)

from starcluster.clustersetup import ClusterSetup
from starcluster.logger import log

class FDR4Setup(ClusterSetup):
def _configure_node(self, node):
node.ssh.execute("apt-get update")
node.ssh.execute("apt-get install fdr")

def run(self, nodes, master, user, user_shell, volumes):
log.info("Installing FDR4 on each node")
for node in nodes:
pool.simple_job(self._configure_node, (node), jobid=node.alias)

def on_add_node(self, node, nodes, master, user, user_shell, volumes):
self._configure_node(node)


Other cloud computing services are only suitable if they can guarantee extremely high performance connections between the compute nodes in the cluster (multi gigabit sustained throughput for each node, and very low latency).

Warning

Before deciding to use the machine-readable interface to FDR, please firstly consider using the FDR API instead, which allows for more thorough integration.

When a machine-readable format is selected (i.e. when refines --format is set to framed_json, json, xml or yaml, e.g. refines --format json file.csp), the behaviour of refines is slightly modified, as follows. Firstly, errors and warnings that are generated as a result of the input script are no-longer sent to stderr, but instead are included as part of the machine-readable output. Errors that result from incorrect command-line flags being passed are still sent to stderr. If refines --quiet is not specified, then log messages are now sent to stderr. The machine-readable output is sent to stdout. The exit code for refines will be 0 precisely when valid machine-readable output has been generated, and a value other than 0 indicates some sort of catastrophic error, either as a result of incorrect flags being passed or a runtime crash (check stderr for more information). In particular, an error in the input CSP script, or a failing assertion, will result in an exit code of 0 and the errors will be included as part of the machine-readable output.

The machine-readable output consists essentially of a number of key-value pairs, specified in either JSON, XML or YAML. The format of the various element types is specified below. The top-level element of the output (the element type is file in XML) and is documented in Files.

If refines --format is set to framed_json, then the behaviour of refines is further altered. Normally, if refines were to be killed, or crashed, when the JSON format is specified, then only a partially-formed JSON object will be output. This means that any assertion results that were already finished are essentially lost. The framed_json format is designed to avoid this problem. Instead of outputing a JSON document only when all assertions and print statements are checked, it outputs a fully formed JSON object after each assertion or print statement. Thus, the results for the ith assertion are contained in the ith file object.

The delimiter between the different files is a single LF character (i.e. \\n). This means the output can be parsed as follows:

for document in fdr_output.split('\n'):


Each JSON document is a fully formed File object, as documented in Files. However, each File object will contain the results of precisely one assertion or print statement.

### Files¶

The top-level element in the output conceptually represents an input file, and has the following properties.

Element Meaning
errors A list of errors that were generated in response to loading the file.
event_map

For various reasons, FDR internally represents events as integers. Thus, in the counterexamples below all events are actually integers, rather than strings. This element contains a map from each integer event to the corresponding string representation.

Warning

In the case of JSON the keys to this map are actually strings, rather than integers since JSON requires all keys to be strings.

In the case of XML, the map is represented by a series of elements of the form <i_40>done</i_40>, which indicates that the event 40 maps to the string done. This is to compensate for the fact that XML does not allow elements to start with numbers.

Warning

No guarantees are provided about the order of the keys in the map. The only guarantee that is provided is that each key will appear in the map at most once.

file_name The name of the file that was loaded.
results A list of assertion results, the format of which is described below. This will be empty if errors was non-empty. The results will appear in the same order as the assertions in the original file.
print_statement_results A list of results from evaulating print statements, the format of which is described below. As with results, this will be empty if errors was non-empty, and the results will appear in the same order as the print statements in the original file.
warnings A list of warnings that were generated when loading the file.

For example, executing refines --quiet --format=json phils6.csp will result in the following JSON to be produced:

{
"errors": [],
"event_map": {
"13": "thinks.1",
"14": "sits.1",
...
},
"file_name": "phils6.csp",
"results": [
...
],
"print_statement_results": [],
"warnings": []
}

Examples of the result section are given below.

### Assertion Results¶

Each item in the results list of Files will contain the following fields.

Element Meaning
assertion_string A string representation of the assertion.
counterexamples An list of counterexamples to the assertion. If the assertion failed (i.e. result is 0) or the assertion passed but is_negated is 1, this will be non-empty. Otherwise it will be empty. The keys that this contains are specified below.
errors A list of errors that were encountered whilst compiling the assertion. If this list is non-empty then none of the following elements will be present.
is_negated This will be 1 if the assertion is of the form assert not and 0 otherwise.
result This will be 1 if the assertion passes and 0 otherwise. Note that if the assertion is negated and the inner assertion fails, then this will be 1.
visited_plys An integer giving the number of plys that were visited in the breadth-first search.
visited_states An integer giving the number of states visited during the search.
visited_transitions An integer giving the number of transitions that were visited.

For example, executing refines --quiet --format=json phils6.csp and extracting the first element of the results array will give the following JSON:

{
"counterexamples": [
...
],
"errors": [],
"is_negated": 0,
"result": 0,
"visited_plys": 9,
"visited_states": 181,
"visited_transitions": 493
},

The contents of an element of the counterexamples list are given below.

### Counterexample¶

A counterexample to an assertion conceptually consists of a behaviour of the implementation that violates the assertion in some way. A counterexample element contains the following fields.

Element Meaning
implementation_behaviour A Behaviour of the implementation that the specification cannot perform. The format of this is specified below.
specification_behaviour A Behaviour of the specification. The format of this is specified below. This item is only present when the assertion is a refinement assertion, or a determinism assertion; for all other assertions (such as deadlock and divergence free assertions), this will not be present.
type

A string representing the type of the counterexample. This will either be:

This is generated as a counterexample to a :[deadlock free] assertion and indicates that the implementation can deadlock after a certain trace (or, if the failures-divergences model is being used, that the implementation can diverge). In this case, specification_behaviour is not present since its behaviour is not relevant.
determinism
This is generated in response to a :[determinism] assertion, and indicates that the implementation can diverge after a certain trace. In this case, specification_behaviour and implementation_behaviour are not really behaviours of the specification and the implementation, but instead are two behaviours that demonstrate non-determinism in the implementation process. Either: one behaviour will be a trace behaviour (indicating it can perform a certain visible event) and once behaviour will be an acceptance behaviour, indicating that the process can refuse the event; or one behaviour will be a divergence behaviour and the other will be an irrelevant trace behaviour.
divergence
This is generated in response to a :[divergence free] assertion, and indicates that the implementation can diverge after a certain trace. In this case, specification_behaviour is not present since its behaviour is not relevant.
refinement_divergence
This is generated in response to a violation of a failures-divergences refinement assertion, and indicates that the implementation can diverge after a certain trace, but the specification cannot.
failure
This indicates that this counterexample is from a failing failures check. Hence, the implementation can refuse to perform events that the specification does not allow to be refused.
trace
This indicates that the implementation can perform a trace that the specification cannot.

For example, executing refines --quiet --format=json phils6.csp and extracting the first element of the counterexamples array from the JSON example given in Assertion Results will give the following JSON:

{
"implementation_behaviour": ...,
}

The contents of the implementation_behaviour value are given below.

### Behaviour¶

Conceptually, a behaviour of a machine (i.e. a process) is a trace that it can perform, along with some action that it can perform after performing the trace that is of interest. For example, a behaviour may indicate that the machine can diverge after a certain trace, or that it accept only a certain set of events, etc. A behaviour element has the following fields:

Element Meaning
child_behaviours If refines --divide is specified and this machine is divisible, this will consist of an array of behaviours of the subprocesses of this machine. For example, if this behaviour is a behaviour of P ||| Q, then this would have two elements, one representing P and the other representing Q.
machine_name If this behaviour is a behaviour of a machine whose name is known (i.e. this is a behaviour of a process that is defined as P = X ||| Y in the input file), this this field contains a string representation of the process name.
trace

This is an array of integers that represent the events that lead up to the actual behaviour. Note that unlike traces from CSP theory, this may include taus.

Note that FDR aligns all traces (as seen in the Debug Viewer), meaning that if you have two behaviours then their trace lengths are guaranteed to be the same. Further, if two behaviours both perform an event at some index i and neither is the child of the other, then it must be the case that the two events are synchronised somehow. In order to ensure that all traces are identical, FDR inserts the event 0 in traces to indicate that this machine does not contribute to this event and does not change state. For example, consider:

channel a, b

P = a -> a -> STOP
Q = a -> b -> a STOP

assert a -> b -> STOP [T= P [| {a} |] Q


A counterexample to this will have implementation_behaviour being a trace behaviour with trace <a, b> and error event a. Its two children will have traces <a, 0> and <a, b> respectively. This indicates that both components synchronise on the a, but the second component performs the b independently of the first.

revealed_trace This field is only present if refines --reveal-taus is specified and this is the top-level implementation behaviour. If so, then this will be as per trace, but any taus that resulted from hiding will be revealed and the original visible event printed instead.
type

This indicates the type of the behaviour, and will be one of the following strings:

divergence
This indicates that the process can diverge having performed the trace. There are no extra properties of the behaviour in this case.
loop
This indicates that the process can repeat some suffix of the trace infinitely often. In this case the field loop_start contains an integer that specifies the index at which the repeat starts. For example, if loop_start was 0 then this indicates the machine can repeat the entire trace, whilst a value of 1 means that it can repeat all but the first event. This often appears when dividing divergence counterexamples.
min_acceptance
This indicates that the process will only accept a certain set of events having performed the trace. The set of events that it accepts is given by the acceptance field, which is a list of integers corresponding to the events that it accepts. This will appear either in a deadlock counterexample where the acceptance field will be the empty array for the top-most implementation behaviour (indicating that it accepts no events, i.e. it deadlocks). It also appears during failure counterexamples.
segmented

This behaviour type appears when counterexamples involving processes such as P = normal(Q) ; P are discovered. In this case FDR will have, most likely, compiled these to [recursive high-level machines](@ref compiler_machine_types). It is possible for a behaviour of P to require several loops around Q. Such behaviours are represented by segmented behaviours. Conceptually, these consist of a series of sections, which are themselves behaviours, that the machine performs in sequence. Thus, segmented behaviours have two extra fields:

last_section
A behaviour that is the last behaviour the machine performs. This is the behaviour that will exhibit the counterexample to the assertion (i.e. this behaviour may be a divergence, loop etc.).
prior_sections
A list of behaviour elements, all of which are guaranteed to have type trace. The machine performs these in order. The error_event in each of the behaviours is what causes the machine to change to the next segment.

For example, consider:

channel a
transparent normal
Q = a -> SKIP
P = normal(Q) ; P
assert a -> STOP [T= P


A counterexample to the above consists of the implementation behaviour where a is performed after performing the trace <a, τ> (where the τ comes from the ). This is represented by the following segmented behaviour:

{
"child_behaviours": [],
"last_section": {
"error_event": "a",
"machine_name": "normal(Q)",
"trace": [],
"type": "trace"
},
"machine_name": "normal(Q)",
"prior_sections": [
{
"error_event": "✓",
"machine_name": "normal(Q)",
"trace": [
"a"
],
"type": "trace"
}
],
"trace": [
"a",
"✓"
],
"type": "segmented"
}


Note in the above the integers that represent the event have been replaced by strings to ease explanation.

trace
This indicates that the machine can perform a particular event of interest having performed the trace. The event it performs is included in the field error_event. If this event is 0, this indicates that the machine did not contribute to the event in question. For example, the behaviour that violates assert STOP [T= STOP ||| a -> STOP will be a trace behaviour with error event a. This will have two child behaviours (one for STOP and one for a -> STOP), the first of which will be a trace behaviour with error event 0 since it does not contribute to the a.

For example, executing refines --quiet --format=json phils6.csp and extracting the implementation_behaviour of the counterexample element in the JSON example given in Counterexample will give the following JSON:

{
"acceptance": [],
"child_behaviours": [
...
]
"machine_name": "SYSTEM",
"trace": [
13,
14,
...
],
"type": "min_acceptance"
}

### Code Examples¶

The following Python program invokes refines and will check all of the assertions in the given file, printing out limited debug information. This can be used as a skeleton for calling refines.

# Used for parsing the output of refines
import json
# Used to invoke refines
import subprocess
# For accessing command line arguments
import sys

path_to_refines = "refines"

def run_fdr(file_to_check):
print "Running FDR on", file_to_check
# Documented at
# http://docs.python.org/2/library/subprocess.html#subprocess.Popen
fdr_process = subprocess.Popen([path_to_refines, "--format=json", file_to_check],
stdout = subprocess.PIPE, stderr = subprocess.PIPE)

# We launch FDR inside a try block to catch a user pressing CTRL+C and
# then terminate FDR. If we did not do this FDR would continue running
# in the background
try:
# Documented at
# http://docs.python.org/2/library/subprocess.html#subprocess.Popen.communicate
(stdout, stderr) = fdr_process.communicate()
except KeyboardInterrupt:
fdr_process.terminate()
# Re-throw the exception
raise

print "Finished"

if fdr_process.returncode == 0:
print "Log data was:"
print stderr

for error in parsed_data["errors"]:
print "Error:", error
for warning in parsed_data["warnings"]:
print "Warning:", error

# If we generated results (if there were errors above this would not
# be present)
if "results" in parsed_data:
for assertion in parsed_data["results"]:
print "Assertion:", assertion["assertion_string"]
# If the assertion has errors then we emit those.
if "errors" in assertion:
print "    Errors during assertion"
for error in assertion["errors"]:
print "Error:", error
else:
print "    Visited States:", assertion["visited_states"]
print "    Passed:", assertion["result"] == 1
else:
# Since FDR exited with a non-zero exit code we cannot parse the
# data on stdout, since it may well be malformed.
print "Failed - exit code", fdr_process.returncode

if __name__ == "__main__":
if len(sys.argv) != 2:
print "Please specify exactly one file"
else:
run_fdr(sys.argv[1])


Note

We would welcome contributions of similar examples in other languages.