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.

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.

Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.