[ ]:

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

Managing Process Models

This tutorial will go through the steps necessary to import and manage process models.

The LTLModel class

An LTLModel can be created from a Linear Temporal Logic on finite traces (LTLf) formula in a string format provided by the user. We adopted the LTLf syntax here. Therefore, the LTLModel has to be imported from src.Declare4Py.ProcessModels.LTLModel and then instantiated.

[1]:

from Declare4Py.ProcessModels.LTLModel import LTLModel

model = LTLModel()
model.parse_from_string("G(ER Triage -> F(CRP))")

[2]:

from ltlf2dfa.parser.ltlf import LTLfParser

parser = LTLfParser()
formula_str = "G(a -> WX b)"
formula = parser(formula_str)       # returns an LTLfFormula

print(formula)

G((a -> WX(b)))

Some basic logical operations on the formulas can be done according to the methods in the LTLModel class. We provide some examples.

[3]:

model.parse_from_string("CRP")

model.add_eventually()
print(model.formula)
model.add_negation()
print(model.formula)
model.add_implication("F(Release A)")
print(model.formula)
print("--------------------------------\n")

model.parse_from_string("Leucocytes")
print(model.formula)
model.add_until("!(CRP)")
print(model.formula)
model.add_always()
print(model.formula)
print("--------------------------------\n")

model.parse_from_string("IV Liquid")
print(model.formula)
model.add_disjunction("IV Antibiotics")
print(model.formula)
model.add_conjunction("X[!](Admission NC)")
print(model.formula)
print("--------------------------------\n")

model.parse_from_string("Return ER")
print(model.formula)
model.add_next()
print(model.formula)
model.add_equivalence("Bad condition")
print(model.formula)

F(crp)
!(F(crp))
(!(F(crp))) -> (F(releasea))
--------------------------------

leucocytes
(leucocytes) U (!(crp))
G((leucocytes) U (!(crp)))
--------------------------------

ivliquid
(ivliquid) || (ivantibiotics)
((ivliquid) || (ivantibiotics)) && (X[!](admissionnc))
--------------------------------

returner
X[!](returner)
(X[!](returner)) <-> (badcondition)

[4]:

from logaut import ltl2dfa
model.parse_from_string("!(X[!](true))") # si usa parse_ltl da pylogics.parsers
print(model.formula)
print(model.parsed_formula)
model.check_satisfiability()
dfa1 = ltl2dfa(model.parsed_formula, backend="lydia")
dfa1 = dfa1.minimize()
print(dfa1.__dict__)
print(dfa1.accepts([{'a': True}, {'a': True}]))
print("-------")

#dfa = ltl2dfa(model.parsed_formula, backend="ltlf2dfa")
#dfa = dfa.minimize()
#print(dfa.__dict__)
#print(dfa.accepts([{'a': True}, {'a': True}]))

!(X[!](true))
(not (next PropositionalTrue(Logic.LTL)))
{'_state_attributes': {}, '_transition_attributes': {}, '_initial_state': 0, '_states': {0, 1, 2}, '_final_states': {0, 1}, '_state_counter': 3, '_transition_function': {0: {1: True}, 2: {2: True}, 1: {2: True}}}
False
-------

Checking an LTLf model satisfiability

An LTLf model can be checked according to its satisfiability (i.e., whether it is satisfiable by a trace or not) with the check_satisfiability method. This is done by transforming the LTLf formula into a Deterministic Finite state Automaton (DFA) and checking its emptyness. 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.

Declare4Py provides the to_ltlf2dfa_backend and to_lydia_backend methods to switch the backends of the LTLf model. The default backend is Lydia.

The check_satisfiability method takes as input the minimize_automaton boolean parameter (with True as default) that performs the minimization of the resulting DFA before the satisfiability checking.

[5]:

model.parse_from_string("CRP & X[!](F(ER Triage && X[!](F(Admission NC))))")
print(f"{model.formula} is satisfiable? {model.check_satisfiability()}")

model.parse_from_string("G(CRP) && F(!(CRP))")
print(f"{model.formula} is satisfiable? {model.check_satisfiability(minimize_automaton=False)}" )

#model.to_ltlf2dfa_backend()
#model.parse_from_string("CRP & X(F(ER Triage && X(F(Admission NC))))")
#print(f"{model.formula} is satisfiable? {model.check_satisfiability()}")

crp &X[!](F(ertriage  && X[!](F(admissionnc)))) is satisfiable? True
G(crp)  && F(!(crp)) is satisfiable? False

The LTLTemplate class

The LTLTemplate class in src.Declare4Py.ProcessModels.LTLModel provides a set of useful LTLf templates. This set contains simple LTLf templates and Target-Branched DECLARE templates. Here, we just list them and their corresponding LTLf formulas. A more detailed use will be shown in the tutorial of the conformance checking with LTLf models.

