BuildTA.java - MoVES - A tool for Modelling and Veriﬁcation of Embedded Systems

i f ( l i n e F o u n d I n F i l e ) { i f ( i nT es tMode )

Sy s tem . o u t . p r i n t ( b o o l S a t i s ? ” True ;\n” : ” ; F a l s e ;\n” ) ; e l s e {

Sy s tem . o u t . p r i n t ( ” V e r i f i c a t i o n t i m e : ” ) ; ex ecT i m e = ex ecT i m e / 1 0 0 0 ;

i n t r e s t = 0 ; i f ( ex ecT i m e> 6 0 ) {

Sy s tem . o u t . p r i n t ( ex ecT i m e / 6 0 ) ; }

e l s e {

Sy s tem . o u t . p r i n t ( 0 ) ; }

Sy s tem . o u t . p r i n t ( ” . ” ) ; i f ( ex ecT i m e %60>=10) {

Sy s tem . o u t . p r i n t ( ( ex ecT i m e %60) ) ; }

e l s e {

Sy s tem . o u t . p r i n t ( ” 0 ” + ( ex ecT i m e %60) ) ; }

Sy s tem . o u t . p r i n t ( ” min\n ” ) ; f o r ( i = 0 ; i<r e s u l t . l e n g t h ; i ++) {

i f ( ! r e s u l t [ i ] [ 0 ] . e q u a l s ( ” ” ) )

Sy s tem . o u t . p r i n t l n ( r e s u l t [ i ] [ 0 ] + ” : ” + r e s u l t [ i ] [ 1 ] ) ; }

} } e l s e {

throw new E x c e p t i o n ( ) ; }

i f ( ! i nT es tMode && t r a c e ) { p a r s e . p r i n t T r a c e ( ) ; i f ( e x p l a i n ) {

p a r s e . p r i n t E x p l a i n ( ) ; }

} }

r e t u r n b o o l S a t i s ; }

}

∗ @par am p l c o n t a i n i n g t h e p l a t f o r m

∗ @par am f o u t o f t y p e P r i n t S t r e a m

∗/

p u b l i c BuildTA ( A p p l i c a t i o n app , P l a t f o r m p l , P r i n t S t r e a m f o u t ){

a p p l i c a t i o n = app ; p l a t f o r m = p l ; t h i s. f o u t = f o u t ; i n t g ;

Env i ronm ent eTemp = new Env i ronm ent ( ) ;

e n v i r o n m e n t s =new Env i ronm ent [ eTemp . e a . l e n g t h ] ; i f ( eTemp . e a . l e n g t h > 0 ) {

f o r (i n t i = 0 ; i<eTemp . e a . l e n g t h ; i ++) { g = 1 ;

f o r (i n t j = 0 ; j< a p p l i c a t i o n . t a s k s . l e n g t h ; j ++) { f o r (i n t k = 0 ; k<a p p l i c a t i o n . t a s k s [ j ] . l e n g t h ; k++) {

i f ( a p p l i c a t i o n . t a s k s [ j ] [ k ] . t a s k I D == eTemp . e a [ i ] . t a s k i d ) { eTemp . e a [ i ] . m a p p e d t a s k = g ;

} e l s e

g++;

} }

e n v i r o n m e n t s [ i ] = eTemp . e a [ i ] ; }

}

s e t P e r i o d s ( ) ; }

/∗ ∗

∗ C a l c u l a t e s p e r i o d s f o r t a s k s a c c o r d i n g t o t h e s p e e d o f t h e i r e x e c u t i o n

∗ p l a t f o r m s . T h e p e r i o d s i s i n t h e e n d d i v i d e d b y t h e g r a n u l a r i t y , a n d r o u n d e d

∗ u p .

∗/

