From ddded1900bf2b362d8d216e107492e5c3d4cdaa2 Mon Sep 17 00:00:00 2001
From: MarcusRostSAP <146723913+MarcusRostSAP@users.noreply.github.com>
Date: Tue, 16 Jan 2024 00:16:41 +0100
Subject: [PATCH 1/8] Integrate bpmn2constraint 2 (#1)
* Added initial integration
* Presentation changes
* Checkpoint changes
* Declare model working
* Finalized bpmn2constraints tutorial
---
.vscode/settings.json | 7 +
.../ProcessModels/BpmnConstraintsModel.py | 95 +
Declare4Py/ProcessModels/DeclareModel.py | 43 +
Declare4Py/ProcessModels/LTLModel.py | 16 +-
Declare4Py/Utils/bpmnconstraints/README.md | 25 +
.../Utils/bpmnconstraints/bpmnconstraints.py | 91 +
.../bpmnconstraints/compiler/bpmn_compiler.py | 471 ++++
.../bpmnconstraints/compiler/ltl/__init__.py | 0
.../compiler/ltl/declare2ltl.py | 262 ++
.../Utils/bpmnconstraints/parser/__init__.py | 0
.../bpmnconstraints/parser/bpmn_parser.py | 412 +++
.../bpmnconstraints/parser/json_model.py | 26 +
.../Utils/bpmnconstraints/parser/xml_model.py | 67 +
.../Utils/bpmnconstraints/requirements.txt | 6 +
.../templates/LTLf_templates.py | 89 +
.../bpmnconstraints/templates/__init__.py | 0
.../templates/declare_templates.py | 90 +
.../templates/matching_templates.py | 79 +
.../tutorial/bpmn2constraints.ipynb | 942 +++++++
.../tutorial/data/Sepsis Cases.png | Bin 0 -> 49737 bytes
.../tutorial/data/Sepsis Cases.xml | 2354 +++++++++++++++++
.../tutorial/data/linear_diagram.png | Bin 0 -> 8032 bytes
.../tutorial/data/linear_sequence.xml | 565 ++++
.../Utils/bpmnconstraints/utils/__init__.py | 0
.../Utils/bpmnconstraints/utils/constants.py | 177 ++
.../Utils/bpmnconstraints/utils/sanitizer.py | 37 +
.../tutorials/1.Managing_Event_Logs.ipynb | 162 +-
.../tutorials/2.Managing_Process_Models.ipynb | 12 +-
.../3.Conformance_checking_LTLf.ipynb | 67 +-
requirements.txt | 5 +
setup.py | 4 +-
31 files changed, 5987 insertions(+), 117 deletions(-)
create mode 100644 .vscode/settings.json
create mode 100644 Declare4Py/ProcessModels/BpmnConstraintsModel.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/README.md
create mode 100644 Declare4Py/Utils/bpmnconstraints/bpmnconstraints.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/compiler/bpmn_compiler.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/compiler/ltl/__init__.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/compiler/ltl/declare2ltl.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/parser/__init__.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/parser/bpmn_parser.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/parser/json_model.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/parser/xml_model.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/requirements.txt
create mode 100644 Declare4Py/Utils/bpmnconstraints/templates/LTLf_templates.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/templates/__init__.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/templates/declare_templates.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/templates/matching_templates.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/tutorial/bpmn2constraints.ipynb
create mode 100644 Declare4Py/Utils/bpmnconstraints/tutorial/data/Sepsis Cases.png
create mode 100644 Declare4Py/Utils/bpmnconstraints/tutorial/data/Sepsis Cases.xml
create mode 100644 Declare4Py/Utils/bpmnconstraints/tutorial/data/linear_diagram.png
create mode 100644 Declare4Py/Utils/bpmnconstraints/tutorial/data/linear_sequence.xml
create mode 100644 Declare4Py/Utils/bpmnconstraints/utils/__init__.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/utils/constants.py
create mode 100644 Declare4Py/Utils/bpmnconstraints/utils/sanitizer.py
diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 00000000..9b388533
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,7 @@
+{
+ "python.testing.pytestArgs": [
+ "tests"
+ ],
+ "python.testing.unittestEnabled": false,
+ "python.testing.pytestEnabled": true
+}
\ No newline at end of file
diff --git a/Declare4Py/ProcessModels/BpmnConstraintsModel.py b/Declare4Py/ProcessModels/BpmnConstraintsModel.py
new file mode 100644
index 00000000..d4ccef5c
--- /dev/null
+++ b/Declare4Py/ProcessModels/BpmnConstraintsModel.py
@@ -0,0 +1,95 @@
+import io
+import logging
+import sys
+import json
+from pathlib import Path
+from tqdm import tqdm
+from Declare4Py.Utils.bpmnconstraints.parser.bpmn_parser import Parser
+from Declare4Py.Utils.bpmnconstraints.compiler.bpmn_compiler import Compiler
+from Declare4Py.ProcessModels.DeclareModel import DeclareModel
+from Declare4Py.ProcessModels.LTLModel import LTLModel
+from Declare4Py.ProcessModels.AbstractModel import ProcessModel
+logging.basicConfig(stream=sys.stdout, level=logging.DEBUG)
+
+class BpmnConstraintsModel(ProcessModel):
+ """
+ BpmnConstraintsModel is designed to extract constraints from a bpmn diagram expressed as a xml file.
+ For example usage, see Declare4Py/Utils/bpmnconstraints/tutorial/bpmn2constraints.ipynb
+ """
+ def __init__(self):
+ super().__init__()
+ self.declare_model = DeclareModel()
+ self.ltl_model = []
+ self.formulas = []
+ self.serialized_constraints: [str] = []
+
+ def parse_from_file(self, model_path: str, **kwargs):
+ xml_path = Path(model_path)
+
+ # Check if the path is a file
+ if not xml_path.is_file():
+ logging.warning("Provided path is not a file: {}".format(model_path))
+ return
+ try:
+ # Parsing and compiling the BPMN constraints
+ parsed_result = Parser(xml_path, True, transitivity=False).run()
+ compiled_result = Compiler(parsed_result, transitivity=True, skip_named_gateways=False).run()
+
+ # Extract DECLARE and LTLf constraints
+ declare_constraints = [constraint.get("DECLARE") for constraint in compiled_result]
+ ltl_constraints = [constraint.get("LTLf") for constraint in compiled_result]
+
+ # Assign the constraints to the class attributes if they exist
+ if declare_constraints and ltl_constraints:
+ self.declare_model = self.declare_model.parse_from_diagram(declare_constraints)
+ for con in ltl_constraints:
+ if con is not None:
+ ltl_model = LTLModel()
+ ltl_model.parse_from_diagram(con, self.declare_model.activities)
+ self.ltl_model.append(ltl_model)
+
+
+ except Exception as e:
+ logging.error(f"{model_path}: {e}")
+
+ def parse_from_string(self, content: str, **kwargs):
+ declare_constraints = []
+ ltl_constraints = []
+
+ # Convert string content to a StringIO object to mimic a file-like object
+ xml_io = io.StringIO(content)
+
+ try:
+ # Parse and compile the BPMN constraints from the string
+ result = Parser(xml_io, True, transitivity=False).run()
+ result = Compiler(result, transitivity=False, skip_named_gateways=False).run()
+
+ # Extract DECLARE and LTLf constraints
+ for constraint in tqdm(result):
+ declare_constraints.append(constraint.get("DECLARE"))
+ ltl_constraints.append(constraint.get("LTLf"))
+
+ # Assign the parsed constraints to the class attributes
+ if declare_constraints:
+ self.declare_model = declare_constraints
+ self.ltl_model = ltl_constraints
+ except Exception as e:
+ logging.error(f"Error parsing from string: {e}")
+
+ def to_file(self, model_path: str, **kwargs):
+ data = {
+ "declare_model": self.declare_model,
+ "ltl_model": self.ltl_model
+ }
+ with open(model_path, 'w') as file:
+ json.dump(data, file, indent=4)
+ logging.info(f"Model saved to {model_path}")
+
+ def set_constraints(self):
+ """Sets the constraints for the Declare model"""
+ for constraint in self.constraints:
+ constraint_str = constraint['template'].templ_str
+ if constraint['template'].supports_cardinality:
+ constraint_str += str(constraint['n'])
+ constraint_str += '[' + ", ".join(constraint["activities"]) + '] |' + ' |'.join(constraint["condition"])
+ self.serialized_constraints.append(constraint_str)
\ No newline at end of file
diff --git a/Declare4Py/ProcessModels/DeclareModel.py b/Declare4Py/ProcessModels/DeclareModel.py
index 9cd5283d..6b6db830 100644
--- a/Declare4Py/ProcessModels/DeclareModel.py
+++ b/Declare4Py/ProcessModels/DeclareModel.py
@@ -1291,6 +1291,49 @@ def parse_from_file(self, filename: str, **kwargs) -> DeclareModel:
self.declare_model_lines = lines
self.parse(lines)
return self
+
+ def parse_from_diagram(self, diagram_lines: [str]) -> DeclareModel:
+ all_activities = set()
+ constraints = {}
+
+ # Extract activities and prepare constraints structure
+ """for line in diagram_lines:
+ parts = line.strip('[]').split('[')
+ _, actions = parts
+ for action in actions.split(', '):
+ activities.add(action)
+ constraints[action] = set()"""
+
+ # Identify constraints and apply templates
+ for line in diagram_lines:
+ template_split = line.split("[", 1)
+ template_search = re.search(r'(^.+?)(\d*$)', template_split[0])
+ parts = line.strip('[]').split('[')
+ _, actions = parts
+ activities = []
+ for action in actions.split(', '):
+ activities.append(action)
+ all_activities.add(action)
+ constraints[action] = set()
+
+ if template_search is not None:
+ parts = line.strip('[]').split('[')
+
+ template_str, cardinality = template_search.groups()
+ template = DeclareModelTemplate.get_template_from_string(template_str)
+ if template is not None:
+ # Add template constraints to the activities
+ tmp = {"template": template, "activities": activities,
+ "condition": ["",""]}#re.split(r'\s+\|', line)[1:]}
+ if template.supports_cardinality:
+ tmp['n'] = 1 if not cardinality else int(cardinality)
+ cardinality = tmp['n']
+ self.constraints.append(tmp)
+ self.parsed_model.add_template(line, template, str(cardinality))
+ self.activities = list(all_activities)
+ self.set_constraints()
+
+ return self
def parse(self, lines: [str]):
declare_parsed_model = self.parsed_model
diff --git a/Declare4Py/ProcessModels/LTLModel.py b/Declare4Py/ProcessModels/LTLModel.py
index 2aab99db..0e761e5f 100644
--- a/Declare4Py/ProcessModels/LTLModel.py
+++ b/Declare4Py/ProcessModels/LTLModel.py
@@ -5,7 +5,7 @@
from Declare4Py.ProcessModels.AbstractModel import ProcessModel
from pylogics.parsers import parse_ltl
from Declare4Py.Utils.utils import Utils
-from typing import List
+from typing import List, Tuple
class LTLModel(ProcessModel, ABC):
@@ -153,7 +153,19 @@ def check_satisfiability(self, minimize_automaton: bool = True) -> bool:
return True
else:
return False
-
+
+ def parse_from_diagram(self, line: str, activites):
+ for word in activites:
+ prefixed_word = 'con_' + word.replace(' ', '').lower()
+ line = line.replace(word.replace(' ', '_'), prefixed_word)
+ if line == word:
+ line = word.replace(' ', '').lower()
+ line = 'con_' + line
+
+ self.parse_from_string(line)
+ self.attribute_type = ["concept:name"]
+
+
def parse_from_string(self, content: str, new_line_ctrl: str = "\n") -> None:
"""
This function expects an LTL formula as a string.
diff --git a/Declare4Py/Utils/bpmnconstraints/README.md b/Declare4Py/Utils/bpmnconstraints/README.md
new file mode 100644
index 00000000..d017c06b
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/README.md
@@ -0,0 +1,25 @@
+# BPMN2Constraints
+[](https://api.reuse.software/info/github.com/signavio/bpmn2constraints)
+
+[](https://opensource.org/licenses/Apache-2.0)
+
+Tool for compiling BPMN models directly to constraints.
+Currently, BPMN2Constraints can compile BPMN models stored in both `JSON` and `XML`
+format and output to `DECLARE`, `SIGNAL`
+and `Linear Temporal Logic on Finite Traces` (LTLf).
+BPMN2Constraints can also compile BPMN diagrams to Mermaid.js compatible flowcharts.
+
+The original repository is available [here](https://github.com/signavio/bpmn2constraints),
+and is developed by SAP Signavio.
+
+A tutorial that provides a walk-through of how to use the tool in
+an SAP Signavio context is provided [here](./tutorial/tutorial.ipynb).
+
+
+## Acknowledgements.
+This project has been authored by:
+- Arvid Bergman ([@arvidbt](https://github.com/arvidbt)),
+- Timotheus Kampik ([@TimKam](https://github.com/TimKam)),
+- Adrian Rebmann ([@adrianrebmann](https://github.com/adrianrebmann)).
+And integrated into Declare4Py by:
+- Marcus Rost ([@marcusrostSAP](https://github.com/MarcusRostSAP)).
\ No newline at end of file
diff --git a/Declare4Py/Utils/bpmnconstraints/bpmnconstraints.py b/Declare4Py/Utils/bpmnconstraints/bpmnconstraints.py
new file mode 100644
index 00000000..101b1765
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/bpmnconstraints.py
@@ -0,0 +1,91 @@
+import logging
+import sys
+from pathlib import Path
+from json import dumps
+from tqdm import tqdm
+from Declare4Py.bpmnconstraints.parser.bpmn_parser import Parser
+from Declare4Py.bpmnconstraints.compiler.bpmn_compiler import Compiler
+from Declare4Py.bpmnconstraints.utils.script_utils import Setup
+from Declare4Py.bpmnconstraints.script_utils.constraint_comparison import ComparisonScript
+from Declare4Py.bpmnconstraints.script_utils.dataset_parsing import ParserScript
+from Declare4Py.bpmnconstraints.script_utils.dataset_compiling import CompilingScript
+
+logging.basicConfig(stream=sys.stdout, level=logging.DEBUG)
+
+
+def bpmnconstraints(parse_path=None, compile_path=None, transitivity=False, compare_constraints=None,
+ dataset=None, dataframe=None, parse_dataset=None, plot=False,
+ constraint_type="DECLARE", compile_dataset=None, skip_named_gateways=False):
+ """
+ Main function for BPMN2Constraints tool. At least one flag should be set.
+
+ Parameters:
+ - parse_path (str): Path to the BPMN file to parse.
+ - compile_path (str): Path to the BPMN file to compile.
+ - transitivity (bool): Flag for transitivity in compilation.
+ - compare_constraints (bool): Flag for comparing constraints.
+ - dataset (str): Path to the dataset for comparison.
+ - dataframe (str): Path to the dataframe of compiled constraints for comparison.
+ - parse_dataset (str): Path to the dataset folder for parsing.
+ - plot (bool): Flag for generating plots.
+ - constraint_type (str): Type of constraint to be generated ("DECLARE" or "LTLf").
+ - compile_dataset (str): Path to the dataset folder for compilation.
+ - skip_named_gateways (bool): Flag to skip adding gateways as tokens in compilation.
+
+ Returns:
+ - list or dict: Depending on the operation, returns a list of constraints or the result of the operation.
+ """
+ constraints = []
+ if parse_path:
+ path = Path(parse_path)
+ setup = Setup(None)
+ if setup.is_file(path):
+ result = Parser(path, True, transitivity).run()
+ if result:
+ print(dumps(result, indent=2))
+
+ elif compile_path:
+ path = Path(compile_path)
+ setup = Setup(None)
+ if setup.is_file(path):
+ result = Parser(path, True, transitivity).run()
+ result = Compiler(result, transitivity, skip_named_gateways).run()
+ if constraint_type == "LTLf":
+ for constraint in tqdm(result):
+ constraints.append(constraint.get("LTLf"))
+ elif constraint_type == "DECLARE":
+ for constraint in tqdm(result):
+ constraints.append(constraint.get("DECLARE"))
+ else:
+ logging.warning(
+ "Unknown constraint type. 'DECLARE' or 'LTLF'."
+ )
+ if result:
+ return constraints
+
+ elif compare_constraints:
+ if dataset is None or dataframe is None:
+ logging.warning("If invoking compare_constrains, include path to dataset and dataframe")
+ dataframe_path = Path(dataframe)
+ dataset_path = Path(dataset)
+ setup = Setup(None)
+ if setup.is_file(dataframe_path) and setup.is_file(dataset_path):
+ script = ComparisonScript(dataset_path, dataframe_path, plot)
+ script.run()
+
+ elif parse_dataset:
+ dataset_path = Path(parse_dataset)
+ setup = Setup(None)
+ if setup.is_directory(dataset_path):
+ script = ParserScript(dataset_path, plot)
+ script.run()
+
+ elif compile_dataset:
+ dataset_path = Path(compile_dataset)
+ setup = Setup(None)
+ if setup.is_directory(dataset_path):
+ script = CompilingScript(dataset_path, transitivity, False)
+ script.run()
+
+ else:
+ print("Invalid or missing arguments.")
diff --git a/Declare4Py/Utils/bpmnconstraints/compiler/bpmn_compiler.py b/Declare4Py/Utils/bpmnconstraints/compiler/bpmn_compiler.py
new file mode 100644
index 00000000..c3fca8d4
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/compiler/bpmn_compiler.py
@@ -0,0 +1,471 @@
+from itertools import combinations
+from Declare4Py.Utils.bpmnconstraints.templates.declare_templates import Declare
+from Declare4Py.Utils.bpmnconstraints.templates.matching_templates import Signal
+from Declare4Py.Utils.bpmnconstraints.compiler.ltl.declare2ltl import Declare2ltl
+from Declare4Py.Utils.bpmnconstraints.templates.LTLf_templates import LTLf
+from Declare4Py.Utils.bpmnconstraints.utils.constants import *
+
+
+class Compiler:
+ def __init__(self, sequence, transitivity, skip_named_gateways) -> None:
+ self.sequence = sequence
+ self.transitivity = transitivity
+ self.declare = Declare()
+ self.signal = Signal()
+ self.ltlf = LTLf()
+ self.concurrent = True
+ self.compiled_sequence = []
+ self.cfo = None
+ self.skip_named_gateways = skip_named_gateways
+
+ def run(self):
+ for cfo in self.sequence:
+ self.cfo = cfo
+ self.__compile()
+
+ return self.compiled_sequence
+
+ def __compile(self):
+ if self.__cfo_is_start():
+ self.__create_init_constraint()
+ if self.__cfo_is_end():
+ self.__create_end_constraint()
+
+ if self.__is_activity():
+ self.__create_succession_constraint()
+
+ elif self.__is_gateway():
+ if self.__cfo_is_splitting():
+ self._create_gateway_constraints()
+ self.__create_precedence_constraint()
+
+ if self.__cfo_is_joining():
+ if not self.__cfo_is_end():
+ self.__create_response_constraint()
+
+ def _create_gateway_constraints(self):
+ if self.__get_cfo_type() in XOR_GATEWAY:
+ self.__create_exclusive_choice_constraint()
+
+ if self.__get_cfo_type() == AND_GATEWAY:
+ self.__create_parallel_gateway_constraint()
+ self.concurrent = True
+
+ if self.__get_cfo_type() == OR_GATEWAY:
+ self.__create_inclusive_choice_constraint()
+
+ def __create_succession_constraint(self):
+ name = self.__get_cfo_name()
+ successors = self.__get_cfo_successors()
+ for successor in successors:
+ if self.__get_cfo_type(successor) in ALLOWED_GATEWAYS:
+ if self.__get_cfo_gateway_successors(successor):
+ successors.extend(self.__get_cfo_gateway_successors(successor))
+ if self.transitivity:
+ try:
+ transitivity = self.__get_cfo_transitivity()
+ transitivity = [x for x in transitivity if not self.__is_gateway(x)]
+ successors.extend(transitivity)
+ except Exception:
+ pass
+
+ for successor in successors:
+ if self.__get_cfo_type(successor) in ALLOWED_END_EVENTS:
+ continue
+ successor_name = self.__get_cfo_name(successor)
+
+ if successor_name in ALLOWED_GATEWAYS:
+ continue
+
+ if self.skip_named_gateways and successor["type"] in ALLOWED_GATEWAYS:
+ continue
+
+ if not self.__is_valid_name(successor_name) or not self.__is_valid_name(
+ name
+ ):
+ continue
+
+ if not successor.get("gateway successor"):
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{name} leads to {successor_name}",
+ signal=self.signal.succession(name, successor_name),
+ declare=self.declare.succession(name, successor_name),
+ ltlf=self.ltlf.succession(name, successor_name)
+ )
+ )
+
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{name} and {successor_name}",
+ signal=self.signal.co_existence(name, successor_name),
+ declare=self.declare.co_existence(name, successor_name),
+ ltlf=self.ltlf.co_existence(name, successor_name)
+ )
+ )
+
+ if "is in gateway" not in self.cfo:
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{name} or {successor_name}",
+ signal=self.signal.choice(name, successor_name),
+ declare=self.declare.choice(name, successor_name),
+ ltlf=self.ltlf.choice(name, successor_name)
+ )
+ )
+
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{name} leads to (with loops) {successor_name}",
+ signal=self.signal.alternate_succession(name, successor_name),
+ declare=self.declare.alternate_succession(name, successor_name),
+ ltlf=self.ltlf.alternate_succession(name, successor_name)
+ )
+ )
+
+ def __create_precedence_constraint(self):
+ successors = self.__get_cfo_successors()
+ predecessors = self.__get_cfo_predecessors()
+
+ for successor in successors:
+ if self.__get_cfo_type(successor) in ALLOWED_GATEWAYS:
+ if self.__get_cfo_gateway_successors(successor):
+ successors.extend(self.__get_cfo_gateway_successors(successor))
+
+ for successor in successors:
+ successor_name = self.__get_cfo_name(successor)
+ if self.__get_cfo_type(successor) in ALLOWED_GATEWAYS:
+ continue
+
+ if not self.__is_valid_name(successor_name):
+ continue
+
+ for predecessor in predecessors:
+ predecessor_name = self.__get_cfo_name(predecessor)
+ if self.__get_cfo_type(predecessor) in ALLOWED_GATEWAYS:
+ continue
+
+ if not self.__is_valid_name(predecessor_name):
+ continue
+
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{predecessor_name} precedes {successor_name}",
+ signal=self.signal.precedence(predecessor_name, successor_name),
+ declare=self.declare.precedence(
+ predecessor_name, successor_name
+ ),
+ ltlf=self.ltlf.precedence(predecessor_name, successor_name)
+ )
+ )
+
+ if self.concurrent:
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{predecessor_name} precedes {successor_name}",
+ signal=self.signal.alternate_precedence(
+ predecessor_name, successor_name
+ ),
+ declare=self.declare.alternate_precedence(
+ predecessor_name, successor_name
+ ),
+ ltlf=self.ltlf.alternate_precedence(
+ predecessor_name, successor_name
+ )
+ )
+ )
+
+ def __is_valid_name(self, name):
+ if name in ALLOWED_START_EVENTS:
+ return False
+ if name in ALLOWED_END_EVENTS:
+ return False
+ if name in ALLOWED_GATEWAYS:
+ return False
+ if name in GATEWAY_NAMES:
+ return False
+ return True
+
+ def __cfo_is_start(self, cfo=None):
+ if cfo:
+ return cfo.get("is start")
+ return self.cfo.get("is start")
+
+ def __cfo_is_end(self, cfo=None):
+ if cfo:
+ return cfo.get("is end")
+ return self.cfo.get("is end")
+
+ def __cfo_is_splitting(self, cfo=None):
+ if cfo:
+ return cfo.get("splitting")
+ return self.cfo.get("splitting")
+
+ def __cfo_is_joining(self, cfo=None):
+ if cfo:
+ return cfo.get("joining")
+ return self.cfo.get("joining")
+
+ def __get_cfo_type(self, cfo=None):
+ if cfo:
+ return cfo.get("type")
+ return self.cfo.get("type")
+
+ def __get_cfo_successors(self, cfo=None):
+ if cfo:
+ return cfo.get("successor")
+ return self.cfo.get("successor")
+
+ def __get_cfo_predecessors(self, cfo=None):
+ if cfo:
+ return cfo.get("predecessor")
+ return self.cfo.get("predecessor")
+
+ def __get_cfo_transitivity(self, cfo=None):
+ if cfo:
+ return cfo.get("transitivity")
+ return self.cfo.get("transitivity")
+
+ def __get_cfo_gateway_successors(self, cfo=None):
+ if cfo:
+ return cfo.get("gateway successors")
+ return self.cfo.get("gateway successors")
+
+ def __create_response_constraint(self):
+ successors = self.__get_cfo_successors()
+ predecessors = self.__get_cfo_predecessors()
+
+ for successor in successors:
+ if self.__get_cfo_type(successor) in ALLOWED_GATEWAYS:
+ if self.__get_cfo_gateway_successors(successor):
+ successors.extend(self.__get_cfo_gateway_successors(successor))
+
+ for predecessor in predecessors:
+ predecessor_name = self.__get_cfo_name(predecessor)
+ if not self.__is_valid_name(predecessor_name):
+ continue
+
+ if self.__get_cfo_type(predecessor) in ALLOWED_GATEWAYS:
+ continue
+
+ for successor in successors:
+ successor_name = self.__get_cfo_name(successor)
+ if not self.__is_valid_name(successor_name):
+ continue
+
+ if self.__get_cfo_type(successor) in ALLOWED_GATEWAYS:
+ continue
+
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{predecessor_name} responds to {successor_name}",
+ signal=self.signal.response(predecessor_name, successor_name),
+ declare=self.declare.response(predecessor_name, successor_name),
+ ltlf=self.ltlf.response(predecessor_name, successor_name),
+ )
+ )
+
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{predecessor_name} responds to {successor_name}",
+ signal=self.signal.alternate_response(
+ predecessor_name, successor_name
+ ),
+ declare=self.declare.alternate_response(
+ predecessor_name, successor_name
+ ),
+ ltlf=self.ltlf.alternate_response(
+ predecessor_name, successor_name
+ ),
+ )
+ )
+
+ def __create_init_constraint(self):
+ if self.__is_gateway():
+ self.cfo.update({"discard": True})
+
+ name = self.__get_cfo_name()
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"starts with {name}",
+ signal=self.signal.init(name),
+ declare=self.declare.init(name),
+ ltlf=self.ltlf.init(name),
+ )
+ )
+
+ def __create_end_constraint(self):
+ name = self.__get_cfo_name()
+
+ if not self.__is_valid_name(name):
+ return
+
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"ends with {name}",
+ signal=self.signal.end(name),
+ declare=self.declare.end(name),
+ ltlf=self.ltlf.end(name),
+ )
+ )
+
+ def __create_exclusive_choice_constraint(self):
+ successors = self.__get_cfo_successors()
+ for successor in successors:
+ if self.__get_cfo_type(successor) in ALLOWED_GATEWAYS:
+ if self.__get_cfo_gateway_successors(successor):
+ successors.extend(self.__get_cfo_gateway_successors(successor))
+
+ if successors:
+ successors = [self.__get_cfo_name(successor) for successor in successors]
+ for split in combinations(successors, 2):
+ if not self.__is_valid_name(split[0]) or not self.__is_valid_name(
+ split[1]
+ ):
+ continue
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{split[0]} xor {split[1]}",
+ signal=self.signal.exclusive_choice(split[0], split[1]),
+ declare=self.declare.exclusive_choice(split[0], split[1]),
+ ltlf=self.ltlf.exclusive_choice(split[0], split[1]),
+ )
+ )
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{split[0]} or {split[1]}",
+ signal=self.signal.choice(split[0], split[1]),
+ declare=self.declare.choice(split[0], split[1]),
+ ltlf=self.ltlf.choice(split[0], split[1]),
+ )
+ )
+
+ predecessors = self.__get_cfo_predecessors()
+ if predecessors:
+ for predecessor in predecessors:
+ predecessor_name = self.__get_cfo_name(predecessor)
+ for successor in successors:
+ if not self.__is_valid_name(
+ predecessor_name
+ ) or not self.__is_valid_name(successor):
+ continue
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{predecessor_name} or {successor}",
+ signal=self.signal.choice(
+ predecessor_name, successor
+ ),
+ declare=self.declare.choice(
+ predecessor_name, successor
+ ),
+ ltlf=self.ltlf.choice(
+ predecessor_name, successor
+ ),
+ )
+ )
+
+ def __create_parallel_gateway_constraint(self):
+ successors = self.__get_cfo_successors()
+ for successor in successors:
+ if self.__get_cfo_type(successor) in ALLOWED_GATEWAYS:
+ if self.__get_cfo_gateway_successors(successor):
+ successors.extend(self.__get_cfo_gateway_successors(successor))
+
+ if successors:
+ successors = [self.__get_cfo_name(successor) for successor in successors]
+ for split in combinations(successors, 2):
+ if not self.__is_valid_name(split[0]) or not self.__is_valid_name(
+ split[1]
+ ):
+ continue
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{split[0]} and {split[1]}",
+ signal=self.signal.co_existence(split[0], split[1]),
+ declare=self.declare.co_existence(split[0], split[1]),
+ ltlf=self.ltlf.co_existence(split[0], split[1]),
+ )
+ )
+
+ def __create_inclusive_choice_constraint(self):
+ successors = self.__get_cfo_successors()
+ for successor in successors:
+ if self.__get_cfo_type(successor) in ALLOWED_GATEWAYS:
+ if self.__get_cfo_gateway_successors(successor):
+ successors.extend(self.__get_cfo_gateway_successors(successor))
+
+ if successors:
+ successors = [self.__get_cfo_name(successor) for successor in successors]
+ for split in combinations(successors, 2):
+ if not self.__is_valid_name(split[0]) or not self.__is_valid_name(
+ split[1]
+ ):
+ continue
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{split[0]} or {split[1]}",
+ signal=self.signal.choice(split[0], split[1]),
+ declare=self.declare.choice(split[0], split[1]),
+ ltlf=self.ltlf.choice(split[0], split[1]),
+ )
+ )
+
+ predecessors = self.__get_cfo_predecessors()
+ if predecessors:
+ for predecessor in predecessors:
+ predecessor_name = self.__get_cfo_name(predecessor)
+ for successor in successors:
+ if not self.__is_valid_name(
+ predecessor_name
+ ) or not self.__is_valid_name(successor):
+ continue
+ self.compiled_sequence.append(
+ self.__create_constraint_object(
+ description=f"{predecessor_name} or {successor}",
+ signal=self.signal.choice(predecessor_name, successor),
+ declare=self.declare.choice(
+ predecessor_name, successor
+ ),
+ ltlf=self.ltlf.choice(
+ predecessor_name, successor
+ ),
+ )
+ )
+
+ def __get_cfo_name(self, cfo=None):
+ if cfo:
+ name = cfo.get("name")
+ else:
+ name = self.cfo.get("name")
+
+ if not name or name == " ":
+ if cfo:
+ return self.__get_cfo_type(cfo)
+ return self.__get_cfo_type()
+ return name
+
+ def __is_activity(self, cfo=None):
+ if cfo:
+ cfo_type = cfo.get("type")
+ else:
+ cfo_type = self.__get_cfo_type()
+ if cfo_type:
+ return cfo_type in ALLOWED_ACTIVITIES
+ return False
+
+ def __is_gateway(self, cfo=None):
+ if cfo:
+ cfo_type = cfo.get("type")
+ else:
+ cfo_type = self.__get_cfo_type()
+ if cfo_type:
+ return cfo_type in ALLOWED_GATEWAYS
+ return False
+
+ def __create_constraint_object(self, description, signal, declare, ltlf):
+ return {
+ "description": description,
+ "SIGNAL": signal,
+ "DECLARE": declare,
+ "LTLf": ltlf,
+ }
diff --git a/Declare4Py/Utils/bpmnconstraints/compiler/ltl/__init__.py b/Declare4Py/Utils/bpmnconstraints/compiler/ltl/__init__.py
new file mode 100644
index 00000000..e69de29b
diff --git a/Declare4Py/Utils/bpmnconstraints/compiler/ltl/declare2ltl.py b/Declare4Py/Utils/bpmnconstraints/compiler/ltl/declare2ltl.py
new file mode 100644
index 00000000..4ff7c3cd
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/compiler/ltl/declare2ltl.py
@@ -0,0 +1,262 @@
+import logging
+from pylogics.syntax.base import And, Implies, Not, Or
+from pylogics.syntax.ltl import (
+ Always,
+ Eventually,
+ Next,
+ Until,
+ PropositionalTrue,
+ Atomic,
+)
+from pylogics.utils.to_string import to_string
+
+# Declare Templates
+
+EXISTENCE = "Existence"
+ABSENCE = "Absence"
+EXACTLY = "Exactly"
+
+INIT = "Init"
+END = "End"
+
+CHOICE = "Choice"
+EXCLUSIVE_CHOICE = "Exclusive Choice"
+RESPONDED_EXISTENCE = "Responded Existence"
+RESPONSE = "Response"
+ALTERNATE_RESPONSE = "Alternate Response"
+CHAIN_RESPONSE = "Chain Response"
+PRECEDENCE = "Precedence"
+ALTERNATE_PRECEDENCE = "Alternate Precedence"
+CHAIN_PRECEDENCE = "Chain Precedence"
+
+SUCCESSION = "Succession"
+ALTERNATE_SUCCESSION = "Alternate Succession"
+CHAIN_SUCCESSION = "Chain Succession"
+CO_EXISTENCE = "Co-Existence"
+
+NOT_CO_EXISTENCE = "Not Co-Existence"
+NOT_RESPONDED_EXISTENCE = "Not Responded Existence"
+NOT_RESPONSE = "Not Response"
+NOT_CHAIN_RESPONSE = "Not Chain Response"
+NOT_PRECEDENCE = "Not Precedence"
+NOT_CHAIN_PRECEDENCE = "Not Chain Precedence"
+
+NOT_SUCCESSION = "Not Succession"
+NOT_ALTERNATE_SUCCESSION = "Not Alternate Succession"
+NOT_CHAIN_SUCCESSION = "Not Chain Succession"
+
+
+class Declare2ltl:
+ def __init__(self) -> None:
+ pass
+
+ def to_ltl_str(self, constraint_str):
+ try:
+ formula = self.__to_ltl(constraint_str)
+ if formula is None:
+ return "Not translatable"
+ return to_string(formula)
+ except Exception:
+ logging.error(constraint_str)
+ return "Not translatable"
+
+ def __to_ltl(self, constraint_str):
+ n = 0
+ templ_str = constraint_str.split("[")[0]
+ if templ_str[-1].isdigit():
+ n = int(templ_str[-1])
+ templ_str = templ_str[:-1]
+ activities = [
+ act.strip() for act in constraint_str.split("[")[1].split("]")[0].split(",")
+ ]
+ activities = [act for act in activities if act != ""]
+ if len(activities) == 0:
+ return None
+ activity_left = Atomic(activities[0].replace(" ", "_"))
+ activity_right = None
+ if len(activities) == 2:
+ activity_right = Atomic(activities[1].replace(" ", "_"))
+ if templ_str == ABSENCE:
+ if n == 1:
+ return Not(Eventually(activity_left))
+ elif n == 2:
+ return Not(
+ Eventually(And(activity_left, Next(Eventually(activity_left))))
+ )
+ elif n == 3:
+ return Not(
+ Eventually(
+ And(
+ activity_left,
+ Next(
+ Eventually(
+ And(activity_left, Next(Eventually(activity_left)))
+ )
+ ),
+ )
+ )
+ )
+ elif n == 4:
+ return Not(
+ Eventually(
+ And(
+ activity_left,
+ Next(
+ Eventually(
+ And(
+ activity_left,
+ Next(
+ Eventually(
+ And(
+ activity_left,
+ Next(Eventually(activity_left)),
+ )
+ )
+ ),
+ )
+ )
+ ),
+ )
+ )
+ )
+ else:
+ raise ValueError("Unsupported n: " + str(n))
+
+ elif templ_str == EXISTENCE:
+ if n == 1:
+ return Eventually(activity_left)
+ elif n == 2:
+ return Eventually(And(activity_left, Next(Eventually(activity_left))))
+ elif n == 3:
+ return Eventually(
+ And(
+ activity_left,
+ Next(
+ Eventually(
+ And(activity_left, Next(Eventually(activity_left)))
+ )
+ ),
+ )
+ )
+ else:
+ raise ValueError("Unsupported n: " + str(n))
+
+ elif templ_str == EXACTLY:
+ if n == 1:
+ return And(
+ self.__to_ltl(constraint_str.replace(EXACTLY, EXISTENCE)),
+ self.__to_ltl(constraint_str.replace(EXACTLY + "1", ABSENCE + "2")),
+ )
+ elif n == 2:
+ return And(
+ self.__to_ltl(constraint_str.replace(EXACTLY, EXISTENCE)),
+ self.__to_ltl(constraint_str.replace(EXACTLY + "2", ABSENCE + "3")),
+ )
+ elif n == 3:
+ return And(
+ self.__to_ltl(constraint_str.replace(EXACTLY, EXISTENCE)),
+ self.__to_ltl(constraint_str.replace(EXACTLY + "3", ABSENCE + "4")),
+ )
+ else:
+ raise ValueError("Unsupported n: " + str(n))
+
+ elif templ_str == INIT:
+ return activity_left
+
+ elif templ_str == END:
+ return Eventually(And(activity_left, Next(Not(PropositionalTrue()))))
+
+ elif templ_str == CHOICE:
+ return Or(Eventually(activity_left), Eventually(activity_right))
+
+ elif templ_str == EXCLUSIVE_CHOICE:
+ return And(
+ Or(Eventually(activity_left), Eventually(activity_right)),
+ Not(And(Eventually(activity_left), Eventually(activity_right))),
+ )
+
+ elif templ_str == RESPONDED_EXISTENCE:
+ return Implies(Eventually(activity_left), Eventually(activity_right))
+
+ elif templ_str == RESPONSE:
+ return Always(Implies(activity_left, Eventually(activity_right)))
+
+ elif templ_str == ALTERNATE_RESPONSE:
+ return Always(
+ Implies(activity_left, Next(Until(Not(activity_left), activity_right)))
+ )
+
+ elif templ_str == CHAIN_RESPONSE:
+ return Always(Implies(activity_left, Next(activity_right)))
+
+ elif templ_str == PRECEDENCE:
+ return Or(
+ Until(Not(activity_right), activity_left), Always(Not(activity_right))
+ )
+ elif templ_str == ALTERNATE_PRECEDENCE:
+ return And(
+ Or(
+ Until(Not(activity_right), activity_left),
+ Always(Not(activity_right)),
+ ),
+ Always(
+ Implies(
+ activity_right,
+ Or(
+ Until(Not(activity_right), activity_left),
+ Always(Not(activity_right)),
+ ),
+ )
+ ),
+ )
+
+ elif templ_str == CHAIN_PRECEDENCE:
+ return Always(Implies(Next(activity_right), activity_left))
+
+ elif templ_str == SUCCESSION:
+ return And(
+ self.__to_ltl(constraint_str.replace(SUCCESSION, RESPONSE)),
+ self.__to_ltl(constraint_str.replace(SUCCESSION, PRECEDENCE)),
+ )
+
+ elif templ_str == ALTERNATE_SUCCESSION:
+ return And(
+ self.__to_ltl(
+ constraint_str.replace(ALTERNATE_SUCCESSION, ALTERNATE_RESPONSE)
+ ),
+ self.__to_ltl(
+ constraint_str.replace(ALTERNATE_SUCCESSION, ALTERNATE_PRECEDENCE)
+ ),
+ )
+
+ elif templ_str == CHAIN_SUCCESSION:
+ return And(
+ self.__to_ltl(constraint_str.replace(CHAIN_SUCCESSION, CHAIN_RESPONSE)),
+ self.__to_ltl(
+ constraint_str.replace(CHAIN_SUCCESSION, CHAIN_PRECEDENCE)
+ ),
+ )
+
+ elif templ_str == CO_EXISTENCE:
+ return And(
+ Implies(Eventually(activity_left), Eventually(activity_right)),
+ Implies(Eventually(activity_right), Eventually(activity_left)),
+ )
+
+ elif templ_str == NOT_RESPONDED_EXISTENCE:
+ return Implies(Eventually(activity_left), Not(Eventually(activity_right)))
+ elif templ_str == NOT_CHAIN_PRECEDENCE:
+ return Always(Implies(Next(activity_right), Not(activity_left)))
+ elif templ_str == NOT_PRECEDENCE:
+ return Always(Implies(Eventually(activity_left), Not(activity_left)))
+ elif templ_str == NOT_RESPONSE:
+ return Always(Implies(activity_left, Not(Eventually(activity_right))))
+ elif templ_str == NOT_CHAIN_RESPONSE:
+ return Always(Implies(Next(activity_left), Not(activity_right)))
+ elif templ_str == NOT_SUCCESSION:
+ return And(
+ self.__to_ltl(constraint_str.replace(NOT_SUCCESSION, NOT_RESPONSE)),
+ self.__to_ltl(constraint_str.replace(NOT_SUCCESSION, NOT_PRECEDENCE)),
+ )
+ else:
+ raise ValueError("Unknown template: " + constraint_str)
diff --git a/Declare4Py/Utils/bpmnconstraints/parser/__init__.py b/Declare4Py/Utils/bpmnconstraints/parser/__init__.py
new file mode 100644
index 00000000..e69de29b
diff --git a/Declare4Py/Utils/bpmnconstraints/parser/bpmn_parser.py b/Declare4Py/Utils/bpmnconstraints/parser/bpmn_parser.py
new file mode 100644
index 00000000..5f1cf2ad
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/parser/bpmn_parser.py
@@ -0,0 +1,412 @@
+import logging
+from pathlib import Path
+from json import load, JSONDecodeError
+from xml.etree import ElementTree
+from Declare4Py.Utils.bpmnconstraints.utils.constants import *
+from Declare4Py.Utils.bpmnconstraints.utils.sanitizer import Sanitizer
+from Declare4Py.Utils.bpmnconstraints.parser.json_model import JsonModel
+from Declare4Py.Utils.bpmnconstraints.parser.xml_model import XmlModel
+
+
+class Parser:
+ def __init__(self, bpmn, is_file, transitivity) -> None:
+ self.transitivity = transitivity
+ self.bpmn_model = self.__create_model(bpmn, is_file)
+ self.bpmn_diagram = self.bpmn_model
+ self.sequence = []
+ self.is_json = is_file and Path(bpmn).suffix == ".json"
+ self.sanitizer = Sanitizer()
+ self.model = None
+
+ def __flatten_model(self):
+ self.bpmn_model[CHILD_SHAPES] = self.__flatten(self.bpmn_model)
+
+ def __create_model(self, bpmn, is_file):
+ if is_file:
+ try:
+ file_extension = Path(bpmn).suffix
+ if not file_extension or file_extension not in [".json", ".xml"]:
+ return None
+ elif file_extension == ".xml":
+ return ElementTree.parse(bpmn).getroot()
+ elif file_extension == ".json":
+ with open(bpmn, "r", encoding="utf-8") as file:
+ return load(file)
+ except JSONDecodeError:
+ raise Exception("Something wrong with format of JSON file.")
+ except OSError:
+ raise Exception("Something went wrong reading the file.")
+ else:
+ return bpmn
+
+ def __flatten(self, model):
+ elements = []
+ for elem in model[CHILD_SHAPES]:
+ if self.model.get_element_type(elem) not in ALLOWED_SWIMLANES:
+ elements.append(elem)
+ else:
+ elements += self.__flatten(elem)
+ return elements
+
+ def run(self):
+ try:
+ if self.is_json:
+ self.model = JsonModel(self.bpmn_model)
+ self.__flatten_model()
+ else:
+ self.model = XmlModel(self.bpmn_model)
+ self.__parse()
+ self.__mark_gateway_elements()
+ if self.transitivity:
+ self.__add_transitivity()
+ self.validate_splitting_and_joining_gateway_cases()
+ return self.sequence
+ except Exception:
+ logging.warning(
+ "\nCould not execute model. Make sure that model is:\n1. Formatted correctly.\n2. File ends with .xml or .json."
+ )
+
+ def validate_splitting_and_joining_gateway_cases(self):
+ """Update 'is start' and 'is end' attributes of cfo based on splitting/joining gateways.
+ Otherwise, the parser interprets the gateways as start/end events instead of the activities.
+ """
+
+ item_indices = {item["name"]: index for index, item in enumerate(self.sequence)}
+ for cfo in self.sequence:
+ if cfo["is start"] and (cfo["type"] in DISCARDED_START_GATEWAYS):
+ cfo["is start"] = False
+ for successor in cfo["successor"]:
+ self.sequence[item_indices[successor["name"]]]["is start"] = True
+ if cfo["is end"] and (cfo["name"] in GATEWAY_NAMES or cfo["type"] == "exclusivegateway"):
+ cfo["is end"] = False
+ for predecessor in cfo["predecessor"]:
+ self.sequence[item_indices[predecessor["name"]]]["is end"] = True
+
+ def __mark_gateway_elements(self):
+ for cfo in self.sequence:
+ predecessors = cfo.get("predecessor")
+ for predecessor in predecessors:
+ predecessor_id = predecessor.get("id")
+ predecessor_cfo = self.__get_cfo_by_id(predecessor_id)
+ if predecessor_cfo:
+ if predecessor_cfo.get(
+ "type"
+ ) in ALLOWED_GATEWAYS and predecessor_cfo.get("splitting"):
+ cfo.update({"is in gateway": True})
+ if predecessor_cfo.get(
+ "type"
+ ) in ALLOWED_GATEWAYS and predecessor_cfo.get("joining"):
+ continue
+ if cfo.get("type") in ALLOWED_GATEWAYS and cfo.get("joining"):
+ continue
+ if "is in gateway" in predecessor_cfo:
+ cfo.update({"is in gateway": True})
+
+ def __get_cfo_by_id(self, successor_id):
+ for cfo in self.sequence:
+ if successor_id == cfo.get("id"):
+ return cfo
+
+ def __get_parsed_cfo_by_bpmn_element(self, elem):
+ elem_id = self.model.get_id(elem)
+ for parsed_cfo in self.sequence:
+ if parsed_cfo.get("id") == elem_id:
+ return parsed_cfo
+
+ def __find_transitive_closure(self, cfo, transitivity):
+ if cfo:
+ for successor in cfo.get("successor"):
+ successor_id = successor.get("id")
+ successor = self.__get_cfo_by_id(successor_id)
+ if successor:
+ if "is in gateway" not in successor:
+ transitivity.append(successor)
+ for successor in cfo.get("successor"):
+ successor_cfo = self.__get_cfo_by_id(successor.get("id"))
+ self.__find_transitive_closure(successor_cfo, transitivity)
+
+ def __add_transitivity(self):
+ for cfo in self.sequence:
+ transitivity = []
+ self.__find_transitive_closure(cfo, transitivity)
+ if transitivity:
+ cfo.update({"transitivity": transitivity})
+
+ def __parse(self):
+ for elem in self.model.get_diagram_elements():
+ cfo = self.__create_cfo(elem)
+ if cfo:
+ self.sequence.append(cfo)
+
+ def __create_cfo(self, elem):
+ if self.__valid_cfo_element(elem):
+ successor = self.__get_successors(elem)
+ predecessor = self.__get_predecessors(elem)
+
+ cfo = {
+ "name": self.__get_label(elem),
+ "type": self.model.get_element_type(elem),
+ "id": self.model.get_id(elem),
+ "successor": self.__format_list(successor),
+ "predecessor": self.__format_list(predecessor),
+ "is start": len(predecessor) == 0
+ or self.__is_predecessor_start_event(predecessor),
+ "is end": len(successor) == 0
+ or self.__is_successor_end_event(successor),
+ }
+
+ if self.__is_element_gateway(elem):
+ cfo.update(
+ {
+ "joining": len(self.model.get_outgoing_connection(elem)) == 1,
+ "splitting": len(self.model.get_outgoing_connection(elem)) >= 2,
+ }
+ )
+ if cfo["successor"]:
+ for successor in cfo["successor"]:
+ if successor.get("type") in ALLOWED_GATEWAYS:
+ elem_id = successor.get("id")
+ elem = self.__get_element_by_id(elem_id)
+ gateway_successors = self.__get_successors(elem)
+ successor.update(
+ {
+ "gateway successors": self.__format_list(
+ gateway_successors, True
+ )
+ }
+ )
+ return cfo
+
+ def __valid_cfo_element(self, elem):
+ if elem is None:
+ return False
+ if self.__is_element_activity(elem):
+ return True
+ if self.__is_element_gateway(elem):
+ return True
+ if self.__is_element_start_event(elem) and self.__valid_start_name(elem):
+ return True
+ if self.__is_element_end_event(elem) and self.__valid_end_name(elem):
+ return True
+ return False
+
+ def __valid_start_name(self, elem):
+ try:
+ start_name = self.model.get_name(elem)
+ if start_name in DISCARDED_START_EVENT_NAMES:
+ return False
+ if len(start_name.strip()) == 0:
+ return False
+ if len(start_name) < VALID_NAME_LENGTH:
+ return False
+ if start_name.isspace():
+ return False
+ except KeyError:
+ return False
+
+ def __valid_end_name(self, elem):
+ try:
+ end_name = self.model.get_name(elem)
+ if end_name in DISCARDED_END_EVENT_NAMES:
+ return False
+ if len(end_name.strip()) == 0:
+ return False
+ if len(end_name) < VALID_NAME_LENGTH:
+ return False
+ if end_name.isspace():
+ return False
+ except KeyError:
+ return False
+
+ def __get_successors(self, elem):
+ try:
+ connection_objects = self.model.get_outgoing_connection(elem)
+ if len(connection_objects) == 0:
+ return []
+ activities = []
+ if isinstance(connection_objects, str):
+ connection_objects = [connection_objects]
+ for connection in connection_objects:
+ if connection:
+ connection_id = (
+ self.model.get_id(connection[0])
+ if isinstance(connection, list)
+ else self.model.get_id(connection)
+ )
+ elem = self.__get_element_by_id(connection_id)
+ if self.model.get_element_type(elem) in ALLOWED_CONNECTING_OBJECTS:
+ connection = self.model.get_outgoing_connection(elem)
+ if connection:
+ elem = (
+ self.__get_element_by_id(
+ self.model.get_id(connection[0])
+ )
+ if isinstance(connection, list)
+ else self.__get_element_by_id(connection)
+ )
+ activities.append(elem)
+ return activities
+ except TypeError:
+ raise Exception
+
+ def __get_predecessors(self, current_elem):
+ predecessors = []
+ current_elem_id = self.model.get_id(current_elem)
+ try:
+ for elem in self.model.get_diagram_elements():
+ successors = self.__get_successors(elem)
+ if successors:
+ for successor in successors:
+ if successor:
+ if self.model.get_id(successor) == current_elem_id:
+ predecessors.append(elem)
+ except Exception:
+ raise Exception
+ return predecessors
+
+ def __format_list(self, elems, gateway=False):
+ formatted = []
+ for elem in elems:
+ if elem:
+ successors = self.__get_successors(elem)
+ cfo = {
+ "name": self.__get_label(elem),
+ "type": self.model.get_element_type(elem),
+ "id": self.model.get_id(elem),
+ "gateway successor": gateway,
+ "splitting": len(successors) >= 2,
+ "is end": len(successors) == 0
+ or self.__is_successor_end_event(successors),
+ }
+
+ try:
+ cfo.update({"splitting": len(self.__get_successors(elem)) >= 2})
+ except Exception:
+ pass
+ formatted.append(cfo)
+ return formatted
+
+ def __get_element_by_id(self, connection_id):
+ try:
+ return next(
+ e
+ for e in self.model.get_diagram_elements()
+ if self.model.get_id(e) == connection_id
+ )
+ except StopIteration:
+ raise Exception(f"Could not find element with ID {connection_id}")
+
+ def __get_activity_type(self, elem):
+ return ACTIVITY_MAPPING.get(self.model.get_element_type(elem), "Activity")
+
+ def __get_gateway_type(self, elem):
+ return GATEWAY_MAPPING.get(self.model.get_element_type(elem), "Gateway")
+
+ def __get_end_type(self, elem):
+ return END_EVENT_MAPPING.get(self.model.get_element_type(elem), "EndEvent")
+
+ def __get_label(self, elem):
+ try:
+ if self.__is_element_activity(elem):
+ try:
+ return self.sanitizer.sanitize_label(self.model.get_name(elem))
+ except KeyError:
+ return self.__get_activity_type(elem)
+ if self.__is_element_gateway(elem):
+ try:
+ return self.sanitizer.sanitize_label(self.model.get_name(elem))
+ except KeyError:
+ return self.__get_gateway_type(elem)
+ if self.__is_element_start_event(elem) or self.__is_element_end_event(elem):
+ try:
+ return self.sanitizer.sanitize_label(self.model.get_name(elem))
+ except KeyError:
+ return self.model.get_element_type(elem)
+ except KeyError:
+ return self.model.get_element_type(elem)
+
+ def __is_element_start_event(self, elem):
+ return self.model.get_element_type(elem) in ALLOWED_START_EVENTS
+
+ def __is_element_end_event(self, elem):
+ return self.model.get_element_type(elem) in ALLOWED_END_EVENTS
+
+ def __is_element_activity(self, elem):
+ return self.model.get_element_type(elem) in ALLOWED_ACTIVITIES
+
+ def __is_element_gateway(self, elem):
+ return self.model.get_element_type(elem) in ALLOWED_GATEWAYS
+
+ def __is_predecessor_start_event(self, predecessors):
+ for predecessor in predecessors:
+ if predecessor:
+ predecessor_type = self.model.get_element_type(predecessor)
+ if (
+ predecessor_type in ALLOWED_START_EVENTS
+ and predecessor_type not in DISCARDED_START_EVENT_NAMES
+ ):
+ if self.__valid_start_name(predecessor):
+ return False
+ return True
+ return False
+
+ def __is_successor_end_event(self, successors):
+ for successor in successors:
+ if successor:
+ if self.model.get_element_type(successor) in ALLOWED_END_EVENTS:
+ if self.__valid_end_name(successor):
+ return False
+ return True
+ return False
+
+ def count_parsable_elements(self):
+ count = 0
+ for elem in self.model.get_diagram_elements():
+ elem_type = self.model.get_element_type(elem)
+ if elem_type in ALLOWED_ACTIVITIES or elem_type in ALLOWED_GATEWAYS:
+ count += 1
+ return count
+
+ def count_model_elements(self):
+ return len(self.bpmn_model[CHILD_SHAPES])
+
+ def count_model_element_types(self):
+ return len(self.get_element_types())
+
+ def count_pools(self):
+ count = 0
+ for elem in self.bpmn_diagram[CHILD_SHAPES]:
+ if self.model.get_element_type(elem) == "Pool":
+ count += 1
+ return count
+
+ def has_start(self):
+ return any(elem.get("is start") for elem in self.sequence)
+
+ def get_element_types(self):
+ elem_types = {}
+
+ for elem in self.model.get_diagram_elements():
+ elem_type = self.model.get_element_type(elem)
+
+ if elem_type in elem_types:
+ elem_types[elem_type] += 1
+ else:
+ elem_types[elem_type] = 1
+ return elem_types
+
+ def contains_multiple_starts(self):
+ count = 0
+ for elem in self.model.get_diagram_elements():
+ if self.__is_element_start_event(elem):
+ count += 1
+ return count > 1
+
+ def or_multiple_paths(self):
+ for elem in self.model.get_diagram_elements():
+ if (
+ self.model.get_element_type(elem) == "InclusiveGateway"
+ and len(self.model.get_outgoing_connection(elem)) >= 3
+ ):
+ return True
+ return False
diff --git a/Declare4Py/Utils/bpmnconstraints/parser/json_model.py b/Declare4Py/Utils/bpmnconstraints/parser/json_model.py
new file mode 100644
index 00000000..783e4e33
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/parser/json_model.py
@@ -0,0 +1,26 @@
+from Declare4Py.Utils.bpmnconstraints.utils.constants import *
+
+class JsonModel:
+ def __init__(self, model) -> None:
+ self.model = model
+
+ def get_child_models(self):
+ return self.model[CHILD_SHAPES]
+
+ def get_element_type(self, elem):
+ return elem[STENCIL][ID].lower()
+
+ def get_diagram_elements(self):
+ try:
+ return self.get_child_models()
+ except KeyError:
+ raise Exception("Could not find any child elements to diagram.")
+
+ def get_outgoing_connection(self, elem):
+ return elem[OUTGOING]
+
+ def get_name(self, elem):
+ return elem[PROPERTIES][NAME]
+
+ def get_id(self, elem):
+ return elem[ELEMENT_ID]
diff --git a/Declare4Py/Utils/bpmnconstraints/parser/xml_model.py b/Declare4Py/Utils/bpmnconstraints/parser/xml_model.py
new file mode 100644
index 00000000..683b15f1
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/parser/xml_model.py
@@ -0,0 +1,67 @@
+from Declare4Py.Utils.bpmnconstraints.utils.constants import *
+from xml.etree import ElementTree
+import xmltodict as xtd
+
+PROCESS_ELEMENT = ".//{http://www.omg.org/spec/BPMN/20100524/MODEL}process"
+
+
+class XmlModel:
+ def __init__(self, model) -> None:
+ self.root = model
+ self.process_elements = self.root.find(PROCESS_ELEMENT)
+ self.child_elements = self.process_elements.findall("./*")
+
+ def __xml_to_dict(self, input_dict):
+ new_dict = {}
+ new_dict["outgoing"] = []
+ for tag_key in input_dict:
+ new_dict["type"] = tag_key.split(":")[1]
+ for key, value in input_dict[tag_key].items():
+ if key in ["ns0:extensionElements"]:
+ continue
+ if key.startswith("@"):
+ new_dict[key[1:]] = value
+ elif key.endswith(":outgoing"):
+ if isinstance(value, list):
+ new_dict["outgoing"].extend(value)
+ else:
+ new_dict["outgoing"].append(value)
+ else:
+ new_dict[key] = value
+ return new_dict
+
+ def get_child_models(self):
+ elements = []
+
+ for child in self.child_elements:
+ xml_string = ElementTree.tostring(child, encoding="utf-8")
+ parsed_xml = self.__xml_to_dict(xtd.parse(xml_string))
+ if parsed_xml["type"] == "extensionElements":
+ continue
+ elements.append(parsed_xml)
+ return elements
+
+ def get_element_type(self, elem):
+ return elem["type"].lower()
+
+ def get_diagram_elements(self):
+ try:
+ return self.get_child_models()
+ except KeyError:
+ raise Exception("Could not find any child elements to diagram.")
+
+ def get_outgoing_connection(self, elem):
+ if elem["type"] == "sequenceFlow":
+ return elem["targetRef"]
+ return elem["outgoing"]
+
+ def get_name(self, elem):
+ try:
+ return elem["name"]
+ except KeyError:
+ return elem["type"].lower()
+
+ def get_id(self, elem):
+ if isinstance(elem, str):
+ return elem
+ return elem["id"]
diff --git a/Declare4Py/Utils/bpmnconstraints/requirements.txt b/Declare4Py/Utils/bpmnconstraints/requirements.txt
new file mode 100644
index 00000000..3a9d0cb6
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/requirements.txt
@@ -0,0 +1,6 @@
+pylogics
+pandas
+matplotlib
+pytest
+tqdm
+xmltodict
\ No newline at end of file
diff --git a/Declare4Py/Utils/bpmnconstraints/templates/LTLf_templates.py b/Declare4Py/Utils/bpmnconstraints/templates/LTLf_templates.py
new file mode 100644
index 00000000..457f9548
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/templates/LTLf_templates.py
@@ -0,0 +1,89 @@
+from pylogics.syntax.base import And, Implies, Not, Or
+from pylogics.syntax.ltl import (
+ Always,
+ Eventually,
+ Next,
+ PropositionalTrue,
+ Atomic,
+)
+from pylogics.utils.to_string import to_string
+
+class LTLf:
+ def __init__(self) -> None:
+ pass
+
+
+ def init(self, element):
+ """{element} is the first to occur"""
+ return f"{element}"
+
+ def end(self, element):
+ """{element} is the last to occur"""
+ formula = Eventually(And(Atomic(element.replace(" ", "_")), Next(Not(PropositionalTrue()))))
+ return to_string(formula)
+
+ def precedence(self, predecessor, successor, return_formula=False):
+ pre_atom = Atomic(predecessor.replace(" ", "_"))
+ suc_atom = Atomic(successor.replace(" ", "_"))
+ # Replace Until with other logical constructs (if needed)
+ formula = Or(Or(Eventually(suc_atom), And(Not(pre_atom), suc_atom)), Always(Not(pre_atom)))
+ return formula if return_formula else to_string(formula)
+
+ def alternate_precedence(self, predecessor, successor, return_formula=False):
+ pre_atom = Atomic(predecessor.replace(" ", "_"))
+ suc_atom = Atomic(successor.replace(" ", "_"))
+ # Replace Until with other logical constructs
+ formula = Always(Implies(suc_atom, And(Next(Not(suc_atom)), Or(Eventually(pre_atom), And(Not(suc_atom), pre_atom)))))
+ return formula if return_formula else to_string(formula)
+
+ def response(self, predecessor, successor, return_formula=False):
+ pre_atom = Atomic(predecessor.replace(" ", "_"))
+ suc_atom = Atomic(successor.replace(" ", "_"))
+ formula = Always(Implies(pre_atom, Eventually(suc_atom)))
+ return formula if return_formula else to_string(formula)
+
+ def alternate_response(self, predecessor, successor, return_formula=False):
+ pre_atom = Atomic(predecessor.replace(" ", "_"))
+ suc_atom = Atomic(successor.replace(" ", "_"))
+ # Replace Until with other logical constructs
+ formula = Always(Implies(pre_atom, Next(Or(Eventually(suc_atom), And(Not(pre_atom), suc_atom)))))
+ return formula if return_formula else to_string(formula)
+
+ def chain_response(self, predecessor, successor, return_formula=False):
+ pre_atom = Atomic(predecessor.replace(" ", "_"))
+ suc_atom = Atomic(successor.replace(" ", "_"))
+ formula = Always(Implies(pre_atom, Next(suc_atom)))
+ return formula if return_formula else to_string(formula)
+
+ def succession(self, predecessor, successor):
+ precedence_formula = self.precedence(predecessor, successor, return_formula=True)
+ response_formula = self.response(predecessor, successor, return_formula=True)
+ combined_formula = And(response_formula, precedence_formula)
+ return to_string(combined_formula)
+
+ def alternate_succession(self, predecessor, successor):
+ alternate_precedence_formula = self.alternate_precedence(predecessor, successor, return_formula=True)
+ alternate_response_formula = self.alternate_response(predecessor, successor, return_formula=True)
+ combined_formula = And(alternate_response_formula, alternate_precedence_formula)
+ return to_string(combined_formula)
+
+ def chain_succession(self, predecessor, successor):
+ chain_response_formula = self.chain_response(predecessor, successor, return_formula=True)
+ chain_precedence_formula = self.precedence(predecessor, successor, return_formula=True)
+ combined_formula = And(chain_response_formula, chain_precedence_formula)
+ return to_string(combined_formula)
+
+ def choice(self, element_right, element_left):
+ right_atom = Atomic(element_right.replace(" ", "_"))
+ left_atom = Atomic(element_left.replace(" ", "_"))
+ return to_string(Or(Eventually(right_atom), Eventually(left_atom)))
+
+ def exclusive_choice(self, element_right, element_left):
+ right_atom = Atomic(element_right.replace(" ", "_"))
+ left_atom = Atomic(element_left.replace(" ", "_"))
+ return to_string(And(Or(Eventually(right_atom), Eventually(left_atom)), Not(And(Eventually(right_atom), Eventually(left_atom)))))
+
+ def co_existence(self, element_right, element_left):
+ right_atom = Atomic(element_right.replace(" ", "_"))
+ left_atom = Atomic(element_left.replace(" ", "_"))
+ return to_string(And(Eventually(right_atom), Eventually(left_atom)))
diff --git a/Declare4Py/Utils/bpmnconstraints/templates/__init__.py b/Declare4Py/Utils/bpmnconstraints/templates/__init__.py
new file mode 100644
index 00000000..e69de29b
diff --git a/Declare4Py/Utils/bpmnconstraints/templates/declare_templates.py b/Declare4Py/Utils/bpmnconstraints/templates/declare_templates.py
new file mode 100644
index 00000000..77c7d8dd
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/templates/declare_templates.py
@@ -0,0 +1,90 @@
+"""Functions to generate Declare constraints.
+"""
+
+
+class Declare:
+ def __init__(self) -> None:
+ pass
+
+ def init(self, element):
+ """{element} is the first to occur"""
+ return f"Init[{element}]"
+
+ def end(self, element):
+ """{element} is the last to occur"""
+ return f"End[{element}]"
+
+ def precedence(self, predecessor, successor):
+ """{successor} occurs only if it is preceded by {predecessor}. Activated by {successor}"""
+ return f"Precedence[{predecessor}, {successor}]"
+
+ def alternate_precedence(self, predecessor, successor):
+ """each time {successor} occurs, it is preceded by {predecessor} and no other {successor}
+ can recur in between. Activated by {successor}"""
+ return f"Alternate Precedence[{predecessor}, {successor}]"
+
+ def chain_precedence(self, predecessor, successor):
+ """
+ each time {successor} occurs, then {predecessor} occurs immediately beforehand.
+ Activated by {successor}
+ """
+ return f"Chain Precedence[{predecessor}, {successor}]"
+
+ def response(self, predecessor, successor):
+ """
+ if {predecessor} occurs, then {successor} occurs at some point after {predecessor}.
+ Activated by {predecessor}
+ """
+ return f"Response[{predecessor}, {successor}]"
+
+ def alternate_response(self, predecessor, successor):
+ """
+ if {predecessor} occurs, then {successor} occurs at some point after {predecessor}
+ and no other {predecessor} can recur in between. Activated by {predecessor}
+ """
+ return f"Alternate Response[{predecessor}, {successor}]"
+
+ def chain_response(self, predecessor, successor):
+ """
+ if {predecessor} occurs, then {successor} occurs immediately after {predecessor}
+ and no other {predecessor} can recur in between. Activated by {predecessor}
+ """
+ return f"Chain Response[{predecessor}, {successor}]"
+
+ def succession(self, predecessor, successor):
+ """
+ {predecessor} occurs if and only if it is followed by {successor}.
+ Activated by {predecessor} and {successor}
+ """
+ return f"Succession[{predecessor}, {successor}]"
+
+ def alternate_succession(self, predecessor, successor):
+ """{predecessor} occurs if and only if it is followed by {successor} and no other {predecessor}
+ can recur in between. Activated by {predecessor} and {successor}"""
+ return f"Alternate Succession[{predecessor}, {successor}]"
+
+ def chain_succession(self, predecessor, successor):
+ """{predecessor} occurs if and only if {successor} occurs immediately after {predecessor}.
+ Activated by {predecessor} and {successor}"""
+ return f"Chain Succession[{predecessor}, {successor}]"
+
+ def choice(self, element_right, element_left):
+ """
+ {element_right} or {element_left} or both eventually occur
+ in the same process instance (OR gateway).
+ Activated by {element_right} and {element_left}
+ """
+ return f"Choice[{element_left}, {element_right}]"
+
+ def exclusive_choice(self, element_right, element_left):
+ """
+ {element_right} or {element_left} occurs, but never both in the same process
+ instance (XOR gateway). Also called 'not co-existence'.
+ Activated by {element_right} and {element_left}
+ """
+ return f"Exclusive Choice[{element_left}, {element_right}]"
+
+ def co_existence(self, element_right, element_left):
+ """{element_right} and {element_left} occur in the same process instance (AND gateway).
+ Activated by {element_right} and {element_left}"""
+ return f"Co-Existence[{element_left}, {element_right}]"
diff --git a/Declare4Py/Utils/bpmnconstraints/templates/matching_templates.py b/Declare4Py/Utils/bpmnconstraints/templates/matching_templates.py
new file mode 100644
index 00000000..429f1fbd
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/templates/matching_templates.py
@@ -0,0 +1,79 @@
+"""Functions generating constraints as SIGNAL matches clauses according to
+ Declare constraints.
+"""
+
+
+class Signal:
+ def __init__(self) -> None:
+ pass
+
+ def init(self, element):
+ """{element} is the first to occur"""
+ return f"(^'{element}')"
+
+ def end(self, element):
+ """{element} is the last to occur"""
+ return f"('{element}'$)"
+
+ def precedence(self, predecessor, successor):
+ """{successor} occurs only if it is preceded by {predecessor}. Activated by {successor}"""
+ return f"(^ (NOT '{predecessor}' | ('{predecessor}' (NOT '{predecessor}')* '{successor}'))*$)"
+
+ def alternate_precedence(self, predecessor, successor):
+ """each time {successor} occurs, it is preceded by {predecessor} and no other
+ {successor} can recur in between. Activated by {successor}"""
+ return f"(^NOT('{successor}')*('{predecessor}' NOT('{successor}')*'{successor}'NOT('{successor}')*)*NOT('{successor}')*$)"
+
+ def chain_precedence(self, predecessor, successor):
+ """each time {successor} occurs, then {predecessor} occurs immediately beforehand.
+ Activated by {successor}"""
+ return f"(^NOT('{successor}')* ('{predecessor}' '{successor}'NOT('{successor}')*)*NOT('{successor}')*$)"
+
+ def response(self, predecessor, successor):
+ """if {predecessor} occurs, then {successor} occurs at some point after {predecessor}
+ Activated by {predecessor}"""
+ return f"(^NOT('{predecessor}')* ('{predecessor}' ANY*'{successor}')* NOT('{predecessor}')*$)"
+
+ def alternate_response(self, predecessor, successor):
+ """if {predecessor} occurs, then {successor} occurs at some point after
+ {predecessor} and no other {predecessor} can recur in between. Activated by {predecessor}
+ """
+ return f"(^NOT('{predecessor}')*('{predecessor}'NOT('{predecessor}')*'{successor}'NOT('{predecessor}')*)*NOT('{predecessor}')*$)"
+
+ def chain_response(self, predecessor, successor):
+ """if {predecessor} occurs, then {successor} occurs immediately after {predecessor}
+ and no other {predecessor} can recur in between. Activated by {predecessor}
+ """
+ return f"(^NOT('{predecessor}')* ('{predecessor}' '{successor}'NOT('{predecessor}')*)*NOT('{predecessor}')*$)"
+
+ def succession(self, predecessor, successor):
+ """{predecessor} occurs if and only if it is followed by {successor}.
+ Activated by {predecessor} and {successor}"""
+ return f"(^NOT('{predecessor}'|'{successor}')*('{predecessor}'~>'{successor}')*NOT('{predecessor}'|'{successor}')*$)"
+
+ def alternate_succession(self, predecessor, successor):
+ """{predecessor} occurs if and only if it is followed by {successor} and no other {predecessor}
+ can recur in between. Activated by {predecessor} and {successor}"""
+ return f"( ^ NOT('{predecessor}'|'{successor}')* ('{predecessor}'NOT('{predecessor}'|'{successor}')*'{successor}'NOT('{predecessor}'|'{successor}')*)*NOT('{predecessor}'|'{successor}')* $)"
+
+ def chain_succession(self, predecessor, successor):
+ """{predecessor} occurs if and only if {successor} occurs immediately after {predecessor}.
+ Activated by {predecessor} and {successor}"""
+ return f"(^NOT('{predecessor}'|'{successor}')* ('{predecessor}' '{successor}'NOT('{predecessor}'|'{successor}')*)*NOT('{predecessor}'|'{successor}')* $)"
+
+ def choice(self, element_right, element_left):
+ """{element_right} or {element_left} or both eventually occur
+ in the same process instance (OR gateway). Activated by {element_right} and {element_left}
+ """
+ return f"(('{element_right}'|'{element_left}'))"
+
+ def exclusive_choice(self, element_right, element_left):
+ """{element_right} or {element_left} occurs, but never both in the same
+ process instance (XOR gateway). Also called 'not co-existence'.
+ Activated by {element_right} and {element_left}"""
+ return f"(^(((NOT('{element_right}')*) ('{element_left}' NOT('{element_right}')*)*)|((NOT('{element_left}')*)('{element_right}' NOT('{element_left}')*)*))$)"
+
+ def co_existence(self, element_right, element_left):
+ """{element_right} and {element_left} occur in the same process instance (AND gateway).
+ Activated by {element_right} and {element_left}"""
+ return f"(^NOT('{element_right}'|'{element_left}')*(('{element_right}'ANY*'{element_left}'ANY*)|('{element_left}'ANY* '{element_right}' ANY*))* NOT('{element_right}'|'{element_left}')*$)"
diff --git a/Declare4Py/Utils/bpmnconstraints/tutorial/bpmn2constraints.ipynb b/Declare4Py/Utils/bpmnconstraints/tutorial/bpmn2constraints.ipynb
new file mode 100644
index 00000000..6f12232a
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/tutorial/bpmn2constraints.ipynb
@@ -0,0 +1,942 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "1d64a8b9a01f2d29",
+ "metadata": {
+ "collapsed": false
+ },
+ "source": [
+ "Bpmn2constraints is made to compile BPMN models from both `JSON` and `XML`, but since `JSON` models are proprietary to SAP Signavio, only `XML` support have been added in this repository. Go to [the original repository](https://github.com/signavio/bpmn2constraints) for the full version. \n",
+ "\n",
+ "In order to start using the tool, import the necessary packages."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "initial_id",
+ "metadata": {
+ "ExecuteTime": {
+ "end_time": "2023-11-29T13:02:59.781359787Z",
+ "start_time": "2023-11-29T13:02:58.421541843Z"
+ },
+ "collapsed": true
+ },
+ "outputs": [
+ {
+ "name": "stderr",
+ "output_type": "stream",
+ "text": [
+ "/home/fleph/sap/Declare4Py/.venv/lib64/python3.11/site-packages/lark/utils.py:163: DeprecationWarning: module 'sre_parse' is deprecated\n",
+ " import sre_parse\n",
+ "/home/fleph/sap/Declare4Py/.venv/lib64/python3.11/site-packages/lark/utils.py:164: DeprecationWarning: module 'sre_constants' is deprecated\n",
+ " import sre_constants\n"
+ ]
+ }
+ ],
+ "source": [
+ "import os\n",
+ "from Declare4Py.ProcessModels.BpmnConstraintsModel import BpmnConstraintsModel"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "a97f59b17a709f11",
+ "metadata": {
+ "collapsed": false
+ },
+ "source": [
+ "Some examples are provided in this repository, such as this linear sequence: \n",
+ "\n",
+ " ![](\"data/linear_diagram.png\")
\n",
+ "\n",
+ "\n",
+ "With bpmn2constraints, this diagram can be translated into DECLARE constraints, such as:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "id": "68aaff03d9d70600",
+ "metadata": {
+ "ExecuteTime": {
+ "end_time": "2023-11-29T13:02:59.918794770Z",
+ "start_time": "2023-11-29T13:02:59.781210072Z"
+ },
+ "collapsed": false
+ },
+ "outputs": [
+ {
+ "name": "stderr",
+ "output_type": "stream",
+ "text": [
+ "WARNING:root:Provided path is not a file: ../examples/linear/linear_sequence.xml\n"
+ ]
+ },
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "Model activities:\n",
+ "-----------------\n",
+ "\n",
+ "\n",
+ "Model constraints:\n",
+ "-----------------\n"
+ ]
+ }
+ ],
+ "source": [
+ "path = os.path.join(\"data\",\"linear_sequence.xml\")\n",
+ "model = BpmnConstraintsModel()\n",
+ "model.parse_from_file(path)\n",
+ "declare_model = model.declare_model\n",
+ "constraints = declare_model.get_decl_model_constraints()\n",
+ "activities = declare_model.get_model_activities()\n",
+ "print(\"Model activities:\")\n",
+ "print(\"-----------------\")\n",
+ "for idx, act in enumerate(activities):\n",
+ " print(idx, act)\n",
+ "print(\"\\n\")\n",
+ "print(\"Model constraints:\")\n",
+ "print(\"-----------------\")\n",
+ "for idx, con in enumerate(constraints):\n",
+ " print(idx, con)\n",
+ "\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "5ad92927",
+ "metadata": {},
+ "source": [
+ "The BpmnConstraintsModel class contains constraints as LTLf as well.\n",
+ "\n",
+ "The LTLf formulas are stored in a class containing:\n",
+ "```formula```, ```parsed_formula``` and ```is_satisfiable```\n",
+ "\n",
+ "Or the result can be easily printed such as:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "id": "9c65a09f",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "for ltl_mod in (model.ltl_model):\n",
+ " print(ltl_mod.formula)\n",
+ " print(ltl_mod.parsed_formula)\n",
+ " print(f'Is satisfiable? {ltl_mod.check_satisfiability()}\\n')\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "bb69acce",
+ "metadata": {},
+ "source": [
+ "The following blocks are bigger and more complex examples of usage of bpmn2constraints. Based on a bpmn diagram from the Sepsis Cases event log.\n",
+ "\n",
+ "\n",
+ " ![](\"data/Sepsis)
\n",
+ ""
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "id": "b4f22f5abf341228",
+ "metadata": {
+ "ExecuteTime": {
+ "end_time": "2023-11-29T13:03:04.894479074Z",
+ "start_time": "2023-11-29T13:03:00.056992740Z"
+ },
+ "collapsed": false
+ },
+ "outputs": [
+ {
+ "ename": "KeyboardInterrupt",
+ "evalue": "",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
+ "\u001b[0;31mKeyboardInterrupt\u001b[0m Traceback (most recent call last)",
+ "Cell \u001b[0;32mIn[4], line 3\u001b[0m\n\u001b[1;32m 1\u001b[0m path \u001b[38;5;241m=\u001b[39m \u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mdata/Sepsis Cases.xml\u001b[39m\u001b[38;5;124m\"\u001b[39m \u001b[38;5;66;03m#Path to data \u001b[39;00m\n\u001b[1;32m 2\u001b[0m model \u001b[38;5;241m=\u001b[39m BpmnConstraintsModel()\n\u001b[0;32m----> 3\u001b[0m \u001b[43mmodel\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mparse_from_file\u001b[49m\u001b[43m(\u001b[49m\u001b[43mmodel_path\u001b[49m\u001b[38;5;241;43m=\u001b[39;49m\u001b[43mpath\u001b[49m\u001b[43m)\u001b[49m \n\u001b[1;32m 5\u001b[0m declare_model \u001b[38;5;241m=\u001b[39m model\u001b[38;5;241m.\u001b[39mdeclare_model\n\u001b[1;32m 6\u001b[0m constraints \u001b[38;5;241m=\u001b[39m declare_model\u001b[38;5;241m.\u001b[39mget_decl_model_constraints()\n",
+ "File \u001b[0;32m~/sap/Declare4Py/Declare4Py/ProcessModels/BpmnConstraintsModel.py:35\u001b[0m, in \u001b[0;36mBpmnConstraintsModel.parse_from_file\u001b[0;34m(self, model_path, **kwargs)\u001b[0m\n\u001b[1;32m 32\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m\n\u001b[1;32m 33\u001b[0m \u001b[38;5;28;01mtry\u001b[39;00m:\n\u001b[1;32m 34\u001b[0m \u001b[38;5;66;03m# Parsing and compiling the BPMN constraints\u001b[39;00m\n\u001b[0;32m---> 35\u001b[0m parsed_result \u001b[38;5;241m=\u001b[39m \u001b[43mParser\u001b[49m\u001b[43m(\u001b[49m\u001b[43mxml_path\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;28;43;01mTrue\u001b[39;49;00m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43mtransitivity\u001b[49m\u001b[38;5;241;43m=\u001b[39;49m\u001b[38;5;28;43;01mFalse\u001b[39;49;00m\u001b[43m)\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mrun\u001b[49m\u001b[43m(\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 36\u001b[0m compiled_result \u001b[38;5;241m=\u001b[39m Compiler(parsed_result, transitivity\u001b[38;5;241m=\u001b[39m\u001b[38;5;28;01mTrue\u001b[39;00m, skip_named_gateways\u001b[38;5;241m=\u001b[39m\u001b[38;5;28;01mFalse\u001b[39;00m)\u001b[38;5;241m.\u001b[39mrun()\n\u001b[1;32m 38\u001b[0m \u001b[38;5;66;03m# Extract DECLARE and LTLf constraints\u001b[39;00m\n",
+ "File \u001b[0;32m~/sap/Declare4Py/Declare4Py/Utils/bpmnconstraints/parser/bpmn_parser.py:58\u001b[0m, in \u001b[0;36mParser.run\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 56\u001b[0m \u001b[38;5;28;01melse\u001b[39;00m:\n\u001b[1;32m 57\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mmodel \u001b[38;5;241m=\u001b[39m XmlModel(\u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mbpmn_model)\n\u001b[0;32m---> 58\u001b[0m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43m__parse\u001b[49m\u001b[43m(\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 59\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39m__mark_gateway_elements()\n\u001b[1;32m 60\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mtransitivity:\n",
+ "File \u001b[0;32m~/sap/Declare4Py/Declare4Py/Utils/bpmnconstraints/parser/bpmn_parser.py:137\u001b[0m, in \u001b[0;36mParser.__parse\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 135\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21m__parse\u001b[39m(\u001b[38;5;28mself\u001b[39m):\n\u001b[1;32m 136\u001b[0m \u001b[38;5;28;01mfor\u001b[39;00m elem \u001b[38;5;129;01min\u001b[39;00m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mmodel\u001b[38;5;241m.\u001b[39mget_diagram_elements():\n\u001b[0;32m--> 137\u001b[0m cfo \u001b[38;5;241m=\u001b[39m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43m__create_cfo\u001b[49m\u001b[43m(\u001b[49m\u001b[43melem\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 138\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m cfo:\n\u001b[1;32m 139\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39msequence\u001b[38;5;241m.\u001b[39mappend(cfo)\n",
+ "File \u001b[0;32m~/sap/Declare4Py/Declare4Py/Utils/bpmnconstraints/parser/bpmn_parser.py:173\u001b[0m, in \u001b[0;36mParser.__create_cfo\u001b[0;34m(self, elem)\u001b[0m\n\u001b[1;32m 169\u001b[0m elem \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39m__get_element_by_id(elem_id)\n\u001b[1;32m 170\u001b[0m gateway_successors \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39m__get_successors(elem)\n\u001b[1;32m 171\u001b[0m successor\u001b[38;5;241m.\u001b[39mupdate(\n\u001b[1;32m 172\u001b[0m {\n\u001b[0;32m--> 173\u001b[0m \u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mgateway successors\u001b[39m\u001b[38;5;124m\"\u001b[39m: \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43m__format_list\u001b[49m\u001b[43m(\u001b[49m\n\u001b[1;32m 174\u001b[0m \u001b[43m \u001b[49m\u001b[43mgateway_successors\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;28;43;01mTrue\u001b[39;49;00m\n\u001b[1;32m 175\u001b[0m \u001b[43m \u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 176\u001b[0m }\n\u001b[1;32m 177\u001b[0m )\n\u001b[1;32m 178\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m cfo\n",
+ "File \u001b[0;32m~/sap/Declare4Py/Declare4Py/Utils/bpmnconstraints/parser/bpmn_parser.py:271\u001b[0m, in \u001b[0;36mParser.__format_list\u001b[0;34m(self, elems, gateway)\u001b[0m\n\u001b[1;32m 269\u001b[0m \u001b[38;5;28;01mfor\u001b[39;00m elem \u001b[38;5;129;01min\u001b[39;00m elems:\n\u001b[1;32m 270\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m elem:\n\u001b[0;32m--> 271\u001b[0m successors \u001b[38;5;241m=\u001b[39m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43m__get_successors\u001b[49m\u001b[43m(\u001b[49m\u001b[43melem\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 272\u001b[0m cfo \u001b[38;5;241m=\u001b[39m {\n\u001b[1;32m 273\u001b[0m \u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mname\u001b[39m\u001b[38;5;124m\"\u001b[39m: \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39m__get_label(elem),\n\u001b[1;32m 274\u001b[0m \u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mtype\u001b[39m\u001b[38;5;124m\"\u001b[39m: \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mmodel\u001b[38;5;241m.\u001b[39mget_element_type(elem),\n\u001b[0;32m (...)\u001b[0m\n\u001b[1;32m 279\u001b[0m \u001b[38;5;129;01mor\u001b[39;00m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39m__is_successor_end_event(successors),\n\u001b[1;32m 280\u001b[0m }\n\u001b[1;32m 282\u001b[0m \u001b[38;5;28;01mtry\u001b[39;00m:\n",
+ "File \u001b[0;32m~/sap/Declare4Py/Declare4Py/Utils/bpmnconstraints/parser/bpmn_parser.py:245\u001b[0m, in \u001b[0;36mParser.__get_successors\u001b[0;34m(self, elem)\u001b[0m\n\u001b[1;32m 238\u001b[0m connection \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mmodel\u001b[38;5;241m.\u001b[39mget_outgoing_connection(elem)\n\u001b[1;32m 239\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m connection:\n\u001b[1;32m 240\u001b[0m elem \u001b[38;5;241m=\u001b[39m (\n\u001b[1;32m 241\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39m__get_element_by_id(\n\u001b[1;32m 242\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mmodel\u001b[38;5;241m.\u001b[39mget_id(connection[\u001b[38;5;241m0\u001b[39m])\n\u001b[1;32m 243\u001b[0m )\n\u001b[1;32m 244\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28misinstance\u001b[39m(connection, \u001b[38;5;28mlist\u001b[39m)\n\u001b[0;32m--> 245\u001b[0m \u001b[38;5;28;01melse\u001b[39;00m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43m__get_element_by_id\u001b[49m\u001b[43m(\u001b[49m\u001b[43mconnection\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 246\u001b[0m )\n\u001b[1;32m 247\u001b[0m activities\u001b[38;5;241m.\u001b[39mappend(elem)\n\u001b[1;32m 248\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m activities\n",
+ "File \u001b[0;32m~/sap/Declare4Py/Declare4Py/Utils/bpmnconstraints/parser/bpmn_parser.py:293\u001b[0m, in \u001b[0;36mParser.__get_element_by_id\u001b[0;34m(self, connection_id)\u001b[0m\n\u001b[1;32m 289\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21m__get_element_by_id\u001b[39m(\u001b[38;5;28mself\u001b[39m, connection_id):\n\u001b[1;32m 290\u001b[0m \u001b[38;5;28;01mtry\u001b[39;00m:\n\u001b[1;32m 291\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m \u001b[38;5;28mnext\u001b[39m(\n\u001b[1;32m 292\u001b[0m e\n\u001b[0;32m--> 293\u001b[0m \u001b[38;5;28;01mfor\u001b[39;00m e \u001b[38;5;129;01min\u001b[39;00m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mmodel\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mget_diagram_elements\u001b[49m\u001b[43m(\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 294\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mmodel\u001b[38;5;241m.\u001b[39mget_id(e) \u001b[38;5;241m==\u001b[39m connection_id\n\u001b[1;32m 295\u001b[0m )\n\u001b[1;32m 296\u001b[0m \u001b[38;5;28;01mexcept\u001b[39;00m \u001b[38;5;167;01mStopIteration\u001b[39;00m:\n\u001b[1;32m 297\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mException\u001b[39;00m(\u001b[38;5;124mf\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mCould not find element with ID \u001b[39m\u001b[38;5;132;01m{\u001b[39;00mconnection_id\u001b[38;5;132;01m}\u001b[39;00m\u001b[38;5;124m\"\u001b[39m)\n",
+ "File \u001b[0;32m~/sap/Declare4Py/Declare4Py/Utils/bpmnconstraints/parser/xml_model.py:49\u001b[0m, in \u001b[0;36mXmlModel.get_diagram_elements\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 47\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21mget_diagram_elements\u001b[39m(\u001b[38;5;28mself\u001b[39m):\n\u001b[1;32m 48\u001b[0m \u001b[38;5;28;01mtry\u001b[39;00m:\n\u001b[0;32m---> 49\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m \u001b[38;5;28;43mself\u001b[39;49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mget_child_models\u001b[49m\u001b[43m(\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 50\u001b[0m \u001b[38;5;28;01mexcept\u001b[39;00m \u001b[38;5;167;01mKeyError\u001b[39;00m:\n\u001b[1;32m 51\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mException\u001b[39;00m(\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mCould not find any child elements to diagram.\u001b[39m\u001b[38;5;124m\"\u001b[39m)\n",
+ "File \u001b[0;32m~/sap/Declare4Py/Declare4Py/Utils/bpmnconstraints/parser/xml_model.py:38\u001b[0m, in \u001b[0;36mXmlModel.get_child_models\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 36\u001b[0m \u001b[38;5;28;01mfor\u001b[39;00m child \u001b[38;5;129;01min\u001b[39;00m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mchild_elements:\n\u001b[1;32m 37\u001b[0m xml_string \u001b[38;5;241m=\u001b[39m ElementTree\u001b[38;5;241m.\u001b[39mtostring(child, encoding\u001b[38;5;241m=\u001b[39m\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mutf-8\u001b[39m\u001b[38;5;124m\"\u001b[39m)\n\u001b[0;32m---> 38\u001b[0m parsed_xml \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39m__xml_to_dict(\u001b[43mxtd\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mparse\u001b[49m\u001b[43m(\u001b[49m\u001b[43mxml_string\u001b[49m\u001b[43m)\u001b[49m)\n\u001b[1;32m 39\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m parsed_xml[\u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mtype\u001b[39m\u001b[38;5;124m\"\u001b[39m] \u001b[38;5;241m==\u001b[39m \u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mextensionElements\u001b[39m\u001b[38;5;124m\"\u001b[39m:\n\u001b[1;32m 40\u001b[0m \u001b[38;5;28;01mcontinue\u001b[39;00m\n",
+ "File \u001b[0;32m~/sap/Declare4Py/.venv/lib64/python3.11/site-packages/xmltodict.py:378\u001b[0m, in \u001b[0;36mparse\u001b[0;34m(xml_input, encoding, expat, process_namespaces, namespace_separator, disable_entities, process_comments, **kwargs)\u001b[0m\n\u001b[1;32m 376\u001b[0m parser\u001b[38;5;241m.\u001b[39mParse(\u001b[38;5;124mb\u001b[39m\u001b[38;5;124m'\u001b[39m\u001b[38;5;124m'\u001b[39m,\u001b[38;5;28;01mTrue\u001b[39;00m)\n\u001b[1;32m 377\u001b[0m \u001b[38;5;28;01melse\u001b[39;00m:\n\u001b[0;32m--> 378\u001b[0m \u001b[43mparser\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mParse\u001b[49m\u001b[43m(\u001b[49m\u001b[43mxml_input\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;28;43;01mTrue\u001b[39;49;00m\u001b[43m)\u001b[49m\n\u001b[1;32m 379\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m handler\u001b[38;5;241m.\u001b[39mitem\n",
+ "File \u001b[0;32m/builddir/build/BUILD/Python-3.11.6/Modules/pyexpat.c:468\u001b[0m, in \u001b[0;36mEndElement\u001b[0;34m()\u001b[0m\n",
+ "File \u001b[0;32m~/sap/Declare4Py/.venv/lib64/python3.11/site-packages/xmltodict.py:128\u001b[0m, in \u001b[0;36m_DictSAXHandler.endElement\u001b[0;34m(self, full_name)\u001b[0m\n\u001b[1;32m 125\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mitem \u001b[38;5;241m=\u001b[39m attrs \u001b[38;5;129;01mor\u001b[39;00m \u001b[38;5;28;01mNone\u001b[39;00m\n\u001b[1;32m 126\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mdata \u001b[38;5;241m=\u001b[39m []\n\u001b[0;32m--> 128\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21mendElement\u001b[39m(\u001b[38;5;28mself\u001b[39m, full_name):\n\u001b[1;32m 129\u001b[0m name \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39m_build_name(full_name)\n\u001b[1;32m 130\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28mlen\u001b[39m(\u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mpath) \u001b[38;5;241m==\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mitem_depth:\n",
+ "\u001b[0;31mKeyboardInterrupt\u001b[0m: "
+ ]
+ }
+ ],
+ "source": [
+ "path = \"data/Sepsis Cases.xml\" #Path to data \n",
+ "model = BpmnConstraintsModel()\n",
+ "model.parse_from_file(model_path=path) \n",
+ "\n",
+ "declare_model = model.declare_model\n",
+ "constraints = declare_model.get_decl_model_constraints()\n",
+ "activities = declare_model.get_model_activities()\n",
+ "\n",
+ "print(\"Model activities:\")\n",
+ "print(\"-----------------\")\n",
+ "for idx, act in enumerate(activities):\n",
+ " print(idx, act)\n",
+ "print(\"\\n\")\n",
+ "print(\"Model constraints:\")\n",
+ "print(\"-----------------\")\n",
+ "for idx, con in enumerate(constraints):\n",
+ " print(idx, con)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "con_erregistration\n",
+ "con_erregistration\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(G((con_ertriage) -> (F(con_ersepsistriage)))) & ((F(con_ersepsistriage)) | ((~(con_ertriage)) & (con_ersepsistriage)) | (G(~(con_ertriage))))\n",
+ "(and (always (implies con_ertriage (eventually con_ersepsistriage))) (or (eventually con_ersepsistriage) (and (not con_ertriage) con_ersepsistriage) (always (not con_ertriage))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_ertriage)) & (F(con_ersepsistriage))\n",
+ "(and (eventually con_ertriage) (eventually con_ersepsistriage))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(G((con_ertriage) -> (X[!]((F(con_ersepsistriage)) | ((~(con_ertriage)) & (con_ersepsistriage)))))) & (G((con_ersepsistriage) -> ((X[!](~(con_ersepsistriage))) & ((F(con_ertriage)) | ((~(con_ersepsistriage)) & (con_ertriage))))))\n",
+ "(and (always (implies con_ertriage (next (or (eventually con_ersepsistriage) (and (not con_ertriage) con_ersepsistriage))))) (always (implies con_ersepsistriage (and (next (not con_ersepsistriage)) (or (eventually con_ertriage) (and (not con_ersepsistriage) con_ertriage))))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "F((con_releasea) & (X[!](false)))\n",
+ "(eventually (and con_releasea (next false)))\n",
+ "Is satisfiable? False\n",
+ "\n",
+ "F((con_releaseb) & (X[!](false)))\n",
+ "(eventually (and con_releaseb (next false)))\n",
+ "Is satisfiable? False\n",
+ "\n",
+ "F((con_releasec) & (X[!](false)))\n",
+ "(eventually (and con_releasec (next false)))\n",
+ "Is satisfiable? False\n",
+ "\n",
+ "F((con_released) & (X[!](false)))\n",
+ "(eventually (and con_released (next false)))\n",
+ "Is satisfiable? False\n",
+ "\n",
+ "F((con_releasee) & (X[!](false)))\n",
+ "(eventually (and con_releasee (next false)))\n",
+ "Is satisfiable? False\n",
+ "\n",
+ "F((con_returner) & (X[!](false)))\n",
+ "(eventually (and con_returner (next false)))\n",
+ "Is satisfiable? False\n",
+ "\n",
+ "(F(con_leucocytes)) & (F(con_crp))\n",
+ "(and (eventually con_leucocytes) (eventually con_crp))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_leucocytes)) & (F(con_ertriage))\n",
+ "(and (eventually con_leucocytes) (eventually con_ertriage))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_leucocytes)) & (F(con_lacticacid))\n",
+ "(and (eventually con_leucocytes) (eventually con_lacticacid))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_crp)) & (F(con_ertriage))\n",
+ "(and (eventually con_crp) (eventually con_ertriage))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_crp)) & (F(con_lacticacid))\n",
+ "(and (eventually con_crp) (eventually con_lacticacid))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_ertriage)) & (F(con_lacticacid))\n",
+ "(and (eventually con_ertriage) (eventually con_lacticacid))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_leucocytes)) | ((~(con_erregistration)) & (con_leucocytes)) | (G(~(con_erregistration)))\n",
+ "(or (eventually con_leucocytes) (and (not con_erregistration) con_leucocytes) (always (not con_erregistration)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_leucocytes) -> ((X[!](~(con_leucocytes))) & ((F(con_erregistration)) | ((~(con_leucocytes)) & (con_erregistration)))))\n",
+ "(always (implies con_leucocytes (and (next (not con_leucocytes)) (or (eventually con_erregistration) (and (not con_leucocytes) con_erregistration)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_crp)) | ((~(con_erregistration)) & (con_crp)) | (G(~(con_erregistration)))\n",
+ "(or (eventually con_crp) (and (not con_erregistration) con_crp) (always (not con_erregistration)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_crp) -> ((X[!](~(con_crp))) & ((F(con_erregistration)) | ((~(con_crp)) & (con_erregistration)))))\n",
+ "(always (implies con_crp (and (next (not con_crp)) (or (eventually con_erregistration) (and (not con_crp) con_erregistration)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_ertriage)) | ((~(con_erregistration)) & (con_ertriage)) | (G(~(con_erregistration)))\n",
+ "(or (eventually con_ertriage) (and (not con_erregistration) con_ertriage) (always (not con_erregistration)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_ertriage) -> ((X[!](~(con_ertriage))) & ((F(con_erregistration)) | ((~(con_ertriage)) & (con_erregistration)))))\n",
+ "(always (implies con_ertriage (and (next (not con_ertriage)) (or (eventually con_erregistration) (and (not con_ertriage) con_erregistration)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_lacticacid)) | ((~(con_erregistration)) & (con_lacticacid)) | (G(~(con_erregistration)))\n",
+ "(or (eventually con_lacticacid) (and (not con_erregistration) con_lacticacid) (always (not con_erregistration)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_lacticacid) -> ((X[!](~(con_lacticacid))) & ((F(con_erregistration)) | ((~(con_lacticacid)) & (con_erregistration)))))\n",
+ "(always (implies con_lacticacid (and (next (not con_lacticacid)) (or (eventually con_erregistration) (and (not con_lacticacid) con_erregistration)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_ivantibiotics)) & (F(con_ivliquid))\n",
+ "(and (eventually con_ivantibiotics) (eventually con_ivliquid))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_ivantibiotics)) | ((~(con_ersepsistriage)) & (con_ivantibiotics)) | (G(~(con_ersepsistriage)))\n",
+ "(or (eventually con_ivantibiotics) (and (not con_ersepsistriage) con_ivantibiotics) (always (not con_ersepsistriage)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_ivantibiotics) -> ((X[!](~(con_ivantibiotics))) & ((F(con_ersepsistriage)) | ((~(con_ivantibiotics)) & (con_ersepsistriage)))))\n",
+ "(always (implies con_ivantibiotics (and (next (not con_ivantibiotics)) (or (eventually con_ersepsistriage) (and (not con_ivantibiotics) con_ersepsistriage)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_ivliquid)) | ((~(con_ersepsistriage)) & (con_ivliquid)) | (G(~(con_ersepsistriage)))\n",
+ "(or (eventually con_ivliquid) (and (not con_ersepsistriage) con_ivliquid) (always (not con_ersepsistriage)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_ivliquid) -> ((X[!](~(con_ivliquid))) & ((F(con_ersepsistriage)) | ((~(con_ivliquid)) & (con_ersepsistriage)))))\n",
+ "(always (implies con_ivliquid (and (next (not con_ivliquid)) (or (eventually con_ersepsistriage) (and (not con_ivliquid) con_ersepsistriage)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_ivantibiotics) -> (F(con_admissionnc)))\n",
+ "(always (implies con_ivantibiotics (eventually con_admissionnc)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_ivantibiotics) -> (X[!]((F(con_admissionnc)) | ((~(con_ivantibiotics)) & (con_admissionnc)))))\n",
+ "(always (implies con_ivantibiotics (next (or (eventually con_admissionnc) (and (not con_ivantibiotics) con_admissionnc)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_ivantibiotics) -> (F(con_admissionic)))\n",
+ "(always (implies con_ivantibiotics (eventually con_admissionic)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_ivantibiotics) -> (X[!]((F(con_admissionic)) | ((~(con_ivantibiotics)) & (con_admissionic)))))\n",
+ "(always (implies con_ivantibiotics (next (or (eventually con_admissionic) (and (not con_ivantibiotics) con_admissionic)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_ivliquid) -> (F(con_admissionnc)))\n",
+ "(always (implies con_ivliquid (eventually con_admissionnc)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_ivliquid) -> (X[!]((F(con_admissionnc)) | ((~(con_ivliquid)) & (con_admissionnc)))))\n",
+ "(always (implies con_ivliquid (next (or (eventually con_admissionnc) (and (not con_ivliquid) con_admissionnc)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_ivliquid) -> (F(con_admissionic)))\n",
+ "(always (implies con_ivliquid (eventually con_admissionic)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_ivliquid) -> (X[!]((F(con_admissionic)) | ((~(con_ivliquid)) & (con_admissionic)))))\n",
+ "(always (implies con_ivliquid (next (or (eventually con_admissionic) (and (not con_ivliquid) con_admissionic)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_admissionnc)) | (F(con_admissionic))) & (~((F(con_admissionnc)) & (F(con_admissionic))))\n",
+ "(and (or (eventually con_admissionnc) (eventually con_admissionic)) (not (and (eventually con_admissionnc) (eventually con_admissionic))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_admissionnc)) | (F(con_admissionic))\n",
+ "(or (eventually con_admissionnc) (eventually con_admissionic))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_lacticacid) -> (F(con_releasea)))\n",
+ "(always (implies con_lacticacid (eventually con_releasea)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_lacticacid) -> (X[!]((F(con_releasea)) | ((~(con_lacticacid)) & (con_releasea)))))\n",
+ "(always (implies con_lacticacid (next (or (eventually con_releasea) (and (not con_lacticacid) con_releasea)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_lacticacid) -> (F(con_releaseb)))\n",
+ "(always (implies con_lacticacid (eventually con_releaseb)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_lacticacid) -> (X[!]((F(con_releaseb)) | ((~(con_lacticacid)) & (con_releaseb)))))\n",
+ "(always (implies con_lacticacid (next (or (eventually con_releaseb) (and (not con_lacticacid) con_releaseb)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_lacticacid) -> (F(con_released)))\n",
+ "(always (implies con_lacticacid (eventually con_released)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_lacticacid) -> (X[!]((F(con_released)) | ((~(con_lacticacid)) & (con_released)))))\n",
+ "(always (implies con_lacticacid (next (or (eventually con_released) (and (not con_lacticacid) con_released)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_lacticacid) -> (F(con_returner)))\n",
+ "(always (implies con_lacticacid (eventually con_returner)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_lacticacid) -> (X[!]((F(con_returner)) | ((~(con_lacticacid)) & (con_returner)))))\n",
+ "(always (implies con_lacticacid (next (or (eventually con_returner) (and (not con_lacticacid) con_returner)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_lacticacid) -> (F(con_releasec)))\n",
+ "(always (implies con_lacticacid (eventually con_releasec)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_lacticacid) -> (X[!]((F(con_releasec)) | ((~(con_lacticacid)) & (con_releasec)))))\n",
+ "(always (implies con_lacticacid (next (or (eventually con_releasec) (and (not con_lacticacid) con_releasec)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_lacticacid) -> (F(con_releasee)))\n",
+ "(always (implies con_lacticacid (eventually con_releasee)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_lacticacid) -> (X[!]((F(con_releasee)) | ((~(con_lacticacid)) & (con_releasee)))))\n",
+ "(always (implies con_lacticacid (next (or (eventually con_releasee) (and (not con_lacticacid) con_releasee)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_leucocytes) -> (F(con_releasea)))\n",
+ "(always (implies con_leucocytes (eventually con_releasea)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_leucocytes) -> (X[!]((F(con_releasea)) | ((~(con_leucocytes)) & (con_releasea)))))\n",
+ "(always (implies con_leucocytes (next (or (eventually con_releasea) (and (not con_leucocytes) con_releasea)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_leucocytes) -> (F(con_releaseb)))\n",
+ "(always (implies con_leucocytes (eventually con_releaseb)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_leucocytes) -> (X[!]((F(con_releaseb)) | ((~(con_leucocytes)) & (con_releaseb)))))\n",
+ "(always (implies con_leucocytes (next (or (eventually con_releaseb) (and (not con_leucocytes) con_releaseb)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_leucocytes) -> (F(con_released)))\n",
+ "(always (implies con_leucocytes (eventually con_released)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_leucocytes) -> (X[!]((F(con_released)) | ((~(con_leucocytes)) & (con_released)))))\n",
+ "(always (implies con_leucocytes (next (or (eventually con_released) (and (not con_leucocytes) con_released)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_leucocytes) -> (F(con_returner)))\n",
+ "(always (implies con_leucocytes (eventually con_returner)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_leucocytes) -> (X[!]((F(con_returner)) | ((~(con_leucocytes)) & (con_returner)))))\n",
+ "(always (implies con_leucocytes (next (or (eventually con_returner) (and (not con_leucocytes) con_returner)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_leucocytes) -> (F(con_releasec)))\n",
+ "(always (implies con_leucocytes (eventually con_releasec)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_leucocytes) -> (X[!]((F(con_releasec)) | ((~(con_leucocytes)) & (con_releasec)))))\n",
+ "(always (implies con_leucocytes (next (or (eventually con_releasec) (and (not con_leucocytes) con_releasec)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_leucocytes) -> (F(con_releasee)))\n",
+ "(always (implies con_leucocytes (eventually con_releasee)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_leucocytes) -> (X[!]((F(con_releasee)) | ((~(con_leucocytes)) & (con_releasee)))))\n",
+ "(always (implies con_leucocytes (next (or (eventually con_releasee) (and (not con_leucocytes) con_releasee)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_crp) -> (F(con_releasea)))\n",
+ "(always (implies con_crp (eventually con_releasea)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_crp) -> (X[!]((F(con_releasea)) | ((~(con_crp)) & (con_releasea)))))\n",
+ "(always (implies con_crp (next (or (eventually con_releasea) (and (not con_crp) con_releasea)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_crp) -> (F(con_releaseb)))\n",
+ "(always (implies con_crp (eventually con_releaseb)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_crp) -> (X[!]((F(con_releaseb)) | ((~(con_crp)) & (con_releaseb)))))\n",
+ "(always (implies con_crp (next (or (eventually con_releaseb) (and (not con_crp) con_releaseb)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_crp) -> (F(con_released)))\n",
+ "(always (implies con_crp (eventually con_released)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_crp) -> (X[!]((F(con_released)) | ((~(con_crp)) & (con_released)))))\n",
+ "(always (implies con_crp (next (or (eventually con_released) (and (not con_crp) con_released)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_crp) -> (F(con_returner)))\n",
+ "(always (implies con_crp (eventually con_returner)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_crp) -> (X[!]((F(con_returner)) | ((~(con_crp)) & (con_returner)))))\n",
+ "(always (implies con_crp (next (or (eventually con_returner) (and (not con_crp) con_returner)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_crp) -> (F(con_releasec)))\n",
+ "(always (implies con_crp (eventually con_releasec)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_crp) -> (X[!]((F(con_releasec)) | ((~(con_crp)) & (con_releasec)))))\n",
+ "(always (implies con_crp (next (or (eventually con_releasec) (and (not con_crp) con_releasec)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_crp) -> (F(con_releasee)))\n",
+ "(always (implies con_crp (eventually con_releasee)))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "G((con_crp) -> (X[!]((F(con_releasee)) | ((~(con_crp)) & (con_releasee)))))\n",
+ "(always (implies con_crp (next (or (eventually con_releasee) (and (not con_crp) con_releasee)))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_releasea)) | (F(con_releaseb))) & (~((F(con_releasea)) & (F(con_releaseb))))\n",
+ "(and (or (eventually con_releasea) (eventually con_releaseb)) (not (and (eventually con_releasea) (eventually con_releaseb))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_releasea)) | (F(con_releaseb))\n",
+ "(or (eventually con_releasea) (eventually con_releaseb))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_releasea)) | (F(con_released))) & (~((F(con_releasea)) & (F(con_released))))\n",
+ "(and (or (eventually con_releasea) (eventually con_released)) (not (and (eventually con_releasea) (eventually con_released))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_releasea)) | (F(con_released))\n",
+ "(or (eventually con_releasea) (eventually con_released))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_releasea)) | (F(con_returner))) & (~((F(con_releasea)) & (F(con_returner))))\n",
+ "(and (or (eventually con_releasea) (eventually con_returner)) (not (and (eventually con_releasea) (eventually con_returner))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_releasea)) | (F(con_returner))\n",
+ "(or (eventually con_releasea) (eventually con_returner))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_releasea)) | (F(con_releasec))) & (~((F(con_releasea)) & (F(con_releasec))))\n",
+ "(and (or (eventually con_releasea) (eventually con_releasec)) (not (and (eventually con_releasea) (eventually con_releasec))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_releasea)) | (F(con_releasec))\n",
+ "(or (eventually con_releasea) (eventually con_releasec))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_releasea)) | (F(con_releasee))) & (~((F(con_releasea)) & (F(con_releasee))))\n",
+ "(and (or (eventually con_releasea) (eventually con_releasee)) (not (and (eventually con_releasea) (eventually con_releasee))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_releasea)) | (F(con_releasee))\n",
+ "(or (eventually con_releasea) (eventually con_releasee))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_releaseb)) | (F(con_released))) & (~((F(con_releaseb)) & (F(con_released))))\n",
+ "(and (or (eventually con_releaseb) (eventually con_released)) (not (and (eventually con_releaseb) (eventually con_released))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_releaseb)) | (F(con_released))\n",
+ "(or (eventually con_releaseb) (eventually con_released))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_releaseb)) | (F(con_returner))) & (~((F(con_releaseb)) & (F(con_returner))))\n",
+ "(and (or (eventually con_releaseb) (eventually con_returner)) (not (and (eventually con_releaseb) (eventually con_returner))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_releaseb)) | (F(con_returner))\n",
+ "(or (eventually con_releaseb) (eventually con_returner))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_releaseb)) | (F(con_releasec))) & (~((F(con_releaseb)) & (F(con_releasec))))\n",
+ "(and (or (eventually con_releaseb) (eventually con_releasec)) (not (and (eventually con_releaseb) (eventually con_releasec))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_releaseb)) | (F(con_releasec))\n",
+ "(or (eventually con_releaseb) (eventually con_releasec))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_releaseb)) | (F(con_releasee))) & (~((F(con_releaseb)) & (F(con_releasee))))\n",
+ "(and (or (eventually con_releaseb) (eventually con_releasee)) (not (and (eventually con_releaseb) (eventually con_releasee))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_releaseb)) | (F(con_releasee))\n",
+ "(or (eventually con_releaseb) (eventually con_releasee))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_released)) | (F(con_returner))) & (~((F(con_released)) & (F(con_returner))))\n",
+ "(and (or (eventually con_released) (eventually con_returner)) (not (and (eventually con_released) (eventually con_returner))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_released)) | (F(con_returner))\n",
+ "(or (eventually con_released) (eventually con_returner))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_released)) | (F(con_releasec))) & (~((F(con_released)) & (F(con_releasec))))\n",
+ "(and (or (eventually con_released) (eventually con_releasec)) (not (and (eventually con_released) (eventually con_releasec))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_released)) | (F(con_releasec))\n",
+ "(or (eventually con_released) (eventually con_releasec))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_released)) | (F(con_releasee))) & (~((F(con_released)) & (F(con_releasee))))\n",
+ "(and (or (eventually con_released) (eventually con_releasee)) (not (and (eventually con_released) (eventually con_releasee))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_released)) | (F(con_releasee))\n",
+ "(or (eventually con_released) (eventually con_releasee))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_returner)) | (F(con_releasec))) & (~((F(con_returner)) & (F(con_releasec))))\n",
+ "(and (or (eventually con_returner) (eventually con_releasec)) (not (and (eventually con_returner) (eventually con_releasec))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_returner)) | (F(con_releasec))\n",
+ "(or (eventually con_returner) (eventually con_releasec))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_returner)) | (F(con_releasee))) & (~((F(con_returner)) & (F(con_releasee))))\n",
+ "(and (or (eventually con_returner) (eventually con_releasee)) (not (and (eventually con_returner) (eventually con_releasee))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_returner)) | (F(con_releasee))\n",
+ "(or (eventually con_returner) (eventually con_releasee))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "((F(con_releasec)) | (F(con_releasee))) & (~((F(con_releasec)) & (F(con_releasee))))\n",
+ "(and (or (eventually con_releasec) (eventually con_releasee)) (not (and (eventually con_releasec) (eventually con_releasee))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_releasec)) | (F(con_releasee))\n",
+ "(or (eventually con_releasec) (eventually con_releasee))\n",
+ "Is satisfiable? True\n",
+ "\n"
+ ]
+ }
+ ],
+ "source": [
+ "\n",
+ "for ltl_mod in model.ltl_model:\n",
+ " print(ltl_mod.formula)\n",
+ " print(ltl_mod.parsed_formula)\n",
+ " print(f'Is satisfiable? {ltl_mod.check_satisfiability()}\\n')\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "8bc1e79e",
+ "metadata": {},
+ "source": [
+ "Now that the BpmnConstraintsModel is set up, it can be used to check conformance"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stderr",
+ "output_type": "stream",
+ "text": [
+ "/home/fleph/sap/Declare4Py/.venv/lib64/python3.11/site-packages/tqdm/auto.py:21: TqdmWarning: IProgress not found. Please update jupyter and ipywidgets. See https://ipywidgets.readthedocs.io/en/stable/user_install.html\n",
+ " from .autonotebook import tqdm as notebook_tqdm\n",
+ "parsing log, completed traces :: 100%|██████████| 1050/1050 [00:00<00:00, 3627.00it/s]\n",
+ "/home/fleph/sap/Declare4Py/.venv/lib64/python3.11/site-packages/pm4py/utils.py:486: UserWarning: the EventLog class has been deprecated and will be removed in a future release.\n",
+ " warnings.warn(\"the EventLog class has been deprecated and will be removed in a future release.\")\n"
+ ]
+ },
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "Accepted traces: 0\n",
+ " case:concept:name accepted\n",
+ "0 A False\n",
+ "1 B False\n",
+ "2 C False\n",
+ "3 D False\n",
+ "4 E False\n",
+ "... ... ...\n",
+ "1045 HNA False\n",
+ "1046 INA False\n",
+ "1047 JNA False\n",
+ "1048 KNA False\n",
+ "1049 LNA False\n",
+ "\n",
+ "[1050 rows x 2 columns]\n",
+ "con_erregistration\n",
+ "0. Accepted traces: 995\n",
+ "(G((con_ertriage) -> (F(con_ersepsistriage)))) & ((F(con_ersepsistriage)) | ((~(con_ertriage)) & (con_ersepsistriage)) | (G(~(con_ertriage))))\n",
+ "1. Accepted traces: 1029\n",
+ "(F(con_ertriage)) & (F(con_ersepsistriage))\n",
+ "2. Accepted traces: 1049\n",
+ "(G((con_ertriage) -> (X[!]((F(con_ersepsistriage)) | ((~(con_ertriage)) & (con_ersepsistriage)))))) & (G((con_ersepsistriage) -> ((X[!](~(con_ersepsistriage))) & ((F(con_ertriage)) | ((~(con_ersepsistriage)) & (con_ertriage))))))\n",
+ "3. Accepted traces: 0\n",
+ "F((con_releasea) & (X[!](false)))\n",
+ "4. Accepted traces: 0\n",
+ "F((con_releaseb) & (X[!](false)))\n",
+ "5. Accepted traces: 0\n",
+ "F((con_releasec) & (X[!](false)))\n",
+ "6. Accepted traces: 0\n",
+ "F((con_released) & (X[!](false)))\n",
+ "7. Accepted traces: 0\n",
+ "F((con_releasee) & (X[!](false)))\n",
+ "8. Accepted traces: 0\n",
+ "F((con_returner) & (X[!](false)))\n",
+ "9. Accepted traces: 0\n",
+ "(F(con_leucocytes)) & (F(con_crp))\n",
+ "10. Accepted traces: 1006\n",
+ "(F(con_leucocytes)) & (F(con_ertriage))\n",
+ "11. Accepted traces: 1012\n",
+ "(F(con_leucocytes)) & (F(con_lacticacid))\n",
+ "12. Accepted traces: 860\n",
+ "(F(con_crp)) & (F(con_ertriage))\n",
+ "13. Accepted traces: 1007\n",
+ "(F(con_crp)) & (F(con_lacticacid))\n",
+ "14. Accepted traces: 860\n",
+ "(F(con_ertriage)) & (F(con_lacticacid))\n",
+ "15. Accepted traces: 860\n",
+ "(F(con_leucocytes)) | ((~(con_erregistration)) & (con_leucocytes)) | (G(~(con_erregistration)))\n",
+ "16. Accepted traces: 1012\n",
+ "G((con_leucocytes) -> ((X[!](~(con_leucocytes))) & ((F(con_erregistration)) | ((~(con_leucocytes)) & (con_erregistration)))))\n",
+ "17. Accepted traces: 42\n",
+ "(F(con_crp)) | ((~(con_erregistration)) & (con_crp)) | (G(~(con_erregistration)))\n",
+ "18. Accepted traces: 1007\n",
+ "G((con_crp) -> ((X[!](~(con_crp))) & ((F(con_erregistration)) | ((~(con_crp)) & (con_erregistration)))))\n",
+ "19. Accepted traces: 46\n",
+ "(F(con_ertriage)) | ((~(con_erregistration)) & (con_ertriage)) | (G(~(con_erregistration)))\n",
+ "20. Accepted traces: 1050\n",
+ "G((con_ertriage) -> ((X[!](~(con_ertriage))) & ((F(con_erregistration)) | ((~(con_ertriage)) & (con_erregistration)))))\n",
+ "21. Accepted traces: 6\n",
+ "(F(con_lacticacid)) | ((~(con_erregistration)) & (con_lacticacid)) | (G(~(con_erregistration)))\n",
+ "22. Accepted traces: 860\n",
+ "G((con_lacticacid) -> ((X[!](~(con_lacticacid))) & ((F(con_erregistration)) | ((~(con_lacticacid)) & (con_erregistration)))))\n",
+ "23. Accepted traces: 192\n",
+ "(F(con_ivantibiotics)) & (F(con_ivliquid))\n",
+ "24. Accepted traces: 753\n",
+ "(F(con_ivantibiotics)) | ((~(con_ersepsistriage)) & (con_ivantibiotics)) | (G(~(con_ersepsistriage)))\n",
+ "25. Accepted traces: 824\n",
+ "G((con_ivantibiotics) -> ((X[!](~(con_ivantibiotics))) & ((F(con_ersepsistriage)) | ((~(con_ivantibiotics)) & (con_ersepsistriage)))))\n",
+ "26. Accepted traces: 227\n",
+ "(F(con_ivliquid)) | ((~(con_ersepsistriage)) & (con_ivliquid)) | (G(~(con_ersepsistriage)))\n",
+ "27. Accepted traces: 754\n",
+ "G((con_ivliquid) -> ((X[!](~(con_ivliquid))) & ((F(con_ersepsistriage)) | ((~(con_ivliquid)) & (con_ersepsistriage)))))\n",
+ "28. Accepted traces: 348\n",
+ "G((con_ivantibiotics) -> (F(con_admissionnc)))\n",
+ "29. Accepted traces: 918\n",
+ "G((con_ivantibiotics) -> (X[!]((F(con_admissionnc)) | ((~(con_ivantibiotics)) & (con_admissionnc)))))\n",
+ "30. Accepted traces: 918\n",
+ "G((con_ivantibiotics) -> (F(con_admissionic)))\n",
+ "31. Accepted traces: 325\n",
+ "G((con_ivantibiotics) -> (X[!]((F(con_admissionic)) | ((~(con_ivantibiotics)) & (con_admissionic)))))\n",
+ "32. Accepted traces: 325\n",
+ "G((con_ivliquid) -> (F(con_admissionnc)))\n",
+ "33. Accepted traces: 911\n",
+ "G((con_ivliquid) -> (X[!]((F(con_admissionnc)) | ((~(con_ivliquid)) & (con_admissionnc)))))\n",
+ "34. Accepted traces: 911\n",
+ "G((con_ivliquid) -> (F(con_admissionic)))\n",
+ "35. Accepted traces: 387\n",
+ "G((con_ivliquid) -> (X[!]((F(con_admissionic)) | ((~(con_ivliquid)) & (con_admissionic)))))\n",
+ "36. Accepted traces: 387\n",
+ "((F(con_admissionnc)) | (F(con_admissionic))) & (~((F(con_admissionnc)) & (F(con_admissionic))))\n",
+ "37. Accepted traces: 710\n",
+ "(F(con_admissionnc)) | (F(con_admissionic))\n",
+ "38. Accepted traces: 810\n",
+ "G((con_lacticacid) -> (F(con_releasea)))\n",
+ "39. Accepted traces: 792\n",
+ "G((con_lacticacid) -> (X[!]((F(con_releasea)) | ((~(con_lacticacid)) & (con_releasea)))))\n",
+ "40. Accepted traces: 792\n",
+ "G((con_lacticacid) -> (F(con_releaseb)))\n",
+ "41. Accepted traces: 240\n",
+ "G((con_lacticacid) -> (X[!]((F(con_releaseb)) | ((~(con_lacticacid)) & (con_releaseb)))))\n",
+ "42. Accepted traces: 240\n",
+ "G((con_lacticacid) -> (F(con_released)))\n",
+ "43. Accepted traces: 212\n",
+ "G((con_lacticacid) -> (X[!]((F(con_released)) | ((~(con_lacticacid)) & (con_released)))))\n",
+ "44. Accepted traces: 212\n",
+ "G((con_lacticacid) -> (F(con_returner)))\n",
+ "45. Accepted traces: 463\n",
+ "G((con_lacticacid) -> (X[!]((F(con_returner)) | ((~(con_lacticacid)) & (con_returner)))))\n",
+ "46. Accepted traces: 463\n",
+ "G((con_lacticacid) -> (F(con_releasec)))\n",
+ "47. Accepted traces: 213\n",
+ "G((con_lacticacid) -> (X[!]((F(con_releasec)) | ((~(con_lacticacid)) & (con_releasec)))))\n",
+ "48. Accepted traces: 213\n",
+ "G((con_lacticacid) -> (F(con_releasee)))\n",
+ "49. Accepted traces: 194\n",
+ "G((con_lacticacid) -> (X[!]((F(con_releasee)) | ((~(con_lacticacid)) & (con_releasee)))))\n",
+ "50. Accepted traces: 194\n",
+ "G((con_leucocytes) -> (F(con_releasea)))\n",
+ "51. Accepted traces: 701\n",
+ "G((con_leucocytes) -> (X[!]((F(con_releasea)) | ((~(con_leucocytes)) & (con_releasea)))))\n",
+ "52. Accepted traces: 701\n",
+ "G((con_leucocytes) -> (F(con_releaseb)))\n",
+ "53. Accepted traces: 94\n",
+ "G((con_leucocytes) -> (X[!]((F(con_releaseb)) | ((~(con_leucocytes)) & (con_releaseb)))))\n",
+ "54. Accepted traces: 94\n",
+ "G((con_leucocytes) -> (F(con_released)))\n",
+ "55. Accepted traces: 62\n",
+ "G((con_leucocytes) -> (X[!]((F(con_released)) | ((~(con_leucocytes)) & (con_released)))))\n",
+ "56. Accepted traces: 62\n",
+ "G((con_leucocytes) -> (F(con_returner)))\n",
+ "57. Accepted traces: 328\n",
+ "G((con_leucocytes) -> (X[!]((F(con_returner)) | ((~(con_leucocytes)) & (con_returner)))))\n",
+ "58. Accepted traces: 328\n",
+ "G((con_leucocytes) -> (F(con_releasec)))\n",
+ "59. Accepted traces: 63\n",
+ "G((con_leucocytes) -> (X[!]((F(con_releasec)) | ((~(con_leucocytes)) & (con_releasec)))))\n",
+ "60. Accepted traces: 63\n",
+ "G((con_leucocytes) -> (F(con_releasee)))\n",
+ "61. Accepted traces: 44\n",
+ "G((con_leucocytes) -> (X[!]((F(con_releasee)) | ((~(con_leucocytes)) & (con_releasee)))))\n",
+ "62. Accepted traces: 44\n",
+ "G((con_crp) -> (F(con_releasea)))\n",
+ "63. Accepted traces: 704\n",
+ "G((con_crp) -> (X[!]((F(con_releasea)) | ((~(con_crp)) & (con_releasea)))))\n",
+ "64. Accepted traces: 704\n",
+ "G((con_crp) -> (F(con_releaseb)))\n",
+ "65. Accepted traces: 99\n",
+ "G((con_crp) -> (X[!]((F(con_releaseb)) | ((~(con_crp)) & (con_releaseb)))))\n",
+ "66. Accepted traces: 99\n",
+ "G((con_crp) -> (F(con_released)))\n",
+ "67. Accepted traces: 67\n",
+ "G((con_crp) -> (X[!]((F(con_released)) | ((~(con_crp)) & (con_released)))))\n",
+ "68. Accepted traces: 67\n",
+ "G((con_crp) -> (F(con_returner)))\n",
+ "69. Accepted traces: 333\n",
+ "G((con_crp) -> (X[!]((F(con_returner)) | ((~(con_crp)) & (con_returner)))))\n",
+ "70. Accepted traces: 333\n",
+ "G((con_crp) -> (F(con_releasec)))\n",
+ "71. Accepted traces: 68\n",
+ "G((con_crp) -> (X[!]((F(con_releasec)) | ((~(con_crp)) & (con_releasec)))))\n",
+ "72. Accepted traces: 68\n",
+ "G((con_crp) -> (F(con_releasee)))\n",
+ "73. Accepted traces: 49\n",
+ "G((con_crp) -> (X[!]((F(con_releasee)) | ((~(con_crp)) & (con_releasee)))))\n",
+ "74. Accepted traces: 49\n",
+ "((F(con_releasea)) | (F(con_releaseb))) & (~((F(con_releasea)) & (F(con_releaseb))))\n",
+ "75. Accepted traces: 727\n",
+ "(F(con_releasea)) | (F(con_releaseb))\n",
+ "76. Accepted traces: 727\n",
+ "((F(con_releasea)) | (F(con_released))) & (~((F(con_releasea)) & (F(con_released))))\n",
+ "77. Accepted traces: 695\n",
+ "(F(con_releasea)) | (F(con_released))\n",
+ "78. Accepted traces: 695\n",
+ "((F(con_releasea)) | (F(con_returner))) & (~((F(con_releasea)) & (F(con_returner))))\n",
+ "79. Accepted traces: 411\n",
+ "(F(con_releasea)) | (F(con_returner))\n",
+ "80. Accepted traces: 688\n",
+ "((F(con_releasea)) | (F(con_releasec))) & (~((F(con_releasea)) & (F(con_releasec))))\n",
+ "81. Accepted traces: 696\n",
+ "(F(con_releasea)) | (F(con_releasec))\n",
+ "82. Accepted traces: 696\n",
+ "((F(con_releasea)) | (F(con_releasee))) & (~((F(con_releasea)) & (F(con_releasee))))\n",
+ "83. Accepted traces: 677\n",
+ "(F(con_releasea)) | (F(con_releasee))\n",
+ "84. Accepted traces: 677\n",
+ "((F(con_releaseb)) | (F(con_released))) & (~((F(con_releaseb)) & (F(con_released))))\n",
+ "85. Accepted traces: 80\n",
+ "(F(con_releaseb)) | (F(con_released))\n",
+ "86. Accepted traces: 80\n",
+ "((F(con_releaseb)) | (F(con_returner))) & (~((F(con_releaseb)) & (F(con_returner))))\n",
+ "87. Accepted traces: 350\n",
+ "(F(con_releaseb)) | (F(con_returner))\n",
+ "88. Accepted traces: 350\n",
+ "((F(con_releaseb)) | (F(con_releasec))) & (~((F(con_releaseb)) & (F(con_releasec))))\n",
+ "89. Accepted traces: 81\n",
+ "(F(con_releaseb)) | (F(con_releasec))\n",
+ "90. Accepted traces: 81\n",
+ "((F(con_releaseb)) | (F(con_releasee))) & (~((F(con_releaseb)) & (F(con_releasee))))\n",
+ "91. Accepted traces: 62\n",
+ "(F(con_releaseb)) | (F(con_releasee))\n",
+ "92. Accepted traces: 62\n",
+ "((F(con_released)) | (F(con_returner))) & (~((F(con_released)) & (F(con_returner))))\n",
+ "93. Accepted traces: 298\n",
+ "(F(con_released)) | (F(con_returner))\n",
+ "94. Accepted traces: 308\n",
+ "((F(con_released)) | (F(con_releasec))) & (~((F(con_released)) & (F(con_releasec))))\n",
+ "95. Accepted traces: 49\n",
+ "(F(con_released)) | (F(con_releasec))\n",
+ "96. Accepted traces: 49\n",
+ "((F(con_released)) | (F(con_releasee))) & (~((F(con_released)) & (F(con_releasee))))\n",
+ "97. Accepted traces: 30\n",
+ "(F(con_released)) | (F(con_releasee))\n",
+ "98. Accepted traces: 30\n",
+ "((F(con_returner)) | (F(con_releasec))) & (~((F(con_returner)) & (F(con_releasec))))\n",
+ "99. Accepted traces: 307\n",
+ "(F(con_returner)) | (F(con_releasec))\n",
+ "100. Accepted traces: 313\n",
+ "((F(con_returner)) | (F(con_releasee))) & (~((F(con_returner)) & (F(con_releasee))))\n",
+ "101. Accepted traces: 298\n",
+ "(F(con_returner)) | (F(con_releasee))\n",
+ "102. Accepted traces: 299\n",
+ "((F(con_releasec)) | (F(con_releasee))) & (~((F(con_releasec)) & (F(con_releasee))))\n",
+ "103. Accepted traces: 31\n",
+ "(F(con_releasec)) | (F(con_releasee))\n",
+ "104. Accepted traces: 31\n"
+ ]
+ }
+ ],
+ "source": [
+ "from Declare4Py.D4PyEventLog import D4PyEventLog\n",
+ "from Declare4Py.ProcessMiningTasks.ConformanceChecking.LTLAnalyzer import LTLAnalyzer\n",
+ "\n",
+ "log_path = os.path.join(\"../../../../\", \"tests\", \"test_logs\",\"Sepsis Cases.xes.gz\")\n",
+ "event_log = D4PyEventLog()\n",
+ "event_log.parse_xes_log(log_path)\n",
+ "\n",
+ "analyzer = LTLAnalyzer(event_log, model.ltl_model)\n",
+ "conf_check_res_df = analyzer.run_multiple_models(minimize_automaton=False) #This does not seem to work as intented currently\n",
+ "print(f\"Accepted traces: {len(conf_check_res_df[conf_check_res_df['accepted'] == True])}\")\n",
+ "print(conf_check_res_df)\n",
+ "\n",
+ "for idx, ltl_mod in enumerate(model.ltl_model):\n",
+ " analyzer = LTLAnalyzer(event_log, ltl_mod)\n",
+ " conf_check_res_df = analyzer.run()\n",
+ " print(ltl_mod.formula)\n",
+ " print(f\"{idx}. Accepted traces: {len(conf_check_res_df[conf_check_res_df['accepted'] == True])}\")\n",
+ "\n"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Python 3",
+ "language": "python",
+ "name": "python3"
+ },
+ "language_info": {
+ "codemirror_mode": {
+ "name": "ipython",
+ "version": 3
+ },
+ "file_extension": ".py",
+ "mimetype": "text/x-python",
+ "name": "python",
+ "nbconvert_exporter": "python",
+ "pygments_lexer": "ipython3",
+ "version": "3.11.6"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
diff --git a/Declare4Py/Utils/bpmnconstraints/tutorial/data/Sepsis Cases.png b/Declare4Py/Utils/bpmnconstraints/tutorial/data/Sepsis Cases.png
new file mode 100644
index 0000000000000000000000000000000000000000..57229a3f216ddcfc4b28cab1e898ffb7ff0c7caa
GIT binary patch
literal 49737
zcmb@u1z44N*FAhxQbj~11QeB)5+tNWr6r}iJETLx1eH?i5E2s7-K}&eNQ0CT(%o=?
zZ{N&3&&<5<^Zvj0e|_J~H8^tabH^|CUVE*z?>F+Y;smG3Poq#M0!fJniYU}6OB4$G
zIvx)EhWHa@Jp6IZP(o1#g>t7up`N}(q4wZcPiIglr&}o0oE{3r7lA^NKK@XyAOIg=
znTp7Wpip^%9{UO*@b?oAisJWB+3l3G@E05dY4HcBBjn%ssubj7{KpdN4k*;QdgQ+o
zVNB;J;BqL*2O>(YKNd#tE5jW|g;(YsHI(UF7;fwb;}`~+8Aup0y&pHvylvLVVfb$P
zGCzC$YxhQfPib{ue8bD+7u2Pi1pW*2K@5god$ePX`cvWThS7~qC
zd)3TqZ6B0*kIlQ#TY?2
zOXabWWH-^+%Zpj53sEZ`Fz}-xFmL%3Z4>n{R)9B>+ggLeZoGcd)_Y%bZ8AiT)uJn@
zg}$Mo!BjR*=wMlc2&GSe>Wde@>Xx+q`PnJkosDj}d0nSoU1i
zi9te98?)Uhj$fW*FDL6S4Q$MP&FMsGsSGFu#qM9!<@22CO&n&R$&DMT0(XaDlu}9R8q$-m2Vj(N4mK^2L5%1iq
ztXkzY5y0c@zVpjBWFnB?rbw(ieE(DUXpZ$zam(TUvhMb36V-CD-k0a*vlBsGttdQ8
z)XJ5H*BUim2Ygj~a~UnH6$|-dR|}LgR9foNX%P3o6C6sjRTWC_d2Cxcq0&P%qEJs;AJ1o%j0%`{CGAx`+0Onxz5C79tH3LS
zPR3cT<7#~GiSvCZJ=$^H94gnJ&q83r=aOV&_=xwkR(DEBB;0TEq8JOI8~xa(btSJ=VWPC(}C>3ZZ&mz2`#pl}Fw-C9x{~%Eak
zHPsbjqCs_h%kh#Sbjk2twTup4>mP-)vn}X1+tT8*Qa5`T?s;eT4kFp4#=Hj53zL(lf(8qc0&BEP#@3!e0C}vIn>%k+~4Q;&U
z(o#sm!osq`rlsSi*X4wEjXE|KLjJs>-tVuGaU{gVGVTj`O?|EF+U~Q-Y)SM-QfS6M
zk4Pvj-SPKhEl+j)Rr`u~Pv8s*bA-n?uKtCX*s2E^r(l15zWET@9k3Xd3CM0;Q+*~E
zGXJA!{!E$H(%9@Sx{wdmEBTQQ6`%h#R&c)oS9L9fI51-Upk$
zNv1*4=tvF9<3Z~9iY)le0mC3C{;dJSc~0vejsb!zGo6V?&NCl+Pqu#=MW*Ee&2S#y(jp;~}tE>?){{LyH%29Pb>$GA$b=Ny(OI
zLZO|X@15p)B5SrspY*daW0q_c*dv=2#II})Z1(GpG46J}j*7>*TcjM1k4n8)EPMaQ
zXF8dvg}xf^BfcgoZ;y~(d~4Y4-E3u(!K8azixsNm7$K>gJ>_!${tw6N$K=X8R&;;b
zBU7~J)}U$E8~RwaT-c~2TsFg{g9RNzny%kPaAl$epKST}>w0^(#vNg%%P-Q)`cqY2
zjb=sDnRsF$EA(_fhjyR@y3Pxxcj=D(WOIOc0C~}9cEyrLB@Cxb)nf6`jd;NrRykU)
z74oO#jmw!QgcT&|TE8Gi2hl?9eGn
z>iNCIc5M6f>C^6JA}EWK)RrhE(MLliw!)T9Di7<_oy%Ph(xT2G3*~0JWelIwUV3V3
zs-rT~Z~HQ%!~pIn()p$X&MU~>D1G>ajg4JacaGnxwN)iuyTaM|N1kC*TAtUiT=#Ky
zz?OWW8hSf$xi_PKGAv6~O^xgX%j{r*Y4PFs{t4t+h|PA=rLId$Nu6#DyGyQo3Yn53
zqCORs(`i^2j_=_Me7>$PgHMB8G1HTY`PBzuZ?A+uKV{5h$+?uTl66$+$@uJeLZxyO
z6q`NN9-YKT&L2k4^vdc-p*gF!sJXd$SH5u@2kkp#66D|Lvq)VD;$JG=oyuA0N|t_e
zK>}ItsWiKa%@^ea>~wbLD_oYZ{`&LEN(sLfe-vq|L3q!+l%JZ)K#IPYXmNa|GX1Rh
zcs;54zAV3q+TtM_eje5{mZ%;h>?oApNLbs{+_3YI^>if!vnsKmt5u7Tz2;>iIU1hS
z5%wgA`gJ8FB&g5M=EBHr#jqPT4ryS+gFo%%Flv5xdl};Ce3Sp>?p)Oz9Z86@ArSXz
zqixF58h4-3$;Ezn7{$qWna|P8emce_oZIaC&#WNf!=3t#PpcZZ$Z4ipr|gSx&XV2Q
zdCQbN<9xU~O>Y|K>8zNeBS`Q_L`q63`0!w#-uww^M>J24rn>szZ4KDkqxSv}7g3PDUC%HJC@0D&2$gj;hZ;17go8hBW#4gi(=1a)T
zWM*XM#DA=uTT11K^MAD^kxl=fw(s#q{tx^8uVat@@A$A4&tAxmlbcH;{EV!uI`(cM
zGTf5ckijQk5DH1yKuTOF4`Pi$3O7c3`8*}%s_S~nNXbg}h=eCL%Ir@H|
zP{w)0sekz(sxk0N^jXR~x5_sAH2XF91z=8FFuUs^kK_b<#ZKH!X3xj@d;x;FUOvP^
z+ADmH&EbOE!?!CAA;7ks9P02sTsQK);w<5F?n)G;$I6#BPk&fl+=JF7Bf)?vXbH$U
zCHP#HJ_xLTy*;+i#brAxushh{RovwS(LPkmYjF!QFE0v+iq9w71PSe#DXOVOPI9k~aAo@jhU*H|-HU#e2Wb
zGCa?zx}OxbmG65pRN2n>Yg!j6lk|)i4MXx&AMo$z1Jt^})#xDp*#9RlB#6l{Rh<^G
zZ|8(DD@JH-XUWDOs<@5$el~M}#~cp7zcOp}r7JT%IjjUYK;s7Zu|T28wH>kqeT9$?
z+{9)M0+ZDT{Q4bh@#&3nE~C5{AP9Sy0&Z=S^?UnPrOf7KE}oqJ#!P1mkvQf1S9y4M
zAkoMbC{#Qi(D$VUl+gUV7h=@=vs6L?>X6MM|8okR9?3ceKqK@p6f}IzPb$h&^xt4%5*uk3KEh0*YcR&nyix)~MV9Cf
z9&0UwQ+N@p8iq-?p3mGT6buchZ+K0GZ2L?Iz5eR@cxM!J$fzF?>8a4sQMmzd3#O0r
z;23o5mMNG=B3S0x)p0+zcGf0|9`A#GZ{v{n^%8@AY}FA9C1YNL&3%AmH?o>ABg@o&*Oaq(O`ww=Fm(^!~t<_7Y?$%I??c8t`Wi;|n5|!s)t-q)`c$Mgm9Pd;pExH71
zrcD2}Hny6ttl|uQ@!_P@k7;RXxoMCf*B8h@<^Mi|jM%TU1nM)l7Iv$)w~CDnxc=ua
z8o#LXA!rNKhHbx@uUHSWzpuIdX04G-eF&KdDWYMfH>|K&Y7HraNVc`FD9rJiwtt{SCr)zIsvX`bUlW0iynqu7(kUhjRa11lQ92ylKDn3h?17joG<%xaMLSE-AtG-BO*+skp-vD85V98eR=+5a$4
zp&hcV@#Ho%cvuG0wM`H8+BYdC!%5a!B|re&kxlQe-w$`MB=hteyka>1zC-v(plq#`
zsbHRvck-Q8QkLibmb%;Inn|j^LIs2Auzed#!RO04DITc;0F?{!zu_fJHRM?+kdxnj
zBvxjE)g$r(XHXuM`WVUfG4C~<`|4URGzB$q?nc{IyOGQo6fTY(9d0X%Fa{d?nQx$D
zHmK<~USFo6e#fHuoUD7hY1M8uqV1vx6CKr?_hrVScm0P{I2XMh4pB7?h^A^$+kQTB
z3mEl1p?2N)9V*kwj#BMm&wD~;qTp8COfs$~+aoS${zL=+w+)_XmrOORQey0)^NG%F
zXDqI_vZ`+Fn<;FSetHhT=^T7rshmN<-@cW>(EmKiml?nV&0ccH2{e_4y-Veg=Q|1o
zNBu{5dYpa!%v4cu2;j6oe?T#bLLL8rMT$aJDhk1EfBW%&I<~L8wzf7YGxOnnr4#1D
z9vA5~P9mr!35vDkIPb$UpVX6|9!7Eq3U*#bHYtrH1X)v=h+86XJS=t<$9ftT1W4ZP
zs&re|zwdjl_q_6500+N6(RWzlAA462xND(#o%b852LZ+?M1L*=?u
zHhoUALnodKr51Ki29+zjo1U3zwE-(EaOwNU`y(uOr%=0|QwrJr@y{$aV}Lv;A8BCRF$
zlZ_do+ZuELKW*~cSSx4%CmV8@eUDH7@hPO+SgKqAjWO*L4|#)HiAj5M;^#<18?ExL
zC{%qf1C?$6e)usa3Y741_*?MQ{<3LCrz_0Ydp$y19~ENYYzFVu|kaYCNX
z?;iZ&WWKG78pJiiUXm(l{uqzU4{rd;clfE$B`>_)%
z_#~S%lbD3WB*m|vqGrbnfsA*t$*a>9oAdMY*J$5~^&%(Ivwm6B%lJy^kD|h|6KayM
zyC;!jr_}Wslm09n>T`?p6(#_t{3<*q8&WjnBGu(*#;`1SaN70cB{R9-v3mH;2Qa#hV;WI6rU*PO1x
zLr-*l=GM|Xt}&&~SxlYMtZ-hO69BrhiB+pq{*Mpdp0hx*D~HuUuGQ@Kk9FxMHAk-B
z_i>ayHDq~`;<)OSmp_9``S|V{Bx=((W3)D)S?XM5^qderFRQRnN$*trkF;c9HqMDG
z?n_XW{ERe>HAhNE`iTUUV`2=s{z=U&Jgd#Q-u;Zv$E1PswbUu6neQK0U@o=ea!Wk;EdgdKrd-`ALZH1_BLfp
zSA;q4(rF9HqOlK^Gm5$#cdu#Nure_0+;h15?NK~_e5-E}Qws2C(@y=`CA+n+&II_V
zUWA%!Bv-%AXOqf(=HrhuB$-2TzVr_xR=xqa%sT|Enx|2dSe(wdtEwu{o{ZKhuN~5L
z{q-sm?%>YPr>97)Di(`n`oj)WfiCR=*6o!a2}_hPAQ85M5*1xwlGGi4y(0C>ha$Qr
z(x+(5k|@>9Lz+-oHyYxx*E*7Gab*-dDILFyv;gEmBjBB!S~3bDd(#$(il#O?ak4au
zqN06@Kh5T6Z%X=Oxc#g1+*FQMJb~vWvBW>$_q0_ZB`Jx9LSYD=tY#Pr8IOxP1W*~4
zPpx+d>(UEdT88am48)h|VEGS{i*yfn_5yfD&G=xg)TUn=KqxVDU|G}AKE=HAt<4(c
zY>Wt3p%1?!K{&QAnd${X>th;%0c7k6gQ*IMQ7m5GsfnVHAaAN;6`eSRVU*YnG72n%B+xr8~IJJ4d?e)0T=
zzV8*4l+4UbY4Y^`NW(s;GrYO>W)g$QZ6GzAae>NVfNoJPJq>WVEvdeYG;9tf_F3FM
z>cV@y;W%$nOuj`GX}ddDG$fKv^lf@sj+Ae9YL`2@2`Hy)pdDY4v#%_
z*B+p=g-T-)=Nx6}h`MPE7j5-U9$Q+qXBx5Ih+h6lRNq@dVa#JQc=A92xCzp;6x^9o
zSX@;nku90_<|4h2W{J&69TRmf{xOM?djW!uw-CDRigS;GcvxoEXS!4*9DKHj00z$w
zP_QqugV&k({`|tqm9KHaN6F*keA;S#x|nyv2VWapbKp9?jP4y`uG_U5)!*Vb1zdJ?KEit
z<^~9rF0ZFq`dA;$nHyHQGw!E*=8vnrI;jajwjavtuRe`-r_v37*bf8n{{o
zx(6NR7ooS=jnotJ-IvuN5@8kNnE|S`rb#`K%X%vx=WfwytJ!?x@=KPdQ5Jj%|Ht#k
zeV|Zb05b0OzHght*_`b*O#yPh_}kp*bb=r2UcBvC^)m6LOB>&x?-5vq>?!Kr`=)P1
zkRG14I8+i>#K-i>wsvrKd^5#@?*OM*(ld=s1eW#x%pk^iof=B2?m@#O6Pvn1s$a^j
zI~SdwA7;^i*zq9y3cvFQa)fF8`*Ad$F9PzzR;%1Mqbl<^PoFt65pd^UbmGUc&)jKj
zo3wbA$N4)L9UL6|+&-DLTCmqvFS-Z4ci|T-PUfU&n%`d+57SeoW!vR3PG7-Zo_cGKby@v8q<*B4)iqt{ren5};l3
zPtQX`Lun57x8=IFSYvr?bxHuAnQjb~ciV2!D*3`3{iwOCteT3irpjsAXVuKruhqQ>
zL-;zfAQ(Z_p{Fk`4nY8&{CtWq^ETXhVmHsM!fY?qY>89i*n)KGIarN_-Y4`4(w{Qe
zK`q&_d=;3ZBtTT;Ml5eR63$)W>!~_A+~-G!g$V}hY=(Jd3?7*1-g6qD+e|(~u4=B()*_9|fe$On6}>k#`T
zSLzKhP%xYx);*k>2iZ1pWAeXW_{oC+9+1cOfa?l_5(`#J)t9*?mkrI$f6mBF15gjJ
zzeV%(Ls#v0%ug&lxsga3^N&55|84nF&<|W^I|9sBl+VJ=XMCbqO
z0`b3o;Xf6Ve?R$Cr>`G)9fCn2w7^59>RVWz-1&95ks?fM3k1Ak|0WQ1gCJ-JgN{lI
z>d4@(4EG=nFYs9*fX-QqmJm(|10>Z^-vmOZwt!l7lr^6s6CIBE%~Kh`wg0fh`z`2Yj6MU`ArxrwlYjX+yS%sXyvYj
z=Xr`dkM-<9jLz;`rv#|l(nw*Oxo+`JRmY7s@|OO+BKL1c`!z?=udr`=4ZS|_28Jj&
zL{5nJjFzs~t}#h7LNhK1(u}GWkGdZ-w{5i=qo)W3-f1IDTnIwl?BCPtN|GcePG_XH
z%=LLtdh^IfeN@hSuRAF|{u=M^2*dpNm9MuuXi`AM4IbJC@MMMWy;Db(-x=PQrO8%y
z0Jm?sMTQWeUFpgh%&DSxn2)|3rKQA5RYT4->eqGw1hdvmTXL{y>)j@#l?5#F-~|!3
ztHSl3FikNF?1rI?N8c987rya~Jv@X#G#Pt{lp*S+?G(KBMkJpS*%AX%j&ji;hJ=?C)Wto>MDWXXn~=Nw3a*C)IBPiJoA)HG+;3mul3Jjfl5dZ0@S|jHt&T0?O<4XEc@4rW^m?`px+(&u&qTCw6fEFiV^S_e*Q7
z)`pYEo#n9_Z+j5eRm_GU*;4=bnU>zAJi8`RKKub^n$6;eGnp>Q2e;pm>PIkAT>C$-
z=-#MDv*c+%aP9Cd!n?mJB3P?ol`&H8B;5{7s1?;k-O-njy4m+@>7`O8{GPg2?wq_{
zoa353fLm{E7dJ2pQe#ZO!p7ndPsI_`NT7#VxhQmLkAht!6f>ton-#kQU^@SM
zaKq2ARo>#K8k1Lt##dqmFi2w!`XA*1oE`
zo=(MA9x$|dy9Pbh@#6Gy8{g@J@!~wAJ5}@aHQVKJ>8F_2s&;mEYfZw3>`wymjO;wD
z{lljgK~+*8bY5UHcyLFo*I?hDjoo03MEC3ihBJBX5Enimb?M*~nWxuAr+C4^!}hJllII4QBq>gnvUmYuhrNkeSvmys#CS(ncWEjW}?RL
zu1igiYtDGXyp5F&-x__nP8AqVFEy9&m9}~_kZ@_YD`n^Nr73#_){A3-;&)!>k{L_0
z*P_{CPTTR)ji{mPG(7HKp|ZH4B(B+rcYnj&<7WV&cw6+ap=g5O#A-N!#dWb^gWw2{
zyMBZdL_W^Lc1?(?s5V!(wWebz;4GB-iXk#!UpaI~p6p^oQk%1Ka*n~|bpnb8E<1kz
z3w7PH{MM2!dM~FKM6|*Nd|JKjE{@lEgf>pS(0Hw|hlknSub)~opgNzp!T#gwvsJ)m
z&4;8a8yZknddR=-CqJUkvu+|KS{(pEQEhE#?2voVz>lR;A=3v>ebu{~@5W1U`~wKg
zGBFjuK)Lv=fY&g=QwjPbDl)yl@B=
z3l~;-Y&?FbaN{y<$kaZom=N^`QB*6_&6}+!wfr6HCz_g@-aZ%zY+^ntZ3{P0so$c=
zDFGT};$}sVm_J#kRZptIH_+D&o@bJ~y)(8tMHJeKySApg7s@8;udqf|);h+TxqQ1jd!|TCa!N(hdNXTijk-Q>@xiRI)wT((RuNun
z9$}E;JcF%ntl9ETjlbf~P8Un{L&hUx#fMlIL8_@GU%67Rw5V`MVw=DFhR!RM!Px&U
zi3p3(=O%Uwgeq|!g01@wiC=@wnr^GtZ;8LPc2d0V(hqwfF%y&wK{gL}Rh&n4Ib3+(G5r(TkA
zy&-yyx5^%E3Bi8w|Zwr~$@9$z9D)@hhGs
zmm9x-*Ov%JPN|`L7~Q5B8>~${nbl;umvK95*A9Kxsq^v{ho3B0wIE2#Xy^^$eqIjv
z9%h0K;|=)RRUpj5ny~*uo|%yJZrGSA@B;F(yM}%D
zzMdqj$xzYp_`bJ%bhvC)`-W84!!AI;_Uk25s)+GBMXtAlR)`aMu8VaioaHb%`_=n<
z(Ae~w`14Jl>piLCr^L+@lzynocd-#M_0{iT2%3sMsCvmmz8%K83Nh;tgp3dCOY!A
zh9rLFt)6-FM!m=jy&io^`z!Z8({+-{SQ^InB{0cQ+nwI8+ysr}BDW*OgyW?W8iwcpgzL
zEVMCQ;})PkawD{1_4ICV3d0NkpYlS?^|)Vla4IqEEX3vAyB$0=*vds?2}!qVm)-`B
z_z@-&Jzh^Xy&lN+hOoUY+K6VXarM`3MJR29Z-Fbzs=lYFfz;9tiI+8Ivesp$fKHYwaMK!$rsP_Wei9j6CrVx{QYXdmDxeL)3Up
zsU`sjw=}S~*yNQjtG^(>VZzMJR{brIC?3Q7Z1odWqFbA+Yu>`lSUKzSj#fH#^-;n{
zIX7Q=#&PR(=G~l%%>8KMXRYTpBoa!J&5-(vScWbypUo&-kdCEV@AZW4glplH;8DKr
zjm(*%?6!*}S@`U=vqzLKx#Dr&%99vJuGY2Nd1!d}Q9iQOb?g)+$5s2tVCj#~nm}o9
z{P8^SOFJjVcY=*m9C6el*KUWMlrOU|Kl#6v?f!48vj1@27e&drxwjaZn7W~~{6RQY
z|Hdn$?4Jd-C{*&98^FCn_4yf?iBBo?aq}fnLw{BLz$Pj``0tY7e=R`c-5p2fatB~zBM_6dr&OYf{44-
z#I}0ZqyS*$dfSGRm)q_XnlPU&?@u-*iSa#0w}vW!g2$$IZ$3vixSF@$
z2CA=-^t}Y2RU;82(IBwU!8iouO1)@a)A9N@k95G}^B$?bo|u9S;`c;T(9w;m!yQLA
z2knIti-a5dSzR=AcW-K=Rw{OZSCIJ%nA_Ajlnnvv?`Sh{nKesm#QCy<6aA0OU=Z2>GL3YE(j
zDsqn)q}#vPQJKT?=g*(hmJm|jd0e4p(2H>*)pqQ}1-jLfO*_Yz1PhhQ>z^so%TWZs
zDo`G@ud>Dq5
z+t`?C%Db@0uqp77;X!HKr&FM^Jv|+alfz(2IR?hI7ADOc*iQT=Szv=3-1A$;MZ9K8
z@xL-|zG7x%WMoi1X|6v96C^=?x+%OFI&)^W
z%8O2)zF4KT+14C5CvKFFbQQ!YH#l2^Bg$Msp)+&CabO_NaK9b2e``$&WVAAjo8MhG
zbq3{q54=E}3qYP7`$<4IlHwk5d=#*LN+wpIY%57Jgqsqe2RoFm{1$C2B_8t=LBc}p
zRpym_CtzOm%AgA&3$V@ELvUR69`l%2pDg4Z^Oz1FV~E%05VUz#H(l8t3G5U=7M5H!+*%lHL0CT{s5d2{vJN@e8e%(k
zV!#^a+S5QL#R%*sE!d=5xvfrM4630=x;;vc2D|&Wp){G&><1$*+bqPnwUs(TdQd*|
z^ie1!BC$R-Q&H3pqY#;3V4|7TZy1TXxV6xg3Bb
zZ|p7pk{5+aKNr`omI8Odh*&IZoIHVnD0q6Y++{iTRV>2e%?_8X2Rp%n=Kxp9WZ86V
zTOXnCRri_TAwNIA5QJEa6!LT@2|Wig@4_C4g0~o%nI9tJBrVW=QpGcIbbqFz(vNozi-*Q*RjoqaG*$LLY$bA
z1t#C}_cs>?Z&$En2MtkEihb7xYmt>63MKsXJ(t=mJY)8Bl3z)ccsx%Qi&X8qWq4>|
zqe_pEJe!MuaZU>SNx=(+-LmSt;{Y9^M@U4N@9AO{32qHgGYJa-ca=Y6P{`I7Kvacr
zwVL!)KaXoA4Dcc!1jQgt7rZ0;wOnxrsIOp9I*h4bBPCkCS!co|DbUElLlc|e>7l2P
z!GIwnbQnyRgPTaFNf$&q<{4{n#kSab?+;mBVncl9EwpH@;Dam>rImyDn4BX-qT*YP(C9$1lJB)rgs)^TTK67hdrn2E=28snsrk8p~nv2G@7FqV82
zi|%`~DFu&RpdHG1z6hM7nr!zJ2f*(Ug0Ld|RMa*sn#B)c&6Q_P+JjT1xwidn>jlFY
zGL|;BF=eb4pdXE!e!ar8oI*@NExTkR6<|a~W3>QRz%uAE=2?&oU`##!EMmD>>(jI~
zHco~TTE+|bb<@Q6L?%ew`pHir;JRYpc5VGeq39iV*lp-1PhN)Lxw1z&f;ruY){j~|
z@Zl&xg-k1sds;%*!a_rt%f^mrYmd+~VwVjC8i6*5LWoOAFzFY(k@DKi(4`d>1#9dy
z0nhL|>^cTR0Vpd&fCT-;PeosnFwtL&^qCFAEe=`+DmLQ<=>u&q8w&&-^G~tp`Wela
z-`T2nZtQ|a6$0i97B~M=4A?dXKO@LktpMTIuecB+4q2n0pPvn;4!*6oGX=Wy2{+$1
zY*v#K3rQiettM}^V#^$+S)Fzv%(pIG?4U^Yh32K^Rzhl}fUAOgnjOTqg~WCZLmyVd
zxJgS9tEwK7RTzts`6=YPVj$(+;jdnV;cvC^Q*60&)TVpL0bO5`#Wt0rcuuQ748^`;
z@~lxP%wr+-FE<~Ye{0`J#&XjZ68vD#ft%ev7^(9+KLuXlH%YW(R~OfLcqf>&=|e-R
zwk!B{^Vh*gc@TV_RQTd!gh&MlXO57cQ#e)Not)^uk(tF9=dmWahWM|+ZV1#od?6;x
zxiQZLQlEq~7!DTpBCKcvZQH0qNXM7$zLKLp6B-%?IB6g?b?7z=lhh@{#(Kc_!c2r;
z{U!ztZoK;>6Kz5*qp(FaI~#8<&$V(I^e&w#su!P|dg
zVw|kV6@%wX)Hg1~{-!BEQIB0jB2>N6Oa-f+IAGM1%C2${I?STN9K;6rzzk6EzTteL
z*{Y`PZX~_or9}X-9ZMH;gae=XohS7cf7pDXDYwBBaWnqpe`Ed|O)u6ME;xGg-a!7i
zYY}KGCW+?kd&I)A+B#U349WhTd3d_)s}ef?2?rp!OVG)Fh>&3oK4PD{Bg;Z}{mp*;
zjEay%qtkASWWq3qSpPWBNVsRavEUJA9ZJ5y`%G;2RK0rGK8*w!{vKa`dzoszgQ{t$
zK@RJIq{(5^7wS^cG}D(wcu7QaHw46*{kXA^G%r<@uXmw<@i+a9TI|$Far*wt9nV6w
zn^M(hIoN77uwr*E
zG70|uf^*pLyzwTlyS~iLL>LCPkf2a~=L$ps^Zu1K|Cbr_f6A`^Z>c+z3qXjZx_TtQ
zfG)2cI#~b#@Es&DOM!(OX~Y0>)Y#oU;Wo0pB!Xd;v`5|2e-6hZ)b-43NwAH==p?zV
z|E_~xg!Jp_PeDfgCLUby1aqmTnVPdwcP%NBp&BPtMt-$2rv8itNCZ9}E!UtZt}uYlF)
zN^oq|-D4CaKe_{!lnFkkIhtJMd-D9CU=cp-h^0J;7d?&)QqW=34ec&VeNc=Js%qIa
zpabAfn0$&L)LK
zS%ImC!m4=Cgdk(iFBVDjAXU+VNNAt`1&88a<(IDiRY7+xFrK}I#>Q$@R
z1Edmo(R-^Ju?yMRt+IlAw9G!+#a@+tO*`F4Z5}DJ%p(6&nH8YN&7|EYhkie6?`FV3
zgrK-;Ul&p~w9*vm?oZ&0d!cJ;u`9P2;`m}CBIaw6_XU23UBwk`h**XHg9sdtbDM%j
z>H0s6pp!XF3=C@a`_Kwp;zz6UP1oh$t!rJINaxzqsJdoyC6?pPwfTx+{nfokTvv{Z
zo)7&n{2RSK6gF!4d`z~8Gt}VUHPhSMm7olwadH_m3hbK#ucS2Y*$Mwyj?ob4D74?H
zh6?JDYMu@>!d0#QRY>_sU!Tq~dj$nYHC9(DIdY}UfZXEJOKSyTSxJ9XM|}y(VfSu6
z!-Dnnw6&o2*b54)4|>h4jg#N~Spr?iOuwWER!=wqQa{;43y-?eVJl(|g%&pCt5Rnz
z73Kz@q!Ye$b=X&j(YXX)S|N7Rn8<9LW781U-IIh;Ugf!={_0j6zumQCrFv
z6`2p0uC~3vA+Xp%1XMt&@=-(Nht%2qoXC!n=PhQudDDFnLWn~mqWD$Z5M(I@xJ!}p
zY%#1<`yx`jeg4s#4&|ZkC^Q9#0)c^1
zQyvE(%o~?6eQ=*kD?%EZ2)aIRX=LWKAPXnnfXlKop`oG%wAkna=o-?QeG8~bc2UT4
z&#DJpgLqcopfeE}SbsX`k(-S`PL{~|GOO>(AqdSC?cl>KlO!L|3D~#1cYNi7z9De<
zH#yFB8HYfA+2bEsEuYWMaDmPoD+Tba+6x4JI-V1*#L=xGTjAeNPn|P!0za*H4lWs}
z+Xv8jV85@uWbp6z0yG9t2$Ke-NFwF#Pv5jENZd6Q$lg5wcu(tv+J7P_F}w_3LG#DZ
zpt`657b&SH96f~$*Y?rT5EK{U)_DyiLt_9wB(pS_4qYlSYi(#|CXd{WLy$AokrwoQ
zPMhH!qN6cnDpp2_7ix|UZ4qf&SoV|(^j);#)*>A>v~8{R69QlaC-8dqR6(u={4;!gZ5X*AAh5t2%H7Z8bwr*s^yK_wm6#0EhPCpznY9
z2{=?G$v@qkOs-sv=bHzMiKa!v$
zV30U}03zzh)U7#OhCXVTDCQK@GQd*VtcmzC2QLY?-P#
zqh;dx947o7SJNThQ!LvH({@iyz2Wl!$uRCZd@Va@0#(oH4wYFGs-uX#&xZ+C<
zE9a99dqOebb)`AKH`7Pc!bfE~u+MDbz}oYnkdQoCbvyIKqE-|uRZ`nG@LK8aET4q=
z-qCN5h1hcyLh;D&Go-AU@2M*xiIxA}osJtDhs7reb#OtK(?nCY>L!JSoB1{M*~Qg6
zfWl|(ZT*s#V{>Ux0=Y7y%}IsnoO$Zx0uNY~;6FJUkeQFhZt`pM%VFH-ivO_730qUl?@14Yok-K(SF
zb2}x-gR8x`k$N2K2{7GPnHd;LZ|=}F!uC8w^H{R
zrg^6iP+H23!kYoCy9YqrDrcj`Shh=`XR
z-aZ0R>PL#X-p~Z3m57b#G0Z0;Yk^o$Oa7ZXtmlOd_pVvHvfDWw!^t=@$
z3-{|LY?S{l>`l`FbUtqVhQ1I(pZW;-Ne3B1B!V;XAnxTs)0LlJmbak=zZAUf0Ya_<
zqhRXUUP2locSiDFjPG*tqV8@Qa!aIAn(OTUPC?qXZi`cSZp6aIoN;%W@6-O(3iaKf
zh2YF{>@&g8P7-*9%c940w!yH=IQA0`vNe}YbjSzz&QWkLtOD_P01lv!1QeWRxx>V&
zTNGB(SFJ`Xje-QXcD8{T6MlHOzHfeplN~ObeD=c4{^y*zR}lK++#=ZGhc__W?(a&+
zpxup=oxp;+%WnjHs4z-9zgpq72M!pZS8tU925^8^h1mE;H0&WylHyM#d>FYgF1hL&
zbqU$ieg4DH7$6sOOTTszqFT)U?sNu^n_(szr>KKoCTc^^eKpgSQsy|-S*no_w8wB5
zOVvPWZMc*YmyI#)9N&s@{xRDI;CwVnr}FOnF=dDiOQw1Qn(|5=f#&$Y?}gc!%D&jY
z44o{x$@AJ_I+aox$LUE!UQw~j7VfuZ5Wt}yz=4V$Ydbe+S~%K+Z1A?TP}qXyc<%j3
zShaShp}`@h7YRmzl6TmR;YzJ-ZEeL#{$jOs0+;gE
zOnOGP#xiW|*bu(!RkM;=r%>_*AP1!{x8y*)PKD~nTZO!*9IV8sc^pW*f|a>YWd(G1
z??xSCTCN-DHi9|uBg(>Vw2sC&LAa5&p}O<_Mw&6xsQyAT`;yIQQ_M
zpTD4S7yp6Wr48BK7z24(?D=Pp2Snti1TNumJ-d4WEA7JF^!WJamu9Py`wxU`*rSJD
z65vbM+5~s(Z$|Ymd~KI?jyu5q9X%a+8J64I0#;7WjSq2gx;Ew%QQu66&!2yHeW-2T
zj8FdlF;l1X!6>A~=-inz{Ptx5!^4MUVMFl762tte%D_*jxUi7jbQil5_Z!D0>*YE^
zVUHdAp|bLF@@WdF-7gQ3R-TLZ0YnMN=x$3gfg$vua;OvNCW>SAoIj=t`^WF@+t&?{
zRpWpc5ZURt4Ax}PQ+K0(Sss58&$4t&in1|0GBWLN$6PTRB5(XXz9xQ|!-D`h6I|e&
zeAg}RwrAXR{dWmK2!IHDr}0*?Mv+A%3zNNrgEH_*>wi1NRkOBRMbA#*nrP(szkc0p
zutT1D9nMorPFc_4zX{1v%7cJ5)ST@pHGLzbzqLV%!0|nTF~RqLPh}
z+gj2z7)BqqZwYORIK7_&rl#lnyvD4rcubx)7(>zX)6*_G9jeRVjvWTSYl-~*p7Vc<
zIYS7q!|$_%goJUWhE3SmIU{D>t?^Z7n`|FfDQFRW(q@lT&l5Xru7zDz3}zB6}fInsTV&H}Hu
z=#NFy(ERG!ApjIvN?v;!+`)4K1Bc-1c|Scjx5oxY<^6FKcQf%mNM!V5z>4`aK8^?F
zKQ9oCR>eJ7k%gnO{yfTRxYSNUN$JuwDQ`p}6p#mUbH1nGAxe;kc*!-83(+mQwyw?`
zkA4Ms-TvCd>a%XZXhf5bv{}!3z|eFgteSCuJL~xHF((vlE`;X|9ju
zJn-he(1;ch#cdr0zM1mLU1*Ke1>L9pw`C9|Z$d1H9vOSPK$t!P!jJQ+?MS&Y!Bv6M
zdh4k&=x@|o?NF<9&2xv~y_+9X57j^qboVJ)S!G5+2QqDk_i6*_9AsL?{3Yn!v;e6W
zZ3SJ93Y+jc1ntcyFzD~yfgrFFLWhTc0;QC-`VO*&>xzo>zMORWRg0}$;cU&NU;FY#
zM{-I^2EqU!z0Taa`@q19%ftz3TMw7!eHE5FS3U+iM3kYcK?(T+_
zk3?}<`mdOG!n-AU%bhH%t>~|NUwZdlyT;3N6A~+l8!H=|T)^eqV%Ru1BhH&ub!a0J;HfKYqDgX`V01(%xx
z)1L~+tvv4c5Wcx~deZ5_XDFzcCa!5-g-#ds7=D*_Ja3Mqhqa-VpWv+`t!-`d-l8+V
zKXKcRW?r~>Q5ovO9*DY`7JZrK0;W|lYWYTQ_8`E7)zsAN0oQ0?#kQvs=W&CTca}V3d>V
zs6AL1tD*MHLoJ&D%F`7`5nsB_~}s0ZsA|v^hk(uYAGn
zg<4wK!ouR016vIy-yIx7{@3WL>@Ot2(;HJtNO!#9;?+aym0xSn@0%*LJ9)A9lMDrQ
zkJI80<*DDl$vdi`;YN%t-WA@H&w5A4prq!1|_cKdUE*eYv`u^F|
zr#ae#LPjav0%p3B{nl1iZf%u#A9)$hP~42|3F?V#@V|UJ+e~c&oa#NmrW*-_^OXS&
z6Y#5S?Mhp2BeZom0drg%^?sU}hO9k`tIf62ebXWlt=4>ACXIiWS`-S49(Yej11UT{
zp5^1%Q`4ZPQB0?UKe*#}G15Hk4vJ8~DBk7RJAg-TbO^&sI2uJt9)e+8H{g`vY+mqa
zDEKaw2`+Oy0CIo4>xQEp`xeXnp(Nk0LqkJ&?tMu-M(`H6#$8#+$|{|monp%aAmv+N
zNkl^D^VJDcPUw7VwxpMfwaTOtbT4E_Z_|B|@tNA3>8u-w+c<1FFQ^qA6(W3I;&Xd*
z^DQ5~bL5=O*`AUCl2sBTU`rn%`@~dapPUq!#0sRHMNin-Hpq9^GQWJJk&s;O2Q4vR
zg|@EQ!^4Aha0w)wMv)>b>Sst}aihG1CGxJaUxt?(BVuB-KW$$Vw7W3COfw)U=UW7K
zn+}4U2<(i+$1z%{ak%N5PDg7xesR$>&mNsjcnP;7VMs=oO^|kR_Dk@nTpHsn(HT6v
zTuZ1-_cF=>-JL-vm#DcnW`~}AhFOn0(kiu@4}vlP)lWX1sqA1s8o1%uth_h*(+!Gh
z?vfCP=SF6Un~#ftK
zA7>DJ4W}I|zRlsBJ<9FR
z3Pyv@7QlQz=5+7Vd&zZKX9u$4<>{kK^tcrljCA0QYSdrV=*sR$u8wkPCh>f=kBwll
zZ;$$Ln{E?{qSL)hE$Sq(X_ct!rmrW>srH_+hiW)
zhqf=38+7N$Zr!yWtBx@!6{DeSYcQDH5B+S#mKFk~P4VNI#GdyXNg6#6p&zSTh&?Z3
zf&I?G%4%?(v;r{F@hxic$~}MgVSQq5&b?*5YeEIyI)soXr0Q(b-YxPEcy(v&Y2;gY
z_3iIsN`Tb~c4(zxZgHRe_O1;h%@F!n<%1U4J@@S-v`l+Wh{G^+8=48wJMbPo9JO41
z;y^&b{k63B=~?TLUoIRE9@VB*x|9VxJ=-7pola1&lzZ~YyJfZC#Xch%5*^mihc5GNwBQGgRgUtBat~$}9qwoHetd?C1Ce>_C9i|eTcNwA@
z+1KC=jF1Po3`f@W?8^2(wIp}=>8{+Dcp4II={G(dC+`7~D>cON3{cJ$UHue9*+*^lbwY^=Vn1~80CP-L_k_sXvp(qj}-Ki4NNGS~l
zxj}q|R8N`?vRdzVCg%bFTBp;ScwbFDe&xbHFU
zaSNP?qwfa_RC!>n=6wP+jdJ{y#ngUWQSrhGEM*a($+&~(|$TN5T!BW
zr3z~(yOP-j<$LLQxpO4Vay2OjaR+&JR;#X)i5B~wQ`m~wPFU|k4Yezi9!ecg0o24%
zepiJD#Q$HA1#u_5J$0gs);os^W6Jf<$
zYKb&p$NNNDBNI<|?LLYV4l~14(9euS(0jgcm(g5BxH|1!Q&UrJ5fKqICj6fdIMjxp
zogKXYq+(W>Jc7D;1vI|#fBpLPJLI4`=qV{JzYttu$=t==lGW^kpCUgf|2i-)Siqwo
zEsk?L;M}eczliQsAd{S0V{7abzLef$+3gq@
z7`W+-4Rqa9gJvq{K>6`)nWWq3Sd7}
z-r*1S{S8T1u`eJg@z(zy9RH6W0D5M+LwyS80i1TVBD1}DQ|O3Q5GDw)b}?^eifrV2
zZ^Sqn{X;{+M=DPdcCPr~wJcOweM`XR-*gLhX9|}tT_UG#Q7W?!0zfCec`^tXE*VQp
zjnUL-XS+&7e+&rc7cmqj-Q|;~z`Nim#aWHHfG)uxZv=|qL$llN9D6W4IM%t)ws`CD
z2VuX$p+2|8DMLn>Or#rZ0JyXA-k`2XgUBzn@uemEj2LpP41w!I#aILv?a0Nd_7B8{
z6%M;27o60NoYXo%z~gSo6yQm)6t0swxv-zhDDxW9M{D@*`VDL#;MDw&FD3iG7iTMJ
zN$j2YaS=6)IuaW0-YC;PjrMX
zr>zkup({czod}GSs~b=R^^r*7n)2x!=gz6TdA9)8B=_q3%ACLU^f*CpBXlznx3zh~
z>N>JEczRqpULh;g)ZgFVO+*WQ1FD6w&&rqlSyaC|V7r?gA0MB)+k`tC7s8XeA$My=
zD@~-q#pz5fX=B9o5X=Ykv*PSYzl~XiSBeA$_qeHUis;KDuILqr>
z^5$$w1+wZ#PIwRE)EE;APNRl6{&VNfnQhv#CI13D#V5BuZUO0R?iKNUw^?^#K@Te1
ze2ZL4yY@)UETh=4F&FyD`#@}`7&tj6KPGOv{>I+u=nyc!u`JcfC=^G4&AycwssIgB
zhK&wC1Q?&y?7ON$KhHE5EpgrGtMJprt%-y?mz7jk(LzXXZ!a|pO6|sBZg^Z(RduX=
ze=SkI7d+*#O-xeq+E0*1cw#LmK(0+c!%`?8I80_nm^$6g&CLykf>8C!Wu$_#$j$gN%ljr9VZ_5R3$|#OS%e;H)M2k#79nn4-qu;r
zDsw*&3Jvh3m2Ut2t-$X;(#l%9%2(>B6R-%_4LEKqKrYD+`s(Y&F{i8Y-v{
z=m~+A&YBB({RDS?{_fqoRm95IIWyWh^z`|2r_!)S)k5}oTIV|}V|PrOH#9VKZbAoR
zW22iOLC?m@`tcMD=ZcXwPee5%f1`uXEa8qYo*7(;8J=fN+
zU$2XJWbqlr)ej(%s&|{H^%{9$qZ*-yZj+0zMROL#iTQkkcZky9C(GcuZ%>t^*tbQ;
zo)EC9eZ!$5{SjIC!#ze`Cr_T74q($%TSmOn#jt^UvDIF_^!J=%5m_fMCwD1&!zsOa
zLF0UDo&0_X<|Lcu<0hda(w^+*r`;29={euD?c#~^(hghJ2E3Lg^POY~7;g?^%>BG)
zeZItIv%1QgTm=p|BIbVIx!XasYm##dU$BR1g|Y
ziWSMue#xDS8-wkD=e)J`R0`IrELUM_yK8>z0%Y?{92VQv7~4&
zrul?k_U+@+BQyK*<;yNC|HLE?A=`O$xHcowUd`M(4_x{w!Mrs^;wf6l`Aq8^Td?csji6+Md$!!t<~MkD$)p#>T>
z>Ja0Wd}z#CNa6Pm2#5ufmPzOh2kd3p)_cocHkIAi5w{gz2K%fy5aM6Qi@}bEfXuYN
zCTy(di|mABV{iYf1$E$$kt{K7!_r`Cc6bQP
zX|$vWFbu0?!Xyj#!-61w+%futKYL~G?*d@;8l-=YRk6F&G=(AafnWo4zur#CFDM~>(!
zAxXD^eTMS
zb-krnhd{ALKZjs@Ue=uZ8D#k+aeRnhLMmT^2zy@Sy?2+1%Oj}jiCGoLGjvWwq-Fya
z1z){ut(UU{nm<|NYybzl8C!KZ0-~-GavLV)l)A9X}`Kf(mn`jF`Ld>K)e*i6+0N
zyXgqt1YGR#<=N$Z&};P~D7G30?B86z9U6TCxso0e+?CGr=X*S!CwHa8h{>*rSugM(
z-{5FCdFargO8aOQPH0tDAm&*Xk%Na1ALdMM-us^y-MsJIxnl(a;*sRJ3Jw3=1q8yu
zFZaC05%_IjAP-{4cbhmuD8PI_z6FZOVPp^q+SqOkn%)F{;*)r*HDh%eGJ3%&tvra_p{reYR1P7~cN=9N8&(i15;rg^Kz<33(3kr7XJ#AWr
zr^JaVOo&Q*fccGXNSYG>o$5Am6l9#Aq^6p${qrgr@v5Yl*pKP)an(yYxQe)rj_YfS
zd2hEN|EUOzSH;VhFMqKe9UUD+rdCl3_RSgw#{3{#rU7X7wU;jehB+bX%R6@XaAc0N
zJr^ql35m>HZN^5Pvobp=Gqq4Xq=?+#TN?xjMyOc0pv7L9-t_`EW)M-{G0N{#&QgFV
zg<4u#;}7Xhuik?B+d&tstur@o+9Y$-r(C7FvQi!fOp4$xPy6e!Ri{0<^IOreZ6%-*zLH(r$+zsOswLC&2R{0c6ix8^8`D
z#INsX0wUK1=Tn$yVQ6l^*lp#(;=dhK3QLMa#IlG1pfI5`Gc$Whe95)KE%EHzgH`&IVN=7Z0$E9KZFn-EMVOn>2<`6f)^>uR*$D1U
zOk7-z-zMc_E}i_QXM?o=ufbyfz0}my!NI}p+AgHzQ-g6#wbgm{ZSk?&E*-5u?wr5!
z?Bw#*(D2(PedHf|ZFLPd(r@?+JORe)5rDknXJe~QnU5o<;gLa^h-xxwugV(fHIa{i
z0^?DCssh%-MVJy*OXzGNBb$rRtMq@&o(g)35leFEjk@Yk=0L@w6<
z!99a{26}o_0!9Rn5QvB5dAt$*5A0n0S@@p=v=1~!$W4f*A3M%JoJ|r}QAbK%b6x`$
zu{RbA&rCU}$+kK)HKl568xXK_vr+kTZRVB9Qt@S0I5XDmq6NC8
z-EU(y_``j(3K
zmuGy^h|%fbz2oY5&JsA-I=3mLA@j|9mNY>SwM3O{L%dfJC%(R6&b1}4zYWxB64=Kr
z&3(PSao@jR&%aIGjUbs=6l{@fXP~2_E2yAsIc?Gs4n(5ayRpTxCJWenZ=UQ7U@uT(
z#-kA!maR?+KEO;4Y&uPV_(|St)y>ROV19RB!T#4Wo5}Z~p+tf}uqh$u-Z!h|qql|3
z8se>!S{G%0PlKG0DZJZ+tyZW@9Pn|I#EcR!vto>LrVns{gdV#m!$+
zhFpeqM{fV#xf{!>sx$&aL%T8nDX5ySM2Xbs5f~(
zv~tyoq{?^J(;VRDzUfDyC*UwW=$CtI{3?B(gf8-<3bwYk@u{q){KR>L8-;7AKl3EY
z%gdL5wydwP_baR0-hf|@t*YX98p^%y4Y~RytP2h#un#tY&*$A(1q2F|YhZJl)(6YA
zm8T@+Sel-$?i2+%xs+y>ks{q$f^xjeRs7dlb$xyPu-nD{BEQGO;zhB)pI>7RCaWRx
zuT^j>TiqCBbtPT`h=V4q59|sv%yv@Ox}rcW%h;fRF&_
zF0UI24%L<4GW}I_CyC#ow2$=QiVFc=f393!0;xT;mfKs7grlS}Wg~HE;lIKSptE$7
zl9rnCy)2JYDQug9%950L6RSR6AeJ-YKmS4?8YfdW{BF=Bd4jUyP?7xUQc5
zvl`8HZL@vBVPRn>4gOXzq(s!YzdZT3Fv3&*>xt}!28Ep^e=8%x*O{u9v|yS&=Kar$
zBn;%&ID;R5GX96)0YZnhYu8S&GN)%`{6A7quySyum$})#;rP$-h0EW(dBa;+Sor=g
zQS2!Cs!G3q$FW}IHF<9ml^9P9^!45Kb#)sGZjHYv$|yMNQyzsP+$6BFG1=zbDM6XX0z3LJVwp0MtXYDTN$F#!PqE%xf>dRrtPU*NW3xzLjXP*$JXWi{H7*FJqV
z(c#vuTqDrGNX0y@FYL#*nt+^`oB*s36R^x0ff&6!C%BDXP-7nCb5?&
zHd$0EHFXlWR*;>2?BL=QQ!%6+iDH0F}k6gdzePOatbbU5bZC<*9;OJGt%-
zs)?-3i2a^)0(>_?f~C;t@{1zRIEY{ASmey(Mt#mE`5>_fh@1qQdMga1{rZZz3lS2Qyl-CZ<_C~Xju`MzJO>>9b@7*nV6Ul2#c4G#}X
zHqrB0i$M@pbBq00un(hjLP$u6Tn;MIm51Awp=2Aj@5KK4cr5RXI4j`@o4$l~OtdqE
z&*tH6{CKEXQo+oxfJ~cwWRu%c7MEd)C0_*1$TrgCi7Ym>|--V_57&jq}7>9f3ae8|C
z-Fx@OqBw-L@0-$+_A;O?ejX~tAH~0J1ey^57tY|G3JpX8Dc!ANo=w{*C{8!^_4QHh
zWHU#JFwxA$2s6|OGq7*@iBC!m8jy6RG<#BU#+(z%pGt?|QmOzIWk$da_l7F#jB$^^
z5;8>P9AsjWNY*M)W7T@y@;z(2eunB}8eTbuBS+$hCJv(4fs2nhYN8`b1Ih&xiKu9+
zA`O?3@5vB3|7~<<;!r$!5IU3f*V-`$A}=O_tYzZkQ)AV9rGRvIk3o`Ve$)5IPe=N6
zl->7N6k_xx4+}fP>fQ)Nr|+Gk?td*>UQ9(MoO5lANj=h;*Tg!J;Zbf(yCRZhGo;j`
zqxH54NqC(}PD$x*xZK7-+ZYGKZHMwnWU*6rd}BE)l?$2OPKnf57gXZCpJj>20a|_k
ztE%eKblKr2`$Vq7m?0hsqRrY?y=6Nh3yhmnOt;?fjd+M>O#vHk@~8IWBC<$LB(8)9
z^MuWtJW6>oAdQrRnk()Xvha@=B{u~$L&wp+=^9FJxF1$YRBeNDOrG?@}L!8BD6bj7}(*`uCqamCs8sQ+I_C1LX
zkaWLLF+V;vb?SCB%`QnEpNJcjuY2bJkP{z0+S=o)MNvVl)RKZZchB>t`5*M8q+VED
z^f*%lP2J{!-3fz7qAKmwC@mSDiSL&brbI*%y2F;Cm@J-r%iK~_R}`s|eIHP``Bnzs
zF_pL7L@Y@}6=U+}3Zo6AjKuBvqc^hH9ImOP-$>|!4o9gr`z#zRuH$DKlN^+EXRR>S
zor8s-0s=>lK}X=jL8$sp42lirqhw07K%4EBcxRc{RV?Wb-|-qZ-laLv4HIP11Kw#2
z1=Oe=IvwiM#Xd0N9ey-wHaQnt#6BxBUF6X?-#+mQ-AQI#%Kq(ufOg&fLj@Lf>W9us
zmDve!92tkqJLd+8sj4}vpkUV~65Jn*jdW<=+9Q}gis%P-g3iIgVZQ*MrI)G4-7MtS
z;vg#AUvR&){7u1B@#hLqEz7b1bE41E9b+e))CbEcL*EgmRJ~cKI5=@T$m{cHU!UGo
z+2%Qs+kH>AG?@{_{{4#f7SYO0a@<&WPBncDWarxYGr3rXwFMYd*5ZDT4IR0IgFAJ<_@LM44M`-
z75ZltR+g@sD(BhQM31E(EuakMHdlhx*qs|P?0a>*w085R1zdSnH+gjL#7|^(P3bo6
z9b4n0N0p#&=W^j;OY{_nGYS?OP~2fKRjXp&4fR$}LHKag2QbKma-cxD2gU8Hbz749
zzV0s_5_eBm%b-w@lccOj9{R{((iF5+)0a*w?;&9tY3dkuh=W7!W2iv;K5u4$tBCre
zn|vB#95+hlW-3aTx;Woxz_J7dp$6iB4{#m|2}x2)(J;JJ=fH49%6@OJuuApfOE0>d
zItr!Ab8EY>behsMNN%g*?sk;F^_jK*xVZFRA@m9h9KS3#T%=lScu<5k`et?A(A8}N
zZazB4N`{hzf?l%Pnv8R!fe%F8}(F+!F3W-#x3Qgf+ZjW%epT
zxhP3~q?L*&Y=2F8DP?cC62${OhoMkThq5)lu-!erVrF^o44JFtc6QQV98t3F!R2$}
zmbE5S&V~m|8jwSdLOI9LNK%p8u3J5P>8LAt#b>;nB-q13d<^p5y}Bz-mIBFO*o{$n
zl!-jrexPKcx4%b@vf^P_KjR2=t`V4>G8Tz#m)5qt=8%iomW|3Wb
zWswbosLy^Zv{|esFocw`X74PF6ZVxjGK7?8TXw~0?CUcE__zqtqK3yn+Ng|DMo%ny
zY5_q6q^d^|dMJTrUuGCuMhO))MpByEz}Vl?I%wl#q0c+^@m$L3?TIezHF(IT`D&NeCxx}X3txoY%_?Nt
zpd)DA6mZT+=5`2|olEKcFAqTq9a^I`6Y%WW^{sDwXBlh`XKh;nk%2HxfBVgTsIpN~
z#hZCZRYhA>mclGqTqWaZf267kTOOMUxwy}rPMG*jdrwbH>ZNVVta1LQB
z@%MlDfz<%>H}d>n9pPUe_!sj0eTq%Sako-ZQkdA;p8(w2xj62y`;XMbBn}C{E;zA6
z)M5ck%6fa-+W^Ihzdhsokq1MHiC$0=H579HLDLZ^gixnk(Zl?JQXsTGL+{@Q
z9(BOBr~n@Ll>54YnHtGUmtKntg-HKHG=r?nnL^~LNd*^vh)|cfiF(rHF(5H<$2s@;
z-;3qAR^Z8gt%ZXD{TS3F_ZO*}Ya_;Uu5
zF0ognL~Npk*d+XF?x*#B-B8IFC7@xFJ3;@SM7rda6F}_fuVQsHoK!(x;lajN64)q}
zpk+}2Da$KhGpNuEg6FY*2Ctf8#6M*)$oGsj$r~^JsD_2qnUrmtL^wG(2DM(_`V`ib
z#|QXhFzq%S0fo=4=?}Z-v*ks8mpLdK!JcJ#$v2}&-03r4E~s=TNDMfRojPT$Bqt~L
zx?K0+jrX%b{{Eume{09v9v~Yuz&asZqduTYE>K#_vU0Gc;tit2v-sZx8vpI1o3Nce
zX!YyGe-Q@56WAj8n?XIU$pjL|^XKZbJ_|C)s#|cA57{+qKOp&$70!NJbKfwAIH@`?cPH#>kDj9$%1QF8PGS-Dou
z^~6z#ESk1<_xeAt?j&CI_wxEY)YFsktQc1zlb82ty{pywELfN)e)|}lh~Vq(NC)68
zBB=ymRJq*hCR-#R2MMWjw$CEN(WAd$Cu1cmDk^HeIAw(1t;EGC9LMt{TH`rrSPyr`MYGNz7932(4ZwT1G(d(c{118Jn93MSZb6G;Vj@-l{x65PAAZdH|
zBh?)i7}y$nW^J&UhrNB%S?LjL{zp-K_)(jTT}!@ix4tMQRz`m1%9R|k%XNPgC4Q%;
zP9hYMdd{a99TOwLBZtu02z;OsE|iIbqwZN{dJ?y@TW5y?XxqlJrvdtm1ug-%i?dHK
zGbg4BxP4>_-!K#(n1uBp>B1ixIEd%Q*JOJ+BDckNofcjn7Ob=#L9IJGDl9#N?xvzN
zB@tEc@kmcydtQYZmV(?zD&b=CcKRQz1K;&mY^v$+Vv#=Ff_&1vA48houG*_tuMWCE
zfkO_KukX(pV=X3n#m#A71XbutTjYCt`~_x$s^B^wO+29bHBEi}m_f|;FX=xJLS_4m
zuwNuSeUrB3wY82%WqJ8uX}eoCUB@t?99gdZY*N)5DRcfYi94%21#15{mjqTJ<07xS
zKkw&*sb781@PvapgT7P;ikxRHjerzW#-5%a+Jj^q6l3UFPF{=k^g{VG&`YhKegx45|22nBNjq96T`BK@H`IN|M^On(KnxD!L#J$HAtwe1e}Mk@l9
z8h~Bq)2Ew;pxR>do6cV)$ofnWP}_u}v{RkwN-j&fBZ9VO!ySdWufVRU3
zSN?1(B*blKF3FPtg}b@K>`A?fU9p>+H)Q#iq=G_3!d2Pa0PNM1seMS?=kg2%XL9?B
z)u_qH)V{(xzi~jO*T`JQ0TK~Eq;jQM5JM051NJB2NDNxqGfrQ9_n@2^|$*xBpcb
z({Vd|=3tT1%JkJ>ptVNrDYM__x{`4KCk5%Nu|sn`}J
zCq1D?*$`CQIm3i70Z+DGVc7#knf>8QxsEQ+LixVyP$k9cqXtwqFm+?Rkh*!ozLk^k
zNLw;9gdg8OtBQKcu$^nyt(!-KO7kzM3q1pR1BEnpJzYk7EGLK1DIoq1={9sNW4Wez
z`LgFjPfsO6z#(u}YWLsTllJv{J8tXj4H$>~1NY+cn8Z4@8&G_zyqNtYNt#_6y&)S<
zZya=?d-K+02LuElQ<(P(e)OA5+J3Vp4XAo$cerMvem0rs_Ug(Rr|=>&^5(s}cSAB5
z!*}0Am6+br($W4od`|^-^$2SMpG}RRgntBk!@e
z@7`vDY=y6k@-3~9zEGp5PoKU|uj=bE#(KudcIwcVQJ{A8s23k346FykmEM1D@~l`r
zG(~ht#pj7Gg)RduvlHp;=&`1ukb7UlWRHCzU5|-yV5F
z$R40>wA^9>EmQ#v){ncfhJ|n3*MvnU)TdqlpYjOebL1veR8$4iZ}bPDIGosI@HlFxRE$wTuZV4^XHw?
zq}h+4H;USUqn4k(i8#jY8Y1*a9e;W={)>IOp%X
zyMF^`lw&|<6c-~wv!bvNR{S9K(yd}g%T>rCYK|~6I(!dr3JZ51+|>kHxP+tO1{!2Y
zc?c0|3}Ho4aAv(#`c`+4FJDLlAH&BHpr^K>@xpk7SLw;sOZhA&3tVJ!WZUL%vZu%r
zsIDE;MfIph#~m4es#Q-9lF!9yM@484A3Bttq+G!va)7Xs!2Np1v5SLXJ_<;;{O6;q
z#0Myk_Y4O?&evl`_PWD4{Gq>CCS1rhIx1ml>i^p$I
z3*s3^Cr8IUJ6l$NA=8Ptzff|WY{B$+nEm9*PtEP^4m;e)No1&iH(1Up1W#z>Km
zK$6O%Vm_2oB3l>|v|fC)Pd1UmNg1(g
zN?>4M1wlT6$M9xczb9MB1Eje%?1QNQ?v{>-h~45Tg#XJ(Sf(f>I=-6?>Ljg1%~-e29mRSgXd
zoC-Jl`bI}XQYvgbp%I@$V}zBC^vXDqia
z3Qdn6m0-;|5a%Q&Pon7a*HID@-*J+ncdq(2TxHkz)~l|)^fd7-x@0fzeEMgazO-=0j)_qy1hh<~b@GGKl+$Y&E?Ua3!MLM({Q-UH8r3zno0lx6_3Fwdx5{nU`7Gsmt
z$*&8|!aj&KY4fbfS`wa1$Souw01Jg!M?$;cm1D-Pvsh7D^Xd@XlFke8^Yhzb7Hos^
z++qF3jsCe2Q%QhGyDqQi!uIn1gcyly#`j^wlss4ua-fy7U0x>efWmI56i7l!$9Q>p
zhag>Xasj{8v2NYERGzdQkYZrYkT4xfLk(+6Fqd%?32jS4VG_NheE~-#7Mfg9H!0H8X{c-|TNIG;=pcRx9wn0Moh_${HcP?~xfViw_4_C!
zjASMtawuCyo84Gr!CQs?d841qqG{_@KST~xnktB|VFaOo6_Zvw`
zgMEB_r1;{d8Hx8e_68wjros}t5pluKE13N@x@?tyHmIHpSthONPtP2CcJUJwlEfvg
z0AJ!i#81T^u?Mci{=|R&_aFFI4(}x``+3<9*so8;l04x#<*0=uvR3x9NnM{uz`5T+WzKihMy5e4jZCOVp
zzvFLkMZzQe5A;J)eB)7s7ZL1cXdSQo$2WW;JfZqh{i9kX?ij^Ys?ETYfrbTzIxAAv
zl^15gmQ$!
zJ{Sjv4m2ePS0a|CuEsj{9^>v34d6}OGMXq5i%$X00(T(D<3oygK-Fpv9k|A}ZQa^o
z52PoMxqTHPq2DIB2TeE&m?YI7{J6;kifbprn<2P5OlWyO>xNa(Q5>!>yS+t&@WG;(
znw*>$WMws_XZ?*x@Fr~wG7bHFAV$P+?bFzF<_+PxOFX=!8?(N;nWFIS=~18KyxiQg
zB&?hM98`%VEf2I7BL_P>JFk#X*dL5jwsOQA^D&~8Wf?gCEc?c>%+;mPb=@7cm&M-%
z5uCd5r7`?LIW#m4N$b=tEYjv7TBk27FF%;}8>I2Y?cQQShg4>sHfgpE#FfH&xoY5$im5pdQGcsqh>U(-=Ug+@dMOEs!=
z4T&F_0PtBXnb8YusTChTO2INgR?om-|InqQK6UL0@H5J^$VX*l0)kSej8+pCXeQMQ
z(4IX3%7c6DSQ3L!B=uPk^z#~EkD=WHCM2#B?-0n4@JPyJJV5x0Jd&u`&VMAP5Y_3a
zHfT>L7LD`!!`F3fys&M>Mx3PBZv&SH5m{sE
zQTK-v#sNc7v8K>A5Jb_v0;AuOSEHXlz65lJQJAFgrNyJxiK48ghH+)|e=g6AZm3E~
z@1p-nt)F}N!LchwcG9ot3M*U~YzeZa^ZiKAS_sT2opFA@Z7zoa=M6JlKdETk}
zW-__3!yUCoWQ;rj2=}7eG}-Za?F?9~q|HVr(e(Q(!GEH2c+UG~!hn5{=r8zUtI0)w
zw-G@%a@WzS&I8ToCZ&$BKuBMAv_bVz)#Vq(|e&ij?$K$SaZ5umnp{>$x
z`_w)u{hTk0XZ+nx5A4K+gWc|1spK?JK2nMX3XLhv*jK(uVn!U#&@PEef4rP}wI?4Y
z4t^e$ruT$c`Rcfsa*{+s70oJ#Dfn783dost$Hm9nb&XyR{`}Hba2(YA$dX^GW8Y&$
zdN<|ww3#A?4~9Q~S~t2%$|@J+(`J5vLylH{`O)A8-#5`QbIF4ax4~#UE`j~>yLv-Y)1EQMe*SjahO3ZT&^tob`C4XU_JE$(a83yY|5U4r
z(Q!#}NGcoix5h74EVh16^_Zzp*QK$lI(Y{n)F~6NhLgiP+7cn!WF~CEmekSnkFkPX
z$o$DBv3S6fP}xjycbEk5IN}s86TtRKbWE}TlVN_aRx*;9)b2+1^b4eVzt}_pcM4R_z
zPKc_cNajwR0hyVqfKv6*6Ucc
z$?!dmvs#r!IX92%qSH3LLqO`uFAyHgiCTSZgN$hq`WO{{%!A!19K0kGJSL6n?C2Nd
zPTOjHr^2c&9jf@D}wZ@6@@dItR1!Ee{udL?ATPJ#Y
z&{wUg_O;z46PJRsV*+DSZQ0YqjF7XBC&-OukrQ9zO>qTN-E8E!nE)}qOSpO6Er<$5
znvbS+;_x
zH)Ow_n+DOZ%%Zj6!o8Vj138{-?v&V~A8h*29A@Qysfm=|VYYp@Vs^FvbM0CD>}RUl
z+Ad|7n}wNK#kT0;#@L`ZsCeQ(htz;yUUFS3XI+h}sBV
z6KJxxxXe{*pWeLE)VcQYN^rMLo2tcs%b!=&otzeb5+nrL1v|Kz1gl7T-ND`
zttOIKKKu#cGwzyoWO26R+{9mcI*DP#^7;3xO|`Wr3~@4Yq9LgkMyy4pp>+evRCuv%
zpJD9tnFi&eUyTRx@%_Z_n|fC4?@DwZC8xwE_dP@R=!+Y&E!$H%_O$ONG5KDVw5GNm
zLBI;6{m(zRfK>pz0-#s^S;4;l`RBj=?0@;f|NPn7!;LK)QW5A{&runKjAyfBB+XUZ
z$L59&gyzf8lyf#eC@5&Q{Z8D$hV4e1xb9NRiKK4eG)|rAK=&|Cmt=3Vk3#9A75zd6
z%@OW0BE-ky4qh=`%yYm{u~WcQ>I$pq)`##QWiOwcbh4#gImkJ3H)_hJrm*}9>+Vx9
z%xq0`kVAP#U(Z=m+9{3Du(6Dx)ngfLYVbWRIGL-vam2gR5U4GkFwNi|ci`SYfX$XhjoT}^{Arc%u?e;}^Yi~1Zn
znX#shRDE{iTMkVR{4a4JT;Gu-n>S*@>h;;!zgaK+m(MGxBull=3{F4M)PJ=H<3W52
zLnEd#wANIrU1>|DHS6!67>{$LHQhVBCeRj;B!@d7{=8C7TFq2~)YfjbHYqN#@
zrPN&8CJ264E^qZRO7AJgEVcr(X@s!bwi(7=m{Ys*_qd%SPnPD=oW2tr6lCwx&)+@Q
zi;e2$g2*<3%z9wi`RY)C{Pzb{xly8geIF`|7bbd439n2D-ab0$h%6Q*9OQ~}$B4=i
z!x!a#x|e#;dmS%gET6*V#j&tuv>>$o3~8$YG($z?xlQ
zKi@GvB=D~LbQHGXTr5u>mM-jC>AK}lA3uJ~JvFuLLtLL2c|38kxY5_K^tV+nJb{U)
z$zVX?RPrXwH
zndWcU##znN(~y|*Dxn2sptRGMedB*1CYsGdbK>`0r%x{>Iesq<{ke=&|Go&~xgj^b
z#MN;83hQ3MP}~+P{z2vRD7PO~=XsS0>uZu-iYfB$}uwl*~!PQ{MKzT?fGK_ezye8l5qcl*{xER~&4h)RD^?!KN6_2kT7mz3NJwsf;PqNAh?4Gi*`
z(mfpen6-}+9gnUSyRPx0=0g)m4?_C=xO=v6wjlLqTXUfj7D77B2?v)U^=>Aj9mj4w
zzoqB^qDi#$^6QRA;R1ybV?GMwJb-dz>nIA)GbS}tWX!I{q3Nd++AuC_y~abt{vOr7
zdPNQ!X^5sFdr{ct@bYTuLkU)=-oy0A(dtH>G}{Lar*@VSxUix>J`6tSDRO%Ox5
z8|$i*A9f*3)f$-vZV)NOZmL8yV8M?f%K1uT1*hYc&-hOo{W7!;g_m$-E^LmO!w7)S
z0MP8GoW*p@JjEiAh(tejk*R~UJ4cRAw=oz6OZrc6iF9QCKkPzv{9O`xf?#D
zUtuGVLh~f2V8qm~re1Yq)TPGoeoEfApsUcCC7yOGnuHMEB_U}>Y%xmu>DjWZKrslo
zoW}!e9AoM?9-*`AeX86bQC+|~Sq#9aRKAWlsKdgI_;#7iEQ~qUnb**3CT>^DeW8Uf
z70pC_%nc+Ql&KSug4k_tUmvXI^cYI1BJ^+H{}BD%qvYb?d!yO-Qxjg{erwB*HR9n@
zr_w7EAAsnVjSk(lU$`tUmBRJdBd2gW*>6nzU|%=#_?k4Zn<@2IH)|cNsk*N8_Dwba
zn8sYIra)!RNrw;oU9xkLsS8(pKg^e)Qi`$!CfY?rMPC%BpS|ZGmo~OMm$=kL
zrHU=@IZYLt$^G|_sO0C)M7B{aR&G_S!p8QqT-sTVMZ56zGjz_@dza2NkXD0EW{MvK
zGREQ~5WCd)QKhb*GUE5We7Vg#Q^b(8UfhF7uMplV(X
zs|hEnhVnTUj>Lc&R!Jr+3dxI%S$?T5Kkm>g_tXA~91swtUtg`~cTs;--p6oV_jJn55<-~)>oV1l*pnlU73kmw9WHs@yIJIk3JO#bpk`K2z|F|Q7MmJu~
zNqSN2oFeg
zqL_pEiGdP3ZD_+a>g0x=HVth%w6od`o2e)3T0XW#6k(C|^E7Vz>k&yzsPk-ocfp{8
zWe3r)PvT;1-wo;gemiO!WHwR~y;CcCP*u|GQOTB{Bqw6npD-fh?`~kh#Fzz|Nl}Zr
zyIYRWO!cAotoO{J=N*ILSK96@IK?`Zj|)vV$ZJmv#0OTrk6x7cUct+1vlC1PD{`|+
z1L3jtev@)qLQi7px_`KHD-`x~7tKla%?$`gM}oLWs=#co;%v5$;VH7>yBN>B-{}-?5Wf53-Mc0Ix4I-lzMaOOoxx@2~K0|D(oH*
z^X1jGer#L38@B@PT;_9Jn2G3KvCw&@)xd+uDWw{*a4>o8{Df6gYmSfeNMK`GnT(Bl
zialk5dsbC;ln$qTtA@XeuIe?>eLYA8B!y^jTGndtT`^>_DmY7Bun-z(XK1{~bDCN5
zAg9su_Xj@+MV@(jEl~8h+pD%sdcFfiOG8Ck#w5J{F=j6Bt
zPQ=nm%s&mx{28`97bdZZA026!v<(zEMr0~&W_d^L7KqoiZ90OVY}L;^!I)31L$;N+
z$2j#3)j2q*1MMX9fBq%y_;q(pW$`(i(*Y@dpM7QfSpKRS9%K}nEB|Vf>YzCecT+|G
z*6`8q5>=_2~)IS(Xu5EzZae-Xgu2
zs5UzN_bgny$gB+4C32P;d%vkzAg`UXWD}!}4y~iFsQYH^T3;k~tLBDuKmVO(LrKc;
zpvtXcZFdJ_NXSnO$RBpX2%GGRrmUk$XR)X|6?ZBYry9OD5ZY6$R!~1Iab7G+Z6tc!21U}3-
zbkA!=_xPkKYhDfZQ8zj!DLrwLu^Nwu?9}o?&2rKi_U2u>c4m@+HkD)bZAG8B>dbUW
zQro`iW}oU0{T9KOLC>me64fbY@Vf0U@$HG(>+C*eatD4Xn>|XRPi1R#>P{e4+@*{2
z=#*!zSId~{7aX9V&1|aNR+!~yU%$~Nxk{}!S5d@i@R+H@Wb{P*y}PgcM`ZMGBz_Rg
zu*%BHN~|_krS;y;7$4RkFQ^~Gno&S?y+Y?)igrbfIBlP!f>Sa}e{$$v^$KB|+ebP@
zJT-q+s-DwcvX{bsV({
zVrY`P27
z`6@N6Levu2o_o?vhNLEBebVrM!B7?JB%ZHSP{>!;#gL|_!#N`AU;8bKN^L^Du43`rJXa<=0A+SF6S3rhnxmJQCGAeUvd{@LmX6Ft2Lr
z$ElM;(q?OdH%8i%M$pt$Jve24ORY(U`ejHa$E2*^wa{x})Dri3K4jZ-KJe%ArLIh`
z$To^odt&Up#nDROxt^&eeOvmG!?Zok3A7c{9*z6k6-t~ZsVmYm5WeSVj>zb)KXZ`1
z@<^~1cUg+h45Q=|j`q-N{uDQ>sRBQ$$S?N38vGX7+1MZL&SB+$Sz+V-^oHXc8Qwc4
zwlYOUKDP+dGtE2Az@2Hh)TM4b>FgRfB1w8&@&$**+2-<>mudB~PmP@4NRpm@m^)Cl
z^Q6@CUh1qVS+&H-t>+lx^ei|sES^$%WhxHr>VGd5c%_mfvm@llI&W3E=1{&DLwe=L
z`m>1vKcb|>mZP&yA8fwHy={TY;?jQkk(}Pw4Q*LVL-PKr-(IVJTqmH~>8_#^I8!xm
zrK@m4@^;;`UJ5TV4Z{;0m7gXA9$T8Ki*8N-CM3x%XPxI~lfo!*pShVf`b*_BedA93
zwQ8Y0{RW1@(*;r!w^G>4#mgU;71^!>HU1?ZTSGxsK
zEGp0{=%*B{wH6h@3KC?7(u$NaiO86MB4Y^1YzTuRw4g$(1d$;iRgo!72{NM=rG$A1
zkbqh-fP{cdLBjOCJEHfy&-Lm3aj!r45zjd}!_MCCS!=y(Ewzpv9aS{lZY}-bLKEx0
zJOh7kS=H6K+SF0&M6$9;%5Ucr+bHz?1Uq+&%`(#^#o;Qs(m7(EH@gL!1YbEu-pN_K
zEvHDVeO8b(m^7FkY2v+)U{IjjH0CJ2rUUc3qIam{=$X$IXOjkR^S>(bdh_r;xkG{D
zbd!Il;%Dt$-!0wkvKmzjzMVm~QIxp4y{>WY8xlv;wIBfsL
z&1Exk7shYP=CRJ>P!`vQty#FGt-o_etPrnwYg6&DX{kHhN0UDqa@4;w{Lc(-9I4hsd5dwtbEOq
zaW~Gsgd#<9EF(@dw$sgZ_;No>x|M1v-ez784%95#bA(o9^)vI${YTz?7fcBE#&b%_
z@YeC(o`XIy9rNaU9i4fWIDOTIKcXu
z_7hDb=Vot@mb+VwNLE({B9$y_CAMB<^gYVCC$ch#tE+`a!d3s^LoVhIEHAJdfISD
zrj4;&^x7i&bvMRfZH3_;Chj1zJrWuZ2>%GxE5biQg^TcyP-ye<&p&Vb-*@=bw(k#4
zBYWfVaZjHfB~{Apjeo+JZ|jWo`v9p5!8um1ceeFo7T8GcfYqi}GiRUsyuYDn*Vz!
zolnYLMT>>ddE3*IMroUwV1e8|9r^CbPE1!%k9INE^G(NHivgI3D-$WWzRt+dPn|O`
ze+nb)vWcZ_xO16V>?;6ZMR@>wPGwl^9QUfN{2#!gSJ^lP-hKRs!QJ!@5OO_VjIROb
zs`*JEdV|i+zwy$YUCCGlvJplLATR5dcQ$>?ir+yD2BUWv0l`_u@#7`npQ+7Cvpew&
zSm{X4{hcaM(7#-X{qT*e2y@nh%$7}fz;rq(qg-xOAf&&_(*aZa5rDYi^A#0Z#*w;z
zg|VP>9lHQT`<^!|Mw}2=i+&iG)~Q
zr>)Eu07JvV0nd+5x)N+>7@8quXg)k~xj%3rApiO_Ec-zf_K`UI2MG7WwnAF$;|`xX
zt`JcE-`TT&#GU`?MB4Ht3pXOlHA7BwB;(R`la$+c)&I`l@9YeLan&HijhY3oY3b53;g`l;a+t2efLE;^$ZRWp!4PkO
zjsLKZn~Rcubq!dAF0e=+J|ntRg2ZEi|EAO9C>A^5N%{imttyUWt4sUzI0c&3g1JI#
zLlXa6A+hRjiC5??0HkUeqA)l23cpf&Ep6xm4@5C?-<^F~$6bdJa^T{I`EclE0e3yb
zCcM-FVN7~Xi;75w_BtAfON6*&EOfC`!*CPNtK(1{T0LA~*=P|ny$3j)SAa?8>KvqM
zfb``;%$ETTG(;5VEe^BC{L%3-d(F(u;u@t7Cb6lFJT5?pWqI)#TO}O8!6U>UI9pjD
zy8}2y(EcE!n0oeme|TMo?*hi$CWSz^_XjMo`s=nts$(EXS2leKG1Kb66zVS0KJ($!
z^imh!?&R>e`GZ5Ut=Lvl`6xdJ!@t`JN;Ef6df=PJ^
zpXN0z{UmmR4#xHAreRBTg%wQbR&uuXr9Fv}rs^Wn!1cPOyPfeRHp?lC{5BZoAz37g
zDS~M9M%Vds9VUvhD3N`#C_cicd$1iixL51--x+ci9IVBgSrGW=Z!lkJ;Y|1GyG)bt
zA*?G^DtP!c)kbG!ae9LoJoNM9r$B65A0IiBtc0M(0IxCc?X?I1EMl*50*;(fNm!s{WE6d{&7qIvC-c2AgZ7u(CmDKXK%q>X+F6)M6?1P-%zHG$g!2
z8I+58{9CIkEU#lON>Ou7B7D@)wO=0(DyI69R=rC4aEu`R#1Eiz&QY3kj#{!#fBvoR|a(B;9gXJUr)IL?v>&zCz()AJyTzW|$i~F(m
zIM{)b-~x?_$8$*_{7@3}fdQJWtWV{s)H;Gd2Z8*P&3=(3#csd8f>cU%0c0AnR{*{r
zZ(GRT^Gl-Q%qsxr!|Mlj;-Pd1t(i{aNqM6uCtU+90B)}sdj>G)>K45d=5mE+JPc0O0b>Q#Gsh;tgi9(_KdJ_VJ>#bAjgMJ)0b+svb_wL;D~MU)@)8ksyzWMS+v8Ko!LX6Q6LQ
zCYZB%LD4ph{ClJG$XmR^**ejbMEMpsX`QzQG0uaIF9atou$jk80=R?JIH}Q+fGy0C
zgv1Cghkv<{?{Mxl{N&^lz8HWBWUg4-lWGXF5rnwe)*^s0bUIno&Jk2S)TIVvz2nx=
zakq#3)(qHd?f6Nxgg+iyTe%Do0r@Ba*jsx?uO6@i9+(juHM|6b=yVj7g;&B`#?S$~
z!i*On?_=K2Qo}2z1s%7JH}z6i?@KbX8gD%sg)OyR-m1}e<_5=Y=>Rm-{r!UX#d|SZ
zW6i8{$1}PHsL38*5sKOnjC`=DbtL1e-cVYY#y%&dpVluJb1*L86Nc>&Pdr7y7T8x3
zU@$-Q1a+Q1*k?LmjSK7FE^bH@2!E;RK%-D#QYqhfW_r$^k>czzG!9M(E!U*>$J@N{P!7G~
z<7Y|gjw)Vy)J&8?b4`IXUS7g8|8kWWcp`@k++M?m-(gD1`PU)Sxe9V1wGh@Phy;mK
zoyiXihgfKn&mDPkuGD?m!QVa9j9&u_cU!PIi0x#dn8UTVpJ#SJmpA{QzEc#mzRnSp
z3)K%FmVww`Q#3*6JNRnC>h$V&Q!zctFnBI)7^pR|%7vlEw~`hoGy*`9E5>O$NG_1^69Zr#UNgO*8>s{k@>7zs{>P>*V
zd99nY9vpxM(IQ-^;+HxA7Tg9Fw)kyONh}vbb3kRJpp#PL2Lmnwk-&zM!Y66!;s|b$
zSP*OLPU%h%Ehbb8gU@kdGQ?3mMU8N&Bth?uyp+#Hp{gqHejVti&dz~u)c=R=y`znF
zOw;!&tnn?qWV<+0;G)F)XIWPwt=qcV73!QcnRHDulRky}D-VPDWiR!U6B4HPiQG3NR1=6B2
z1;lf7TjBn4*}1u(%Gr(9`PKG>k9Flg)qkto3itZB!~dZWZM)IcyG|rX1L~S2ivQE?
zehXk0w@9Wfr6Y_lJ{1u3T98i?Yjr=Xi>_;e^|3t=1)?nS!=DJXTSD!fAaL&1Ay?d&
zz>+Vqbcmp-Hl11wr(oBkGvl^mp-?hI<b{#mHb6gV
zgKeJpeP^h+l_L@MYb4M~WA7Ks1OUTrXBFX6A1hmb(vi^ZDe;Z496e>nIQ|UeRAFAz
z>lMvY?fh0h|84Ym1Njtz)AQk=6?ho>jP;xTm5^L|S}3ln_%2sC%(2ilJmkUQQ_#J<
z8D0%Nj%I)L5c{8tx?Iv-0dZiEt79Vj6bD1^Kbp5FnC0+&%9~ZnG&z_oXser7M^{^@
zz;pEVNMb+dy-U|_1+;lX>ZpbExQL$V%YW(#>z1P9h0;OvX^MRshIAgxVBm|SV^NkLQ@S9tRYtta(~PzS#Mw3Rh0
z{O!
zWTq6QB0N-dA1B0C?*Wy1um!Z9vr|S>74Tk|Yd_Dyu5MDe!{ekryu6skf|~rTdc|#Rot2n3x6~^;A!=w{FQ9D1^sg5O0MRn=9i=
zWrL0RD`2e<3zN9+uH1h?SdZ2^8j>NtfiYIYuSUBYi2XD|!PM%Iu}n_5!57DmVvoQ;uPNX8*T0*-Ih9M$Xb!
z>w10P#X~9=l+}F7qm>__I%+SZjg~&$c1z8}9KCK;905l5cH@MfLYJO{uPv)yWabBT
zz#|6!6y;!O{n00P0s`gd-WZD%Gmxf)KLogeR2^lE(Lzm23!&
zSSy@GeRBh}^ZK8X*}nuZu*P(iGLJ@Hc|eM_uUaFI^;iyv+zkF7{}oQYTQQz^E2uj2
T65`lJL`;4(|DoV}my7=fc60_^
literal 0
HcmV?d00001
diff --git a/Declare4Py/Utils/bpmnconstraints/tutorial/data/Sepsis Cases.xml b/Declare4Py/Utils/bpmnconstraints/tutorial/data/Sepsis Cases.xml
new file mode 100644
index 00000000..52a5652d
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/tutorial/data/Sepsis Cases.xml
@@ -0,0 +1,2354 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-C7A03837-87D1-4615-B245-9FCF9560D74E
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-C7A03837-87D1-4615-B245-9FCF9560D74E
+ sid-9C2F3034-BC18-43E3-8722-5DF161551791
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-95261D07-3239-411D-B667-7273F1F8F960
+ sid-A5FB31FB-F215-43D0-9D0D-100633C8EC9B
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-04B70A2A-FFC5-4F77-9614-02268F6BFF7C
+ sid-2FE2A4A5-9480-4369-AEBD-D298012BCE89
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-46B5DFDD-3089-4B94-AF06-7ADE96BFB62D
+ sid-B4324C2D-4A0E-4DF5-9990-2007A29650B4
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-84C64016-7C0C-4E0A-B704-2FD141934206
+ sid-6E1359BF-970D-4707-BE78-C4C1E08A9311
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-A5FB31FB-F215-43D0-9D0D-100633C8EC9B
+ sid-30065BD3-2208-4D27-ADB6-E32BEB9CEC32
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-D7D5E586-7F4C-4F35-BA1D-BA6C3A46BCE1
+ sid-2DADEC08-ACAB-4789-A8BD-3B3907AE1646
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-673A899B-DDF7-42DC-A04A-16A7AAAB9EFA
+ sid-B0448896-4932-419F-91EC-8829FACEA9BE
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-26BA9710-56FA-4E20-AC97-E4B3D35BEC37
+ sid-81A30C51-F021-4FDF-802D-9DD4ED51BF7D
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-45128663-CB2C-4BE8-BD6A-AB70673A02C5
+ sid-3CA86796-3E6A-4291-B3A6-2E9C269A0BAE
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-6B167E29-6E3C-43D9-BB64-739CA339D765
+ sid-9BE66A87-9697-4A56-994F-00B349892CF6
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-8B528875-BAE6-4D06-94A3-6458D5536049
+ sid-3741208D-EFE5-482E-AAD0-517FA35C132D
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-F80ADAA7-450F-4997-8A5C-D865CB2D2FD2
+ sid-8104CE26-6EC7-4DAE-B935-77DC23AFEF0A
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-AA98DE0A-52D1-42DD-B58A-65C3500AA611
+ sid-6BE88D76-A5F6-4633-B1C6-4C881A7FEDF0
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-484E2997-041C-44CE-8B28-3B7E2CD0F65D
+ sid-59665398-3AC0-452B-B271-9F0CCDDCAEA9
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-C2118417-2B89-4FFA-B0D6-CD005F59CBD3
+ sid-03D94D1C-6322-41A1-B096-3427CF43C34A
+
+
+
+
+
+
+
+
+
+
+
+ sid-9C2F3034-BC18-43E3-8722-5DF161551791
+ sid-46B5DFDD-3089-4B94-AF06-7ADE96BFB62D
+ sid-84C64016-7C0C-4E0A-B704-2FD141934206
+ sid-95261D07-3239-411D-B667-7273F1F8F960
+ sid-04B70A2A-FFC5-4F77-9614-02268F6BFF7C
+
+
+
+
+
+
+
+
+
+
+
+ sid-30065BD3-2208-4D27-ADB6-E32BEB9CEC32
+ sid-D7D5E586-7F4C-4F35-BA1D-BA6C3A46BCE1
+ sid-673A899B-DDF7-42DC-A04A-16A7AAAB9EFA
+
+
+
+
+
+
+
+
+
+
+
+ sid-2DADEC08-ACAB-4789-A8BD-3B3907AE1646
+ sid-B0448896-4932-419F-91EC-8829FACEA9BE
+ sid-6341B142-3E5F-4FF1-878C-98027293AFDA
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-6341B142-3E5F-4FF1-878C-98027293AFDA
+ sid-26BA9710-56FA-4E20-AC97-E4B3D35BEC37
+ sid-45128663-CB2C-4BE8-BD6A-AB70673A02C5
+
+
+
+
+
+
+
+
+
+
+
+ sid-B4324C2D-4A0E-4DF5-9990-2007A29650B4
+ sid-6E1359BF-970D-4707-BE78-C4C1E08A9311
+ sid-2FE2A4A5-9480-4369-AEBD-D298012BCE89
+ sid-5EDF3A07-F093-4B64-93B2-DD90A77C1A62
+ sid-F763C894-ABF1-496E-9681-72B185F435CD
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-F763C894-ABF1-496E-9681-72B185F435CD
+ sid-6B167E29-6E3C-43D9-BB64-739CA339D765
+ sid-8B528875-BAE6-4D06-94A3-6458D5536049
+ sid-AA98DE0A-52D1-42DD-B58A-65C3500AA611
+ sid-C2118417-2B89-4FFA-B0D6-CD005F59CBD3
+ sid-F80ADAA7-450F-4997-8A5C-D865CB2D2FD2
+ sid-484E2997-041C-44CE-8B28-3B7E2CD0F65D
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-3741208D-EFE5-482E-AAD0-517FA35C132D
+ sid-6BE88D76-A5F6-4633-B1C6-4C881A7FEDF0
+ sid-59665398-3AC0-452B-B271-9F0CCDDCAEA9
+ sid-9BE66A87-9697-4A56-994F-00B349892CF6
+ sid-03D94D1C-6322-41A1-B096-3427CF43C34A
+ sid-8104CE26-6EC7-4DAE-B935-77DC23AFEF0A
+ sid-98654991-8552-4B38-838C-B0D8BB99E48C
+
+
+
+
+
+
+
+
+
+
+
+ sid-98654991-8552-4B38-838C-B0D8BB99E48C
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-3CA86796-3E6A-4291-B3A6-2E9C269A0BAE
+ sid-81A30C51-F021-4FDF-802D-9DD4ED51BF7D
+ sid-5EDF3A07-F093-4B64-93B2-DD90A77C1A62
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Declare4Py/Utils/bpmnconstraints/tutorial/data/linear_diagram.png b/Declare4Py/Utils/bpmnconstraints/tutorial/data/linear_diagram.png
new file mode 100644
index 0000000000000000000000000000000000000000..7e4a29eda1d03d8b0d82c9a96f8a44aea61fe6fb
GIT binary patch
literal 8032
zcmd6MWmr_*-!2GB4XA{qAT1zW($YCJD$UT1(v1QRASDjz5E2qf51kJ=NDL`ROAQSI
zLk#(Dp7(#^!})Z+oO8`Jd(ED;SL|P}`;O7oRwX5-BgVnOAyrpX(#OHMqXqm9C%gw-
zYiQH>faZyfnm!l@Cy)aN=UpTY&N=YcyA2#19|0VkEh`)x$#fhX>NlB9deT4#zJoki
z9tWo?A^1WM2HfL%>8mQ>l%p6nft!2QnyN}TH@Ba!twp!pL~qoLy>M{Ix^KU@DLiEK
zI5>>;>Pqs4{xiE-ME-`quAn-P2&1DPnCd>Fev_7GoutgoU0(bo@6Im!$!mo+Ud
z(kbSmPQShz{gl1fIm*Af*!xJu)9bd-g0*o{Q&SxKB*JE!?#wJ~KiF`-S(Fp{2Qe(`
zBILcHJ6@#2G+u5lHC_m&x6>9iZVzq!IW#0XJw1*7$(i%aX|Ca*TGV9{RK;JG3XK$D
zBUM*afR^}T(4U2cg%Q1Rw8DQ=iWr9Yib(wc1JHSTMIjlvDq9oR~8pLzIgJ$
zA52Gny8%+7G)lYoa_TxdIfA}Bzj3|LgMw*ho-yiRuu)<6gTs2&L`L+4fsUJ1(D;>W
zPwkv+tH%ErNz0L=aCVU(wbyX`EzLs6yxG?X+Winp6L`G!>&-c4GsJb@y)eW%R)np9
z*-4F#Tu4hcA||DN-gkC3g5bWpTB0^vVKp}|?|j{xrA}7Y09)WSZs%5e`RI(~Wp406
z4>dTQ=LtD-w|+5up;#{;w$q+fz|2faSru{W0F%kFR)ry1yv5cpa2`
zyBP2Uu(zsU?BU6?X{s29jgj1-S-B$3|DJy2GeJ((+m&9GChw$tc3*+3ligiVBLJvaAmX(~~KAEiiaXo@z9Fg*T*2Df8hfqt
zukQuQv5%CUoSd*jaPb@%40iNJUcN(;DhF^EJr^gp@c^+b8v`ErNqtE?c-!q9RTwYU
z>O5`+Kiq1CRI8MXuKt8^`s^>r*sS%ZkfLNx&AjG)rZOVPB>P_H+s@QD*-Tbg<}?9<
zD|DGEca!v3Xn~jIHvMe7c7s5cegP8mQ1b#jQ>ko;60R~kfry)$jf4@=f9De8t#L{Q
zlWcv1e39@%*A`{@&P4ibPl`63E(8sIptf+-*Vn%eLm7`NNiIcF48Fs~(|YniEgP`#
z4!^m#$QCFmeW*L>FXa=rAK&Bw_wTH)sduUdI~Xk?(tr552F@35laHb~y9Mq>bQEwI
z6l%4f%(xKTV28uRPAZ&6zIHH%F&g*))&wWvYj`3mEPT|E#Ht!nbSxhb
z(UMdkCnx9dGhSXdv}{sps=cSIciE|{t0x*GRzb|)3Jbps@HG#{G0MycswerYrtr02dLpIc=|uabv8%Ac
zf`Z6;k@`(hczMm{PyegvhKkRu)tElkL~rAUH;~%F&(sMB@6EAZ@E4H)LTVm2Vn9r7
zU&ZaYXh4$oC4gt5^Alx-42rblom2BVF8t+kR*oQqXIk+NaHdyX$tfv5yXk^9_lDC2
zyBIwCm_-9!6VkG><_iFA^Up**F3XEyEayc}MZVf{r!_dT}iT{Sd|Id5-y}3s8
zRQt70Em_~X1R0WKJbXU}nHV$6PzaczTqYbo8%?xOW!oM7@FIapuFXqc9(Ul;O55cK
zUDx_<4yhP#-R4z6K|y?z{l5;VH;hrF53aKj(Ki^<)|pS9~u=YTagi*8!a-*4@wfSU*BcLW10xYZSg3QM@lR
zCo6rk*Sx=HZD0T=R!L;M8enATY&&*0uabSQ9>Y;%sn$9%!ry+mTmTryRNq19*%HAP
z-gqTM(Mj$2)87)P^9#AZrC?MfD~CJG`SaE3;-c&C%8ua61LU5;uFX6e$=-=sj^#fw
zuXQ%UOC{@#(Bx|@Fji4fQ8oRu!$LPTFV6(XD&JM;Vh5q~Q(`?6b{ZvjncH|ZaJKcW
zF88(F4d0<+q6aEdf04}@Lr%zKjr;seX5dzdpu{!RD>I0D^RC!xO@48Ej
zuwJ$bx*V-or^}xGiEsh30fmo2|7+!pCcpi*>v_LLnZ-z7!gwjUD~!Q+H&-$?Y}J_L
zay08;=*8}o#;iRc*4y#1$MGfqXne(UP8@tV{KIAr;xVvcT(6=&hyauZmk2y0yA
z+F3KBAIH#hBp#DW23o>rLFqhiRdg6G!KTZ2x;g72f4fLscB-PjO#
z>^xrMWZ-~29vjmSq(uW(B`SAwiI4yknx)||^hFdEMEeqQr0ZA9y66VxZmx&#w_TuO
z9whfnS%$g!?#*pR8c_3^*oGeeu#{MzD^RBp4mtN0e)H!abNY-&l$12439kBEaYhby
zb{R%LUP_E|!=su*74uc%eJ{vlkM_fEW&^V3mtv$3q+-0Qxacl|td_SOdyMSz4=cj1
z24bZ3C(|qfOOB+GaJjHHgO|_t9}C$=8@zlWA$vOKrLA-E+a^&oD
zmzQ?}-_6D1jbxIcx6P4LeTsxdtLt=ikAx1Cq_J*<