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 advanceMauro
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 advancebyeMauro
On Sunday, March 24, 2013 6:30:40 PM UTC+1, Leslie Lamport wrote:
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:
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
Best regards,LeslieP.S. Can anyone tell me why the web page provided by Google groups ignores mychoice 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 -------------------------------
Init == q >1 /\ q<n
Next == \neg((n%q) = 0)
/\ q' = q+1
H == Init /\ [Next]_q
THEOREM H => Init
Thanks in advance
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.