[1]:

import warnings
warnings.filterwarnings("ignore", category=UserWarning)

Conformance Checking with a LTLf model¶

The class ProcessMiningTasks.ConformanceChecking.LTLAnalyzer.LTLAnalyzer provides a way to check if the log conforms to a Linear Temporal Logic on finite traces (LTLf) formula. The formula can be a provided by the user as a string, note that we adopted the LTLf syntax here. In addition, we also provide the following set of LTLf templates:

eventually_a;
next_a;
eventually_a_and_eventually_b;
eventually_a_then_b;
eventually_a_or_b;
eventually_a_next_b;
eventually_a_then_b_then_c;
eventually_a_next_b_next_c;

the following set of LTLf templates called Is First (Last):

is_first_state_a;
is_second_state_a;
is_third_state_a;
last;
second_last;
third_last;
is_last_state_a;
is_second_last_state_a;
is_third_last_state_a;

the following set of LTLf templates with multiple attributes:

p_does_a;
a_is_done_by_p_and_q;
p_does_a_and_b;
p_does_a_and_then_b;
p_does_a_and_eventually_b;
p_does_a_a_not_b;
a_done_by_p_p_not_q;

and the following Target-Branched DECLARE templates:

precedence;
chain_precedence;
responded_existence;
chain_response;
not_chain_precedence;
not_chain_response;
response;
not_precedence;
not_response;
not_responded_existence;
alternate_response;
alternate_precedence.

First of all, an event log has to be imported.

[2]:

import os
from Declare4Py.D4PyEventLog import D4PyEventLog

log_path = os.path.join("../../../", "tests", "test_logs","Sepsis Cases.xes.gz")
event_log = D4PyEventLog()
event_log.parse_xes_log(log_path)

The next step is to create an LTLModel from an input LTLf formula in string format with the class ProcessModels.LTLModel.LTLModel and pass it to the LTL conformance checker implemented in the src.Declare4Py.ProcessMiningTasks.ConformanceChecking.LTLAnalyzer.LTLAnalyzer class. The corresponding method run will do the conformance checking and return a Pandas dataframe. This dataframe contains the traces ids in the first column and the results of the conformance checking in the second column. The run method transforms the LTLf formula into a Deterministic Finite state Automaton (DFA) and checks whether a trace in a log is accepted. This transformation is performed by using two backends:

Lydia, C++ backend that needs to be installed with Docker, more details here;
LTLf2DFA, that needs to be installed with pip install git+https://github.com/whitemech/LTLf2DFA.git@develop#egg=ltlf2dfa. More details here.

As explained in the tutorial regarding process models, it is possible to switch the backends of the LTLf model with the to_ltlf2dfa_backend and to_lydia_backend methods. The default backend is Lydia.

For speeding up the computation, the run method takes as input the integer parameter jobs that sets the number of processes to run in parallel. Each process considers a portion of the input event log. The default value of the number of jobs is 1. Note that, with small logs (i.e., with a small number of events) the performance with multiple jobs can be comparable with the ones of a single job.

We show an example of LTLf conformance checking with the F(ER Triage) formula.

[3]:

from Declare4Py.ProcessModels.LTLModel import LTLModel
from Declare4Py.ProcessMiningTasks.ConformanceChecking.LTLAnalyzer import LTLAnalyzer

model = LTLModel()
model.parse_from_string("F(CRP)")

analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run(jobs=2)
conf_check_res_df

[3]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	False
1047	JNA	False
1048	KNA	False
1049	LNA	False

1050 rows × 2 columns

Conformance Checking with LTLf Templates¶

Declare4Py offers some LTLf templates in the src.Declare4Py.ProcessModels.LTLModel.LTLTemplate class. You just need to instantiate a single template by passing the template name to the LTLTemplate class and then filling the template with some proper activities to obtain an LTLModel and run the LTL checker.

The LTLTemplate’s function fill_template expects a list with the parameters equal to those expected by the template and a list of attribute types and returns an LTLModel object containing the parsed formula of the template and the list of attribute types. The LTLf formula of the template can be retrieved by accessing the formula attribute of the LTLModel object.

`eventually_a`¶

This is a unary template taking one activity as input. The corresponding LTLf formula is F(a).

[4]:

from Declare4Py.ProcessModels.LTLModel import LTLTemplate

