?

基于Petri網局部性的極大沖突集枚舉算法

2016-11-17 05:43劉顯明
電子學報 2016年8期
關鍵詞:枚舉庫所等價

潘 理,鄭 紅,劉顯明,楊 勃

(1.湖南理工學院信息與通信工程學院,湖南岳陽 414006;2.華東理工大學信息科學與工程學院,上海 200237;3.江西省電力公司信息通信分公司,江西南昌 330077)

?

基于Petri網局部性的極大沖突集枚舉算法

潘 理1,鄭 紅2,劉顯明3,楊 勃1

(1.湖南理工學院信息與通信工程學院,湖南岳陽 414006;2.華東理工大學信息科學與工程學院,上海 200237;3.江西省電力公司信息通信分公司,江西南昌 330077)

沖突是Petri網研究的重要主題.目前Petri網沖突研究主要集中于沖突建模和沖突消解策略,而對沖突問題本身的計算復雜性卻很少關注.提出Petri網的沖突集問題,并證明沖突集問題是NP(Non-deterministic Polynomial)完全的.提出極大沖突集動態枚舉算法,該算法基于當前標識的所有極大沖突集,利用Petri網實施局部性,僅計算下一標識中受局部性影響的極大沖突集,從而避免重新枚舉所有極大沖突集.該算法時間復雜度為O(m2n),m是當前標識的極大沖突集數目,n是變遷數.最后證明自由選擇網、非對稱選擇網的極大沖突集枚舉算法復雜度可降至O(n2).極大沖突集枚舉算法研究將為Petri網沖突問題的算法求解提供理論參考.

Petri網;沖突集問題;NP(Non-deterministic Polynomial)完全性;極大沖突集枚舉算法

電子學報URL:http://www.ejournal.org.cn DOI:10.3969/j.issn.0372-2112.2016.08.013

1 引言

沖突是Petri網理論的重要概念.沖突的本質是資源競爭[1].當多個沖突變遷競爭有限資源,若其中一個獲得資源,其它與之沖突的變遷就會喪失使能.若變遷集合中的任意兩個變遷都是沖突的,稱這個集合為沖突集.現有Petri網沖突研究主要集中于沖突處理策略和沖突問題建模.經典Petri網采用不確定選擇策略處理變遷沖突[2];優先級Petri網通過設置優先級來解決沖突[3];時間Petri網則利用時間競爭來處理變遷之間的沖突[4];謂詞/變遷網通過謂詞來控制沖突變遷的實施[5];隨機Petri網則引入某種實施概率分布來處理變遷間的沖突[6,7].在建模方面,近期Zeng等利用Petri網方法探討應急響應過程中資源沖突偵測和消解[8];Tian等利用時間Petri網的時間約束特性處理實時系統的沖突問題[9];Popescu等利用Petri網方法解決面向服務制造系統調度過程中的資源沖突[10].

上述研究注重沖突問題建模及沖突消解策略,而對沖突問題本身的計算復雜性卻很少關注.現實系統中的沖突情況往往非常復雜,枚舉系統的極大沖突集,對于全面了解系統沖突、尋求沖突消解方案是非常重要的.因此,對沖突集問題復雜度進行界定,并提出基于Petri網特征的枚舉算法,將為Petri網沖突問題的計算求解提供一種探索途徑.目前已有大量文獻研究Petri網的死鎖問題、活性問題、可達性問題、合法實施序列問題、合成問題、步問題等,得出了一系列有價值的計算復雜性結論[11-16].但這些結論并沒涉及沖突集問題.本文嘗試以沖突集問題為研究對象,通過從已知NP完全問題歸約到沖突集問題,證明沖突集問題的NP完全性;然后利用Petri網實施的局部性特征,提出動態枚舉算法,降低極大沖突集枚舉的計算成本,為沖突集問題的復雜性研究提供有益參考.

2 沖突集問題

2.1 基本定義

用N表示自然數集{0,1,2,…},用Z+表示正整數集.

定義1[1]一個Petri網是一個四元組Σ=(P,T,F,M0),其中:

(1)P是庫所集;(2)T是變遷集,且P∩T=?;(3)F?(P×T)∪(T×P)是流關系;(4)M0:P→N是初始標識.

