[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?"



Ok, I finally got it, I need to put the spec between those lines.

Thanks!

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

The Toolbox is doing exactly what it should with your specification,
which is

   --------------------- MODULE UdpMultiPackets -----------------
  
   ==============================================================

You seem to have a lot of stuff in the file that is not part of your
specification and is ignored, as it should be.

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