A Comparison of the Declarative Modelling Languages B, Dash, and TLA+

Abstract

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+, with a new modelling language called Dash. Dash is an extension of Alloy with explicit syntactic constructs for modelling transition systems, and it includes control state hierarchy and events. Particular topics that we cover in our comparison are: differences in the datatypes and type systems; how the transitions/operations can be described; how the transition relation is a combination of the transitions; and the default choice each language makes regarding permitted variable changes in a transition. Our goal is to discuss the interesting differentiating characteristics of each language to aid users in determining which language is the most suitable for their system.