This section describes some common uses of spec-directives in migrating from CAST to HAC.
CHECK_CHANNELS production rules may be replaced with exclhi and excllo directives, which are used by hacprsim for built-in checking of mutual exclusion at run-time.
Forced exclusive high/low rings, which used to be inside PRS bodies, were declared as exclhi and excllo. In HAC, they are now the mk_exclhi and mk_excllo spec directives.