Лекция 3. Моделирование программ и схем (1185525), страница 3
Текст из файла (страница 3)
 ðåçóëüòàòåïîëó÷àåòñÿ óíèêàëüíàÿ ðàçìåòêà òî÷åê âõîäà è âûõîäà äëÿ âñåõîïåðàòîðîâ ïðîãðàììû.x:=y; if x>0 then y:=z else z:=x ; x:=z;0: x:=y;:1 2: if x>0 then 3: y:=z:4 else 5: z:=x:6 ;:7 8: x:=z;:90: x:=y;:1 1: if x>0 then 3: y:=z:4 else 5: z:=x:4 ;:4 4: x:=z;:9Òðàíñëÿöèÿ ïðîãðàìì â ìîäåëè ÊðèïêåÂâåäåì ñïåöèàëüíóþ ïåðåìåííóþ pc , êîòîðàÿ íàçûâàåòñÿñ÷åò÷èêîì êîìàíä ; åå çíà÷åíèÿìè ÿâëÿþòñÿ ìåòêè ïðîãðàììû,à òàêæå îñîáûé ýëåìåíò ⊥ , êîòîðûé ñîîòâåòñòâóåòíåîïðåäåëåííîìó çíà÷åíèþ . Íåîïðåäåëåííîå çíà÷åíèåòðåáóåòñÿ, êîãäà ðå÷ü èäåò î ïàðàëëåëüíûõ ïðîãðàììàõ. Âòàêîì ñëó÷àå ðàâåíñòâî pc = ⊥ ÿâëÿåòñÿ ïðèçíàêîì òîãî, ÷òîïðîãðàììà íåàêòèâíà.Ïóñòü V ìíîæåñòâî ïåðåìåííûõ ïðîãðàììû.
