A.6 Special Definitions

A.6.1 External

External definitions are used to enable additional ‘magic’ functions supported by a specific tool. Requiring a definition, rather than silently inserting names into the initial environment, has two advantages: any dependencies on such functions are made explicit and there is no possibility that users will introduce conflicting definitions without being aware of it. For example, to make use of an (imaginary) frobnicate external function, we might say

external frobnicate
P(s) = c!frobnicate(s^<0>, 7) -> STOP

Without the external definition, frobnicate would be reported as an undeclared identifier. Tools should report as an error any attempt to define an external name which they do not recognise.

A.6.2 Transparent

FDR 1.9 introduced the notion of compression operators into CSP_M(see section Methods of compression). These are used to reduce the state-space or otherwise optimise the underlying representation of a process within FDR. While these could be defined using external definitions, they are required to be semantically neutral. It is thus safe for tools which do not understand the compression operations to ignore them. By defining them as transparent, tools are able to do so; unrecognised external operations would be treated as errors. As an example,

transparent diamond, normalise
squidge(P) = normalise(diamond(P))

enables the diamond and normalise compression operators in FDR, while other tools see definitions of the identity functions, as if we had written

diamond(P) = P
normalise(P) = P
squidge(P) = normalise(diamond(P))

A.6.3 Assert

Assertions are used to state properties which are believed to hold of the other definitions in a script. (FDR1 scripts adopted a convention of defining two processes SPEC and SYSTEM, with the understanding that the check SPEC[=SYSTEM should be performed. This has weaknesses: the correct model for the check is not always apparent, and some scripts require multiple checks.) The most basic form of the definition is

assert b

where b is a boolean expression. For example,

primes        = ...
take(0,_)     = <>
take(n,<x>^s) = <x> ^ take(n-1,s)
assert <2,3,5,7,11> == take(5, primes)

It is also possible to express refinement checks (typically for use by FDR)

assert p [m= q

where p and q are processes and m denotes the model: T for traces, F or FD for failures and failures-divergences, R or RD for Refusal Testing and Refusal Testing-divergences, V or VD for Revival Testing and Revival Testing-divergences and TP for the tau priority model. The set of prioritised events for the tau priority model is specified after the process:

assert P [= Q :[ tau priority over ]: tocks

where tocks is a set of events.

Similarly, we have

assert p :[ deterministic [FD] ]
assert p :[ deadlock free [F] ]
assert p :[ divergence free ]

for the other supported checks within FDR. Only the models F and FD may be used with the first two, with FD assumed if the model is omitted.

All assertions can be negated by prefixing them with not. This allows scripts to be constructed where all checks are expected to succeed (useful when a large number of checks are to be performed.)

Note that process tests cannot be used in any other context. The process assertions in a script are used to initialise the list of checks in FDR.

A.6.4 Print

Print definitions indicate expressions to be evaluated. The standard tools in the CSP_Mdistribution include ‘check’ which evaluates all (non-process) assertions and print definitions in a script. This can be useful when debugging problems with scripts. FDR uses any print definitions to initialise the list of expressions for the evaluator panel.

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