.

Test.tla

@@ -3,22 +3,24 @@ EXTENDS Integers, TLC
 
 S == 1..2
 
+Max(s) == CHOOSE x \in s : \A y \in s : x >= y
+
+
 (***
 --algorithm PrintSet {
   variable X = S;
   {
 e:  print "";
-a:  while (X /= {}) {
-b:    with (x \in X) {
+b:    with (x = Max(X)) {
         print x;
         print X;
         X := X \ {x}
       }
-    }
+
   }
 }
 ***)
-\* BEGIN TRANSLATION (chksum(pcal) = "9746c50d" /\ chksum(tla) = "7a93560d")
+\* BEGIN TRANSLATION (chksum(pcal) = "e2897145" /\ chksum(tla) = "a33ba03b")
 VARIABLES X, pc
 
 vars == << X, pc >>
@@ -29,26 +31,20 @@ Init == (* Global variables *)
 
 e == /\ pc = "e"
      /\ PrintT("")
-     /\ pc' = "a"
-     /\ X' = X
-
-a == /\ pc = "a"
-     /\ IF X /= {}
-           THEN /\ pc' = "b"
-           ELSE /\ pc' = "Done"
+     /\ pc' = "b"
      /\ X' = X
 
 b == /\ pc = "b"
-     /\ \E x \in X:
+     /\ LET x == Max(X) IN
           /\ PrintT(x)
           /\ PrintT(X)
           /\ X' = X \ {x}
-     /\ pc' = "a"
+     /\ pc' = "Done"
 
 (* Allow infinite stuttering to prevent deadlock on termination. *)
 Terminating == pc = "Done" /\ UNCHANGED vars
 
-Next == e \/ a \/ b
+Next == e \/ b
            \/ Terminating
 
 Spec == Init /\ [][Next]_vars
@@ -58,6 +54,3 @@ Termination == <>(pc = "Done")
 \* END TRANSLATION 
 
 =============================================================================
-\* Modification History
-\* Last modified Fri Feb 11 13:45:43 MSK 2022 by kirr
-\* Created Fri Feb 11 13:28:53 MSK 2022 by kirr

Test.toolbox/Test___Model_1.launch

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
     <stringAttribute key="configurationName" value="Model_1"/>
-    <intAttribute key="fpIndex" value="101"/>
+    <intAttribute key="fpIndex" value="97"/>
     <stringAttribute key="modelBehaviorSpec" value="Spec"/>
     <intAttribute key="modelBehaviorSpecType" value="1"/>
     <listAttribute key="modelCorrectnessProperties">