Îïðåäåëèììíîæåñòâî V 0 øòðèõîâàíûõ ïåðåìåííûõ v 0 , ïî îäíîé äëÿêàæäîé ïåðåìåííîé v ∈ V , à òàêæå øòðèõîâàíóþ ïåðåìåííóþpc 0 äëÿ ñ÷åò÷èêà êîìàíä pc .Òàê êàê êàæäûé ïåðåõîä îáû÷íî èçìåíÿåò íåáîëüøîå ÷èñëîïåðåìåííûõ ïðîãðàììû, çàïèñü same(Y ) áóäåò èñïîëüçîâàòüñÿäëÿ îáîçíà÷åíèÿ ôîðìóëûV0y ∈Y (y = y ) .Òðàíñëÿöèÿ ïðîãðàìì â ìîäåëè ÊðèïêåÑíà÷àëà âûïèøåì ôîðìóëó, îïèñûâàþùóþ ìíîæåñòâîíà÷àëüíûõ ñîñòîÿíèé ïðîãðàììû P .
Äëÿ çàäàííîãî óñëîâèÿpre(V ) , îïðåäåëÿþùåãî íà÷àëüíûå çíà÷åíèÿ ïåðåìåííûõïðîãðàììû P , îíà èìååò âèäS0 (V , pc) ≡ pre(V ) ∧ pc = m .Ïðîöåäóðà òðàíñëÿöèè C çàâèñèò îò òðåõ ïàðàìåòðîâ: âõîäíîéìåòêè ` , ðàçìå÷åííîãî îïåðàòîðà P è âûõîäíîé ìåòêè `0 .Ïðîöåäóðà îïðåäåëÿåòñÿ ðåêóðñèâíî è èñïîëüçóåò ïî îäíîìóïðàâèëó äëÿ êàæäîãî òèïà îïåðàòîðîâ ÿçûêà. ÏðåäèêàòC(`, P, `0 ) ïðåäñòàâëÿåò ìíîæåñòâî ïåðåõîäîâ ïðîãðàììû P ââèäå äèçúþíêöèè âñåõ ïåðåõîäîâ ýòîãî ìíîæåñòâà.
Êàæäîåñëàãàåìîå òàêîé äèçúþíêöèè, ñîîòâåòñòâóþùåå îòäåëüíîìóïåðåõîäó, îïðåäåëÿåò çíà÷åíèå áóëåâîãî óñëîâèÿ è çíà÷åíèåñ÷åò÷èêà êîìàíä, äëÿ êîòîðûõ âîçìîæíî âûïîëíåíèå ýòîãîïåðåõîäà. Óêàçàííîå ñëàãàåìîå îáðàùàåòñÿ â èñòèíó âñÿêèéðàç, êîãäà ïåðåõîä îñóùåñòâèì; â ïðîòèâíîì ñëó÷àå îíî áóäåòëîæíûì.Òðàíñëÿöèÿ ïðîãðàìì â ìîäåëè ÊðèïêåÎïåðàòîð ïðèñâàèâàíèÿ:C(`, v := e, `0 ) ≡pc = ` ∧ pc 0 = `0 ∧ v 0 = e ∧ same(V \ {v }) .Òðàíñëÿöèÿ ïðîãðàìì â ìîäåëè ÊðèïêåÎïåðàòîð ïðèñâàèâàíèÿ:C(`, v := e, `0 ) ≡pc = ` ∧ pc 0 = `0 ∧ v 0 = e ∧ same(V \ {v }) .Îïåðàòîð skip:C(`, skip, `0 ) ≡ pc = ` ∧ (pc 0 = ` ∨ pc 0 = `0 ) ∧ same(V ) .Òðàíñëÿöèÿ ïðîãðàìì â ìîäåëè ÊðèïêåÎïåðàòîð ïðèñâàèâàíèÿ:C(`, v := e, `0 ) ≡pc = ` ∧ pc 0 = `0 ∧ v 0 = e ∧ same(V \ {v }) .Îïåðàòîð skip:C(`, skip, `0 ) ≡ pc = ` ∧ (pc 0 = ` ∨ pc 0 = `0 ) ∧ same(V ) .Ïîñëåäîâàòåëüíàÿ êîìïîçèöèÿ îïåðàòîðîâ:C(`, P1 ; `00 : P2 , `0 ) ≡ C(`, P1 , `00 ) ∧ C(`00 , P2 , `0 ) .Òðàíñëÿöèÿ ïðîãðàìì â ìîäåëè ÊðèïêåÎïåðàòîð âåòâëåíèÿ if-then-else:C(`, if b then `1 : P1 else `2 : P2 end if, `0 )ïðåäñòàâëÿåò ñîáîé äèçúþíêöèþ ñëåäóþùèõ ÷åòûðåõ ôîðìóë:Ipc = ` ∧ pc 0 = `1 ∧ b ∧ same(V ) ,Ipc = ` ∧ pc 0 = `2 ∧ ¬b ∧ same(V ) ,IC(`1 , P1 , `0 ) ,IC(`2 , P2 , `0 ) .Ïåðâûé äèçúþíêò ñîîòâåòñòâóåò ñëó÷àþ, êîãäà óñëîâèå bèñòèííî.
Ïðè ýòîì ñëåäóþùèì áóäåò âûïîëíÿòüñÿ îïåðàòîð P1. Âòîðîé äèçúþíêò ñîîòâåòñòâóåò ñëó÷àþ, êîãäà óñëîâèå bëîæíî. Òîãäà ñëåäóþùèì áóäåò èñïîëíÿòüñÿ îïåðàòîð P2 . Îáàäèçúþíêòà îïèñûâàþò ïåðåõîäû, çàíÿòûå èñêëþ÷èòåëüíîèçìåíåíèåì ïîêàçàíèÿ ñ÷åò÷èêà êîìàíä. Òðåòèé è ÷åòâåðòûéäèçúþíêòû ýòî ôîðìóëû äëÿ ïåðåõîäîâ P1 è P2 .Òðàíñëÿöèÿ ïðîãðàìì â ìîäåëè ÊðèïêåÎïåðàòîð èòåðàöèè while-do:C(`, while b do `1 : P1 end while, `0 )ïðåäñòàâëÿåò ñîáîé äèçúþíêöèþ ñëåäóþùèõ òðåõ ôîðìóë:Ipc = ` ∧ pc 0 = `1 ∧ b ∧ same(V ) ,Ipc = ` ∧ pc 0 = `0 ∧ ¬b ∧ same(V ) ,IC(`1 , P1 , `) .Ïåðâûé äèçúþíêò ñîîòâåòñòâóåò ñëó÷àþ, êîãäà óñëîâèå bèñòèííî. Ïðè ýòîì ñëåäóþùèì áóäåò èñïîëíÿòüñÿ îïåðàòîð P1 .Âòîðîé äèçúþíêò ñîîòâåòñòâóåò ñëó÷àþ, êîãäà óñëîâèå bëîæíî, è òîãäà èñïîëíåíèå îïåðàòîðà èòåðàöèè çàâåðøàåòñÿ.Òðåòèé äèçúþíêò ýòî ôîðìóëà äëÿ ïåðåõîäîâ îïåðàòîðà P1 .Çàìåòèì, ÷òî òî÷êà âûõîäà îïåðàòîðà P1 ñîâïàäàåò ñ òî÷êîéâõîäà â îïåðàòîð èòåðàöèè.
Òàêèì îáðàçîì, êàê òîëüêîçàâåðøàåòñÿ èñïîëíåíèå îïåðàòîðà P1 , îïåðàòîð èòåðàöèèçàïóñêàåòñÿ ïîâòîðíî.Òðàíñëÿöèÿ ïðîãðàìì â ìîäåëè ÊðèïêåÏàðàëëåëüíàÿ êîìïîçèöèÿ P :P = ` : cobegin `1 : P1L `01 k `2 : P2L `02 k . . . k `n : PnL `0n coend : L0 .Òðàíñëÿöèÿ ïðîãðàìì â ìîäåëè ÊðèïêåÏàðàëëåëüíàÿ êîìïîçèöèÿ P :P = ` : cobegin `1 : P1L `01 k `2 : P2L `02 k . . . k `n : PnL `0n coend : L0 .ôîðìóëàC(`, cobegin P1 k P2 k . . .
k Pn coend, `0 )ïðåäñòàâëÿåò ñîáîé äèçúþíêöèþ òðåõ ñëåäóþùèõ ïîäôîðìóë:Ipc = ` ∧ pc10 = `1 ∧ . . . ∧ pcn0 = `n ∧ pc 0 = ⊥ ,Ipc V= ⊥ ∧ pc1 = `01 ∧ . . . ∧ pcn = `0n ∧ pc 0 = `0 ∧∧ ni=1 (pci0 = ⊥) ,Wn0i=1 C(`i , Pi , `i ) ∧ same(V \ Vi ) ∧ same(PC \ {pci }) .IÏåðâûé äèçúþíêò îïèñûâàåò èíèöèàëèçàöèþ ïàðàëëåëüíûõïðîöåññîâ. Âòîðîé äèçúþíêò îïèñûâàåò çàâåðøåíèåïàðàëëåëüíîé ïðîãðàììû. Òðåòèé äèçúþíêò îïèñûâàåò÷åðåäóþùååñÿ èñïîëíåíèå ïàðàëëåëüíûõ ïðîöåññîâ.Òðàíñëÿöèÿ ïðîãðàìì â ìîäåëè ÊðèïêåÎïåðàòîð wait.Îïåðàòîð wait(b) ïåðèîäè÷åñêè ïðîâåðÿåò çíà÷åíèå áóëåâîéïåðåìåííîé b , äî òåõ ïîð ïîêà îí íå îáíàðóæèò, ÷òî bîáðàòèëàñü â èñòèíó. Êîãäà ïåðåìåííàÿ b ñòàëà èñòèííîé,îñóùåñòâëÿåòñÿ ïåðåõîä ê ïîñëåäóþùåìó îïåðàòîðóïðîãðàììû.Ôîðìóëà C(`, wait(b), `0 ) ïðåäñòàâëÿåò ñîáîé äèçúþíêöèþñëåäóþùèõ äâóõ ïîäôîðìóë:pci = ` ∧ pci0 = ` ∧ ¬b ∧ same(Vi ) ,pci = ` ∧ pci0 = `0 ∧ b ∧ same(Vi ) .Ïðèìåð ïðîãðàììûÇàäà÷àÈìååòñÿ íåñêîëüêî êîìïüþòåðîâ è òîëüêî îäèí ïðèíòåð.
Íèîäèí êîìïüþòåð íå îñâåäîìëåí î ñóùåñòâîâàíèè äðóãèõêîìïüþòåðîâ. Êàê ïðàâèëüíî îðãàíèçîâàòü èõ âçàèìîäåéñòâèå,÷òîáû âñå îíè ìîãëè ïîëüçîâàòüñÿ ýòèì ïðèíòåðîì?'$w HHÏðèìåð ïðîãðàììûÇàäà÷àÏðåäïîëàãàåòñÿ òàêæå, ÷òî ó ïðèíòåðà åñòü åäèíñòâåííûéîäíîáèòîâûé ðåãèñòð R, îáùåäîñòóïíûé äëÿ ñ÷èòûâàíèÿ èçàïèñè. Ýòîò ðåãèñòð ìîæåò íàõîäèòñÿ â îäíîì èç äâóõñîñòîÿíèé busy (ïðèíòåð çàíÿò) è free (ïðèíòåð ñâîáîäåí).'$wRHH Ïðèìåð ïðîãðàììûÏðåæäå ÷åì ïèñàòü ïðîãðàììó (äðàéâåð), îáåñïå÷èâàþùóþâçàèìîäåéñòâèå êàæäîãî êîìïüþòåðà ñ ïðèíòåðîì, íóæíîñôîðìóëèðîâàòü òðåáîâàíèÿ, ïðåäúÿâëÿåìûå ê ýòîé ïðîãðàììå.Ïðèìåð ïðîãðàììûÏðåæäå ÷åì ïèñàòü ïðîãðàììó (äðàéâåð), îáåñïå÷èâàþùóþâçàèìîäåéñòâèå êàæäîãî êîìïüþòåðà ñ ïðèíòåðîì, íóæíîñôîðìóëèðîâàòü òðåáîâàíèÿ, ïðåäúÿâëÿåìûå ê ýòîé ïðîãðàììå.1.
Âñÿêèé ðàç, êîãäà ïðèíòåð ñâîáîäåí è õîòÿ áû îäèíêîìïüþòåð ñîáèðàåòñÿ îòïðàâèòü äàííûå íà ïå÷àòü,ïðèíòåð áóäåò ðàíî èëè ïîçäíî çàíÿò;Ïðèìåð ïðîãðàììûÏðåæäå ÷åì ïèñàòü ïðîãðàììó (äðàéâåð), îáåñïå÷èâàþùóþâçàèìîäåéñòâèå êàæäîãî êîìïüþòåðà ñ ïðèíòåðîì, íóæíîñôîðìóëèðîâàòü òðåáîâàíèÿ, ïðåäúÿâëÿåìûå ê ýòîé ïðîãðàììå.1. Âñÿêèé ðàç, êîãäà ïðèíòåð ñâîáîäåí è õîòÿ áû îäèíêîìïüþòåð ñîáèðàåòñÿ îòïðàâèòü äàííûå íà ïå÷àòü,ïðèíòåð áóäåò ðàíî èëè ïîçäíî çàíÿò;2. Âñÿêèé ðàç, ïîñëå òîãî êàê ïðèíòåð îêàçàëñÿ çàíÿò, îíäîëæåí êîãäà-íèáóäü ïðèñòóïèòü ê ïå÷àòè;Ïðèìåð ïðîãðàììûÏðåæäå ÷åì ïèñàòü ïðîãðàììó (äðàéâåð), îáåñïå÷èâàþùóþâçàèìîäåéñòâèå êàæäîãî êîìïüþòåðà ñ ïðèíòåðîì, íóæíîñôîðìóëèðîâàòü òðåáîâàíèÿ, ïðåäúÿâëÿåìûå ê ýòîé ïðîãðàììå.1.
Âñÿêèé ðàç, êîãäà ïðèíòåð ñâîáîäåí è õîòÿ áû îäèíêîìïüþòåð ñîáèðàåòñÿ îòïðàâèòü äàííûå íà ïå÷àòü,ïðèíòåð áóäåò ðàíî èëè ïîçäíî çàíÿò;2. Âñÿêèé ðàç, ïîñëå òîãî êàê ïðèíòåð îêàçàëñÿ çàíÿò, îíäîëæåí êîãäà-íèáóäü ïðèñòóïèòü ê ïå÷àòè;3. Êîìïüþòåð, çàâåðøèâøèé ïå÷àòü, äîëæåí êîãäà-íèáóäüîñâîáîäèòü ïðèíòåð;Ïðèìåð ïðîãðàììûÏðåæäå ÷åì ïèñàòü ïðîãðàììó (äðàéâåð), îáåñïå÷èâàþùóþâçàèìîäåéñòâèå êàæäîãî êîìïüþòåðà ñ ïðèíòåðîì, íóæíîñôîðìóëèðîâàòü òðåáîâàíèÿ, ïðåäúÿâëÿåìûå ê ýòîé ïðîãðàììå.1. Âñÿêèé ðàç, êîãäà ïðèíòåð ñâîáîäåí è õîòÿ áû îäèíêîìïüþòåð ñîáèðàåòñÿ îòïðàâèòü äàííûå íà ïå÷àòü,ïðèíòåð áóäåò ðàíî èëè ïîçäíî çàíÿò;2. Âñÿêèé ðàç, ïîñëå òîãî êàê ïðèíòåð îêàçàëñÿ çàíÿò, îíäîëæåí êîãäà-íèáóäü ïðèñòóïèòü ê ïå÷àòè;3.
Êîìïüþòåð, çàâåðøèâøèé ïå÷àòü, äîëæåí êîãäà-íèáóäüîñâîáîäèòü ïðèíòåð;4. Äàííûå íà ïå÷àòü âñåãäà ïåðåäàåò íå áîëåå ÷åì îäèíêîìïüþòåð.Ïðèìåð ïðîãðàììûÏðåæäå ÷åì ïèñàòü ïðîãðàììó (äðàéâåð), îáåñïå÷èâàþùóþâçàèìîäåéñòâèå êàæäîãî êîìïüþòåðà ñ ïðèíòåðîì, íóæíîñôîðìóëèðîâàòü òðåáîâàíèÿ, ïðåäúÿâëÿåìûå ê ýòîé ïðîãðàììå.1. Âñÿêèé ðàç, êîãäà ïðèíòåð ñâîáîäåí è õîòÿ áû îäèíêîìïüþòåð ñîáèðàåòñÿ îòïðàâèòü äàííûå íà ïå÷àòü,ïðèíòåð áóäåò ðàíî èëè ïîçäíî çàíÿò;2. Âñÿêèé ðàç, ïîñëå òîãî êàê ïðèíòåð îêàçàëñÿ çàíÿò, îíäîëæåí êîãäà-íèáóäü ïðèñòóïèòü ê ïå÷àòè;3. Êîìïüþòåð, çàâåðøèâøèé ïå÷àòü, äîëæåí êîãäà-íèáóäüîñâîáîäèòü ïðèíòåð;4.
Äàííûå íà ïå÷àòü âñåãäà ïåðåäàåò íå áîëåå ÷åì îäèíêîìïüþòåð.À êàêèå åùå òðåáîâàíèÿ ðàçóìíî ïðåäúÿâèòü ê íàøåìóäðàéâåðó?Ïðèìåð ïðîãðàììûÄëÿ ñâÿçè ñ ïðèíòåðîì ïðîãðàììèñò ïðåäëîæèë ñíàáäèòüêàæäûé êîìïüþòåð îäíîé è òîé æå ïðîãðàììîéπ : while true doodwait (R=free);R:=busy;output(X,printer );R:=freeÏðèìåð ïðîãðàììûÄëÿ ñâÿçè ñ ïðèíòåðîì ïðîãðàììèñò ïðåäëîæèë ñíàáäèòüêàæäûé êîìïüþòåð îäíîé è òîé æå ïðîãðàììîéπ : while true doodwait (R=free);R:=busy;output(X,printer );R:=freeÝòî ïðîñòàÿ è ðàçóìíàÿ ïðîãðàììà.Íî áóäåò ëè ñèñòåìà êîìïüþòåðîâ, ñíàáæåííûõ ýòîéïðîãðàììîé, âåñòè ñåáÿ â ñîîòâåòñòâèè ñ óêàçàííûìèòðåáîâàíèÿìè?Ïðèìåð ïðîãðàììûÐàññìîòðèì ïàðàëëåëüíóþ êîìïîçèöèþ ýòèõ ïðîãðàììcobeginπ 0 : while truedo wait (R=free); R:=busy; skip; R:=free; odkπ 00 : while truecoenddo wait (R=free); R:=busy; skip; R:=free; odÏðèìåð ïðîãðàììûÌîäåëü Êðèïêå äëÿ ïðîãðàììût (L1 , {R/free})'- iπ0it(L1 , {R/busy })?i(L2 , {R/free})?i(L3 , {R/busy })&?i(L4 , {R/busy })Ïðèìåð ïðîãðàììûÌîäåëü Êðèïêå äëÿ ïðîãðàììû- it'(L01 , free)tiπ0è ïðîãðàììû '- it (L001 , free)(L01 , busy )? 00i(L2 , free)?i?i(L03 , busy )?i(L04 , busy )&ti(L001 , busy )? 0i(L2 , free)π 00(L003 , busy )?i(L004 , busy )&Ïðèìåð ïðîãðàììûÌîäåëü Êðèïêå äëÿ'π 0 k π 00(L0 , L00 , free)- t 1 1$'- i$000000@(L2 , L1 , free) R t(L1 , L2 , free)@t $'@66000R t@ (L2 , L2 , free) @0000 , L00 , busy )000(L3 , L1 , busy ) ? (L2 , L3 , busy ) ?(L(L01 , L00323 , busy )R t?@t$ -t ' t?@ R t(L03 , L003 , busy )@ I(L04 , L00(L0 , L00 , busy )1 , busy ) ??t ?t(L0 , L00 , busy )(L04 , L00t ?t 1 4&%2 , busy ) 2 4(L0 , L00 , busy )ti1 1 (L03 , L004 , busy ) ?(L04 , L00?3 , busy )t - tY%&H*HH (L04 ,L00,busy)4 t H0 , L00H00(L03 , L00,free)(L,free)(L01 , L00(L01 ,?1 - t3 , free) L4 , free)t- t4 1 HH- t ? HHH000000000(L3 , L2 , free) ? ?(L , L , free) (L2 , L4 ,Hfree) ? ?(L02 , L003 , free)H t t - t- t4 2 Àëãîðèòì ÏåòåðñîíàÀ ïîñìîòðèòå íà ïàðàëëåëüíóþ êîìïîçèöèþ ïðîãðàììcobeginπ1 : while truedo h b1 :=true; x:=2i;wait (x=1 ∨ ¬b2 ); skip; b1 :=false;odkπ2 : while truedo h b2 :=true; x:=1i;wait (x=2 ∨ ¬b1 ); skip; b2 :=false;coendodÀëãîðèòì ÏåòåðñîíàÀ ïîñìîòðèòå íà ïàðàëëåëüíóþ êîìïîçèöèþ ïðîãðàììcobeginπ1 : while truedo h b1 :=true; x:=2i;wait (x=1 ∨ ¬b2 ); skip; b1 :=false;odkπ2 : while truedo h b2 :=true; x:=1i;wait (x=2 ∨ ¬b1 ); skip; b2 :=false;coendodÀ ìîãóò ëè çäåñü äâà ïðîöåññà îäíîâðåìåííî îêàçàòüñÿ âêðèòè÷åñêîé ñåêöèè?Ïðèìåð ïðîãðàììûÀ êàê ñôîðìóëèðîâàòü òðåáîâàíèÿïðàâèëüíîñòè?Ïðèìåð ïðîãðàììûÇàäà÷à îá îáåäàþùèõ ôèëîñîôàõÊÎÍÅÖ ËÅÊÖÈÈ 3..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
