Declarative behavioural modelling is a powerful modelling paradigm that enables users to model system func- tionality abstractly and concisely. We compare two well-used formal declarative modelling languages, B and TLA+, ...