MODULE main
VAR e : {e1 , e2 , e3 , e4 , e5 , e6 , e7 , e8 , e9 , e10 , e11 , e12
};
VAR j : 3..9;
VAR i : 1..24;
VAR x : 0..6;
VAR primes : 0..10;
VAR factorial : 1..1000;
VAR sigma : 0..5;
VAR loop : 1..3;
FROZENVAR number : 0..8;

ASSIGN
init( e ) := e1;
init( j ) := 3;
init( i ) := 1;
init( x ) := 0;
init( primes ) := 0;
init( factorial ) := 1;
init( sigma ) := 0;
init( loop ) := 1;
next( e ) := case
e = e1 & ( number > 2 ) : e2;
e = e2 & ( j <= number ) : e3;
e = e3 : e4;
e = e4 & (x < (j - 2) ): e5;
e = e4 & !(x < (j - 2) ): e7;
e = e5 : e6;
e = e6 : e4;
e = e7 : e2;
e = e2 & ! ( j <= number ) : e8;
e = e8 : e9;
e = e9 & number = 3 : e10;
e = e9 & number != 3 : e11;
e = e1 & ! ( number > 2 ) : e12;
TRUE: e;
esac;
next( j ) := case
e = e7 & next( e ) = e2 & j+1 <= 9 : j +1;
TRUE: j;
esac;
next( i ) := case
next(e) = e3 : 1;
next(e) = e6 & i<24: i + 1;
TRUE: i;
esac;
next( x ) := case
e = e3 & next( e ) = e4 : 0;
e = e6 & next( e ) = e4 & x + 1 <= 6 : x + 1;
TRUE: x;
esac;
next( primes ) := case
next(e) = e8 & (-1 + sigma ) >= 0 & (-1+sigma ) <= 4 : -1 + sigma;
TRUE: primes;
esac;
next( factorial ) := case
next(e) = e3 : 1;
next(e) = e5 & factorial <= 1000 & factorial * i <= 1000: factorial *
i;
TRUE: factorial;
esac;
next( sigma ) := case
next(e) = e7 & ( sigma + ( factorial - j * (factorial / j ) ) ) <= 5 :
sigma + ( factorial - j * ( factorial / j ));
TRUE: sigma;
esac;
next( loop ) := case
loop = 1 & j = next( j ) & x = next( x ) & sigma = next( sigma ) &
factorial =next( factorial ) & primes = next( primes ) & i = next( i ) &
e = next( e ) : 2;
loop = 2 : 3;
TRUE: loop;
esac;