Serialized BDDs from the Model Checking Competition

This is a collection of real-life BDDs created from a reachability analysis of 1-safe Petri nets from the Model Checking Competition. These can be used to benchmark the performance of one (or more) BDD packages. Contents Each .zip archive multiple .zip archives for the models from that particular year. Each archive for one such model includes the following serialized BDDs: relation.bdd: A single joined relation of all transitions in the Petri net. states_<n>.bdd: The first set of states with a BDD of magnitude 2ⁿ that was constructed while computing all reachable states in the Petri net. Usage These BDDs can be used in two of the benchmarks from the BDD Benchmarking Suite: Apply: Load two (or more) BDDs and combine them with either an or or an and operation. This is a reimplementation of the benchmark by Pastva and Henzinger (Zenodo). RelProd: Load the relation (relation.bdd) and (states_<n>.bdd) and combine them with a forward or backwards application of the relational product. Reproduction See README.md for all the details.本数据集收录了来自模型检查竞赛（Model Checking Competition）中对1-安全佩特里网（Petri net）进行可达性分析所得到的真实二元决策图（Binary Decision Diagram，BDD）集合，可用于评测单个或多个BDD软件包的性能。 ### 数据集内容 每个压缩包均包含对应年度模型的多个子压缩包。单个模型对应的压缩包内含如下序列化BDD文件： 1. `relation.bdd`：该佩特里网中所有变迁的联合关联关系单一BDD。 2. `states_<n>.bdd`：在计算该佩特里网所有可达状态的过程中构建的、大小为2ⁿ的状态集合BDD。 ### 使用场景 该BDD集合可用于BDD基准测试套件（BDD Benchmarking Suite）中的两项基准测试： 1. **Apply测试**：加载两个或多个BDD，并通过逻辑或（or）或逻辑与（and）运算进行组合。本测试为Pastva与Henzinger（Zenodo）所提出基准测试的重实现版本。 2. **RelProd测试**：加载关联关系文件`relation.bdd`与状态集合文件`states_<n>.bdd`，通过正向或反向应用关系乘积运算进行组合。 ### 复现方法 详细信息请参阅`README.md`文件。