Modeling and Reasoning with Multisets and Multirelations in Alloy

Abstract

Multisets and multirelations arise naturally in modeling; however, most modeling languages either have limited or completely lack support for multisets and multirelations. Alloy, for instance, is a lightweight relational modeling language which provides automatic analysis of models. In Alloy, ordinary sets and relations are the only first-class language semantic constructs; therefore to work with multisets and multirelations, modelers need to invent ad-hoc ways to encode these multiconcepts or rely on a third-party library that provides their implementations, assuming there is such one. In fact, such a library has been missing for Alloy, and implementing a fully functional multiconcepts library is challenging, especially when it is required to encode an algebra of operations over multiconcepts. This thesis presents two sound and practical mathematical formalizations of multiconcepts, namely, index-based and multiplicity-based, which encode multisets and multirelations using only basic concepts such as ordinary sets, total functions and natural numbers. We implement two generic multiconcepts libraries in Alloy based on the corresponding formalizations. Each library has a carefully designed interface and can be seamlessly integrated into existing relational models. We also perform an empirical evaluation on both implementations; the result shows multiplicity-based encoding is more scalable in terms of performance; thus, it is more preferable in practice.