Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : http://savenkov.lvk.cs.msu.su/mc/lect03.pdf Äàòà èçìåíåíèÿ: Mon Mar 19 03:44:30 2012 Äàòà èíäåêñèðîâàíèÿ: Sat Apr 9 22:23:53 2016 Êîäèðîâêà:

3 (LTS). LTS . ()



· 15 · 3 : 1 (10 ) + 2 ( 5 ) · ·
­ 0..9 ­ , . ; , -1 , ­ 10..19 ( ) ­ , ­ 20 ( , ) +1 ; , +1 =>



· · · · · · · , (LTS) , ,



· · , , · , ·


...
, ,


, :
() ( ) ()

( )



( )

()



()







int main (){ printf( }

t t l t l l l t l l t (ACFG) l = T t = T t l t



, ,

( TAKEOFF (!FALL) U (LANDED))

l l l t l t t l l l l l l



( )




(LTS)
TS = S , Act, Ã , I , AP, L Ã
· ­ , S · ­ , ­ , Act a à · à S â A â S ­ ct , I · S ­ , · AP ­ , · L : S 2 AP ­ .
S ­ , Act ­
:

a

s, a0 , s' Ãa s Ãa0 s' Ã Ã


LTS
0,?,? 0: int x = 2; 1: int y = 0; 2: while (x>0) { 3: y += 1; 4: x -= 1; } 5:
int x = 2;

1,2,?
int y = 0;

2,2,0
x>0 x -= 1;

2,1,1
x>0

3,2,0
y += 1;

3,1,1
y += 1;

4,2,1 2,0,2

4,1,2
x -= 1; !(x > 0)

: (, x, y)

5,0,2


LTS
0,?,? 0: int x = 2; 1: int y = 0; 2: while (x>0) { 3: y += 1; 4: x -= 1; } 5:
int x = 2;

S
à Ã
S â Act â S
a

1,2,?
int y = 0;

2,2,0
x>0 x -= 1;

2,1,1
x>0

3,2,0
y += 1;

3,1,1
y += 1;

I S

4,2,1 2,0,2

4,1,2
x -= 1; !(x > 0)

L

: (, x, y)

5,0,2

ßcn t = 0, cn t = 1,.. .Ý
Ò
Ò AP = Ð x = 0, x = 1,.. . Ù
Ò y = 0, y = 1,.. .
Ò Ñ ×



· AP , · · , · ­ «»


LTS
0,?,? 0: int x = 2; 1: int y = 0; 2: while (x>0) { 3: y += 1; 4: x -= 1; } 5:
int x = 2;

S
à Ã
S â Act â S
a

1,2,?
int y = 0;

2,2,0
x>0 x -= 1;

2,1,1
x>0

3,2,0
y += 1;

3,1,1
y += 1;

I S

4,2,1 2,0,2

4,1,2
x -= 1; !(x > 0)

L

: (, x, y)

5,0,2

ßcn t = 0, cn t = 1,.. .Ý
Ò
Ò AP = Ð {x = 0, x = 1,. ..} Ù ,.. . AP =
Ò y = 0, y = 1,.. .
Ò Ñ ×


LTS
x = ? 0: int x = 2; 1: int y = 0; 2: while (x>0) { 3: y += 1; 4: x -= 1; } 5:
int x = 2;

S
à Ã
S â Act â S
a

x = 2
int y = 0;

x = 2
x>0 x -= 1;

x = 1
x>0

x = 2
y += 1;

x = 1
y += 1;

I S

x = 2 x = 0

x = 1
x -= 1; !(x > 0)

L
AP = {x = 0, x = 1,...}

: (, x, y)

x = 0


LTS
x = ? 0: int x = 2; 1: int y = 0; 2: while (x>0) { 3: y += 1; 4: x -= 1; } 5:
: (, x, y)
int x = 2;

x = 2
x -= 1;

x = 1
x -= 1;

x = 0
AP = {x = 0, x = 1,...}


«» ,


?


LTS
int p; process Prod() { while(1) 1.1: if(p < 2) 1.2: p += 1; } process Cons() { while(1) 2.1: if(p > 0) 2.2: p -= 1; } : ( Prod, Cons, p)
( . , ) Prod Cons

(1.1,2.1),0
p<2

p -= 1

(1.2,2.1),0
p += 1

(1.1,2.2),1
p>0 p<2

(1.1,2.1),1
p<2 p -= 1

(1.2,2.1),1
p += 1 p>0

(1.1,2.1),2
p>0

(1.2,2.2),1
p += 1

p -= 1 ,

(1.1,2.2),2



· , · = · LTS



· · , , , · ,



· Prod Cond · , · ­
­


­ !
· :
­ ()
·
Prod Cons

ELF System board Processor


­ !
· :
­
·


­ !
· :
­
· ,


LTS
· LTS , AP = {a}
a a a a



­


LTS
· LTS ,

? ?
­



s a
Post ( s, a ) = {s' S | s à s' }, Post ( s) = Ã
s s a a b c
a aAct



Post ( s, a )

a a b c

s a
Pre ( s, a ) = {s' S | s' Ãa s}, Pre ( s) = Ã
a a b c s s
aAct



Pre ( s, a )

a a b c



· TS S , t à , I , AP, L = Ac , Ã
­ , :
a

I 1
:

Post ( s, a) 1, s S , a Act

­ ,

I 1 Post ( s) {s' S | L( s' ) = A} 1, s S , A 2
s