標識M可表示為一個|P|元向量,第i個元素表示庫所pi中的令牌數.流關系F可表示為特征函數的形式,即F:(P×T)∪(T×P)→{0,1}.用·p={t|(t,p)∈F}和p·={t|(p,t)∈F}表示庫所p的輸入變遷集和輸出變遷集;類似的,用·t和t·表示變遷t的輸入庫所集和輸出庫所集.

定義2[1]一個變遷t∈T在標識M是使能的,當且僅當?p∈P,F(p,t)≤M(p).用En(M)表示標識M下所有使能變遷的集合.

定義3[1]如果tf在標識M是使能的,那么tf可以實施并產生一個新的后繼標識M′,且?p∈P,M′(p)=M(p)-F(p,tf)+F(tf,p).

定義4[1]給定t1,t2∈En(M),若?p∈P,使F(p,t1)+F(p,t2)>M(p),則稱變遷t1和t2在標識M是(有效)沖突的,用t1Mt2表示.

定義5 給定一個變遷集U?T,如果?t1,t2∈U,有t1Mt2,則U是標識M的一個沖突集.若不存在其它沖突集U′,使U?U′,則稱U是M的極大沖突集.用MCS(M)表示在標識M下的所有極大沖突集的集合.

2.2 沖突集問題

定義6[17]復雜類P表示用確定型圖靈機在多項式時間內可解決的判定問題集,NP表示用非確定型圖靈機在多項式時間內可解決的判定問題集.

定義7[17]若判定問題A屬于NP,且所有其它NP問題都能多項式時間多一歸約到A,則稱A是NP完全的.

引理1[17]對于判定問題A,若存在NP完全問題B,使B多項式時間多一歸約到A,則A是NP困難的.若A是NP困難的且A∈NP,則A是NP完全的.

定義8 (沖突集問題,CS)給定Petri網Σ=(P,T,F,M0),標識M∈RS(M0)和正整數k≤|T|,問在標識M是否包含變遷數至少為k的沖突集?

接下來,通過從已知NP完全問題(團問題)歸約到沖突集問題,來證明沖突集問題的NP完全性.

設G=(V,E)是簡單無向圖,這里V是頂點集,E是邊集.給定一個頂點子集A?V,用G(A)表示由A誘導的子圖.

定義9[18]給定圖G=(V,E),如果?u,w∈V,有(u,w)∈E,則稱G是完全的.若G(Q)是完全圖,則稱Q是G的一個團.

定義10[18](團問題,CLIQUE)給定簡單無向圖G=(V,E)和正整數k≤|V|,問G是否包含基數至少為k的團?

引理2[18]團問題是NP完全的.

定理1 沖突集問題是NP完全的.

證明 (1)首先證明沖突集問題是NP困難的.

考慮從團問題多項式時間多一歸約到沖突集問題.設簡單無向圖G=(V,E)和正整數s是團問題的一個實例,要構造沖突集問題的一個實例:Petri網Σ、標識M和正整數k,使Σ在標識M有一個大小至少為k的沖突集當且僅當G有一個大小至少為s的團.按照下面的方式進行構造:

(ⅰ)vi∈V當且僅當ti∈T,即Petri網Σ中的每個變遷t1,t2,…,tn對應圖G中的每個頂點v1,v2,…,vn.

(ⅱ)(vi,vj)∈E當且僅當pij∈P∧M(pij)=1∧F(pij,ti)=1∧F(pij,tj)=1.換句話說,兩頂點vi和vj相鄰當且僅當ti與tj共享輸入庫所pij,庫所pij中放置1個令牌,且弧(pij,ti)和(pij,tj)的權值均為1.

(ⅲ)vi是孤立點當且僅當pi∈P∧M(pi)=1∧F(pi,ti)=1.即vi是孤立點當且僅當ti有一個輸入庫所pi,庫所pi中放置1個令牌,且弧(pi,ti)的權值為1.

(ⅳ)k=s.

從上面構造可以看出,Petri網Σ的每個變遷對應圖G的每個頂點,且每個變遷在M都使能;兩個變遷共享一個庫所當且僅當圖G中對應的兩個頂點是相鄰的.如圖1(a)所示,圖G有4個頂點v1,v2,v3,v4,其中包含一個s=3的團{v1,v2,v3}.通過上述構造得到Petri網Σ和標識M,如圖1(b)所示,Σ有4個變遷t1,t2,t3,t4,4個庫所p12,p13,p23,p4,每個庫所中都有1個令牌,4個變遷均使能.容易看出,Petri網Σ在M包含一個k=3的沖突集{t1,t2,t3}.

