[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] my first tla program



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

On Wed, Mar 20, 2013 at 10:38 AM, Stephan Merz <stepha...@xxxxxxxxx> wrote:
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

On Mar 20, 2013, at 6:36 PM, Bert_emme <bertan...@xxxxxxxxx> wrote:

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

On Wednesday, March 20, 2013 6:01:34 PM UTC+1, Stephan Merz wrote:
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





--
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.
 
 


--
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.