The FDR Command-Line Interface¶

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
SYSTEM :[deadlock free [F]]:
  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

refines --divide, refines --reveal-taus

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

refines --brief, refines --reveal-taus

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

See also

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.

See also

refines --brief, refines --divide

--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
SYSTEM :[deadlock free [F]]: Failed
SYSTEMs :[deadlock free [F]]: Failed
BSYSTEM :[deadlock free [F]]: Passed
ASSYSTEM :[deadlock free [F]]: Passed
ASSYSTEMs :[deadlock free [F]]: Passed

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).

[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

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.write("PATH=/home/sgeadmin/mpich3/bin:$PATH\n")
        env_file.close()

    def run(self, nodes, master, user, user_shell, volumes):
        log.info("Building mpich 3.1.1 from source")
        master.ssh.execute("""
            cd /home/sgeadmin
            wget http://www.mpich.org/static/downloads/3.1.1/mpich-3.1.1.tar.gz
            tar xzvf mpich-3.1.1.tar.gz
            cd mpich-3.1.1
            ./configure --prefix=/home/sgeadmin/mpich3
            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
from starcluster import threadpool

class FDR4Setup(ClusterSetup):
    def _configure_node(self, node):
        node.ssh.execute("echo \"deb http://www.cs.ox.ac.uk/projects/fdr/downloads/debian/ fdr release\n\" > /etc/apt/sources.list.d/fdr.list")
        node.ssh.execute("wget -qO - http://www.cs.ox.ac.uk/projects/fdr/downloads/linux_deploy.key | apt-key add -")
        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")
        pool = threadpool.get_thread_pool(20, False)
        for node in nodes:
            pool.simple_job(self._configure_node, (node), jobid=node.alias)
        pool.wait(numtasks=len(nodes))

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

Machine-Readable Formats¶

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'):
   file_object = json.loads(document)

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.

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

{
    "assertion_string": "SYSTEM :[deadlock free [F]]",
    "counterexamples": [
        ...
    ],
    "errors": [],
    "is_negated": 0,
    "result": 0,
    "visited_plys": 9,
    "visited_states": 181,
    "visited_transitions": 493
},

{
    "implementation_behaviour": ...,
    "type": "deadlock"
}

channel a, b

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

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

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

{
  "print_statement": "1+1",
  "location": "test.csp:1:1-10",
  "errors": [],
  "result": "2"
}

# 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

        # Parse the machine-readable data
        parsed_data = json.loads(stdout)

        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])