Relational Modeling and Reasoning with Multisets and Multirelations in Alloy

Multisets and multirelations arise naturally in modeling. In contrast, while ordinary sets and relations are first-class citizens in the Alloy environment, Alloy does not provide a direct way to work with multisets and multirelations. In this report, we present a sound and practical mathematical framework which encodes multisets and multirelations using only ordinary sets and total functions. We implement the encoding as a mutliconcepts library in Alloy which is declarative, compatible with ordinary sets and relations, and can be incorporated into existing models seamlessly.