template: LTLTemplate = LTLTemplate('eventually_a')
model: LTLModel = template.fill_template(['CRP'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F(con_crp)

[4]:

	case:concept:name	accepted
0	A	True
1	B	True
2	C	True
3	D	True
4	E	True
...	...	...
1045	HNA	True
1046	INA	False
1047	JNA	False
1048	KNA	True
1049	LNA	False

1050 rows × 2 columns

`next_a`¶

This is a unary template taking one activity as input. The corresponding LTLf formula is X(a).

[5]:

template = LTLTemplate('next_a')
model = template.fill_template(['ER Triage'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: X[!](con_ertriage)

[5]:

	case:concept:name	accepted
0	A	False
1	B	True
2	C	True
3	D	True
4	E	True
...	...	...
1045	HNA	True
1046	INA	True
1047	JNA	True
1048	KNA	True
1049	LNA	True

1050 rows × 2 columns

`eventually_a_and_eventually_b`¶

This is a binary template taking two activities as input. The corresponding LTLf formula is F(a) && F(b).

[6]:

template = LTLTemplate('eventually_a_and_eventually_b')
model = template.fill_template(['Leucocytes', 'CRP'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F(con_leucocytes)  && F(con_crp)

[6]:

	case:concept:name	accepted
0	A	True
1	B	True
2	C	True
3	D	True
4	E	True
...	...	...
1045	HNA	True
1046	INA	False
1047	JNA	False
1048	KNA	True
1049	LNA	False

1050 rows × 2 columns

`eventually_a_then_b`¶

This is a binary template taking two activities as input. The corresponding LTLf formula is F(a && F(b)).

[7]:

template = LTLTemplate('eventually_a_then_b')
model = template.fill_template(['Leucocytes', 'CRP'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F(con_leucocytes  && F(con_crp))

[7]:

	case:concept:name	accepted
0	A	True
1	B	True
2	C	True
3	D	True
4	E	False
...	...	...
1045	HNA	True
1046	INA	False
1047	JNA	False
1048	KNA	True
1049	LNA	False

1050 rows × 2 columns

`eventually_a_or_b`¶

This is a binary template taking two activities as input. The corresponding LTLf formula is F(a) || F(b).

[8]:

template = LTLTemplate('eventually_a_or_b')
model = template.fill_template(['Leucocytes', 'CRP'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F(con_leucocytes) || F(con_crp)

[8]:

	case:concept:name	accepted
0	A	True
1	B	True
2	C	True
3	D	True
4	E	True
...	...	...
1045	HNA	True
1046	INA	False
1047	JNA	False
1048	KNA	True
1049	LNA	False

1050 rows × 2 columns

`eventually_a_next_b`¶

This is a binary template taking two activities as input. The corresponding LTLf formula is F(a && X(b)).

[9]:

template = LTLTemplate('eventually_a_next_b')
model = template.fill_template(['Leucocytes', 'CRP'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F(con_leucocytes  && X[!](con_crp))

[9]:

	case:concept:name	accepted
0	A	True
1	B	False
2	C	True
3	D	True
4	E	False
...	...	...
1045	HNA	True
1046	INA	False
1047	JNA	False
1048	KNA	True
1049	LNA	False

1050 rows × 2 columns

`eventually_a_then_b_then_c`¶

This is a ternary template taking three activities as input. The corresponding LTLf formula is F(a && F(b && F(c))).

[10]:

template = LTLTemplate('eventually_a_then_b_then_c')
model = template.fill_template(['ER Registration', 'Leucocytes', 'CRP'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F(con_erregistration  && F(con_leucocytes  && F(con_crp)))

[10]:

	case:concept:name	accepted
0	A	True
1	B	True
2	C	True
3	D	True
4	E	False
...	...	...
1045	HNA	True
1046	INA	False
1047	JNA	False
1048	KNA	True
1049	LNA	False

1050 rows × 2 columns

`eventually_a_next_b_next_c`¶

This is a ternary template taking three activities as input. The corresponding LTLf formula is F(a && X(b && X(c))).

[11]:

template = LTLTemplate('eventually_a_next_b_next_c')
model = template.fill_template(['ER Registration', 'CRP', 'Leucocytes'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F(con_erregistration  && X[!](con_crp  && X[!](con_leucocytes)))

[11]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	False
1047	JNA	False
1048	KNA	False
1049	LNA	False

1050 rows × 2 columns

Conformance Checking with LTLf Templates Is First (Last)¶

These templates follow the same structure as the one used for simple LTLf templates. The fill_template method takes a list of generic attributes and a list of attribute types that match the type of the attributes in the first list. If the type of the attribute is ‘concept:name’ then the second list can be omitted.

`is_first_state_a`¶

This formula identifies all traces where attribute A is performed in the first event.

[12]:

template: LTLTemplate = LTLTemplate('is_first_state_a')
model : LTLModel = template.fill_template(['ER Registration'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: con_erregistration

[12]:

	case:concept:name	accepted
0	A	True
1	B	True
2	C	True
3	D	True
4	E	True
...	...	...
1045	HNA	True
1046	INA	True
1047	JNA	True
1048	KNA	True
1049	LNA	True

1050 rows × 2 columns

`is_second_state_a`¶

This formula identifies all traces where attribute A is performed in the second event.

[13]:

template: LTLTemplate = LTLTemplate('is_second_state_a')
model : LTLModel = template.fill_template(['ER Triage'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: X[!](con_ertriage)

[13]:

	case:concept:name	accepted
0	A	False
1	B	True
2	C	True
3	D	True
4	E	True
...	...	...
1045	HNA	True
1046	INA	True
1047	JNA	True
1048	KNA	True
1049	LNA	True

1050 rows × 2 columns

`is_third_state_a`¶

This formula identifies all traces where attribute A is performed in the third event.

[14]:

template: LTLTemplate = LTLTemplate('is_third_state_a')
model : LTLModel = template.fill_template(['ER Sepsis Triage'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: X[!](X[!](con_ersepsistriage))

[14]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	True
3	D	True
4	E	True
...	...	...
1045	HNA	True
1046	INA	True
1047	JNA	True
1048	KNA	True
1049	LNA	True

1050 rows × 2 columns

`last`¶

This formula identifies all traces where the attribute is guaranteed to change in the very next event. This formula takes an empty list as parameter.

[15]:

template: LTLTemplate = LTLTemplate('last')
model : LTLModel = template.fill_template([])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: !(X[!](true))

[15]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	False
1047	JNA	False
1048	KNA	False
1049	LNA	False

1050 rows × 2 columns

`second_last`¶

This formula identifies all traces where at some point, there will be a change in the activity, indicating that it is not always equal to its previous event. This formula takes an empty list as parameter.

[16]:

template: LTLTemplate = LTLTemplate('second_last')
model : LTLModel = template.fill_template([])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: X[!](!(X[!](true)))

[16]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	False
1047	JNA	False
1048	KNA	False
1049	LNA	False

1050 rows × 2 columns

`third_last`¶

This formula identifies all traces where there will be a change in the activity in the very next time step and that this change will persist at least once more in the future. This formula takes an empty list as parameter.

[17]:

template: LTLTemplate = LTLTemplate('third_last')
model : LTLModel = template.fill_template([])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: X[!](X[!](!(X[!](true))))

[17]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	True
1047	JNA	True
1048	KNA	False
1049	LNA	True

1050 rows × 2 columns

`is_last_state_a`¶

This formula identifies all traces where attribute A is performed in the last event.

[18]:

template: LTLTemplate = LTLTemplate('is_last_state_a')
model : LTLModel = template.fill_template(['Release A'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F(con_releasea  &&  !(X[!](true)))

[18]:

	case:concept:name	accepted
0	A	True
1	B	True
2	C	True
3	D	False
4	E	False
...	...	...
1045	HNA	True
1046	INA	False
1047	JNA	False
1048	KNA	True
1049	LNA	False

1050 rows × 2 columns

`is_second_last_state_a`¶

This formula identifies all traces where attribute A is performed in the penultimate event.

[19]:

template: LTLTemplate = LTLTemplate('is_second_last_state_a')
model : LTLModel = template.fill_template(['Leucocytes'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F(con_leucocytes  && X[!](!(X[!](true))))

[19]:

	case:concept:name	accepted
0	A	True
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	False
1047	JNA	False
1048	KNA	False
1049	LNA	False

1050 rows × 2 columns

`is_third_last_state_a`¶

This formula identifies all traces where attribute A is performed in the third-last event.

[20]:

template: LTLTemplate = LTLTemplate('is_third_last_state_a')
model : LTLModel = template.fill_template(['CRP'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F(con_crp  && X[!](X[!](!(X[!](true)))))

[20]:

	case:concept:name	accepted
0	A	True
1	B	True
2	C	False
3	D	True
4	E	False
...	...	...
1045	HNA	False
1046	INA	False
1047	JNA	False
1048	KNA	False
1049	LNA	False

1050 rows × 2 columns

Conformance Checking with LTLf Templates with multiple attributes¶

For these templates, the fill_template method takes a list of generic attributes (in string format) and a list of attribute types (also strings) as parameters. The order of the elements of these two lists is important. For each template, the instantiated template formula and its corresponding checking in the input log will be computed.

`p_does_a`¶

[21]:

template: LTLTemplate = LTLTemplate('p_does_a')
model : LTLModel = template.fill_template(['A', 'ER Registration'], attr_type=['org:group', 'concept:name'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F(org_a  && con_erregistration)

[21]:

	case:concept:name	accepted
0	A	True
1	B	True
2	C	True
3	D	True
4	E	True
...	...	...
1045	HNA	True
1046	INA	True
1047	JNA	True
1048	KNA	True
1049	LNA	False

1050 rows × 2 columns

`a_is_done_by_p_and_q`¶

[22]:

template: LTLTemplate = LTLTemplate('a_is_done_by_p_and_q')
model : LTLModel = template.fill_template(['A', 'B', 'ER Registration'], attr_type=['org:group', 'concept:name'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: (F(F(org_a  && con_erregistration))  && F(F(org_b  && con_erregistration)))

[22]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	False
1047	JNA	False
1048	KNA	False
1049	LNA	False

1050 rows × 2 columns

`p_does_a_and_b`¶

[23]:

template: LTLTemplate = LTLTemplate('p_does_a_and_b')
model : LTLModel = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: (F(F(org_a  &&  con_erregistration))  && F(F(org_a  &&  con_leucocytes)))

[23]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	False
1047	JNA	False
1048	KNA	False
1049	LNA	False

1050 rows × 2 columns

`p_does_a_and_then_b`¶

[24]:

template: LTLTemplate = LTLTemplate('p_does_a_and_then_b')
model : LTLModel = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F((F(org_a  && con_erregistration)  && X[!](F(org_a  && con_leucocytes))))

[24]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	False
1047	JNA	False
1048	KNA	False
1049	LNA	False

1050 rows × 2 columns

`p_does_a_and_eventually_b`¶

[25]:

template: LTLTemplate = LTLTemplate('p_does_a_and_eventually_b')
model : LTLModel = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F((F(org_a  && con_erregistration)  && F(F(org_a  && con_leucocytes))))

[25]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	False
1047	JNA	False
1048	KNA	False
1049	LNA	False

1050 rows × 2 columns

`p_does_a_a_not_b`¶

[26]:

template: LTLTemplate = LTLTemplate('p_does_a_a_not_b')
model : LTLModel = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F((con_erregistration  &&  (!con_leucocytes  && org_a)))

[26]:

	case:concept:name	accepted
0	A	True
1	B	True
2	C	True
3	D	True
4	E	True
...	...	...
1045	HNA	True
1046	INA	True
1047	JNA	True
1048	KNA	True
1049	LNA	False

1050 rows × 2 columns

`a_done_by_p_p_not_q`¶

[27]:

template = LTLTemplate('a_done_by_p_p_not_q')
model = template.fill_template(['A', 'B', 'ER Registration'], attr_type=['org:group', 'concept:name'])
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F((org_a  &&   (!org_b  && con_erregistration)))

[27]:

	case:concept:name	accepted
0	A	True
1	B	True
2	C	True
3	D	True
4	E	True
...	...	...
1045	HNA	True
1046	INA	True
1047	JNA	True
1048	KNA	True
1049	LNA	False

1050 rows × 2 columns

Conformance Checking with Target-Branched DECLARE templates¶

For these binary templates, the fill_template method takes two lists of activities (in string format) as parameters. For each template, the instantiated template formula and its corresponding checking in the input log will be computed.

`precedence`¶

[28]:

template = LTLTemplate('precedence')
activities_a = ["ER Triage", "CRP"]
activities_b = ["Leucocytes", "Admission NC", "Release A"]
model = template.fill_template(activities_a, activities_b)
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: ((!(con_leucocytes || con_admissionnc || con_releasea))U(con_ertriage || con_crp)) || G(!(con_leucocytes || con_admissionnc || con_releasea))

[28]:

	case:concept:name	accepted
0	A	False
1	B	True
2	C	True
3	D	True
4	E	True
...	...	...
1045	HNA	True
1046	INA	True
1047	JNA	True
1048	KNA	True
1049	LNA	True

1050 rows × 2 columns

`chain_precedence`¶

[29]:

template = LTLTemplate('chain_precedence')
activities_a = ["ER Triage", "CRP", "Leucocytes"]
activities_b = ["Leucocytes", "Admission NC", "Release A"]
model = template.fill_template(activities_a, activities_b)
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: G(X[!](con_leucocytes || con_admissionnc || con_releasea) ->  (con_ertriage || con_crp || con_leucocytes))

[29]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	True
...	...	...
1045	HNA	False
1046	INA	True
1047	JNA	True
1048	KNA	False
1049	LNA	True

1050 rows × 2 columns

`responded_existence`¶

[30]:

template = LTLTemplate('responded_existence')
activities_a = ["ER Triage", "CRP", "Leucocytes"]
activities_b = ["Leucocytes", "Admission NC", "Release A"]
model = template.fill_template(activities_a, activities_b)
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F(con_ertriage || con_crp || con_leucocytes) -> F(con_leucocytes || con_admissionnc || con_releasea)

[30]:

	case:concept:name	accepted
0	A	True
1	B	True
2	C	True
3	D	True
4	E	True
...	...	...
1045	HNA	True
1046	INA	False
1047	JNA	False
1048	KNA	True
1049	LNA	False

1050 rows × 2 columns

`chain_response`¶

[31]:

template = LTLTemplate('chain_response')
activities_a = ["ER Registration", "CRP"]
activities_b = ["ER Triage", "Leucocytes", "Release A"]
model = template.fill_template(activities_a, activities_b)
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: G((con_erregistration  || con_crp) -> X[!](con_ertriage || con_leucocytes || con_releasea))

[31]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	True
...	...	...
1045	HNA	False
1046	INA	True
1047	JNA	True
1048	KNA	False
1049	LNA	True

1050 rows × 2 columns

`not_chain_precedence`¶

[32]:

template = LTLTemplate('not_chain_precedence')
activities_a = ["ER Triage", "CRP", "Leucocytes"]
activities_b = ["Leucocytes", "Admission NC", "Release A"]
model = template.fill_template(activities_a, activities_b)
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: G(X[!](con_leucocytes || con_admissionnc || con_releasea) ->  !(con_ertriage || con_crp || con_leucocytes))

[32]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	True
1047	JNA	True
1048	KNA	False
1049	LNA	True

1050 rows × 2 columns

`not_chain_response`¶

[33]:

template = LTLTemplate('not_chain_response')
activities_a = ["ER Triage", "CRP", "Leucocytes"]
activities_b = ["Leucocytes", "Admission NC", "Release A"]
model = template.fill_template(activities_a, activities_b)
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: G((con_ertriage || con_crp || con_leucocytes) -> X[!](!(con_leucocytes || con_admissionnc || con_releasea)))

[33]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	True
1047	JNA	True
1048	KNA	False
1049	LNA	True

1050 rows × 2 columns

`response`¶

[34]:

template = LTLTemplate('response')
activities_a = ["ER Triage", "CRP", "Leucocytes"]
activities_b = ["Leucocytes", "Admission NC", "Release A"]
model = template.fill_template(activities_a, activities_b)
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: G((con_ertriage || con_crp || con_leucocytes) -> F(con_leucocytes || con_admissionnc || con_releasea))

[34]:

	case:concept:name	accepted
0	A	True
1	B	True
2	C	True
3	D	True
4	E	True
...	...	...
1045	HNA	True
1046	INA	False
1047	JNA	False
1048	KNA	True
1049	LNA	False

1050 rows × 2 columns

`not_precedence`¶

[35]:

template = LTLTemplate('not_precedence')
activities_a = ["ER Triage", "CRP", "Leucocytes"]
activities_b = ["Leucocytes", "Admission NC", "Release A"]
model = template.fill_template(activities_a, activities_b)
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: G(F(con_leucocytes || con_admissionnc || con_releasea) -> !(con_ertriage || con_crp || con_leucocytes))

[35]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	True
1047	JNA	True
1048	KNA	False
1049	LNA	True

1050 rows × 2 columns

`not_response`¶

[36]:

template = LTLTemplate('not_response')
activities_a = ["ER Triage", "CRP", "Leucocytes"]
activities_b = ["Leucocytes", "Admission NC", "Release A"]
model = template.fill_template(activities_a, activities_b)
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: G((con_ertriage || con_crp || con_leucocytes) ->  !(F(con_leucocytes || con_admissionnc || con_releasea)))

[36]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	True
1047	JNA	True
1048	KNA	False
1049	LNA	True

1050 rows × 2 columns

`not_responded_existence`¶

[37]:

template = LTLTemplate('not_responded_existence')
activities_a = ["ER Triage", "CRP", "Leucocytes"]
activities_b = ["Leucocytes", "Admission NC", "Release A"]
model = template.fill_template(activities_a, activities_b)
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: F(con_ertriage || con_crp || con_leucocytes) ->  !(F(con_leucocytes || con_admissionnc || con_releasea))

[37]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	True
1047	JNA	True
1048	KNA	False
1049	LNA	True

1050 rows × 2 columns

`alternate_response`¶

[38]:

template = LTLTemplate('alternate_response')
activities_a = ["ER Triage", "CRP", "Leucocytes"]
activities_b = ["Leucocytes", "Admission NC", "Release A"]
model = template.fill_template(activities_a, activities_b)
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: G((con_ertriage || con_crp || con_leucocytes) -> X[!]((!(con_ertriage || con_crp || con_leucocytes)U(con_leucocytes || con_admissionnc || con_releasea))))

[38]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	False
1047	JNA	False
1048	KNA	False
1049	LNA	False

1050 rows × 2 columns

`alternate_precedence`¶

[39]:

template = LTLTemplate('alternate_precedence')
activities_a = ["ER Triage", "CRP", "Leucocytes"]
activities_b = ["Leucocytes", "Admission NC", "Release A"]
model = template.fill_template(activities_a, activities_b)
print(f"Formula: {model.formula}")
analyzer = LTLAnalyzer(event_log, model)
conf_check_res_df = analyzer.run()
conf_check_res_df

Formula: ((!(con_leucocytes || con_admissionnc || con_releasea))U(con_ertriage || con_crp || con_leucocytes))  && G((con_leucocytes || con_admissionnc || con_releasea) -> X[!]((!(con_leucocytes || con_admissionnc || con_releasea))U(con_ertriage || con_crp || con_leucocytes)) || G(!(con_leucocytes || con_admissionnc || con_releasea)))

[39]:

	case:concept:name	accepted
0	A	False
1	B	False
2	C	False
3	D	False
4	E	False
...	...	...
1045	HNA	False
1046	INA	True
1047	JNA	True
1048	KNA	False
1049	LNA	True

1050 rows × 2 columns

Conformance Checking with a LTLf model¶

Conformance Checking with LTLf Templates¶

eventually_a¶

next_a¶

eventually_a_and_eventually_b¶

eventually_a_then_b¶

eventually_a_or_b¶

eventually_a_next_b¶

eventually_a_then_b_then_c¶

eventually_a_next_b_next_c¶

Conformance Checking with LTLf Templates Is First (Last)¶

is_first_state_a¶

is_second_state_a¶

is_third_state_a¶

last¶

second_last¶

third_last¶

is_last_state_a¶

is_second_last_state_a¶

is_third_last_state_a¶

Conformance Checking with LTLf Templates with multiple attributes¶

p_does_a¶

a_is_done_by_p_and_q¶

p_does_a_and_b¶

p_does_a_and_then_b¶

p_does_a_and_eventually_b¶

p_does_a_a_not_b¶

a_done_by_p_p_not_q¶

Conformance Checking with Target-Branched DECLARE templates¶

precedence¶

chain_precedence¶

responded_existence¶

chain_response¶

not_chain_precedence¶

not_chain_response¶

response¶

not_precedence¶

not_response¶

not_responded_existence¶

alternate_response¶

alternate_precedence¶

`eventually_a`¶

`next_a`¶

`eventually_a_and_eventually_b`¶

`eventually_a_then_b`¶

`eventually_a_or_b`¶

`eventually_a_next_b`¶

`eventually_a_then_b_then_c`¶

`eventually_a_next_b_next_c`¶

`is_first_state_a`¶

`is_second_state_a`¶

`is_third_state_a`¶

`last`¶

`second_last`¶

`third_last`¶

`is_last_state_a`¶

`is_second_last_state_a`¶

`is_third_last_state_a`¶

`p_does_a`¶

`a_is_done_by_p_and_q`¶

`p_does_a_and_b`¶

`p_does_a_and_then_b`¶

`p_does_a_and_eventually_b`¶

`p_does_a_a_not_b`¶

`a_done_by_p_p_not_q`¶

`precedence`¶

`chain_precedence`¶

`responded_existence`¶

`chain_response`¶

`not_chain_precedence`¶

`not_chain_response`¶

`response`¶

`not_precedence`¶

`not_response`¶

`not_responded_existence`¶

`alternate_response`¶

`alternate_precedence`¶