Re: my first tla program

[Bert_emme <bertan...@xxxxxxxxx>]

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