|
types
|
|
MyInt = int [2..100];
|
|
LengthInt = int [0..40];
|
|
Primes = autocons system
|
|
|[
|
|
var
|
|
initialized : bool = false ;
|
|
primes : list [ 40 ] of MyInt = [3]
|
|
actions
|
|
obs init = requires initialized = false :
|
|
primes := [ x | var x: MyInt & (forall tmp : MyInt :
|
|
(tmp < x => (x mod tmp <> 0 ))) ] ;
|
|
initialized := true end;
|
|
|
|
obs Prime(a: MyInt) =
|
|
requires (exists i : LengthInt : (primes[i] = a)) :
|
|
skip
|
|
end
|
|
|
|
do
|
|
init() // var A : MyInt : Prime(A)
|
|
od
|
|
]|
|
|
system
|
|
Primes
|
|
|