p r i v a t e s t a t i c v oi d s e t P e r i o d s ( ) {

i n t l cm = p l a t f o r m . calcLCM ( p l a t f o r m . p r o c S p e e d ( ) , 0 , 1 ) ; f o r (i n t i = 0 ; i<p l a t f o r m . p r o c e s s o r s . l e n g t h ; i ++) {

f o r (i n t j = 0 ; j<a p p l i c a t i o n . t a s k s [ i ] . l e n g t h ; j ++) { i f ( ! a p p l i c a t i o n . t a s k s [ i ] [ j ] . n o n p e r i o d i c ) {

a p p l i c a t i o n . t a s k s [ i ] [ j ] . p =

(i n t) ( ( l cm∗a p p l i c a t i o n . t a s k s [ i ] [ j ] . p t i m e ) / a p p l i c a t i o n . g r a n u l a r i t y ) ;

}

a p p l i c a t i o n . t a s k s [ i ] [ j ] . d =

(i n t) ( ( l cm∗a p p l i c a t i o n . t a s k s [ i ] [ j ] . d t i m e ) / a p p l i c a t i o n . g r a n u l a r i t y ) ;

a p p l i c a t i o n . t a s k s [ i ] [ j ] . emax =

(i n t) Math . c e i l ( a p p l i c a t i o n . t a s k s [ i ] [ j ] . e m a x o r g∗

(double) ( l cm / p l a t f o r m . p r o c e s s o r s [ a p p l i c a t i o n . t a s k s [ i ] [ j ] . p r o c−1 ] . f r e q u e n c y ) / (double) a p p l i c a t i o n . g r a n u l a r i t y ) ;

a p p l i c a t i o n . t a s k s [ i ] [ j ] . emin =

(i n t) Math . c e i l ( a p p l i c a t i o n . t a s k s [ i ] [ j ] . e m i n o r g∗

a p p l i c a t i o n . t a s k s [ i ] [ j ] . o =

(i n t) ( ( l cm∗a p p l i c a t i o n . t a s k s [ i ] [ j ] . o t i m e ) / (double) a p p l i c a t i o n . g r a n u l a r i t y ) ;

} }

f o r (i n t i = 0 ; i<e n v i r o n m e n t s . l e n g t h ; i ++) { e n v i r o n m e n t s [ i ] . i n t e r a r r i v a l c y c l e s = (i n t)

( l cm∗e n v i r o n m e n t s [ i ] . i n t e r a r r i v a l / a p p l i c a t i o n . g r a n u l a r i t y ) ; }

} /∗ ∗

∗ R e t u r n t h e a p p l i c a t i o n

∗ @ r e t u r n A p p l i c a t i o n

∗/

p u b l i c A p p l i c a t i o n getApp ( ) { r e t u r n a p p l i c a t i o n ; }

/∗ ∗

∗ C o n v e r t s t h e d e p e n d e n c y [ ] [ ] t o a s t r i n g u s e d i n t h e m o d e l .

∗ @par am i n t [ ] [ ] c o n t a i n i n g d e p e n d e n c i e s .

∗ W r i t t e n t o f o u t

∗/

p r i v a t e s t a t i c v oi d t o S t r i n g D e p (i n t[ ] [ ] d ){

f o u t . p r i n t ( ”{{” ) ;

f o r (i n t i = 0; i<d . l e n g t h ; i ++){

f o r (i n t j = 0; j<d [ 0 ] . l e n g t h ; j ++){

i f( j ! = ( d [ 0 ] . l e n g t h−1) )

f o u t . p r i n t ( d [ i ] [ j ]+ ” , ” ) ; e l s e

f o u t . p r i n t ( d [ i ] [ j ] ) ; }

i f( i ==(d . l e n g t h−1) ) { f o u t . p r i n t ( ”} };\n” ) ; }

e l s e {

f o u t . p r i n t ( ”},{” ) ; }

} } /∗ ∗

∗ C o n v e r t s t h e s p e c i f i e d e n v i r o n m e n t s t o a s t r i n g , w h i c h i s u s e d i n t h e m o d e l .

∗ t h e s t r i n g i s w r i t t e n d i r e c t l y i n f o u t .

∗/

p r i v a t e s t a t i c v oi d t o S t r i n g E n v i r o n m e n t ( ) { S t r i n g en = ” ” ;

f o r (i n t i = 0 ; i<e n v i r o n m e n t s . l e n g t h ; i ++) {

en += ” env ” + i + ” = Env i ronm ent ( ”+e n v i r o n m e n t s [ i ] . m a p p e d t a s k+” , t r i g g e r [ ”+( e n v i r o n m e n t s [ i ] . m apped tas k−1)+” ] , ” +

e n v i r o n m e n t s [ i ] . i n t e r a r r i v a l c y c l e s +” ) ;\n” ; }

f o u t . p r i n t l n ( en ) ; }

/∗ ∗

∗ T a s k s i s c o n v e r t e d t o a s t r i n g .

∗ @par am t a s T h e t a s k w h i c h i s t o b e c o n v e r t e d .

∗ @par am l A l o c a l i d o f t y p e i n t .

∗ @par am g A g l o b a l i d o f t y p e i n t .

∗ T h e r e s u l t i s w r i t t e n o n f o u t .

∗/

p r i v a t e s t a t i c v oi d t o S t r i n g T a s k s ( Task t a s ,i n t l , i n t g ){

S t r i n g t a s k ;

S t r i n g d e a d l i n e T y p e = ” ” ; i f ( t a s . s d == 1 )

d e a d l i n e T y p e = ”SOFT” ; e l s e i f( t a s . s d == 2 )

d e a d l i n e T y p e = ”FIRM” ; e l s e

d e a d l i n e T y p e = ”HARD” ; i f ( ! t a s . n o n p e r i o d i c ) {

t a s k = ” T as k c ”+(g +1)+” = Task ( ”+( t a s . p r o c )+” , ”+(g +1)+” , ”+( l +1)+” ,

”+t a s . emin+” , ”+t a s . emax+” , ”+t a s . d+” , ”+t a s . o+” , ”+t a s . p+” ,

”+t a s . p r i+” , t i d [ ” + (( t a s . p r o c )−1)+” ] , g t i d [ ” + (( t a s . p r o c )−1)+” ] , s a c t [ ” + (( t a s . p r o c )−1)+” ] [ REA ] , s a c t [ ” + (( t a s . p r o c )−1)+” ] [ RUN] , s a c t [ ” + (( t a s . p r o c )−1)+” ] [ PRE ] , s a c t [ ” + (( t a s . p r o c )−1)+” ] [ FIN ] ,

”+d e a d l i n e T y p e+” , ” + t a s . maxCount + ” ) ; ” ; }

e l s e {

t a s k = ” T as k c ”+(g +1)+” = T r i g g e r e d ( ”+( t a s . p r o c )+” , ”+(g +1)+” , ”+( l +1)+” ,

”+t a s . emin+” , ”+t a s . emax+” , ”+t a s . d+” , ”+t a s . p r i+” , t i d [ ” + (( t a s . p r o c )−1)+” ] , g t i d [ ” + (( t a s . p r o c )−1)+” ] , t r i g g e r [ ”+(g )+” ] , s a c t [ ” + (( t a s . p r o c )−1)+” ] [ REA ] ,

s a c t [ ” + (( t a s . p r o c )−1)+” ] [ RUN] , s a c t [ ” + (( t a s . p r o c )−1)+” ] [ PRE ] , s a c t [ ” + (( t a s . p r o c )−1)+” ] [ FIN ] , ”+d e a d l i n e T y p e+” ) ; ” ;

}

f o u t . p r i n t l n ( t a s k ) ; }

/∗ ∗

∗ F i n d s t h e o s f o r e a c h p r o c e s s i n g e l e m e n t a n d w r i t e s

∗ t h e m a s a n a r r a y t o f o u t .

∗/

p r i v a t e s t a t i c v oi d t y p e O f P r o c ( ) {

S t r i n g t e s t = ” i n t [ 0 , 3 ] p r o c e s s o r S c h e d u l i n g [M] ={” ; f o r (i n t i = 0 ; i<( p l a t f o r m . p r o c e s s o r s ) . l e n g t h ; i ++) {

i f ( i > 0 ) { t e s t += ” , ” ; }

t e s t += t y p e P r o c ( p l a t f o r m . p r o c e s s o r s [ i ] ) ; }

t e s t += ”}; \n // C o n t a i n s i n f o r m a t i o n a b o u t t h e s c h e d u l i n g p r i n c i p l e f o r e a c h p r o c e s s o r .\n” ;

f o u t . p r i n t l n ( t e s t ) ; }

/∗ ∗

∗ G e t t h e t y p e o f a l l o c a t i o n a l g o r i t h m

∗ @par am p r T h e p r o c e s s o r t o f i n d a l g o r i t h m f o r

∗ @ r e t u r n S t r i n g c o n t a i n i n g a l l o c a t i o n a l g o r i t h m .

∗/

p r i v a t e s t a t i c S t r i n g t y p e A l l ( P r o c e s s o r p r ) { s w i t c h( p r . a l l o c a t i o n ) {

c a s e P r o c e s s o r . PCS : r e t u r n ”PCS” ; c a s e P r o c e s s o r . PRI INH :

r e t u r n ” PRI INH ” ; c a s e P r o c e s s o r . NPCS :

r e t u r n ”NPCS” ; }

r e t u r n ” ” ; }

/∗ ∗

∗ G e t t h e t y p e o f s c h e d u l i n g a l g o r i t h m

∗ @par am p r T h e p r o c e s s o r t o f i n d a l g o r i t h m f o r

∗ @ r e t u r n S t r i n g c o n t a i n i n g s c h e d u l i n g a l g o r i t h m .

∗/

p r i v a t e s t a t i c S t r i n g t y p e P r o c ( P r o c e s s o r p r ){

s w i t c h( p r . s chedT y pe ){

c a s e P r o c e s s o r . EDF:

r e t u r n ”EDF” ; c a s e P r o c e s s o r .RM:

r e t u r n ”RM” ; c a s e P r o c e s s o r .DM:

r e t u r n ”DM” ; c a s e P r o c e s s o r . FP :

r e t u r n ”FP” ; }

r e t u r n ” ” ; }

/∗ ∗

∗ R e t u r n s t h e n u m b e r o f r e s o u r c e s i n t h e s y s t e m .

∗ @ r e t u r n i n t T h e n u m b e r o f r e s o u r c e s .

∗/

p r i v a t e s t a t i c i n t n r O f R e s o u r c e s ( ) {

r e t u r n a p p l i c a t i o n . r e s o u r c e s U s e d [ 0 ] . l e n g t h ; }

/∗ ∗

∗ C o n v e r t s t h e n e e d e d r e s o u r c e s a r r a y i n t o a s t r i n g w h i c h i s

∗ w r i t t e n d i r e c t l y t o f o u t .

∗/

p r i v a t e s t a t i c v oi d t o S t r i n g N e e d e d ( ) {

S t r i n g r e s = ” b o o l N e e d e d R e s o u r c e s [M] [ N ] [ R ] = ” ; f o r (i n t j = 0 ; j<n r O f P r o c ( p l a t f o r m . p r o c e s s o r s ) ; j ++) {

i f ( j>0)

r e s += ” , ” ; i f ( j == 0 )

r e s += ”{” ;

f o r (i n t i = 0; i<maxNrTasks ( a p p l i c a t i o n . t a s k s ) ; i ++) { i f ( i > 0 )

r e s += ” , ” ; i f ( i == 0 ) { r e s += ”{” ; }

f o r (i n t k = 0 ; k<n r O f R e s o u r c e s ( ) ; k++) { i f ( k == 0 ) {

r e s += ”{” ; }

e l s e { r e s += ” , ” ; }

t r y { r e s +=

a p p l i c a t i o n . r e s o u r c e s U s e d [ a p p l i c a t i o n . t a s k s [ j ] [ i ] . ta s k I D−1 ] [ k ] ; }

c a t c h ( A r r a y I n d e x O u t O f B o u n d s E x c e p t i o n a i o o b e ) { r e s+= ” 0 ” ; } i f ( k == n r O f R e s o u r c e s ( )−1)

r e s += ”}” ; }

i f ( i==maxNrTasks ( a p p l i c a t i o n . t a s k s )−1) { f o u t . p r i n t ( r e s + ”}” ) ;

r e s = ” ” ; }

}

i f ( j ==n r O f P r o c ( p l a t f o r m . p r o c e s s o r s )−1) f o u t . p r i n t ( ”};\n” ) ;

} }

/∗ ∗

∗ T h e p r o c e s s i n g e l e m e n t ( c o n t r o l l e r , s y n c h r o n i z e r , a l l o c a t i o n a n d

∗ s c h e d u l e r i s d e s c r i b e d a s s t r i n g s . T h e s e s t r i n g s a r e w r i t t e n o n f o u t .

∗/

p r i v a t e s t a t i c v oi d t o S t r i n g P r o c ( P r o c e s s o r pr , i n t i ){

f o u t . p r i n t l n ( ”Con”+( i +1)+” = C o n t r o l ( ”+( i +1)+” , f t i d [ ”+ i +” ] , t i d [ ”+i +” ] , g t i d [ ”+i +” ] , c a c t [ ”+ i +” ] [ SYN ] , c a c t [ ”+i +” ] [ SCH ] , c a c t [ ”+ i +” ] [ ALL ] , s a c t [ ”+i +” ] [ REA ] , s a c t [ ”+ i +” ] [ FIN ] , s a c t [ ”+ i +” ] [ RUN] ,

s a c t [ ”+i +” ] [ PRE ] ) ;\n”+

” Syn ”+( i +1)+” = S y n c h r o n i z e r ( ”+( i +1)+” , f t i d [ ”+ i +” ] , c a c t [ ”+ i+” ] [ SYN ] ) ;\n ”+

” Sch ”+( i +1)+” = S c h e d u l e r ( ”+( i +1)+” , f t i d [ ”+ i +” ] , c a c t [ ”+ i +” ] [ SCH ] ) ;\n ”+

” A l l o c ”+( i +1)+” = A l l o c a t o r ( ”+( i +1)+” , ” + t y p e A l l ( p r ) + ” , c a c t [ ”+ i +” ] [ ALL ] ) ; ” ) ;

} /∗ ∗

∗ G e n e r a t e s t h e s y s t e m s p e c i f i c a t i o n i n UPPAAL .

∗ u s e s t h e f u n c t i o n s : t o S t r i n g P r o c a n d T o S t r i n g T a s k s .

∗ @par am t a T a s k [ ] [ ] c o n t a i n i n g t h e t a s k m a p p i n g a r r a y

∗ @par am p a P r o c e s s o r [ ] c o n t a i n i n g t h e p r o c e s s o r s o f t h e s y s t e m .

∗/

p r i v a t e s t a t i c v oi d t o S t r i n g A l l ( Task [ ] [ ] ta , P r o c e s s o r [ ] pa ){

S t r i n g r s = ” ” ; i n t g b l = 0;

f o r (i n t i = 0; i<t a . l e n g t h ; i ++){

i f ( t a [ i ] ! =n u l l){

t o S t r i n g P r o c ( pa [ i ] , i ) ;

f o r (i n t j = 0; j<t a [ i ] . l e n g t h ; j ++){

i f ( t a [ i ] [ j ] ! =n u l l){

t o S t r i n g T a s k s ( t a [ i ] [ j ] , j , g b l ) ; g b l ++;

} } } }

t o S t r i n g E n v i r o n m e n t ( ) ; }

/∗ ∗

∗ R e t u r n s t h e t o t a l n u m b e r o f p r o c e s s o r s .

∗ @ r e t u r n i n t T h e t o t a l n u m b e r o f p r o c e s s o r s .

∗/

p r i v a t e s t a t i c i n t n r O f P r o c ( P r o c e s s o r [ ] p ) {r e t u r n p . l e n g t h ;}

/∗ ∗

∗ R e t u r n s t h e m ax im um n u m b e r o f t a s k s o n o n e p r o c e s s o r .

∗ @ r e t u r n i n t T h e m ax im um n u m b e r o f t a s k s o n o n e p r o c e s s o r .

∗/

p r i v a t e s t a t i c i n t maxNrTasks ( Task [ ] [ ] t ) { i n t mx = 0 ;

f o r(i n t i = 0; i<t . l e n g t h ; i ++) i f( t [ i ] . l e n g t h>mx)

mx=t [ i ] . l e n g t h ; r e t u r n mx ;

} /∗ ∗

∗ R e t u r n s t h e t o t a l n u m b e r o f t a s k s i n t h e s y s t e m .

∗ @ r e t u r n i n t T h e t o t a l n u m b e r o f t a s k s i n t h e s y s t e m .

∗/

p r i v a t e s t a t i c i n t t o t a l N r T a s k s ( Task [ ] [ ] t ){

i n t c n t = 0;

f o r (i n t i = 0; i<t . l e n g t h ; i ++){

i f ( t [ i ] ! =n u l l){

f o r(i n t j = 0; j<t [ i ] . l e n g t h ; j ++){

i f ( t [ i ] [ j ] ! =n u l l) c n t ++;

} } }

r e t u r n c n t ; }

/∗ ∗

∗ C r e a t e s t h e l o c a l T o G l o b a l i n t e g e r [ ] [ ] i n t h e UPPAAL m o d e l

∗ c o n t a i n i n g i n f o r m a t i o n a b o u t w h i c h g l o b a l−i d s i s s t o r e d o n w h i c h

∗ p r o c e s s o r . W r i t t e n t o f o u t

∗ @par am t A t a s k [ ] [ ] w i t h a l l t a s k s .

∗/

p r i v a t e s t a t i c v oi d l o c a l T o G l o b a l ( Task [ ] [ ] t ){ i n t coun = 1 ;

S t r i n g r e s = ” i n t [ 0 ,MN] l t o g [M] [ N]={{” ; f o r(i n t i = 0; i<t . l e n g t h ; i ++){

f o r(i n t j = 0; j<maxNrTasks ( t ) ; j ++){

i f ( j<t [ i ] . l e n g t h ){

r e s+=coun ; coun ++;

}

e l s e r e s+=” 0 ” ; i f( j != maxNrTasks ( t )−1)

r e s+=” , ” ;

} r e s+=”}” ; i f( i != t . l e n g t h−1)

r e s+=” , {” ; }

r e s+=”}; / / g l o b a l t a s k i d s from l o c a l s\n ” ; f o u t . p r i n t l n ( r e s ) ;

} /∗ ∗

∗ C r e a t e s t h e s y s t e m−d e c l a r a t i o n . A s s i g n s a l l t a s k s a n d p r o c e s s o r s t o t h e UPPAAL

∗ s y s t e m . W r i t t e n t o f o u t .

∗ @par am t a T a s k [ ] [ ] c o n t a i n i n g a l l t a s k s

∗ @par am p a P r o c e s s o r [ ] c o n t a i n i n g a l l p r o c e s s o r s .

∗/

p r i v a t e s t a t i c v oi d t o S t r i n g S y s t e m ( Task [ ] [ ] ta , P r o c e s s o r [ ] pa ){

S t r i n g r e s = ” s y s t e m ” ; S t r i n g conn = ” ” ; S t r i n g s y n = ” ” ;

f o r(i n t i = 1; i<=t o t a l N r T a s k s ( t a ) ; i ++){

i f ( i<t o t a l N r T a s k s ( t a ) ) {

r e s+=” T as k c ”+ i + ” & l t ; ” ; / / ” , ” ; }

e l s e {

r e s+=” T as k c ”+ i +” , ” ; }

}

f o r(i n t i = 1; i<n r O f P r o c ( pa ) ; i ++){

conn+=”Con”+ i + ” & l t ; ” ; / / ” , ” ; / / ” & l t ; ” ; s y n+=” Syn ”+ i +” , Sch ”+ i +” , A l l o c ”+ i +” , ” ; }

conn += ”Con”+n r O f P r o c ( pa ) ;

s y n += ” Syn ”+n r O f P r o c ( pa ) + ” , Sch ” +n r O f P r o c ( pa ) + ” , A l l o c ” +n r O f P r o c ( pa ) ;

r e s += conn + ” , ” ;

r e s += s y n + ” , R e s c h e d u l e r ” ;

f o r (i n t i = 0 ; i<e n v i r o n m e n t s . l e n g t h ; i ++) { r e s += ” , env ” + i ;

}

f o u t . p r i n t ( r e s ) ; }

/∗ ∗

∗ What i s t h e t o t a l n u m b e r o f c o s t s i n t h e s y s t e m ?

∗ @ r e t u r n i n t T h e t o t a l n u m b e r o f c o s t s .

∗/

p r i v a t e s t a t i c i n t t o S t r i n g N r O f C o s t s ( ) { r e t u r n a p p l i c a t i o n . c a . l e n g t h ; }

/∗ ∗

∗ G e n e r a t e s a a r r a y f o r UPPAAL c o n t a i n i n g i n f o r m a t i o n a b o u t w h i c h t a s k s

∗ u s e s w h i c h c o s t s , a n d h o w m uc h o f t h e s e t h e y a r e u s i n g .

∗ W r i t t e n t o t h e m o d e l u s i n g f o u t .

∗/

p r i v a t e s t a t i c v oi d t o S t r i n g C o s t s U s e d ( ) { f o u t . p r i n t ( ” i n t t o t a l C o s t [M] [ NOC] ={” ) ;

f o r (i n t j = 0 ; j<p l a t f o r m . p r o c e s s o r s . l e n g t h ; j ++) {

i f ( j>0)

f o u t . p r i n t ( ” , ” ) ; f o u t . p r i n t ( ”{” ) ;

f o r (i n t i = 0 ; i<a p p l i c a t i o n . c a . l e n g t h ; i ++) {

i f ( i>0)

f o u t . p r i n t ( ” , ” ) ; f o u t . p r i n t ( ” 0 ” ) ; }

f o u t . p r i n t ( ”}” ) ; }

f o u t . p r i n t ( ”};\n” ) ; }

/∗ ∗

∗ T h e c o s t−a r r a y i s g e n e r a t e d .

∗/

p r i v a t e s t a t i c v oi d t o S t r i n g C o s t s ( ) { S t r i n g s t r = ” i n t c o s t s [MN ] [ NOC ] [ 5 ] = ” ;

f o r (i n t i = 0 ; i<t o t a l N r T a s k s ( a p p l i c a t i o n . t a s k s ) ; i ++) { i f ( i ==0)

s t r += ”{” ; e l s e

s t r += ” , ” ;

f o r (i n t j = 0 ; j<a p p l i c a t i o n . c a . l e n g t h ; j ++) { i f ( j ==0)

s t r += ”{” ; e l s e

s t r += ” , ” ;

f o r (i n t k = 0 ; k<a p p l i c a t i o n . c a [ j ] . c o s t s [ i ] . l e n g t h ; k++) { i f ( k == 0 )

s t r += ”{” ; e l s e

s t r += ” , ” ;

s t r += a p p l i c a t i o n . c a [ j ] . c o s t s [ i ] [ k ] ; i f ( k == a p p l i c a t i o n . c a [ j ] . c o s t s [ i ] . l e n g t h−1)

s t r += ”}” ; }

i f ( j == a p p l i c a t i o n . c a . l e n g t h−1) { f o u t . p r i n t ( s t r + ”}” ) ;

s t r = ” ” ; }

}

i f ( i==t o t a l N r T a s k s ( a p p l i c a t i o n . t a s k s )−1) { f o u t . p r i n t ( ”};\n” ) ;

} } } /∗ ∗

∗ G e n e r a t e s i n f o r m a t i o n a b o u t s h a r e d c o s t s ( e . g . m e m o r y s h a r i n g )

∗/

p r i v a t e s t a t i c v oi d c o s t s D e p e n d ( ) {

S t r i n g s t r = ” i n t c o s t D e p e n d [MN ] [ MN] = ” ;

f o r (i n t i = 0 ; i<a p p l i c a t i o n . c a [ 0 ] . s h a r e d . l e n g t h ; i ++) { i f ( i ==0)

s t r += ”{” ; e l s e

s t r += ” , ” ; s t r += ”{” ;

f o r (i n t j = 0 ; j<a p p l i c a t i o n . c a [ 0 ] . s h a r e d [ i ] . l e n g t h ; j ++) {

i f ( j>0)

s t r += ” , ” ;

s t r += a p p l i c a t i o n . c a [ 0 ] . s h a r e d [ i ] [ j ] ; }

f o u t . p r i n t ( s t r+ ”}” ) ; s t r = ” ” ;

i f ( i==a p p l i c a t i o n . c a [ 0 ] . s h a r e d . l e n g t h−1) f o u t . p r i n t ( ”};\n” ) ;

} } /∗ ∗

∗ G e n e r a t e s a n a r r a y o f s i z e MNxMN c o n t a i n i n g z e r o s t o h a n d l e

∗ t h e s h a r e d c o s t s f r o m t h e m o d e l .

∗/

p r i v a t e s t a t i c v oi d s h a r e d C o s t s ( ) {

S t r i n g s t r = ” i n t s h a r e d C o s t [MN ] [ MN] = ” ;

f o r (i n t i = 0 ; i<t o t a l N r T a s k s ( a p p l i c a t i o n . t a s k s ) ; i ++) { i f ( i ==0)

s t r += ”{” ; e l s e

s t r += ” , ” ; s t r += ”{” ;

f o r (i n t j = 0 ; j<t o t a l N r T a s k s ( a p p l i c a t i o n . t a s k s ) ; j ++){

i f ( j>0)

s t r += ” , ” ; s t r += ” 0 ” ; }

f o u t . p r i n t ( s t r+ ”}” ) ; s t r = ” ” ;

i f ( i==t o t a l N r T a s k s ( a p p l i c a t i o n . t a s k s )−1) f o u t . p r i n t ( ”};\n” ) ;

} } /∗ ∗

∗ G e n e r a t e s t h e e n t i r e XML−s y s t e m . M a k e s u s e o f t h e f o l l o w i n g f u n c t i o n s :

∗ n r O f P r o c , m a x N r O f T a s k s , t o t a l N r O f T a s k s , n r O f R e s o u r c e s , T o S t r i n g N r O f C o s t s ,

∗ t y p e O f P r o c , l o c a l T o G l o b a l , t o S t r i n g U s e d C o s t s , t o S t r i n g N e e d e d , s h a r e d C o s t s ,

∗ c o s t D e p e n d , t o S t r i n g A l l , t o S t r i n g S y s t e m

∗/

s t a t i c v oi d mkXML( ) { f o u t . p r i n t (

”<?xml v e r s i o n = ’ 1 . 0 ’ e n c o d i n g = ’ u t f−8’?><!DOCTYPE n t a PUBLIC ’−// U ppaal Team //DTD F l a t Sy s tem 1 . 1 / /EN ’

’ h t t p : / /www. i t . uu . s e / r e s e a r c h / g r o u p / d a r t s / u p p a a l / f l a t−1 1 . dtd’><nta><d e c l a r a t i o n>\n”

” c o n s t i n t M = ”+n r O f P r o c ( p l a t f o r m . p r o c e s s o r s )+” ; // The number o f P r o c e s s o r s\n” +

” c o n s t i n t N = ”+maxNrTasks ( a p p l i c a t i o n . t a s k s )+” ; // The maximum number o f t a s k s p e r P r o c e s s o r\n” +

” c o n s t i n t MN = ”+t o t a l N r T a s k s ( a p p l i c a t i o n . t a s k s )+” ; // The t o t a l number o f t a s k s\n”

” c o n s t i n t R = ” + n r O f R e s o u r c e s ( ) + ” ; / / The t o t a l number o f r e s o u r c e s\n” +

” c o n s t i n t NOC = ”+t o S t r i n g N r O f C o s t s ( )+” ; // T o t a l number o f c o s t s\n ” +

”\n” +

” // s y m b o l i c r e p r e s e n t a t i o n o f s c h e d u l i n g a c t i o n s\n” +

” c o n s t i n t REA = 0 , RUN = 1 , PRE = 2 , FIN = 3 ; \n” +

”\n” +

” // s y m b o l i c r e p r e s e n t a t i o n o f i n t e r n a l p r o c e s s o r s y n c h r o n i z i n g\n” +

” c o n s t i n t SYN = 0 , SCH = 1 , ALL = 2 ;\n” +

”\n” +

” // s y m b o l i c r e p r e s e n t a t i o n o f s t a t e s f o r c o s t−m odel\n” +

” c o n s t i n t STATIC = 0 , IDLE = 1 , READY = 2 , RUNNING = 3 , PREEMPTED=4;\n” +

” // S y m b o l i c r e p r e s e n t a t i o n o f memory and pow er .\n” +

” c o n s t i n t Memory = 0 , Power = 1 ;\n ” +

”\n” +

” // S y m b o l i c r e p r e s e n t a t i o n o f c o s t t y p e s .\n” +

” c o n s t i n t HARD = 0 , SOFT = 1 , FIRM = 2 ;\n” +

”\n” +

” // s y m b o l i c r e p r e s e n t a t i o n o f s c h e d u l i n g p r i n c i p l e s\n” +

” c o n s t i n t FP = 0 , RM = 1 , DM = 2 , EDF = 3 ;\n ” +

”\n” +

” // s y m b o l i c r e p r e s e n t a t i o n o f a l l o c a t i o n a l g o r i t h m s\n” +

” c o n s t i n t PCS=0 , PRI INH = 1 , NPCS = 2 ;\n” +

”\n” ) ; t y p e O f P r o c ( ) ;

l o c a l T o G l o b a l ( a p p l i c a t i o n . t a s k s ) ;

f o u t . p r i n t ( ” b r o a d c a s t chan r e s c h e d u l e ; // b r o a d c a s t c h a n n e l f o r r e s c h e l d u l i n g a f t e r a t a s k h a s f i n i s h e d\n” +

” chan t r i g g e r [MN] ;\n” +

”\n” +

” chan a c t i v a t e R e s c h e d u l e ;\n ” +

” chan c a c t [M ] [ 3 ] ; // c h a n n e l a r r a y f o r i n t e r n a l p r o c e s s o r a c t i o n s\n ” +

” chan s a c t [M ] [ 4 ] ; // c h a n n e l a r r a y f o r s c h e d u l i n g a c t i o n s\n ” +

” b o o l p r e e m p t e d ; // s e t when any t a s k i s p r e e m p t e d\n” +

”\n” +

” i n t [ 0 , N ] t i d [M] ; // t r a n s f e r o f l o c a l t a s k i d from t a s k t o c o n t r o l l e r\n” +

” i n t [ 0 , N ] c u r t i d [M] ; // v a r i a b l e u s e d t o h o l d t h e i d o f t h e t a s k c u r r e n t l y c h o s e n\n”

” i n t [ 0 ,MN] g t i d [M] ; // t r a n s f e r o f g l o b a l t a s k i d from t a s k t o c o n t r o l l e r\n” +

” i n t [ 0 ,MN] f t i d [M] ; // t a s k i d o f t a s k w hi ch h a s f i n i s h e d , f t i d =0 means no f i n i s h e d t a s k\n ” +

” i n t [ 0 ,MN] l t i d [M] ; // v a r i a b l e u s e d t o h o l d t h e i d o f t h e t a s k c u r r e n t l y r u n n i n g\n”

” b o o l Ready [M] [ N ] ; // a r r a y o f t a s k s w hi ch hav e i s s u e d r e a d y s i g n a l s\n” +

” b o o l S y n c h r o n i z e d [MN ] ; // a r r a y o f t a s k s w hi ch a r e n o t a w a i t i n g d e p e n d e n c i e s t o be r e s o l v e d\n” +

” b o o l A l l o c a t e d [MN ] ; // a r r a y o f t a s k s w hi ch a r e n o t a w a i t i n g r e s o u r c e s\n” +

” b o o l t a s k R e a d y F o r T r i g g e r i n g [MN ] ; // a r r a y h o l d i n g t a s k s r e a d y f o r t r i g g e r i n g\n ” +

” b o o l p r e e m p t e d O r I d l e [MN ] ; // A rray u s e d i n t h e c o s t m odel t o t e s t i f a t a s k i s p r e e m p t e d o r i d l e\n” +

” // A rray c o n t a i n i n g t h e n e e d e d r e s o u r c e s ( a s b o o l e a n s )\n ” ) ; t o S t r i n g N e e d e d ( ) ;

f o u t . p r i n t ( ”\n” +

” i n t U s e d R e s o u r c e s [M] [ R ] ; // a r r a y i n d i c a t i n g w h e t h e r a r e s o u r c e i s t a k e n\n” +

”\n” +

” b o o l WaitDep [MN] ; // a r r a y f o r t a s k s w hi ch a r e a w a i t i n g d e p e n d e n c i e s t o be r e s o l v e d\n” +

”\n” +

” b o o l r u n n i n g [M] ; // i n d i c a t i n g w e t h e r a t a s k i s c u r r e n t l y r u n n i n g on t h e p r o c e s s o r\n” +

”\n” +

” b o o l m i s s e d D e a d l i n e = f a l s e ; // S e t i f a hard−d e a d l i n e t a s k m i s s e s a d e a d l i n e .\n” +

” b o o l e n d S t a t e [MN] ; // S e t when a t a s k r e a c h e s i t s end s t a t e .\n” +

”\n” ) ;

t o S t r i n g C o s t s U s e d ( ) ; f o u t . p r i n t ( ”\n” +

” / / [ t a s k 1 . . taskMN ] [ mem, pow er ] [ s t a t i c , i d l e , r e a d y , run , preem pt ]\n” ) ; t o S t r i n g C o s t s ( ) ;

f o u t . p r i n t ( ”\n” +

” // W r i t e r / Reader\n” ) ; c o s t s D e p e n d ( ) ;

f o u t . p r i n t l n ( ”\n ” ) ; s h a r e d C o s t s ( ) ; f o u t . p r i n t l n ( ”\n ” +

” // C r i t e r i a u s a b l e i n s c h e d u l i n g\n ” +

” i n t s t a t i c C r i t e r i a [M ] [ N ] ; // c r i t e r i o n u s e d f o r s t a t i c s c h e d u l i n g and c o n t a i n s t h e o r i g i n a l p a r a m e t e r s f o r dy nam i c s c h e d u l i n g .\n” +

” i n t d y n a m i c C r i t e r i a [M] [ N ] ; // c r i t e r i o n u s e d f o r dy nam i c s c h e d u l i n g\n”

”\n ” +

” // a r r a y f o r o r i g i n a l d e p e n d e n c i e s , 1 f o r dependency , 0 f o r no d e p e n d e n c y\n” +

”\n ” +

” b o o l o r i g d e p [MN ] [ MN]= ” ) ; t o S t r i n g D e p ( a p p l i c a t i o n . d e p e n d e n c i e s ) ; f o u t . p r i n t ( ”\n ” +

” // d y n a m i c a l l y u p d a t e d a r r a y f o r c u r r e n t d e p e n d e n c i e s\n ” +

” b o o l depend [MN] [ MN]= ” ) ; t o S t r i n g D e p ( a p p l i c a t i o n . d e p e n d e n c i e s ) ; f o u t . p r i n t ( ”\n ” +

” // L o c k i n g m echani s m s\n ” +

” b o o l nowrun [M] ; // e n s u r i n g c o m p l e t i o n o f ’ r u n s ’ b e f o r e r e a c t i n g on r e a d y\n” +

” b o o l p e n d i n g [MN ] ; // e n s u r i n g g l o b a l w a i t f o r f i n i s h &amp ; r e a d y b e f o r e n e x t ’ run ’\n” +

” b o o l h e d f [MN] ; // e n s u r i n g s y n c h r o n i z a t i o n on e x t r a s t a t e i n r e a d y f o r e d f\n ” +

” b o o l h t [M ] ; // e n s u r i n g c o m p l e t i o n o f a l l ’ r u n s ’ b e f o r e n e x t ’ run ’\n” +

” b o o l h f i n [M] ; // e n s u r i n g r e a c t i o n on f i n i s h b e f o r e r e a d y\n” +

” b o o l l i n [M] ; // e n s u r i n g c o m p l e t i o n o f l o c a l s c h e d u l i n g b e f o r e g l o c a l r e s c h e d u l e\n” +

” b o o l h r ; // e n s u r i n g r e s c h e d u l e b e f o r e n e x t ’ run ’\n” +

” b o o l c o n t r o l l e r L o c k [M] ; // E x t e r n a l c o n t r o l l e r l o c k\n ” +

” b o o l p r o c e s s i n g [M] ; // I n t e r n a l c o n t r o l l e r l o c k\n” +

”\n ” +

” // f u n c t i o n c h e c k i n g f o r d e p e n d e n c i e s f o r t a s k t\n” +

” b o o l t a s k H a s D e p e n d e n c y ( i n t t ) {\n ” +

” f o r ( i n i : i n t [ 0 ,MN−1 ] ) { \n ” +

” i f ( depend [ t ] [ i n i ] ) {\n” +

” r e t u r n t r u e ;\n” +

” }\n” +

” }\n ” +

” r e t u r n f a l s e ;\n” +

”}\n ” +

”\n ” +

” // f u n c t i o n u p d a t i n g d e p e n d e n c i e s when t a s k t h a s f i n i s h e d\n” +

” v o i d opdDep ( i n t t ) {\n” +

” f o r ( i n i : i n t [ 0 ,MN−1 ] ) {\n” +

” depend [ i n i ] [ t ]= f a l s e ;\n” +

” }\n ” +

”}\n ” +

”\n ” +

” // f u n c t i o n s e t t i n g t h e o r i g i n a l d e p e n d e n c y v a l u e s f o r t a s k t\n” +

” v o i d s e t O r i g D e p ( i n t t ) {\n” +

” f o r ( i n i : i n t [ 0 ,MN−1 ] ) {\n” +

” depend [ t ] [ i n i ]= o r i g d e p [ t ] [ i n i ] ;\n” +

” }\n ” +

”}\n ” +

”\n ” +

” // f u n c t i o n c h e c k i n g f o r e x i s t a n c e o f b o o l e a n v a l u e i n a r r a y o f s i z e M\n” +

” b o o l l o c k e d ( b o o l l a [M] ) {\n” +

” f o r ( i n i : i n t [ 0 ,M−1 ] ) { \n” +

” i f ( l a [ i n i ] ) {\n” +

” r e t u r n t r u e ;\n” +

” }\n” +

” }\n ” +

” r e t u r n f a l s e ;\n” +

”}\n ” +

”\n ” +

” // f u n c t i o n c h e c k i n g f o r e x i s t a n c e o f b o o l e a n v a l u e i n a r r a y o f s i z e N\n” +

” b o o l pend ( b o o l pen [ N ] ) {\n” +

” b o o l b = f a l s e ;\n” +

” f o r ( i n i : i n t [ 0 , N−1 ] ) {\n” +

” i f ( pen [ i n i ] == t r u e ) {\n” +

” r e t u r n t r u e ; \n” +

” }\n” +

” }\n ” +

” r e t u r n f a l s e ;\n” +

”}\n ” +

”\n ” +

” // F u n c t i o n t o v e r i f y i f a l l t a s k s h a s r e a c h e d t h e i r end s t a t e s\n ” +

” b o o l a l l F i n i s h ( ) {\n” +

” f o r ( i n i : i n t [ 0 , MN−1 ] ) {\n” +

” i f ( ! e n d S t a t e [ i n i ] ) {\n” +

” r e t u r n f a l s e ;\n” +

” }\n” +

” }\n ” +

” r e t u r n t r u e ;\n” +

”}\n ” +

”\n ” +

” // f u n c t i o n c h e c k i n g f o r e x i s t a n c e o f b o o l e a n v a l u e i n a r r a y o f s i z e MN\n” +

” b o o l pendMN ( b o o l pen [MN] ) {\n” +

” b o o l b = f a l s e ;\n” +

” f o r ( i n i : i n t [ 0 ,MN−1 ] ) {\n” +

” i f ( pen [ i n i ] == t r u e ) {\n” +

” r e t u r n t r u e ; \n” +

” }\n” +

” }\n ” +

” r e t u r n f a l s e ;\n” +

”}\n” +

”\n” +

” // F u n c t i o n u s e d t o c h e c k t h e t o t a l c o s t i n any s t a t e\n ” +

” i n t t o t a l C o s t U s e d ( i n t c o s t n r ) {\n” +

” i n t t o t a l = 0 ;\n” +

” f o r ( i n i : i n t [ 0 ,M−1 ] ) {\n” +

” t o t a l += t o t a l C o s t [ i n i ] [ c o s t n r ] ; \n” +

” }\n ”+

” r e t u r n t o t a l ;\n” +

”}\n” +

”\n” +

” // F u n c t i o n u s e d t o s e e i f any r e a d y o r f i n i s h s i g n a l s t i l l n e e d s t o be r e c i e v e d\n”

” b o o l n o t S i g n a l s P e n d i n g ( ) {\n” +

” r e t u r n ( ! l o c k e d ( h t )\n ” +

” &&amp ; ! l o c k e d ( h f i n )\n ” +

” &&amp ; ! l o c k e d ( p r o c e s s i n g )\n” +

” &&amp ; ! pendMN ( p e n d i n g )\n” +

” &&amp ; ! pendMN ( h e d f ) ) ;\n” +

”}\n” +

”\n” +

” // F u n c t i o n t h a t adds c o s t t o t h e c o s t u s e d i n b e g i n n i n g o f a t i m e u n i t .\n” +

” v o i d u p d a t e C o s t ( i n t g t a s k n r , i n t s c h n r , i n t S t a t e ) {\n ” +

” i f ( S t a t e == READY &&amp ; p r e e m p t e d O r I d l e [ g t a s k n r−1 ] ) {\n” +

” S t a t e = PREEMPTED;\n ” +

” }\n ” +

” f o r ( i : i n t [ 0 ,NOC−1 ] ) {\n ” +

” i f ( i==Memory &&amp ; S t a t e == RUNNING) {\n” +

” i n t s haredC os tT em p = 0 ;\n” +

” f o r ( j : i n t [ 0 , MN−1 ] ) {\n” +

” s haredC os tT em p += s h a r e d C o s t [ g t a s k n r−1 ] [ j ] ;\n” +

” s h a r e d C o s t [ g t a s k n r−1 ] [ j ] = c o s t D e p e n d [ g t a s k n r−1 ] [ j ] ;\n” +

” }\n” +

” t o t a l C o s t [ s c h n r−1 ] [ i ] += c o s t s [ g t a s k n r−1 ] [ i ] [ S t a t e ]−s haredC os tT em p ;\n ” +

” }\n” +

” e l s e {\n” +

” t o t a l C o s t [ s c h n r−1 ] [ i ] += c o s t s [ g t a s k n r−1 ] [ i ] [ S t a t e ] ;\n” +

” }\n” +

” }\n ” +

”}\n” +

”\n” +

” // F u n c t i o n t h a t r e s e t s t h e c o s t i n t h e end o f a t i m e u n i t\n” +

” v o i d r e s e t C o s t ( i n t g t a s k n r , i n t s c h n r , i n t S t a t e ) {\n” +

” i f ( S t a t e == READY &&amp ; p r e e m p t e d O r I d l e [ g t a s k n r−1 ] ) {\n” +

” S t a t e = PREEMPTED;\n ” +

” }\n ” +

” i f ( ! ( S t a t e == IDLE &&amp ; ! p r e e m p t e d O r I d l e [ g t a s k n r−1 ] ) ) {\n ” +

” f o r ( i : i n t [ 0 ,NOC−1 ] ) {\n” +

” // R e s e t s t h e m em ory us e a f t e r f i r s t t i m e u n i t .\n” +

” i f ( i==Memory &&amp ; S t a t e == RUNNING) {\n” +

” i n t s haredC os tT em p = 0 ;\n” +

” f o r ( j : i n t [ 0 , MN−1 ] ) {\n” +

” i f ( s h a r e d C o s t [ j ] [ g t a s k n r−1] &g t ; 0 ) {\n” +

” f o r ( k : i n t [ 0 , M−1 ] ) {\n ” +

” f o r ( l : i n t [ 0 , N−1 ] ) {\n” +

” i f ( l t o g [ k ] [ l ] == ( j +1) ) {\n ” +

” t o t a l C o s t [ k ] [ i ] −= s h a r e d C o s t [ j ] [ g t a s k n r−1 ] ;\n” +

” s h a r e d C o s t [ j ] [ g t a s k n r−1] = 0 ;\n” +

” }\n” +

” }\n ” +

” }\n” +

” i f ( s h a r e d C o s t [ g t a s k n r−1 ] [ j ] == c o s t D e p e n d [ g t a s k n r−1 ] [ j ] )\n” +

” s haredC os tT em p−= s h a r e d C o s t [ g t a s k n r−1 ] [ j ] ;\n ” +

” e l s e\n ” +

” s haredC os tT em p−= c o s t D e p e n d [ g t a s k n r−1 ] [ j ] ;\n ” +

” }\n” +

” t o t a l C o s t [ s c h n r−1 ] [ i ]−= c o s t s [ g t a s k n r−1 ] [ i ] [ S t a t e ]+ s haredC os tT em p ;\n ” +

” }\n” +

” e l s e {\n ” +

” t o t a l C o s t [ s c h n r−1 ] [ i ]−= c o s t s [ g t a s k n r−1 ] [ i ] [ S t a t e ] ;\n” +

” }\n” +

” }\n ” +

”}\n” +

”\n</ d e c l a r a t i o n><t e m p l a t e><name>Task</name>c o n s t i n t s c h n r , c o n s t i n t g t a s k n r , c o n s t i n t t a s k n r , c o n s t i n t emin , c o n s t i n t emax , c o n s t i n t dead , c o n s t i n t o f f s e t , c o n s t i n t pti m e , i n t p r i o r , i n t [ 0 , N ] &amp ; t i d , i n t [ 0 , MN]

&amp ; g t i d , chan &amp ; r e a d y , chan &amp ; run , chan &amp ; preem pt , chan &amp ; f i n i s h , c o n s t i n t [ 0 , 2 ] sd , i n t maxCount<d e c l a r a t i o n>c l o c k x ;\n ” +

” i n t c o u n t e r = 0 ;\n” +

”\n” +

” i n t cp ;\n” +

” i n t c r ;\n” +

”\n” +

” i n t i ;\n” +

”\n ” +

” b o o l t a s k H a s O f f s e t ( ) {\n ” +

” r e t u r n ( o f f s e t &g t ; 0 ) ;\n ” +

”}\n ” +

”\n ” +

” b o o l maxCountReached ( ) {\n” +

” r e t u r n ( c o u n t e r &g t ;= maxCount &&amp ; maxCount &g t ; 0 ) ;\n” +

”}\n ” +

”\n ” +

” v o i d u p d a t e E n d S t a t e ( ) {\n ” +

” e n d S t a t e [ g t a s k n r−1]= t r u e ;\n” +

” p e n d i n g [ g t a s k n r−1] = f a l s e ;\n” +

”}\n ” +

”\n ” +

” v o i d f i r m D e a d l i n e M i s s e s ( ) {\n” +

” d y n a m i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1] = 0;\n” +

” Ready [ s c h n r−1 ] [ t a s k n r−1]= f a l s e ;\n ” +

” S y n c h r o n i z e d [ g t a s k n r−1]= f a l s e ;\n ” +

” A l l o c a t e d [ g t a s k n r−1]= f a l s e ;\n” +

” x = cp ;\n” +

”}\n ” +

”\n ” +

” v o i d f i n i s h B e f o r e P e r i o d E n d ( ) {\n” +

” t i d=t a s k n r ;\n ” +

” g t i d = g t a s k n r ;\n” +

” d y n a m i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1] = 0;\n” +

” h f i n [ s c h n r−1]= f a l s e ;\n ” +

” x = cp ;\n” +

” p r e e m p t e d O r I d l e [ g t a s k n r−1] = t r u e ;\n”+

” u p d a t e C o s t ( g t a s k n r , s c h n r , IDLE ) ;\n” +

”}\n ” +

”\n ” +

” v o i d f i n i s h A t P e r i o d E n d ( ) {\n” +

” i f ( ! ( s d == FIRM &&amp ; cp==p t i m e &&amp ; c r&g t ; 0 ) ) {\n ” +

” t i d=t a s k n r ;\n” +

” g t i d=g t a s k n r ;\n” +

” }\n ” +

” d y n a m i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1] = 0;\n” +

” h f i n [ s c h n r−1]= f a l s e ;\n ” +

” i f ( c o u n t e r & l t ; maxCount | | maxCount == 0 ) {\n” +

” p e n d i n g [ g t a s k n r−1]= t r u e ;\n” +

” }\n ” +

” i f ( cp &g t ; p t i m e &&amp ; s d == SOFT) {\n” +

” cp = p t i m e ;\n” +

” }\n ” +

” x=cp ;\n” +

”}\n ” +

”\n ” +

” v o i d runOneTimeUnit ( ) {\n ” +

” h t [ s c h n r−1]= f a l s e ;\n ” +

” l i n [ s c h n r−1]= f a l s e ; \n ” +

”\n ” +

” c r−−; \n” +

” cp++;\n” +

” d y n a m i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1]−−;\n” +

” nowrun [ s c h n r−1]= f a l s e ;\n” +

”\n ” +

” i f ( c r==0 | | ( s d == FIRM &&amp ; cp==dead ) ) {\n” +

” h f i n [ s c h n r−1]= t r u e ;\n” +

” }\n ” +

” r e s e t C o s t ( g t a s k n r , s c h n r , RUNNING) ;\n” +

”}\n ” +

”\n ” +

” b o o l tas k H as MoreRunti m e ( ) {\n” +

” r e t u r n ( c r&g t ; 0 ) ;\n” +

”}\n ” +

”\n ” +

” b o o l d e a d l i n e M i s s e d ( ) {\n ” +

” r e t u r n ( cp==dead &&amp ; s d == HARD &&amp ; t i d != t a s k n r ) ;\n” +

”}\n ” +

”\n ” +

” b o o l d e a d l i n e M i s s e d R u n ( ) {\n” +

” r e t u r n ( cp&g t ; dead &&amp ; s d == HARD) ;\n” +

”}\n ” +

”\n ” +

” b o o l deadl i neN otMi s s edY etO rSO FT ( ) {\n” +

” r e t u r n ( ( ( cp& l t ; dead &&amp ; s d == HARD) \n” +

” | | ( s d == SOFT ) \n” +

” | | ( cp& l t ; dead−1 &&amp ; s d==FIRM) )\n” +

” &&amp ; ! l o c k e d ( c o n t r o l l e r L o c k )\n” +

” &&amp ; ! l o c k e d ( h f i n )\n” +

” &&amp ; ! l o c k e d ( h t )\n ” +

” &&amp ; ! pendMN ( p e n d i n g ) ) ;\n” +

”}\n ” +

”\n ” +

” b o o l deadl i neN otMi s s edO rSO FT ( ) {\n ” +

” r e t u r n ( ( ( cp& l t ;= dead &&amp ; s d == HARD) \n” +

” | | ( s d == SOFT) \n” +

” | | ( cp& l t ;= dead−1 &&amp ; s d==FIRM) )\n” +

” &&amp ; t i d == t a s k n r ) ;\n” +

”}\n” +

”\n” +

” b o o l F i r m d e a d l i n e W i l l M i s s ( ) {\n” +

” r e t u r n ( s d==FIRM\n” +

” &&amp ; cp == ( dead−1)\n ” +

” &&amp ; t i d != t a s k n r\n ” +

” &&amp ; ! l o c k e d ( c o n t r o l l e r L o c k )\n ”+

” &&amp ; ! l o c k e d ( h f i n ) \n” +

” &&amp ; ! l o c k e d ( h t ) ) ;\n ” +

”}\n” +

”\n” +

” b o o l F i r m d e a d l i n e M i s s e d B e f o r e P e r i o d ( ) {\n” +

” r e t u r n ( s d==FIRM\n” +

” &&amp ; cp == dead\n” +

” &&amp ; p t i m e &g t ; dead\n” +

” &&amp ; c r &g t ; 0 ) ;\n ” +

”}\n” +

”\n” +

” b o o l F i r m d e a d l i n e M i s s e d A t P e r i o d ( ) {\n ” +

” r e t u r n ( s d==FIRM\n” +

” &&amp ; cp == p t i m e\n ” +

” &&amp ; c r &g t ; 0 ) ;\n ” +

”}\n” +

”\n” +

” v o i d u p d a t e M i s s e d D e a d l i n e ( ) {\n” +

” m i s s e d D e a d l i n e =t r u e ;\n ” +

”}\n” +

”\n” +

” v o i d s e t P e r i o d C l o c k ( ) {\n ” +

” x=pti m e−1;\n ” +

”}\n” +

”\n” +

” v o i d i n i t O n e R u n ( ) {\n” +

” x =0;\n” +

” l i n [ s c h n r−1]= t r u e ;\n” +

” nowrun [ s c h n r−1]= t r u e ;\n ” +

” p r e e m p t e d O r I d l e [ g t a s k n r−1] = f a l s e ;\n” +

” u p d a t e C o s t ( g t a s k n r , s c h n r , RUNNING) ;\n” +

”}\n” +

”\n” +

” v o i d s e t P r e e m p t e d ( ) {\n” +

” p r e e m p t e d=t r u e ;\n” +

” p r e e m p t e d O r I d l e [ g t a s k n r−1] = t r u e ;\n” +

” x =0;\n” +

”}\n” +

”\n” +

” v o i d i n i t O f f s e t ( ) {\n” +

” x =0;\n” +

” u p d a t e C o s t ( g t a s k n r , s c h n r , STATIC) ;\n” +

”}\n” +

”\n” +

” v o i d e n s u r e R u n C o m p l e t i o n ( ) {\n” +

” h t [ s c h n r−1]= t r u e ;\n” +

”}\n” +

”\n” +

” b o o l r e a d y F o r N e x t P e r i o d ( ) {\n” +

” r e t u r n ! ( nowrun [ s c h n r−1] \n” +

” | | l o c k e d ( h t )\n ” +

” | | l o c k e d ( h f i n )\n” +

” | | pendMN ( h e d f )\n” +

” | | maxCountReached ( ) ) ;\n ” +

”}\n” +

”\n” +

” v o i d s e t S t a t i c S c h e d u l i n g ( ) {\n” +

” i f ( p r o c e s s o r S c h e d u l i n g [ s c h n r−1] == FP) {\n ” +

” s t a t i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1]= p r i o r ; \n” +

” }\n ” +

” i f ( p r o c e s s o r S c h e d u l i n g [ s c h n r−1] == RM) {\n ” +

” s t a t i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1]=p t i m e ; \n” +

” }\n ” +

” i f ( p r o c e s s o r S c h e d u l i n g [ s c h n r−1] == DM) {\n ” +

” s t a t i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1]=dead ; \n ” +

” }\n ” +

”}\n” +

”\n” +

” v o i d i n i t N e x t P e r i o d ( i n t i ) {\n” +

” cp =0;\n” +

” t i d=t a s k n r ;\n ” +

” p e n d i n g [ g t a s k n r−1]= f a l s e ;\n” +

” d y n a m i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1]=dead ;\n ” +

” s e t O r i g D e p ( g t a s k n r−1) ;\n ” +

” c r=i ;\n” +

” i f ( ! maxCount==0) {\n” +

” c o u n t e r ++;\n ” +

” }\n ” +

” s e t S t a t i c S c h e d u l i n g ( ) ;\n” +

”\n ” +

” x =0;\n” +

”} \n ” +

”\n ” +

” v o i d s e t W a i t F o r U p d a t e D y n a m i c S c h e d u l i n g ( ) {\n ” +

” h e d f [ g t a s k n r−1]= t r u e ;\n” +

” u p d a t e C o s t ( g t a s k n r , s c h n r , READY) ;\n” +

”}\n ” +

”\n ” +

” v o i d u p d a t e D y n a m i c S c h e d u l i n g ( ) {\n ” +

” d y n a m i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1]−−;\n” +

” x =0;\n” +

” cp++;\n” +

” h e d f [ g t a s k n r−1]= f a l s e ;\n” +

” r e s e t C o s t ( g t a s k n r , s c h n r , READY) ;\n” +

”}\n ” +

