Re: my first tla program

[Stephan Merz]

Hello Mauro,

welcome to TLA+ and to this group. TLA+ is not a programming language but a language for modeling algorithms and systems. In this sense, we tend to avoid terms such as "program" and "runnable". I presume that what you mean is that TLC, the TLA+ model checker, cannot enumerate the states that your specification (formula H of your module) generates, even after fixing a concrete value for the parameter n. The subset of TLA+ that TLC can evaluate is described in chapter 14 of the TLA+ book ("Specifying Systems"), I also encourage you to study the hyperbook, even if it is work in progress.

The reason why TLC can't evaluate your specification is that formula Init contains too little information to determine a finite set of possible values for the (only) variable q. Remember that TLA+ is untyped, the value of q could for example be any real number between 1 and n but it could also be any other value (such as a string or a set) that satisfies the predicate. (For example, TLA+ does not specify whether 1 < {} is true or false.)

You can easily remedy that problem by writing

Init == q \in 2 .. (n-1)

which is probably what you intended. I'd also advise you to add

ASSUME n \in Nat

to document the fact that you intend the parameter n to be a natural number. (TLC will check that the assumption actually holds when you provide a specific value for n in a model.)

I am less sure that the next-state relation (formula Next) that you specified really corresponds to what you had in mind, but the previous hints should help you use TLC to find out if it does or not.

Best regards,

Stephan

On Wednesday, March 20, 2013 5:46:24 PM UTC+1, 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

[Bert_emme]

Now I would ask you if my solution model in correct form the algorithms that I have in mind.

I correct, with your advise, my error and I change the next-state relation

Next == IF \neg((n%q) = 0) THEN q' = q+1 ELSE q'=q

Thanks for your last fast response

mauro

[Stephan Merz]

No need to change the next-state relation: the ELSE case is taken care of by the formula [Next]_q in your specification, which allows for stuttering (and this is in fact the only possible transition when n % q is different from 0.

I cannot tell if the specification corresponds to what you have in mind. What I'm puzzled by is the condition. Suppose that n=20 and q=5. Then n % q = 0, and your specification will stutter forever. Is that what you are thinking of? Again, I encourage you to play with TLC to find out how your specification behaves.

Minor detail: you can write "n % q # 0", which is equivalent but a little more readable than "\neg((n%q)=0)". Negation can be written as "~", and inequality as "#".

Best regards,

Stephan

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

[TLA Plus]

Stephan is (of course) correct about your ELSE clause being redundant, since the two versions of the Next action produce mathematically equivalent TLA+ specifications Init /\ []Next.  However, I suggest you create your spec in the Toolbox and run the model checker on the two versions.  You will find that with your original specification, the model checker complains that there is a deadlock.  (You can disable deadlock checking.)  It should find no error with the second version (the one with the IF / THEN /ELSE expression).  You may learn something by examining the error trace demonstrating deadlock in the first spec.

 

Also, I believe that Stephan (surprisingly) made a minor error in his email, and that only stuttering steps are allowed in the case when n % q equals 0.

 

Leslie

[TLA Plus]

I meant that the spec  Init /\ [][Next]_q  is the same for the two different versions of Next.

 

By the way, I recommend using a fixed-width font like Courier for emails about TLA+, since it makes formulas easier to read.

 

Leslie

[Bert_emme]

sorry, I don't see over what I do when I'm searching... There isn't malice by myself....

Now I have a new question:

I don't have problem with division even if I don't know if my assumption is right... but we can speech about this an other time...

my problem is that the when a run the TLC the distinct states stay fixed at 0, and there isn't any state during the computation.

The second problem is that I don't have any output.

The math that stays behind it is:

\begin{cases}

m &\text{is a prime number} \\

p_k = p_s +m&\text{is also a prime number} \\

p_r = p_s +m &\text{is prime}

\end{cases}

where p_s is a P_j/2

where P_j is all even number

Thanks in advance

and I hope I don't make the same error of my previous post

[Leslie Lamport]

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:

[Bert_emme]

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 

[Bert_emme]

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

[TLA Plus]

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

--

[Bert_emme]

On Friday, April 12, 2013 7:19:38 PM UTC+2, Leslie Lamport wrote:

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

Hi, I'm recurrance... I have a problem with instancesation...

I have a problem with NZ-system... Or I think so...

The system error is:

The configuration file did not specify the initial state predicate.

Can also be caused by trying to run TLC on a specification from

a module imported with a parameterized INSTANCE statement.

This error appear after and post my study over NZ system.

In the inner module I have write the follow restriction:

Calculate == \E r \in Nat : q'=r /\ q = r-1

I assume two costant rho and omega where I give them the value 3600 and 10

I hope I will be exaustive

Thanks in advance

bye 

[Stephan Merz]

Hello,

without seeing your spec it is impossible to guess what the problem is.

1. Did you follow Leslie's advice and write your specification as a single module? In particular, Leslie told you in a previous message about the limitation of TLC handling parameterized instantiation as in

  Op(x) == INSTANCE SomeModule WITH someConstant <- x

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

2. The definition

Calculate == \E r \in Nat : q'=r /\ q = r-1

cannot be evaluated by TLC because it contains quantification over an infinite set. You can instruct TLC to substitute a finite set for Nat (see Advanced Options -> Definition Override). But this does not seem to be the cause of your problem because you would have gotten a different error message.

Hope this helps,

Stephan

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.

Visit this group at http://groups.google.com/group/tlaplus.

[Bert_emme]

hi Merz,

I have two questions:

1) If i don't use INSTANCE I use a recursive function to define Prime module? 

2) If I have two module either with one variable prime but in the second module I call three different time the first module, I need to specify the INLness? The INLness is essential relate at one module or a the relation between two module?For example the clock module  if it has more than two variable primed needs the INLness, but if I call a module for three time I have the exclude the possibility that these three call happend the same time? I have to exclude the possibility that the change of the primed variable of the first module happends when change the primed variable of the second module?

I'm  so much in trouble...

I must to re-read the chapter... I think

thanks in advance

Mauro

[Leslie Lamport]

Stephan Merz is responding to this off the list because discussion of Bert_emme's problem does not seem to be of general interest.