Re: [tlaplus] Re: my first tla program

[TLA Plus <tlapl...@xxxxxxxxx>]

Dear Bert_emme,

 

A casual glance at your specification indicates that it is not correct.  Here is what I recommend that you do.

 

1. Stop using instantiation--that is, don't use INSTANCE.  Write your
   complete spec in a single module.  Don't worry about splitting your
   spec into multiple modules until you can correctly write one in a
   single module.

 

2. Use TLC to debug your spec.  When TLC reports an error, use the
   Toolbox's help pages and the Hyperbook to figure out what caused
   the error.

 

3. Post a further question to this group only if you get an error report
   that you can't understand.  In that case, include the spec, a
   description of the model, and the error report.

 

Leslie Lamport

On Fri, Apr 12, 2013 at 3:48 AM, Bert_emme <bertan...@xxxxxxxxx> wrote:

Hi, I solve my problem variable and reality... I attach my first program as it is after  I take a little rest....

Is there some problems with minLimit?

Thanks in advance

Mauro

On Tuesday, April 2, 2013 1:56:30 PM UTC+2, Bert_emme wrote:

Dear Lamport,

I have solve the problem with my variable...

But now I have some trouble to stop TLC to run on InnerFIFO... I left apart my program for now...

Some hint?...

I appreciate the how you write your book,... the theory of action (book' = [book EXCEPT !.ch = @+1]...

I thanks in advance

bye

Mauro 

On Sunday, March 24, 2013 6:30:40 PM UTC+1, Leslie Lamport wrote:

Dear Bert_emme,

One limitation of TLC is that it does not handle parametrized
instantiation.  So, it cannot handle formulas defined by the statement

   primeNum(q) == INSTANCE prime WITH pr <- q

It will handle formulas defined by

   primeNum == INSTANCE prime WITH pr <- n

This is documented in:

  http://research.microsoft.com/en-us/um/people/lamport/tla/current-tools.pdf

A link to that document is prominently displayed on the page for
obtaining the stand-alone version of the tools.  Unfortunately, it did
not make it to the page for users of the Toolbox.  I appologize for
that omission and will correct it.

TLC should have reported an error when you ran it on the spec.  The
error message was probably not very informative.  However, it should
have made you realize that the question you should have asked was:
What caused the error?  You should not have been surprised that TLC
did not find any states or produce any output.  If TLC did not report
an error, then please send me the .tla files and I will try to find
out why.

Best regards,

Leslie

P.S. Can anyone tell me why the web page provided by Google groups ignores my

choice of font when typing this reply?   It worked the last time I tried to do it.

 

-------------
On Wednesday, March 20, 2013 8:46:24 AM UTC-8, Bert_emme wrote:

Hi, I'm new to this languages and in this way to think problem.
I would know if this non runnable program has some sense or is totally unsenseble.

------------------------------- MODULE prime -------------------------------
EXTENDS Naturals
CONSTANT n
VARIABLE q

Init == q >1 /\ q<n
       
Next == \neg((n%q) = 0)
        /\ q' = q+1
H == Init /\ [][Next]_q

=============================================================================
THEOREM H => []Init

Thanks in advance
Mauro

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, 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?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.