.

Test.tla

+-------------------------------- MODULE Test --------------------------------
+EXTENDS Integers, TLC
+
+S == 1..2
+
+(***
+--algorithm PrintSet {
+  variable X = S;
+  {
+e:  print "";
+a:  while (X /= {}) {
+b:    with (x \in X) {
+        print x;
+        print X;
+        X := X \ {x}
+      }
+    }
+  }
+}
+***)
+\* BEGIN TRANSLATION (chksum(pcal) = "9746c50d" /\ chksum(tla) = "7a93560d")
+VARIABLES X, pc
+
+vars == << X, pc >>
+
+Init == (* Global variables *)
+        /\ X = S
+        /\ pc = "e"
+
+e == /\ pc = "e"
+     /\ PrintT("")
+     /\ pc' = "a"
+     /\ X' = X
+
+a == /\ pc = "a"
+     /\ IF X /= {}
+           THEN /\ pc' = "b"
+           ELSE /\ pc' = "Done"
+     /\ X' = X
+
+b == /\ pc = "b"
+     /\ \E x \in X:
+          /\ PrintT(x)
+          /\ PrintT(X)
+          /\ X' = X \ {x}
+     /\ pc' = "a"
+
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == pc = "Done" /\ UNCHANGED vars
+
+Next == e \/ a \/ b
+           \/ Terminating
+
+Spec == Init /\ [][Next]_vars
+
+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/.project

+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>Test</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>toolbox.builder.TLAParserBuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>toolbox.natures.TLANature</nature>
+	</natures>
+	<linkedResources>
+		<link>
+			<name>Test.tla</name>
+			<type>1</type>
+			<locationURI>PARENT-1-PROJECT_LOC/Test.tla</locationURI>
+		</link>
+	</linkedResources>
+</projectDescription>

Test.toolbox/.settings/org.lamport.tla.toolbox.prefs

+ProjectRootFile=PARENT-1-PROJECT_LOC/Test.tla
+eclipse.preferences.version=1

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"/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="0Termination"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <stringAttribute key="specName" value="Test"/>
+</launchConfiguration>