Relational Modeling and Reasoning with Multisets and Multirelations in Alloy

TitleRelational Modeling and Reasoning with Multisets and Multirelations in Alloy
Publication TypeReport
Year of Publication2016
AuthorsSun, P., Z. Diskin, M. Antkiewicz, and K. Czarnecki
Document NumberGSDLAB-TR 2016-01-22
Abstract

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.

AttachmentSize
TR.pdf593.27 KB
multi.als2.29 KB
mset.als959 bytes
mrel.als1.18 KB
Bundling model and visulization.zip3.76 KB
test-suite.zip4.05 KB