An LTLf template can be instantiated by providing the name of the template to the LTLTemplate class. Then, the template has to be filled with proper activity names with the fill_template() method:

[6]:

from Declare4Py.ProcessModels.LTLModel import LTLTemplate

template = LTLTemplate('eventually_a_then_b')
model = template.fill_template(['Leucocytes', 'CRP'])
print(f"Formula for {template.template_str}: {model.formula}")

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

Declare4Py provides the following set of simple LTLf templates:

  1. next_a;

  2. eventually_a;

  3. eventually_a_and_eventually_b;

  4. eventually_a_then_b;

  5. eventually_a_or_b;

  6. eventually_a_next_b;

  7. eventually_a_then_b_then_c;

  8. eventually_a_next_b_next_c;

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

  1. is_first_state_a;

  2. is_second_state_a;

  3. is_third_state_a;

  4. last;

  5. second_last;

  6. third_last;

  7. is_last_state_a;

  8. is_second_last_state_a;

  9. is_third_last_state_a;

the following set of LTLf templates with multiple attributes:

  1. p_does_a;

  2. a_is_done_by_p_and_q;

  3. p_does_a_and_b;

  4. p_does_a_and_then_b;

  5. p_does_a_and_eventually_b;

  6. p_does_a_a_not_b;

  7. a_done_by_p_p_not_q;

and the following Target-Branched DECLARE templates:

  1. precedence;

  2. chain_precedence;

  3. responded_existence;

  4. chain_response;

  5. not_chain_precedence;

  6. not_chain_response;

  7. response;

  8. not_precedence;

  9. not_response;

  10. not_responded_existence;

  11. alternate_response;

  12. alternate_precedence.

We show the corresponding LTLf formulas of the templates.

[7]:

from Declare4Py.ProcessModels.LTLModel import LTLTemplate

print("\nSimple LTLf templates:")
print("---------------------")
template = LTLTemplate('next_a')
model = template.fill_template(['ER Triage'])
print(f"Formula for {template.template_str}: {model.formula}")

template: LTLTemplate = LTLTemplate('eventually_a')
model: LTLModel = template.fill_template(['CRP'])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('eventually_a_then_b')
model = template.fill_template(['Leucocytes', 'CRP'])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('eventually_a_or_b')
model = template.fill_template(['Leucocytes', 'CRP'])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('eventually_a_next_b')
model = template.fill_template(['Leucocytes', 'CRP'])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('eventually_a_then_b_then_c')
model = template.fill_template(['ER Registration', 'Leucocytes', 'CRP'])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('eventually_a_next_b_next_c')
model = template.fill_template(['ER Registration', 'CRP', 'Leucocytes'])
print(f"Formula for {template.template_str}: {model.formula}")

print("\nIs First (Last) LTLf templates:")
print("---------------------")

template = LTLTemplate('is_first_state_a')
model = template.fill_template(['ER Triage'])
print(f"Formula for {template.template_str}: {model.formula}")

template: LTLTemplate = LTLTemplate('is_second_state_a')
model: LTLModel = template.fill_template(['CRP'])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('is_third_state_a')
model = template.fill_template(['Leucocytes'])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('last')
model = template.fill_template([])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('second_last')
model = template.fill_template([])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('third_last')
model = template.fill_template([])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('is_last_state_a')
model = template.fill_template(['ER Registration'])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('is_second_last_state_a')
model = template.fill_template(['Leucocytes'])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('is_third_last_state_a')
model = template.fill_template(['CRP'])
print(f"Formula for {template.template_str}: {model.formula}")

print("\n Multiple attributes LTLf templates:")
print("---------------------")
template = LTLTemplate('p_does_a')
model = template.fill_template(['A', 'ER Registration'], attr_type=['org:group', 'concept:name'])
print(f"Formula for {template.template_str}: {model.formula}")

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 for {template.template_str}: {model.formula}")

template = LTLTemplate('p_does_a_and_b')
model = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('p_does_a_and_then_b')
model = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('p_does_a_and_eventually_b')
model = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])
print(f"Formula for {template.template_str}: {model.formula}")

template = LTLTemplate('p_does_a_a_not_b')
model = template.fill_template(['A', 'ER Registration', 'Leucocytes'], attr_type=['org:group', 'concept:name'])
print(f"Formula for {template.template_str}: {model.formula}")

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 for {template.template_str}: {model.formula}")


print("\nTB-DECLARE templates:")
print("---------------------")
tb_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']


for template_str in tb_declare_templates:
    template = LTLTemplate(template_str)
    activation_list = ["ER Triage", "CRP"]
    target_list = ["Leucocytes", "Release A"]
    model = template.fill_template(activation_list, target_list)
    print(f"Formula for {template.template_str}: {model.formula}")


