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

[Chen Fu <chen...@xxxxxxxxx>]

I've removed Java 8 from the system and installed Java 6. I am also using the one bit spec from beginning of the hyper book. Still facing the same problem: I can not specify initial predicate and next state relation. the radio button is stuck at "No Behavior Spec".

---------------------------- MODULE OneBitClock ----------------------------

　

=============================================================================

\* Modification History

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

\* Created Fri Apr 24 13:25:41 PDT 2015 by chenfu

VARIABLE b

Init1 == (b=0) \/ (b=1)

Next1 == \/ /\ b = 0

                  /\ b' = 1

              \/ /\ b = 1

                /\ b' = 0

On Fri, Apr 24, 2015 at 12:52 PM, Chen Fu <chen...@xxxxxxxxx> wrote:

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

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.