da4py 0.0.1

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

Author : Boltenhagen Mathilde
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

python 3.7.x

EXAMPLE OF USE

 > from pm4py.objects.petri import importer
 > from pm4py.objects.log.importer.xes import factory as xes_importer
 > from da4py.src.main.conformanceArtefacts import ConformanceArtefacts

 # get the data with pm4py 
 > net, m0, mf = importer.pnml.import_net("./medium/CloseToM8.pnml")
 > log = xes_importer.import_log("./medium/CloseToM8.xes")

 # da4py has a common class for the different artefacts
 > artefacts =  ConformanceArtefacts(size_of_run = 6, max_d = 13)

 # launch a multi-alignment
 > artefacts.multiAlignment(net,m0,mf,log)

FOLDERS

┬  
├ src : python code
├ examples : data and example files
└ ...

ACKNOWLEDGEMENT

Affiliations : LSV, CNRS, ENS Paris-Saclay, Inria, Université Paris-Saclay