Re: my first tla program

[Leslie Lamport <tlapl...@xxxxxxxxx>]

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