Fun fact: the author of these rules (Gerard Holzmann) is also the inventor of the Spin model checker (spinroot.com)!