MODULE main
VAR
e : { e1 , e2 , e3 , e4 , e5 , e6 , e7 , e8 , e9 , e10 , e11 , e12 } ;
j : 3..9;
i : 1..7;
x: 0..6;
primes : − 1..10;
factorial : 1..720;
sigma : 0 . . 1 0 ;
deadlock : 1 . . 3 ;
c : 0..10;
FROZENVAR number : 0 . . 8 ;
−−DEFINE number := 5 ;

ASSIGN
i n i t ( e ) := e1 ;
i n i t ( j ) := 3 ;
i n i t ( i ) := 1 ;
i n i t ( p r i m e s ) := 0 ;
i n i t ( f a c t o r i a l ) := 1 ;
i n i t ( sigma ) := 0 ;
i n i t ( d e a d l o c k ) := 1 ;
i n i t ( c ) := 0 ;

next ( deadlock ) := case
deadlock = 1 &
j = next ( j ) &
x = next ( x ) &
sigma = next ( sigma ) &
factorial = next ( factorial ) &
primes = next ( primes ) &
i = next ( i ) &
c = next ( c ) &
e = next ( e ) : 2 ;
deadlock = 2 : 3;
TRUE : d e a d l o c k ;
esac ;
n e x t ( e ) := c a s e
e = e1 & number > 2 : e2 ;
e = e1 & number <= 2 : e12 ;
e = e2 & j <= number : e3 ;
e = e2 & j > number : e8 ;
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 = e8 : e9 ;
e = e9 & number = 3 : e10 ;
e = e9 & number != 3 : e11 ;
TRUE : e;
esac ;


next ( x ) := c a s e
e = e3 & next ( e ) = e4 : 0 ;
e = e6 & next ( e ) = e4 & x + 1 <= 6 : x + 1 ;
TRUE : x ;
esac ;
next ( j ) := case
e = e7 & next ( e ) = e2 & j <= 8 : j + 1 ;
TRUE : j ;
esac ;

next ( factorial ) := c a s e
e = e3 : 1 ;
next ( e ) = e5 & factorial <= 720 & factorial ∗ i <= 720 : factorial ∗ i ;
TRUE : factorial ;
esac ;
next ( i ) := case
next ( e ) = e3 : 1 ;
next ( e ) = e6 & i < 7 : i + 1 ;
TRUE : i ;
esac ;
next ( sigma ) := case
e = e7 & ( sigma + ( factorial − j ∗ ( factorial / j ) ) ) <= 10 : sigma + ( factorial − j ∗ (
factorial / j )) ;
TRUE : sigma ;
esac ;
next ( primes ) := case
e = e8 & (−1 + sigma ) >= 0 & (−1+sigma ) <= 10 : (−1 + sigma ) ;
TRUE : primes ;
esac ;

next ( c ) := case
c + 1 > 10 : c ;
e = e3 : c + 1 ;
TRUE : c ;
esac ;

CTLSPEC(number<3)-> AF e=e12;