現在證明Petri網Σ在標識M有一個大小至少為k的沖突集當且僅當G有一個大小至少為s的團.Q是G的一個團且|Q|≤s,當且僅當?vi,vj∈Q,(vi,vj)∈E;由上面構造步驟,當且僅當得到對應的變遷集U,|U|=|Q|,U?En(M)且?ti,tj∈U,F(pij,ti)+F(pij,tj)>M(pij);即U在標識M是一個沖突集且|U|≤k.

進一步分析這是一個多項式時間的構造.設|V|=n,則V,E和k的輸入長度分別為O(n),O(n2)和O(n),故實例的輸入總長度是O(n2).構造步(ⅰ)根據頂點集V確定變遷集T,故|T|=n;構造步(ⅱ)和(ⅲ)根據邊集E確定庫所集P,故|P|=O(n2);標識M的規模是|P|=O(n2),流關系F的規模是|P‖T|=O(n3).因此整個構造需時間O(n3),即從CLIQUE能多項式時間歸約到沖突集問題.由于CLIQUE是NP完全的(引理2),根據引理1,沖突集問題是NP困難的.

(2)證明沖突集問題屬于NP.

對于Petri網Σ,對任何標識M∈RS(M0),給出一個驗證沖突集問題的非確定型算法(見算法1).

假設|P|=m,|T|=n.則P,T,F,M和k的長度分別是O(m),O(n),O(mn),O(m)和O(n),故輸入的總長度是O(mn).U的長度是O(n),驗證(ⅰ)需時間O(n),驗證(ⅱ)需時間O(mn2),故驗證(ⅰ)和(ⅱ)需時間O(mn2).這是一個能在多項式時間內驗證沖突集問題的非確定型算法.因此沖突集問題屬于NP.

綜合(1)和(2)的證明,根據引理1,沖突集問題是NP完全的.證畢.

3 極大沖突集枚舉算法

3.1 極大沖突集枚舉問題

定義11[17]復雜類FP表示用確定型圖靈機在多項式時間可解決的函數問題集.

定義12 (極大沖突集枚舉問題)給定Petri網Σ=(P,T,F,M0)和標識M∈RS(M0),求Petri網Σ在標識M的所有極大沖突集.

Petri網的極大沖突集枚舉問題,可以使用已有的極大團枚舉算法來求解.不幸的是,極大團枚舉問題是一個已知的NP困難問題.求解這個問題最有效的算法是由Bron和Kerbosch提出的分支限界算法[19],文獻[20]證明這種算法在最壞情況下的時間復雜度為O(nn/3).幸運的是,Petri網的實施具有局部性特征.每一次變遷實施僅僅改變與該變遷相關的前集和后集.因此,每一次變遷實施之后,并不需要重新生成所有的極大沖突集,而只需考慮受實施變遷局部環境影響的那些極大沖突集,這無疑將降低極大沖突集枚舉問題的計算復雜度.3.2 極大沖突集枚舉算法

接下來討論極大沖突集枚舉問題的算法求解.為了簡化算法描述,我們假設Petri網是安全的.用MCS(M,ti)表示在標識M下包含變遷ti的極大沖突集的集合.進一步,用MCS(M,S)表示包含S中所有變遷的極大沖突集的集合,即這些極大沖突集均包含變遷子集S.

Petri網變遷實施可分為兩步,第一步根據流關系,從變遷的輸入庫所中取出相應數量的令牌;第二步根據流關系,將相應數量的令牌放置到變遷的輸出庫所.第一步可能使某些原來沖突的變遷變為不沖突,第二步可能新增一些沖突關系.下面根據影響沖突關系變化的兩個步驟,定義兩個相應的基本操作:

(1)操作del(M,t):執行M-F(·,t),刪除不再沖突的關系;(2)操作add(M,t):執行M-F(·,t)+F(t,·),添加新的沖突關系.

用Dis(M,t)=En(M)En(M-F(·,t))在標識M實施t后喪失使能的變遷集.操作del(M,t)如算法2所示.對標識M下的每個極大沖突集c,在標識M-F(·,t),若c包含非使能變遷,則刪除非使能變遷.再判斷c是否包含在其它極大沖突集中,若包含,則說明c不是標識M-F(·,t)的極大沖突集,刪除c.

