API Examples

For each language a simple command line tool has been produced that will check all assertions in a file, and then print the counterexample that is produced. This includes dividing the counterexample into sub-behaviours of the various components of the system. You may use these files as the basis of your integration into FDR3.

The files below (namely, command_line.cc, CommandLine.java and command_line.py) are hereby placed in the public domain. This means that any parts of these files may be incorporated into your own files that you then license under different means.

C++

Compilation instructions: g++ -std=c++11 -I/opt/fdr/include -L/opt/fdr/lib -lfdr -o libfdr_demo command_line.cc.

Download

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
#include <iostream>

#include <fdr/fdr.h>

/// Pretty prints the specified behaviour to stdout
static void describe_behaviour(
    const FDR::Session& session,
    const FDR::Assertions::DebugContext& debug_context,
    const FDR::Assertions::Behaviour& behaviour,
    unsigned int indent,
    const bool recurse)
{
    // Describe the behaviour type
    std::cout << std::string(indent, ' ') << "behaviour type: ";
    indent += 2;
    if (dynamic_cast<const FDR::Assertions::ExplicitDivergenceBehaviour*>(&behaviour))
        std::cout << "explicit divergence after trace";
    else if (dynamic_cast<const FDR::Assertions::IrrelevantBehaviour*>(&behaviour))
        std::cout << "irrelevant";
    else if (auto loop =
            dynamic_cast<const FDR::Assertions::LoopBehaviour*>(&behaviour))
        std::cout << "loops after index " << loop->loop_index();
    else if (auto min_acceptance =
        dynamic_cast<const FDR::Assertions::MinAcceptanceBehaviour*>(&behaviour))
    {
        std::cout << "minimal acceptance refusing {";
        for (const FDR::LTS::CompiledEvent event : min_acceptance->min_acceptance())
            std::cout << session.uncompile_event(event)->to_string() << ", ";
        std::cout << "}";
    }
    else if (auto segmented =
        dynamic_cast<const FDR::Assertions::SegmentedBehaviour*>(&behaviour))
    {
        std::cout << "Segmented behaviour consisting of:\n";
        // Describe the sections of this behaviour. Note that it is very
        // important that false is passed to the the descibe methods below
        // because segments themselves cannot be divded via the DebugContext.
        // That is, asking for behaviour_children for a behaviour of a
        // SegmentedBehaviour is not allowed.
        for (const std::shared_ptr<FDR::Assertions::Behaviour>& child :
                segmented->prior_sections())
            describe_behaviour(session, debug_context, *child, indent + 2, false);
        describe_behaviour(session, debug_context, *segmented->last(),
            indent + 2, false);
    }
    else if (auto trace = dynamic_cast<const FDR::Assertions::TraceBehaviour*>(&behaviour))
        std::cout << "performs event " << session.uncompile_event(trace->error_event())->to_string();
    std::cout << std::endl;

    // Describe the trace of the behaviour
    std::cout << std::string(indent, ' ') << "Trace: ";
    for (const FDR::LTS::CompiledEvent event : behaviour.trace())
    {
        if (event == FDR::LTS::INVALID_EVENT)
            std::cout << "-, ";
        else
            std::cout << session.uncompile_event(event)->to_string() << ", ";
    }
    std::cout << std::endl;

    // Describe any named states of the behaviour
    std::cout << std::string(indent, ' ') << "States: ";
    for (const std::shared_ptr<FDR::LTS::Node>& node : behaviour.node_path())
    {
        if (node == nullptr)
            std::cout << "-, ";
        else
        {
            std::shared_ptr<FDR::Evaluator::ProcessName> process_name =
                session.machine_node_name(*behaviour.machine(), *node);
            if (process_name == nullptr)
                std::cout << "(unknown), ";
            else
                std::cout << process_name->to_string() << ", ";
        }
    }
    std::cout << std::endl;

    // Describe our own children recursively
    if (recurse)
    {
        for (const std::shared_ptr<FDR::Assertions::Behaviour>& child :
                debug_context.behaviour_children(behaviour))
        {
            describe_behaviour(session, debug_context, *child, indent + 2, true);
        }
    }
}

