WWW.DISSERS.RU

턺駒잃痼 昐탱祿胱痼 좨죄훨瑙各

   쿡鎖 禎縯依循潗!


Pages:     | 1 |   ...   | 5 | 6 || 8 |

퇸泣 壯 裔穽前 dead(t) 厥鏑謫-茁增諺 剪橓震 yes, 桎 渟釣軸 t 瞬奄 靭倧述.

쿡魏裔鎭蟻增脣 桎莘, 破 遵鎭循 溢鴨蟻 瞬奄 靭倧脣, 穽迪譽賊嶢 禎溢缸 衆抑策緘 切鏃窓:

t [init ALL(enable(t))].

행靭 侑陝桎 蓴蘖嫂狀增 侑陝桎尊 憎緘增脣循杖, 禎懿妬諺:

t [(init ALL(enable(t)))].

흡鎭卒釣診打 菴牆迹 切鏃窓 壯 晤劉 厥鏑謫 衆抑策咸:

deadness:- init(S),transition(T), not(implies(init,all(not(enable(T)))),S), !,fail.

deadness.

퇸泣 壯 裔穽前 deadness 厥鏑謫-茁增諺 剪橓震 yes, 桎 尿衆抑暢茵 遵鎭循 溢鴨蟻 瞬奄 靭倧脣.

樂迹增脣 禎鎭莊歪蟻狀 鍊脣增 쾰 哀魏裔鎭蟻增循 桎莘, 破 渟釣軸 t 遵鎭脣 溢鴨泣 禎鎭莊歪蟻狀 鍊脣, 尿禎蟻奧奄 衆抑策咸 愷-切鏃窓:

init POT(ALL(POT(enable(t)))).

흡忽 衆荻閃, 渟釣軸 t 禎鎭莊歪蟻狀-鍊脣, 嚴泣 脣傲跡壯 診魏 茁膣惺, 惟宸 佺 蓴憶菴 夭檍 脣傲跡狀增 增城 調嗚予孼裝. 卵抑暢 剪靭震潗, 破 日跡嚴軫 禎鎭莊歪蟻狀 鍊述 渟釣軸哀 醇賊嶢 日跡嚴軫 埰依純-鍊述 渟釣軸哀, 禎憙佃 禎鎭莊歪蟻狀 鍊脣 渟釣軸 診唯 瞬奄 埰依純-鍊述.

昆 晤劉 厥鏑謫 菴牆 切鏃窓 溢蓮 岫潗 穽迪粧儼穽奄寮荻陝 衆抑策陷 翟調吾:

potlive(T):- init(S),implies(init,pot(all(pot(enable(T)))),S).

퇸泣 壯 裔穽前 potlive(t) 厥鏑謫-茁增諺 剪橓震 yes, 桎 渟釣軸 t 瞬奄 禎鎭莊歪蟻狀 鍊述.

쿡魏裔鎭蟻增脣 桎莘, 破 遵鎭循 溢鴨蟻 瞬奄 禎鎭莊歪蟻狀 鍊脣, 穽迪譽賊嶢 禎溢缸 衆抑策緘 切鏃窓:

t [init POT(ALL(POT(enable(t))))].

행靭 侑陝桎 蓴蘖嫂狀增 侑陝桎尊 憎緘增脣循杖, 禎懿妬諺:

t [(init POT(ALL(POT(enable(t)))))].

흡鎭卒釣診打 菴牆迹 切鏃窓 壯 晤劉 厥鏑謫 衆抑策咸:

potliveness:- init(S),transition(T), not(implies(init,pot(all(pot(enable(t))))),S), !,fail.

potliveness.

퇸泣 壯 裔穽前 potliveness 厥鏑謫-茁增諺 剪橓震 yes, 桎 尿衆抑暢茵 遵鎭循 溢鴨蟻 瞬奄 禎鎭莊歪蟻狀 鍊脣.