”\n ” +

” v o i d i n i t N o O f f s e t ( ) {\n ” +

” p e n d i n g [ g t a s k n r−1]= t r u e ;\n” +

” u p d a t e C o s t ( g t a s k n r , s c h n r , STATIC) ;\n” +

”\n ” +

” x=p t i m e ;\n ” +

”}\n ” +

”\n ” +

” v o i d s e t P e n d ( ) {\n” +

” i f ( c o u n t e r & l t ; maxCount | | maxCount == 0 ) { \n” +

” p e n d i n g [ g t a s k n r−1]= t r u e ;\n” +

” }\n ” +

” r e s e t C o s t ( g t a s k n r , s c h n r , IDLE ) ;\n” +

” p r e e m p t e d O r I d l e [ g t a s k n r−1] = f a l s e ;\n”+

”}\n ” +

”\n ” +

” b o o l t a s k F i n i s h B e f o r e P e r i o d E n d ( ) {\n” +

” r e t u r n ( c r ==0\n” +

” &&amp ; ! l o c k e d ( h t )\n ” +

” &&amp ; ! pendMN ( h e d f )\n” +

” &&amp ; cp& l t ; p t i m e\n ” +

” &&amp ; ( cp& l t ;= dead \n” +

” | | ( cp&g t ; dead &&amp ; s d==SOFT) ) ) ;\n ” +

”}\n ” +