/// Pretty prints the specified counterexample to stdout
static void describe_counterexample(
    const FDR::Session& session,
    const FDR::Assertions::Counterexample& counterexample)
{
    // Firstly, just print a simple description of the counterexample
    std::cout << "Counterexample type: ";
    if (dynamic_cast<const FDR::Assertions::DeadlockCounterexample*>(
            &counterexample))
        std::cout << "deadlock";
    else if (dynamic_cast<const FDR::Assertions::DeterminismCounterexample*>(
                &counterexample))
        std::cout << "determinism";
    else if (dynamic_cast<const FDR::Assertions::DivergenceCounterexample*>(
                &counterexample))
        std::cout << "divergence";
    else if (auto min_acceptance =
            dynamic_cast<const FDR::Assertions::MinAcceptanceCounterexample*>(
                &counterexample))
    {
        std::cout << "minimal acceptance refusing {";
        for (const FDR::LTS::CompiledEvent event : min_acceptance->min_acceptance())
            std::cout << session.uncompile_event(event)->to_string() << ", ";
        std::cout << "}";
    }
    else if (auto trace =
            dynamic_cast<const FDR::Assertions::TraceCounterexample*>(
                &counterexample))
        std::cout << "trace with event " << session.uncompile_event(
            trace->error_event())->to_string();
    else
        std::cout << "unknown";
    std::cout << std::endl;

    // In order to print the children we use a DebugContext. This allows for
    // division of behaviours into their component behaviours, and also ensures
    // proper alignment amongst the child components.
    if (auto refinement_counterexample =
            dynamic_cast<const FDR::Assertions::RefinementCounterexample*>(
                &counterexample))
    {
        std::cout << "Children:" << std::endl;
        FDR::Assertions::DebugContext debug_context(*refinement_counterexample,
            false);
        debug_context.initialise(nullptr);
        describe_behaviour(session, debug_context,
            *debug_context.root_behaviours()[0], 2, true);
        describe_behaviour(session, debug_context,
            *debug_context.root_behaviours()[1], 2, true);
    }
    else if (auto property_counterexample =
            dynamic_cast<const FDR::Assertions::PropertyCounterexample*>(
                &counterexample))
    {
        std::cout << "Children:" << std::endl;
        FDR::Assertions::DebugContext debug_context(*property_counterexample,
            false);
        debug_context.initialise(nullptr);
        describe_behaviour(session, debug_context,
            *debug_context.root_behaviours()[0], 2, true);
    }
}

/// The actual main function.
static int real_main(int& argc, char**& argv)
{
    if (!FDR::has_valid_license())
    {
        std::cout << "Please run refines or FDR4 to obtain a valid license before running this." << std::endl;
        return EXIT_FAILURE;
    }
        
    std::cout << "Using FDR version " << FDR::version() << std::endl;

    if (argc != 2)
    {
        std::cerr << "Expected exactly one argument." << std::endl;
        return EXIT_FAILURE;
    }

    const std::string file_name = argv[1];

    std::cout << "Loading " << file_name << std::endl;

    FDR::Session session;
    try
    {
        session.load_file(file_name);
    }
    catch (const FDR::FileLoadError& error)
    {
        std::cout << "Could not load. Error: " << error.what() << std::endl;
        return EXIT_FAILURE;
    }

    // Check each of the assertions
    for (const std::shared_ptr<FDR::Assertions::Assertion>& assertion
            : session.assertions())
    {
        std::cout << "Checking: " << assertion->to_string() << std::endl;
        try
        {
            assertion->execute(nullptr);
            std::cout
                << (assertion->passed() ? "Passed" : "Failed")
                << ", found " << assertion->counterexamples().size()
                << " counterexamples" << std::endl;

            // Pretty print the counterexamples
            for (const std::shared_ptr<FDR::Assertions::Counterexample>&
                    counterexample : assertion->counterexamples())
            {
                describe_counterexample(session, *counterexample);
            }
        }
        catch (const FDR::InputFileError& error)
        {
            std::cout << "Could not compile: " << error.what() << std::endl;
            return EXIT_FAILURE;
        }
    }

    return EXIT_SUCCESS;
}

int main(int argc, char** argv)
{
    FDR::library_init(&argc, &argv);

    int return_code = real_main(argc, argv);

    FDR::library_exit();

    return return_code;
}

Java

Compilation instructions:

javac -classpath /opt/fdr/lib/fdr.jar CommandLine.java
java -classpath /opt/fdr/lib/fdr.jar:. CommandLine

