If you are modeling in text (which is a good thing) why not use something like alloy (http://alloy.mit.edu/) which is far more expressive and can be analyzed and checked automatically.