add ToBag operator

Author: muenchnerkindl

modules/SequencesExt.tla

@@ -1,5 +1,5 @@
 ---------------------------- MODULE SequencesExt ----------------------------
-EXTENDS Sequences, Naturals, FiniteSets, FiniteSetsExt, Folds, Functions
+EXTENDS Sequences, Naturals, FiniteSets, FiniteSetsExt, Folds, Functions, Bags
 \* TLAPM does not play well with LOCAL INSTANCE, reinstate the following
 \* when that issue is fixed.
 \* LOCAL INSTANCE Sequences
@@ -8,6 +8,7 @@ EXTENDS Sequences, Naturals, FiniteSets, FiniteSetsExt, Folds, Functions
 \* LOCAL INSTANCE FiniteSetsExt
 \* LOCAL INSTANCE Folds
 \* LOCAL INSTANCE Functions
+\* LOCAL INSTANCE Bags
 LOCAL INSTANCE TLC
   (*************************************************************************)
   (* Imports the definitions from the modules, but doesn't export them.    *)
@@ -33,6 +34,12 @@ LOCAL INSTANCE TLC
 ToSet(s) ==
   { s[i] : i \in DOMAIN s }
 
+(**************************************************************************)
+(* Convert a sequence to the bag of its elements.                         *)
+(**************************************************************************)
+ToBag(s) ==
+  [x \in Range(s) |-> Cardinality({i \in DOMAIN s : s[i] = x})]
+
 (**************************************************************************)
 (* Convert a set to some sequence that contains all the elements of the   *)
 (* set exactly once, and contains no other elements.                      *)

tests/SequencesExtTests.tla

@@ -12,6 +12,10 @@ ASSUME(ToSet([i \in 1..10 |-> i]) = 1..10)
 ASSUME(ToSet(Tail([i \in 1..10 |-> i])) = 2..10)
 ASSUME(ToSet([i \in 0..9 |-> 42]) = {42})
 
+ASSUME(ToBag(<<>>) = <<>>)
+ASSUME(ToBag(<<1,2,1>>) = (1 :> 2) @@ (2 :> 1))
+ASSUME(ToBag([i \in 1..10 |-> 42]) = (42 :> 10))
+
 ASSUME(SetToSeq({}) = <<>>)
 ASSUME(SetToSeq({1}) = <<1>>)
 ASSUME(LET s == {"t","l","a","p","l","u","s"}