An old article I wrote for WF2 and ModelCHECK. Forgive the non-native format, and the age of the document. However it may be useful to those still on WF2. I need to update this for WF4/5
