/JavaBDD_Application

JavaBDD 的应用，包括：电路正确性验证、布尔函数运算，以及 CTL 模型检验。基于 SpringBoot 框架，使用 Graphviz 可视化。

Primary LanguageHTMLGNU General Public License v3.0GPL-3.0

JavaBDD_Application

BDD：Binary Decision Diagram，二元决策图，是一种用于表示布尔函数的数据结构

JavaBDD：用于操作 BDD 的 Java 库，官网

本仓库的代码呈现了一部分 JavaBDD 的应用，包括：

  • 电路正确性验证
  • 布尔函数运算
  • CTL 模型检验

其他说明：

  • 基于 SpringBoot 框架实现，使用 Graphviz 可视化 BDD；
  • 包含了 JavaBDD 库的用法笔记和补充资料；
  • 实现了一种基于 JavaBDD 库的布尔表达式求值算法；
  • 实现了一种将复杂 CTL 公式解析为 SemanticTree 语义树结构的算法；
  • 实现了一种基于 JavaBDD 库求取前驱状态集的算法，以及基于该算法和 SemanticTree 语义树结构实现模型检验的算法；
  • 实现了基于 Graphviz 引擎的对复杂系统状态机和 CTL 公式解析后的语义树进行可视化的功能

PS：