da4py implements state-of-the-art Process Mining methods over SAT encoding. An Ocaml version is Darksider.
Project description
Author : Boltenhagen Mathilde with Thomas Chatain and Josep Carmona
Date : 09.2019
INTRODUCTION
This project implements Process Mining algorithms with SAT encodings to get optimal results in case of verification problems.
Boolean formulas are first created, then converted to CNF and solved with SAT solvers, thanks to pysat
.
This librairy used pm4py
Objects.
The project is a translation of the Ocaml version darksider
created by Thomas Chatain and Mathilde Boltenhagen.
Scientific papers
- Encoding Conformance Checking Artefacts in SAT by Mathilde Boltenhagen, Thomas Chatain, Josep Carmona
- Anti-alignments in conformance checking–the dark side of process models by Thomas Chatain, Josep Carmona
To be implemented soon
- (Ocaml version exists) Generalized Alignment-Based Trace Clustering of Process Behavior by Mathilde Boltenhagen, Thomas Chatain, Josep Carmona
ENVIRONNEMENT & INSTALLATION
python 3.7.x
Simply run :
pip install da4py
(https://pypi.org/project/da4py/0.0.1/)
USAGE
The librairie uses pm4py.
pm4py.objects.petri import importer
pm4py.objects.log.importer.xes import factory as xes_importer
from da4py.src.main.conformanceArtefacts import ConformanceArtefacts
# get the data with pm4py
model, m0, mf = importer.pnml.import_net('<PATH_TO_MODEL>')
traces = xes_importer.import_log('<PATH_TO_LOG>')
Anti-alignment
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.
This launches the main module. This object, the model and the traces must be reloaded for each experimentation. This is an issue that will be fix soon.
artefacts = ConformanceArtefacts()
We can to set the size of the anti-alignment we want (usefull for prefix) :
artefacts.setSize_of_run(10)
For execution times or memory problems, we can set the maximum number of difference that will be tried.
artefacts.setMax_d(10)
Two types of distances are available :
- Hamming distance
- Edit distance
artefacts.setDistance_type("edit")
Then an anti-alignment can be found by running :
artefacts.antiAlignment(model,m0,mf,traces)
print(artefacts.getRun())
print(artefacts.getTracesWithDistances())
Precision
Then we can compute precision :
print(artefacts.getPrecision())
Other features
One can add silent transition label that will not cost in the distances :
artefacts.setSilentLabel("tau")
We can also compute sum instead of min :
artefacts.setOptimizeMin(False)
Multi-alignment
The same features (not precision) also work for multi-alignment:
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-Alignment
artefacts.multiAlignment(model,m0,mf,traces)
print(artefacts.getRun())
print(artefacts.getTracesWithDistances())
ACKNOWLEDGEMENT
Affiliations : LSV, CNRS, ENS Paris-Saclay, Inria, Université Paris-Saclay
Project details
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.