Simple LTLf templates:
---------------------
Formula for next_a: X[!](con_ertriage)
Formula for eventually_a: F(con_crp)
Formula for eventually_a_then_b: F(con_leucocytes  && F(con_crp))
Formula for eventually_a_or_b: F(con_leucocytes) || F(con_crp)
Formula for eventually_a_next_b: F(con_leucocytes  && X[!](con_crp))
Formula for eventually_a_then_b_then_c: F(con_erregistration  && F(con_leucocytes  && F(con_crp)))
Formula for eventually_a_next_b_next_c: F(con_erregistration  && X[!](con_crp  && X[!](con_leucocytes)))

Is First (Last) LTLf templates:
---------------------
Formula for is_first_state_a: con_ertriage
Formula for is_second_state_a: X[!](con_crp)
Formula for is_third_state_a: X[!](X[!](con_leucocytes))
Formula for last: !(X[!](true))
Formula for second_last: X[!](!(X[!](true)))
Formula for third_last: X[!](X[!](!(X[!](true))))
Formula for is_last_state_a: F(con_erregistration  &&  !(X[!](true)))
Formula for is_second_last_state_a: F(con_leucocytes  && X[!](!(X[!](true))))
Formula for is_third_last_state_a: F(con_crp  && X[!](X[!](!(X[!](true)))))

 Multiple attributes LTLf templates:
---------------------
Formula for p_does_a: F(org_a  && con_erregistration)
Formula for a_is_done_by_p_and_q: (F(F(org_a  && con_erregistration))  && F(F(org_b  && con_erregistration)))
Formula for p_does_a_and_b: (F(F(org_a  &&  con_erregistration))  && F(F(org_a  &&  con_leucocytes)))
Formula for p_does_a_and_then_b: F((F(org_a  && con_erregistration)  && X[!](F(org_a  && con_leucocytes))))
Formula for p_does_a_and_eventually_b: F((F(org_a  && con_erregistration)  && F(F(org_a  && con_leucocytes))))
Formula for p_does_a_a_not_b: F((con_erregistration  &&  (!con_leucocytes  && org_a)))
Formula for a_done_by_p_p_not_q: F((org_a  &&   (!org_b  && con_erregistration)))

TB-DECLARE templates:
---------------------
Formula for precedence: ((!(con_leucocytes || con_releasea))U(con_ertriage || con_crp)) || G(!(con_leucocytes || con_releasea))
Formula for chain_precedence: G(X[!](con_leucocytes || con_releasea) ->  (con_ertriage || con_crp))
Formula for responded_existence: F(con_ertriage || con_crp) -> F(con_leucocytes || con_releasea)
Formula for chain_response: G((con_ertriage  || con_crp) -> X[!](con_leucocytes || con_releasea))
Formula for not_chain_precedence: G(X[!](con_leucocytes || con_releasea) ->  !(con_ertriage || con_crp))
Formula for not_chain_response: G((con_ertriage || con_crp) -> X[!](!(con_leucocytes || con_releasea)))
Formula for response: G((con_ertriage || con_crp) -> F(con_leucocytes || con_releasea))
Formula for not_precedence: G(F(con_leucocytes || con_releasea) -> !(con_ertriage || con_crp))
Formula for not_response: G((con_ertriage || con_crp) ->  !(F(con_leucocytes || con_releasea)))
Formula for not_responded_existence: F(con_ertriage || con_crp) ->  !(F(con_leucocytes || con_releasea))
Formula for alternate_response: G((con_ertriage || con_crp) -> X[!]((!(con_ertriage || con_crp)U(con_leucocytes || con_releasea))))
Formula for alternate_precedence: ((!(con_leucocytes || con_releasea))U(con_ertriage || con_crp))  && G((con_leucocytes || con_releasea) -> X[!]((!(con_leucocytes || con_releasea))U(con_ertriage || con_crp)) || G(!(con_leucocytes || con_releasea)))

The DeclareModel and DeclareModelTemplate classes

The DECLARE language provides a set of LTLf templates that are well known and adopted in the Process Mininig community. We start by importing the classes DeclareModel and DeclareModelTemplate.

[8]:

import os

from Declare4Py.ProcessModels.DeclareModel import DeclareModel
from Declare4Py.ProcessModels.DeclareModel import DeclareModelTemplate

The DECLARE constraints supported by Declare4Py can be retrieved with the get_unary_templates() and get_binary_templates methods of the DeclareModelTemplate class:

[9]:

unary_templates = DeclareModelTemplate.get_unary_templates()
binary_templates = DeclareModelTemplate.get_binary_templates()

