Constraining ocra expressions

[norro]

Add constraints for ocra expressions (some of them redundant to nusmv expressions), to exclude them from polluting nusmv models. That is:

• Allow ocra expressions only in ocra roots (can be child of)
• Disallow redundant nusmv expressions in ocra