”\n ” +

” b o o l t a s k F i n i s h A t P e r i o d E n d ( ) {\n” +

” r e t u r n ( c r ==0\n” +

” &&amp ; ! l o c k e d ( h t )\n ” +

” &&amp ; ! pendMN ( h e d f )\n” +

” &&amp ; ( ( cp==p t i m e &&amp ; cp==dead ) \n ” +

” | | ( cp &g t ; p t i m e &&amp ; s d == SOFT) ) ) ;\n ” +

”}\n ” +

”\n ” +

” b o o l ready ForN ex tRun ( ) {\n” +

” r e t u r n ( c r&g t ; 0 \n” +

” &&amp ; ! pendMN ( p e n d i n g )\n” +

” &&amp ; ! l o c k e d ( h t )\n ” +

” &&amp ; ! l o c k e d ( h f i n )\n” +

” &&amp ; ! l o c k e d ( c o n t r o l l e r L o c k )\n” +

” &&amp ; ! h r\n” +

” &&amp ; ( ( s d == SOFT) \n” +

” | | ( cp & l t ; dead &&amp ; s d == FIRM) \n” +

” | | ( cp & l t ;= dead &&amp ; s d == HARD) ) ) ; \n” +

” // &&amp ; ! pendMN ( h e d f ) ) ;\n” +

”}\n ” +

