da4py 0.0.2

da4py implements state-of-the-art Process Mining methods over SAT encoding. An Ocaml version is Darksider.

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