Search code examples
alloyformal-methods

Are there multisets in Alloy?

Is there a way to model a system using bags(multisets) as well in Alloy? And if there is no explicit notion of bags, is there any possible workaround?

Thanks.

Solution

  • Thanks for all your help but I did it the following way eventually:

    First I restricted my bags to contain only elements with non-zero multiplicity

    module bags

open util/natural
open util/relation

sig Element{}

sig Bag{
    elements: Element -> one Natural
}{
    all e: Element.elements | e != Zero
}

    And coded union/difference/intersection like this:

    fun BagUnion[b1, b2 : Element -> one Natural]: Element -> one Natural{
    let e = (dom[b1] + dom[b2]) | e -> add[e.b1, e.b2]  
}

fun BagDifference[b1, b2 : Element -> one Natural]: Element -> one Natural{
    let e = dom[b1] | e -> max[Zero + sub[e.b1, e.b2]] 
}

fun BagIntersection[b1, b2 : Element -> one Natural]: Element -> one Natural{
    let e = (dom[b1] & dom[b2]) | e -> min[e.b1 + e.b2] 
}