\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
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.LeslieOn Wed, Mar 20, 2013 at 11:27 AM, TLA Plus <tlap...@xxxxxxxxx> wrote:
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.LeslieOn Wed, Mar 20, 2013 at 10:38 AM, Stephan Merz <step...@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,StephanOn Mar 20, 2013, at 6:36 PM, Bert_emme <bert...@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 relationNext == IF \neg((n%q) = 0) THEN q' = q+1 ELSE q'=qThanks for your last fast responsemauro
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 writingInit == q \in 2 .. (n-1)which is probably what you intended. I'd also advise you to add
ASSUME n \in Natto 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 qInit == q >1 /\ q<n
Next == \neg((n%q) = 0)
/\ q' = q+1
H == Init /\ [][Next]_q==============================
============================== =================
THEOREM H => []InitThanks 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...@googlegroups.com .
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...@googlegroups.com .
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 .
Attachment:
calcm.pdf
Description: Adobe PDF document