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