print("Unary templates:")
print("-----------------")
for template in unary_templates:
    print(template.templ_str)
print("\n")

print("Binary templates:")
print("-----------------")
for template in binary_templates:
    print(template.templ_str)

Unary templates:
-----------------
Existence
Absence
Exactly
Init
End


Binary templates:
-----------------
Choice
Exclusive Choice
Responded Existence
Response
Alternate Response
Chain Response
Precedence
Alternate Precedence
Chain Precedence
Succession
Alternate Succession
Co-Existence
Chain Succession
Not Chain Succession
Not Co-Existence
Not Succession
Not Responded Existence
Not Response
Not Precedence
Not Chain Response
Not Chain Precedence

Notice that for the templates Existence, Absence and Exactly an additional parameter is necessary for the cardinality. This has to be encoded in the DECLARE .decl model with a numeric suffix, for example Exactly2 or Existence23.

The next step is the parsing a DECLARE model.

[10]:

model_path = os.path.join("../../../", "tests", "test_models","data_model.decl")
declare_model = DeclareModel().parse_from_file(model_path)

The DECLARE model can be inspected by getting all the activity names or the constraints. This information is returned as a list of strings.

[12]:

model_activities = declare_model.get_decl_model_activities()
model_constraints = declare_model.get_decl_model_constraints()

print("Model activities:")
print("-----------------")
for idx, act in enumerate(model_activities):
    print(idx, act)
print("\n")

print("Model constraints:")
print("-----------------")
for idx, constr in enumerate(model_constraints):
    print(idx, constr)

Model activities:
-----------------
0 ER Triage
1 ER Registration
2 ER Sepsis Triage
3 Leucocytes
4 CRP
5 LacticAcid
6 IV Antibiotics
7 Admission NC
8 IV Liquid
9 Release A
10 Return ER
11 Admission IC


Model constraints:
-----------------
0 Existence2[Admission NC] | |
1 Chain Response[Admission NC, Release B] |A.org:group is K |T.org:group is E |
2 Chain Response[Admission NC, Release A] |A.org:group is I |T.org:group is E |133020,957701,s
3 Chain Precedence[IV Liquid, Admission NC] |A.org:group is I |T.org:group is A |92,14473,s
4 Chain Response[ER Registration, ER Triage] |(A.DiagnosticArtAstrup is false) AND (A.SIRSCritHeartRate is true) AND (A.org:group is A) AND (A.DiagnosticBlood is true) AND (A.DisfuncOrg is false) AND (A.DiagnosticECG is true) AND (A.Age >= 45) AND (A.InfectionSuspected is true) AND (A.DiagnosticLacticAcid is true) AND (A.DiagnosticSputum is true) AND (A.Hypoxie is false) AND (A.DiagnosticUrinaryCulture is true) AND (A.DiagnosticLiquor is false) AND (A.SIRSCritTemperature is true) AND (A.Infusion is true) AND (A.Hypotensie is false) AND (A.DiagnosticUrinarySediment is true) AND (A.Oligurie is false) AND (A.Age <= 80) AND (A.SIRSCritTachypnea is true) AND (A.DiagnosticOther is false) AND (A.SIRSCritLeucos is false) AND (A.DiagnosticIC is true) AND (A.SIRSCriteria2OrMore is true) AND (A.DiagnosticXthorax is true) |T.org:group is C |52,2154,s
5 Chain Precedence[Release A, Return ER] |A.org:group is ? |T.org:group is E |1121801,1121801,s
6 Chain Precedence[ER Sepsis Triage, IV Antibiotics] |A.org:group is L |T.org:group is L |15,11000,s
7 Chain Response[ER Sepsis Triage, IV Antibiotics] |A.org:group is L |T.org:group is L |15,11000,s
8 Chain Precedence[Admission IC, Admission NC] |A.org:group is J |T.org:group is J |
9 Chain Precedence[IV Antibiotics, Admission NC] |A.org:group is F |T.org:group is A |92,14459,s
10 Chain Precedence[Admission NC, Release B] |A.org:group is E |T.org:group is K |48225,48225,s
11 Chain Response[Admission IC, Admission NC] |A.org:group is J |T.org:group is J |61534,61534,s
12 Chain Response[LacticAcid, Leucocytes] |A.LacticAcid <= 0.8 |T.Leucocytes >= 13.8 |0,2778,m
13 Chain Precedence[ER Registration, ER Triage] |A.org:group is C |(T.InfectionSuspected is true) AND (T.SIRSCritTemperature is true) AND (T.DiagnosticLacticAcid is true) AND (T.DiagnosticBlood is true) AND (T.DiagnosticIC is true) AND (T.SIRSCriteria2OrMore is true) AND (T.DiagnosticECG is true) |52,2154,s