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