AP



· TS , :

= s0a1s1a2 s2 ...an sn , si Ãa si +1 0 i < n. Ã
i +1

· TS :

= s0a1s1a2 s2a3..., si Ãa si +1 0 i. Ã
i +1

· ,

s0 I



· , . · TS .



0,?,?
int x = 2;

(1.1,2.1),0
p<2

1,2,?
int y = 0;

p -= 1

(1.2,2.1),0
p += 1 x>0

(1.1,2.2),1
p>0 p<2

2,2,0
x>0 x -= 1;

2,1,1 3,1,1
y += 1;

(1.1,2.1),1
p<2 p -= 1

3,2,0
y += 1;

4,2,1 2,0,2

4,1,2
x -= 1; !(x > 0)

(1.2,2.1),1
p += 1 p>0

(1.1,2.1),2
p>0

(1.2,2.2),1
p += 1

5,0,2

(1.1,2.2),2
p -= 1



0,?,?
int x = 2;

(1.1,2.1),0
p<2

1,2,?
int y = 0;

p -= 1

(1.2,2.1),0
p += 1 x>0

(1.1,2.2),1
p>0 p<2

2,2,0
x>0 x -= 1;

2,1,1 3,1,1
y += 1;

(1.1,2.1),1
p<2 p -= 1

3,2,0
y += 1;

4,2,1 2,0,2

4,1,2
x -= 1; !(x > 0)

(1.2,2.1),1
p += 1 p>0

(1.1,2.1),2
p>0

(1.2,2.2),1
p += 1

5,0,2

(1.1,2.2),2
p -= 1



0,?,?
int x = 2;

(1.1,2.1),0
p<2

1,2,?
int y = 0;

p -= 1

(1.2,2.1),0
p += 1 x>0

(1.1,2.2),1
p>0 p<2

2,2,0
x>0 x -= 1;

2,1,1 3,1,1
y += 1;

(1.1,2.1),1
p<2 p -= 1

3,2,0
y += 1;

4,2,1 2,0,2

4,1,2
x -= 1; !(x > 0)

(1.2,2.1),1
p += 1 p>0

(1.1,2.1),2
p>0

(1.2,2.2),1
p += 1

5,0,2

(1.1,2.2),2
p -= 1



0,?,?
int x = 2;

(1.1,2.1),0
p<2

1,2,?
int y = 0;

p -= 1

(1.2,2.1),0
p += 1 x>0

(1.1,2.2),1
p>0 p<2

2,2,0
x>0 x -= 1;

2,1,1 3,1,1
y += 1;

(1.1,2.1),1
p<2 p -= 1

3,2,0
y += 1;

4,2,1 2,0,2

4,1,2
x -= 1; !(x > 0)

(1.2,2.1),1
p += 1 p>0

(1.1,2.1),2
p>0

(1.2,2.2),1
p += 1

5,0,2

(1.1,2.2),2
p -= 1