Download

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
import java.io.File;
import java.io.PrintStream;
import uk.ac.ox.cs.fdr.*;

public class CommandLine {

public static void main(String argv[]) {
    int returnCode;
    try {
        returnCode = realMain(argv);
    }
    finally {
        // Shutdown FDR
        fdr.libraryExit();
    }

    System.exit(returnCode);
}

/**
 * The actual main function.
 */
private static int realMain(String[] argv)
{
    PrintStream out = System.out;
    
    if (!fdr.hasValidLicense())
    {
        out.println("Please run refines or FDR4 to obtain a valid license before running this.");
        return 1;
    }

    out.println("Using FDR version "+ fdr.version());

    if (argv.length != 1) {
        out.println("Expected exactly one argument.");
        return 1;
    }

    String fileName = argv[0];
    out.println("Loading "+ fileName);

    Session session = new Session();
    try {
        session.loadFile(fileName);
    }
    catch (FileLoadError error) {
        out.println("Could not load. Error: "+error.toString());
        return 1;
    }

    // Check each of the assertions
    for (Assertion assertion : session.assertions()) {
        out.println("Checking: "+assertion.toString());
        try {
            assertion.execute(null);
            out.println(
                (assertion.passed() ? "Passed" : "Failed")
                +", found "+(assertion.counterexamples().size())
                +" counterexamples");

            // Pretty print the counterexamples
            for (Counterexample counterexample : assertion.counterexamples()) {
                describeCounterexample(out, session, counterexample);
            }
        }
        catch (InputFileError error) {
            out.println("Could not compile: "+error.toString());
            return 1;
        }
    }

    return 0;
}

/**
 * Pretty prints the specified counterexample to out.
 */
private static void describeCounterexample(PrintStream out, Session session,
    Counterexample counterexample)
{
    // Firstly, just print a simple description of the counterexample
    //
    // This uses dynamic casting to check the assertion type.
    out.print("Counterexample type: ");
    if (counterexample instanceof DeadlockCounterexample)
        out.println("deadlock");
    else if (counterexample instanceof DeterminismCounterexample)
        out.println("determinism");
    else if (counterexample instanceof DivergenceCounterexample)
        out.println("divergence");
    else if (counterexample instanceof MinAcceptanceCounterexample)
    {
        MinAcceptanceCounterexample minAcceptance =
            (MinAcceptanceCounterexample) counterexample;
        out.print("minimal acceptance refusing {");
        for (Long event : minAcceptance.minAcceptance())
            out.print(session.uncompileEvent(event).toString() + ", ");
        out.println("}");
    }
    else if (counterexample instanceof TraceCounterexample)
    {
        TraceCounterexample trace = (TraceCounterexample) counterexample;
        out.println("trace with event "+ session.uncompileEvent(
            trace.errorEvent()).toString());
    }
    else
        out.println("unknown");

    out.println("Children:");

    // In order to print the children we use a DebugContext. This allows for
    // division of behaviours into their component behaviours, and also ensures
    // proper alignment amongst the child components.
    DebugContext debugContext = null;

    if (counterexample instanceof RefinementCounterexample)
        debugContext = new DebugContext((RefinementCounterexample) counterexample, false);
    else if (counterexample instanceof PropertyCounterexample)
        debugContext = new DebugContext((PropertyCounterexample) counterexample, false);

    debugContext.initialise(null);
    for (Behaviour root : debugContext.rootBehaviours())
        describeBehaviour(out, session, debugContext, root, 2, true);
}

/**
 * Prints a vaguely human readable description of the given behaviour to out.
 */
private static void describeBehaviour(PrintStream out, Session session,
    DebugContext debugContext, Behaviour behaviour, int indent,
    boolean recurse)
{
    // Describe the behaviour type
    printIndent(out, indent); out.print("behaviour type: ");
    indent += 2;
    if (behaviour instanceof ExplicitDivergenceBehaviour)
        out.println("explicit divergence after trace");
    else if (behaviour instanceof IrrelevantBehaviour)
        out.println("irrelevant");
    else if (behaviour instanceof LoopBehaviour)
    {
        LoopBehaviour loop = (LoopBehaviour) behaviour;
        out.println("loops after index " + loop.loopIndex());
    }
    else if (behaviour instanceof MinAcceptanceBehaviour)
    {
        MinAcceptanceBehaviour minAcceptance = (MinAcceptanceBehaviour) behaviour;
        out.print("minimal acceptance refusing {");
        for (Long event : minAcceptance.minAcceptance())
            out.print(session.uncompileEvent(event).toString() + ", ");
        out.println("}");
    }
    else if (behaviour instanceof SegmentedBehaviour)
    {
        SegmentedBehaviour segmented = (SegmentedBehaviour) behaviour;
        out.println("Segmented behaviour consisting of:");
        // Describe the sections of this behaviour. Note that it is very
        // important that false is passed to the the descibe methods below
        // because segments themselves cannot be divded via the DebugContext.
        // That is, asking for behaviourChildren for a behaviour of a
        // SegmentedBehaviour is not allowed.
        for (TraceBehaviour child : segmented.priorSections())
            describeBehaviour(out, session, debugContext, child, indent + 2, false);
        describeBehaviour(out, session, debugContext, segmented.last(),
            indent + 2, false);
    }
    else if (behaviour instanceof TraceBehaviour)
    {
        TraceBehaviour trace = (TraceBehaviour) behaviour;
        out.println("performs event " +
            session.uncompileEvent(trace.errorEvent()).toString());
    }

    // Describe the trace of the behaviour
    printIndent(out, indent); out.print("Trace: ");
    for (Long event : behaviour.trace())
    {
        // INVALIDEVENT indiciates that this machine did not perform an event at
        // the specified index (i.e. it was not synchronised with the machines
        // that actually did perform the event).
        if (event == fdr.INVALIDEVENT)
            out.print("-, ");
        else
            out.print(session.uncompileEvent(event).toString() + ", ");
    }
    out.println();

    // Describe any named states of the behaviour
    printIndent(out, indent); out.print("States: ");
    for (Node node : behaviour.nodePath())
    {
        if (node == null)
            out.print("-, ");
        else
        {
            ProcessName processName = session.machineNodeName(behaviour.machine(), node);
            if (processName == null)
                out.print("(unknown), ");
            else
                out.print(processName.toString()+", ");
        }
    }
    out.println();

    // Describe our own children recursively
    if (recurse) {
        for (Behaviour child : debugContext.behaviourChildren(behaviour))
            describeBehaviour(out, session, debugContext, child, indent + 2, true);
    }
}

/**
 * Prints a number of spaces to out.
 */
private static void printIndent(PrintStream out, int indent) {
    for (int i = 0; i < indent; ++i)
        out.print(' ');
}

}

