C.3 Object model

C.3.1 Notes on the object model

Making use of this information will require access to good Tcl documentation. We use Ousterhout’s own "Tcl and the Tk Toolkit" (ISBN 0-201-63337).

The object model presented by FDR through Tcl was constructed to meet Formal Systems’ internal requirements and has since been extended with certain user-requested operations. The model is neither complete nor minimal; not all of FDR’s functionality is made available, and that which is available may be accessible in multiple ways. Furthermore, this documentation does not list all of the available commands, merely those which are likely to be useful.

The commands are all provided in an object-oriented style, as described on page 283 of Ousterhout. They were added using Wayne Christopher’s objectify tool. As a consequence, all the objects feature built-in help for all their commands. However, using commands which are not documented here is strongly discouraged.

The Tcl objects are associated with objects inside the FDR engine. Unless the Tcl objects are explicitly deleted, these objects will persist inside the engine, consuming resources. This may be signficant when performing several memory-intensive checks.

To start FDR without a GUI, use

fdr2tix -insecure -nowindow

The first flag prevents the use of a slave interpreter, while the second forces the use of the Tcl startup code, rather than Tk.

C.3.2 Session objects

Sessions with FDR are created by the session command which returns the name of the new session.

session load dirname scriptname

Loads the specified script into the compiler, after changing to the specified directory. Normally the script name will not contain any path components, so all include directives are interpreted relative to the directory containg the first script. No value is returned.

session compile process model

Compiles process in the environment defined by the current loaded script. A script must have been loaded, even if process contains only builtin process terms. Any symbols which have special meaning to Tcl will, in general, need to be escaped. The return value is the name of the new ism.

The model is specified by using a -t or -f flag for the traces and failures model respectively. If no flag is supplied then the failures-divergences model is assumed.

C.3.3 Ism objects

The ism objects encapsulate state-machines. They are produced by the compile method of a session. The first group of supported operations build hypotheses which can be tested. They all return the name of the new hypothesis.

ism refinedby ism model

Builds a hypothesis which checks for refinement between the two state-machines in the model described by the flag. The same model must be used to compile both the machines and to perform the check.

ism deadlockfree model

Builds a hypothesis which checks that the state-machine cannot deadlock. The same model must be used to compile the machine and perform the check (the traces model is not permitted.)

ism deterministic model

Builds a hypothesis which checks that the state-machine is deterministic. The same model must be used to compile the machine and perform the check (the traces model is not permitted.)

ism livelockfree

Builds a hypothesis which checks that the state-machine cannot livelock. The machine must have been compiled in the failures-divergences model.

The second group of commands allow simple enumeration of a state-machine.

ism transitions

Returns the transitions of the state-machine as a list of three-integer lists. Each triple contains the source and destination state within the machine, separated by the number of an event which links them. The machine is initially in state 0.

ism acceptances

Returns the minimal acceptances of the state-machine as a list of list of list of event numbers, one for each state.

ism divergences

Returns a list of 0/1 values indicating whether each state in the machine is divergent. (1 indicates that it is divergent.)

ism event number

Returns the name of the event corresponding the the given number.

ism compress method model

Returns a new ism which is the result of compressing the existing machine using the named method. The compressions available are precisely those which can be enabled by transparent definitions (for example, normal calls the normalisation routine.) The model may be specified for those compressions where it is signicant, in which case it must match the model used to compile the machine.

ism numeric_initials node

Returns an FDRSet containing the initials of the ism for the given node number. The starting node is node 0.

The final group of commands allow decomposition of a state-machine as an operator tree.

ism operator

Returns the name of the outermost operator. Current names include "parallel", "link", "sharing", "rename" and "hide". If a machine cannot be decomposed then "leaf" is returned. Code using this call should treat all unrecognised names as if they were "leaf"; far more operator names are used internally than are documented here.

Given a recognised operator name, the component machines and wiring sets can be extracted using the next two commands.

ism parts

Returns the sub-machines which make up this one (as a list of ism names.) The three parallel operators both return two machine names corresponding to their left and right process arguments. Hiding and renaming return the single machine name corresponding to their process argument.

ism wiring

Return a list of lists of event numbers representing the event sets associated with the operator.

‘share’

A single list is returned corresponding to the synchronisation set. This set currently includes "_tick".

‘hide’

A single list is returned corresponding to the set of events being hidden.

‘parallel’

Two lists are returned corresponding to the left and right synchronisation set. Both sets currently include "_tick".

‘link’

Two lists of the same length are returned. The corresponding events from each list are to be synchonized and hidden.

‘rename’

Two lists of the same length are returned. Any occurrence of events in the first list is to be replaced by the corresponding event(s) in the second.

C.3.4 Hypothesis objects

Hypotheses represent potential checks which FDR could perform. They correspond to the list of checks displayed in the main FDR window. They are produced by methods on ism objects (deadlockfree, for instance).

hypothesis assert

This starts the check and returns a string indicating the result. Possible return values are

true

xtrue

result is true

false

xfalse

result is false

broken

check completed, but result was unsound

The distinction between true/xtrue and false/xfalse is meaningful only when debugging.

C.3.5 FDRSet objects

FDRSets are sets of ints which are implemented using FDR’s internal set representation. This allows much faster interaction with FDR than translating the set into a tcl representation and back again.

Except for insert, all of the methods on an FDRSet object are functional in nature; that is they return a newly created value, without modifying their arguments.

FDRSet insert list(int)

Inserts the list of ints given as an argument into this FDRSet object.

FDRSet union FDRSet

Returns the union of this FDRSet and the argument.

FDRSet diff FDRSet

Returns the set difference of this FDRSet and the argument.

FDRSet inter FDRSet

Returns the intersection of this FDRSet and the argument.

FDRSet equals FDRSet

Returns true if the contents of this FDRSet and the argument are equal.

FDRSet contents

Return the contents of the FDRSet as a tcl list.

This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.