Example of composing of a multi-set with a multi-relation

A span from Bundle to Item.

abstract Bundle
contains ->> Item +

Two bundles.

B1 : Bundle
[ contains in Bread ]
[ # contains = 2 ]
B2 : Bundle
[ contains = Milk, Butter ]

And three items.

abstract Item
Bread : Item
Butter : Item
Milk : Item

A family of bundles

abstract bundles ->> Bundle
bundlesIB1 : bundles ->> B1 2
bundlesIB2 : bundles ->> B2

A family to represent the result of the composition bundles ; contains.

allItem ->> Item 6..*

Escape to Alloy to compose allItem = bundles ; contains:

[alloy|
fact {
  compose 
  [ c0_bundles,  c0_bundles_ref                   // family
  , c0_contains, ~r_c0_contains, c0_contains_ref  // span
  , c0_allItem,  c0_allItem_ref                   // family
  ]
}

pred compose[
  idx: univ, i_elem: idx->univ,                 // family
  hd:  univ, sleg:   hd->univ,  tleg: hd->univ, // span
  res: univ, r_elem: res->univ]                 // family
{
  some idx && some hd    // why is it needed? we should be able to compose empty families and spans as well
  some r1: res->idx | some r2: res->hd |
   all a: idx, b: hd |
    a.i_elem = b.sleg implies { one r: res | r.r1 = a && r.r2 = b } &&
    #res = #(idx<:i_elem).~(hd<:sleg) &&
    res<:r_elem = r2.(hd<:tleg)
}
|]

Next, we elaborate the model to illustrate the composition of two multi-relations.