TYPE multiset{t: type}
INHERIT equality{multiset{t}}
IMPORT frequency FROM sequence{t}
MODEL(n: map{t, nat})
INVARIANT ALL(m: multiset{t} :: default(m.n) = 0)
MESSAGE empty REPLY(m: multiset{t})
WHERE ALL(x: t :: m.n[x] = 0)
MESSAGE add(x: t, m1: multiset{t}) REPLY(m2: multiset{t})
WHERE m2.n[x] = m1.n[x] + 1,
ALL(y: t SUCH THAT y ~= x :: m2.n[y] = m1.n[y])
MESSAGE remove(x: t, m1: multiset{t})
WHEN x IN m1 REPLY(m2: multiset{t})
WHERE m2.n[x] = m1.n[x] - 1,
ALL(y: t SUCH THAT y ~= x :: m2.n[y] = m1.n[y])
OTHERWISE REPLY(m1: multiset{t})
MESSAGE "U"(m1 m2: multiset{t}) REPLY(m3: multiset{t})
WHERE ALL(x: t :: m3.n[x] = m1.n[x] + m1.n[x])
MESSAGE "IN"(x: t, m: multiset{t}) REPLY(b: boolean)
WHERE b <=> m.n[x] > 0
MESSAGE frequency(x: t, m: multiset{t}) REPLY(n: nat)
WHERE n = m.n[x]
MESSAGE size(m: multiset{t}) REPLY(n: nat)
WHERE n = SUM(x: t :: m.n[x])
-- The number of occurrences for all items in the multiset.
MESSAGE domain(m: multiset{t}) REPLY(s: set{t})
WHERE s = domain(m.n)
-- The set of elements that appear in the multiset
-- at least once.
MESSAGE scan(m: multiset{t})
GENERATE(s: sequence{t})
WHERE ALL(x: t :: frequency(x, m) = frequency(x, s))
-- The order of the elements is not specified.
-- Note the overloading of frequency:
-- sequence concept & multiset message.
END