Download Failures-Divergence Refinement

Appendix A: Syntax Reference
61
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 CSPM
distribution 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.