hello world post pcal calc

tlaplus/gossip/hello.cfg

@@ -0,0 +1,2 @@
+SPECIFICATION Spec
+\* Add statements after this line.

tlaplus/gossip/hello.old

@@ -0,0 +1,8 @@
+EXTENDS TLC
+
+(* --algorithm hello_world
+variable s \in  {"Hello", "World!"};
+begin
+  A:
+    print s;
+end algorithm; *)

tlaplus/gossip/hello.tla

@@ -5,4 +5,29 @@ variable s \in  {"Hello", "World!"};
 begin
   A:
     print s;
-end algorithm; *)
+end algorithm; *)
+\* BEGIN TRANSLATION
+VARIABLES s, pc
+
+vars == << s, pc >>
+
+Init == (* Global variables *)
+        /\ s \in {"Hello", "World!"}
+        /\ pc = "A"
+
+A == /\ pc = "A"
+     /\ PrintT(s)
+     /\ pc' = "Done"
+     /\ s' = s
+
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == pc = "Done" /\ UNCHANGED vars
+
+Next == A
+           \/ Terminating
+
+Spec == Init /\ [][Next]_vars
+
+Termination == <>(pc = "Done")
+
+\* END TRANSLATION