Move SetToSeq operator from SVG to SequencesExt.

modules/SVG.tla

@@ -1,5 +1,5 @@
 ----------------------------- MODULE SVG -----------------------------
-EXTENDS Naturals, Sequences, Integers, TLC, FiniteSets
+EXTENDS Naturals, Sequences, SequencesExt, Integers, TLC, FiniteSets
 
 (******************************************************************************)
 (* Helper Operators                                                           *)
@@ -110,14 +110,6 @@ Group(children, attrs) ==
     (* contained in this group.                                               *)
     (**************************************************************************)
     SVGElem("g", attrs, children, "")
-
-SetToSeq(S) == 
-    (**************************************************************************)
-    (* Convert a set to some sequence that contains all the elements of the   *)
-    (* set exactly once, and contains no other elements.                      *)
-    (**************************************************************************)
-    LET Injective(f) == \A x, y \in DOMAIN f : (f[x] = f[y]) => (x = y) IN
-    CHOOSE f \in [1..Cardinality(S) -> S] : Injective(f)
 
 MakeFrame(elem) == 
     (******************************************************************************)

modules/SequencesExt.tla

@@ -2,6 +2,7 @@
 
 LOCAL INSTANCE Sequences
 LOCAL INSTANCE Naturals
+LOCAL INSTANCE FiniteSets
   (*************************************************************************)
   (* Imports the definitions from the modules, but doesn't export them.    *)
   (*************************************************************************)
@@ -13,7 +14,7 @@ ToSet(s) ==
   (* The image of the given sequence s. Cardinality(ToSet(s)) <= Len(s)    *)
   (* see https://en.wikipedia.org/wiki/Image_(mathematics)                 *)
   (*************************************************************************)
-  { s[i] : i \in 1..Len(s) }
+  { s[i] : i \in DOMAIN s }
 
 IsInjective(s) == 
   (*************************************************************************)
@@ -24,6 +25,13 @@ IsInjective(s) ==
   (* This definition is overridden by TLC in the Java class SequencesExt.  *)
   (* The operator is overridden by the Java method with the same name.     *)
   (*************************************************************************)
-  \A i,j \in 1..Len(s): i # j => s[i] # s[j]
+  \A i, j \in DOMAIN s: (s[i] = s[j]) => (i = j)
+
+SetToSeq(S) == 
+  (**************************************************************************)
+  (* Convert a set to some sequence that contains all the elements of the   *)
+  (* set exactly once, and contains no other elements.                      *)
+  (**************************************************************************)
+  CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f)
 
 =============================================================================

tests/SequencesExtTests.tla

@@ -1,5 +1,14 @@
 ------------------------- MODULE SequencesExtTests -------------------------
-EXTENDS Sequences, SequencesExt, Naturals, TLC
+EXTENDS Sequences, SequencesExt, Naturals, TLC, FiniteSets
+
+ASSUME(ToSet(<<>>) = {})
+ASSUME(ToSet(<<1>>) = {1})
+ASSUME(ToSet(<<1,1>>) = {1})
+ASSUME(ToSet(<<1,2,3>>) = {1,2,3})
+ASSUME(ToSet([i \in 1..10 |-> 42]) = {42})
+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(IsInjective(<<>>))
 ASSUME(IsInjective(<<1>>))
@@ -12,4 +21,9 @@ ASSUME(IsInjective([i \in 1..10 |-> {i}]))
 ASSUME(IsInjective([i \in 1..10 |-> {i}]))
 ASSUME(~IsInjective([i \in 1..10 |-> {1,2,3}]))
 
+ASSUME(SetToSeq({}) = <<>>)
+ASSUME(SetToSeq({1}) = <<1>>)
+ASSUME(LET s == {"t","l","a","p","l","u","s"}
+           seq == SetToSeq(s)
+       IN Len(seq) = Cardinality(s) /\ ToSet(seq) = s)
 =============================================================================