Biodivine 参数化布尔网络

现在您还可以通过Python访问lib-param-bn的全部功能！该库作为AEON.py包的一部分提供。

Rust库，用于处理（参数化）布尔网络。支持

• 从.aeon，.bnet和.sbml格式读取/写入布尔网络模型。
• 基本静态分析，如单调性检查或网络分解。
• 网络参数和部分未知的更新函数。
• 完全符号化的异步转换图。
• (遗留)半符号化的异步转换图。

欲了解更多信息，请查看我们教程模块中的文档。

实用二进制文件

除了主库外，还有一些用于测试或基准测试主库功能的二进制文件。目前，这些二进制文件不是自动化测试过程的一部分，因为它们需要用优化编译，并且通常使用与标准Cargo测试完全不同的工作流程。将来，这些应该作为单独的工作流程包括在内，但现在，如果您更改了相关算法，可以使用它们进行手动测试。

一般来说，所有这些二进制文件都假设有一个参数，即布尔网络文件的路径，支持任何格式（然而，不建议使用.bnet进行涉及调节单调性的测试）。因此，您可以运行以下命令来执行任何测试（使用您希望的BINARY_NAME）

cargo run --release --bin BINARY_NAME --features print-progress -- MODEL_PATH

某些算法在开启 print-progress 特性标志时可以打印中间进度。如果您不希望这种行为，请从命令中移除 --features print-progress。

测试反馈顶点集和独立回路

反馈顶点集问题要求计算一个顶点集，移除这些顶点后，图将变为无环。通常希望找到 最小 的这样一个集。

独立回路问题要求计算一组不相交的回路集，一旦移除这些回路，图将变为无环（即每个其他回路都与独立集的成员相交）。通常希望找到 最大 的这样一个集。

与该特性相关的有四个二进制文件：check_fvs、check_ic、check_nfvs 和 check_nic。前两个测试反馈顶点集和独立回路的贪婪优化搜索。其余两个测试问题的负变体（我们不测试正变体，因为它在功能上与负变体对称）。每个二进制文件都检查应适用于任何正确结果的基基本不变量。

由于这些算法是贪婪的、非最优的，因此您应该期望算法即使在非常大的网络（例如，>1000个变量）上也能完成。特别是，BBM基准中的每个模型都可以在不到一秒的时间内处理而不会出现问题。

测试不动点和投影不动点

不动点问题要求识别每个没有出向的顶点（或参数化网络中参数化和顶点的组合）。

投影不动点问题要求识别满足至少存在一个不动点的变量子集的估值。特别是，不动点顶点 x 是一个顶点，对于该顶点存在一种颜色 c（参数估值），使得 x 在 c 中是一个不动点。对称地，颜色 c 是不动点颜色，如果存在一个顶点 x 使得 x 在 c 中是一个不动点。

有一个测试二进制文件 check_fixed_points，它比较几个算法的结果以确保正确性。此外，还有 bench_fixed_points_naive、bench_fixed_points_symbolic、bench_fixed_points_solver、bench_fixed_points_symbolic_vertices 和 bench_fixed_points_symbolic_colors，它们独立测试每个算法的性能。

请注意，朴素算法通常会在非平凡模型上耗尽内存。因此，check_fixed_points 可能会在网络很大或有很多参数时失败。这就是为什么基准被分离成单独的二进制文件：因为一些算法可以并且会超时或OOM。

PBN到颜色图转储

为了分析（非常）小的网络，将它们转储为显式着色图可能很有用。有一个名为 dump-graph 的二进制文件可以做到这一点

cargo build --release
./target/release/dump-graph MODEL_PATH > graph_edges.txt

该二进制文件将模型文件的路径作为第一个参数，并将图转储到标准输出。

由于图是显式的，预期输出大小对于约>10个变量和>1000个有效参数化（其中参数化是更大的瓶颈）的PBN将无法管理。

您可以在 aeon_models/g2a_*.aeon 模型上测试该功能，这些模型都应该足够小。