Re: my first tla program

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