用 RUST 编写的逻辑 HCTL 符号模型检查器

此存储库包含混合逻辑 HCTL 符号模型检查器的 RUST 实现。该方法专注于（部分指定的）布尔网络的分析。特别是，它允许在大型、非平凡网络上检查任何用 HCTL 表达的行为假设。这包括稳定性、双稳态、吸引子或振荡行为等属性。

先决条件

要运行模型检查器，您需要 RUST 编译器。我们建议遵循 rustlang.org 上的说明。

如果您不熟悉 RUST，还可以在 AEON.py 中找到大多数重要功能绑定的 Python 绑定。

功能

此存储库包含 CLI 模型检查工具和模型检查库。

模型检查工具

给定一个（部分定义的）布尔网络模型和 HCTL 公式（编码我们想要检查的属性），该工具计算网络的所有状态（以及相应的参数化）来满足公式。目前，只有命令行界面，即将实现 GUI。根据模式，程序可以生成编码结果的 BDD，可以打印满足状态和颜色的数量，或打印所有满足的赋值。

要直接调用模型检查器，请使用以下命令编译代码

cargo build --release

然后运行二进制文件

.\target\release\hctl-model-checker <MODEL_PATH> <FORMULAE_PATH>

• MODEL_PATH 是包含所选格式的 BN 模型的文件的路径（见下文，aeon 是默认值）
• FORMULAE_PATH 是包含有效 HCTL 公式的文件的路径（每行一个）

我们支持以下可选参数

• -o <OUTPUT_BUNDLE> - 生成包含结果BDD的zip包的路径。
• -e <EXTENDED_CONTEXT> - 包含BDD的输入zip包的路径，用于指定通配符的上下文（仅适用于扩展公式）。
• -p <PRINT_OPTION> - 打印的信息量 - 其中之一为 no-print / summary / with-progress / exhaustive。
• -h 或 --help 以获取更多信息

库

此包还提供了一个API来利用模型检查功能。最相关的高级功能可以在模块 analysis 和 model_checking 中找到。此外，有关解析（解析器、标记化器、句法树）的有用功能和结构在 preprocessing 模块中。

模型格式

模型检查器默认以 aeon 格式的BN模型为其输入，benchmark_models 目录中包含许多示例模型。但是，您也可以使用 SBML 和 boolnet 模型。

HCTL公式

包含HCTL属性的文件必须每行包含一个正确格式的公式。公式不得包含自由变量。

格式在包含多个重要公式的 benchmark_formulae.txt 中展示。

要创建自定义公式，您可以使用任何HCTL运算符和许多派生运算符。我们使用以下语法

• 常量：true / True / 1，false / False / 0
• 命题：字母数字字符和下划线（例如 p_1）
• 变量：字母数字字符和下划线，用 in """" 包围（例如 {x_1}）
• 否定：~
• 布尔二元运算符：&，|，=>，<=>，^
• 时间一元运算符：AX，EX，AF，EF，AG，EG
• 时间二元运算符：AU，EU，AW，EW
• 混合运算符
  • 绑定x：!{x}:
  • 跳跃x：@{x}:
  • 存在x：3{x}:
  • 对于所有x: V{x}:
• 括号: (, )