WWW.DISSERS.RU

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

   쿡鎖 禎縯依循潗!


Pages:     | 1 |   ...   | 4 | 5 || 7 | 8 |

厥 尿禎蟻吾循杖 靭桎菴 夭嶢惺姚牆謫 溢鴨泣尊循杖 憙涉 ト葺音哀循杖 溢鴨泣 溢蓮 岫潗 鴨診泣預尊循 淳鴨 衆抑策緘 墮禎把: (輕鴨泣尊循杖) [給奧蟻診執 溢鴨泣尊循杖] (잿贍了 釣奧蟻診桎 溢鴨泣尊循杖 述播孼孼猥 竣迹增 溢鴨泣).

쾰 灑音 墮音壯穽設音牆紅 鴨栯軫僥 穽 橓鳥淸魏打 尿禎蟻吾循杖諺 茵鎭茵震特仲撓 溢鴨音 溢蓮 尿禎蟻吾循潗 衆抑策咸 墮禎把: [희衆抑暢茵 茁增諺] (遯鏃贍了荻陝狀 全尿陝猥 茁增諺 穽抑瞬諺紅 張 疾齬荻陝僥) [輕鴨蟻 茁增諺 述調蓮牆酷 鎭鏃妖性 溢鴨泣 疾齬荻陝] (쿡魏裔鎭蟻增脣 疾齬暢荏 竣迹增 茁增諺) [행幽特杖 惟拙焉帙前震 締檣打佺寮荻陝 茁增諺]. 菴牆迹 紳設 修鴨 調葺茵疾外城劃 夭孼狀 憙 墮禎把, 診唯 妖鎭卒釣診打 穽全蹟擾姚壯蟻狀 橓軫緘栯 荀諺孼狀 依燼孺 鎭鏃妖性 依燼特仲謫 穽謫調壹寮荻陝. 헉嚴 蓮 穽外賊嶢 疾陝曾典茵打 前狀純紅 全儼城典荻 穽全蹟擾姚壯蟻狀 橓軫緘栯 荀諺孼狀 依燼孺, 壯晤循諺迹 依燼惟 鴨釣循 述婆衆孼僥 (Computation Tree Logic, 櫛愉晟孼狀 CTL), 日跡嚴軫 幽蹟荻 晤魏 厥鏑謫 [34].

찐諺孼壯 依燼魏 溢蓮 岫潗 前狀脣 靭桎菴 橓鳥淸魏打 述婆衆嶢言茴紅 茁增諺 穽專嚴櫛, 嚴泣 撓 溢悅 穽抑增設嶢 鎭鏃妖性 惟張杷績蕣佃城狀 溢鴨泣. 捏潗 靭桎菴 裔幽妬奄 衆抑策緘. 尿禎蟻吾循杖諺 楫業搖凹惺僚 茁增諺 櫛增設秩 切鏃窓 荀諺孼狀 依燼孺, 穽抑增設陷 全釣鴨音牆酷 寀橓阻鴨杖 檍 締檣打佺寮荻陝僚, 惟桎終 張翟軸怏溢 哀魏裔潗. 毘 切鏃窓 渟釣脣秩 穽鏑謫荻仲猥 幽蹟, 惟桎終 妖鎭卒釣震宗秩 壯 分.

厥 妖鎭卒釣診打 尿禎蟻奧奄 惟張杷績蕣佃城壯 溢鴨蟻 締檣打佺寮荻陝 茁增諺, 禎懿特牆 魏孺-泣灑 翟調吾 了 檍 楫業搖凹惺僚.

3.1. 巾燼魏 鴨釣循 述婆衆孼僥 及葺溢疾夭 切鏃贍茴赤 全釣鴨音杖 依燼孺 鴨釣循 述婆衆孼僥 (愷). 鸞宗攸債 愷- 溢鴨泣 嚴潗 疾迹魏 M=(S,R,P), 宸 S 惟張杷赤 日跡嚴軫 櫛增杖; R S S 訟壯存赤 剪狀袍杖 壯 日跡嚴軫 S, 全釣鴨緘 渟釣軸液 靭輦 櫛增杖麟 (si,sj)R, 嚴泣 憎緘增詢奄 渟釣軸 了 櫛增杖 si 櫛增杖 sj; P 締檣打 壯午成孼 櫛增杖 城佃燮裝 述仲暹顥陝僥. 淃 城佃燮裝 述仲暹顥陝猥 禎杖茵奄 述仲暹顥陝猥 穽全蹟擾姚壯蟻狀 依燼孺.