콸鎭鏃妖了 汁褻城顥陝 渟釣軸哀 間 衆抑暢 了 穽設堯 締檣打佺寮荻陝 遵鎭 躬疾, 述灑 渟釣軸菴 秧 汁褻城顥陝 了 日跡嚴軫 調嗚予孼裝 渟釣軸哀 張鴨鎭鏃妖寮荻陝.

쾰 張惟桎終 穽堯跡孼僥 遵鎭述 溢鴨音 禎音午 午城, 汁褻城顥齧 泣 惟檣釣帙渾 渟釣軸 釣奧蟻診鎭 鴨鎭鏃妖寮荻陝狀莘 堯 張鴨鎭鏃妖寮荻陝狀莘 述灑調. 콸鎭鏃妖寮荻陝裝 述灑 渟釣軸菴 t 衆綵齧秩 桎 衆綵齧, 惟宸 渟釣軸 t 禎瞬奄 楫尿劉 調嗚予孼裝 渟釣軸哀 泣飇 抑妖增橓牆佃 婆衆. 쾰 全釣鴨音杖 憙謫 竣迹增循 尿禎蟻吾循杖諺 荀諺孼狀 依燼孺 旬抑諺 穽抑凹城 fired. 희震牆赤 午成孼猥 述調蓮杖 fired(t,s) 蹟壯妬奄, 破 穽 汁褻城顥陝僚 渟釣軸菴 t 遵鎭循 溢鴨蟻 渟釣軸怏 櫛增杖 s. 흡忽 衆荻閃, 憎緘增詢奄 櫛增杖 s1, 了 惟桎尊莘 嚴潗 涯侁, 禎靭特牆 渟釣軸哀 t, 橓涯咸 櫛增杖 s. 膠釣鴨泣 菴牆渾 穽抑凹城 壯 晤劉 厥鏑謫 衆抑策陷 翟調吾:

fired(T,S):- arc(S1,T,S).

쾰 哀魏裔鎭蟻增循 桎莘, 破 穽 汁褻城顥陝僚 渟釣軸菴 t 剪憎秩軫暢 張鴨鎭鏃妖寮荻陝裝 述灑, 溢蓮 尿禎蟻吾循潗 衆抑策咸 愷찡典壬乙:

init ALL(enable(t)PRETILDA(fired(t))).

흡忽 衆荻閃, 穽 汁褻城顥陝僚 渟釣軸菴 t 剪憎秩軫暢 張鴨鎭鏃妖寮荻陝裝 述灑, 嚴泣 脣 蓴嶪 櫛增杖 遵鎭脣 溢鴨泣, 壯婆壯緘 竣赤 締檣打佺寮荻陝猥 了 壯妬蟻狀莘 櫛增杖 了 調嗚予孼狀增 渟釣軸菴 t 壯 衆抑策緘 胞愼 蓴憶菴 衆抑暢 憶 汁褻城顥陝猥. 卵抑暢 裔靭震潗, 破 了 櫛增杖 溢蓮 述軸怏潗 桎蟻惟 賊壯 涯侁, 禎靭特牆 渟釣軸哀 t.

昆 晤劉 厥鏑謫 菴牆 切鏃窓 溢蓮 岫潗 穽迪粧儼穽奄寮荻陝 衆抑策陷 翟調吾:

determ(T):- init(S),implies(init,all(implies(enable(T), pretilda(fired(T)))),S).

퇸泣 壯 裔穽前 determ(t) 厥鏑謫-茁增諺 剪橓震 yes, 桎 渟釣軸 t c調蓀執循奄 蓴憶菴 鴨鎭鏃妖寮荻陝狀.

3.3.2. 酪增諺 翟陷麟 釣憎猝閃 膠釣鴨泣, 剪憎秩軫策 泣 茁增諺 了 2- 檉調應言茴紅 穽專嚴櫛, 調醴言陷 檉宗 翟陷 釣憎猝荻 (鳥.2.1), 膣炡孺. 淃 膣炡惟 禎崖暹脹億齧秩 診魏 茁膣惺, 惟宸 杖 賊妖 了 穽專嚴櫛 張 溢蓮 調譽外城劃.

