EXTENDS TLC

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