”\n ” +

”</ d e c l a r a t i o n><l o c a t i o n i d =\” i d 0\” x=\”−320\” y=\”−424\”><name x=\”−304\”

y=\”−408\”>F i n i s h</name></l o c a t i o n><l o c a t i o n i d =\” i d 1\” x=\”−520\”

y=\”−96\”><name x=\”−568\” y=\”−128\”>O f f s e t</name><l a b e l k i n d =\” i n v a r i a n t\”

x =\”−568\” y=\”−80\”>//Wait f o r o f f s e t\n” +

” x& l t ;= o f f s e t−1</ l a b e l></l o c a t i o n><l o c a t i o n i d =\” i d 2\” x=\”−520\” y=\”−256\”><name x =\”−560\” y=\”−288\”>S t a r t</name><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 3\”

x =\”128\” y=\”−416\”><name x =\”80\” y=\”−448\”>ReadyDynamic</name><l a b e l k i n d =\” i n v a r i a n t\” x =\”112\” y=\”−400\”>x& l t ;=1</ l a b e l></l o c a t i o n><l o c a t i o n i d =\” i d 4\” x =\”120\” y=\”352\”><name x =\”40\” y=\”336\”>Running3</name><l a b e l k i n d =\” i n v a r i a n t\” x =\”110\” y=\”367\”>x& l t ;=1</ l a b e l></l o c a t i o n><l o c a t i o n i d =\” i d 5\” x =\”200\” y=\”264\”><name x =\”208\” y=\”240\”>Running2</name><l a b e l k i n d =\” i n v a r i a n t\” x =\”208\” y=\”272\”>x& l t ;1</ l a b e l></l o c a t i o n><l o c a t i o n i d =\” i d 6\” x =\”376\” y=\”−256\”><name x =\”384\”

y=\”−248\”>M i s s e d D e a d l i n e</name></l o c a t i o n><l o c a t i o n i d =\” i d 7\” x=\”−320\”

y=\”−96\”><name x=\”−384\” y=\”−96\”>I d l e W a i t</name><l a b e l k i n d =\” i n v a r i a n t\”

x =\”−400\” y=\”−72\”>//W a i t i n g f o r n e x t p e r i o d\n” +

” x& l t ; pti m e</ l a b e l></ l o c a t i o n><l o c a t i o n i d =\” i d 8\” x =\”128\” y=\”160\”><name x =\”48\” y=\”136\”>Running</name></ l o c a t i o n><l o c a t i o n i d =\” i d 9\”

x =\”128\” y=\”−256\”><name x =\”118\”

y=\”−286\”>Ready</name></ l o c a t i o n><l o c a t i o n i d =\” i d 1 0\” x=\”−320\”

y=\”−256\”><name x=\”−352\” y=\”−280\”>I d l e</name><l a b e l k i n d =\” i n v a r i a n t\”

x=\”−428\” y=\”−248\”>// W a i t i n g f o r n e x t p e r i o d\n” +

” x& l t ;= pti m e</ l a b e l></ l o c a t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 8\”/><t a r g e t r e f =\” i d 6\”/><l a b e l k i n d =\”g u a r d\” x =\”344\”

y=\”184\”>d e a d l i n e M i s s e d R u n ( )</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”344\”

y=\”200\”>u p d a t e M i s s e d D e a d l i n e ( )</ l a b e l><n a i l x =\”376\”

y=\”160\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 9\”/><t a r g e t r e f =\” i d 7\”/><l a b e l k i n d =\” g u a r d\” x=\”−176\”

y=\”−248\”>F i r m d e a d l i n e W i l l M i s s ( )</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−176\”

y=\”−232\”>f i r m D e a d l i n e M i s s e s ( )</ l a b e l><n a i l x =\”88\” y=\”−208\”/><n a i l x=\”−250\” y=\”−208\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 0\”/><t a r g e t r e f =\” i d 0\”/><l a b e l k i n d =\” g u a r d\” x=\”−456\”

y=\”−400\”>maxCountReached ( )</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”−432\”

y=\”−384\”>u p d a t e E n d S t a t e ( )</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1\”/><t a r g e t r e f =\” i d 7\”/><l a b e l k i n d =\”g u a r d\” x=\”−496\”

y=\”−152\”>// F i n i s h e d w a i t i n g f o r o f f s e t\n” +

” x==o f f s e t−1</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−496\”

y=\”−120\”>s e t P e r i o d C l o c k ( )</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2\”/><t a r g e t r e f =\” i d 1\”/><l a b e l k i n d =\”g u a r d\” x=\”−624\”

y=\”−240\”>t a s k H a s O f f s e t ( )</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−656\”

y=\”−224\”>i n i t O f f s e t ( ) ” +

”</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2\”/><t a r g e t r e f =\” i d 1 0\”/><l a b e l k i n d =\” g u a r d\” x=\”−488\” y=\”−312\”>! t a s k H a s O f f s e t ( )</ l a b e l><l a b e l

k i n d =\” a s s i g n m e n t\” x=\”−488\” y=\”−296\”>i n i t N o O f f s e t ( ) ” +

”</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 9\”/><t a r g e t r e f =\” i d 3\”/><l a b e l k i n d =\” g u a r d\” x =\”184\” y=\”−384\”>deadl i neN otMi s s edY etO rSO FT ( )</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”184\” y=\”−352\”>s e t W a i t F o r U p d a t e D y n a m i c S c h e d u l i n g ( ) ” +

”</ l a b e l><n a i l x =\”184\” y=\”−344\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 3\”/><t a r g e t r e f =\” i d 9\”/><l a b e l k i n d =\”g u a r d\” x=\”−104\”

y=\”−376\”>//Time u n i t c o m p l e t i o n\n” +

” x==1</l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−104\”

y=\”−344\”>u p d a t e D y n a m i c S c h e d u l i n g ( ) ” +

”</ l a b e l><n a i l x =\”72\” y=\”−344\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 4\”/><t a r g e t r e f =\” i d 8\”/><l a b e l k i n d =\”g u a r d\” x=\”−72\”

y=\”224\”>// C om pl ete one run\n” +

” x==1</l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−72\” y=\”256\”>runOneTimeUnit ( ) ” +

”</ l a b e l><n a i l x =\”40\” y=\”256\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 5\”/><t a r g e t r e f =\” i d 4\”/><l a b e l k i n d =\”g u a r d\” x =\”168\”

y=\”296\”>// C o n t i n u e run\n ” +

” x&g t ;0</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”168\”

y=\”328\”>e n s u r e R u n C o m p l e t i o n ( )</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 8\”/><t a r g e t r e f =\” i d 5\”/><l a b e l k i n d =\”g u a r d\” x =\”176\”

y=\”168\”>ready ForN ex tRun ( )</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”176\”

y=\”184\”>i n i t O n e R u n ( ) ” +

”</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 9\”/><t a r g e t r e f =\” i d 6\”/><l a b e l k i n d =\” g u a r d\” x =\”192\” y=\”−296\”>d e a d l i n e M i s s e d ( )</ l a b e l><l a b e l

k i n d =\” a s s i g n m e n t\” x =\”192\”

y=\”−280\”>u p d a t e M i s s e d D e a d l i n e ( )</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 8\”/><t a r g e t r e f =\” i d 1 0\”/><l a b e l k i n d =\”g u a r d\” x=\”−88\”

y=\”−50\”>t a s k F i n i s h A t P e r i o d E n d ( ) | | \n ” +

” F i r m d e a d l i n e M i s s e d A t P e r i o d ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−88\”

y=\”−24\”>f i n i s h !</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−88\”

y=\”−8\”>f i n i s h A t P e r i o d E n d ( )</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 7\”/><t a r g e t r e f =\” i d 1 0\”/><l a b e l k i n d =\”g u a r d\” x=\”−392\”

y=\”−208\”>x&g t ; pti m e−1</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−384\”

y=\”−192\”>s e t P e n d ( )</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 8\”/><t a r g e t r e f =\” i d 7\”/><l a b e l k i n d =\”g u a r d\” x=\”−312\”

y=\”16\”>t a s k F i n i s h B e f o r e P e r i o d E n d ( ) | | \n” +

” F i r m d e a d l i n e M i s s e d B e f o r e P e r i o d ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x =\”−312\”

y=\”48\”>f i n i s h !</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−312\”

y=\”64\”>f i n i s h B e f o r e P e r i o d E n d ( )</ l a b e l><n a i l x=\”−32\”

y=\”160\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 8\”/><t a r g e t r e f =\” i d 9\”/><l a b e l k i n d =\” g u a r d\” x =\”200\”

y=\”−56\”>tas k H as MoreRunti m e ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x =\”200\”

y=\”−40\”>preem pt ?</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”200\”

y=\”−24\”>s e t P r e e m p t e d ( )</ l a b e l><n a i l x =\”192\” y=\”120\”/><n a i l x =\”192\”

y=\”−208\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 9\”/><t a r g e t r e f =\” i d 8\”/><l a b e l k i n d =\” g u a r d\” x=\”−40\”

y=\”−176\”>deadl i neN otMi s s edO rSO FT ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\”

x=\”−40\” y=\”−160\”>run ?</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 0\”/><t a r g e t r e f =\” i d 9\”/><l a b e l k i n d =\” s e l e c t\” x=\”−296\”

y=\”−344\”>i : i n t [ emin , emax ]</ l a b e l><l a b e l k i n d =\”g u a r d\” x=\”−296\”

y=\”−328\”>x==p t i m e &&amp ;\n r e a d y F o r N e x t P e r i o d ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−296\” y=\”−296\”>r e a d y !</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−296\”

y=\”−280\”>i n i t N e x t P e r i o d ( i )</ l a b e l></ t r a n s i t i o n></t e m p l a t e>” +

”<t e m p l a t e><name>S c h e d u l e r</name>c o n s t i n t s c h n r , i n t [ 0 ,MN] &amp ; f t i d , chan &amp ; s c h e d u l e<d e c l a r a t i o n>i n t [ 0 , N ] i t ; // i t e r a t i o n

v a r i a b l e\n” +

” i n t l c r i ; // v a r i a b l e u s e d t o h o l d t h e c r i t e r i o n o f t h e t a s k c u r r e n t l y c h o s e n\n” +

” i n t [ 0 ,MN] l i ; // v a r i a b l e u s e d t o h o l d g l o b a l i d f o r t a s k s\n” +

” i n t t r a n s I D =0;\n ” +

”\n” +

” b o o l a T a s k I s R e a d y ;\n” +

”\n” +

” v o i d noT as k s Ready ( ) {\n” +

” c u r t i d [ s c h n r−1] = 0;\n” +

”}\n” +

”\n ” +

