用于将二进制决策图转换为自动机的Python库。
bdd2dfa的Python项目详细描述
bdd2dfa公司
一个简单的python包装器，用于解释二进制决策图（bdd） 作为确定性有限自动机（DFAs）。在
包接受来自^{
形式上，得到的DFA对象是拟约化bdd（QDDs）
其中all离开self loop，状态的标签是一个元组：(int, str | bool)，其中第一个条目决定输入的数量，直到这个节点被激活，第二个条目是节点或BDD的真值赋值的决策变量。在
目录
安装
如果您只需要使用bdd2dfa，您只需运行：
$ pip install bdd2dfa
对于开发人员，请注意，此项目使用 poetrypython包/依赖项 管理工具。请先熟悉一下，然后 运行：
$ poetry install
使用
# Create BDDfromddimportBDDmanager=BDD()manager.declare('x','y','z')x,y,z=map(manager.var,'xyz')bexpr=x&y&z# Convert to DFAfrombdd2dfaimportto_dfaqdd=to_dfa(bexpr)assertlen(qdd.states())==7# End at leaf node.assertqdd.label([1,1,1])==(0,True)assertqdd.label([0,1,1])==(0,False)# End at Non-leaf node.assertqdd.label([1,1])==(0,'z')assertqdd.label([0,1])==(1,False)# leaf nodes are self loops.assertqdd.label([1,1,1,1])==(0,True)assertqdd.label([1,1,1,1,1])==(0,True)
生成的DFA对象的每个状态都有三个属性：
node：对dd给出的内部BDD节点的引用。在parity：dd支持边反BDDs，其中一些边指向 对布尔函数求反的布尔函数 节点将指向标准BDD。奇偶校验值决定 节点是否debt：在这个节点可以 过渡。必需的，因为BDD边可以跳过不相关的 决定。在
例如
^{pr2}$BDD与QDD
to_dfa还支持导出BDD，而不是QDD。这就完成了
通过切换qdd标志。在
bdd=to_dfa(bexpr,qdd=False)
DFA使用与QDD相似的状态，但没有
debt属性。当你只想走BDD时很有用。在
note标签字母表也只返回决策变量/真值赋值。在
如果dfa包是用draw选项安装的，我们可以
通过导出到
graphvizdot文件。在
fromdfa.drawimportwrite_dotwrite_dot(qdd,"qdd.dot")write_dot(bdd,"bdd.dot")
使用dot命令进行编译会为qdd.dot生成以下结果
以及bdd.dot的以下内容：
- 项目
标签：
欢迎加入QQ群-->： 979659372