膠釣鴨泣 日跡嚴軫 愷-切鏃窓. 蹶增 Pa - 日跡嚴軫 城佃燮裝 述仲暹顥陝僥, - 日跡嚴軫 愷-切鏃窓. 警跡嚴軫 全釣鴨奄 衆抑策陷 翟調吾:

1. 及 嚴潗 禎鴦狀蓮增脣 ;

2. 퇸泣 1 , 桎 1 ;

3. 퇸泣 1,2 , 桎 p1&p2 P, ALL(p1,p2) P, SOME(p1,p2) P, POT(p1,p2) P, INEV(p1,p2) P, 宸 ALL, SOME, POT, INEV - 荀諺孼裝 全儼城典.

찐諺孼裝 全儼城典 POT INEV 旬抑孼 秧 蒼尊緘杖 荀諺孼裝 依燼特仲撓 述調蓮杖. 絞 溢身 岫潗 禎懿特裝 了 全儼城典荻 ALL SOME 尿禎蟻吾循杖諺 衆抑策陷 櫛剪狀袍杖: POT(p1,p2), 嚴泣 ~ALL(p1,~p2);

INEV(p1,p2), 嚴泣 ~SOME(p1,~p2).

菴蟻張橒諺 秧 釣贍了惺僚 述袍蒼佃腸執 特執釣 荀諺孼裝 全儼城典荻 旬賊秩 壓 蓴禎溢侁鎭蟻裝 全儼城典 - PRE PRETILDA.

蹶潗 述婆衆孼僥 - 憙 悚仲佺円壯 禎衆抑荻城言茴前潗 櫛增杖 (s0,s1,s2,...), 宸 i (si,si+1) R. 행炡贈 M, s f 堯 櫛愉晟孼狀 s f 蹟壯妬奄, 破 切鏃窓 f 述禎鷹夭 櫛增杖 s 增宗攸債 . 較狀袍杖 全釣鴨奄 衆抑策陷 翟調吾 ( 全釣鴨音杖 p1 2 - 切鏃窓 愷):

1. s p, 嚴泣 城佃燮狀 述仲暹顥陝猥 尿震牆 櫛增杖 s;

2. s ~p, 嚴泣 ~(s p);

3. s p1&p2, 嚴泣 s p1 & s p2;

4.s0 ALL(p1,p2), 嚴泣 秧 魏輦謫 艇震 (s0,s1,...,sk) 述禎鷹奄 衆抑策緘 埰依淳:

i ((0 i k) & j ((0 j < i) sj p1)) si p2.

흡忽 衆荻閃, ALL(p1,p2) 尿震牆 滄音 s 鴨釣循 , 嚴泣 秧 魏輦謫 艇震 , 壯婆壯緘莘 了 滄乙 s, p2 前診奄 尿震牆忽, 禎魏 1 張 增陝奄 依悅忽;

5. s0 SOME(p1,p2), 嚴泣 憎緘增詢奄 艇潗 (s0,s1,...,sk) 診惟, 破 i ((0 i k) & j ((0 j < i) sj p1)) si p.

흡忽 衆荻閃, SOME(p1,p2) 尿震牆 滄音 s0 鴨釣循 , 嚴泣 憎緘增詢奄 艇潗 鴨釣橓 , 壯婆壯陷栯 了 滄乙 s0, 秧 菴牆謫 艇震 尊增齧秩 尿震牆忽, 禎魏 1 張 增陝奄 依悅忽;

6. s0 POT(p1,p2), 嚴泣 憎緘增詢奄 艇潗 (s0,s1,...,sk) 診惟, 破 i ((0 i k) & j ((0 j < i) sj p1)) & si p2.

흡忽 衆荻閃, POT(p1,p2) 尿震牆 滄音 s0 鴨釣循 , 嚴泣 憎緘增詢奄 艇潗, 壯婆壯陷栯 了 滄乙 s0 適陝婆循陷栯 滄音 si, 惟桎尊 尊增齧秩 尿震牆忽 哀 滄乙 si, 2 尿震牆 滄音 si;

7. s0 INEV(p1,p2), ec泣 秧 魏輦謫 艇震 (s0,s1,...,si,...,sk) 述禎鷹奄 衆抑策緘 埰依淳:

i ((0 i k) & j ((0 j < i) sj p1)) & si p2.

흡忽 衆荻閃, INEV(p1,p2) 尿震牆 滄音 s0 鴨釣循 , 嚴泣 秧 魏輦謫 艇震, 壯婆壯緘莘 了 滄乙 s0 適陝婆循緘莘 滄音 si, 尊增齧秩 尿震牆忽 哀 滄乙 si, 2 尿震牆 滄音 si;

8. s PRE (p), 嚴泣 s' (s,s') R & s' p.

흡忽 衆荻閃, PRE(p) 滄音 s 鴨釣循 尿震牆, 嚴泣 憎緘增詢奄 穽檍日凹 滄乙 s, 宸 尿震牆;

9. s PRETILDA (p), 嚴泣 s' (s,s') R s' p.

흡忽 衆荻閃, PRETILDA(p) 滄音 s 鴨釣循 尿震牆, 嚴泣 秧 魏輦謫 穽檍日凹 滄乙 s p 尿震牆.

厥 述婆衆孼僚 切鏃窓 瞬跡孼裝麟 荀諺孼裝麟 全儼城典閃 張翟軸怏溢 全釣鴨潗 櫛增杖, 壯 惟桎終 修涯 穽夭孼潗 灑音 "紳愴適猥" 全儼城典. 及葺溢疾夭 述婆衆孼猥 切鏃窓 s OP1(OP2(p1,p2),OP3(p3,p4)).

膠儼城典 OP1 修鴨 專孼外城劃 壯 櫛增杖 s, 桎 荀諺 魏 全儼城典 OP2 OP3 修涯 專孼外城劃 壯 櫛增杖, 全釣鴨音牆紅 穽 專孼劉 OP1. 잿贍謫料狀, 1 2, 診唯 3 4 修涯 專孼外城劃 壯 櫛增杖, 全釣鴨音牆紅 穽 述婆衆孼僚 OP2 OP3 櫛剪橓秩軫孼狀.

遯鏃窓 述禎鷹夭 增宗攸債 , 嚴泣 憎緘增詢奄 診惟 櫛增杖 s 憙迹 增宗攸債, 破 ,s p. 遯鏃窓 翟緘午成夭 秧 增宗攸債 , 嚴泣 秧 魏輦謫 櫛增杖 s 增宗攸債 鴨栯軫嶢言茴 ,s p. 遯鏃窓 瞬奄 鎭典諺迹, 嚴泣 佺 鴨栯軫嶢言茴 秧 魏輦迹 溢鴨泣 .

3.2. 흡鎭卒釣診打 荀諺孼狀 依燼孺 壯 晤劉 厥鏑謫 驕孼魏 荀諺孼裝 依燼特仲撓 全儼城典荻 前狀述循奄 壯 撓 釣有猝外狀 述婆衆孼僚 尿禎蟻吾循杖諺 晤魏 厥鏑謫. 菴牆佃 綵齬狀 禎櫛訟 秧 憙撓 墮音 尿禎蟻奧奄 橓猝 厥鏑謫 - Arity Prolog, 尿禎蟻奧諺 IBM-櫛筍嚴震荏 屈쫄 [22].

3.2.1. 給贍了惺 POT - 全儼城典 給贍了惺 憙謫 全儼城典 裔菴奄 衆抑策陷 釣有猝外裝 債設張杖諺:

T,s POT(p1,p2), 嚴泣 T,s p2 (p1 & PRE POT(p1,p2)) (3.3) 間輦 愷-切鏃窓 全釣鴨奄 穽抑凹城 厥鏑謫. 遯鏃窓 s PRE p 穽抑增設奄 穽抑凹城佃 pre(p,l,s), 宸 - 愷-切鏃窓, s - 櫛增杖 l - 楫尿適 櫛增杖. 嗜蟻 楫尿魏 櫛增杖 翟卽奄 杖蓮. 較狀袍杖 R 穽抑增設奄 穽抑凹城佃 arc, 穽料諺 arc(s,t,s1) 全釣鴨奄, 破 渟釣軸 t 了靭奄 櫛增杖 s 壯 s1. 쾰 專孼孺 切鏃窓 s p 尿禎蟻奧奄 穽抑凹城 call.

厥鏑謫荻仲 妖鎭卒釣診打 切鏃窓 3.1 全釣鴨奄 魏 pre(P,L,S):-arc(S,T,S1), P=..K, insert(K,[L,S1],P0), P01=..P0, call(P01),!.

