PDF hosted at the Radboud Repository of the Radboud University Nijmegen

Document technical information

Format pdf
Size 476.7 kB
First found Jun 9, 2017

Document content analysis

Category Also themed
Language
Type
not defined
Concepts
no text concepts found

Persons

Organizations

Places

Transcript

PDF hosted at the Radboud Repository of the Radboud University
Nijmegen
The version of this text has not yet been defined or was untraceable and may differ from the
publisher's version.
For additional information about this publication click this link.
http://hdl.handle.net/2066/18941
Please be advised that this information was generated on 2014-10-15 and may be subject to
change.
Linear Parametric Model Checking of Timed Automata
T.S. Hune, J.M.T. Romijn, M.I.A. Stoelinga, F.W. Vaandrager
Computing Science Institute/
CSI-R0102 January 2001
Computing Science Institute Nijmegen
Faculty of Mathematics and Informatics
Catholic University of Nijmegen
Toernooiveld 1
6525 ED Nijmegen
The Netherlands
!
" # ! $ % !
& $ '( ) *
$ & ! $ !+ $ ! ',- ( * $ !!$ * * $ !!$ & *
$ $ + . $ !! ,-
& " $ !
$ * )* ! '#$
/* $ ! (&
! ) ! +
0123 01456
01403 72 63
!
"
! &8&8 &8&5 &5&9
:&;&;
!"#$ !%$ &' !"($ ) * + ,
)
,
* * ,
* - ,
,
*
, .*/ * 0 , ,
* .)
,
,
) 1
)
,
/ , ,
* 2 )
* 3
1
)
1
) * 4
) * * 5, )
,
*
1
! $ < = 80893 >+ ?$! '>?( ! $
[email protected]< = <5;77 >+ ?! ! ! '?(& * * ! ! + &
'***&$&!( !! $ :!&
Æ
5
!"#$ )
,
5
) ) 2
!6$ *
3 ,
* 0
) ) )
+ 0 5
3
) Æ
* 1
,
,
)
5
* )
) *
) !6$ 789 4
) ) )
0 ,
0 :
789 * ,
0 ; * 1
< ,
0 3
5
* 3
, ) !""$ * 1 5
*
0
) * * ,
* 1
)* =1
)
) 1
!"($ ,
1
&' 5
!($ 7&' 7&' 5
0
<
;
)
7&' ) 5 ,
0 . ' 7 )
/ 7&' :
* ,
*
)
,
2=== "6># * !"?$ * *3
!($
+ 7&' 1
*
+ !#$ * ,
) ) 5
,
5* * ,
5
2
* )
,
5
. 1
@ !>$/ * !#$ 1 ;
2 ) :
* ) ) <
A
) ) ) 6 3
) B 6 ,
* ) 6 ( # 33 * *
( 1
) )
01
B
C 1
! "
" # .
/ , "" " # # ! $$ # . / % # . . / . // . / % # ! $ " ./ & ! $ ' 0
C ! $ # ! ! $ # . / & # 0
& ! "#
! $ -C ! $ ! $ C . / ! $ C ( ,
C ) ! $ ! $ ( * ) C C D D D * :
- ,
,
E )
+ )
, , 4
) )
:
- )
) *
.
/ C C C <
,
)
* )
- ! $ ! $ ; - .
/ C *
)
5
.7&/ ,
) * ,
* !($ ) 7&' 7& ,
)
)
01
C 01
C ) * )*
,
F . ) /
+ " 1
)
1
4
* C 4
0
" .0
/ 4
,
)
+ # - ,
,
. / C F 4
) * , )
.. / . // . / 7
,
, ! $ 1
* ) ./ ) ./ + . / ,
6
, & . / C ! $ ,
! $ . / . / C + 1
-C )
C F + *
4
) 0
1
!B BF$ 5
,
!6G($
.& +/ # C . / & &
- " , # . / " " " + " # C " + ) " F ) , " -C F 2* F " * )
*
) , -
y>=q
S0
x:=0
S1
x<=p
x<=5
# $ ! 0
& + )
:
) 1* ,5
, ,
D ,
.
1
/ * , !$
, C -C . D /./ C F./ D )
.!$/./ C ./ )
*
.7 / # C . / ! ! .! ! / & " ! ! ! ! ·½
! ! " ! C . / .! ! $ # !
#
!/
. / # C . / . / . / C F . / C ./
C . / C C #F
& " F
. / . / C C D . / . / - . / C . / . / C !$
0 !/ ! $ # !
2 ,
* )
,
0 < 3
1
1*
)
,
)
* ) * " #
! & #
$ --C ¾% ¿%
*
$
% --C % % % % %
.! # ! % ! C % % ! ! $ C ¾%
% ! $ ! $ C ¿% % ! $ ! $ )
) )- 1#
! $ C $
$
$ # - !B BF$ & + ) * 2 & + , ! $ * 1
* ! $ 2 * ! $ C ! !$$$ *
!B$ * ,
$ ! $ C $ $%#& '
(
) $%
B ) & + A 1 !"6$ * 1,
2 ,
)
) ) 5
B C ! &
(
-C FH
*$$
+ C F ,#H
-C H
*
-./ C H
H
-C F
* * * -C )
C * C F 1 * 1 )
0* C +
8)
,
. C -C F/ )
*
. -C / )
2 )
F F 1 *
lock != i,
x > min_delay
lock != 0,
x> min_rw
x:=0
start
x<=max_rw
x:= 0
lock==0,
x > min_rw
x:=0
x>min_rw
x:=0,
lock:=i
set
x<=max_rw
x>min_delay,
lock==i
try_enter
x<= max_delay
cs
x:=0, lock:=0
# = ! :D # I) & + B .
,
;
1 !"
6 "% ">$H !"%$ / 2 .) / H H ,
@* ,
* F I
* * , ! /
,
) 0 & + * ) ) Æ
& + + & + 4
!"#$ 0
< * 4
** )*
2 3
%
Æ
* !>$ * )
** )$
@* ) )
!#$ )
I
) *
) 3
012 )
2 3
;
5 1 .& D "/ .& D "/ 1
)
. / F " + * .
"/ ' )
* .
F/ )
) 1
,
+ )
0 ,
,
) 1 * * 3 2) ;
5 1 .&@/ '
F & " ' ' F 1# # ' & ! '$ C ! ' $ ' 0
! '$ % " '! $ .234 ' " ' % '
. /5 ' ' ( .234 4 2) &@ . '/ ' .234 ! .234 &
! '$ C . / ! $ ! '$ &@ ) 3
)
0
1
*
. D D D / D . D D D /
C . D / D D . D / D . D /
+ )
,
) @
,
* * 5
* ) " ) F )
,
. / C . / C
C . C / C < 0 &@
* :,
@
5 ' .234 . '/ )
( C . C / D ) 0
-
6
7
8
9
:
C C C . / . / C C . / C . / C . / C . / C . / . / C . / C . / C ) . / C ) . / D C . / ) C . / %
%
%
%
%
?
1 ) * ,
3
* &@ 0* 4
)
) / . '/ .234 ! $ !
'
& 2,
* )
) , . / ,
. / ' F ( ) )
C F ,* . / C '
" )
,
, . / ,
. / ' F ( 2 1
, )
,
0 ,
) , . /.
'
'
'
' '
."/
0 D " ,
D " ,
)
,* * *
4
)
2 1 )
,
* , ,
* )
F ( D " ) , . / D .B/
)* .B/ ,
* *
. / C
.6/
. '/ . C / D .#/
' .6/ .#/ 7
"."/ ,
. / C
D ) :,
.B/ )
) ."/ ) * ) * ,
3
!>$ + :
&@ &@ . /
/ . '/ . ' / .234 . '/ ! ! '$ ! ' $ .!! $ ! $ - C . C / /
#
2)
< :
* &@- 3 J
6 7
2 @ 2 * @ .) ,
)
@/ )
2 &@ *
&@ 4
0
) &@ &@ * )
&@ * &@ ' C . / .' / C . C / 0
0
) ' ' ( ( E ' ' ( ( E '8(
';(
' ( ' (
' ( ' B C(
' ' ( ( E ' ' ( ( E '2(
'5(
' ( ' ' ( (
' ( ' ' ( B C(
'6( ' ( ' ( ' ( ' (
' ( ' (
2 K*
L ) &@ 2 )
KL )
&@ 4 )
KL ) ) )
*
K L B # &@ )* : .F / 2 )
' &@ * * )
3
*
¼
! '$ ! ! $
¼
C ! ' $ . '/ . ' /
. KL +
. / ! '$ . / C @* )
,
1 &@ . ' / . '/ . ' / . / ! ' $
4
. .' / / C *
7
C ' C ' ,* . / ! ' $ * " . '/ . ' /
. .' / / C @* )
,
C C . C / C .F / @* 7
".%/
C F @ . / C C F * 7
"."/ C F F
7
C ' C '!$ * B . '/ . ' /
. / ! '$ . / C ) . / ! ' $
. .' / / C C .' / 7
C .' / ' C ' * 6 . '/ . ' / ,
* . / ! ' $
. .' / / C C .' / @* )
,
C .' / C .F / @* 7
".%/
C F @ . / C C F * 7
"."/ C F F 7
C .' / ' C '!$ * # . '/ . ' / @* . / ! ' $
>
. / C @*
*
1 ' . '/ . ' / . / ! ' $ . / C )
*
1 ' . ' / . ' / . / ! ' $ ,
*
( . '/ . ' /
K"L +
. '/ . ' / . / ! ' $ @* 3
, . '/ . ' / )
. / ! '$ . / C 0,
, . '/ . ' /
¼
¼¼
" C " C ' C ' C .' / 7
. / ! '$ C .' / @* 0 . / C * C . C / ' )
, .B/ .#/ 7
" *
. / C B C B C ' C '!$ C .' / . / C C
.' / 7
@* 7
".%/ C .
C / 9 .B/ .#/ 7
" ) , *
. / C ,* . / ' . / ! '$
6 C 6 C .' / ' C ' 7
4
,
. / ! '$ . / C 4
,
C
. C / ' ) , .B/ .#/ 7
" *
. / C # C # C .' / ' C '!$ 4
,
C .' / . / C 7
@* 7
".%/ C . C / 9 .B/ .#/ 7
" *
. / C ,*
. / ' . / ! '$
( C ( ' . '/ . ' / . ' / . ' / @* *
. / ! ' $ . / C + * *
. / ! '$ . / C 2
) . / C ¼
¼¼
= @ 5
5 *54 .4/
!?$ 2 )
* 1
) )
4 * ;
)
) ;
* ;
)
.
0 >/ 2 * .* * 0
/ &@ 1
@
) )
* 4 < *
4 5 ( ,
* '
* < * ,
)
0 .( '/ )
. '/ &@ ( 8
"F
!F & D "$ ,
2 ) ( ,
!F &$
. '/
.( '/ . ' /
.( D " ' /
.( & D " '/ .( D " F '/
.( & D " F '/ .( D " F F '/
4
)
. '/ . ' / 1 :
0 .F F F '/ 0 .& D " F F ' / 2 )
* . ' / * *54 . '/ 2 * 0
;
,
* 2 . '/ * * 4
)
. '/ . ' /
; . '/ . ' / . ' / '
) * )
* *54 : &@
! '$ C ! ' $ . '/ . ' /
. @* ,
7
# * ,
. / . '/
. / C . / C * 7
".(/
. / C D " , +$ .234 " + !?$
6 I5
@ 3
." / )
" 5
2 )
,
'. / )
* ,
) ) &@
) &@ 3
&@ ) ) &@
) ) * ,
) .B ¿ / 2 *
,
.
*
6 ,
+ &@ )
)
) &@ * @ !BF$ 2 ' &@ -C '!$ &@ * ."/ ' C * . D /H
.B/ ' C * . / 4
3
0
* *
'!½ -C -C $ C '!½ -C $ ! -C $
2 * ) 0 ,
*
""
3 % . '/ . '!$/ ) 3
*
4 . '/ # !
.234 ) ! '$ - C !$
! '!$$$
! $ 4
* ,
9 7
? 3
* ) 7
C -C ' C '!$
KL ! '$ C !$ 2 ,
! ' $ )
) . / C ' ( .
" ( C C ' C ' . / C ' ' . / C '
B ( C C ' C ' . / C ' F !$ . / C '
6 ( C C ' C 9 . / C ' )
,
. / . / C . / !$ . / C '
# ( C C ' C D 9 . / C ' )
,
. / . / C . / !$ D . / C '
KL ! ' $ 4
,
,
1 , ! '$ C !$ '
* )
)* C . / C . / * . / C C ( C '
9 7
B )
0 ,
. / ' 0
* )
&@ 5
' # + @ !>$ * . /
C F , 4
,
) 5 / . '/ # !
.234 ) F ! '$ - D C ! ' #$ ! $ . KL F ! '$ D C 4
! ' #$ )
) ' # . / C 7
4
)
-
C F C F
2 * 0 ' # . / C ,* C F 2 ' ! '$ )
,
. / C . / !$ @ F . / C . / !$
. / C C F C F 2 ' ! '$ )
,
. / C . / . / !$ @ . / . / C .. / / .. / / !$ . / C KL ! ' #$ 2 & C F . / ' #C ' ,* .
C C F/ & F ) C F C F . / C ' . / . / !$ * . / .. / / !$ @ . / C '
"B
2 ) 1 ,
, . / ' ' 7
C 1.F . / !$ . / !$/
C .. / D !$ . / D !$/
C . D /*B
C
2,
* ,
) ' . / )
,
) ) , * )
' . / ) 4
* :
* . / C ' ,*
F . / D !$
.(/
9 ' )
,
* !$ . C / !$ D !$
C ' . / . / !$
9 ) , )
. / !$ . C / . / !$ D !$ . / D !$
. / !$ . / D !$
.%/
@* :
.(/ .%/ 1 0 *
0 F I) C 2 0 * ,
, . /
' ' * . / C . / . / . / .. / !$/ C !$
. / !$ C ' +
. / C . / D . / D . / D .. / D ! $/ C ! $
. / !$ C '
2 01 2 . / !$ . / C . / C . / . / .. / !$/ C !$
. / !$ C ' <
)
. / !$ C ,
* C :* .%/ C . /D !$ C . / C . / . / . / .. / !$/ !$
. / !$ C '
C ' )
C *
"6
9! 4 &@ )
**
: 9! ! * .! C . / !/ ! . '/ . '/
.234 ! . '/ . #/
.234 " ;
C .F / ¼ . '/
! & . '/ . ' / . ' !$ #/
. '/ . ' /
¼ . ' / 9 7
# 7
( ) * ,
. '/ * . / ! '$ . / C ./
2 * * & + 0
* 5
*
2 * ,
0
* * < 1
* K
L )
5
,
)
= * * #
+ # # " . '/ . / ! '$ ! $ " . /
@* + )
) F * . '/ 9 . / ! '$ 0 7
( 7
# )
) C . / C . / . / ! #$ @* 7
>
)
1 F ! $ D C . / C . /
, & + * ,
. / C . / 2 )
. / ! $ . / . / ! $ #F . / )
,
* 5
) . ' / . '/ 9 . / ! '$ 0 * 7
( 7
# )
)
' . / C ./
. / ! ' !$ #$ . ' / . ' / @* 7
> )
1
F ! ' !$$$ D C . / C ./ , & + * ,
. / C ./ 2 ) . / ! $ . / . / 9 7
J )
1 ! ' $ C !$ 9 7
( 7
# ) . / C . / ! ' $ ) 0 "F )
* 5
,
, * * .
"#
2 . / C . / * 0 . / . / . / @* *
. / =1
) . / . / . / . / ,
:
)
0 * 0 0 * 0 #
+ # # ! $ " . / " . '/ . / ! '$ 2 * 1
)
)* 3
* 5
* + ) ,
* . / . D / . D / . D D / )* * . / . D D / ) * )
* 1
) * ) * * + )
. / . D / )
C #F 5
@* 0 . D / C
. / 9 7
> )
,
. D / ! #$ . / ! $ . D / ! #$ . D / C . / 7
# 7
( )
¼ 1 ' . #/ . '/ . D / ! '$ @* 0
. '/ * ! $ )
. / . / . / @* *
1 * ) . ' / . / ! ' $
@* 0 . / C C !$ ,
)
,
C C D . / C ./ 9 7
# 7
( ,
1 ' . ' / . ' / . / ! ' $ @* 7
J ! ' !$$$ ,
* 7
> ! ' !$ #$ 9 . / C ./ 7
# 7
( )
1 ' . / ! '$ . ' !$ #/ . '/ *
0 * )
1
. ' / . '/
.
¼
¼
, 6 B ) * 5
" 5
* &@ 2 , ,
1 ,
,
,
* 4
F " )
,
)
* .)
/ " * ) "(
¸ µ
´Ë¼¸
´ ¸
¸
´Ë½¸
¸ µ
µ
´Ë¼¸
¸
µ
# % $ = :& ;&
$;6 #
4
) 0
) * % * * %
2 )
* )
) * '
0 ,
&@
4
* ) ,
) / % " % ; ) )
:,
) :,
2 ) % E
' (
' (
' ( ' (
' ( ' (
¼
' ( ' ( ' (
' ( ' (
½
¾
' ( ' ( ' (½ '¾ ( ' ' ( ' (
(
½
' (
' ( ' (
½ ¾
' ( ' (
¾
' (
' ( ' (
½ ¾
' ( ' (
) ,
: ! % $ . / . / C % ! % ! ' $ . '/ . ' /
! '$ ! ! %$ C
"%
. -
4
,
' . / ! '$ . / C %
' . / ! ' $ . '/ . ' / 4
% )
% *
% ) )
,
C C C F )
,
% % C % % C " D 1.% % /
$ @
7
% C F . / ! '$ . / C %
% % C + . / C * C . '/ . '/
)
C ' C ' )
% % C , % % C ) . / ! '$ . / C @* 7
# )
,
1 ' . '/ . ' /
. / ! ' $ 7
( *
' ) . ' / . ' / . / ! ' $ )
,
. '/ . ' /
$ 2 7
% C " D " . / ! '$ . / C %
% % C % % '
* . / C % . / C % @* * *
% ' )
,
1 ' . '/ ½ . ' / . / ! ' $ +* *
% ' *
' . ' / ¾ . ' /
½ ¾
. / ! ' $ . '/ . ' /
% % C % % '
* . / C % . / C % . / C %
*
*
' . '/ ½ . ' / ½ ¾
. ' / . / C % . / ! ' $ . '/ "- @* , )
' ' . '/ . ' / . / ! ' $ . / ! '$ . / C %
$ @
, +
. '/ . ' /
. / ! ' $
% C
% C C ' C ' * . / ! '$ . / C % C , % C % C ) . '/ . ' /
,
. '/ . ' / 1 ' . '/. ' / . ' /
. ' / @* 7
( )
,
. / ! ' $ )
,
* 7
# . / C . / ! '$
$ 2 +
. '/ . ' / . / ! ' $ , . '/ . ' /
½
¾
% C % C % % . '/ . ' / . ' / . ' / ' +* *
*
. / C % . / ! ' $ * *
0 *
. / C % . / ! '$ . / C % %
½
% C % C % % . '/ . ' / @* *
)
,
. / C % . / ! '$
"?
%
C * , 6 4
) *
# ) 1
*
) * ¿% & + * * $ ' (
FE FE FE ' ( ' ( ¼ ' (
E ' ( FE ' ( ' ( ' (
FE ' ( ' ( ' (
& ' ( & ' ( F ' ( ' ( !! ' ( & ' ( ' ( ' ( FE ' (
# ' ! ) * % * , ,
¾% % * ) 0
% )
B B * * H ,
* )
+ ;
)
,
)
1 ) * * )
) 0 ) * + 5
@ * @ * )
)
* ) ) &@ * 1 ,
* @
1 1 ,
) * , & + 4
,
) * ,
)
,
* * * )
8
,
.
,
/ , * & + : ! ! "J
&
< ) 1*
) ,
* 5
, * , *
* )
8
)
& + 2* ,
, & +
. / ;
B + ,
)
;
D B .& B / B B & + ) 789 C D
D C F5 ,
* F ,
*
F )
.! " # # )
8
.789/ # " , 7 ( 789 )
)
+ B 789 )
) )
) ) 01
+ C , , )
01
- C . . ) + ! - C + - C
4
, # 2,
* 1
, , ) ,
=1
, ,
,
0 .,
5
1
,/ B 6
4 ) 1
, * , 1
0
1
1
!$ 0
C ./ C ./ C 4
:
1
, 789 ,
)
1
!$ 0
,
* 1
, 789
)
* 1
!$ . / C !$ .
0
B/
1
, * ,
F C F ,
2 )
,
! $ C !$ 1
, 789 ,
)
1
)* 1
, , )
1
. ; ./ ./
/ 4
1
, 789 * .# //
) : # )
/ 4
)
F ,
* F ) )
. 5
)
/ *
)
* . )
/ *
)
4
789
3
)
& + 2 )
,
.* 0/ ">
* . ,
5
/ ) * 0
*
* , * ,
#
%
!
- ! $ C ¿% # # / / - ! $ ¼ ¼ C ¿%
6 ! $ C ¾% # # / / - ! $ ¼ ¼ C ¾%
. .
/ @ ,
* 789 , ,
# # / / 1
)
,
!# .,$ !,, .,$ !# .,$ !# .,$ )
,
..# // / C ..# / / / C (
'
) 1
) & 6 5
789 , 8 ( 789 2 ,
,
@* F
) 5
!. F/$ C ¿ &5
6 .
) ! $ C !$/ *
! $ 1
, F # / '
* ! $ C ¿ ; #. / /. / #. / 4
) 1
) )
,
* * * * 5
)
* 5
* *
. 789/ ) 2 )
) ! $ C ¿ , * ! $ C ¿ # / /. / C #. / & 6
! $ C ¿ # / ) #. / /. / #. / S0
x:=0
S1 x<=max
x=> min
S2
# ( ! ) ! :
)
1 .5
1
/ , ,
.0/ ) & + 2 !6$ ) & + ) ) )
,
789
* * !.F /$ ) 5
5
* .!B$/ 789 ) 789 # ,
)
,
* ,
#
! !.F /$ C ¿ $ # .# // ! $ C ¿ BF
. KLG
!.F /$ C ! $ :
& 6 K* LG 0 !.F /$ 7
1 1 1 ,
0 .
* 0 C ! ! ! ! C . / 1 C 1 ./H 1 ,
/ I) #., / C F
/.. / C 1 D 1 D" ,
* , )
,
..F / / C C ..# // / C 0 ! $ ! $ C ¿
(
'
9 ! * F #
D D ) * , !B$ *
* ) ,
,
.! #
.! ! # $
! $ C $
- ! $ C $
# ./ $ " $ $
2 * 0 C ! ! ! ) ! C . / ! $ * ! ! ! ! $ )
! C . / ./
* & + ) *
$ )
.
1
F/ )
,
! $ C $ , * !F$ C $ !"$ C $ F5
* * .* / ) :
) C F
.
9 + .! < ! $ - ! $ C $ $
, 9 & + =1
# * * ¿ ) 4
!F$ C ¿ !"$ C
¿ & ( ! $ C ¿ + ) =1
#
! $ C ¿ # / ) #. / C /. / 2 1
)
) ,
,
* ! $ ¾ ¿ #. / /. / 4
0 C ) 0 ) ,
& +
2& ¼ " # # / & ¼ " # = # + C 4# & ¼ ./ ./ ./ C ./ B"
#
" !
- ! $ C ¿% C # # / / - ! $ ¼ ¼ C ¿%
6 ! $ C ¾% # # / / - ! $ ¼ ¼ C ¾%
C 7
1
)
)
C
D D )
1
,
1
,
)
)
,
. <
/ / C !/$ !/ $
# # C !# $ !#$
# # / / C !.# //$ !.# / /$
2 ,
* ,
*
/ / C !/$ !/ $
# # C !#$ !# $
# # / # C !.# //$ !.# / /$
I) .# // 1
, 7
& & +
. .# /// C ./ ./ !.# //$ 4
) . .# /// C 4
) & 1 ./ . / !.# //$ !.# / /$ * . .# /// C & & 1
* & . .# /// C I) * ) ,
* ! $ ! $ * $ ! $ ! $ < C - ) " +
! $ C ¾% # / # # / / ! $ ¾ ¿% )
,
¼
¼
#
# / / - ! $ ¼
¼¼
¼
¼¼ C ¿%
."/ ) . / C *
! $ ¾ ¿% + ! $ ¾
¿% ! $ C ¾%
< C- 7
.# // 1
, ! $ C ¾% # # / / +
0 ! $ 4
# # / /
0 ! $ . )
- ! $ C ¾%
0 0
% ,
* ! $ 0
% ! $ C ¾% /
4
) 4
)
C .# // C .# / / 0 )
)
0 C ! ! ! ) ! C . / . / C C +
0 1 " 2 4
)
* C C * , )
, * 0 "#
¼
¼
¼
¼
¼
¼
¼
¼
¼
¼
¼
BB
¼
¼
2 , )
* )
,
0 ! $ , * 0
, 2 )
# # / / . / !.# / /$ !.# //$ C , ,
2* )
K
L
!.# //$ . / 0 * )
*
*
# # / /
7
¼
1 C 1 C
!$ . /
¼
C
!$ . /
F 1 1 1 C
) ,
C + :
1 1 . / C )
,
)
,
1 F 1 F 1 1 F :
1 1 2 * & & )
,
,
*
1 !$ . /
1 !$ . /
I) 1 , 0 1 C
¼
.=/ D
.
/
)
. D D D / C D D , )
,
1 F
I) C .# D / / & 4
. / C & 1
* C !$ C ! $ . / C . . // C & 1 4
)
C D . D D
. , , ) F F F ¼
! $ C D
¼
C . D
./ / 1
1
/
.# D /
1
1
# / ! $ 1
!$ . !$ . //
C . /
1 .
D /
1 . / C . / C B6
' ."/ .B/ *
. / C * ,
. / C 0 ! $ ¼
¼
(
'
, )
5
:
. )* /
)
) M
A * :
) 9 - ! ¼ $ C ¿% C # ¼ # / ¼ / - ! $ ¼ ¼ C ¿%
6 ! ¼ $ C ¾% # ¼ # / ¼ / - ! $ ¼ ¼ C ¾%
7
.# // 1
, 7
* * .# //./ ,
* *
C C I)
) * * & % (
'
) 1
) ,
& % " , : '
% * F C F C F
# F F / - ! $ C ¿% ! $ C ¿%
.
¼
¼
¼
¼
x<=2
y>=10
q0
q
x<=max
x:=0
# ) = 0 ';( ! !&
4
,
789 ,
* ,
15
) * ;
*
,
4
2=== '
!"B$ A 1 !"6$ .*/ 1
!6$ @
5
.)
01
,
,
/ @
.) / ,
!"%$
)* 789 4
1
:
) *
) 789 :
,
,
. * :
/ * )
)
*
# " ( ) :
789 ,
0 ; 0* * * 5
B#
= > '
(
) $%
2 )
* , ,
* ) B 4
Æ
* *
5
* * '
B # 2 )
*
) 2 *
789 - )
1 * 1
* 3 & ¾. ! !
/ 4 & F F 1 * &
)
,
, - C 4 C .!!$ C
3 C /
Æ9 > 4
) 1
C 4 !$ C 3
4
F * ) 4
,
5
* 5
!F$ C 3 !"$ C 3 I)
& ( *
! $ C 3 , .)
* ,
/ ! $ C 3 . / C F . / C
. / . / C & 6 *
15
* ) ,
* )
5
* & 6 ! $ C 3 )
F . / . / . / . / C 4 ! $ C 3
4
) C 4 C !$ C 3 .
9 > &
C ! $ C 3 & ¿. ! !/ 4
)
# 7
, . / C . / C F . / C
. / C " @* 5
)
,
!F$ C 3
.?/
! $ C 3 .J/
4
) ) C F C C C C !$ C 3 .>/
B(
+
C F C C C '
C . /
2 . / C F .?/ ) ! $ C 3 . / F
& # 2 Æ C F C C
C
C "
.J/ *
! $ C 3 * & + &
( *
! $ C 3
# 7
* )
" " @* )
,
C " C ! $ C 3 ."F/
C C
C " C
C ! $ C 3 @* )
,
.>/ .)
) . / C
F ,
* .>/ " / )
& ( ) C C
C
C ! $ C 3 I) & 6 *
3 G ) * * G ,
)
,
I
)
* )
)H . / *
. / )
,
C C ! $ C 3
& % *
C C ! $ C 3 4
,
"F ) *
5
1
) &+' 9 B '&9 ? ?
* 4
,
* ) * ) *
) ) BF )
,
1
) )
1
) .
,
0 / ) :
789 5
*
,
1 :
,
0 4
,
)
,
* )
789G
. )
F ,
* ,
* )
,
* ,
* /
B%
9# $%
> -##
2 )
1
) *
1
, < *
) ,
* )
1 0
* 5,
<
,
* , 1 @
* * +)* F * * *
2=== "6># .
4
857/ ) *
* )
) ) * 0 ) .F "/ ) ) )
* * ,
) 4
!"J "?$ 1
) *
.
? / 2 0,
) 1
5
1 * )
) ,
)
)
) " * ,
)
F ) 2 * 4
,
* ) ) *¾ ..I
I
/ .I
I
//
/ >[email protected] 2 ) !"J$ * * * ) - 4
,
1
* * )
4
,
)
)
)
C 2 B !"J$ 3
) * ) )
1
) 5
,
" 2 0
*
* )
) ,
,
0
* * , # * ! 200 G?% # *
* ! 222 G?% = <&
B?
+ ;
!"?$ ) ) )
* * *- B% 2 0
* * *
)
, )
* Æ
* ) !"?$
* * ,
, 1
4
,
1
* * )
4
,
)
)
)
C ) )
2 )
C + 5
)
,
, * C * 789 )
1
) &5
6 ) 4
) , * 0
* ) B & 6 )
4
0 * + C ! &" !,5 &"
- C , ! & !,5 & 4
0* ) ) B% 0
, *
) 0
, * * , )
,
5
0
/ >[email protected]
4
,
* * & % )
0 , ,
0* I) )
,
) * ) )
,
* 5
* )
) , * F 5
3
,
, * 0
* & ( )
, 0
,
* * , )
7
)
)
*B ,
+ ? 5 * * )
C ) 789 ,
) ,
1 ."/ * * .B/ 0
+
, @* )
) C 4
) *
& 6 , ,
) ,
)
) " * * ,
* C ) 4
* , * *
* 2 !"?$ ) 0
)
,
) )
)
*
- B% B% 5 # >[email protected]
BJ
B;1C
B;1C
B;9C
B;9C
B;9C
B;9C
8&7 ;16 G$
!
; 133 H$
;&0 20 G$
;; ;2 G$
!
; 133 H$
8&0 231 G$
# * <# 0
,
* ,
.) ,
!"?$/ + * Æ
* ) * 1
) ,
,
1
4
,
* 3
,
*
) 0
4
,
)
0
) ) - B% C B% 5 B% B% C 5 )
2 )
+ * , * ,
) ) )
,
789 )
* & % 2 *
) * & )
8,
8 :
2 )
5) ) :
* ,
2 !J$ ,
* @
!J$ * !#$ )
,
,
B1C
B1C
B1C
; ;&2 25 G$
8 ;; ;13 G$
8 2&6 05 G$
# + <# $!! * )
,
!J$ 2 !J$ ;
) *
* 0 4
* ) ) *
,
*
B>
<
,
!J$ B D 6 )
,
* * ,
* ) ) ) 1
,
3
2 * )
01
,
9 *
)
,
1
B D6 )
,
)
,
B ) ) !J$ * * ) ,
0
* * ) ;
01
,
,
!J$ ) * )
)
,
* ,
!J$ ,
)
,
) *
,
!J$ ,
2 )
,
B ) ,
!J$
$%#
4
,
1
) 3
,
* A 1 1 2 A .) ,
5
/ )
3
) ) * ) 5
4
)
1 ) B '&9 B%% 3 &
N 9 ) 1 ,
A ) ) ) !#$ ) 6 !
;& G& $! ! ,& ,& !)! & I&"& ! & ?% "&=& ! ! A& %$ ! G ! I ;77; 033 ! ;J89& )> ;778&
8& & ! &,& & ! & ! ;80F;12J
826 ;775&
2& & && ?% ! G&K& >!& = ) & "# $ !
678J03;& G = ;772&
5& & <& ! & & $ L $ ! & <&& < ! &=& ! %" &
$ '(
;166 ! 5;7J525& )> 8333&
6& A& ! & , $ ! ?& & = + <<< ;275
,=G& F--
&*&! & - I 8333& $! $ &
6F
0& G& % & * @& G & @ & ! & K
& HF G! )
) & &I& ? ! G&K& >! ! %) &
$ '(
>
! ;589 ! 650J663& )> I-I ;771&
9& &?& &<& , ! &,& & &
$ & GA*)? & ;77;&
1& =&& D I&)=& H && ! I& & $!! $ M <& ! $ $ ! <! ! ;8;9 ! 5;0J52;& )
> ;779&
7& & & ! + +) & I& ! &
$
'(
*
+ ! ! A$ : 539 !
;79J8;8& )> ;773&
;3& :& ! = * ! & !, &
! $
- !$.//0& <<< )
= ;777&
;;& & & ?% =&)?& ? ! ?& ")& F G! ?$!
& @& A$ ! / &
$ '(
;865 ! 503J502&
)> ;779&
;8& <<< & <<< !! ? = & ! ;275);776
;770&
;2& ,& ,& # & $ * !
6';(F;J;; :$ ;719&
;5& H& A& , =& = ! "& K& & &1 2
!
3
;';J8(F;25J;68 @$ ;779&
;6& &:& , $ "&I& ! G& & = + )
! & &=& ! ?& ! + &
!
+
4 +
! -++./50
,$ ;510 ! ;52J;69&
)> ;771&
;0& && ,& 67 $ & G H =$ & :
;770&
;9& &=&,& ! G&&& & G + <<< ;275 )
8& )3337 )
G 8333& ! ! ! &
2
!
3 -!0&
;1& G&&& ! :&"& >!& <<< ;275& I&)=& H
! # &
$*$! +
*
77 ! $ A ;03; ! 62J95& )> ;777&
;7& $ &
83& & K
& G! ! & A& %$ ! :&"& >! !
7 ! ;575 ! ;;5J;68& )> @$ ;771&
"
#
6"
,
1
1
)
,
,
3
;
1
1
, )
)
- &@
*
# / 1
, )
.
/ ,
*
% $ *
*
(
,
&
"
!
1
.
)
'
6
+
7
6B

Similar documents

×

Report this document