Dear Chen Fu,
You have discovered two amusing bugs or features:
- The SANY parser does not complain if it tries to parse a file without
a module.
- The Translate PlusCal Algorithm command will translate a PlusCal
algorithm, even if it does not occur inside a module.
Even if I decide that they are bugs, it's unlikely that they will be
fixed soon.
In any case, your problem will be solved by putting your specification
inside a module, which begins something like:
-------- MODULE Name --------
Leslie