[發明專利]基于BDD求解功能覆蓋組條件約束語句的方法、設備和介質

有效

• 申請號: 202310920127.4
• 申請日: 2023-07-26
• 公開（公告）號: CN116663491B
• 公開（公告）日: 2023-10-13
• 發明（設計）人: 陳穎;冀偉安
• 申請（專利權）人: 北京云樞創新軟件技術有限公司;上海合見工業軟件集團有限公司;成都融見軟件科技有限公司
• 主分類號: G06F30/398
• 分類號: G06F30/398;G06F111/04;G06F115/10
• 代理公司: 北京鍾維聯合知識產權代理有限公司 11579
• 代理人: 丁慧玲

1.一種基于BDD求解功能覆蓋組條件約束語句的方法，其特征在于，包括：

步驟S1、獲取功能覆蓋組中的目標條件約束語句對應的目標變量{A₁,A₂,…,A_n,…,A_N}，A_n為目標條件約束語句對應的第n個目標變量，n的取值范圍為1到N，目標條件約束語句對應的目標變量總數N≥1；

步驟S2、獲取每一A_n對應的比特位數B_n，確定比特位總數；

步驟S3、構建M個布爾變量，每一布爾變量對應一個目標變量中的一個比特位，將目標條件約束語句轉換為由M個布爾變量表示的目標布爾函數；

步驟S4、基于所述M個布爾變量和所述目標布爾函數生成目標BDD，所述目標BDD中每一條從根節點到葉子True節點的路徑表示一組滿足目標條件約束語句的變量取值，BDD為二叉決策圖；

步驟S5、遍歷所述目標BDD的每一條從根節點到葉子True節點的路徑，獲取每一路徑對應的三狀態字符串，基于每一路徑對應的三狀態字符串生成目標條件約束語句的目標解。

2.根據權利要求1所述的方法，其特征在于，

所述步驟S4包括：

步驟S41、為每一布爾變量設置一個對應的層級，生成M個布爾變量層級，構建每一層級和目標變量的比特位之間的映射關系；

步驟S42、在M個布爾變量層級底部設置底部層級，底部層級設置葉子True節點；

步驟S43、基于所述目標布爾函數在每一層級設置對應的狀態節點，并沿根節點到葉子True節點的方向構建狀態節點之間的有向連接線，生成X條從根節點到葉子True節點的路徑{D₁,D₂,…,D_x,…,D_X}，得到所述目標BDD?，其中，D_x為第x條路徑，x的取值范圍為1到X，有向連接線為實線或虛線。

3.根據權利要求2所述的方法，其特征在于，

所述步驟S5包括：

步驟S51、遍歷每一D_x，若在D_x中不存在第m層級對應的狀態節點，則將第m層級對應的狀態設置為“？”，“？”表示第m層級對應的狀態為0或者1，若存在，則執行步驟S52，m的取值范圍為1到M；

步驟S52、判斷以D_x中以第m層級對應的狀態節點為起點的有向連接線的類型，若為實線，則將第m層級對應的狀態設置為“1”，若為虛線，則將第m層級對應的狀態設置為“0”，基于D_x中所有層級對應的狀態生成D_x對應的三狀態字符串（d₁^x,d₂^x,…,d_m^x,…,d_M^x），d_m^x為D_x對應的三狀態字符串中第m層級對應的狀態，d_m^x等于“0”、“1”或“？”；

步驟S53、基于D_x對應的三狀態字符串以及每一層級和目標變量的比特位之間的映射關系，生成目標條件約束語句的目標解。

4.根據權利要求3所述的方法，其特征在于，

所述步驟S41中，按照隨機的順序為每一布爾變量設置一個對應的層級；

所述步驟S53中，基于每一層級和目標變量的比特位之間的映射關系，確定每一目標變量的每一比特位的值，生成目標條件約束語句的目標解。

5.根據權利要求3所述的方法，其特征在于，

N=1，所述步驟S41中，按照目標變量比特位的排序為每一布爾變量設置一個對應的層級；

步驟S53中，D_x對應的三狀態字符串即為目標條件約束語句的目標解。