設|T|=n,|MCS(M)|=m.變遷t的實施通常只會影響少量極大沖突集,但最壞情況下,可能涉及絕大多數極大沖突集.因此,求解MCS(M,c)通常需O(n),但最壞情況下需O(mn).若循環m次,則該操作的時間復雜度通常為O(mn),最壞情況下為O(m2n).

用Newly(M,t)=En(M′)En(M-F(·,t))表示在新標識M′=M-F(·,t)+F(t,·)新使能的變遷集合.操作add(M,t)如算法3所示.對每個新使能的變遷ti,若ti不與任何極大沖突集相沖突,則ti獨自構成極大沖突集;若ti與某個極大沖突集c的所有變遷沖突,則ti并入c;若ti與極大沖突集c的部分變遷沖突,且這部分變遷不是其它極大沖突集的子集,則ti與部分變遷構成新的極大沖突集.

設|T|=n,|MCS(M)|=m,|Newly(M,t)|=k.外層for循環k次,內層for循環m次,內層循環體通常需O(n);最壞情況下變遷實施影響多數極大沖突集,則需O(mn).故整個算法通常情況需O(kmn),最壞情況下需O(km2n).極大沖突集動態枚舉算法enum(M,t)如算法4所示,算法思路如下:若在標識M實施變遷t,首先使用del(M,t)從所有極大沖突集中刪除喪失使能的變遷,計算得到標識M-F(·,t)的極大沖突集;然后在標識M-F(·,t)+F(t,·),對所有新增使能變遷,使用add(M,t)添加新的沖突關系,得到新標識下所有極大沖突集.

由于新使能變遷數k通常遠小于變遷數n,根據del和add操作的復雜度分析,極大沖突集動態枚舉算法的時間復雜度通常情況為O(mn),最壞情況下需O(m2n).下面舉例說明極大沖突集動態枚舉算法.如圖2所示.

在初始標識M0=(1 1 1 0 1 0),En(M0)={t1,t2,t3,t4,t7},使用add(M0,λ)得到MCS(M0)={{t1,t2},{t2,t3},{t4},{t7}},這里λ是空變遷.

4 特殊子問題

下面介紹三種典型的特殊子網:自由選擇網、擴展自由選擇網和非對稱選擇網.

定義13[2]給定Petri網Σ=(P,T,F,M0),且所有弧的權值為1.

已經證明,這三種子網具有包含關系:FC?EFC?AC[7].因此,從AC獲得的結論,對FC和EFC仍是有效的.定義變遷集T上的結構沖突關系R={(t1,t2)∈T2|·t1∩·t2≠?}.

定理2 對于非對稱選擇網,結構沖突關系R是等價關系.

證明 ?t∈T,有·t∩·t≠?,即(t,t)∈R,故R是自反的.

?t1,t2∈T,若(t1,t2)∈R,即·t1∩·t2≠?,則·t2∩·t1≠?,即(t2,t1)∈R,故R是對稱的.

因此R是等價關系.證畢.