Python

Execute using python command_line.py.

Download

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
import os
import platform
import sys

fdr_to_use = None
if sys.argv[1].startswith("--fdr="):
    fdr_to_use = sys.argv[1][len("--fdr="):]
    del sys.argv[1]
elif platform.system() == "Linux":
    for bin_dir in os.environ.get("PATH", "").split(":"):
        fdr4_binary = os.path.join(bin_dir, "fdr4")
        if os.path.exists(fdr4_binary):
            real_fdr4 = os.path.realpath(os.path.join(bin_dir, "fdr4"))
            fdr_to_use = os.path.join(os.path.basename(os.path.basename(real_fdr4)), "lib")
            break
elif platform.system() == "Darwin":
    for app_dir in ["/Applications", os.path.join("~", "Applications")]:
        if os.path.exists(os.path.join(app_dir, "FDR4.app")):
            fdr_to_use = os.path.join(app_dir, "FDR4.app", "Contents", "Frameworks")
            break

print fdr_to_use
sys.path.append(fdr_to_use)
import fdr

def main():
    fdr.library_init()
    return_code = real_main()
    fdr.library_exit()
    sys.exit(return_code)

def real_main():
    if not fdr.has_valid_license():
        print "Please run refines or FDR4 to obtain a valid license before running this."
        return 1
    
    print "Using FDR version %s" % fdr.version()

    if len(sys.argv) != 2:
        print "Expected exactly one argument."
        return 1

    file_name = sys.argv[1];
    print "Loading %s" % file_name

    session = fdr.Session()
    try:
        session.load_file(file_name)
    except fdr.FileLoadError, error:
        print "Could not load. Error: %s" % error
        return 1

    # Check each of the assertions
    for assertion in session.assertions():
        print "Checking: %s" % assertion
        try:
            assertion.execute(None)
            print "%s, found %s counterexamples" % \
                ("Passed" if assertion.passed() else "Failed",
                    len(assertion.counterexamples()))

            # Pretty print the counterexamples
            for counterexample in assertion.counterexamples():
                describe_counterexample(session, counterexample)
        except fdr.InputFileError, error:
            print "Could not compile: %s" % error
            return 1

    return 0