膠儼城典 剪遵特杖 "!" 翟晤循奄 妖鎭卒釣診桎 厥鏑謫 尿魏潗 桎蟻惟 渟躁赤 釣袍杖, 嚴泣 佺 憎緘增詢奄.

及葺溢疾夭 釣贍了惺療 債設張杖 3.3, 魏焌緘莘 全儼城典 POT.

厥抑增設夭 菴牆赤 債設張杖 衆抑策緘 切鏃:

T,s POT(p1,p2), 嚴泣 T,s p2 (3.4) T,s POT(p1,p2), 嚴泣 T,s p1 & PRE POST(p1,p2) (3.5) 厥鏑謫荻仲 釣贍了惺 債設張杖 3.4:

pot(P1,P2,L,S):-P2=..T,insert(T,[S],P0),P01=..P0,call(P01),!. (3.6) 厥鏑謫荻仲 釣贍了惺 債設張杖 3.5:

pot(P1,P2,L,S):-P1=..T,insert(T,[S],P0),P01=..P0,call(P01), pre(pot(P1,P2),[S|L],S). (3.7) 蠣 穽鏑謫荻仲猥 幽蹟 3.6 3.7 僖淳循音粧裝 債設張杖 3.4 3.5, 撓 述禎鷹孼猥 壯 穽蟾震劉 張 穽妖前嶢 跡巍齧荏 釣奧蟻診桎.

厥 撓 述禎鷹孼僚 穽迪拯賊嶢 裔打幽外陝猥, 禎仲鏑獪 張脣傲跡狀 全釣鴨泣潗, 岫依 張惟桎尊 櫛增杖 穽迹鴨狀 堯 張. 쥔 謫調杖特杖 鎭典奄料嚴惟 溢鴨泣 秧 了悚縯杖 裔打幽外陝僥 旬賊秩 張惟桎終 謫調杖婆循陷 埰依淳 穽 專孼劉 荀諺孼裝 全儼城典荻.

毘 埰依淳 尿禎蟻奧 楫尿適 櫛增杖 l, 旬抑孼裝 述袍.

爛尿適 l 增尊嶢 軸鴨 專孼孺 菴牆謫 荀諺孼狀莘 全儼城典 櫛鴨阻嶢 槍 穽迹鴨牆酷 櫛增杖. 콧牆酷 埰依淳 釣贍了策秩 禎溢缸 穽抑凹城 outl. 厥抑凹城 outl(s,l) 尿震張, 嚴泣 s 張 瞬奄 凞諺孼桎 楫尿魏 l. 厥鏑謫荻仲赤 全釣鴨音杖 穽抑凹城 outl 衆抑策緘:

outl(S,[]):-!.

outl(S,[S1|L]):-noneg(S,S1), outl(S,L).

宸 noneg(S,S1) - 穽抑凹城, 寀橓阻菴陷, 破 S 張 調純 S1.

noneg(S,S1):-remove(S,S1,[]),!,fail.

noneg(S,S1).

퇸泣 桎 蓮 焌荏 穽抑凹城 pot(p1,p2) 專孼外齧秩 桎 蓮 焌溢 滄音 s, 桎 剪橓 哀飮孼 岫潗 剪鳥稱鎭蟻裝. 毘 埰依淳 穽抑剪荀晟齧 悚仲佺円狀 裔打幽外陝猥. 綵奄佃 謫調杖婆循緘莘 埰依淳 POT全儼城典 全釣鴨奄 衆抑策陷麟 穽鏑謫荻仲夭 幽蹟閃:

pot(P1,P2,L,S):-outl(S,L), P2=..T,insert(T,[S],P0),P01=..P0,call(P01), !.

pot(P1,P2,L,S):-outl(S,L), P1=..T,insert(T,[S],P0),P01=..P0,call(P01), pre(pot(P1,P2),[S|L],S).

3.2.2. 給贍了惺 ALL-全儼城典 給贍了惺 ALL-全儼城典 裔菴奄 衆抑策陷 釣有猝外裝 債設張杖諺:

T,s ALL(p1,p2), 嚴泣 T,s p2 & (~p1 PRETILDA ALL(p1,p2)) (3.8) 遯鏃贍茴赤 全釣鴨音杖 全儼城典 PRETILDA 裔菴狀 切鏃窓迹 3.2.

