diff --git a/.gitignore b/.gitignore
index a840c1c0..baf2d789 100644
--- a/.gitignore
+++ b/.gitignore
@@ -138,3 +138,5 @@ dmypy.json
*.lp
*.asp
+# vsc files
+.vscode
diff --git a/Declare4Py/ProcessModels/BpmnConstraintsModel.py b/Declare4Py/ProcessModels/BpmnConstraintsModel.py
new file mode 100644
index 00000000..55151785
--- /dev/null
+++ b/Declare4Py/ProcessModels/BpmnConstraintsModel.py
@@ -0,0 +1,103 @@
+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):
+ """
+
+ Uses a path to a xml file to parse and create a DeclareModel and a LTLModel for Declare4Py
+
+ arguments:
+ modelpath - The path to the xml file, as a string
+ 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..1da5bc27 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:
+ """
+ Parses a xml file generated from a bpmn diagram.
+ args:
+ diagram_lines: A list of declare constraints generated from a bpmn diagram
+
+ Returns:
+ DeclareModel
+ """
+ all_activities = set()
+ constraints = {}
+
+ # 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) # Extract the activities for the current constraint
+ all_activities.add(action) # Extract the activity for the entire model
+ 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:
+ # bpmn2constraints don't use conditions
+ 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..14fc53a8 100644
--- a/Declare4Py/ProcessModels/LTLModel.py
+++ b/Declare4Py/ProcessModels/LTLModel.py
@@ -153,7 +153,30 @@ def check_satisfiability(self, minimize_automaton: bool = True) -> bool:
return True
else:
return False
+
+ def parse_from_diagram(self, line: str, activites):
+ """
+ Parses a xml file generated from a bpmn diagram.
+ args:
+ line - A string containing the LTLf formula to parse
+ activities - A list of activities generated from the DeclareModel
+
+ Returns:
+ Void
+ """
+ for word in activites:
+ """ TODO: While this works currently, som modifications should be made to either parse_from_string or
+ the analyzer to make it applicable to all event logs """
+ 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..b77d6c03
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/README.md
@@ -0,0 +1,13 @@
+# BPMN2Constraints
+
+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).
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..8c797624
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/requirements.txt
@@ -0,0 +1,2 @@
+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..e27733fd
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/tutorial/bpmn2constraints.ipynb
@@ -0,0 +1,1078 @@
+{
+ "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": 2,
+ "id": "initial_id",
+ "metadata": {
+ "ExecuteTime": {
+ "end_time": "2023-11-29T13:02:59.781359787Z",
+ "start_time": "2023-11-29T13:02:58.421541843Z"
+ },
+ "collapsed": true
+ },
+ "outputs": [],
+ "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": 3,
+ "id": "68aaff03d9d70600",
+ "metadata": {
+ "ExecuteTime": {
+ "end_time": "2023-11-29T13:02:59.918794770Z",
+ "start_time": "2023-11-29T13:02:59.781210072Z"
+ },
+ "collapsed": false
+ },
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "Model activities:\n",
+ "-----------------\n",
+ "0 check invoice\n",
+ "1 register invoice\n",
+ "2 accept invoice\n",
+ "\n",
+ "\n",
+ "Model constraints:\n",
+ "-----------------\n",
+ "0 Init[register invoice] | |\n",
+ "1 Succession[register invoice, check invoice] | |\n",
+ "2 Co-Existence[check invoice, register invoice] | |\n",
+ "3 Choice[check invoice, register invoice] | |\n",
+ "4 Alternate Succession[register invoice, check invoice] | |\n",
+ "5 Succession[check invoice, accept invoice] | |\n",
+ "6 Co-Existence[accept invoice, check invoice] | |\n",
+ "7 Choice[accept invoice, check invoice] | |\n",
+ "8 Alternate Succession[check invoice, accept invoice] | |\n",
+ "9 End[accept invoice] | |\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": 4,
+ "id": "9c65a09f",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "con_registerinvoice\n",
+ "con_registerinvoice\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(G((con_registerinvoice) -> (F(con_checkinvoice)))) & ((F(con_checkinvoice)) | ((~(con_registerinvoice)) & (con_checkinvoice)) | (G(~(con_registerinvoice))))\n",
+ "(and (always (implies con_registerinvoice (eventually con_checkinvoice))) (or (eventually con_checkinvoice) (and (not con_registerinvoice) con_checkinvoice) (always (not con_registerinvoice))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_registerinvoice)) & (F(con_checkinvoice))\n",
+ "(and (eventually con_registerinvoice) (eventually con_checkinvoice))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_registerinvoice)) | (F(con_checkinvoice))\n",
+ "(or (eventually con_registerinvoice) (eventually con_checkinvoice))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(G((con_registerinvoice) -> (X[!]((F(con_checkinvoice)) | ((~(con_registerinvoice)) & (con_checkinvoice)))))) & (G((con_checkinvoice) -> ((X[!](~(con_checkinvoice))) & ((F(con_registerinvoice)) | ((~(con_checkinvoice)) & (con_registerinvoice))))))\n",
+ "(and (always (implies con_registerinvoice (next (or (eventually con_checkinvoice) (and (not con_registerinvoice) con_checkinvoice))))) (always (implies con_checkinvoice (and (next (not con_checkinvoice)) (or (eventually con_registerinvoice) (and (not con_checkinvoice) con_registerinvoice))))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(G((con_checkinvoice) -> (F(con_acceptinvoice)))) & ((F(con_acceptinvoice)) | ((~(con_checkinvoice)) & (con_acceptinvoice)) | (G(~(con_checkinvoice))))\n",
+ "(and (always (implies con_checkinvoice (eventually con_acceptinvoice))) (or (eventually con_acceptinvoice) (and (not con_checkinvoice) con_acceptinvoice) (always (not con_checkinvoice))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_checkinvoice)) & (F(con_acceptinvoice))\n",
+ "(and (eventually con_checkinvoice) (eventually con_acceptinvoice))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(F(con_checkinvoice)) | (F(con_acceptinvoice))\n",
+ "(or (eventually con_checkinvoice) (eventually con_acceptinvoice))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "(G((con_checkinvoice) -> (X[!]((F(con_acceptinvoice)) | ((~(con_checkinvoice)) & (con_acceptinvoice)))))) & (G((con_acceptinvoice) -> ((X[!](~(con_acceptinvoice))) & ((F(con_checkinvoice)) | ((~(con_acceptinvoice)) & (con_checkinvoice))))))\n",
+ "(and (always (implies con_checkinvoice (next (or (eventually con_acceptinvoice) (and (not con_checkinvoice) con_acceptinvoice))))) (always (implies con_acceptinvoice (and (next (not con_acceptinvoice)) (or (eventually con_checkinvoice) (and (not con_acceptinvoice) con_checkinvoice))))))\n",
+ "Is satisfiable? True\n",
+ "\n",
+ "F((con_acceptinvoice) & (X[!](false)))\n",
+ "(eventually (and con_acceptinvoice (next false)))\n",
+ "Is satisfiable? False\n",
+ "\n"
+ ]
+ }
+ ],
+ "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": 5,
+ "id": "b4f22f5abf341228",
+ "metadata": {
+ "ExecuteTime": {
+ "end_time": "2023-11-29T13:03:04.894479074Z",
+ "start_time": "2023-11-29T13:03:00.056992740Z"
+ },
+ "collapsed": false
+ },
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "Model activities:\n",
+ "-----------------\n",
+ "0 CRP\n",
+ "1 IV Antibiotics\n",
+ "2 ER Registration\n",
+ "3 Admission IC\n",
+ "4 Release A\n",
+ "5 ER Sepsis Triage\n",
+ "6 Return ER\n",
+ "7 Admission NC\n",
+ "8 Release D\n",
+ "9 Leucocytes\n",
+ "10 Lactic Acid\n",
+ "11 Release C\n",
+ "12 ER Triage\n",
+ "13 Release B\n",
+ "14 IV Liquid\n",
+ "15 Release E\n",
+ "\n",
+ "\n",
+ "Model constraints:\n",
+ "-----------------\n",
+ "0 Init[ER Registration] | |\n",
+ "1 Succession[ER Triage, ER Sepsis Triage] | |\n",
+ "2 Co-Existence[ER Sepsis Triage, ER Triage] | |\n",
+ "3 Alternate Succession[ER Triage, ER Sepsis Triage] | |\n",
+ "4 End[Release A] | |\n",
+ "5 End[Release B] | |\n",
+ "6 End[Release C] | |\n",
+ "7 End[Release D] | |\n",
+ "8 End[Release E] | |\n",
+ "9 End[Return ER] | |\n",
+ "10 Co-Existence[CRP, Leucocytes] | |\n",
+ "11 Co-Existence[ER Triage, Leucocytes] | |\n",
+ "12 Co-Existence[Lactic Acid, Leucocytes] | |\n",
+ "13 Co-Existence[ER Triage, CRP] | |\n",
+ "14 Co-Existence[Lactic Acid, CRP] | |\n",
+ "15 Co-Existence[Lactic Acid, ER Triage] | |\n",
+ "16 Precedence[ER Registration, Leucocytes] | |\n",
+ "17 Alternate Precedence[ER Registration, Leucocytes] | |\n",
+ "18 Precedence[ER Registration, CRP] | |\n",
+ "19 Alternate Precedence[ER Registration, CRP] | |\n",
+ "20 Precedence[ER Registration, ER Triage] | |\n",
+ "21 Alternate Precedence[ER Registration, ER Triage] | |\n",
+ "22 Precedence[ER Registration, Lactic Acid] | |\n",
+ "23 Alternate Precedence[ER Registration, Lactic Acid] | |\n",
+ "24 Co-Existence[IV Liquid, IV Antibiotics] | |\n",
+ "25 Precedence[ER Sepsis Triage, IV Antibiotics] | |\n",
+ "26 Alternate Precedence[ER Sepsis Triage, IV Antibiotics] | |\n",
+ "27 Precedence[ER Sepsis Triage, IV Liquid] | |\n",
+ "28 Alternate Precedence[ER Sepsis Triage, IV Liquid] | |\n",
+ "29 Response[IV Antibiotics, Admission NC] | |\n",
+ "30 Alternate Response[IV Antibiotics, Admission NC] | |\n",
+ "31 Response[IV Antibiotics, Admission IC] | |\n",
+ "32 Alternate Response[IV Antibiotics, Admission IC] | |\n",
+ "33 Response[IV Liquid, Admission NC] | |\n",
+ "34 Alternate Response[IV Liquid, Admission NC] | |\n",
+ "35 Response[IV Liquid, Admission IC] | |\n",
+ "36 Alternate Response[IV Liquid, Admission IC] | |\n",
+ "37 Exclusive Choice[Admission IC, Admission NC] | |\n",
+ "38 Choice[Admission IC, Admission NC] | |\n",
+ "39 Response[Lactic Acid, Release A] | |\n",
+ "40 Alternate Response[Lactic Acid, Release A] | |\n",
+ "41 Response[Lactic Acid, Release B] | |\n",
+ "42 Alternate Response[Lactic Acid, Release B] | |\n",
+ "43 Response[Lactic Acid, Release D] | |\n",
+ "44 Alternate Response[Lactic Acid, Release D] | |\n",
+ "45 Response[Lactic Acid, Return ER] | |\n",
+ "46 Alternate Response[Lactic Acid, Return ER] | |\n",
+ "47 Response[Lactic Acid, Release C] | |\n",
+ "48 Alternate Response[Lactic Acid, Release C] | |\n",
+ "49 Response[Lactic Acid, Release E] | |\n",
+ "50 Alternate Response[Lactic Acid, Release E] | |\n",
+ "51 Response[Leucocytes, Release A] | |\n",
+ "52 Alternate Response[Leucocytes, Release A] | |\n",
+ "53 Response[Leucocytes, Release B] | |\n",
+ "54 Alternate Response[Leucocytes, Release B] | |\n",
+ "55 Response[Leucocytes, Release D] | |\n",
+ "56 Alternate Response[Leucocytes, Release D] | |\n",
+ "57 Response[Leucocytes, Return ER] | |\n",
+ "58 Alternate Response[Leucocytes, Return ER] | |\n",
+ "59 Response[Leucocytes, Release C] | |\n",
+ "60 Alternate Response[Leucocytes, Release C] | |\n",
+ "61 Response[Leucocytes, Release E] | |\n",
+ "62 Alternate Response[Leucocytes, Release E] | |\n",
+ "63 Response[CRP, Release A] | |\n",
+ "64 Alternate Response[CRP, Release A] | |\n",
+ "65 Response[CRP, Release B] | |\n",
+ "66 Alternate Response[CRP, Release B] | |\n",
+ "67 Response[CRP, Release D] | |\n",
+ "68 Alternate Response[CRP, Release D] | |\n",
+ "69 Response[CRP, Return ER] | |\n",
+ "70 Alternate Response[CRP, Return ER] | |\n",
+ "71 Response[CRP, Release C] | |\n",
+ "72 Alternate Response[CRP, Release C] | |\n",
+ "73 Response[CRP, Release E] | |\n",
+ "74 Alternate Response[CRP, Release E] | |\n",
+ "75 Exclusive Choice[Release B, Release A] | |\n",
+ "76 Choice[Release B, Release A] | |\n",
+ "77 Exclusive Choice[Release D, Release A] | |\n",
+ "78 Choice[Release D, Release A] | |\n",
+ "79 Exclusive Choice[Return ER, Release A] | |\n",
+ "80 Choice[Return ER, Release A] | |\n",
+ "81 Exclusive Choice[Release C, Release A] | |\n",
+ "82 Choice[Release C, Release A] | |\n",
+ "83 Exclusive Choice[Release E, Release A] | |\n",
+ "84 Choice[Release E, Release A] | |\n",
+ "85 Exclusive Choice[Release D, Release B] | |\n",
+ "86 Choice[Release D, Release B] | |\n",
+ "87 Exclusive Choice[Return ER, Release B] | |\n",
+ "88 Choice[Return ER, Release B] | |\n",
+ "89 Exclusive Choice[Release C, Release B] | |\n",
+ "90 Choice[Release C, Release B] | |\n",
+ "91 Exclusive Choice[Release E, Release B] | |\n",
+ "92 Choice[Release E, Release B] | |\n",
+ "93 Exclusive Choice[Return ER, Release D] | |\n",
+ "94 Choice[Return ER, Release D] | |\n",
+ "95 Exclusive Choice[Release C, Release D] | |\n",
+ "96 Choice[Release C, Release D] | |\n",
+ "97 Exclusive Choice[Release E, Release D] | |\n",
+ "98 Choice[Release E, Release D] | |\n",
+ "99 Exclusive Choice[Release C, Return ER] | |\n",
+ "100 Choice[Release C, Return ER] | |\n",
+ "101 Exclusive Choice[Release E, Return ER] | |\n",
+ "102 Choice[Release E, Return ER] | |\n",
+ "103 Exclusive Choice[Release E, Release C] | |\n",
+ "104 Choice[Release E, Release C] | |\n"
+ ]
+ }
+ ],
+ "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": 6,
+ "id": "b8e0af0d",
+ "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"
+ ]
+ },
+ {
+ "ename": "Exception",
+ "evalue": "the Lydia command lydia --logic=ltlf --inline=(F(con_releasea)) | (F(con_releasee)) -p failed.\nstdout=\nstderr=docker: Error response from daemon: failed to create task for container: failed to create shim task: OCI runtime create failed: runc create failed: unable to start container process: unable to apply cgroup configuration: unable to start unit \"docker-74e8c5cae5843e6a150e8b54c21be121b58a410c7bf0d7802912aafda863fb96.scope\" (properties [{Name:Description Value:\"libcontainer container 74e8c5cae5843e6a150e8b54c21be121b58a410c7bf0d7802912aafda863fb96\"} {Name:Slice Value:\"system.slice\"} {Name:Delegate Value:true} {Name:PIDs Value:@au [15115]} {Name:MemoryAccounting Value:true} {Name:CPUAccounting Value:true} {Name:IOAccounting Value:true} {Name:TasksAccounting Value:true} {Name:DefaultDependencies Value:false}]): Message recipient disconnected from message bus without replying: unknown.\ntime=\"2024-02-21T14:44:27+01:00\" level=error msg=\"error waiting for container: \"\n",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
+ "\u001b[0;31mLogautException\u001b[0m Traceback (most recent call last)",
+ "File \u001b[0;32m~/sap/Declare4Py/.venv/lib/python3.10/site-packages/logaut/backends/lydia/_lydia_utils.py:40\u001b[0m, in \u001b[0;36mcall_lydia\u001b[0;34m(*args)\u001b[0m\n\u001b[1;32m 39\u001b[0m stderr \u001b[39m=\u001b[39m result\u001b[39m.\u001b[39mstderr\u001b[39m.\u001b[39mdecode()\n\u001b[0;32m---> 40\u001b[0m enforce(result\u001b[39m.\u001b[39;49mreturncode \u001b[39m==\u001b[39;49m \u001b[39m0\u001b[39;49m, exception_cls\u001b[39m=\u001b[39;49mLogautException)\n\u001b[1;32m 41\u001b[0m \u001b[39mreturn\u001b[39;00m output\n",
+ "File \u001b[0;32m~/sap/Declare4Py/.venv/lib/python3.10/site-packages/pylogics/helpers/misc.py:44\u001b[0m, in \u001b[0;36menforce\u001b[0;34m(condition, message, exception_cls)\u001b[0m\n\u001b[1;32m 43\u001b[0m \u001b[39mif\u001b[39;00m \u001b[39mnot\u001b[39;00m condition:\n\u001b[0;32m---> 44\u001b[0m \u001b[39mraise\u001b[39;00m exception_cls(message)\n",
+ "\u001b[0;31mLogautException\u001b[0m: ",
+ "\nDuring handling of the above exception, another exception occurred:\n",
+ "\u001b[0;31mException\u001b[0m Traceback (most recent call last)",
+ "\u001b[1;32m/home/toddy/sap/Declare4Py/Declare4Py/Utils/bpmnconstraints/tutorial/bpmn2constraints.ipynb Cell 9\u001b[0m line \u001b[0;36m4\n\u001b[1;32m 2\u001b[0m \u001b[39mprint\u001b[39m(ltl_mod\u001b[39m.\u001b[39mformula)\n\u001b[1;32m 3\u001b[0m \u001b[39mprint\u001b[39m(ltl_mod\u001b[39m.\u001b[39mparsed_formula)\n\u001b[0;32m----> 4\u001b[0m \u001b[39mprint\u001b[39m(\u001b[39mf\u001b[39m\u001b[39m'\u001b[39m\u001b[39mIs satisfiable? \u001b[39m\u001b[39m{\u001b[39;00mltl_mod\u001b[39m.\u001b[39;49mcheck_satisfiability()\u001b[39m}\u001b[39;00m\u001b[39m\\n\u001b[39;00m\u001b[39m'\u001b[39m)\n",
+ "File \u001b[0;32m~/sap/Declare4Py/.venv/lib/python3.10/site-packages/Declare4Py/ProcessModels/LTLModel.py:149\u001b[0m, in \u001b[0;36mLTLModel.check_satisfiability\u001b[0;34m(self, minimize_automaton)\u001b[0m\n\u001b[1;32m 147\u001b[0m \u001b[39mif\u001b[39;00m \u001b[39mself\u001b[39m\u001b[39m.\u001b[39mbackend \u001b[39mnot\u001b[39;00m \u001b[39min\u001b[39;00m [\u001b[39m\"\u001b[39m\u001b[39mlydia\u001b[39m\u001b[39m\"\u001b[39m, \u001b[39m\"\u001b[39m\u001b[39mltlf2dfa\u001b[39m\u001b[39m\"\u001b[39m]:\n\u001b[1;32m 148\u001b[0m \u001b[39mraise\u001b[39;00m \u001b[39mRuntimeError\u001b[39;00m(\u001b[39m\"\u001b[39m\u001b[39mOnly lydia and ltlf2dfa are supported backends.\u001b[39m\u001b[39m\"\u001b[39m)\n\u001b[0;32m--> 149\u001b[0m dfa \u001b[39m=\u001b[39m ltl2dfa(\u001b[39mself\u001b[39;49m\u001b[39m.\u001b[39;49mparsed_formula, backend\u001b[39m=\u001b[39;49m\u001b[39mself\u001b[39;49m\u001b[39m.\u001b[39;49mbackend)\n\u001b[1;32m 150\u001b[0m \u001b[39mif\u001b[39;00m minimize_automaton:\n\u001b[1;32m 151\u001b[0m dfa \u001b[39m=\u001b[39m dfa\u001b[39m.\u001b[39mminimize()\n",
+ "File \u001b[0;32m~/sap/Declare4Py/.venv/lib/python3.10/site-packages/logaut/core.py:52\u001b[0m, in \u001b[0;36mltl2dfa\u001b[0;34m(formula, backend, **backend_options)\u001b[0m\n\u001b[1;32m 41\u001b[0m \u001b[39mdef\u001b[39;00m \u001b[39mltl2dfa\u001b[39m(\n\u001b[1;32m 42\u001b[0m formula: Formula, backend: \u001b[39mstr\u001b[39m \u001b[39m=\u001b[39m _DEFAULT_BACKEND, \u001b[39m*\u001b[39m\u001b[39m*\u001b[39mbackend_options\n\u001b[1;32m 43\u001b[0m ) \u001b[39m-\u001b[39m\u001b[39m>\u001b[39m DFA:\n\u001b[1;32m 44\u001b[0m \u001b[39m \u001b[39m\u001b[39m\"\"\"\u001b[39;00m\n\u001b[1;32m 45\u001b[0m \u001b[39m From LTL to DFA.\u001b[39;00m\n\u001b[1;32m 46\u001b[0m \n\u001b[0;32m (...)\u001b[0m\n\u001b[1;32m 50\u001b[0m \u001b[39m :return: the DFA.\u001b[39;00m\n\u001b[1;32m 51\u001b[0m \u001b[39m \"\"\"\u001b[39;00m\n\u001b[0;32m---> 52\u001b[0m \u001b[39mreturn\u001b[39;00m _call_method(formula, backend, ltl2dfa\u001b[39m.\u001b[39;49m\u001b[39m__name__\u001b[39;49m, \u001b[39m*\u001b[39;49m\u001b[39m*\u001b[39;49mbackend_options)\n",
+ "File \u001b[0;32m~/sap/Declare4Py/.venv/lib/python3.10/site-packages/logaut/core.py:38\u001b[0m, in \u001b[0;36m_call_method\u001b[0;34m(formula, backend_id, method_name, **backend_options)\u001b[0m\n\u001b[1;32m 36\u001b[0m backend \u001b[39m=\u001b[39m logaut\u001b[39m.\u001b[39mbackends\u001b[39m.\u001b[39mmake(backend_id, \u001b[39m*\u001b[39m\u001b[39m*\u001b[39mbackend_options)\n\u001b[1;32m 37\u001b[0m method \u001b[39m=\u001b[39m \u001b[39mgetattr\u001b[39m(backend, method_name)\n\u001b[0;32m---> 38\u001b[0m \u001b[39mreturn\u001b[39;00m method(formula)\n",
+ "File \u001b[0;32m~/sap/Declare4Py/.venv/lib/python3.10/site-packages/logaut/backends/lydia/core.py:68\u001b[0m, in \u001b[0;36mLydiaBackend.ltl2dfa\u001b[0;34m(self, formula)\u001b[0m\n\u001b[1;32m 66\u001b[0m \u001b[39mdef\u001b[39;00m \u001b[39mltl2dfa\u001b[39m(\u001b[39mself\u001b[39m, formula: Formula) \u001b[39m-\u001b[39m\u001b[39m>\u001b[39m DFA:\n\u001b[1;32m 67\u001b[0m \u001b[39m \u001b[39m\u001b[39m\"\"\"From LTL to DFA.\"\"\"\u001b[39;00m\n\u001b[0;32m---> 68\u001b[0m \u001b[39mreturn\u001b[39;00m _process_formula(formula)\n",
+ "File \u001b[0;32m~/sap/Declare4Py/.venv/lib/python3.10/site-packages/logaut/backends/lydia/core.py:79\u001b[0m, in \u001b[0;36m_process_formula\u001b[0;34m(formula)\u001b[0m\n\u001b[1;32m 72\u001b[0m \u001b[39m\u001b[39m\u001b[39m\"\"\"\u001b[39;00m\n\u001b[1;32m 73\u001b[0m \u001b[39mProcess a formula with Lydia.\u001b[39;00m\n\u001b[1;32m 74\u001b[0m \n\u001b[1;32m 75\u001b[0m \u001b[39m:param formula: the formula\u001b[39;00m\n\u001b[1;32m 76\u001b[0m \u001b[39m:return: the DFA\u001b[39;00m\n\u001b[1;32m 77\u001b[0m \u001b[39m\"\"\"\u001b[39;00m\n\u001b[1;32m 78\u001b[0m formula_str \u001b[39m=\u001b[39m to_string(formula)\n\u001b[0;32m---> 79\u001b[0m output \u001b[39m=\u001b[39m call_lydia(\n\u001b[1;32m 80\u001b[0m \u001b[39mf\u001b[39;49m\u001b[39m\"\u001b[39;49m\u001b[39m--logic=\u001b[39;49m\u001b[39m{\u001b[39;49;00mformula\u001b[39m.\u001b[39;49mlogic\u001b[39m.\u001b[39;49mvalue\u001b[39m}\u001b[39;49;00m\u001b[39mf\u001b[39;49m\u001b[39m\"\u001b[39;49m, \u001b[39mf\u001b[39;49m\u001b[39m\"\u001b[39;49m\u001b[39m--inline=\u001b[39;49m\u001b[39m{\u001b[39;49;00mformula_str\u001b[39m}\u001b[39;49;00m\u001b[39m\"\u001b[39;49m, \u001b[39m\"\u001b[39;49m\u001b[39m-p\u001b[39;49m\u001b[39m\"\u001b[39;49m\n\u001b[1;32m 81\u001b[0m )\n\u001b[1;32m 82\u001b[0m mona_output_string \u001b[39m=\u001b[39m postprocess_lydia_output(output)\n\u001b[1;32m 83\u001b[0m mona_output \u001b[39m=\u001b[39m parse_mona_output(mona_output_string)\n",
+ "File \u001b[0;32m~/sap/Declare4Py/.venv/lib/python3.10/site-packages/logaut/backends/lydia/_lydia_utils.py:43\u001b[0m, in \u001b[0;36mcall_lydia\u001b[0;34m(*args)\u001b[0m\n\u001b[1;32m 41\u001b[0m \u001b[39mreturn\u001b[39;00m output\n\u001b[1;32m 42\u001b[0m \u001b[39mexcept\u001b[39;00m LogautException:\n\u001b[0;32m---> 43\u001b[0m \u001b[39mraise\u001b[39;00m \u001b[39mException\u001b[39;00m( \u001b[39m# type: ignore\u001b[39;00m\n\u001b[1;32m 44\u001b[0m \u001b[39mf\u001b[39m\u001b[39m\"\u001b[39m\u001b[39mthe Lydia command \u001b[39m\u001b[39m{\u001b[39;00m\u001b[39m'\u001b[39m\u001b[39m \u001b[39m\u001b[39m'\u001b[39m\u001b[39m.\u001b[39mjoin(command)\u001b[39m}\u001b[39;00m\u001b[39m failed.\u001b[39m\u001b[39m\\n\u001b[39;00m\u001b[39mstdout=\u001b[39m\u001b[39m{\u001b[39;00moutput\u001b[39m}\u001b[39;00m\u001b[39m\\n\u001b[39;00m\u001b[39mstderr=\u001b[39m\u001b[39m{\u001b[39;00mstderr\u001b[39m}\u001b[39;00m\u001b[39m\"\u001b[39m \u001b[39m# type: ignore\u001b[39;00m\n\u001b[1;32m 45\u001b[0m )\n\u001b[1;32m 46\u001b[0m \u001b[39mexcept\u001b[39;00m \u001b[39mException\u001b[39;00m \u001b[39mas\u001b[39;00m e:\n\u001b[1;32m 47\u001b[0m \u001b[39mraise\u001b[39;00m \u001b[39mException\u001b[39;00m(\u001b[39mf\u001b[39m\u001b[39m\"\u001b[39m\u001b[39man error occurred while running lydia: \u001b[39m\u001b[39m{\u001b[39;00m\u001b[39mstr\u001b[39m(e)\u001b[39m}\u001b[39;00m\u001b[39m\"\u001b[39m) \u001b[39mfrom\u001b[39;00m \u001b[39me\u001b[39;00m\n",
+ "\u001b[0;31mException\u001b[0m: the Lydia command lydia --logic=ltlf --inline=(F(con_releasea)) | (F(con_releasee)) -p failed.\nstdout=\nstderr=docker: Error response from daemon: failed to create task for container: failed to create shim task: OCI runtime create failed: runc create failed: unable to start container process: unable to apply cgroup configuration: unable to start unit \"docker-74e8c5cae5843e6a150e8b54c21be121b58a410c7bf0d7802912aafda863fb96.scope\" (properties [{Name:Description Value:\"libcontainer container 74e8c5cae5843e6a150e8b54c21be121b58a410c7bf0d7802912aafda863fb96\"} {Name:Slice Value:\"system.slice\"} {Name:Delegate Value:true} {Name:PIDs Value:@au [15115]} {Name:MemoryAccounting Value:true} {Name:CPUAccounting Value:true} {Name:IOAccounting Value:true} {Name:TasksAccounting Value:true} {Name:DefaultDependencies Value:false}]): Message recipient disconnected from message bus without replying: unknown.\ntime=\"2024-02-21T14:44:27+01:00\" level=error msg=\"error waiting for container: \"\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": 7,
+ "id": "d3ca4381",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stderr",
+ "output_type": "stream",
+ "text": [
+ "/home/toddy/sap/Declare4Py/.venv/lib/python3.10/site-packages/pm4py/util/dt_parsing/parser.py:76: UserWarning: ISO8601 strings are not fully supported with strpfromiso for Python versions below 3.11\n",
+ " warnings.warn(\n",
+ "/home/toddy/sap/Declare4Py/.venv/lib/python3.10/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, 1381.44it/s]\n",
+ "/home/toddy/sap/Declare4Py/.venv/lib/python3.10/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"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Showcasing the issue with DECLARE analyzer"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "The checker function for template Succession has not been implemented yet.\n"
+ ]
+ },
+ {
+ "ename": "TypeError",
+ "evalue": "'NoneType' object is not callable",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
+ "\u001b[0;31mTypeError\u001b[0m Traceback (most recent call last)",
+ "\u001b[1;32m/home/toddy/sap/Declare4Py/Declare4Py/Utils/bpmnconstraints/tutorial/bpmn2constraints.ipynb Cell 13\u001b[0m line \u001b[0;36m4\n\u001b[1;32m 1\u001b[0m \u001b[39mfrom\u001b[39;00m \u001b[39mDeclare4Py\u001b[39;00m\u001b[39m.\u001b[39;00m\u001b[39mProcessMiningTasks\u001b[39;00m\u001b[39m.\u001b[39;00m\u001b[39mConformanceChecking\u001b[39;00m\u001b[39m.\u001b[39;00m\u001b[39mMPDeclareAnalyzer\u001b[39;00m \u001b[39mimport\u001b[39;00m MPDeclareAnalyzer, MPDeclareResultsBrowser\n\u001b[1;32m 3\u001b[0m basic_checker \u001b[39m=\u001b[39m MPDeclareAnalyzer(log\u001b[39m=\u001b[39mevent_log, declare_model\u001b[39m=\u001b[39mdeclare_model, consider_vacuity\u001b[39m=\u001b[39m\u001b[39mFalse\u001b[39;00m)\n\u001b[0;32m----> 4\u001b[0m conf_check_res: MPDeclareResultsBrowser \u001b[39m=\u001b[39m basic_checker\u001b[39m.\u001b[39;49mrun()\n",
+ "File \u001b[0;32m~/sap/Declare4Py/.venv/lib/python3.10/site-packages/Declare4Py/ProcessMiningTasks/ConformanceChecking/MPDeclareAnalyzer.py:46\u001b[0m, in \u001b[0;36mMPDeclareAnalyzer.run\u001b[0;34m(self)\u001b[0m\n\u001b[1;32m 44\u001b[0m log_checkers_results \u001b[39m=\u001b[39m []\n\u001b[1;32m 45\u001b[0m \u001b[39mfor\u001b[39;00m trace \u001b[39min\u001b[39;00m \u001b[39mself\u001b[39m\u001b[39m.\u001b[39mevent_log\u001b[39m.\u001b[39mget_log():\n\u001b[0;32m---> 46\u001b[0m log_checkers_results\u001b[39m.\u001b[39mappend(ConstraintChecker()\u001b[39m.\u001b[39;49mcheck_trace_conformance(trace, \u001b[39mself\u001b[39;49m\u001b[39m.\u001b[39;49mprocess_model,\n\u001b[1;32m 47\u001b[0m \u001b[39mself\u001b[39;49m\u001b[39m.\u001b[39;49mconsider_vacuity,\n\u001b[1;32m 48\u001b[0m \u001b[39mself\u001b[39;49m\u001b[39m.\u001b[39;49mevent_log\u001b[39m.\u001b[39;49mactivity_key))\n\u001b[1;32m 49\u001b[0m \u001b[39mreturn\u001b[39;00m MPDeclareResultsBrowser(log_checkers_results, \u001b[39mself\u001b[39m\u001b[39m.\u001b[39mprocess_model\u001b[39m.\u001b[39mserialized_constraints)\n",
+ "File \u001b[0;32m~/sap/Declare4Py/.venv/lib/python3.10/site-packages/Declare4Py/Utils/Declare/Checkers.py:47\u001b[0m, in \u001b[0;36mConstraintChecker.check_trace_conformance\u001b[0;34m(self, trace, decl_model, consider_vacuity, concept_name)\u001b[0m\n\u001b[1;32m 45\u001b[0m rules[\u001b[39m\"\u001b[39m\u001b[39mtime\u001b[39m\u001b[39m\"\u001b[39m] \u001b[39m=\u001b[39m constraint[\u001b[39m'\u001b[39m\u001b[39mcondition\u001b[39m\u001b[39m'\u001b[39m][\u001b[39m-\u001b[39m\u001b[39m1\u001b[39m] \u001b[39m# time condition is always at last position\u001b[39;00m\n\u001b[1;32m 46\u001b[0m \u001b[39mtry\u001b[39;00m:\n\u001b[0;32m---> 47\u001b[0m trace_results\u001b[39m.\u001b[39mappend(TemplateConstraintChecker(trace, \u001b[39mTrue\u001b[39;49;00m, constraint[\u001b[39m'\u001b[39;49m\u001b[39mactivities\u001b[39;49m\u001b[39m'\u001b[39;49m], rules,\n\u001b[1;32m 48\u001b[0m concept_name)\u001b[39m.\u001b[39;49mget_template(constraint[\u001b[39m'\u001b[39;49m\u001b[39mtemplate\u001b[39;49m\u001b[39m'\u001b[39;49m])())\n\u001b[1;32m 49\u001b[0m \u001b[39mexcept\u001b[39;00m \u001b[39mSyntaxError\u001b[39;00m:\n\u001b[1;32m 50\u001b[0m \u001b[39m# TODO: use python logger\u001b[39;00m\n\u001b[1;32m 51\u001b[0m \u001b[39mif\u001b[39;00m constraint_str \u001b[39mnot\u001b[39;00m \u001b[39min\u001b[39;00m error_constraint_set:\n",
+ "\u001b[0;31mTypeError\u001b[0m: 'NoneType' object is not callable"
+ ]
+ }
+ ],
+ "source": [
+ "from Declare4Py.ProcessMiningTasks.ConformanceChecking.MPDeclareAnalyzer import MPDeclareAnalyzer, MPDeclareResultsBrowser\n",
+ "\n",
+ "basic_checker = MPDeclareAnalyzer(log=event_log, declare_model=declare_model, consider_vacuity=False)\n",
+ "conf_check_res: MPDeclareResultsBrowser = basic_checker.run()"
+ ]
+ }
+ ],
+ "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.10.12"
+ }
+ },
+ "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 00000000..57229a3f
Binary files /dev/null and b/Declare4Py/Utils/bpmnconstraints/tutorial/data/Sepsis Cases.png differ
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 00000000..7e4a29ed
Binary files /dev/null and b/Declare4Py/Utils/bpmnconstraints/tutorial/data/linear_diagram.png differ
diff --git a/Declare4Py/Utils/bpmnconstraints/tutorial/data/linear_sequence.xml b/Declare4Py/Utils/bpmnconstraints/tutorial/data/linear_sequence.xml
new file mode 100644
index 00000000..d7280baf
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/tutorial/data/linear_sequence.xml
@@ -0,0 +1,565 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-901975D0-4ACF-435A-947B-CBE43084E37E
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-901975D0-4ACF-435A-947B-CBE43084E37E
+ sid-E99436E0-2FD8-4D15-A06C-ABA769A68FB4
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-E99436E0-2FD8-4D15-A06C-ABA769A68FB4
+ sid-1E17AE5F-3352-4DCD-A9D4-28F49EF82206
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ sid-1E17AE5F-3352-4DCD-A9D4-28F49EF82206
+ sid-68983014-C7A8-4FA0-A13C-32ACFD4069CA
+
+
+
+
+
+
+
+
+
+
+
+ sid-68983014-C7A8-4FA0-A13C-32ACFD4069CA
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Declare4Py/Utils/bpmnconstraints/utils/__init__.py b/Declare4Py/Utils/bpmnconstraints/utils/__init__.py
new file mode 100644
index 00000000..e69de29b
diff --git a/Declare4Py/Utils/bpmnconstraints/utils/constants.py b/Declare4Py/Utils/bpmnconstraints/utils/constants.py
new file mode 100644
index 00000000..59551518
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/utils/constants.py
@@ -0,0 +1,177 @@
+"""Constants for the parser"""
+
+ALLOWED_GATEWAYS = [
+ "exclusive_databased_gateway",
+ "parallelgateway",
+ "inclusivegateway",
+ "complexgateway",
+ "eventbasedgateway",
+ "exclusivegateway",
+]
+
+DISCARDED_START_GATEWAYS = [
+ "exclusive_databased_gateway",
+ "exclusivegateway"
+]
+
+ALLOWED_ACTIVITIES = [
+ "task",
+ "event",
+ "collapsedsubprocess",
+ "businessrole",
+ "eventsubprocess",
+ "collapsedeventsubprocess",
+ "subprocess",
+ "process",
+ "intermediatemessageeventcatching",
+ "intermediatetimerevent",
+ "intermediateescalationevent",
+ "intermediateconditionalevent",
+ "intermediatelinkeventcatching",
+ "intermediateerrorevent",
+ "intermediatecancelevent",
+ "intermediatecompensationeventcatching",
+ "intermediatesignaleventcatching",
+ "intermediatemultipleeventcatching",
+ "intermediateparallelmultipleeventcatching",
+ "intermediateevent",
+ "intermediatemessageeventthrowing",
+ "intermediateescalationeventthrowing",
+ "intermediatelinkeventthrowing",
+ "intermediatecompensationeventthrowing",
+ "intermediatesignaleventthrowing",
+ "intermediatemultipleeventthrowing",
+]
+
+ALLOWED_START_EVENTS = [
+ "startevent",
+ "startnoneevent",
+ "startmessageevent",
+ "starttimerevent",
+ "starterrorevent",
+ "startcompensationevent",
+ "startparallelmultipleevent",
+ "startescalationevent",
+ "startconditionalevent",
+ "startsignalevent",
+ "startmultipleevent",
+]
+
+ALLOWED_END_EVENTS = [
+ "end",
+ "endevent",
+ "endnoneevent",
+ "endescalationevent",
+ "endmessageevent",
+ "enderrorevent",
+ "endcancelevent",
+ "endcompensationevent",
+ "endsignalevent",
+ "endmultipleevent",
+ "endterminateevent",
+]
+
+ALLOWED_SWIMLANES = [
+ "pool",
+ "lane",
+]
+
+ALLOWED_CONNECTING_OBJECTS = ["sequenceflow"]
+
+GATEWAY_MAPPING = {
+ ALLOWED_GATEWAYS[0]: "XOR",
+ ALLOWED_GATEWAYS[1]: "AND",
+ ALLOWED_GATEWAYS[2]: "OR",
+ ALLOWED_GATEWAYS[3]: "COMPLEX",
+ ALLOWED_GATEWAYS[4]: "EVENT_BASED",
+}
+
+END_EVENT_MAPPING = {
+ "endnoneevent": "endnoneevent",
+ "endescalationevent": "endescalationevent",
+ "endmessageevent": "endmessageevent",
+ "enderrorevent": "enderrorevent",
+ "endcancelevent": "endcancelevent",
+ "endcompensationevent": "endcompensationevent",
+ "endsignalevent": "endsignalevent",
+ "endmultipleevent": "endmultipleevent",
+ "endterminateevent": "endterminateevent",
+}
+
+ACTIVITY_MAPPING = {
+ "task": "task",
+ "event": "event",
+ "collapsedsubprocess": "subprocess",
+ "eventsubprocess": "subprocess",
+ "collapsedeventsubprocess": "subprocess",
+ "subprocess": "subprocess",
+ "intermediatemessageeventcatching": "catchactivity",
+ "intermediatetimerevent": "intermediateevent",
+ "intermediateescalationevent": "intermediateevent",
+ "intermediateconditionalevent": "intermediateevent",
+ "intermediatelinkeventcatching": "catchactivity",
+ "intermediateerrorevent": "intermediateevent",
+ "intermediatecancelevent": "intermediateevent",
+ "intermediatecompensationeventcatching": "catchactivity",
+ "intermediatesignaleventcatching": "catchactivity",
+ "intermediatemultipleeventcatching": "catchactivity",
+ "intermediateparallelmultipleeventcatching": "catchactivity",
+ "intermediateevent": "intermediateevent",
+ "intermediatemessageeventthrowing": "throwactivity",
+ "intermediateescalationeventthrowing": "throwactivity",
+ "intermediatelinkeventthrowing": "throwactivity",
+ "intermediatecompensationeventthrowing": "throwactivity",
+ "intermediatesignaleventthrowing": "throwactivity",
+ "intermediatemultipleeventthrowing": "throwactivity",
+}
+
+GATEWAY_NAMES = [
+ "AND",
+ "XOR",
+ "OR",
+ "COMPLEX",
+ "EVENT_BASED",
+]
+
+DISCARDED_CONSTRAINTS = [
+ "Exactly1",
+ "Responded Existence",
+ "Absence2",
+ "Existence1",
+ "Existence2",
+ "Exactly2",
+]
+
+DISCARDED_START_EVENT_NAMES = ["start", "Start", "START", "AND", "XOR", "OR"]
+
+DISCARDED_END_EVENT_NAMES = [
+ "end",
+ "End",
+ "END",
+ "AND",
+ "XOR",
+ "OR",
+]
+
+XOR_GATEWAY = ["exclusive_databased_gateway", "exclusivegateway"]
+AND_GATEWAY = "parallelgateway"
+OR_GATEWAY = "inclusivegateway"
+
+VALID_NAME_LENGTH = 5
+
+CHILD_SHAPES = "childShapes"
+OUTGOING = "outgoing"
+ELEMENT_ID = "resourceId"
+STENCIL = "stencil"
+ID = "id"
+PROPERTIES = "properties"
+NAME = "name"
+
+DECLARE_CONSTRAINT_REGEX_PATTERN = r"(\w+(?:-\w+)?(?: \w+)?)(?: \w+)?\[(.*?)\]"
+
+DECLARE_GATEWAYS = ["Co-Existence", "Choice", "Exclusive Choice"]
+
+DEFAULT_DIRECTION = "LR"
+SEQUENCE_FLOW = "-->"
+# END_EVENT_STYLING_DEF = "classDef EndEvent fill:stroke:#000,stroke-width:4px"
+# END_EVENT_STYLE = ":::EndEvent"
diff --git a/Declare4Py/Utils/bpmnconstraints/utils/sanitizer.py b/Declare4Py/Utils/bpmnconstraints/utils/sanitizer.py
new file mode 100644
index 00000000..fb727d2c
--- /dev/null
+++ b/Declare4Py/Utils/bpmnconstraints/utils/sanitizer.py
@@ -0,0 +1,37 @@
+"""
+All code in module is based upon Adrian Rebmann's codebase.
+"""
+
+import re
+
+NON_ALPHANUM = re.compile("[^a-zA-Z]")
+CAMEL_PATTERN_1 = re.compile("(.)([A-Z][a-z]+)")
+CAMEL_PATTERN_2 = re.compile("([a-z0-9])([A-Z])")
+
+
+class Sanitizer:
+ def __init__(self) -> None:
+ pass
+
+ def sanitize_label(self, label):
+ label = str(label)
+ if " - " in label:
+ label = label.split(" - ")[-1]
+ if "&" in label:
+ label = label.replace("&", "and")
+ label = label.replace("\n", " ").replace("\r", "")
+ label = label.replace("(s)", "s")
+ label = label.replace("'", "")
+ label = re.sub(" +", " ", label)
+
+ label = NON_ALPHANUM.sub(" ", label)
+ label = label.strip()
+
+ label = self.__camel_to_white(label)
+
+ label = re.sub(r"\s{1,}", " ", label)
+ return label
+
+ def __camel_to_white(self, label):
+ label = CAMEL_PATTERN_1.sub(r"\1 \2", label)
+ return CAMEL_PATTERN_2.sub(r"\1 \2", label)