"""
Pretty prints the specified counterexample to out.
"""
def describe_counterexample(session, counterexample):
    # Firstly, just print a simple description of the counterexample
    if isinstance(counterexample, fdr.DeadlockCounterexample):
        t = "deadlock"
    elif isinstance(counterexample, fdr.DeterminismCounterexample):
        t = "determinism"
    elif isinstance(counterexample, fdr.DivergenceCounterexample):
        t = "divergence"
    elif isinstance(counterexample, fdr.MinAcceptanceCounterexample):
        t = "minimal acceptance refusing {"
        for event in counterexample.min_acceptance():
            t += str(session.uncompile_event(event)) + ", "
        t += "}"
    elif isinstance(counterexample, fdr.TraceCounterexample):
        t = "trace with event "+str(session.uncompile_event(
                counterexample.error_event()))
    else:
        t = "unknown"

    print "Counterexample type: "+t
    print "Children:"

    # In order to print the children we use a DebugContext. This allows for
    # division of behaviours into their component behaviours, and also ensures
    # proper alignment amongst the child components.
    debug_context = fdr.DebugContext(counterexample, False)
    debug_context.initialise(None)

    for behaviour in debug_context.root_behaviours():
        describe_behaviour(session, debug_context, behaviour, 2, True)

"""
Prints a vaguely human readable description of the given behaviour to out.
"""
def describe_behaviour(session, debug_context, behaviour, indent, recurse):
    # Describe the behaviour type
    indent += 2;
    if isinstance(behaviour, fdr.ExplicitDivergenceBehaviour):
        print "%sbehaviour type: explicit divergence after trace" % (" "*indent)
    elif isinstance(behaviour, fdr.IrrelevantBehaviour):
        print "%sbehaviour type: irrelevant" % (" "*indent)
    elif isinstance(behaviour, fdr.LoopBehaviour):
        print "%sbehaviour type: loops after index %s" % (" "*indent, behaviour.loop_index())
    elif isinstance(behaviour, fdr.MinAcceptanceBehaviour):
        s = ""
        for event in behaviour.min_acceptance():
            s += str(session.uncompile_event(event)) + ", "
        print "%sbehaviour type: minimal acceptance refusing {%s}" % (" "*indent, s)
    elif isinstance(behaviour, fdr.SegmentedBehaviour):
        print "%sbehaviour type: Segmented behaviour consisting of:" % (" "*indent)
        # Describe the sections of this behaviour. Note that it is very
        # important that false is passed to the the descibe methods below
        # because segments themselves cannot be divded via the DebugContext.
        # That is, asking for behaviourChildren for a behaviour of a
        # SegmentedBehaviour is not allowed.
        for child in behaviour.prior_sections():
            describe_behaviour(session, debug_context, child, indent + 2, False)
        describe_behaviour(session, debug_context, behaviour.last(), indent + 2, False)
    elif isinstance(behaviour, fdr.TraceBehaviour):
        print "%sbehaviour type: loops after index %s" % (" "*indent,
            session.uncompile_event(behaviour.error_event()))

    # Describe the trace of the behaviour
    t = ""
    for event in behaviour.trace():
        if event == fdr.INVALID_EVENT:
            t += "-, "
        else:
            t += str(session.uncompile_event(event)) + ", "
    print "%sTrace: %s" % (" "*indent, t)

    # Describe any named states of the behaviour
    t = ""
    for node in behaviour.node_path():
        if node == None:
            t += "-, "
        else:
            process_name = session.machine_node_name(behaviour.machine(), node)
            if process_name == None:
                t += "(unknown), "
            else:
                t += str(process_name)+", "
    print "%sStates: %s" % (" "*indent, t)

    # Describe our own children recursively
    if recurse:
        for child in debug_context.behaviour_children(behaviour):
            describe_behaviour(session, debug_context, child, indent + 2, recurse)

if __name__ == "__main__":
    main()