Re: my first tla program

[Leslie Lamport <tlapl...@xxxxxxxxx>]

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

 

On Wednesday, March 20, 2013 8:46:24 AM UTC-8, 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