” v o i d f i n d H i g h e s t P r i o r i t y ( ) {\n” +

” f o r ( i t : i n t [ 0 , N−1 ] ) {\n” +

” l i = l t o g [ s c h n r−1 ] [ i t ] ;\n” +

” i f ( l i ! = 0 ) {\n” +

” i f ( A l l o c a t e d [ l i−1 ] ) {\n” +

” i f ( p r o c e s s o r S c h e d u l i n g [ s c h n r−1] != EDF &&amp ; ( s t a t i c C r i t e r i a [ s c h n r−1 ] [ i t ] & l t ; l c r i ) ) {\n ” +

” c u r t i d [ s c h n r−1]= i t +1;\n ” +

” l c r i = s t a t i c C r i t e r i a [ s c h n r−1 ] [ i t ] ;\n ” +

” }\n” +

” e l s e i f ( p r o c e s s o r S c h e d u l i n g [ s c h n r−1] == EDF &&amp ; ( d y n a m i c C r i t e r i a [ s c h n r−1 ] [ i t ] & l t ; l c r i ) ) {\n ” +

” c u r t i d [ s c h n r−1]= i t +1;\n ” +

” l c r i =d y n a m i c C r i t e r i a [ s c h n r−1 ] [ i t ] ;\n” +

” }\n” +

” }\n ” +

”}\n ” +

”\n ” +

” v o i d tas k s Ready O nPr oc ( ) {\n” +

” a T a s k I s R e a d y = f a l s e ;\n ” +

” f o r ( i t : i n t [ 0 , N−1 ] ) {\n” +

” l i = l t o g [ s c h n r−1 ] [ i t ] ;\n” +

” i f ( l i != 0 ) {\n” +

” i f ( A l l o c a t e d [ l i−1 ] ) {\n” +

” a T a s k I s R e a d y = t r u e ;\n” +

” i f ( p r o c e s s o r S c h e d u l i n g [ s c h n r−1] != EDF) {\n ” +

” l c r i = s t a t i c C r i t e r i a [ s c h n r−1 ] [ i t ] ;\n” +

” }\n ” +

” e l s e {\n” +

” l c r i = d y n a m i c C r i t e r i a [ s c h n r−1 ] [ i t ] ;\n” +

” }\n ” +

” c u r t i d [ s c h n r−1] = i t +1;\n ” +

” r e t u r n ;\n” +

” }\n” +

” }\n ” +

”}\n ” +

”\n ” +

”</ d e c l a r a t i o n><l o c a t i o n i d =\” i d 1 1\” x=\”−224\” y=\”−160\”></ l o c a t i o n><l o c a t i o n i d =\” i d 1 2\” x =\”24\” y=\”−160\”><com m i tted /></ l o c a t i o n><i n i t

r e f =\” i d 1 1\”/><t r a n s i t i o n><s o u r c e r e f =\” i d 1 2\”/><t a r g e t r e f =\” i d 1 1\”/><l a b e l k i n d =\”g u a r d\” x=\”−160\” y=\”−96\”>aT as k I s Ready</ l a b e l><l a b e l

k i n d =\” s y n c h r o n i s a t i o n\” x=\”−160\” y=\”−64\”>// S c h e d u l e r f i n i s h i n g\n” +

” s c h e d u l e !</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−160\”

y=\”−80\”>f i n d H i g h e s t P r i o r i t y ( )</ l a b e l><n a i l x=\”−8\” y=\”−96\”/><n a i l x =\”−192\” y=\”−96\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 2\”/><t a r g e t

r e f =\” i d 1 1\”/><l a b e l k i n d =\”g u a r d\” x=\”−160\”

y =\”−296\”>!aT as k I s Ready</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−160\”

y=\”−264\”>// S c h e d u l e r f i n i s h i n g\n ” +

” s c h e d u l e !</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−160\”

y=\”−280\”>noT as k s Ready ( )</ l a b e l><n a i l x=\”−8\” y=\”−224\”/><n a i l x=\”−192\”

y=\”−224\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 1\”/><t a r g e t

r e f =\” i d 1 2\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−184\” y=\”−216\”>// S c h e d u l e r s t a r t i n g\n” +

” s c h e d u l e ?</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−184\”

y=\”−184\”>tas k s Ready O nPro c ( )</ l a b e l></ t r a n s i t i o n></t e m p l a t e>” +

”<t e m p l a t e><name>C o n t r o l</name>c o n s t i n t s c h n r , i n t [ 0 ,MN] &amp ; f t i d , i n t [ 0 , N ] &amp ; t i d , i n t [ 0 ,MN] &amp ; g t i d , chan &amp ; s y n c h r o n i z e , chan

&amp ; s c h e d u l e , chan &amp ; a l l o c a t e , chan &amp ; r e a d y , chan &amp ; f i n i s h , chan

&amp ; run , chan &amp ; preem pt<d e c l a r a t i o n>i n t [−1 ,MN] t r i g I D = −1;\n ” +

” i n t l t = 0 ;\n ” +

”\n ” +

” v o i d t r i g g e r s ( ) {\n” +

” t r i g I D = −1;\n” +

” f o r ( i t : i n t [ 0 ,MN−1 ] ) {\n” +

” l t = l t o g [ s c h n r−1 ] [ t i d−1 ] ;\n” +

” i f ( l t != 0 ) {\n” +

” i f ( o r i g d e p [ i t ] [ l t−1] &&amp ; t a s k R e a d y F o r T r i g g e r i n g [ i t ] ) {\n” +

” t r i g I D = i t ;\n” +

” }\n” +

” }\n ” +

”}\n ” +

”\n ” +

” b o o l t r i g g e r T a s k ( ) {\n” +

” r e t u r n ( t r i g I D&g t ; (−1 ) ) ;\n” +

”}\n ” +

”\n ” +

” b o o l a l l S i g n a l s R e c e i v e d ( ) {\n” +

” r e t u r n ( ! pendMN ( p e n d i n g ) &&amp ; \n” +

” ! l o c k e d ( h f i n ) &&amp ; \n” +

” ! pendMN ( h e d f ) ) ;\n” +

”}\n ” +

”\n” +

” v o i d s t o p P r o c e s s o r ( ) {\n ” +

” f t i d =g t i d ;\n ” +

” r u n n i n g [ s c h n r−1]= f a l s e ;\n ” +

”}\n” +

”\n” +

” v o i d l o c k P r o c e s s o r ( ) {\n ” +

” c o n t r o l l e r L o c k [ s c h n r−1]= t r u e ;\n” +

” p r o c e s s i n g [ s c h n r−1] = t r u e ;\n” +

”}\n” +

”\n” +

” v o i d u n l o c k P r o c e s s i n g ( ) {\n ” +

” p r o c e s s i n g [ s c h n r−1]= f a l s e ;\n” +

”}\n” +

”\n” +

” v o i d u n l o c k C o n t r o l l e r L o c k ( ) {\n” +

” c o n t r o l l e r L o c k [ s c h n r−1]= f a l s e ;\n ” +

”}\n” +

”\n” +

” v o i d s e t R e a d y T a s k I d ( ) {\n ” +

” Ready [ s c h n r−1 ] [ t i d−1]= t r u e ;\n” +

” f t i d =0;\n” +

”}\n” +

”\n” +

” b o o l n o R e s c h e d u l e ( ) {\n” +

” r e t u r n ( ! h r &&amp ; ! l o c k e d ( p r o c e s s i n g ) ) ;\n” +

”}\n” +

”\n” +

” v o i d s e t R e a d y T a s k I d 2 ( ) {\n ” +

” Ready [ s c h n r−1 ] [ t i d−1]= t r u e ;\n” +

”}\n” +

”\n” +

” b o o l p r o c e s s o r N o t R u n n i n g ( ) {\n” +

” r e t u r n ( ! r u n n i n g [ s c h n r−1] &&amp ; c u r t i d [ s c h n r−1] != 0 ) ;\n” +

”}\n” +

”\n” +

” v o i d r u n P r o c e s s o r ( ) {\n” +

” r u n n i n g [ s c h n r−1] = t r u e ;\n” +

”}\n” +

”\n” +

” v o i d s e t R u n n i n g T a s k I d ( ) {\n ” +

” t i d=c u r t i d [ s c h n r−1 ] ;\n ” +

” l t i d [ s c h n r−1] = c u r t i d [ s c h n r−1 ] ;\n ” +

”}\n” +

”\n” +

” b o o l n o S c h e d u l i n g C h a n g e ( ) {\n” +

” r e t u r n ( ( l t i d [ s c h n r−1]== c u r t i d [ s c h n r−1] &&amp ; r u n n i n g [ s c h n r−1 ] ) | | c u r t i d [ s c h n r−1]==0) ;\n” +

”}\n” +

”\n” +

” b o o l r u n n i n g T a s k H a s L o w e r P r i o r i t y ( ) {\n” +

” r e t u r n ( l t i d [ s c h n r−1]!= c u r t i d [ s c h n r−1] &&amp ; r u n n i n g [ s c h n r−1 ] ) ;\n” +

”}\n” +

”\n” +

” v o i d r e s e r v e ( i n t t a s k ){\n ” +

” f o r ( i t : i n t [ 0 , R−1 ] ){\n” +

” i f ( N e e d e d R e s o u r c e s [ s c h n r−1 ] [ t a s k−1 ] [ i t ] )\n ” +

” U s e d R e s o u r c e s [ s c h n r−1 ] [ i t ]= t a s k ;\n” +

” }\n ” +

”}\n” +

”\n” +

” v o i d r e l e a s e ( i n t t a s k ){\n ” +

” f o r ( i t : i n t [ 0 , R−1 ] ){\n” +

” i f ( N e e d e d R e s o u r c e s [ s c h n r−1 ] [ t a s k−1 ] [ i t ] )\n ” +

” U s e d R e s o u r c e s [ s c h n r−1 ] [ i t ]= f a l s e ;\n” +

” }\n ” +

”}\n” +

”</ d e c l a r a t i o n><l o c a t i o n i d =\” i d 1 3\” x=\”−416\” y=\”−304\”

c o l o r =\”# f f f f f f\”><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 1 4\” x =\”−512\”

y=\”−304\” c o l o r =\”# f f f f f f\”><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 1 5\”

x=\”−32\” y =\”0\” c o l o r =\”# f f f f f f\”><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 1 6\” x =\”160\” y =\”0\”

c o l o r =\”# f f f f f f\”><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 1 7\” x =\”−128\”

y=\”−128\”><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 1 8\” x=\”−320\”

y=\”0\”><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 1 9\” x =\”−320\”

y=\”128\”></ l o c a t i o n><l o c a t i o n i d =\” i d 2 0\” x =\”−128\”

y=\”0\”><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 2 1\” x =\”−320\”

y=\”−128\”><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 2 2\” x=\”−128\”

y=\”−256\”><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 2 3\” x=\”−448\” y=\”−256\”

c o l o r =\”# f f f f f f\”></ l o c a t i o n><l o c a t i o n i d =\” i d 2 4\” x=\”−704\”

y=\”−256\” c o l o r =\”# f f f f f f\”></ l o c a t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 3\”/><t a r g e t r e f =\” i d 2 3\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−424\”

y=\”−288\”>t r i g g e r [ t r i g I D ] !</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 4\”/><t a r g e t r e f =\” i d 1 3\”/><l a b e l k i n d =\”g u a r d\” x=\”−496\”

y=\”−328\”>t r i g g e r T a s k ( )</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 4\”/><t a r g e t r e f =\” i d 2 3\”/><l a b e l k i n d =\”g u a r d\” x=\”−552\”

y=\”−264\”>! t r i g g e r T a s k ( )</ l a b e l><n a i l x=\”−496\”

y=\”−256\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 9\”/><t a r g e t r e f =\” i d 1 5\”/><l a b e l k i n d =\”g u a r d\” x=\”−280\”

y =\”104\”>n o R e s c h e d u l e ( )</ l a b e l><n a i l x=\”−256\” y=\”128\”/><n a i l x=\”−32\”

y=\”128\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 9\”/><t a r g e t r e f =\” i d 2 1\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−432\”

y=\”32\”>r e s c h e d u l e ?</ l a b e l><n a i l x=\”−352\” y=\”128\”/><n a i l x=\”−352\”

y=\”−64\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 6\”/><t a r g e t r e f =\” i d 2 4\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x =\”128\”

y=\”−328\”>run !</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”64\”

y=\”−312\”>r u n P r o c e s s o r ( ) ,\n” +

” r e s e r v e ( t i d ) ,\n ” +

” u n l o c k C o n t r o l l e r L o c k ( )</ l a b e l><n a i l x =\”160\” y=\”−384\”/><n a i l x=\”−736\”

y=\”−384\”/><n a i l x=\”−736\” y=\”−256\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 5\”/><t a r g e t r e f =\” i d 2 4\”/><l a b e l k i n d =\”g u a r d\” x=\”−32\”

y=\”−208\”>n o S c h e d u l i n g C h a n g e ( )</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−32\”

y=\”−192\”>u n l o c k C o n t r o l l e r L o c k ( )</ l a b e l><n a i l x=\”−32\” y=\”−352\”/><n a i l x =\”−704\” y=\”−352\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 5\”/><t a r g e t

r e f =\” i d 1 6\”/><l a b e l k i n d =\”g u a r d\” x =\”8\”

y=\”−72\”>p r o c e s s o r N o t R u n n i n g ( )</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”8\”

y=\”−56\”>s e t R u n n i n g T a s k I d ( )</ l a b e l><n a i l x =\”0\” y=\”−32\”/><n a i l x =\”128\” y=\”−32\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 7\”/><t a r g e t

r e f =\” i d 1 8\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−264\”

y=\”−80\”>a l l o c a t e ?</ l a b e l><n a i l x=\”−128\” y=\”−64\”/><n a i l x =\”−320\”

y=\”−64\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 1\”/><t a r g e t r e f =\” i d 1 7\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−264\”

y=\”−144\”>a l l o c a t e !</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 5\”/><t a r g e t r e f =\” i d 1 6\”/><l a b e l k i n d =\”g u a r d\” x=\”−16\”

y=\”32\”>r u n n i n g T a s k H a s L o w e r P r i o r i t y ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\”

x=\”−16\” y=\”48\”>preem pt !</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−16\”

y=\”64\”>s e t R u n n i n g T a s k I d ( )</ l a b e l><n a i l x =\”0\” y=\”32\”/><n a i l x =\”128\”

y=\”32\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 3\”/><t a r g e t

r e f =\” i d 2 3\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−504\” y=\”−208\”>//Wait f o r a l l Ready s i g n a l s\n” +

” r e a d y ?</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−504\”

y=\”−176\”>s e t R e a d y T a s k I d 2 ( )</ l a b e l><n a i l x=\”−400\” y=\”−208\”/><n a i l x =\”−448\” y=\”−208\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 4\”/><t a r g e t

r e f =\” i d 2 1\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−632\”

y=\”−128\”>r e s c h e d u l e ?</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−632\”

y=\”−112\”>l o c k P r o c e s s o r ( )</ l a b e l><n a i l x =\”−704\” y=\”−128\”/><n a i l x=\”−352\”

y=\”−128\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 0\”/><t a r g e t

r e f =\” i d 1 9\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−272\” y=\”32\”>//Wait f o r s c h e d u l e r\n” +

” s c h e d u l e ?</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−272\”

y=\”64\”>u n l o c k P r o c e s s i n g ( )</ l a b e l><n a i l x =\”−128\” y=\”64\”/><n a i l x=\”−320\”

y=\”64\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 1 8\”/><t a r g e t

r e f =\” i d 2 0\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−264\” y=\”−32\”>// A c t i v a t e s c h e d u l e r\n” +

” s c h e d u l e !</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 2\”/><t a r g e t

r e f =\” i d 2 1\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−280\” y=\”−224\”>//Wait f o r s y n c h r o n i z e r\n ” +

” s y n c h r o n i z e ?</ l a b e l><n a i l x=\”−128\” y=\”−192\”/><n a i l x=\”−320\”

y=\”−192\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 3\”/><t a r g e t r e f =\” i d 2 2\”/><l a b e l k i n d =\”g u a r d\” x=\”−288\”

y=\”−304\”>a l l S i g n a l s R e c e i v e d ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\”

x =\”−288\” y=\”−288\”>// a c t i v a t e s y n c h r o n i z e r\n ” +

” s y n c h r o n i z e !</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 4\”/><t a r g e t r e f =\” i d 2 3\”/><l a b e l k i n d =\”g u a r d\” x=\”−696\”

y =\”−240\”>! h f i n [ s c h n r−1]</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−696\”

y=\”−224\”>// Get f i r s t r e a d y s i g n a l\n ” +

” r e a d y ?</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−696\”

y=\”−192\”>s e t R e a d y T a s k I d ( ) ,\n” +

” l o c k P r o c e s s o r ( )</ l a b e l><n a i l x =\”−672\” y=\”−224\”/><n a i l x=\”−480\”

y=\”−224\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 4\”/><t a r g e t

r e f =\” i d 1 4\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−640\” y=\”−336\”>//Get one f i n i s h s i g n a l\n ” +

” f i n i s h ?</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−640\”

y=\”−304\”>s t o p P r o c e s s o r ( ) ,\n” +

” l o c k P r o c e s s o r ( ) ,\n” +

” r e l e a s e ( t i d ) ,\n ” +

” t r i g g e r s ( )</ l a b e l><n a i l x=\”−672\” y=\”−304\”/></ t r a n s i t i o n></t e m p l a t e>” +

”<t e m p l a t e><name>S y n c h r o n i z e r</name>c o n s t i n t s c h n r , i n t [ 0 ,MN] &amp ; f t i d , chan &amp ; s y n c h r o n i z e<d e c l a r a t i o n>i n t [ 0 ,MN] i ; // i t e r a t i o n v a r i a b l e\n” +

” // i n t [ 0 ,M∗N ] i t ; // i t e r a t i o n v a r i a b l e\n” +

” i n t [ 0 ,MN] l i ; // v a r i a b l e u s e d t o h o l d g l o b a l i d f o r t a s k s\n” +

” b o o l depCh ; // f l a g u s e d i f a d e p e n d e n c y h a s b e e n c h a n g e d\n” +

”\n ” +

” b o o l aD ependency H as C hanged ( ) {\n” +

” r e t u r n ( depCh ) ;\n” +

”}\n ” +

”\n ” +

” b o o l a T a s k H a s F i n i s h e d ( ) {\n” +

” r e t u r n ( f t i d ! = 0 ) ;\n” +

”}\n ” +

”\n ” +

” v o i d s e t G l o b a l R e s c h e d u l e ( ) {\n” +

” depCh= f a l s e ;\n ” +

” h r = t r u e ;\n ” +

”}\n” +

”\n” +

” v o i d s y n c F i n i s h ( ) {\n” +

” i f ( f t i d &g t ; 0 ) {\n” +

” opdDep ( f t i d−1) ;\n” +

” S y n c h r o n i z e d [ f t i d−1]= f a l s e ;\n” +

” f o r ( i : i n t [ 0 ,MN−1 ] ) {\n” +

” i f ( WaitDep [ i ] &&amp ; ! t a s k H a s D e p e n d e n c y ( i ) ) {\n” +

” S y n c h r o n i z e d [ i ]= t r u e ;\n” +

” WaitDep [ i ]= f a l s e ; \n” +

” depCh=t r u e ;\n” +

” }\n” +

” }\n ” +

”}\n” +

”\n” +

” v o i d s y ncReady ( ) {\n” +

” f o r ( i : i n t [ 0 , N−1 ] ) {\n ” +

” i f ( Ready [ s c h n r−1 ] [ i ] ) {\n” +

” l i =l t o g [ s c h n r−1 ] [ i ] ;\n” +

” Ready [ s c h n r−1 ] [ i ]= f a l s e ;\n” +

” i f ( t a s k H a s D e p e n d e n c y ( l i−1) ) {\n” +

” WaitDep [ l i−1]= t r u e ;\n” +

” }\n” +

” e l s e {\n ” +

” S y n c h r o n i z e d [ l i−1]= t r u e ;\n ” +

” }\n” +

” }\n ” +

”}</ d e c l a r a t i o n><l o c a t i o n i d =\” i d 2 5\” x =\”32\”

y=\”−192\”><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 2 6\” x=\”−224\”

y=\”−192\”><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 2 7\” x=\”−224\”

y=\”−40\”></l o c a t i o n><t r a n s i t i o n><s o u r c e

r e f =\” i d 2 6\”/><t a r g e t r e f =\” i d 2 7\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−384\”

y=\”−120\”>// S y n c h r o n i z e r f i n i s h i n g\n ” +

” s y n c h r o n i z e !</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 5\”/><t a r g e t r e f =\” i d 2 7\”/><l a b e l k i n d =\”g u a r d\” x=\”−200\”

y=\”−152\”>!aD ependency H as C hanged ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\”

x=\”−200\” y=\”−136\”>// S y n c h r o n i z e r f i n i s h i n g\n ” +

” s y n c h r o n i z e !</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 5\”/><t a r g e t r e f =\” i d 2 6\”/><l a b e l k i n d =\”g u a r d\” x=\”−160\”

y=\”−248\”>aD ependency H as C hanged ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\”

x=\”−160\” y=\”−232\”>a c t i v a t e R e s c h e d u l e !</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\”

x=\”−160\”

y=\”−216\”>s e t G l o b a l R e s c h e d u l e ( )</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 7\”/><t a r g e t r e f =\” i d 2 5\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x =\”40\”

y=\”−136\”>// S y n c h r o n i z e r s t a r t i n g\n ” +

” s y n c h r o n i z e ?</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”40\”

y=\”−104\”>s y n c F i n i s h ( ) ,\n ” +

” s y ncReady ( )</ l a b e l><n a i l x =\”32\” y=\”−40\”/></ t r a n s i t i o n></t e m p l a t e>” +

”<t e m p l a t e><name>A l l o c a t o r</name>c o n s t i n t s c h n r , i n t a l l o c a t i o n P r o t o c o l , chan &amp ; a l l o c a t e<d e c l a r a t i o n>i n t g t i ;\n” +

” b o o l r e s o u r c e C o n f l i c t , s e n d R e s c h e d ;\n ” +

”\n” +

” v o i d r e m o v e R e s c h e d F l a g ( ) {\n” +

” s e n d R e s c h e d= f a l s e ;\n” +

”}\n” +

”\n” +

” v o i d c h e c k R e s o u r c e s ( ){\n ” +

” f o r ( i t : i n t [ 0 , N−1 ] ){\n” +

” g t i = l t o g [ s c h n r−1 ] [ i t ] ;\n” +

” i f ( g t i ){\n ” +

” i f ( S y n c h r o n i z e d [ g t i−1 ] ){\n” +

” f o r ( r : i n t [ 0 , R−1 ] ){\n” +

” i f ( U s e d R e s o u r c e s [ s c h n r−1 ] [ r ] &&amp ; a l l o c a t i o n P r o t o c o l==NPCS) {\n” +

” r e s o u r c e C o n f l i c t = t r u e ;\n” +

” }\n” +

” e l s e i f ( N e e d e d R e s o u r c e s [ s c h n r−1 ] [ i t ] [ r ] &&amp ; U s e d R e s o u r c e s [ s c h n r−1 ] [ r ] ){\n” +

” r e s o u r c e C o n f l i c t=t r u e ;\n ” +

” i f ( a l l o c a t i o n P r o t o c o l==PRI INH &&amp ;

( s t a t i c C r i t e r i a [ s c h n r−1 ] [ ( U s e d R e s o u r c e s [ s c h n r−1 ] [ r ] )−1] &g t ; s t a t i c C r i t e r i a [ s c h n r−1 ] [ i t ] ) ){\n” +

” s t a t i c C r i t e r i a [ s c h n r−1 ] [ ( U s e d R e s o u r c e s [ s c h n r−1 ] [ r ] )−1] = s t a t i c C r i t e r i a [ s c h n r−1 ] [ i t ] ;\n” +

” h r=t r u e ;\n ” +

” s e n d R e s c h e d=t r u e ;\n” +

” }\n ” +

” i f ( a l l o c a t i o n P r o t o c o l==PRI INH &&amp ;

( d y n a m i c C r i t e r i a [ s c h n r−1 ] [ ( U s e d R e s o u r c e s [ s c h n r−1 ] [ r ] )−1] &g t ; d y n a m i c C r i t e r i a [ s c h n r−1 ] [ i t ] ) ){\n” +

” d y n a m i c C r i t e r i a [ s c h n r−1 ] [ ( U s e d R e s o u r c e s [ s c h n r−1 ] [ r ] )−1] = d y n a m i c C r i t e r i a [ s c h n r−1 ] [ i t ] ;\n” +

” h r=t r u e ;\n ” +

” s e n d R e s c h e d=t r u e ;\n” +

” }\n ” +

” }\n” +

” i f ( ! r e s o u r c e C o n f l i c t )\n” +

” A l l o c a t e d [ g t i−1]= t r u e ;\n ” +

” r e s o u r c e C o n f l i c t= f a l s e ;\n ” +

” }\n” +

” e l s e{\n ” +

” A l l o c a t e d [ g t i−1]= f a l s e ;\n ” +

” }\n” +

” }\n ” +

”}\n ” +

”</ d e c l a r a t i o n><l o c a t i o n i d =\” i d 2 8\” x=\”−192\”

y=\”−160\”><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 2 9\” x=\”−352\”

y=\”−160\”></ l o c a t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 8\”/><t a r g e t r e f =\” i d 2 8\”/><l a b e l k i n d =\”g u a r d\” x=\”−120\”

y=\”−184\”>s e n d R e s c h e d</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−120\”

y=\”−168\”>a c t i v a t e R e s c h e d u l e !</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−120\”

y=\”−152\”>r e m o v e R e s c h e d F l a g ( )</ l a b e l><n a i l x=\”−128\” y=\”−192\”/><n a i l x =\”−128\” y=\”−128\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 8\”/><t a r g e t

r e f =\” i d 2 9\”/><l a b e l k i n d =\”g u a r d\” x=\”−320\”

y =\”−128\”>!s e n d R e s c h e d</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−320\”

y=\”−112\”>a l l o c a t e !</ l a b e l><n a i l x=\”−224\” y=\”−128\”/><n a i l x=\”−320\”

y=\”−128\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 2 9\”/><t a r g e t r e f =\” i d 2 8\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−312\”

y=\”−232\”>a l l o c a t e ?</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−312\”

y=\”−216\”>c h e c k R e s o u r c e s ( )</ l a b e l><n a i l x =\”−320\” y=\”−192\”/><n a i l x =\”−224\” y=\”−192\”/></ t r a n s i t i o n></t e m p l a t e>” +

”<t e m p l a t e><name>R e s c h e d u l e r</name><d e c l a r a t i o n>v o i d u n l o c k R e s c h e d u l e ( ) {\n ” +

” h r = f a l s e ;\n” +

”}</ d e c l a r a t i o n><l o c a t i o n i d =\” i d 3 0\” x =\”32\”

y=\”−96\”></ l o c a t i o n><l o c a t i o n i d =\” i d 3 1\” x=\”−192\”

y=\”−96\”></l o c a t i o n><t r a n s i t i o n><s o u r c e

r e f =\” i d 3 0\”/><t a r g e t r e f =\” i d 3 0\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x =\”104\”

y=\”−112\”>a c t i v a t e R e s c h e d u l e ?</ l a b e l><n a i l x =\”96\” y=\”−128\”/><n a i l x =\”96\”

y=\”−64\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 3 0\”/><t a r g e t r e f =\” i d 3 1\”/><l a b e l k i n d =\”g u a r d\” x=\”−136\”

y=\”−64\”>n o t S i g n a l s P e n d i n g ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−136\”

y=\”−48\”>r e s c h e d u l e !</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−136\”

y=\”−32\”>u n l o c k R e s c h e d u l e ( )</ l a b e l><n a i l x =\”0\” y=\”−64\”/><n a i l x=\”−160\”

y=\”−64\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 3 1\”/><t a r g e t r e f =\” i d 3 0\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−144\”

y=\”−152\”>a c t i v a t e R e s c h e d u l e ?</ l a b e l><n a i l x=\”−160\” y=\”−128\”/><n a i l x =\”0\” y=\”−128\”/></ t r a n s i t i o n></t e m p l a t e>” +

”<t e m p l a t e><name>T r i g g e r e d</name>c o n s t i n t s c h n r , c o n s t i n t g t a s k n r , c o n s t i n t t a s k n r , c o n s t i n t emin , c o n s t i n t emax , c o n s t i n t dead , i n t p r i o r , i n t [ 0 , N ] &amp ; t i d , i n t [ 0 ,MN] &amp ; g t i d , chan &amp ; t r i g g e r , chan &amp ; r e a d y , chan

&amp ; run , chan &amp ; preem pt , chan &amp ; f i n i s h , c o n s t i n t [ 0 , 2 ] sd<d e c l a r a t i o n>c l o c k x ;\n ” +

” i n t c o u n t e r = 0 ;\n” +

”\n ” +

” i n t cp ;\n” +

” i n t c r ;\n” +

”\n ” +

” i n t i ;\n” +

”\n ” +

” v o i d s e t R e a d y F o r T r i g g e r i n g ( ) {\n” +

” t a s k R e a d y F o r T r i g g e r i n g [ g t a s k n r−1] = t r u e ;\n ” +

” e n d S t a t e [ g t a s k n r−1] = t r u e ;\n” +

” u p d a t e C o s t ( g t a s k n r , s c h n r , STATIC) ;\n” +

” r e s e t C o s t ( g t a s k n r , s c h n r , IDLE ) ;\n” +

” p r e e m p t e d O r I d l e [ g t a s k n r−1] = f a l s e ;\n” +

”}\n ” +

”\n ” +

” v o i d f i n i s h e d ( ) {\n” +

” i f ( ! ( s d==FIRM &&amp ; cp==dead &&amp ; c r &g t ; 0 ) ) {\n ” +

” t i d=t a s k n r ;\n” +

” g t i d=g t a s k n r ;\n” +

” }\n ” +

” e n d S t a t e [ g t a s k n r−1]= t r u e ;\n” +

” h f i n [ s c h n r−1] = f a l s e ;\n” +

” u p d a t e C o s t ( g t a s k n r , s c h n r , IDLE ) ;\n” +

” p r e e m p t e d O r I d l e [ g t a s k n r−1] = t r u e ;\n” +

”}\n ” +

”\n ” +

” v o i d a s s i g n E n o u g h R u n t i m e ( ) {\n” +

” cp=dead−c r ;\n ” +

” x =0;\n” +

”}\n ” +

”\n ” +

” v o i d runOneTimeUnit ( ) {\n ” +

” h t [ s c h n r−1]= f a l s e ;\n ” +

” l i n [ s c h n r−1]= f a l s e ; \n ” +

”\n ” +

” c r−−; \n” +

” cp ++;\n” +

” d y n a m i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1]−−;\n” +

” nowrun [ s c h n r−1]= f a l s e ;\n ” +

” r e s e t C o s t ( g t a s k n r , s c h n r , RUNNING) ;\n” +

” i f ( c r ==0 | | ( s d == FIRM &&amp ; cp==dead ) ) {\n” +

” h f i n [ s c h n r−1]= t r u e ;\n ” +

” }\n ” +

”}\n” +

”\n” +

” b o o l tas k H as MoreRunti m e ( ) {\n” +

” r e t u r n ( c r&g t ; 0 ) ;\n” +

”}\n” +

”\n” +

” b o o l d e a d l i n e M i s s e d ( ) {\n ” +

” r e t u r n ( cp==dead &&amp ; s d == HARD &&amp ; t i d != t a s k n r ) ;\n” +

”}\n” +

”\n” +

” b o o l d e a d l i n e M i s s e d R u n ( ) {\n” +

” r e t u r n ( cp==dead &&amp ; s d == HARD &&amp ; c r &g t ; 0 ) ;\n ” +

”}\n” +

”\n” +

” b o o l deadl i neN otMi s s edY etO rSO FT ( ) {\n ” +

” r e t u r n ( ( ( cp& l t ; dead &&amp ; s d == HARD) \n” +

” | | ( s d == SOFT) \n” +

” | | ( cp& l t ; dead−1 &&amp ; s d==FIRM) )\n” +

” &&amp ; ! l o c k e d ( c o n t r o l l e r L o c k )\n ” +

” &&amp ; ! l o c k e d ( h f i n )\n ” +

” &&amp ; ! l o c k e d ( h t ) ) ;\n ” +

”}\n” +

”\n” +

” b o o l deadl i neN otMi s s edO rSO FT ( ) {\n ” +

” r e t u r n ( ( ( cp& l t ;= dead &&amp ; s d == HARD) \n” +

” | | ( s d == SOFT) \n” +

” | | ( cp& l t ;= dead−1 &&amp ; s d==FIRM) )\n” +

” &&amp ; t i d == t a s k n r ) ;\n” +

”}\n” +

”\n” +

” b o o l F i r m d e a d l i n e W i l l M i s s ( ) {\n” +

” r e t u r n ( s d==FIRM\n” +

” &&amp ; cp == ( dead−1)\n ” +

” &&amp ; t i d != t a s k n r ) ;\n” +

”}\n” +

”\n” +

” b o o l F i r m d e a d l i n e M i s s e d ( ) {\n” +

” r e t u r n ( s d==FIRM &&amp ;\n” +

” cp==dead &&amp ;\n” +

” c r &g t ; 0 ) ;\n” +

”}\n” +

”\n” +

” v o i d s e t M i s s e d D e a d l i n e ( ) {\n” +

” m i s s e d D e a d l i n e =t r u e ;\n ” +

”}\n” +

”\n” +

” v o i d i n i t O n e R u n ( ) {\n” +

” x =0;\n” +

” l i n [ s c h n r−1]= t r u e ;\n” +

” nowrun [ s c h n r−1]= t r u e ;\n ” +

” p r e e m p t e d O r I d l e [ g t a s k n r−1] = f a l s e ;\n” +

” u p d a t e C o s t ( g t a s k n r , s c h n r , RUNNING) ;\n” +

”}\n” +

”\n” +

” v o i d s e t P r e e m p t e d ( ) {\n” +

” p r e e m p t e d = t r u e ;\n” +

” p r e e m p t e d O r I d l e [ g t a s k n r−1] = t r u e ;\n”+

” x =0;\n” +

”}\n” +

”\n” +

” v o i d e n s u r e R u n C o m p l e t i o n ( ) {\n” +

” h t [ s c h n r−1]= t r u e ;\n” +

”}\n” +

”\n” +

” b o o l f i n i s h S i g n a l s P e n d i n g ( ) {\n” +

” r e t u r n ( nowrun [ s c h n r−1] \n” +

” | | l o c k e d ( h f i n )\n” +

” | | pendMN ( h e d f ) ) ;\n” +

”}\n” +

”\n” +

” v o i d i n i t N e x t P e r i o d ( i n t i ) {\n” +

” cp =0;\n” +

” t i d=t a s k n r ;\n ” +

” g t i d = g t a s k n r ;\n” +

” p e n d i n g [ g t a s k n r−1]= f a l s e ;\n” +

” e n d S t a t e [ g t a s k n r−1] = f a l s e ;\n” +

” d y n a m i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1]=dead ;\n ” +

” s e t O r i g D e p ( g t a s k n r−1) ;\n ” +

” c r=i ;\n” +

” x =0;\n” +

”} \n ” +

”\n ” +

” v o i d s e t W a i t F o r U p d a t e D y n a m i c S c h e d u l i n g ( ) {\n ” +

” h e d f [ g t a s k n r−1]= t r u e ;\n” +

” u p d a t e C o s t ( g t a s k n r , s c h n r , READY) ;\n” +

”}\n ” +

”\n ” +

” v o i d u p d a t e D y n a m i c S c h e d u l i n g ( ) {\n ” +

” d y n a m i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1]−−;\n” +

” x =0;\n” +

” cp++;\n” +

” h e d f [ g t a s k n r−1]= f a l s e ;\n” +

” r e s e t C o s t ( g t a s k n r , s c h n r , READY) ;\n” +

”}\n ” +

”\n ” +

” v o i d i n i t T a s k ( ) {\n” +

” p e n d i n g [ g t a s k n r−1]= t r u e ;\n” +

” i f ( p r o c e s s o r S c h e d u l i n g [ s c h n r−1] == FP) {\n ” +

” s t a t i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1]= p r i o r ; \n” +

” }\n ” +

” e l s e {\n” +

” s t a t i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1]=dead ; \n” +

” }\n ” +

” t a s k R e a d y F o r T r i g g e r i n g [ g t a s k n r−1] = f a l s e ;\n” +

”}\n ” +

”\n ” +

” b o o l t a s k H a s F i n i s h e d ( ) {\n” +

” r e t u r n ( c r ==0\n” +

” &&amp ; ! l o c k e d ( h t )\n ” +

” &&amp ; ! pendMN ( h e d f ) ) ;\n” +

”}\n ” +

”\n ” +

” b o o l ready ForN ex tRun ( ) {\n” +

” r e t u r n ( c r&g t ; 0 \n” +

” &&amp ; ! pendMN ( p e n d i n g )\n” +

” &&amp ; ! l o c k e d ( h t )\n ” +

” &&amp ; ! l o c k e d ( h f i n )\n” +

” &&amp ; ! l o c k e d ( c o n t r o l l e r L o c k )\n” +

” &&amp ; ! h r\n” +

” &&amp ; ( ( s d == SOFT) \n” +

” | | ( cp & l t ; dead &&amp ; s d == FIRM) \n” +

” | | ( cp & l t ;= dead &&amp ; s d == HARD) ) ) ; \n” +

” // &&amp ; ! pendMN ( h e d f ) ) ;\n” +

”}\n ” +

”\n ” +

” v o i d f i r m D e a d l i n e M i s s e s ( ) {\n” +

” d y n a m i c C r i t e r i a [ s c h n r−1 ] [ t a s k n r−1] = 0;\n” +

” Ready [ s c h n r−1 ] [ t a s k n r−1]= f a l s e ;\n ” +

” S y n c h r o n i z e d [ g t a s k n r−1]= f a l s e ;\n ” +

” A l l o c a t e d [ g t a s k n r−1]= f a l s e ;\n” +

” u p d a t e C o s t ( g t a s k n r , s c h n r , IDLE ) ;\n” +

” p r e e m p t e d O r I d l e [ g t a s k n r−1] = t r u e ;\n” +

” x = cp ;\n” +

”}\n ” +

”\n ” +

”</ d e c l a r a t i o n><l o c a t i o n i d =\” i d 3 2\” x=\”−424\” y=\”−256\”><name x=\”−480\”

y=\”−288\”>I d l e W a i t</name></l o c a t i o n><l o c a t i o n i d =\” i d 3 3\” x=\”−296\”

y=\”−256\”></ l o c a t i o n><l o c a t i o n i d =\” i d 3 4\” x=\”−424\”

y=\”−128\”><name x=\”−456\”

y=\”−120\”>S t a r t</name><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 3 5\” x=\”−24\”

y=\”−416\”><name x=\”−72\” y=\”−448\”>ReadyDynamic</name><l a b e l

k i n d =\” i n v a r i a n t\” x=\”−40\” y=\”−400\”>x& l t ;=1</ l a b e l></l o c a t i o n><l o c a t i o n i d =\” i d 3 6\” x=\”−32\” y=\”352\”><name x=\”−112\”

y =\”336\”>Running3</name><l a b e l k i n d =\” i n v a r i a n t\” x=\”−42\”

y =\”367\”>x& l t ;=1</ l a b e l></l o c a t i o n><l o c a t i o n i d =\” i d 3 7\” x =\”48\”

y=\”264\”><name x =\”56\” y=\”240\”>Running2</name><l a b e l k i n d =\” i n v a r i a n t\”

x =\”56\” y=\”272\”>x& l t ;1</ l a b e l></l o c a t i o n><l o c a t i o n i d =\” i d 3 8\” x =\”224\”

y=\”−256\”><name x =\”232\” y=\”−248\”>M i s s e d D e a d l i n e</name></ l o c a t i o n><l o c a t i o n i d =\” i d 3 9\” x=\”−24\” y=\”160\”><name x=\”−104\”

y =\”136\”>Running</name></ l o c a t i o n><l o c a t i o n i d =\” i d 4 0\” x=\”−24\”

y=\”−256\”><name x=\”−34\” y=\”−286\”>Ready</name></ l o c a t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 3 4\”/><t a r g e t r e f =\” i d 3 2\”/><l a b e l k i n d =\” a s s i g n m e n t\” x =\”−416\”

y=\”−192\”>s e t R e a d y F o r T r i g g e r i n g ( )</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 3 2\”/><t a r g e t r e f =\” i d 3 3\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−392\”

y=\”−296\”>t r i g g e r ?</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−392\”

y=\”−280\”>i n i t T a s k ( )</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 4 0\”/><t a r g e t r e f =\” i d 3 4\”/><l a b e l k i n d =\”g u a r d\” x=\”−288\”

y=\”−152\”>F i r m d e a d l i n e W i l l M i s s ( )</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−288\”

y=\”−128\”>f i r m D e a d l i n e M i s s e s ( )</ l a b e l><n a i l x=\”−80\”

y=\”−128\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 4 0\”/><t a r g e t r e f =\” i d 3 5\”/><l a b e l k i n d =\”g u a r d\” x =\”24\” y=\”−380\”>” +

” deadl i neN otMi s s edY etO rS O FT ( )</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”32\” y=\”−368\”>s e t W a i t F o r U p d a t e D y n a m i c S c h e d u l i n g ( ) ” +

”</ l a b e l><n a i l x =\”32\” y=\”−344\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 3 5\”/><t a r g e t r e f =\” i d 4 0\”/><l a b e l k i n d =\”g u a r d\” x=\”−224\”

y=\”−400\”>//Time u n i t c o m p l e t i o n\n” +

” x==1</l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−256\”

y=\”−368\”>u p d a t e D y n a m i c S c h e d u l i n g ( ) ” +

”</ l a b e l><n a i l x=\”−80\” y=\”−344\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 3 6\”/><t a r g e t r e f =\” i d 3 9\”/><l a b e l k i n d =\”g u a r d\” x=\”−224\”

y=\”224\”>// C om pl ete one run\n” +

” x==1</l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−224\” y=\”256\”>runOneTimeUnit ( ) ” +

”</ l a b e l><n a i l x=\”−112\” y=\”256\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 3 7\”/><t a r g e t r e f =\” i d 3 6\”/><l a b e l k i n d =\”g u a r d\” x =\”16\” y=\”296\”>// C o n t i n u e run\n ” +

” x&g t ;0</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”16\”

y=\”328\”>e n s u r e R u n C o m p l e t i o n ( )</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 3 9\”/><t a r g e t r e f =\” i d 3 7\”/><l a b e l k i n d =\”g u a r d\” x =\”24\” y=\”168\”>ready ForN ex tRun ( )</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”24\”

y=\”184\”>i n i t O n e R u n ( ) ” +

”</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 4 0\”/><t a r g e t r e f =\” i d 3 8\”/><l a b e l k i n d =\”g u a r d\” x =\”48\” y=\”−296\”>d e a d l i n e M i s s e d ( )</ l a b e l><l a b e l

k i n d =\” a s s i g n m e n t\” x =\”72\”

y=\”−276\”>s e t M i s s e d D e a d l i n e ( )</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 3 9\”/><t a r g e t r e f =\” i d 3 8\”/><l a b e l k i n d =\”g u a r d\” x =\”216\”

y=\”164\”>d e a d l i n e M i s s e d R u n ( )</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”216\”

y=\”184\”>s e t M i s s e d D e a d l i n e ( )</ l a b e l><n a i l x =\”224\”

y=\”160\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 3 9\”/><t a r g e t r e f =\” i d 3 4\”/><l a b e l k i n d =\”g u a r d\” x=\”−304\” y=\”22\”>t a s k H a s F i n i s h e d ( )

| | \n F i r m d e a d l i n e M i s s e d ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−304\”

y=\”48\”>f i n i s h !</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x=\”−304\”

y=\”64\”>f i n i s h e d ( )</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 3 9\”/><t a r g e t r e f =\” i d 4 0\”/><l a b e l k i n d =\”g u a r d\” x =\”48\”

y=\”−80\”>tas k H as MoreRunti m e ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x =\”48\”

y=\”−64\”>preem pt ?</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”48\”

y=\”−48\”>s e t P r e e m p t e d ( )</ l a b e l><n a i l x =\”40\” y=\”128\”/><n a i l x =\”40\”

y=\”−216\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 4 0\”/><t a r g e t r e f =\” i d 3 9\”/><l a b e l k i n d =\”g u a r d\” x=\”−208\” y=\”−188\”>” +

” deadl i neN otMi s s edO rSO FT ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−208\”

y=\”−176\”>run ?</ l a b e l></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 3 3\”/><t a r g e t r e f =\” i d 4 0\”/><l a b e l k i n d =\” s e l e c t\” x=\”−256\”

y=\”−327\”>i : i n t [ emin , emax ]</ l a b e l><l a b e l k i n d =\”g u a r d\” x=\”−256\”

y=\”−312\”>! f i n i s h S i g n a l s P e n d i n g ( )</ l a b e l><l a b e l k i n d =\” s y n c h r o n i s a t i o n\”

x=\”−256\” y=\”−296\”>r e a d y !</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”−256\”

y=\”−280\”>i n i t N e x t P e r i o d ( i )</ l a b e l></ t r a n s i t i o n></t e m p l a t e>” +

”<t e m p l a t e><name>Env i ronm ent</name>i n t t a s k i d , chan &amp ; t r i g g e r , i n t i n t e r a r r i v a l<d e c l a r a t i o n>i n t temp ;\n ” +

” c l o c k x ; \n” +

” i n t c l ;\n” +

”\n” +

” b o o l t a s k I s R e a d y ( ) {\n”+

” r e t u r n ( ! l o c k e d ( h t ) \n ” +

” &&amp ; ! l o c k e d ( l i n ) \n ”+

” &&amp ; t a s k R e a d y F o r T r i g g e r i n g [ t a s k i d−1] \n ”+

” &&amp ; c l &g t ;= i n t e r a r r i v a l ) ;\n ”+

”}\n”+

”\n”+

” v o i d u p d a t e C l o c k ( ) {\n”+

” x =0;\n”+

” i f ( c l & l t ; 3 2 0 0 0 ) {\n ” +

” c l ++;\n”+

” }\n ”+

”}\n”+

”\n”+

” v o i d r e s e t C l o c k ( ) {\n”+

” x =0;\n”+

” c l =0;\n”+

”}</ d e c l a r a t i o n><l o c a t i o n i d =\” i d 4 1\” x=\”−768\”

y=\”0\”><com m i tted /></ l o c a t i o n><l o c a t i o n i d =\” i d 4 2\” x =\”−960\” y=\”0\”><l a b e l k i n d =\” i n v a r i a n t\” x=\”−970\” y=\”15\”>x& l t ;=1</ l a b e l></l o c a t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 4 2\”/><t a r g e t r e f =\” i d 4 2\”/><l a b e l k i n d =\” g u a r d\” x =\”−1064\” y=\”−16\”>x==1</l a b e l><l a b e l k i n d =\” a s s i g n m e n t\”

x=\”−1104\” y=\”0\”>u p d a t e C l o c k ( )</ l a b e l><n a i l x=\”−1024\” y=\”−24\”/><n a i l x=\”−1024\” y=\”24\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 4 1\”/><t a r g e t r e f =\” i d 4 2\”/><l a b e l k i n d =\” s y n c h r o n i s a t i o n\” x=\”−896\”

y=\”64\”>t r i g g e r !</ l a b e l><l a b e l k i n d =\” a s s i g n m e n t\” x =\”−896\”

y=\”80\”>r e s e t C l o c k ( )</ l a b e l><n a i l x=\”−864\”

y=\”32\”/></ t r a n s i t i o n><t r a n s i t i o n><s o u r c e r e f =\” i d 4 2\”/><t a r g e t r e f =\” i d 4 1\”/><l a b e l k i n d =\”g u a r d\” x=\”−912\” y=\”−80\”>t a s k I s R e a d y ( )

&&amp ; x==0</l a b e l><n a i l x=\”−864\”

y=\”−32\”/></ t r a n s i t i o n></t e m p l a t e><s y s tem>\n” ) ; t o S t r i n g A l l ( a p p l i c a t i o n . t a s k s , p l a t f o r m . p r o c e s s o r s ) ; t o S t r i n g S y s t e m ( a p p l i c a t i o n . t a s k s , p l a t f o r m . p r o c e s s o r s ) ; f o u t . p r i n t ( ” ;</ s y s tem></nta>” ) ;

}}

In document MoVES - A tool for Modelling and Veriﬁcation of Embedded Systems (Sider 151-173)