No need to change the nextstate 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
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 nextstate 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 .. (n1)
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 nextstate 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.
