da4py通过SAT编码实现了最先进的进程挖掘方法。Ocaml的版本更黑暗。
da4p的Python项目详细描述
Author : Boltenhagen Mathilde with Thomas Chatain and Josep Carmona Date : 09.2019
简介
该项目使用SAT编码实现Process Mining算法，以获得验证问题的最佳结果。
由于pysat，布尔公式首先被创建，然后转换成CNF形式并用SAT解算器求解。
这个库使用了pm4py对象。在
这个项目是由thomaschatain和mathildeboltenhagen创建的Ocaml版本的翻译。在
科学论文
- 编码符合性检查工件在SAT由mathildeboltenhagen，thomaschatain，Josep Carmona编写
- Anti-alignments in conformance checking–流程模型的黑暗面，作者：thomaschatain，Josep Carmona
- 基于广义对齐的过程行为跟踪聚类，作者：mathildeboltenhagen，thomaschatain，Josep Carmona
环境与安装
python 3.7.x
只需运行：
pip install da4py
（https://pypi.org/project/da4py/0.0.1/）
使用
图书馆使用pm4py。在
pm4py.objects.petriimportimporterpm4py.objects.log.importer.xesimportfactoryasxes_importerfromda4py.src.main.conformanceArtefactsimportConformanceArtefacts# get the data with pm4py model,m0,mf=importer.pnml.import_net('<PATH_TO_MODEL>')traces=xes_importer.import_log('<PATH_TO_LOG>')
反对准
Formal definition : Given a finite collection $L$ of log traces and a model $N$, an anti-alignment is a run $u \in Runs(N)$ which maximizes its distance $\min_{\sigma \in L} dist(\sigma,u)$ to the log.
这将启动主模块。每次实验都必须重新加载该对象、模型和轨迹。这是一个很快就会解决的问题。在
^{pr2}$我们可以设置所需的反对齐大小（用于前缀）：
artefacts.setSize_of_run(10)
对于执行时间或内存问题，我们可以设置将尝试的最大差异数。在
artefacts.setMax_d(10)
有两种类型的距离可用：
- 汉明距离
- 编辑距离
artefacts.setDistance_type("edit")
然后可以通过运行以下命令找到反对准：
artefacts.antiAlignment(model,m0,mf,traces)print(artefacts.getRun())print(artefacts.getTracesWithDistances())
精度
然后我们可以计算精度：
print(artefacts.getPrecision())
其他功能
您可以添加无声过渡标签，在距离方面不需要花费：
artefacts.setSilentLabel("tau")
我们也可以用求和代替最小值：
artefacts.setOptimizeMin(False)
多重对齐
相同的功能（不是精度）也适用于多重对齐：
model,m0,mf=importer.pnml.import_net('<PATH_TO_MODEL>')traces=xes_importer.import_log('<PATH_TO_LOG>')artefacts=ConformanceArtefacts()artefacts.setSilentLabel("tau")artefacts.setDistance_type("hamming")artefacts.setOptimizeMin(True)artefacts.setSize_of_run(10)artefacts.setMax_d(10)# run a multi-Alignmentartefacts.multiAlignment(model,m0,mf,traces)print(artefacts.getRun())print(artefacts.getTracesWithDistances())
美国宇航局
AMSTC是一种跟踪聚类方法，允许从流程模型中提取子网质心。然后输入 一个日志和一个模型，它输出一组子网和相关的群集跟踪。该方法在SAT中实现，但采样方法允许运行大型日志。在
# process modelmodel,m0,mf=importer.pnml.import_net('examples/medium/model2.pnml')# log tracestraces=xes_importer.import_log('examples/medium/model2.xes')# sampleSize : number of traces that are used in the sampling methodsampleSize=5# sizeOfRun : maximal length requested to compute alignment sizeOfRun=8# maxNbC : maximal number of transitions per cluster to avoid to get a unique centroidmaxNbC=5# m : number of cluster that will be searching at each AMSTC of the sampling method. Understand that more than m cluster can bereturned.m=2# maxCounter : as this is a sampling method, maxCounter is the number of fails of AMSTC before the sampling method stops# silent_label : every transition that contains this string will not cost in alignmentclustering=samplingVariantsForAmstc(net,m0,mf,log,sampleSize,sizeOfRun,maxD,maxNbC,m,maxCounter=1,silent_label="tau")
然后，可以像以下那样使用聚类：
frompm4py.visualization.petrinetimportfactoryasvizufor(centroid,traces)inclustering:iftype(centroid)istuple:net,m0,mf=centroidvizu.apply(net,m0,mf).view()print(traces)
SAT编码和公式形状
该工具首先使用da4的运算符类和与或构造SAT公式py.utils.公式.py。这些公式在已发表的相关论文中有详细的描述。在
AND( [], [],
AND( [m_ip [0, 0]], [m_ip [0, 1]],
AND( [], [],
OR( [], [],
AND( [tau_it [1, 0]], [tau_it [1, 1], tau_it [1, 2]], )
AND( [tau_it [1, 1]], [tau_it [1, 0], tau_it [1, 2]], )
AND( [tau_it [1, 2]], [tau_it [1, 0], tau_it [1, 1]], ))
OR( [], [tau_it [1, 0]],
AND( [], [],
OR( [], [],
AND( [m_ip [1, 0], m_ip [0, 0]], [], )
AND( [], [m_ip [1, 0], m_ip [0, 0]], ))
AND( [m_ip [1, 1], m_ip [0, 1]], [], )))
...
然后，将公式转换为WCNF形式，并用pysat库求解。在
[[2], [-1], [7, -82], [-8, -82], [-9, -82], [8, -83], [82, 83, 84], [3, -86]...]
确认
附属机构：LSV，CNRS，ENS Paris Saclay，Inria，巴黎萨克雷大学
- 项目
标签：
欢迎加入QQ群-->： 979659372
