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

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

Thanks Leslie for the quick response. my bad I had not post the complete file, where the spec is inside a MODULE, and here is the top portion I omitted

-------------------------- MODULE UdpMultiPackets --------------------------



\* Modification History

\* Last modified Fri Apr 24 11:13:11 PDT 2015 by chenfu

\* Created Thu Apr 23 16:33:20 PDT 2015 by chenfu

\* This is a multi-packet transportation protocol over UDP

\* A Sender has PckCount number of packets to send to an Receiver, over a

\* unreliable UDP network, which could lose or reorder packets.


\* We want to ensures that under strong fairness (if infinitely often m is

\* in the message queue then it is eventually received), all packets are

\* eventually received.


\* Thanks Dr. Lamport for guidance!

On Fri, Apr 24, 2015 at 12:35 PM, Leslie Lamport <tlapl...@xxxxxxxxx> wrote:

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


You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/Uv7oQ6wYXcc/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.