For example I have defined a property isOk of type boolean. If a value edited by the user is not true or false it's highlighted in red. Thus it's shown as an error. But if I build my model it says successful, even though the model checker level is at its highest level. Is this intended to act like this? Do I need to define a constraint for each boolean datatype to let the model checker recognize this as an error or do I need to build my own bool datatype to satisfy my needs?