較憎秩軫猥 膣炡惟 瞬奄 賊杖 了 前狀純紅 竣迹增 茁增諺 檉調應言茴忽 穽專嚴焌麟. 쾰 哀魏裔鎭蟻增循 剪憎秩軫 膣炡惟 哀增城展狀 禎魏裔潗, 破 櫛剪橓秩軫策咸 遵鎭循 溢鴨蟻 鍊循.

膠釣鴨泣 穽抑凹城 transition, 尿禎蟻奧諺渾 鎭音 幽蹟 裔莘依盾佃 liveness, 衆抑策陷 翟調吾:

transition(t11).

transition(t12).

transition(t13).

transition(t21).

transition(t22).

transition(t23).

昆 墮音脣 寀橓阻鴨杖 liveness 厥鏑謫-妖鎭卒釣診桎 剪橓妬奄 no, 破 瘡暹顥齧 壯 穽尿寀增淳 調葺茵疾外齧溢 茁增諺 膣炡惟.

3.3.3. 행菴妬 洵殲日謫 尿幽特杖 淃魏蓮, 破 遵鎭循 溢鴨蟻, 穽抑增設音牆 壯 鳥.2.3, 全尿顥齧 裔菴罷 洵殲日謫 尿幽特杖. 間 岫依 剪靭特狀 調醴. 2.2, 賊杖 了 前狀純紅 竣迹增 愉嶢料嚴惟 翟乙增 瞬奄 桎, 破 賊狀荀諺孼狀 張 溢蓮 壯軸怏潗 張 灑音 賊狀莘 穽專嚴焌 (竣迹增脣 洵殲日謫 尿幽特杖). 捺典壬泣宗諺 菴牆赤 疾齬荻陝猥 鎭鏃妖性 遵鎭述 溢鴨音 荀諺孼狀 依燼孺.

膠釣鴨泣 穽抑凹城 crit 衆抑策陷 翟調吾:

crit(I,S):-inlist(cr(I),S).

毘剪 穽抑凹城 尿震張, 嚴泣 禎預打 cr(I) 醇賊嶢 櫛增杖 S.

희震牆赤 午成孼猥 述調蓮杖 crit(I,S) 妖鎭卒釣震宗奄 魏 壯軸輦孼猥 i莘 穽專嚴焌 愉嶢料嚴惟 翟乙增. 尿禎蟻吾循杖諺 憙謫 穽抑凹城 溢悅 壯炡焌潗 衆抑策姮 切鏃窓 荀諺孼狀 依燼孺, 述調縯姮 竣迹增脣 洵殲日謫 尿幽特杖:

init ALL (crit(a) & crit(b)) 堯, 尿禎蟻奧 鎭典諺 鴨涯柚僚, 檍 溢悅 渟釣炡焌潗 淳鴨:

init ALL (crit(a) & crit(b)), 宸 init - 穽抑凹城, 全釣鴨陷 壯妬蟻狀 櫛增杖 茁增諺. 콧牆 切鏃窓 修鴨 尿震牆迹, 嚴泣 脣 蓴嶪 櫛增杖 茁增諺, 壯婆壯 剪 壯妬蟻狀莘, 蓴憶菴 修鴨 述禎鷹潗 衆抑策緘 埰依淳: 禎預打 cr(a) cr(b) 賊狀荀諺孼狀 張 茵簇寮荻陝.



흡鎭卒釣診打 菴牆迹 切鏃窓 壯 晤劉 厥鏑謫 溢蓮 岫潗 衆抑策緘:

implies(init,all(not(and(crit(a),crit(b)))),S).

찰禎鷹孼猥 菴牆謫 墮音脣莘 寀橓阻鴨杖 穽外賊嶢 禎依鍊鎭蟻狀壬 釣奧蟻診膣 (true), 破 溢悅 妖鎭卒釣震尊循潗 魏 壯泣婆 竣迹增循 洵殲日謫 尿幽特杖.

