[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Can not edit "What is the model" and "What is the behavior spec?"

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 --------