厥茵 釣贍了惺 憙迹 切鏃窓 壯 晤劉 厥鏑謫 張脣傲跡壯 了-裔 壯泣婆 侑陝桎調 蓴蘖嫂狀增.쾰 疾陝曾典茵打 切鏃窓 3.2 僖淳循音粧腸, 張 櫛鴨阻晟策 侑陝桎 蓴蘖嫂狀增, 脣楫鏑淮暢馹 了橓增裝 櫛剪狀袍杖諺:

x p(x) x p(x) 釣奧蟻診鎭 禎懿妬奄 切鏃窓:

s PRETILDA p, 嚴泣 s' ((s,s') R s' p) 행靭 全儼惺療 夭町凹惺僚 菴牆迹 切鏃窓, 禎懿妬諺 切鏃窓:

s PRETILDA p, 嚴泣 ~s'(s,s') R & (s' p).

毘 切鏃窓 溢蓮 岫潗 壯穽壬 釣贍了荻陝 艇鎭 調繒俺音杖 檍 壯 壓 妬增:

S PRETILDA p CPRETILDA(p,s) CPRETILDA(p,s) 蹟壯妬奄 : s'(s,s') R & (s' p) 厥鏑謫荻仲 妖鎭卒釣診打 憙撓 壓採 述調蓮杖 衆抑策咸:

pretilda(P,L,S):-non(cpretilda(P,L,S)).

cpretilda(P,L,S):-arc(S,T,S1), P=..K,insert(K,[L,S1],P0),P01=..P0, non(P01).

宸 non-穽抑凹城 全釣鴨奄 魏 non(P):-call(P),!,fail.

non(P).

到設張杖 3.8 疾陝曾典麟宗奄 幽姓裔蟻腸 切鏃 穽抑增設奄 切鏃 衆抑策陷 穽鏑謫荻仲撓 幽蹟荻:

all(P1,P2,L,S):- P2=..T,insert(T,[S],P0),P02=..P0,call(P02), P1=..K,insert(K,[S],P00),P01=..P00,non(P01), !.

all(P1,P2,L,S):-P2=..T,insert(T,[S],P0),P02=..P0,call(P02), pretilda(all(P1,P2),[S|L],S).

嶠壯惟 專孼魏 釣有猝外狀莘 債設張杖 3.8 禎溢缸 菴牆紅 幽蹟荻 張脣傲跡壯 旬巍 剪憎秩軫 謫調杖婆循陷 埰依淳.

퇸泣 穽 禎鋌叱 專孼嶢 穽抑凹城 all(p1,p2) 前蔡嚴軫奄 禎蕣典裝 渟釣軸 調張 調葺溢疾孼狀 櫛增杖 s, 桎 菴牆渾 穽抑凹城 張翟軸怏溢 專孼嶢 魏 尿震牆渾 穽焉調震潗 菴蟻張橒策 釣有猝外腸 專孼有 秧 穽抑剪荀晟孼 裔打幽外陝.

쾰 全釣鴨音杖 桎莘, 瞬奄 泣 翟衒攸 凞諺孼桎 楫尿魏, 旬賊嶢 穽抑凹城 inl. 찰調蓮杖 inl(s,l) 蹟壯妬奄, 破 s 瞬奄 凞諺孼桎 楫尿魏 l. 厥鏑謫荻仲赤 全釣鴨音杖 穽抑凹城 inl 衆抑策緘:

inl(X,[Z|Y]):-remove(X,Z,[]),!.

inl(X,[Z|Y]):-inl(X,Y).

희禎蟻奧 穽抑凹城 inl 荏 溢蓮 全釣鴨泣潗 禎艾賊緘 謫調杖婆循緘 埰依淳 菴潗 適佺妬鎭蟻狀 穽鏑謫荻仲赤 全釣鴨音杖 ALL-全儼城典:

all(P1,P2,L,S):-inl(S,L), !.

all(P1,P2,L,S):- P2=..T,insert(T,[S],P0),P02=..P0,call(P02), P1=..K,insert(K,[S],P00),P01=..P00,non(P01), !.

all(P1,P2,L,S):-P2=..T,insert(T,[S],P0),P02=..P0,call(P02), pretilda(all(P1,P2),[S|L],S).

3.2.3. 給贍了惺 崖昌撓 荀諺孼裝 全儼城典荻 給有猝外裝 債設張杖 秧 全儼城典荻 INEV SOME 夭廬 衆抑策陷 淳:

T,s INEV(p1,p2), 嚴泣 T,s p2 (p1 & PRETILDA INEV(p1,p2)).

T,s SOME(p1,p2), 嚴泣 T,s p2 & (p1 PRE SOME(p1,p2)).

滑蓮 穽外賊嶢 穽鏑謫荻仲 釣贍了惺 菴牆紅 全儼城典荻, 盾誼妬 謫調杖婆鎭蟻裝 埰依淳:

inev(P1,P2,L,S):-inl(S,L),!,fail.

inev(P1,P2,L,S):-P2=..K,insert(K,[S],P00),P02=..P00,call(P02), !.

inev(P1,P2,L,S):-arc(S,T,S1), !, P1=..K,insert(K,[S],P0),P01=..P0,call(P01), pretilda(inev(P1,P2),[S|L],S).

some(P1,P2,L,S):-inl(S,L), !.

some(P1,P2,L,S):-P2=..K,insert(K,[S],P0),P02=..P0,call(P02), non(arc(S,T,S1)), !.

some(P1,P2,L,S):-P2=..K,insert(K,[S],P00),P02=..P00,call(P02), P1=..T,insert(T,[S],P0),P01=..P0, non(P01), !.

some(P1,P2,L,S):-P2=..K,insert(K,[S],P0),P02=..P0,call(P02), pre(some(P1,P2),[S|L],S).

袞惟桎終 蒼尊緘杖 滑蓮 穽外賊秩 張惟桎終 蒼尊緘杖 穽抑增設音杖 全儼城典荻 荀諺孼狀 依燼孺. 찌-渟躁紅, 楫尿適 l 尿禎蟻奧奄 桎蟻惟 軸鴨 述禎鷹孼 穽謫調壹. 腦孺 翟調吾, 荀諺孼狀 全儼城典 溢蓮 述晤循潗 悚 尿禎蟻吾循杖 憙謫 檉調靭疾. 衆綵齧 POT-全儼城典, 憙 蒼尊緘杖 全釣鴨奄 衆抑策陷 幽蹟佃:

pot(P1,P2,S):-pot(P1,P2,[],S).

행靭震, 破 壯妬蟻狀 午成孼猥 楫尿魏 l 嚴潗 [], 破 瞬奄 穽了壯惟 艇增謫 楫尿魏.

콧蟻張橒猥 蒼尊緘杖 哀增嵬筬秩 艇鎭 埰疾陝孼 埰依純謫 穽抑凹城 1. 憙佃 衆綵齧 荏 穽抑禎乙侁諺, 破 穽抑凹城 1 夭檍 午成孼猥 "尿震壯" 張惟桎尊 櫛增杖. 콸幽燮惺 憙謫 牒攸 菴奄 衆抑策陷 穽鏑謫荻仲夭 幽蹟佃:

true(S).

쥔奧衆荻裝 POT-全儼城典 夭檍 桎蟻惟 壓 燮身靭粧. 煖愉晟孼猥 燮身靭粧荻 POT-全儼城典 溢蓮 岫潗 裔菴狀 衆抑策陷 幽蹟佃:

pot(P,S):-pot(true,P,[],S).

淃哀殺酷 蒼尊緘杖 溢身 穽夭孼潗 惟 蓴諺 崖昌夭 荀諺孼裝 全儼城典閃.

3.2.4. 給贍了惺 張荀諺孼裝 依燼特仲撓 全儼城典荻 厥 妖鎭卒釣診打 愷-切鏃窓 壯 晤劉 厥鏑謫 張翟軸怏溢 專孼外城 張 桎蟻惟 荀諺孼裝, 狀 張荀諺孼裝 依燼特仲猥 全儼城典.

쾰 憙謫 述調蓮杖 哀飮裝 岫潗 裔炡焌裝 幽姓裔蟻狀 切鏃 渟釣橓鴨裝 穽鏑謫荻仲猥 幽蹟.

滑蓮 穽外賊秩 穽鏑謫荻仲猥 幽蹟 秧 專孼孺 衆抑策陷 張荀諺孼裝 依燼特仲撓 全儼城典荻: 剪鳥稱杖 (NOT), 怏旿檣打 (OR), 惟藏檣打 (AND), 夭町凹惺僚 (IMPLIES), 僖淳循音粧狀增 (EQU):

not(P,S):-P=..T,insert(T,[S],P0),P01=..P0,call(P01), !, fail.

not(P,S).

or(P1,P2,S):-P1=..T,insert(T,[S],P0),P01=..P0,call(P01),!.

or(P1,P2,S):-P2=..T,insert(T,[S],P0),P02=..P0,call(P02).

and(P1,P2,S):-P1=..T,insert(T,[S],P0),P01=..P0,call(P01), P2=..K,insert(K,[S],P00),P02=..P00,call(P02).

implies(P1,P2,S):-P1=..T,insert(T,[S],P0),P01=..P0,call(P01), not(P2,S),!,fail.

implies(P1,P2,S).

equ(P1,P2,S):-P1=..T,insert(T,[S],P0),P01=..P0,call(P01), P2=..K,insert(K,[S],P00),P02=..P00,call(P02), !.

equ(P1,P2,S):-not(P1,S), not(P2,S).

3.3. 희衆抑荻陝猥 遵鎭述 溢鴨音 滑蓮 穽外賊秩 釣奧蟻診執 尿衆抑荻陝僥 遵鎭述 溢鴨音, 調葺溢疾孼裝 紳設 2, 禎溢缸 荀諺孼狀 依燼孺. 찐諺孼壯 依燼魏 述增蒼齧 尊泣 晤魏 全尿陝 哀魏晤循諺紅 竣迹增 茁增諺. 卵抑暢 剪靭震潗, 破 杖蓮 修涯 尿禎蟻吾循潗 桎蟻惟 悚奧衆荻裝 荀諺孼裝 全儼城典. 厥 裔炡茁 切鏃窓 秧 蓴嶪 穽抑凹城荻 修鴨 全埰魏潗 燮身靭粧, 全釣鴨陷 櫛增杖 茁增諺.

3.3.1. 쿡魏裔鎭蟻增脣 竣迹增 遵鎭述 溢鴨音 樂迹增循 遵鎭述 溢鴨音 岫泣 全釣鴨音裝 調醴. 1.2. 쾰 哀魏裔鎭蟻增循 竣迹增 全釣鴨泣 穽抑凹城 enable. 희震牆赤 午成孼猥 述調蓮杖 enable(t,s) 禎魏晤循奄, 破 櫛增杖 s 調嗚予孼 渟釣軸 t.

毘剪 穽抑凹城 尿震張 櫛增杖 s, 嚴泣 憎緘增詢奄 涯侁 了 櫛增杖 s 櫛增杖 s1. 厥鏑謫荻仲赤 全釣鴨音杖 憙謫 穽抑凹城 衆抑策緘:

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

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

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

흡忽 衆荻閃, 渟釣軸 t 鍊脣, 嚴泣 脣 蓴嶪 櫛增杖 遵鎭脣 溢鴨泣, 壯婆壯緘 竣赤 締檣打佺寮荻陝猥 了 壯妬蟻狀莘 櫛增杖, 渟釣軸 t 禎鎭莊歪蟻狀 調嗚予孼.

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

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

퇸泣 壯 裔穽前 live(t) 厥鏑謫-茁增諺 剪橓震 yes, 桎 渟釣軸 t 瞬奄 鍊述. 卵抑暢 裔靭震潗, 破 溢蓮 岫潗 櫛增設音狀 張仲鏑獪 愷찡典壬 秧 穽荻儼孺 竣迹增循 鍊脣增 渟釣軸菴. 腦, 壯穽夭儼, 尿禎蟻吾循杖諺 僖淳循音粧裝 櫛剪狀袍杖, 穽外抑孼裝 調醴. 3.1, 溢身 岫潗 禎懿特裝 衆抑策陷 切鏃窓:

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

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

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

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

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

勒陝曾典麟尊循牆 診孺 翟調吾 愷-切鏃窓 妖鎭卒釣震宗奄 壯 晤劉 厥鏑謫 診:

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

liveness.

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

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

init ALL(enable(t)).

흡忽 衆荻閃, 渟釣軸 t 靭倧述, 嚴泣 脣 蓴嶪 櫛增杖 遵鎭脣 溢鴨泣, 壯婆壯緘 竣赤 締檣打佺寮荻陝猥 了 壯妬蟻狀莘 櫛增杖, 渟釣軸 t 張 調嗚予孼.

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

dead(T):- init(S),implies(init,all(not(enable(T))),S).

Pages:     | 1 |   ...   | 4 | 5 || 7 | 8 |






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

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