淃魏蓮 述禎鷹孼猥 衆抑策緘莘 疾齬荻陝, 穽抑瞬諺謫 茁增諺 菴牆迹 裔菴特 (重. 調醴. 2.2): "給袍杖 醇跡鴨杖 穽專嚴櫛 撓 愉嶢料嚴孺 翟乙增... 張 剪幽雪顥齧秩 壯 張全釣鴨音牆赤 荀諺, 瞬奄 惟張杷忽 禎 荀諺孼".

쾰 憙謫 全釣鴨泣 穽抑凹城 outside 衆抑策陷 翟調吾:

outside(I,S):-inlist(idle(I),S).

毘剪 穽抑凹城 尿震張, 嚴泣 禎預打 idle(I) 醇賊嶢 櫛增杖 S.

희震牆赤 午成孼猥 述調蓮杖 outside(I,S) 妖鎭卒釣震宗奄 魏 壯軸輦孼猥 i-莘 穽專嚴焌 純 愉嶢料嚴惟 翟乙增. 尿禎蟻吾循杖諺 憙謫 穽抑凹城 溢悅 壯炡焌潗 衆抑策陷 切鏃窓 荀諺孼狀 依燼孺, 述調縯陷 剪靭特牆赤 疾齬荻陝猥:

initALL(outside(a)INEV(crit(a)) initALL(outside(b)INEV(crit(b)).

흡鎭卒釣診打 渟躁迹 了 憙撓 壓採 切鏃窓 壯 晤劉 厥鏑謫 修鴨 衆抑策緘:

implies(init,all(implies(req(a),inev(crit(a)))),S).

찜典 切鏃窓 穽抑增設奄 陝贍謫料裝 翟調吾. 흡鎭卒釣診打 菴牆紅 厥鏑謫-述調蓮杖 禎魏裔乙 撓 尿震牆前潗, 衆抑荻城言茴, 剪靭特牆赤 疾齬荻陝猥 述禎鷹奄.

쿡魏蓮 剪憎秩軫猥 膣炡惟 菴牆迹 茁增諺. 厥抑凹城 transition, 尿禎蟻奧諺渾 鎭音 幽蹟 liveness, 全釣鴨奄 衆抑策陷 翟調吾:

transition(T0):- index(S),tr(T),T0=..[T,S].

index(a).

index(b).

tr(seize).

tr(release).

釣奧蟻診鎭 述禎鷹孼 墮音脣莘 寀橓阻鴨杖 liveness 厥鏑謫妖鎭卒釣診桎 述菴奄 yes (墮蟻 哀增嵬腸診). 헥成嶢 膣炡孺 茁增諺 剪憎秩軫策.

3.3.4. 행菴妬 "翟抑筬陷 淸依櫛憔" 쿡魏蓮 剪憎秩軫猥 茁膣惺僚 莘依厓迹 重儼震 淸依櫛切 (重. 鳥.2.6), 妖成 - 剪憎秩軫猥 膣炡惟.

膠釣鴨泣 穽抑凹城 transition, 尿禎蟻奧諺渾 幽蹟 liveness c音涯陷 翟調吾:

transition(T0):- philosopher(S),tr(T),T0=..[T,S].

philosopher(1).

philosopher(2).

philosopher(3).

philosopher(4).

philosopher(5).

tr(get).

tr(put).

論音脣 寀橓阻鴨杖 liveness 憙佃 衆綵齧 尿震牆, 衆抑荻城言茴, 茁膣惺 莘依厓迹 重儼震 剪憎秩軫暢.

쿡魏蓮 壯泣婆 茁膣惺僚 莘依菴杖 穽抑增設音牆迹 茁增諺, 堯 魏 檍 余 壯晤循, 茁膣惺僚 剪鎭卽孼.

膠釣鴨泣 穽抑凹城 thinking 衆抑策陷 翟調吾:

thinking(I,S):- inlist(think(I),S).

희震牆赤 午成孼猥 述調蓮杖 thinkihg(I,S) 妖鎭卒釣震宗奄 魏 調傲鴻音杖 蓮乙杖 i-莘 淸依櫛牒 禎翟抑城.

膠釣鴨泣 穽抑凹城 eating c音涯陷 翟調吾:

eating(I,S):-inlist(eat(I),S).

희震牆赤 午成孼猥 穽抑凹城 妖鎭卒釣震宗奄 魏 穽齬顥陝猥 i-莘 淸依櫛牒 櫛增杖 禎疾齬音杖 炡陷.

쾰 哀魏裔鎭蟻增循 壯泣婆 剪鎭卽孼僥 穽抑乙侁奄 衆抑策咸 切鏃窓:

i (initALL(thinking(i)INEV(eating(i)))), 尿震牆赤 午成孼猥 惟桎尊 修鴨 竣巍奄言劃軫荻城 壯泣婆 剪鎭卽孼僥.

흡鎭卒釣診打 菴牆迹 切鏃窓 壯 晤劉 厥鏑謫 修鴨 衆抑策緘:

starvation_free:-philosopher(I), not(implies(init,all(implies(req(I),inev(eating(I))))),S),!.

starvation_free:-fail.

昆 裔穽前 starvation_free 厥鏑謫-茁增諺 剪橓震 yes, 破 蹟壯妬奄, 破 茁增諺 夭檍 靭增 茁膣惺 剪鎭卽孼.

3.3.5. 잼莘鳥嫉 洵殲日謫 尿幽特杖 劤 쿡魏蓮 竣迹增脣 洵殲日謫 尿幽特杖. 쭹殲日赤 尿幽特杖 夭檍 靭增, 嚴泣 秧 蓴嶪 循鳥陝桎 締檣打佺寮荻陝 茁增諺, 增燮膣緘 了 壯妬蟻狀莘 櫛增杖, 杖惟宸 張 壯頌菴奄 賊狀荀諺孼狀 壯軸輦孼猥 壓採 滄依 愉嶢料嚴孺 翟乙增.

膠釣鴨泣 穽抑凹城 crit 衆抑策陷 翟調吾:

crit(I,S):- inlist(critical(I,H),S).

희震牆赤 午成孼猥 述調蓮杖 crit(I,S) 妖鎭卒釣震宗奄 魏 壯軸輦孼猥 i-莘 滄乙 愉嶢料嚴惟 翟乙增. 愷-切鏃窓 秧 穽荻儼孺 竣迹增循 洵殲日謫 尿幽特杖 夭檍 淳:

initALL(crit(site_a) & crit(site_b)).

행穽前 mutual_exclusion 秧 穽荻儼孺 瘡暹陝狀莘 竣迹增循 壯 晤劉 厥鏑謫 溢蓮 夭奄 衆抑策陷 淳:

mutual_exclusion:- init(S),implies(init,all(not( and(crit(site_a), crit(site_b)))),S).

쭘抑 墮音脣 寀橓阻鴨杖 mutual_exclusion 特釣 張惟桎尊 荀諺, 厥鏑謫-妖鎭卒釣診桎 述菴增 剪橓 yes, 破 蹟壯妬奄, 破 橓鳥淸打宗諺 茁增諺 翟乙菴奄 竣迹增脣 洵殲日謫 尿幽特杖.

쿡魏蓮 剪憎秩軫猥 頌適寮荻適 劤, 調灑診緘 櫛剪橓秩軫僚 贍莘鳥嫉佃 洵殲日謫 尿幽特杖. 茁增諺 剪憎秩軫策 頌適寮荻孺, 嚴泣 秧 蓴嶪 循鳥陝桎 締檣打佺寮荻陝 茁增諺, 增燮膣緘 了 壯妬蟻狀莘 櫛增杖, 穽 裔穽前 滄乙 壯 醇跡鴨杖 愉嶢料嚴有 翟乙增, 佺 (滄言) 調狀 堯 禎醴狀, 狀 張了悚悅 張 脣藕奄. 쭘抑諺 穽抑凹城 req 衆抑策陷 翟調吾:

req(I,S):- inlist(request(I,J,H),S).

희震牆赤 午成孼猥 述調蓮杖 req(I,S) 妖鎭卒釣震宗奄 魏 莘桎純前潗 蓮乙杖 i-莘 滄乙 脣煜 竣澱 愉嶢料嚴有 翟乙增. 쾰 穽荻儼孺 剪憎秩軫 頌適寮荻適 尿禎蟻奧奄 衆抑策咸 愷-切鏃窓 (秧 滄乙 site_a):

initALL(req(site_a)INEV(crit(site_a)).

쾰 滄乙 site_b 切鏃窓 增尊嶢 陝贍謫料狀. 遯鏃窓寮荻有 櫛剪橓秩軫策緘莘 裔穽前 壯 晤劉 厥鏑謫 溢悅 全釣鴨泣潗 衆抑策陷 翟調吾:

starvation_free:- init(S),implies(init(S),all(implies( req(site_a),inev(crit(site_a)))),S).

昆 裔穽前 starvation_free 厥鏑謫-茁增諺 剪橓妬奄 yes, 破 溢悅 穽迪粧儼穽奄寮荻城 魏 剪憎秩軫猥 頌適寮荻適.





쾰 哀魏裔鎭蟻增循 剪憎秩軫 膣炡惟 全釣鴨泣 穽抑凹城 transition, 尿禎蟻奧諺渾 鎭音 幽蹟 liveness, 衆抑策陷 翟調吾:

transition(T0):- site(S),tr(T),T)=..[T,S].

site(site_a).

site(site_b).

tr(send).

tr(receive).

tr(release).

tr(i_reply).

tr(w_reply).

給奧蟻診執 專孼孺 墮音脣莘 寀橓阻鴨杖 liveness 禎譽鏑 逡言城 述脣, 破 膣炡孺 茁增諺 剪憎秩軫策.

3.3.6. 잼獲儼壯震純-訟桎述 穽剪適鏑 枏嶢齧秩, 破 穽剪適鏑 櫛增設音 惟拙焉帙, 嚴泣 穽 釣贍了惺僚 禎橓鴨杖 茁增諺 剪橓妬奄 衆抑策陷 疾齬荻陝:

1. 較憎秩軫猥 膣炡惟, .. 診孺 櫛增杖, 惟宸 墮蟻 余 張 哀增嵬腸診, 杖 賊妖 翟衒攸 張 溢蓮 了靭杖潗 竣赤莘 櫛增杖.

2. 淃鷹剪 - 蓴 穽抑埰溢疾孼裝 楫業搖凹惺猥 埰依淳, 鴨栯軫 茁膣惺僚 綵鎭裝, 櫛剪橓秩軫策陷 櫛增杖 哀增畏夭.

3. 較憎秩軫猥 悚楫鏑偃裝 裔打幽外陝僥.

4. 袞哀艇增夭前潗 渟釣禎鷹孼僥 - 釣贍了惺 謫調杖特杖 壯 惟泣特增脣 渟釣軸哀 剪鴨蟻裝 櫛增杖, 翟埰依瞬孼裝 楫業搖凹惺猥.

5. 煖剪橓秩軫猥 鎭鏃妖贍茴紅 櫛增杖 禎增設音牆忽 楫業搖凹惺 墮.

毘 潗 埰依淳 全釣鴨 翟姮 惟拙焉帙前潗, 禎仲鏑獪 蓴 穽剪適鏑 翟裔鎭蟻狀 哀飮裝 昶荻音軫典潗 憙夭 埰依淳. 憾佃 翟緘 惟拙焉帙前震 秧 魏輦謫 惟檣釣帙謫 震檉 穽剪適鏑荻 憎緘增詢奄 妬增壯 惟拙焉帙前潗, 翟埰依瞬孼壯 楫業搖凹迹 穽剪適鏑. 魏特增橓 埰依淳, 全釣鴨陷 妬增腸 惟拙焉帙前潗 읒-穽剪適鏑, 溢悅 述鴨泣潗, 壯穽夭儼, 衆抑策陷: "遽杖 張 哀飮壯 渟釣菴循潗 灑音 特 賊妖 魏崖 賊狀荀諺孼狀", "躬釣菴迭凹 溢蓮 壯軸怏潗 泣灑 櫛增杖 莘桎純前震, 泣灑 櫛增杖 跡巍陝 禎曖橓阻鴨杖, 狀 張 翟迪 汁暹".

쿡魏蓮 翟姮 惟拙焉帙前潗 읒-穽剪適鏑. 쾰 憙謫 哀魏蓮, 破 遵鎭循 溢鴨蟻, 穽抑增設音牆 壯 鳥.2.11, 鍊循.

膠釣鴨泣 穽抑凹城 transition, 尿禎蟻奧諺渾 鎭音 幽蹟 liveness, 衆抑策陷 翟調吾:

transition(T0):- bit(S),tr(T),T0=..[T,S].

bit(zero).

bit(one).

tr(tsend).

tr(recack).

tr(propagate).

tr(repeata).

tr(reception).

tr(loss).

tr(repeatm).

昆 寀橓阻鴨杖 liveness 厥鏑謫-妖鎭卒釣診桎 剪橓妬奄 yes, 衆抑荻城言茴, 읒-穽剪適鏑 翟緘 惟拙焉鎭.

淃魏蓮 述禎鷹孼猥 埰依淳 妬增狀 惟拙焉帙前震, 櫛紳葉狀 惟桎尊壬 泣杖 張 哀飮壯 渟釣菴循潗 灑音 特 賊妖 魏崖 賊狀荀諺孼狀. 흔 遵鎭脣 溢鴨泣 壯 鳥.2.11 淳厓, 破 汁抑 渟釣菴婆 全釣鴨奄 禎預打麟 send receive. 璥簇寮荻魏 誼灑 了 憙撓 禎預打 蹟壯妬奄 壯軸輦孼猥 汁抑 渟釣菴婆 魏崖(荻). 羸衆 魏崖荻 汁抑 渟釣菴婆 全釣鴨奄 魏 M(send) + M(receive), 宸 締檣打 菴牆佃 衆綵齧 增設嶢 櫛剪橓秩軫猥 禎預打 遵鎭脣 溢鴨泣 婆衆孼狀 午成孼猥 茵簇寮荻孺. 刀佃腸桎 疾齬荻陝猥 鎭鏃妖性 遵鎭脣 溢鴨泣 切鏃窓寮暢秩 衆抑策陷 翟調吾: 蓴憶菴 哀飮狀 述禎鷹潗 張調橓章軫:

0 M(send)+M(receive) 1.

C 尿禎蟻吾循杖諺 荀諺孼狀 依燼孺 菴牆赤 埰依淳 溢蓮 岫潗 述調蓮狀 淳鴨 衆抑策緘 切鏃窓:

initALL(M(send)=0 & M(receive)= M(send)=0 & M(receive)= M(send)=1 & M(receive)=0).

찰調預 菴牆策 切鏃窓 壯 晤劉 厥鏑謫. 쭘抑諺 穽抑凹城 num(E,N,L) 秧 全釣鴨音杖 N - 婆衆 醇跡鴨杖 凞諺孼診 E 楫尿適 L, 衆抑策陷 翟調吾:

num(E,0,[]).

num(E,N,[E|R]):-num(E,N1,R), N is N1+1.

num(E,N,[F|R]):-num(E,N,R).

尿禎蟻吾循杖諺 菴牆謫 穽抑凹城 述袍穽外抑孼壯 愷-切鏃窓 穽抑增設奄 壯 晤劉 厥鏑謫 衆抑策陷 翟調吾:

implies(init,all(or(or(and(num(send(_,_,_),0), num(receive(_,_,_),0)),and(num(send(_,_,_),0), num(receive(_,_,_),1))),and(num(send(_,_,_),1), num(receive(_,_,_),0)))),S).

콧牆赤 寀橓阻鴨杖 哀增嵬齧秩, 衆抑荻城言茴, 剪靭特牆赤 埰依淳 述禎鷹奄.

淃魏蓮 述禎鷹孼猥 埰依淳 妬增狀 惟拙焉帙前震 읒-穽剪適鏑, 櫛紳葉狀 惟桎尊壬 渟釣菴迭凹 溢蓮 壯軸怏潗 泣灑 櫛增杖 莘桎純前震, 泣灑 櫛增杖 跡巍陝 禎曖橓阻鴨杖 (狀 張 翟迪 汁暹). 間 岫依 剪靭特狀 調醴.2.5, 埰依淳 M(send)=1 妖鎭卒釣震宗奄 魏 壯軸輦孼猥 渟釣菴迭凹 櫛增杖 莘桎純前震, M(wait)=1 - 櫛增杖 跡巍陝 禎曖橓阻鴨杖. 鎭鏃妖性 遵鎭述 溢鴨音 菴牆赤 埰依淳 惟拙焉帙前震 溢蓮 岫潗 曾典壬泣尊循狀 衆抑策陷 翟調吾:

蓴憶菴 哀飮狀 述禎鷹潗 調橓章軫:

M(psend)+M(wait)=1.

흡忽 衆荻閃, 禎預打 psend wait 翟調奧 妖循鳥陝.

遯鏃窓 荀諺孼狀 依燼孺, 穽抑增設咸 菴牆赤 寀橓阻鴨杖, 衆抑策咸:

initALL(M(psend)=0 & M(wait)= M(psend)=1 & M(wait)=0)).

흡鎭卒釣診打 菴牆迹 切鏃窓 壯 晤劉 厥鏑謫 衆抑策咸:

implies(init(all(or(and(num(psend(_),0),num(wait(_),1)), and(num(psend(_),1),num(wait(_),0)))),S).

콧牆赤 墮音脣 寀橓阻鴨杖 哀增嵬齧秩, 衆抑荻城言茴, 剪靭特牆赤 埰依淳 述禎鷹奄.

厥荻儼夭 尿震牆前潗 衆抑策緘莘 寀橓阻鴨杖: " 誼灑 衆綵齧 渟釣菴牆渾 魏崖 調狀 堯 禎醴狀, 狀 張了悚悅 禎曖橓遭嶢". 쾰 憙謫 全釣鴨泣 穽抑凹城 sended confirmed.

sended(S):-inlist(wait(B),S).

confirmed(S):-inlist(psend(B),S).

희震牆前潗 渟躁謫 穽抑凹城 瘡暹顥齧 壯 桎, 破 魏崖 渟釣菴, 蕣典謫 - 壯 桎, 破 穽抑或蔡僥 渟釣菴牆渾 魏崖 禎曖橓阻鴨.

遯鏃窓 荀諺孼狀 依燼孺, 穽抑增設咸 菴牆赤 寀橓阻鴨杖, 裔炡證循奄 衆抑策陷 翟調吾:

initALL(sendedINEV(confirmed)).

昆 晤劉 厥鏑謫 菴牆 切鏃窓 妖鎭卒釣震宗奄 衆抑策陷 翟調吾:

implies(init,all(implies(sended,inev(confirmed)))),S).

厥 專孼劉 菴牆謫 寀橓阻鴨杖 修鴨 禎懿特 依悅渾 釣奧蟻診.

Pages:     | 1 |   ...   | 5 | 6 || 8 |










2011 www.dissers.ru - チ嚴町城壯 凞焉疾佺壯 訟頌姚鎭魏

璥鎭鳥贍 憙謫 焌煜 調傲余孼 秧 蹟壯惟佾孼, 蓴 穽設 穽妖雪音縯 撓 設桎調.
퇸泣 찰 張 櫛紳葉裝 鎭, 破 쭌 茵鎭鳥贍 調傲余명 壯 憙佃 焌煜, 禎縯懿栯診, 壯炡鋪鎭 壯, 荏 鎭特杖 1-2 調灑婆 厓彦 昶贍夭 憶.