用[t]={t(|t∈T∧(t,t′)∈R}表示t關于R的等價類.

定理3 若t是AC的一個變遷,則?p∈·t,使p·=[t].

證明 根據AC的定義,?p′,P∈·t,有p′·?p·或p·?p′·,故?是一個全序關系.由于·t是有限集,故必有最大元,不妨設為p·.又?ti∈ [t],有·t∩·ti≠?,不妨設pi∈·t∩·ti,于是t∈p·∩pi·,故pi·?p·或p·?pi·.由于p·是·t上關于?的最大元,即有pi·?p·,故得ti∈p·.于是p·? [t].

假設?ti∈p·但ti[t],則有p∈·t∩·ti,即(t,ti)∈R,于是有ti∈[t],矛盾.因此,p·= [t].證畢.

依據等價關系R,可以將變遷集劃分成互不相交的子集,每個子集就是一個等價類.因此,每個變遷僅屬于一個等價類.

定理4 若t∈En(M),則(·t)·∩En(M)是極大沖突集.

證明 由定理3可知,(·t)·是t關于R的等價類[t],即等價類中的變遷相互沖突,因此(·t)·∩En(M)是沖突集;又[t]中變遷不屬于任何其他等價類,因此(·t)·∩En(M)是極大沖突集.證畢.

定理5 對于非對稱選擇網,求解極大沖突集枚舉問題的時間復雜度為O(n2),這里|T|=n.

證明 非對稱選擇網的極大沖突集枚舉算法如算法5所示.首先算法初始化MCS(M)為空集.然后求出每個變遷的關于有效沖突關系R的等價類,每個等價類即為一個極大沖突集.

先證明算法的正確性.

(ⅰ)由于En(M)是有限集,故for循環的次數是有限的.它根據等價類產生極大沖突集,因此for循環執行完成后,極大沖突集的數目不超過|En(M)|.因此算法一定會終止.

(ⅱ)根據定理4,對任何ti∈En(M),(·ti)·∩En(M)是一個極大沖突集.由定理2和定理3可知,根據沖突關系R,可以將En(M)中所有變遷劃分到不同的等價類(極大沖突集),且每個使能變遷對應一個等價類(極大沖突集).在循環過程中,每得到一個等價類,就會從En(M)中刪除該等價類中所有變遷,因此,不會出現重復的極大沖突集.因此算法最終返回的MCS(M)一定包含所有極大沖突集.

再分析算法的復雜性.設|T|=n.循環次數不超過n,每次循環需時間O(n),因此整個算法需時間O(n2).證畢.

5 結論

沖突的本質是系統資源的競爭,對沖突問題的研究是Petri網的重要主題之一.本文提出Petri網的沖突集問題,并利用Petri網的實施局部性,提出極大沖突集枚舉動態算法.文章的主要結論有:(1)Petri網的沖突集問題是NP完全的;(2)所提極大沖突集枚舉算法的時間復雜度為O(m2n),其中m是當前標識的極大沖突集數目,n是變遷數;(3)極大沖突集枚舉問題對自由選擇網、非對稱選擇網的復雜度為O(n2).下階段工作將運用上述研究結論,探索混合語義時間Petri網模型的調度策略[21],處理調度過程中面臨的資源沖突問題,并應用于柔性制造系統、工作流系統的調度問題研究.

[1]Girault C,Valk R.Petri Nets for Systems Engineering:A Guide to Modeling,Verification,and Applications[M].Berlin:Springer-Verlag,2013.

[2]Murata T.Petri nets:Properties,Analysis and Applications[J].Proceedings of the IEEE,1989,77(4):541-580.

[3]Yen H C.Priority conflict-free Petri nets[J].Acta informatica,1998,35(8):673-688.

[4]Merlin P M,et al.Recoverability of communication protocols-Implications of a theoretical study[J].IEEE Transactions on Communications,1976,24(9):1036-1043.

[5]Genrich H J.Predicate/Transition Nets[M].Berlin:Springer-Verlag Petri Nets:Central Models and Their Properties,1987.

[6]林闖.隨機 Petri 網和系統性能評價[M],北京:清華大學出版社,2009.

[7]Balbo G.Introduction to Stochastic Petri Nets[M].Berlin:Springer-Verlag Lectures on Formal Methods and PerformanceAnalysis,2001.

[8]Zeng Q,Liu C,Duan H.Resource conflict detection and removal strategy for nondeterministic emergency response processes using Petri nets[J].Enterprise Information Systems,2015:1-22.

[9]Tian Z,Zhang Z D,Ye Y D,et al.Analysis of real-time system conflict based on fuzzy time Petri nets[J].Journal of Intelligent & Fuzzy Systems:Applications in Engineering and Technology,2014,26(2):983-991.

[10]Popescu C,Soto M C,Lastra J L M.A Petri net-based approach to incremental modelling of flow and resources in service-oriented manufacturing systems[J].International Journal of Production Research,2012,50(2):325-343.

[11]Cheng A,et al.Complexity results for 1-safe nets[J].Theoretical Computer Science,1995,147(1-2):117-136.

[12]Esparza J.Reachability in live and safe free-choice Petri nets is NP-complete[J].Theoretical Computer Science,1998,198(1):211-224.

[13]Esparza J.Decidability and Complexity of Petri Net Problems—an Introduction[M].Berlin Heidelberg Springer:Lectures on Petri Nets I:Basic Models,1998:374-428.

[14]Jiang C.Polynomial-time algorithm for the legal firing sequences problem of a type of synchronous composition Petri nets[J].Science in China Series:Information Sciences,2001,44(3):226-233.

[15]Badouel E,Bernardinello L,Darondeau P.The synthesis problem for elementary net systems is NP-complete[J].Theoretical Computer Science,1997,186(1):107-134.

[16]潘理,趙衛東,王志成,等.Petri網的步問題研究[J].軟件學報,2009,20(3):505-514.

Li Pan,Weidong Zhao,Zhicheng Wang.On the step problem for Petri nets[J].Journal of Software,2009,20(3):505-514 (in Chinese)

[17]Papadimitriou C H.Computational Complexity[M].Chichester:John Wiley and Sons Ltd.,2003.

[18]Garey M R,Johnson D S.Computers and Intractability[M].New York:W.H.Freeman & Co Ltd,2002.

[19]Bron C,Kerbosch J.Algorithm 457:finding all cliques of an undirected graph[J].Communications of the ACM,1973,16(9):575-577.

[20]Tomita E,Tanaka A,Takahashi H.The worst-case time complexity for generating all maximal cliques and computational experiments[J].Theoretical Computer Science,2006,363(1):28-42.

[21]潘理,丁志軍,郭觀七.混合語義時間Petri網模型[J].軟件學報,2011,22(6):1199-1209.

Li Pan,Zhijun Ding,Guanqi Guo.Time Petri net model with mixed semantics[J].Journal of Software,2011,22(6):1199-1209.(in Chinese)

潘 理 男,1975年出生,湖南平江人.博士,湖南理工學院副教授.研究方向為Petri網、形式化建模與優化.

E-mail:panli.hnist@gmail.com

鄭 紅(通信作者) 女,1973年出生,博士,華東理工大學副教授,美國加州大學河濱分校訪問學者.研究方向為普適計算、Petri網應用.

E-mail:zhenghong@ecust.edu.cn

Maximal Conflict Set Enumeration Algorithm Based on Locality of Petri Nets

PAN Li1,ZHENG Hong2,LIU Xian-ming3,YANG Bo1

(1.SchoolofInformationandCommunicationEngineering,HunanInstituteofScienceandTechnology,Yueyang,Hunan414006,China;2.InformationScienceandEngineeringCollege,EastChinaUniversityofScienceandTechnology,Shanghai,200237China;3.InformationandCommunicationBranch,JiangxiElectricPowerCompany,Nanchang,Jiangxi330077,China)

Conflict is an essential concept in Petri net theory.The existing research focuses on the modelling and resolution strategies of conflict problems,but less on the computational complexity of the problems theirselves.In this paper,we propose the conflict set problem for Petri nets,and prove that the conflict set problem is NP-complete.Furthermore,we present a dynamic algorithm for the maximal conflict set enumeration.Our algorithm only computes those conflict sets that are affected by local firing,which avoids enumerating all maximal conflict sets at each marking.The algorithm needs time O(m2n) where m is the number of maximal conflict sets at the current marking and n is the number of transitions.Finally,we show that the maximal conflict set enumeration problem can be solved in O(n2) for free-choice nets and asymmetric choice nets.The results on complexity of thel conflict set problem provide a theoretical reference for solving conflict problems of Petri nets.

Petri nets;conflict set problem;NP completeness;maximal conflict set enumeration algorithm

2015-05-12;

2015-11-09;責任編輯:馬蘭英

國家自然科學基金(No.61473118);湖南省教育廳科學研究重點項目(No.15A079);湖南省科技計劃項目(No.2014GK3026);江西省電力公司科技項目(No.5218351400A1)

TP301

A

0372-2112 (2016)08-1858-06

猜你喜歡
枚舉庫所等價
等價轉化
基于理解性教學的信息技術教學案例研究
基于FPGA的Petri 網模擬器設計與實現
數組在處理枚舉無規律數據中的應用
n次自然數冪和的一個等價無窮大
基于太陽影子定位枚舉法模型的研究
基于枚舉的并行排序與選擇算法設計
收斂的非線性迭代數列xn+1=g(xn)的等價數列
環Fpm+uFpm+…+uk-1Fpm上常循環碼的等價性
基于一種擴展模糊Petri網的列車運行晚點致因建模分析
91香蕉高清国产线观看免费-97夜夜澡人人爽人人喊a-99久久久无码国产精品9-国产亚洲日韩欧美综合