0,?,?
int x = 2;

(1.1,2.1),0
p<2

1,2,?
int y = 0;

p -= 1

(1.2,2.1),0
p += 1 x>0

(1.1,2.2),1
p>0 p<2

2,2,0
x>0 x -= 1;

2,1,1 3,1,1
y += 1;

(1.1,2.1),1
p<2 p -= 1

3,2,0
y += 1;

4,2,1 2,0,2

4,1,2
x -= 1; !(x > 0)

(1.2,2.1),1
p += 1 p>0

(1.1,2.1),2
p>0

(1.2,2.2),1
p += 1

5,0,2

(1.1,2.2),2
p -= 1



sS · ( ) TS, ,

s0 Ã s1 Ã ... Ã n sn = s. Ã Ã Ã
2

a1

a

a

· Reach(TS) , TS.



· ; . (). · .



· :

TS = S , Act, Ãa , I , AP, L Ã
· ( ): · :

= s0a1s1a2 s2a3...
AP

tr = L( s0 ) L( s1 ) L( s2 ). .. (2 )

«»



(1.1,2.1),0
p<2


{a p = 0} a a !a !a a a

2 !a !b !a !b a b a b !a !b !a !b

ßa p 0Ý Ð Ù b p = 1 × Ñ

(1.2,2.1),0
p += 1

(1.1,2.1),1
p>0

(1.1,2.1),1
p -= 1

(1.1,2.1),0
p<2

(1.2,2.1),0
p += 1 ...



· : a « » b « » · : « · : · :
a ü ü ü ü ü ü ü ... a ü ü ü ü b a ü ... a ü ü ü ü ü b ü ... ü ü ü ü ü ü ü ...

»



· , AP

(2 )

· : · TS :

TS Traces(TS ) TS ( P ) P



() ()

( )



( )

()



()







· I: N ­ , ­ N , , : N â AP {T, }

I (tr) = , ,

n > 0, p AP ( n , p ) = T p L( s )



· tr tr' , :

I (tr) = , ,

I (tr' ) = , , '

: N â AP {T, } ' : N â AP' {T, }
AP' AP

· , tr' tr tr ' () tr ( ),

: N N : n, k N (n k (n) (k ) n N , p AP' ( (n, p) = ' ( (n), p)

)

)



p = T q = F r = F p = T q = F r = T p = F q = F r = F p = F q = T r = T p = F q = T r = F

AP={p,q,r}
p = T q = F p = T q = F p = F q = F p = F q = T p = F q = T

AP'={p,q}
p = T q = F p = F q = F p = F q = T

AP'={p,q}



() ()

( )



( )

()



()







· P ­ , ­ . () P , : , · , :



· P ­ , ­ . () P , :

M P


· , :


tr Trace s(TS ( P ))tr' Trace s(TS ( M )) : tr tr'

,





· TS , ?
­ , ­ , ­ , ­ , . . , ­ . .



· TS , ?

TS = S , Act, Ã , I , AP, L Ã a TS ' = S ' , Act' , Ã ' , I ' , AP' , L' Ã
Ac t ' Ac t AP ' AP : S S ' , s0 ' = ( s0 ) s1 Ãa s2 ( s1 ) Ãa ( s2 ) Ã Ã s S , L' ( ( s )) = L( s ) AP '


a



p = T,q = T a p = F,q = F b p = T,q = T d p = F,q = T e p = T,q = F f p = F,q = T q = T q = F f c q = T e q = T q = T d c q = F b q = T d q = F f q = T a q = F b e c q = T a

(P)

(M1)

(M2)



() ()

( )



( )

()



()







· , :
1. , , 2. ,



· , :
1.

AP APM
( )

2.

M P
( )

· ,



p = T,q = T a p = F,q = F b p = T,q = T d p = F,q = T e p = T,q = F f p = F,q = T q = T q = F f c q = T e q = T q = T d c q = F b q = T d q = F f q = T a q = F b e c q = T a

(P)

(M1)

(M2)


­
· , p=Tq=T ­ , · , q= F q= T ­ , · q= F 3 q= T ­ 1 , 2 ­ .



() ()

( )



( )

()



()






! ?