diff --git a/models/bpmn-origin/json_from_bpmn/e038TravelAgency.json b/models/bpmn-origin/json_from_bpmn/e038TravelAgency.json
new file mode 100644
index 0000000..8c298a7
--- /dev/null
+++ b/models/bpmn-origin/json_from_bpmn/e038TravelAgency.json
@@ -0,0 +1,366 @@
+{
+    "catN": {
+        "Task_1q91vog": {
+            "tag": "SendTask"
+        },
+        "EndEvent_17rlcaz": {
+            "tag": "NoneEndEvent"
+        },
+        "IntermediateThrowEvent_0neineb": {
+            "tag": "CatchMessageIntermediateEvent"
+        },
+        "ExclusiveGateway_0i09ijx": {
+            "tag": "XorGateway"
+        },
+        "IntermediateThrowEvent_12d113r": {
+            "tag": "CatchMessageIntermediateEvent"
+        },
+        "ExclusiveGateway_192ovii": {
+            "tag": "XorGateway"
+        },
+        "StartEvent_1": {
+            "tag": "NoneStartEvent"
+        },
+        "BoundaryEvent_0qlhw6m": {
+            "tag": "MessageBoundaryEvent",
+            "cancelActivity": true
+        },
+        "StartEvent_1f3jj6d": {
+            "tag": "NoneStartEvent"
+        },
+        "ExclusiveGateway_1dc5v3z": {
+            "tag": "XorGateway"
+        },
+        "SubProcess_1agd6n3": {
+            "tag": "SubProcess"
+        },
+        "TravelAgency_": {
+            "tag": "Process"
+        },
+        "EndEvent_0u6deep": {
+            "tag": "CatchMessageIntermediateEvent"
+        },
+        "Task_07u875a": {
+            "tag": "ReceiveTask"
+        },
+        "Task_1bn6n5q": {
+            "tag": "SendTask"
+        },
+        "EndEvent_055yt9k": {
+            "tag": "NoneEndEvent"
+        },
+        "EndEvent_10gqkzy": {
+            "tag": "NoneEndEvent"
+        },
+        "IntermediateThrowEvent_0b4rm53": {
+            "tag": "ThrowMessageIntermediateEvent"
+        },
+        "Customer_": {
+            "tag": "Process"
+        },
+        "BoundaryEvent_19y0yk9": {
+            "tag": "MessageBoundaryEvent",
+            "cancelActivity": true
+        },
+        "Task_002ndsu": {
+            "tag": "SendTask"
+        },
+        "StartEvent_0qomvov": {
+            "tag": "NoneStartEvent"
+        },
+        "Task_1ne4gpy": {
+            "tag": "SendTask"
+        },
+        "EndEvent_0syu44v": {
+            "tag": "NoneEndEvent"
+        },
+        "IntermediateThrowEvent_02q48nh": {
+            "tag": "ThrowMessageIntermediateEvent"
+        },
+        "EndEvent_1vkzo14": {
+            "tag": "NoneEndEvent"
+        },
+        "IntermediateThrowEvent_0xjpikb": {
+            "tag": "CatchMessageIntermediateEvent"
+        },
+        "Task_1v9s881": {
+            "tag": "SendTask"
+        },
+        "ExclusiveGateway_0wgdt1i": {
+            "tag": "XorGateway"
+        }
+    },
+    "catE": {
+        "SequenceFlow_1h5h7h5": "NormalSequenceFlow",
+        "SequenceFlow_0ybs6n8": "NormalSequenceFlow",
+        "SequenceFlow_0rfye55": "DefaultSequenceFlow",
+        "SequenceFlow_0sfyd5z": "NormalSequenceFlow",
+        "SequenceFlow_17r8ru7": "NormalSequenceFlow",
+        "SequenceFlow_0ot5p93": "NormalSequenceFlow",
+        "SequenceFlow_13z4ilm": "ConditionalSequenceFlow",
+        "SequenceFlow_0ljbxox": "NormalSequenceFlow",
+        "SequenceFlow_1pk6qce": "NormalSequenceFlow",
+        "SequenceFlow_0yhi6sc": "NormalSequenceFlow",
+        "SequenceFlow_0mdvaai": "NormalSequenceFlow",
+        "SequenceFlow_016h32p": "NormalSequenceFlow",
+        "SequenceFlow_1uwq0b6": "ConditionalSequenceFlow",
+        "MessageFlow_1m551dh": "MessageFlow",
+        "MessageFlow_1yfhhru": "MessageFlow",
+        "MessageFlow_04an7oz": "MessageFlow",
+        "SequenceFlow_0b34324": "NormalSequenceFlow",
+        "SequenceFlow_023db5j": "NormalSequenceFlow",
+        "SequenceFlow_1yvkisw": "NormalSequenceFlow",
+        "SequenceFlow_1qku5do": "NormalSequenceFlow",
+        "SequenceFlow_1rma3l8": "NormalSequenceFlow",
+        "SequenceFlow_0b6ku63": "DefaultSequenceFlow",
+        "MessageFlow_1goz1mt": "MessageFlow",
+        "MessageFlow_18qwt5e": "MessageFlow",
+        "MessageFlow_0knd10s": "MessageFlow",
+        "SequenceFlow_1oyuvjd": "NormalSequenceFlow",
+        "SequenceFlow_1dptcxp": "NormalSequenceFlow",
+        "SequenceFlow_1fn4lqy": "NormalSequenceFlow",
+        "MessageFlow_0joml9p": "MessageFlow",
+        "SequenceFlow_0bejayl": "NormalSequenceFlow",
+        "SequenceFlow_1j6r6o5": "NormalSequenceFlow"
+    },
+    "containN": {
+        "SubProcess_1agd6n3": [
+            "StartEvent_0qomvov",
+            "IntermediateThrowEvent_0xjpikb",
+            "IntermediateThrowEvent_0neineb",
+            "Task_002ndsu",
+            "Task_1ne4gpy",
+            "EndEvent_1vkzo14"
+        ],
+        "TravelAgency_": [
+            "StartEvent_1f3jj6d",
+            "ExclusiveGateway_1dc5v3z",
+            "Task_1bn6n5q",
+            "ExclusiveGateway_0i09ijx",
+            "SubProcess_1agd6n3",
+            "IntermediateThrowEvent_0b4rm53",
+            "EndEvent_10gqkzy",
+            "BoundaryEvent_19y0yk9",
+            "EndEvent_17rlcaz"
+        ],
+        "Customer_": [
+            "Task_1v9s881",
+            "ExclusiveGateway_192ovii",
+            "ExclusiveGateway_0wgdt1i",
+            "StartEvent_1",
+            "Task_07u875a",
+            "EndEvent_055yt9k",
+            "EndEvent_0u6deep",
+            "IntermediateThrowEvent_12d113r",
+            "Task_1q91vog",
+            "BoundaryEvent_0qlhw6m",
+            "EndEvent_0syu44v",
+            "IntermediateThrowEvent_02q48nh"
+        ]
+    },
+    "messageE": {
+        "MessageFlow_1m551dh": "Confirmation",
+        "MessageFlow_1yfhhru": "Travel",
+        "MessageFlow_04an7oz": "Ticket",
+        "MessageFlow_1goz1mt": "Payment",
+        "MessageFlow_18qwt5e": "Abort",
+        "MessageFlow_0knd10s": "Offer",
+        "MessageFlow_0joml9p": "NoMore"
+    },
+    "targetE": {
+        "SequenceFlow_1h5h7h5": "IntermediateThrowEvent_12d113r",
+        "SequenceFlow_0ybs6n8": "EndEvent_0syu44v",
+        "SequenceFlow_0rfye55": "IntermediateThrowEvent_0b4rm53",
+        "SequenceFlow_0sfyd5z": "ExclusiveGateway_192ovii",
+        "SequenceFlow_17r8ru7": "IntermediateThrowEvent_0xjpikb",
+        "SequenceFlow_0ot5p93": "Task_1ne4gpy",
+        "SequenceFlow_13z4ilm": "ExclusiveGateway_1dc5v3z",
+        "SequenceFlow_0ljbxox": "EndEvent_0u6deep",
+        "SequenceFlow_1pk6qce": "IntermediateThrowEvent_02q48nh",
+        "SequenceFlow_0yhi6sc": "SubProcess_1agd6n3",
+        "SequenceFlow_0mdvaai": "ExclusiveGateway_0i09ijx",
+        "SequenceFlow_016h32p": "Task_07u875a",
+        "SequenceFlow_1uwq0b6": "Task_1v9s881",
+        "MessageFlow_1m551dh": "EndEvent_0u6deep",
+        "MessageFlow_1yfhhru": "IntermediateThrowEvent_0xjpikb",
+        "MessageFlow_04an7oz": "IntermediateThrowEvent_12d113r",
+        "SequenceFlow_0b34324": "Task_1bn6n5q",
+        "SequenceFlow_023db5j": "EndEvent_1vkzo14",
+        "SequenceFlow_1yvkisw": "EndEvent_10gqkzy",
+        "SequenceFlow_1qku5do": "EndEvent_055yt9k",
+        "SequenceFlow_1rma3l8": "ExclusiveGateway_0wgdt1i",
+        "SequenceFlow_0b6ku63": "ExclusiveGateway_0wgdt1i",
+        "MessageFlow_1goz1mt": "IntermediateThrowEvent_0neineb",
+        "MessageFlow_18qwt5e": "BoundaryEvent_19y0yk9",
+        "MessageFlow_0knd10s": "Task_07u875a",
+        "SequenceFlow_1oyuvjd": "EndEvent_17rlcaz",
+        "SequenceFlow_1dptcxp": "Task_1q91vog",
+        "SequenceFlow_1fn4lqy": "ExclusiveGateway_1dc5v3z",
+        "MessageFlow_0joml9p": "BoundaryEvent_0qlhw6m",
+        "SequenceFlow_0bejayl": "Task_002ndsu",
+        "SequenceFlow_1j6r6o5": "IntermediateThrowEvent_0neineb"
+    },
+    "name": "e038TravelAgency",
+    "attached": {
+        "BoundaryEvent_0qlhw6m": "Task_07u875a",
+        "BoundaryEvent_19y0yk9": "SubProcess_1agd6n3"
+    },
+    "containE": {
+        "SubProcess_1agd6n3": [
+            "SequenceFlow_17r8ru7",
+            "SequenceFlow_1j6r6o5",
+            "SequenceFlow_0bejayl",
+            "SequenceFlow_0ot5p93",
+            "SequenceFlow_023db5j"
+        ],
+        "TravelAgency_": [
+            "SequenceFlow_1fn4lqy",
+            "SequenceFlow_0b34324",
+            "SequenceFlow_0mdvaai",
+            "SequenceFlow_13z4ilm",
+            "SequenceFlow_0rfye55",
+            "SequenceFlow_0yhi6sc",
+            "SequenceFlow_1yvkisw",
+            "SequenceFlow_1oyuvjd"
+        ],
+        "Customer_": [
+            "SequenceFlow_1uwq0b6",
+            "SequenceFlow_0b6ku63",
+            "SequenceFlow_0sfyd5z",
+            "SequenceFlow_016h32p",
+            "SequenceFlow_1rma3l8",
+            "SequenceFlow_1dptcxp",
+            "SequenceFlow_1h5h7h5",
+            "SequenceFlow_0ljbxox",
+            "SequenceFlow_1qku5do",
+            "SequenceFlow_1pk6qce",
+            "SequenceFlow_0ybs6n8"
+        ]
+    },
+    "edges": [
+        "MessageFlow_0knd10s",
+        "MessageFlow_1yfhhru",
+        "MessageFlow_1m551dh",
+        "MessageFlow_1goz1mt",
+        "MessageFlow_04an7oz",
+        "MessageFlow_0joml9p",
+        "MessageFlow_18qwt5e",
+        "SequenceFlow_1uwq0b6",
+        "SequenceFlow_0b6ku63",
+        "SequenceFlow_0sfyd5z",
+        "SequenceFlow_016h32p",
+        "SequenceFlow_1rma3l8",
+        "SequenceFlow_1dptcxp",
+        "SequenceFlow_1h5h7h5",
+        "SequenceFlow_0ljbxox",
+        "SequenceFlow_1qku5do",
+        "SequenceFlow_1pk6qce",
+        "SequenceFlow_0ybs6n8",
+        "SequenceFlow_1fn4lqy",
+        "SequenceFlow_0b34324",
+        "SequenceFlow_0mdvaai",
+        "SequenceFlow_13z4ilm",
+        "SequenceFlow_0rfye55",
+        "SequenceFlow_0yhi6sc",
+        "SequenceFlow_1yvkisw",
+        "SequenceFlow_1oyuvjd",
+        "SequenceFlow_17r8ru7",
+        "SequenceFlow_1j6r6o5",
+        "SequenceFlow_0bejayl",
+        "SequenceFlow_0ot5p93",
+        "SequenceFlow_023db5j"
+    ],
+    "messages": [
+        "Offer",
+        "Travel",
+        "Confirmation",
+        "Payment",
+        "Ticket",
+        "NoMore",
+        "Abort"
+    ],
+    "sourceE": {
+        "SequenceFlow_1h5h7h5": "Task_1q91vog",
+        "SequenceFlow_0ybs6n8": "IntermediateThrowEvent_02q48nh",
+        "SequenceFlow_0rfye55": "ExclusiveGateway_0i09ijx",
+        "SequenceFlow_0sfyd5z": "Task_07u875a",
+        "SequenceFlow_17r8ru7": "StartEvent_0qomvov",
+        "SequenceFlow_0ot5p93": "Task_002ndsu",
+        "SequenceFlow_13z4ilm": "ExclusiveGateway_0i09ijx",
+        "SequenceFlow_0ljbxox": "IntermediateThrowEvent_12d113r",
+        "SequenceFlow_1pk6qce": "BoundaryEvent_0qlhw6m",
+        "SequenceFlow_0yhi6sc": "IntermediateThrowEvent_0b4rm53",
+        "SequenceFlow_0mdvaai": "Task_1bn6n5q",
+        "SequenceFlow_016h32p": "ExclusiveGateway_0wgdt1i",
+        "SequenceFlow_1uwq0b6": "ExclusiveGateway_192ovii",
+        "MessageFlow_1m551dh": "Task_002ndsu",
+        "MessageFlow_1yfhhru": "Task_1v9s881",
+        "MessageFlow_04an7oz": "Task_1ne4gpy",
+        "SequenceFlow_0b34324": "ExclusiveGateway_1dc5v3z",
+        "SequenceFlow_023db5j": "Task_1ne4gpy",
+        "SequenceFlow_1yvkisw": "SubProcess_1agd6n3",
+        "SequenceFlow_1qku5do": "EndEvent_0u6deep",
+        "SequenceFlow_1rma3l8": "StartEvent_1",
+        "SequenceFlow_0b6ku63": "ExclusiveGateway_192ovii",
+        "MessageFlow_1goz1mt": "Task_1q91vog",
+        "MessageFlow_18qwt5e": "IntermediateThrowEvent_02q48nh",
+        "MessageFlow_0knd10s": "Task_1bn6n5q",
+        "SequenceFlow_1oyuvjd": "BoundaryEvent_19y0yk9",
+        "SequenceFlow_1dptcxp": "Task_1v9s881",
+        "SequenceFlow_1fn4lqy": "StartEvent_1f3jj6d",
+        "MessageFlow_0joml9p": "IntermediateThrowEvent_0b4rm53",
+        "SequenceFlow_0bejayl": "IntermediateThrowEvent_0neineb",
+        "SequenceFlow_1j6r6o5": "IntermediateThrowEvent_0xjpikb"
+    },
+    "nodes": [
+        "Customer_",
+        "TravelAgency_",
+        "Task_1v9s881",
+        "ExclusiveGateway_192ovii",
+        "ExclusiveGateway_0wgdt1i",
+        "StartEvent_1",
+        "Task_07u875a",
+        "EndEvent_055yt9k",
+        "EndEvent_0u6deep",
+        "IntermediateThrowEvent_12d113r",
+        "Task_1q91vog",
+        "BoundaryEvent_0qlhw6m",
+        "EndEvent_0syu44v",
+        "IntermediateThrowEvent_02q48nh",
+        "StartEvent_1f3jj6d",
+        "ExclusiveGateway_1dc5v3z",
+        "Task_1bn6n5q",
+        "ExclusiveGateway_0i09ijx",
+        "SubProcess_1agd6n3",
+        "IntermediateThrowEvent_0b4rm53",
+        "EndEvent_10gqkzy",
+        "BoundaryEvent_19y0yk9",
+        "EndEvent_17rlcaz",
+        "StartEvent_0qomvov",
+        "IntermediateThrowEvent_0xjpikb",
+        "IntermediateThrowEvent_0neineb",
+        "Task_002ndsu",
+        "Task_1ne4gpy",
+        "EndEvent_1vkzo14"
+    ],
+    "nameN": {
+        "Task_1q91vog": "Pay Travel",
+        "EndEvent_17rlcaz": "Offer Aborted",
+        "IntermediateThrowEvent_0neineb": "Payment Received",
+        "IntermediateThrowEvent_12d113r": "Ticket Received",
+        "ExclusiveGateway_192ovii": "is the offer interesting?",
+        "StartEvent_1": "Offer Management",
+        "StartEvent_1f3jj6d": "Offer Needed",
+        "SubProcess_1agd6n3": "ExchangeSP",
+        "EndEvent_0u6deep": "Booking Confirmed",
+        "Task_07u875a": "Check Travel Offer",
+        "Task_1bn6n5q": "Make Travel Offer",
+        "EndEvent_055yt9k": "Transaction Completed",
+        "EndEvent_10gqkzy": "Offer Completed",
+        "Task_002ndsu": "Confirm Booking",
+        "Task_1ne4gpy": "Order Ticket",
+        "EndEvent_0syu44v": "Transaction Aborted",
+        "IntermediateThrowEvent_0xjpikb": "Booking Received",
+        "Task_1v9s881": "Book Travel"
+    }
+}
\ No newline at end of file
diff --git a/models/bpmn-origin/json_from_bpmn/e039TravelAgency.json b/models/bpmn-origin/json_from_bpmn/e039TravelAgency.json
new file mode 100644
index 0000000..aa0a44e
--- /dev/null
+++ b/models/bpmn-origin/json_from_bpmn/e039TravelAgency.json
@@ -0,0 +1,241 @@
+{
+    "catN": {
+        "Task_1q91vog": {
+            "tag": "SendTask"
+        },
+        "IntermediateThrowEvent_0neineb": {
+            "tag": "CatchMessageIntermediateEvent"
+        },
+        "ExclusiveGateway_0i09ijx": {
+            "tag": "XorGateway"
+        },
+        "IntermediateThrowEvent_12d113r": {
+            "tag": "CatchMessageIntermediateEvent"
+        },
+        "StartEvent_1": {
+            "tag": "NoneStartEvent"
+        },
+        "StartEvent_1f3jj6d": {
+            "tag": "NoneStartEvent"
+        },
+        "ExclusiveGateway_1dc5v3z": {
+            "tag": "XorGateway"
+        },
+        "TravelAgency_": {
+            "tag": "Process"
+        },
+        "EndEvent_0u6deep": {
+            "tag": "CatchMessageIntermediateEvent"
+        },
+        "Task_07u875a": {
+            "tag": "ReceiveTask"
+        },
+        "Task_1bn6n5q": {
+            "tag": "SendTask"
+        },
+        "EndEvent_055yt9k": {
+            "tag": "NoneEndEvent"
+        },
+        "EndEvent_10gqkzy": {
+            "tag": "TerminateEndEvent"
+        },
+        "Customer_": {
+            "tag": "Process"
+        },
+        "Task_002ndsu": {
+            "tag": "SendTask"
+        },
+        "Task_1ne4gpy": {
+            "tag": "SendTask"
+        },
+        "IntermediateThrowEvent_0xjpikb": {
+            "tag": "CatchMessageIntermediateEvent"
+        },
+        "Task_1v9s881": {
+            "tag": "SendTask"
+        }
+    },
+    "catE": {
+        "SequenceFlow_1h5h7h5": "NormalSequenceFlow",
+        "SequenceFlow_0rfye55": "DefaultSequenceFlow",
+        "SequenceFlow_1rlj8av": "NormalSequenceFlow",
+        "SequenceFlow_1qtcxep": "NormalSequenceFlow",
+        "SequenceFlow_13z4ilm": "ConditionalSequenceFlow",
+        "SequenceFlow_0ljbxox": "NormalSequenceFlow",
+        "SequenceFlow_0n80biv": "NormalSequenceFlow",
+        "SequenceFlow_0mdvaai": "NormalSequenceFlow",
+        "SequenceFlow_11rxzkm": "NormalSequenceFlow",
+        "MessageFlow_1m551dh": "MessageFlow",
+        "SequenceFlow_1njgdzy": "NormalSequenceFlow",
+        "MessageFlow_1yfhhru": "MessageFlow",
+        "MessageFlow_04an7oz": "MessageFlow",
+        "SequenceFlow_0b34324": "NormalSequenceFlow",
+        "SequenceFlow_1qku5do": "NormalSequenceFlow",
+        "MessageFlow_1goz1mt": "MessageFlow",
+        "MessageFlow_0knd10s": "MessageFlow",
+        "SequenceFlow_1dptcxp": "NormalSequenceFlow",
+        "SequenceFlow_1fn4lqy": "NormalSequenceFlow",
+        "SequenceFlow_00s838q": "NormalSequenceFlow"
+    },
+    "containN": {
+        "TravelAgency_": [
+            "StartEvent_1f3jj6d",
+            "ExclusiveGateway_1dc5v3z",
+            "Task_1bn6n5q",
+            "IntermediateThrowEvent_0xjpikb",
+            "EndEvent_10gqkzy",
+            "Task_1ne4gpy",
+            "Task_002ndsu",
+            "IntermediateThrowEvent_0neineb",
+            "ExclusiveGateway_0i09ijx"
+        ],
+        "Customer_": [
+            "Task_1v9s881",
+            "StartEvent_1",
+            "Task_07u875a",
+            "EndEvent_055yt9k",
+            "EndEvent_0u6deep",
+            "IntermediateThrowEvent_12d113r",
+            "Task_1q91vog"
+        ]
+    },
+    "messageE": {
+        "MessageFlow_1m551dh": "Confirmation",
+        "MessageFlow_1yfhhru": "Travel",
+        "MessageFlow_04an7oz": "Ticket",
+        "MessageFlow_1goz1mt": "Payment",
+        "MessageFlow_0knd10s": "Offer"
+    },
+    "targetE": {
+        "SequenceFlow_1h5h7h5": "IntermediateThrowEvent_12d113r",
+        "SequenceFlow_0rfye55": "IntermediateThrowEvent_0xjpikb",
+        "SequenceFlow_1rlj8av": "IntermediateThrowEvent_0neineb",
+        "SequenceFlow_1qtcxep": "Task_07u875a",
+        "SequenceFlow_13z4ilm": "ExclusiveGateway_1dc5v3z",
+        "SequenceFlow_0ljbxox": "EndEvent_0u6deep",
+        "SequenceFlow_0n80biv": "Task_002ndsu",
+        "SequenceFlow_0mdvaai": "ExclusiveGateway_0i09ijx",
+        "SequenceFlow_11rxzkm": "EndEvent_10gqkzy",
+        "MessageFlow_1m551dh": "EndEvent_0u6deep",
+        "SequenceFlow_1njgdzy": "Task_1v9s881",
+        "MessageFlow_1yfhhru": "IntermediateThrowEvent_0xjpikb",
+        "MessageFlow_04an7oz": "IntermediateThrowEvent_12d113r",
+        "SequenceFlow_0b34324": "Task_1bn6n5q",
+        "SequenceFlow_1qku5do": "EndEvent_055yt9k",
+        "MessageFlow_1goz1mt": "IntermediateThrowEvent_0neineb",
+        "MessageFlow_0knd10s": "Task_07u875a",
+        "SequenceFlow_1dptcxp": "Task_1q91vog",
+        "SequenceFlow_1fn4lqy": "ExclusiveGateway_1dc5v3z",
+        "SequenceFlow_00s838q": "Task_1ne4gpy"
+    },
+    "name": "e039TravelAgency",
+    "attached": {},
+    "containE": {
+        "TravelAgency_": [
+            "SequenceFlow_11rxzkm",
+            "SequenceFlow_00s838q",
+            "SequenceFlow_0n80biv",
+            "SequenceFlow_1rlj8av",
+            "SequenceFlow_0rfye55",
+            "SequenceFlow_13z4ilm",
+            "SequenceFlow_0mdvaai",
+            "SequenceFlow_0b34324",
+            "SequenceFlow_1fn4lqy"
+        ],
+        "Customer_": [
+            "SequenceFlow_1dptcxp",
+            "SequenceFlow_1h5h7h5",
+            "SequenceFlow_0ljbxox",
+            "SequenceFlow_1qku5do",
+            "SequenceFlow_1qtcxep",
+            "SequenceFlow_1njgdzy"
+        ]
+    },
+    "edges": [
+        "MessageFlow_0knd10s",
+        "MessageFlow_1yfhhru",
+        "MessageFlow_1m551dh",
+        "MessageFlow_1goz1mt",
+        "MessageFlow_04an7oz",
+        "SequenceFlow_1dptcxp",
+        "SequenceFlow_1h5h7h5",
+        "SequenceFlow_0ljbxox",
+        "SequenceFlow_1qku5do",
+        "SequenceFlow_1qtcxep",
+        "SequenceFlow_1njgdzy",
+        "SequenceFlow_11rxzkm",
+        "SequenceFlow_00s838q",
+        "SequenceFlow_0n80biv",
+        "SequenceFlow_1rlj8av",
+        "SequenceFlow_0rfye55",
+        "SequenceFlow_13z4ilm",
+        "SequenceFlow_0mdvaai",
+        "SequenceFlow_0b34324",
+        "SequenceFlow_1fn4lqy"
+    ],
+    "messages": [
+        "Offer",
+        "Travel",
+        "Confirmation",
+        "Payment",
+        "Ticket"
+    ],
+    "sourceE": {
+        "SequenceFlow_1h5h7h5": "Task_1q91vog",
+        "SequenceFlow_0rfye55": "ExclusiveGateway_0i09ijx",
+        "SequenceFlow_1rlj8av": "IntermediateThrowEvent_0xjpikb",
+        "SequenceFlow_1qtcxep": "StartEvent_1",
+        "SequenceFlow_13z4ilm": "ExclusiveGateway_0i09ijx",
+        "SequenceFlow_0ljbxox": "IntermediateThrowEvent_12d113r",
+        "SequenceFlow_0n80biv": "IntermediateThrowEvent_0neineb",
+        "SequenceFlow_0mdvaai": "Task_1bn6n5q",
+        "SequenceFlow_11rxzkm": "Task_1ne4gpy",
+        "MessageFlow_1m551dh": "Task_002ndsu",
+        "SequenceFlow_1njgdzy": "Task_07u875a",
+        "MessageFlow_1yfhhru": "Task_1v9s881",
+        "MessageFlow_04an7oz": "Task_1ne4gpy",
+        "SequenceFlow_0b34324": "ExclusiveGateway_1dc5v3z",
+        "SequenceFlow_1qku5do": "EndEvent_0u6deep",
+        "MessageFlow_1goz1mt": "Task_1q91vog",
+        "MessageFlow_0knd10s": "Task_1bn6n5q",
+        "SequenceFlow_1dptcxp": "Task_1v9s881",
+        "SequenceFlow_1fn4lqy": "StartEvent_1f3jj6d",
+        "SequenceFlow_00s838q": "Task_002ndsu"
+    },
+    "nodes": [
+        "Customer_",
+        "TravelAgency_",
+        "Task_1v9s881",
+        "StartEvent_1",
+        "Task_07u875a",
+        "EndEvent_055yt9k",
+        "EndEvent_0u6deep",
+        "IntermediateThrowEvent_12d113r",
+        "Task_1q91vog",
+        "StartEvent_1f3jj6d",
+        "ExclusiveGateway_1dc5v3z",
+        "Task_1bn6n5q",
+        "IntermediateThrowEvent_0xjpikb",
+        "EndEvent_10gqkzy",
+        "Task_1ne4gpy",
+        "Task_002ndsu",
+        "IntermediateThrowEvent_0neineb",
+        "ExclusiveGateway_0i09ijx"
+    ],
+    "nameN": {
+        "Task_1q91vog": "Pay Travel",
+        "IntermediateThrowEvent_0neineb": "Payment Received",
+        "IntermediateThrowEvent_12d113r": "Ticket Received",
+        "StartEvent_1": "Offer Management",
+        "StartEvent_1f3jj6d": "Offer Needed",
+        "EndEvent_0u6deep": "Booking Confirmed",
+        "Task_07u875a": "Check Travel Offer",
+        "Task_1bn6n5q": "Make Travel Offer",
+        "EndEvent_055yt9k": "Transaction Completed",
+        "EndEvent_10gqkzy": "Offer Completed",
+        "Task_002ndsu": "Confirm Booking",
+        "Task_1ne4gpy": "Order Ticket",
+        "IntermediateThrowEvent_0xjpikb": "Booking Received",
+        "Task_1v9s881": "Book Travel"
+    }
+}
\ No newline at end of file
diff --git a/models/bpmn-origin/png/e020InternshipProcedure.png b/models/bpmn-origin/png/e020InternshipProcedure.png
index c87d44f..d5fe22f 100644
Binary files a/models/bpmn-origin/png/e020InternshipProcedure.png and b/models/bpmn-origin/png/e020InternshipProcedure.png differ
diff --git a/models/bpmn-origin/png/e038TravelAgency.png b/models/bpmn-origin/png/e038TravelAgency.png
new file mode 100644
index 0000000..1662e10
Binary files /dev/null and b/models/bpmn-origin/png/e038TravelAgency.png differ
diff --git a/models/bpmn-origin/png/e039TravelAgency.png b/models/bpmn-origin/png/e039TravelAgency.png
new file mode 100644
index 0000000..a3dbf94
Binary files /dev/null and b/models/bpmn-origin/png/e039TravelAgency.png differ
diff --git a/models/bpmn-origin/src/e038TravelAgency.bpmn b/models/bpmn-origin/src/e038TravelAgency.bpmn
new file mode 100644
index 0000000..cca1a4e
--- /dev/null
+++ b/models/bpmn-origin/src/e038TravelAgency.bpmn
@@ -0,0 +1,449 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<bpmn:definitions xmlns:bpmn="http://www.omg.org/spec/BPMN/20100524/MODEL" xmlns:bpmndi="http://www.omg.org/spec/BPMN/20100524/DI" xmlns:di="http://www.omg.org/spec/DD/20100524/DI" xmlns:dc="http://www.omg.org/spec/DD/20100524/DC" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" id="Definitions_00sp5ic" targetNamespace="http://bpmn.io/schema/bpmn" exporter="Camunda Modeler" exporterVersion="3.0.1">
+  <bpmn:collaboration id="e038TravelAgency">
+    <bpmn:documentation>modified from "A Classification of BPMN Collaborations based on Safeness and Soundness Notions", EXPRESS/SOS 2018.</bpmn:documentation>
+    <bpmn:participant id="Customer" name="Customer" processRef="Customer_" />
+    <bpmn:participant id="TravelAgency" name="Travel Agency" processRef="TravelAgency_" />
+    <bpmn:messageFlow id="MessageFlow_0knd10s" name="Offer" sourceRef="Task_1bn6n5q" targetRef="Task_07u875a" />
+    <bpmn:messageFlow id="MessageFlow_1yfhhru" name="Travel" sourceRef="Task_1v9s881" targetRef="IntermediateThrowEvent_0xjpikb" />
+    <bpmn:messageFlow id="MessageFlow_1m551dh" name="Confirmation" sourceRef="Task_002ndsu" targetRef="EndEvent_0u6deep" />
+    <bpmn:messageFlow id="MessageFlow_1goz1mt" name="Payment" sourceRef="Task_1q91vog" targetRef="IntermediateThrowEvent_0neineb" />
+    <bpmn:messageFlow id="MessageFlow_04an7oz" name="Ticket" sourceRef="Task_1ne4gpy" targetRef="IntermediateThrowEvent_12d113r" />
+    <bpmn:messageFlow id="MessageFlow_0joml9p" name="NoMore" sourceRef="IntermediateThrowEvent_0b4rm53" targetRef="BoundaryEvent_0qlhw6m" />
+    <bpmn:messageFlow id="MessageFlow_18qwt5e" name="Abort" sourceRef="IntermediateThrowEvent_02q48nh" targetRef="BoundaryEvent_19y0yk9" />
+  </bpmn:collaboration>
+  <bpmn:process id="Customer_" name="Customer" isExecutable="true">
+    <bpmn:sequenceFlow id="SequenceFlow_1uwq0b6" name="yes" sourceRef="ExclusiveGateway_192ovii" targetRef="Task_1v9s881">
+      <bpmn:conditionExpression xsi:type="bpmn:tFormalExpression">cond</bpmn:conditionExpression>
+    </bpmn:sequenceFlow>
+    <bpmn:sequenceFlow id="SequenceFlow_0b6ku63" name="no" sourceRef="ExclusiveGateway_192ovii" targetRef="ExclusiveGateway_0wgdt1i" />
+    <bpmn:sequenceFlow id="SequenceFlow_0sfyd5z" sourceRef="Task_07u875a" targetRef="ExclusiveGateway_192ovii" />
+    <bpmn:sequenceFlow id="SequenceFlow_016h32p" sourceRef="ExclusiveGateway_0wgdt1i" targetRef="Task_07u875a" />
+    <bpmn:sequenceFlow id="SequenceFlow_1rma3l8" sourceRef="StartEvent_1" targetRef="ExclusiveGateway_0wgdt1i" />
+    <bpmn:sendTask id="Task_1v9s881" name="Book Travel">
+      <bpmn:incoming>SequenceFlow_1uwq0b6</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_1dptcxp</bpmn:outgoing>
+    </bpmn:sendTask>
+    <bpmn:exclusiveGateway id="ExclusiveGateway_192ovii" name="is the offer interesting?" default="SequenceFlow_0b6ku63">
+      <bpmn:incoming>SequenceFlow_0sfyd5z</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_0b6ku63</bpmn:outgoing>
+      <bpmn:outgoing>SequenceFlow_1uwq0b6</bpmn:outgoing>
+    </bpmn:exclusiveGateway>
+    <bpmn:exclusiveGateway id="ExclusiveGateway_0wgdt1i">
+      <bpmn:incoming>SequenceFlow_1rma3l8</bpmn:incoming>
+      <bpmn:incoming>SequenceFlow_0b6ku63</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_016h32p</bpmn:outgoing>
+    </bpmn:exclusiveGateway>
+    <bpmn:startEvent id="StartEvent_1" name="Offer Management">
+      <bpmn:outgoing>SequenceFlow_1rma3l8</bpmn:outgoing>
+    </bpmn:startEvent>
+    <bpmn:receiveTask id="Task_07u875a" name="Check Travel Offer">
+      <bpmn:incoming>SequenceFlow_016h32p</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_0sfyd5z</bpmn:outgoing>
+    </bpmn:receiveTask>
+    <bpmn:endEvent id="EndEvent_055yt9k" name="Transaction Completed">
+      <bpmn:incoming>SequenceFlow_1qku5do</bpmn:incoming>
+    </bpmn:endEvent>
+    <bpmn:intermediateCatchEvent id="EndEvent_0u6deep" name="Booking Confirmed">
+      <bpmn:incoming>SequenceFlow_0ljbxox</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_1qku5do</bpmn:outgoing>
+      <bpmn:messageEventDefinition />
+    </bpmn:intermediateCatchEvent>
+    <bpmn:intermediateCatchEvent id="IntermediateThrowEvent_12d113r" name="Ticket Received">
+      <bpmn:incoming>SequenceFlow_1h5h7h5</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_0ljbxox</bpmn:outgoing>
+      <bpmn:messageEventDefinition />
+    </bpmn:intermediateCatchEvent>
+    <bpmn:sequenceFlow id="SequenceFlow_1dptcxp" sourceRef="Task_1v9s881" targetRef="Task_1q91vog" />
+    <bpmn:sequenceFlow id="SequenceFlow_1h5h7h5" sourceRef="Task_1q91vog" targetRef="IntermediateThrowEvent_12d113r" />
+    <bpmn:sequenceFlow id="SequenceFlow_0ljbxox" sourceRef="IntermediateThrowEvent_12d113r" targetRef="EndEvent_0u6deep" />
+    <bpmn:sequenceFlow id="SequenceFlow_1qku5do" sourceRef="EndEvent_0u6deep" targetRef="EndEvent_055yt9k" />
+    <bpmn:sendTask id="Task_1q91vog" name="Pay Travel">
+      <bpmn:incoming>SequenceFlow_1dptcxp</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_1h5h7h5</bpmn:outgoing>
+    </bpmn:sendTask>
+    <bpmn:boundaryEvent id="BoundaryEvent_0qlhw6m" attachedToRef="Task_07u875a">
+      <bpmn:outgoing>SequenceFlow_1pk6qce</bpmn:outgoing>
+      <bpmn:messageEventDefinition />
+    </bpmn:boundaryEvent>
+    <bpmn:sequenceFlow id="SequenceFlow_1pk6qce" sourceRef="BoundaryEvent_0qlhw6m" targetRef="IntermediateThrowEvent_02q48nh" />
+    <bpmn:endEvent id="EndEvent_0syu44v" name="Transaction Aborted">
+      <bpmn:incoming>SequenceFlow_0ybs6n8</bpmn:incoming>
+    </bpmn:endEvent>
+    <bpmn:sequenceFlow id="SequenceFlow_0ybs6n8" sourceRef="IntermediateThrowEvent_02q48nh" targetRef="EndEvent_0syu44v" />
+    <bpmn:intermediateThrowEvent id="IntermediateThrowEvent_02q48nh">
+      <bpmn:incoming>SequenceFlow_1pk6qce</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_0ybs6n8</bpmn:outgoing>
+      <bpmn:messageEventDefinition />
+    </bpmn:intermediateThrowEvent>
+  </bpmn:process>
+  <bpmn:process id="TravelAgency_" name="TravelAgency" isExecutable="false">
+    <bpmn:startEvent id="StartEvent_1f3jj6d" name="Offer Needed">
+      <bpmn:outgoing>SequenceFlow_1fn4lqy</bpmn:outgoing>
+    </bpmn:startEvent>
+    <bpmn:exclusiveGateway id="ExclusiveGateway_1dc5v3z">
+      <bpmn:incoming>SequenceFlow_1fn4lqy</bpmn:incoming>
+      <bpmn:incoming>SequenceFlow_13z4ilm</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_0b34324</bpmn:outgoing>
+    </bpmn:exclusiveGateway>
+    <bpmn:sendTask id="Task_1bn6n5q" name="Make Travel Offer">
+      <bpmn:incoming>SequenceFlow_0b34324</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_0mdvaai</bpmn:outgoing>
+    </bpmn:sendTask>
+    <bpmn:exclusiveGateway id="ExclusiveGateway_0i09ijx" default="SequenceFlow_0rfye55">
+      <bpmn:incoming>SequenceFlow_0mdvaai</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_0rfye55</bpmn:outgoing>
+      <bpmn:outgoing>SequenceFlow_13z4ilm</bpmn:outgoing>
+    </bpmn:exclusiveGateway>
+    <bpmn:sequenceFlow id="SequenceFlow_1fn4lqy" sourceRef="StartEvent_1f3jj6d" targetRef="ExclusiveGateway_1dc5v3z" />
+    <bpmn:sequenceFlow id="SequenceFlow_0b34324" sourceRef="ExclusiveGateway_1dc5v3z" targetRef="Task_1bn6n5q" />
+    <bpmn:sequenceFlow id="SequenceFlow_0mdvaai" sourceRef="Task_1bn6n5q" targetRef="ExclusiveGateway_0i09ijx" />
+    <bpmn:sequenceFlow id="SequenceFlow_13z4ilm" name="more offers" sourceRef="ExclusiveGateway_0i09ijx" targetRef="ExclusiveGateway_1dc5v3z">
+      <bpmn:conditionExpression xsi:type="bpmn:tFormalExpression">cond2</bpmn:conditionExpression>
+    </bpmn:sequenceFlow>
+    <bpmn:sequenceFlow id="SequenceFlow_0rfye55" sourceRef="ExclusiveGateway_0i09ijx" targetRef="IntermediateThrowEvent_0b4rm53" />
+    <bpmn:sequenceFlow id="SequenceFlow_0yhi6sc" sourceRef="IntermediateThrowEvent_0b4rm53" targetRef="SubProcess_1agd6n3" />
+    <bpmn:subProcess id="SubProcess_1agd6n3" name="ExchangeSP">
+      <bpmn:incoming>SequenceFlow_0yhi6sc</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_1yvkisw</bpmn:outgoing>
+      <bpmn:startEvent id="StartEvent_0qomvov">
+        <bpmn:outgoing>SequenceFlow_17r8ru7</bpmn:outgoing>
+      </bpmn:startEvent>
+      <bpmn:intermediateCatchEvent id="IntermediateThrowEvent_0xjpikb" name="Booking Received">
+        <bpmn:incoming>SequenceFlow_17r8ru7</bpmn:incoming>
+        <bpmn:outgoing>SequenceFlow_1j6r6o5</bpmn:outgoing>
+        <bpmn:messageEventDefinition />
+      </bpmn:intermediateCatchEvent>
+      <bpmn:intermediateCatchEvent id="IntermediateThrowEvent_0neineb" name="Payment Received">
+        <bpmn:incoming>SequenceFlow_1j6r6o5</bpmn:incoming>
+        <bpmn:outgoing>SequenceFlow_0bejayl</bpmn:outgoing>
+        <bpmn:messageEventDefinition />
+      </bpmn:intermediateCatchEvent>
+      <bpmn:sendTask id="Task_002ndsu" name="Confirm Booking">
+        <bpmn:incoming>SequenceFlow_0bejayl</bpmn:incoming>
+        <bpmn:outgoing>SequenceFlow_0ot5p93</bpmn:outgoing>
+      </bpmn:sendTask>
+      <bpmn:sendTask id="Task_1ne4gpy" name="Order Ticket">
+        <bpmn:incoming>SequenceFlow_0ot5p93</bpmn:incoming>
+        <bpmn:outgoing>SequenceFlow_023db5j</bpmn:outgoing>
+      </bpmn:sendTask>
+      <bpmn:sequenceFlow id="SequenceFlow_17r8ru7" sourceRef="StartEvent_0qomvov" targetRef="IntermediateThrowEvent_0xjpikb" />
+      <bpmn:sequenceFlow id="SequenceFlow_1j6r6o5" sourceRef="IntermediateThrowEvent_0xjpikb" targetRef="IntermediateThrowEvent_0neineb" />
+      <bpmn:sequenceFlow id="SequenceFlow_0bejayl" sourceRef="IntermediateThrowEvent_0neineb" targetRef="Task_002ndsu" />
+      <bpmn:sequenceFlow id="SequenceFlow_0ot5p93" sourceRef="Task_002ndsu" targetRef="Task_1ne4gpy" />
+      <bpmn:endEvent id="EndEvent_1vkzo14">
+        <bpmn:incoming>SequenceFlow_023db5j</bpmn:incoming>
+      </bpmn:endEvent>
+      <bpmn:sequenceFlow id="SequenceFlow_023db5j" sourceRef="Task_1ne4gpy" targetRef="EndEvent_1vkzo14" />
+    </bpmn:subProcess>
+    <bpmn:sequenceFlow id="SequenceFlow_1yvkisw" sourceRef="SubProcess_1agd6n3" targetRef="EndEvent_10gqkzy" />
+    <bpmn:intermediateThrowEvent id="IntermediateThrowEvent_0b4rm53">
+      <bpmn:incoming>SequenceFlow_0rfye55</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_0yhi6sc</bpmn:outgoing>
+      <bpmn:messageEventDefinition />
+    </bpmn:intermediateThrowEvent>
+    <bpmn:endEvent id="EndEvent_10gqkzy" name="Offer Completed">
+      <bpmn:incoming>SequenceFlow_1yvkisw</bpmn:incoming>
+    </bpmn:endEvent>
+    <bpmn:boundaryEvent id="BoundaryEvent_19y0yk9" attachedToRef="SubProcess_1agd6n3">
+      <bpmn:outgoing>SequenceFlow_1oyuvjd</bpmn:outgoing>
+      <bpmn:messageEventDefinition />
+    </bpmn:boundaryEvent>
+    <bpmn:endEvent id="EndEvent_17rlcaz" name="Offer Aborted">
+      <bpmn:incoming>SequenceFlow_1oyuvjd</bpmn:incoming>
+    </bpmn:endEvent>
+    <bpmn:sequenceFlow id="SequenceFlow_1oyuvjd" sourceRef="BoundaryEvent_19y0yk9" targetRef="EndEvent_17rlcaz" />
+  </bpmn:process>
+  <bpmndi:BPMNDiagram id="BPMNDiagram_1">
+    <bpmndi:BPMNPlane id="BPMNPlane_1" bpmnElement="e038TravelAgency">
+      <bpmndi:BPMNShape id="Participant_1jwnza9_di" bpmnElement="Customer" isHorizontal="true">
+        <dc:Bounds x="112" y="59" width="1071" height="264" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="_BPMNShape_StartEvent_2" bpmnElement="StartEvent_1">
+        <dc:Bounds x="168" y="147" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="162" y="189" width="65" height="27" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="Participant_1g2dbh1_di" bpmnElement="TravelAgency" isHorizontal="true">
+        <dc:Bounds x="112" y="350" width="1177" height="489" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="ExclusiveGateway_0wgdt1i_di" bpmnElement="ExclusiveGateway_0wgdt1i" isMarkerVisible="true">
+        <dc:Bounds x="254" y="140" width="50" height="50" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="SequenceFlow_1rma3l8_di" bpmnElement="SequenceFlow_1rma3l8">
+        <di:waypoint x="204" y="165" />
+        <di:waypoint x="254" y="165" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_016h32p_di" bpmnElement="SequenceFlow_016h32p">
+        <di:waypoint x="304" y="165" />
+        <di:waypoint x="354" y="165" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="ExclusiveGateway_192ovii_di" bpmnElement="ExclusiveGateway_192ovii" isMarkerVisible="true">
+        <dc:Bounds x="504" y="140" width="50" height="50" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="501" y="197" width="57" height="27" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="SequenceFlow_0sfyd5z_di" bpmnElement="SequenceFlow_0sfyd5z">
+        <di:waypoint x="454" y="165" />
+        <di:waypoint x="504" y="165" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_0b6ku63_di" bpmnElement="SequenceFlow_0b6ku63">
+        <di:waypoint x="529" y="140" />
+        <di:waypoint x="529" y="97" />
+        <di:waypoint x="279" y="97" />
+        <di:waypoint x="279" y="140" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="398" y="79" width="13" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_1uwq0b6_di" bpmnElement="SequenceFlow_1uwq0b6">
+        <di:waypoint x="554" y="165" />
+        <di:waypoint x="604" y="165" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="570" y="147" width="18" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="SendTask_0krlihp_di" bpmnElement="Task_1v9s881">
+        <dc:Bounds x="604" y="125" width="100" height="80" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="IntermediateCatchEvent_0jedtds_di" bpmnElement="EndEvent_0u6deep">
+        <dc:Bounds x="1017" y="147" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="1009" y="110" width="51" height="27" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="SendTask_1adf2oi_di" bpmnElement="Task_1q91vog">
+        <dc:Bounds x="766" y="125" width="100" height="80" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="IntermediateCatchEvent_14mnh2k_di" bpmnElement="IntermediateThrowEvent_12d113r">
+        <dc:Bounds x="925" y="147" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="904" y="123" width="78" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="EndEvent_055yt9k_di" bpmnElement="EndEvent_055yt9k">
+        <dc:Bounds x="1101" y="147" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="1091" y="190" width="58" height="27" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="StartEvent_1f3jj6d_di" bpmnElement="StartEvent_1f3jj6d">
+        <dc:Bounds x="166" y="493" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="162" y="536" width="66" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="ExclusiveGateway_1dc5v3z_di" bpmnElement="ExclusiveGateway_1dc5v3z" isMarkerVisible="true">
+        <dc:Bounds x="252" y="486" width="50" height="50" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="SequenceFlow_1fn4lqy_di" bpmnElement="SequenceFlow_1fn4lqy">
+        <di:waypoint x="202" y="511" />
+        <di:waypoint x="252" y="511" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_0b34324_di" bpmnElement="SequenceFlow_0b34324">
+        <di:waypoint x="302" y="511" />
+        <di:waypoint x="352" y="511" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="SendTask_0bw2qnz_di" bpmnElement="Task_1bn6n5q">
+        <dc:Bounds x="352" y="471" width="100" height="80" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="ReceiveTask_19i23d3_di" bpmnElement="Task_07u875a">
+        <dc:Bounds x="354" y="125" width="100" height="80" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="MessageFlow_0knd10s_di" bpmnElement="MessageFlow_0knd10s">
+        <di:waypoint x="402" y="471" />
+        <di:waypoint x="402" y="205" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="368" y="293" width="25" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_0mdvaai_di" bpmnElement="SequenceFlow_0mdvaai">
+        <di:waypoint x="452" y="511" />
+        <di:waypoint x="502" y="511" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_13z4ilm_di" bpmnElement="SequenceFlow_13z4ilm">
+        <di:waypoint x="527" y="536" />
+        <di:waypoint x="527" y="583" />
+        <di:waypoint x="277" y="583" />
+        <di:waypoint x="277" y="536" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="374" y="565" width="56" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_0rfye55_di" bpmnElement="SequenceFlow_0rfye55">
+        <di:waypoint x="552" y="511" />
+        <di:waypoint x="585" y="511" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="IntermediateCatchEvent_19uqca7_di" bpmnElement="IntermediateThrowEvent_0xjpikb">
+        <dc:Bounds x="636" y="660" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="610" y="703" width="89" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="MessageFlow_1yfhhru_di" bpmnElement="MessageFlow_1yfhhru">
+        <di:waypoint x="654" y="205" />
+        <di:waypoint x="654" y="660" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="661" y="514" width="31" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="SendTask_113xqju_di" bpmnElement="Task_002ndsu">
+        <dc:Bounds x="793" y="638" width="100" height="80" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="MessageFlow_1m551dh_di" bpmnElement="MessageFlow_1m551dh">
+        <di:waypoint x="843" y="638" />
+        <di:waypoint x="843" y="254" />
+        <di:waypoint x="1035" y="254" />
+        <di:waypoint x="1035" y="183" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="1040" y="227" width="63" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="IntermediateCatchEvent_0vxu9if_di" bpmnElement="IntermediateThrowEvent_0neineb">
+        <dc:Bounds x="716" y="660" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="711" y="703" width="46" height="27" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="MessageFlow_1goz1mt_di" bpmnElement="MessageFlow_1goz1mt">
+        <di:waypoint x="800" y="205" />
+        <di:waypoint x="800" y="338" />
+        <di:waypoint x="734" y="338" />
+        <di:waypoint x="734" y="660" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="740" y="508" width="44" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="SendTask_0kg5r2e_di" bpmnElement="Task_1ne4gpy">
+        <dc:Bounds x="933" y="638" width="100" height="80" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="MessageFlow_04an7oz_di" bpmnElement="MessageFlow_04an7oz">
+        <di:waypoint x="943" y="638" />
+        <di:waypoint x="943" y="183" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="951" y="226" width="29" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_1dptcxp_di" bpmnElement="SequenceFlow_1dptcxp">
+        <di:waypoint x="704" y="165" />
+        <di:waypoint x="766" y="165" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_1h5h7h5_di" bpmnElement="SequenceFlow_1h5h7h5">
+        <di:waypoint x="866" y="165" />
+        <di:waypoint x="925" y="165" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_0ljbxox_di" bpmnElement="SequenceFlow_0ljbxox">
+        <di:waypoint x="961" y="165" />
+        <di:waypoint x="1017" y="165" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_1qku5do_di" bpmnElement="SequenceFlow_1qku5do">
+        <di:waypoint x="1053" y="165" />
+        <di:waypoint x="1101" y="165" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="ExclusiveGateway_03jcm8s_di" bpmnElement="ExclusiveGateway_0i09ijx" isMarkerVisible="true">
+        <dc:Bounds x="502" y="486" width="50" height="50" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="EndEvent_055pokc_di" bpmnElement="EndEvent_10gqkzy">
+        <dc:Bounds x="1202" y="660" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="1179" y="706" width="81" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="SequenceFlow_0yhi6sc_di" bpmnElement="SequenceFlow_0yhi6sc">
+        <di:waypoint x="603" y="529" />
+        <di:waypoint x="603" y="580" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="MessageFlow_0joml9p_di" bpmnElement="MessageFlow_0joml9p">
+        <di:waypoint x="603" y="493" />
+        <di:waypoint x="603" y="337" />
+        <di:waypoint x="431" y="337" />
+        <di:waypoint x="431" y="223" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="438" y="280" width="40" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="IntermediateThrowEvent_1oh51cc_di" bpmnElement="IntermediateThrowEvent_0b4rm53">
+        <dc:Bounds x="585" y="493" width="36" height="36" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="BoundaryEvent_0ovcx04_di" bpmnElement="BoundaryEvent_0qlhw6m">
+        <dc:Bounds x="413" y="187" width="36" height="36" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="SequenceFlow_1pk6qce_di" bpmnElement="SequenceFlow_1pk6qce">
+        <di:waypoint x="440" y="220" />
+        <di:waypoint x="470" y="270" />
+        <di:waypoint x="511" y="270" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="EndEvent_0syu44v_di" bpmnElement="EndEvent_0syu44v">
+        <dc:Bounds x="585" y="252" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="575" y="295" width="58" height="27" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="SequenceFlow_0ybs6n8_di" bpmnElement="SequenceFlow_0ybs6n8">
+        <di:waypoint x="547" y="270" />
+        <di:waypoint x="585" y="270" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="SubProcess_1agd6n3_di" bpmnElement="SubProcess_1agd6n3" isExpanded="true">
+        <dc:Bounds x="551" y="580" width="609" height="195" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="StartEvent_0qomvov_di" bpmnElement="StartEvent_0qomvov">
+        <dc:Bounds x="572" y="660" width="36" height="36" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="SequenceFlow_17r8ru7_di" bpmnElement="SequenceFlow_17r8ru7">
+        <di:waypoint x="608" y="678" />
+        <di:waypoint x="636" y="678" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_1j6r6o5_di" bpmnElement="SequenceFlow_1j6r6o5">
+        <di:waypoint x="672" y="678" />
+        <di:waypoint x="716" y="678" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_0bejayl_di" bpmnElement="SequenceFlow_0bejayl">
+        <di:waypoint x="752" y="678" />
+        <di:waypoint x="793" y="678" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_0ot5p93_di" bpmnElement="SequenceFlow_0ot5p93">
+        <di:waypoint x="893" y="678" />
+        <di:waypoint x="933" y="678" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="EndEvent_1vkzo14_di" bpmnElement="EndEvent_1vkzo14">
+        <dc:Bounds x="1088" y="660" width="36" height="36" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="SequenceFlow_023db5j_di" bpmnElement="SequenceFlow_023db5j">
+        <di:waypoint x="1033" y="678" />
+        <di:waypoint x="1088" y="678" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_1yvkisw_di" bpmnElement="SequenceFlow_1yvkisw">
+        <di:waypoint x="1160" y="678" />
+        <di:waypoint x="1202" y="678" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="BoundaryEvent_1sb27m5_di" bpmnElement="BoundaryEvent_19y0yk9">
+        <dc:Bounds x="1053" y="562" width="36" height="36" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="IntermediateThrowEvent_01tmgla_di" bpmnElement="IntermediateThrowEvent_02q48nh">
+        <dc:Bounds x="511" y="252" width="36" height="36" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="MessageFlow_18qwt5e_di" bpmnElement="MessageFlow_18qwt5e">
+        <di:waypoint x="529" y="288" />
+        <di:waypoint x="529" y="425" />
+        <di:waypoint x="1071" y="425" />
+        <di:waypoint x="1071" y="562" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="787" y="407" width="27" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="EndEvent_17rlcaz_di" bpmnElement="EndEvent_17rlcaz">
+        <dc:Bounds x="1202" y="509" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="1188" y="552" width="66" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="SequenceFlow_1oyuvjd_di" bpmnElement="SequenceFlow_1oyuvjd">
+        <di:waypoint x="1081" y="565" />
+        <di:waypoint x="1107" y="527" />
+        <di:waypoint x="1202" y="527" />
+      </bpmndi:BPMNEdge>
+    </bpmndi:BPMNPlane>
+  </bpmndi:BPMNDiagram>
+</bpmn:definitions>
diff --git a/models/bpmn-origin/src/e038TravelAgency.constraint b/models/bpmn-origin/src/e038TravelAgency.constraint
new file mode 100644
index 0000000..4d00c14
--- /dev/null
+++ b/models/bpmn-origin/src/e038TravelAgency.constraint
@@ -0,0 +1,4 @@
+CONSTANT ConstraintNode <- TRUE
+         ConstraintEdge <- MaxMessageEdgeMarking2
+         Constraint <- ConstraintNodeEdge
+
diff --git a/models/bpmn-origin/src/e039TravelAgency.bpmn b/models/bpmn-origin/src/e039TravelAgency.bpmn
new file mode 100644
index 0000000..9bd6298
--- /dev/null
+++ b/models/bpmn-origin/src/e039TravelAgency.bpmn
@@ -0,0 +1,285 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<bpmn:definitions xmlns:bpmn="http://www.omg.org/spec/BPMN/20100524/MODEL" xmlns:bpmndi="http://www.omg.org/spec/BPMN/20100524/DI" xmlns:di="http://www.omg.org/spec/DD/20100524/DI" xmlns:dc="http://www.omg.org/spec/DD/20100524/DC" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" id="Definitions_00sp5ic" targetNamespace="http://bpmn.io/schema/bpmn" exporter="Camunda Modeler" exporterVersion="3.0.1">
+  <bpmn:collaboration id="e039TravelAgency">
+    <bpmn:documentation>modified from "A Classification of BPMN Collaborations based on Safeness and Soundness Notions", EXPRESS/SOS 2018.</bpmn:documentation>
+    <bpmn:participant id="Customer" name="Customer" processRef="Customer_" />
+    <bpmn:participant id="TravelAgency" name="Travel Agency" processRef="TravelAgency_" />
+    <bpmn:messageFlow id="MessageFlow_0knd10s" name="Offer" sourceRef="Task_1bn6n5q" targetRef="Task_07u875a" />
+    <bpmn:messageFlow id="MessageFlow_1yfhhru" name="Travel" sourceRef="Task_1v9s881" targetRef="IntermediateThrowEvent_0xjpikb" />
+    <bpmn:messageFlow id="MessageFlow_1m551dh" name="Confirmation" sourceRef="Task_002ndsu" targetRef="EndEvent_0u6deep" />
+    <bpmn:messageFlow id="MessageFlow_1goz1mt" name="Payment" sourceRef="Task_1q91vog" targetRef="IntermediateThrowEvent_0neineb" />
+    <bpmn:messageFlow id="MessageFlow_04an7oz" name="Ticket" sourceRef="Task_1ne4gpy" targetRef="IntermediateThrowEvent_12d113r" />
+  </bpmn:collaboration>
+  <bpmn:process id="Customer_" name="Customer" isExecutable="true">
+    <bpmn:sendTask id="Task_1v9s881" name="Book Travel">
+      <bpmn:incoming>SequenceFlow_1njgdzy</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_1dptcxp</bpmn:outgoing>
+    </bpmn:sendTask>
+    <bpmn:startEvent id="StartEvent_1" name="Offer Management">
+      <bpmn:outgoing>SequenceFlow_1qtcxep</bpmn:outgoing>
+    </bpmn:startEvent>
+    <bpmn:receiveTask id="Task_07u875a" name="Check Travel Offer">
+      <bpmn:incoming>SequenceFlow_1qtcxep</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_1njgdzy</bpmn:outgoing>
+    </bpmn:receiveTask>
+    <bpmn:endEvent id="EndEvent_055yt9k" name="Transaction Completed">
+      <bpmn:incoming>SequenceFlow_1qku5do</bpmn:incoming>
+    </bpmn:endEvent>
+    <bpmn:intermediateCatchEvent id="EndEvent_0u6deep" name="Booking Confirmed">
+      <bpmn:incoming>SequenceFlow_0ljbxox</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_1qku5do</bpmn:outgoing>
+      <bpmn:messageEventDefinition />
+    </bpmn:intermediateCatchEvent>
+    <bpmn:intermediateCatchEvent id="IntermediateThrowEvent_12d113r" name="Ticket Received">
+      <bpmn:incoming>SequenceFlow_1h5h7h5</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_0ljbxox</bpmn:outgoing>
+      <bpmn:messageEventDefinition />
+    </bpmn:intermediateCatchEvent>
+    <bpmn:sequenceFlow id="SequenceFlow_1dptcxp" sourceRef="Task_1v9s881" targetRef="Task_1q91vog" />
+    <bpmn:sequenceFlow id="SequenceFlow_1h5h7h5" sourceRef="Task_1q91vog" targetRef="IntermediateThrowEvent_12d113r" />
+    <bpmn:sequenceFlow id="SequenceFlow_0ljbxox" sourceRef="IntermediateThrowEvent_12d113r" targetRef="EndEvent_0u6deep" />
+    <bpmn:sequenceFlow id="SequenceFlow_1qku5do" sourceRef="EndEvent_0u6deep" targetRef="EndEvent_055yt9k" />
+    <bpmn:sendTask id="Task_1q91vog" name="Pay Travel">
+      <bpmn:incoming>SequenceFlow_1dptcxp</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_1h5h7h5</bpmn:outgoing>
+    </bpmn:sendTask>
+    <bpmn:sequenceFlow id="SequenceFlow_1qtcxep" sourceRef="StartEvent_1" targetRef="Task_07u875a" />
+    <bpmn:sequenceFlow id="SequenceFlow_1njgdzy" sourceRef="Task_07u875a" targetRef="Task_1v9s881" />
+  </bpmn:process>
+  <bpmn:process id="TravelAgency_" name="TravelAgency" isExecutable="false">
+    <bpmn:startEvent id="StartEvent_1f3jj6d" name="Offer Needed">
+      <bpmn:outgoing>SequenceFlow_1fn4lqy</bpmn:outgoing>
+    </bpmn:startEvent>
+    <bpmn:exclusiveGateway id="ExclusiveGateway_1dc5v3z">
+      <bpmn:incoming>SequenceFlow_1fn4lqy</bpmn:incoming>
+      <bpmn:incoming>SequenceFlow_13z4ilm</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_0b34324</bpmn:outgoing>
+    </bpmn:exclusiveGateway>
+    <bpmn:sendTask id="Task_1bn6n5q" name="Make Travel Offer">
+      <bpmn:incoming>SequenceFlow_0b34324</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_0mdvaai</bpmn:outgoing>
+    </bpmn:sendTask>
+    <bpmn:intermediateCatchEvent id="IntermediateThrowEvent_0xjpikb" name="Booking Received">
+      <bpmn:incoming>SequenceFlow_0rfye55</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_1rlj8av</bpmn:outgoing>
+      <bpmn:messageEventDefinition />
+    </bpmn:intermediateCatchEvent>
+    <bpmn:endEvent id="EndEvent_10gqkzy" name="Offer Completed">
+      <bpmn:incoming>SequenceFlow_11rxzkm</bpmn:incoming>
+      <bpmn:terminateEventDefinition />
+    </bpmn:endEvent>
+    <bpmn:sendTask id="Task_1ne4gpy" name="Order Ticket">
+      <bpmn:incoming>SequenceFlow_00s838q</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_11rxzkm</bpmn:outgoing>
+    </bpmn:sendTask>
+    <bpmn:sendTask id="Task_002ndsu" name="Confirm Booking">
+      <bpmn:incoming>SequenceFlow_0n80biv</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_00s838q</bpmn:outgoing>
+    </bpmn:sendTask>
+    <bpmn:intermediateCatchEvent id="IntermediateThrowEvent_0neineb" name="Payment Received">
+      <bpmn:incoming>SequenceFlow_1rlj8av</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_0n80biv</bpmn:outgoing>
+      <bpmn:messageEventDefinition />
+    </bpmn:intermediateCatchEvent>
+    <bpmn:sequenceFlow id="SequenceFlow_11rxzkm" sourceRef="Task_1ne4gpy" targetRef="EndEvent_10gqkzy" />
+    <bpmn:sequenceFlow id="SequenceFlow_00s838q" sourceRef="Task_002ndsu" targetRef="Task_1ne4gpy" />
+    <bpmn:sequenceFlow id="SequenceFlow_0n80biv" sourceRef="IntermediateThrowEvent_0neineb" targetRef="Task_002ndsu" />
+    <bpmn:sequenceFlow id="SequenceFlow_1rlj8av" sourceRef="IntermediateThrowEvent_0xjpikb" targetRef="IntermediateThrowEvent_0neineb" />
+    <bpmn:sequenceFlow id="SequenceFlow_0rfye55" sourceRef="ExclusiveGateway_0i09ijx" targetRef="IntermediateThrowEvent_0xjpikb" />
+    <bpmn:sequenceFlow id="SequenceFlow_13z4ilm" name="more offers" sourceRef="ExclusiveGateway_0i09ijx" targetRef="ExclusiveGateway_1dc5v3z">
+      <bpmn:conditionExpression xsi:type="bpmn:tFormalExpression">cond2</bpmn:conditionExpression>
+    </bpmn:sequenceFlow>
+    <bpmn:sequenceFlow id="SequenceFlow_0mdvaai" sourceRef="Task_1bn6n5q" targetRef="ExclusiveGateway_0i09ijx" />
+    <bpmn:sequenceFlow id="SequenceFlow_0b34324" sourceRef="ExclusiveGateway_1dc5v3z" targetRef="Task_1bn6n5q" />
+    <bpmn:sequenceFlow id="SequenceFlow_1fn4lqy" sourceRef="StartEvent_1f3jj6d" targetRef="ExclusiveGateway_1dc5v3z" />
+    <bpmn:exclusiveGateway id="ExclusiveGateway_0i09ijx" default="SequenceFlow_0rfye55">
+      <bpmn:incoming>SequenceFlow_0mdvaai</bpmn:incoming>
+      <bpmn:outgoing>SequenceFlow_0rfye55</bpmn:outgoing>
+      <bpmn:outgoing>SequenceFlow_13z4ilm</bpmn:outgoing>
+    </bpmn:exclusiveGateway>
+  </bpmn:process>
+  <bpmndi:BPMNDiagram id="BPMNDiagram_1">
+    <bpmndi:BPMNPlane id="BPMNPlane_1" bpmnElement="e039TravelAgency">
+      <bpmndi:BPMNShape id="Participant_1jwnza9_di" bpmnElement="Customer">
+        <dc:Bounds x="112" y="59" width="1072" height="185" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="_BPMNShape_StartEvent_2" bpmnElement="StartEvent_1">
+        <dc:Bounds x="168" y="147" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="162" y="189" width="65" height="27" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="Participant_1g2dbh1_di" bpmnElement="TravelAgency">
+        <dc:Bounds x="112" y="261" width="1075" height="156" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="SendTask_0krlihp_di" bpmnElement="Task_1v9s881">
+        <dc:Bounds x="604" y="125" width="100" height="80" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="IntermediateCatchEvent_0jedtds_di" bpmnElement="EndEvent_0u6deep">
+        <dc:Bounds x="1017" y="147" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="1009" y="110" width="51" height="27" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="SendTask_1adf2oi_di" bpmnElement="Task_1q91vog">
+        <dc:Bounds x="766" y="125" width="100" height="80" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="IntermediateCatchEvent_14mnh2k_di" bpmnElement="IntermediateThrowEvent_12d113r">
+        <dc:Bounds x="925" y="147" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="904" y="123" width="78" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="EndEvent_055yt9k_di" bpmnElement="EndEvent_055yt9k">
+        <dc:Bounds x="1101" y="147" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="1091" y="190" width="58" height="27" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="StartEvent_1f3jj6d_di" bpmnElement="StartEvent_1f3jj6d">
+        <dc:Bounds x="166" y="303" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="162" y="346" width="66" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="ExclusiveGateway_1dc5v3z_di" bpmnElement="ExclusiveGateway_1dc5v3z" isMarkerVisible="true">
+        <dc:Bounds x="252" y="296" width="50" height="50" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="SequenceFlow_1fn4lqy_di" bpmnElement="SequenceFlow_1fn4lqy">
+        <di:waypoint x="202" y="321" />
+        <di:waypoint x="252" y="321" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_0b34324_di" bpmnElement="SequenceFlow_0b34324">
+        <di:waypoint x="302" y="321" />
+        <di:waypoint x="352" y="321" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="SendTask_0bw2qnz_di" bpmnElement="Task_1bn6n5q">
+        <dc:Bounds x="352" y="281" width="100" height="80" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNShape id="ReceiveTask_19i23d3_di" bpmnElement="Task_07u875a">
+        <dc:Bounds x="354" y="125" width="100" height="80" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="MessageFlow_0knd10s_di" bpmnElement="MessageFlow_0knd10s">
+        <di:waypoint x="402" y="281" />
+        <di:waypoint x="402" y="205" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="410" y="226" width="25" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_0mdvaai_di" bpmnElement="SequenceFlow_0mdvaai">
+        <di:waypoint x="452" y="321" />
+        <di:waypoint x="502" y="321" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_13z4ilm_di" bpmnElement="SequenceFlow_13z4ilm">
+        <di:waypoint x="527" y="346" />
+        <di:waypoint x="527" y="393" />
+        <di:waypoint x="277" y="393" />
+        <di:waypoint x="277" y="346" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="375" y="375" width="56" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_0rfye55_di" bpmnElement="SequenceFlow_0rfye55">
+        <di:waypoint x="552" y="321" />
+        <di:waypoint x="636" y="321" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="IntermediateCatchEvent_19uqca7_di" bpmnElement="IntermediateThrowEvent_0xjpikb">
+        <dc:Bounds x="636" y="303" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="610" y="346" width="89" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="MessageFlow_1yfhhru_di" bpmnElement="MessageFlow_1yfhhru">
+        <di:waypoint x="654" y="205" />
+        <di:waypoint x="654" y="303" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="661" y="266" width="31" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="SendTask_113xqju_di" bpmnElement="Task_002ndsu">
+        <dc:Bounds x="806" y="281" width="100" height="80" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="MessageFlow_1m551dh_di" bpmnElement="MessageFlow_1m551dh">
+        <di:waypoint x="856" y="281" />
+        <di:waypoint x="856" y="254" />
+        <di:waypoint x="1035" y="254" />
+        <di:waypoint x="1035" y="183" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="1040" y="227" width="63" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="IntermediateCatchEvent_0vxu9if_di" bpmnElement="IntermediateThrowEvent_0neineb">
+        <dc:Bounds x="724" y="303" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="719" y="346" width="46" height="27" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="MessageFlow_1goz1mt_di" bpmnElement="MessageFlow_1goz1mt">
+        <di:waypoint x="815" y="205" />
+        <di:waypoint x="752" y="306" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="780" y="263" width="44" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="SendTask_0kg5r2e_di" bpmnElement="Task_1ne4gpy">
+        <dc:Bounds x="958" y="281" width="100" height="80" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="MessageFlow_04an7oz_di" bpmnElement="MessageFlow_04an7oz">
+        <di:waypoint x="1008" y="281" />
+        <di:waypoint x="952" y="180" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="945" y="229" width="29" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="EndEvent_0f7edvw_di" bpmnElement="EndEvent_10gqkzy">
+        <dc:Bounds x="1108" y="303" width="36" height="36" />
+        <bpmndi:BPMNLabel>
+          <dc:Bounds x="1086" y="346" width="81" height="14" />
+        </bpmndi:BPMNLabel>
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="SequenceFlow_1dptcxp_di" bpmnElement="SequenceFlow_1dptcxp">
+        <di:waypoint x="704" y="165" />
+        <di:waypoint x="766" y="165" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_1h5h7h5_di" bpmnElement="SequenceFlow_1h5h7h5">
+        <di:waypoint x="866" y="165" />
+        <di:waypoint x="925" y="165" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_0ljbxox_di" bpmnElement="SequenceFlow_0ljbxox">
+        <di:waypoint x="961" y="165" />
+        <di:waypoint x="1017" y="165" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_1qku5do_di" bpmnElement="SequenceFlow_1qku5do">
+        <di:waypoint x="1053" y="165" />
+        <di:waypoint x="1101" y="165" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_1rlj8av_di" bpmnElement="SequenceFlow_1rlj8av">
+        <di:waypoint x="672" y="321" />
+        <di:waypoint x="724" y="321" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_0n80biv_di" bpmnElement="SequenceFlow_0n80biv">
+        <di:waypoint x="760" y="321" />
+        <di:waypoint x="806" y="321" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_00s838q_di" bpmnElement="SequenceFlow_00s838q">
+        <di:waypoint x="906" y="321" />
+        <di:waypoint x="958" y="321" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_11rxzkm_di" bpmnElement="SequenceFlow_11rxzkm">
+        <di:waypoint x="1058" y="321" />
+        <di:waypoint x="1108" y="321" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNShape id="ExclusiveGateway_13iwbh2_di" bpmnElement="ExclusiveGateway_0i09ijx" isMarkerVisible="true">
+        <dc:Bounds x="502" y="296" width="50" height="50" />
+      </bpmndi:BPMNShape>
+      <bpmndi:BPMNEdge id="SequenceFlow_1qtcxep_di" bpmnElement="SequenceFlow_1qtcxep">
+        <di:waypoint x="204" y="165" />
+        <di:waypoint x="354" y="165" />
+      </bpmndi:BPMNEdge>
+      <bpmndi:BPMNEdge id="SequenceFlow_1njgdzy_di" bpmnElement="SequenceFlow_1njgdzy">
+        <di:waypoint x="454" y="165" />
+        <di:waypoint x="604" y="165" />
+      </bpmndi:BPMNEdge>
+    </bpmndi:BPMNPlane>
+  </bpmndi:BPMNDiagram>
+</bpmn:definitions>
diff --git a/models/bpmn-origin/src/e039TravelAgency.constraint b/models/bpmn-origin/src/e039TravelAgency.constraint
new file mode 100644
index 0000000..4d00c14
--- /dev/null
+++ b/models/bpmn-origin/src/e039TravelAgency.constraint
@@ -0,0 +1,4 @@
+CONSTANT ConstraintNode <- TRUE
+         ConstraintEdge <- MaxMessageEdgeMarking2
+         Constraint <- ConstraintNodeEdge
+
diff --git a/models/bpmn-origin/tla_from_bpmn/e038TravelAgency.tla b/models/bpmn-origin/tla_from_bpmn/e038TravelAgency.tla
new file mode 100644
index 0000000..c8d6636
--- /dev/null
+++ b/models/bpmn-origin/tla_from_bpmn/e038TravelAgency.tla
@@ -0,0 +1,184 @@
+---------------- MODULE e038TravelAgency ----------------
+
+EXTENDS TLC, PWSTypes
+
+VARIABLES nodemarks, edgemarks, net
+
+ContainRel ==
+  "Customer_" :> { "Task_1v9s881", "ExclusiveGateway_192ovii", "ExclusiveGateway_0wgdt1i", "StartEvent_1", "Task_07u875a", "EndEvent_055yt9k", "EndEvent_0u6deep", "IntermediateThrowEvent_12d113r", "Task_1q91vog", "BoundaryEvent_0qlhw6m", "EndEvent_0syu44v", "IntermediateThrowEvent_02q48nh" }
+  @@ "SubProcess_1agd6n3" :> { "StartEvent_0qomvov", "IntermediateThrowEvent_0xjpikb", "IntermediateThrowEvent_0neineb", "Task_002ndsu", "Task_1ne4gpy", "EndEvent_1vkzo14" }
+  @@ "TravelAgency_" :> { "StartEvent_1f3jj6d", "ExclusiveGateway_1dc5v3z", "Task_1bn6n5q", "ExclusiveGateway_0i09ijx", "SubProcess_1agd6n3", "IntermediateThrowEvent_0b4rm53", "EndEvent_10gqkzy", "BoundaryEvent_19y0yk9", "EndEvent_17rlcaz" }
+
+Node == {
+  "Customer_","TravelAgency_","Task_1v9s881","ExclusiveGateway_192ovii","ExclusiveGateway_0wgdt1i","StartEvent_1","Task_07u875a","EndEvent_055yt9k","EndEvent_0u6deep","IntermediateThrowEvent_12d113r","Task_1q91vog","BoundaryEvent_0qlhw6m","EndEvent_0syu44v","IntermediateThrowEvent_02q48nh","StartEvent_1f3jj6d","ExclusiveGateway_1dc5v3z","Task_1bn6n5q","ExclusiveGateway_0i09ijx","SubProcess_1agd6n3","IntermediateThrowEvent_0b4rm53","EndEvent_10gqkzy","BoundaryEvent_19y0yk9","EndEvent_17rlcaz","StartEvent_0qomvov","IntermediateThrowEvent_0xjpikb","IntermediateThrowEvent_0neineb","Task_002ndsu","Task_1ne4gpy","EndEvent_1vkzo14"
+}
+
+Edge == {
+  "MessageFlow_0knd10s","MessageFlow_1yfhhru","MessageFlow_1m551dh","MessageFlow_1goz1mt","MessageFlow_04an7oz","MessageFlow_0joml9p","MessageFlow_18qwt5e","SequenceFlow_1uwq0b6","SequenceFlow_0b6ku63","SequenceFlow_0sfyd5z","SequenceFlow_016h32p","SequenceFlow_1rma3l8","SequenceFlow_1dptcxp","SequenceFlow_1h5h7h5","SequenceFlow_0ljbxox","SequenceFlow_1qku5do","SequenceFlow_1pk6qce","SequenceFlow_0ybs6n8","SequenceFlow_1fn4lqy","SequenceFlow_0b34324","SequenceFlow_0mdvaai","SequenceFlow_13z4ilm","SequenceFlow_0rfye55","SequenceFlow_0yhi6sc","SequenceFlow_1yvkisw","SequenceFlow_1oyuvjd","SequenceFlow_17r8ru7","SequenceFlow_1j6r6o5","SequenceFlow_0bejayl","SequenceFlow_0ot5p93","SequenceFlow_023db5j"
+}
+
+Message == { "Offer", "Travel", "Confirmation", "Payment", "Ticket", "NoMore", "Abort" }
+
+msgtype ==
+      "MessageFlow_0knd10s" :> "Offer"
+  @@ "MessageFlow_1yfhhru" :> "Travel"
+  @@ "MessageFlow_1m551dh" :> "Confirmation"
+  @@ "MessageFlow_1goz1mt" :> "Payment"
+  @@ "MessageFlow_04an7oz" :> "Ticket"
+  @@ "MessageFlow_0joml9p" :> "NoMore"
+  @@ "MessageFlow_18qwt5e" :> "Abort"
+
+source ==
+   "MessageFlow_0knd10s" :> "Task_1bn6n5q"
+@@ "MessageFlow_1yfhhru" :> "Task_1v9s881"
+@@ "MessageFlow_1m551dh" :> "Task_002ndsu"
+@@ "MessageFlow_1goz1mt" :> "Task_1q91vog"
+@@ "MessageFlow_04an7oz" :> "Task_1ne4gpy"
+@@ "MessageFlow_0joml9p" :> "IntermediateThrowEvent_0b4rm53"
+@@ "MessageFlow_18qwt5e" :> "IntermediateThrowEvent_02q48nh"
+@@ "SequenceFlow_1uwq0b6" :> "ExclusiveGateway_192ovii"
+@@ "SequenceFlow_0b6ku63" :> "ExclusiveGateway_192ovii"
+@@ "SequenceFlow_0sfyd5z" :> "Task_07u875a"
+@@ "SequenceFlow_016h32p" :> "ExclusiveGateway_0wgdt1i"
+@@ "SequenceFlow_1rma3l8" :> "StartEvent_1"
+@@ "SequenceFlow_1dptcxp" :> "Task_1v9s881"
+@@ "SequenceFlow_1h5h7h5" :> "Task_1q91vog"
+@@ "SequenceFlow_0ljbxox" :> "IntermediateThrowEvent_12d113r"
+@@ "SequenceFlow_1qku5do" :> "EndEvent_0u6deep"
+@@ "SequenceFlow_1pk6qce" :> "BoundaryEvent_0qlhw6m"
+@@ "SequenceFlow_0ybs6n8" :> "IntermediateThrowEvent_02q48nh"
+@@ "SequenceFlow_1fn4lqy" :> "StartEvent_1f3jj6d"
+@@ "SequenceFlow_0b34324" :> "ExclusiveGateway_1dc5v3z"
+@@ "SequenceFlow_0mdvaai" :> "Task_1bn6n5q"
+@@ "SequenceFlow_13z4ilm" :> "ExclusiveGateway_0i09ijx"
+@@ "SequenceFlow_0rfye55" :> "ExclusiveGateway_0i09ijx"
+@@ "SequenceFlow_0yhi6sc" :> "IntermediateThrowEvent_0b4rm53"
+@@ "SequenceFlow_1yvkisw" :> "SubProcess_1agd6n3"
+@@ "SequenceFlow_1oyuvjd" :> "BoundaryEvent_19y0yk9"
+@@ "SequenceFlow_17r8ru7" :> "StartEvent_0qomvov"
+@@ "SequenceFlow_1j6r6o5" :> "IntermediateThrowEvent_0xjpikb"
+@@ "SequenceFlow_0bejayl" :> "IntermediateThrowEvent_0neineb"
+@@ "SequenceFlow_0ot5p93" :> "Task_002ndsu"
+@@ "SequenceFlow_023db5j" :> "Task_1ne4gpy"
+
+target ==
+   "MessageFlow_0knd10s" :> "Task_07u875a"
+@@ "MessageFlow_1yfhhru" :> "IntermediateThrowEvent_0xjpikb"
+@@ "MessageFlow_1m551dh" :> "EndEvent_0u6deep"
+@@ "MessageFlow_1goz1mt" :> "IntermediateThrowEvent_0neineb"
+@@ "MessageFlow_04an7oz" :> "IntermediateThrowEvent_12d113r"
+@@ "MessageFlow_0joml9p" :> "BoundaryEvent_0qlhw6m"
+@@ "MessageFlow_18qwt5e" :> "BoundaryEvent_19y0yk9"
+@@ "SequenceFlow_1uwq0b6" :> "Task_1v9s881"
+@@ "SequenceFlow_0b6ku63" :> "ExclusiveGateway_0wgdt1i"
+@@ "SequenceFlow_0sfyd5z" :> "ExclusiveGateway_192ovii"
+@@ "SequenceFlow_016h32p" :> "Task_07u875a"
+@@ "SequenceFlow_1rma3l8" :> "ExclusiveGateway_0wgdt1i"
+@@ "SequenceFlow_1dptcxp" :> "Task_1q91vog"
+@@ "SequenceFlow_1h5h7h5" :> "IntermediateThrowEvent_12d113r"
+@@ "SequenceFlow_0ljbxox" :> "EndEvent_0u6deep"
+@@ "SequenceFlow_1qku5do" :> "EndEvent_055yt9k"
+@@ "SequenceFlow_1pk6qce" :> "IntermediateThrowEvent_02q48nh"
+@@ "SequenceFlow_0ybs6n8" :> "EndEvent_0syu44v"
+@@ "SequenceFlow_1fn4lqy" :> "ExclusiveGateway_1dc5v3z"
+@@ "SequenceFlow_0b34324" :> "Task_1bn6n5q"
+@@ "SequenceFlow_0mdvaai" :> "ExclusiveGateway_0i09ijx"
+@@ "SequenceFlow_13z4ilm" :> "ExclusiveGateway_1dc5v3z"
+@@ "SequenceFlow_0rfye55" :> "IntermediateThrowEvent_0b4rm53"
+@@ "SequenceFlow_0yhi6sc" :> "SubProcess_1agd6n3"
+@@ "SequenceFlow_1yvkisw" :> "EndEvent_10gqkzy"
+@@ "SequenceFlow_1oyuvjd" :> "EndEvent_17rlcaz"
+@@ "SequenceFlow_17r8ru7" :> "IntermediateThrowEvent_0xjpikb"
+@@ "SequenceFlow_1j6r6o5" :> "IntermediateThrowEvent_0neineb"
+@@ "SequenceFlow_0bejayl" :> "Task_002ndsu"
+@@ "SequenceFlow_0ot5p93" :> "Task_1ne4gpy"
+@@ "SequenceFlow_023db5j" :> "EndEvent_1vkzo14"
+
+CatN ==
+   "Customer_" :> Process
+@@ "TravelAgency_" :> Process
+@@ "Task_1v9s881" :> SendTask
+@@ "ExclusiveGateway_192ovii" :> ExclusiveOr
+@@ "ExclusiveGateway_0wgdt1i" :> ExclusiveOr
+@@ "StartEvent_1" :> NoneStartEvent
+@@ "Task_07u875a" :> ReceiveTask
+@@ "EndEvent_055yt9k" :> NoneEndEvent
+@@ "EndEvent_0u6deep" :> CatchMessageIntermediateEvent
+@@ "IntermediateThrowEvent_12d113r" :> CatchMessageIntermediateEvent
+@@ "Task_1q91vog" :> SendTask
+@@ "BoundaryEvent_0qlhw6m" :> MessageBoundaryEvent
+@@ "EndEvent_0syu44v" :> NoneEndEvent
+@@ "IntermediateThrowEvent_02q48nh" :> ThrowMessageIntermediateEvent
+@@ "StartEvent_1f3jj6d" :> NoneStartEvent
+@@ "ExclusiveGateway_1dc5v3z" :> ExclusiveOr
+@@ "Task_1bn6n5q" :> SendTask
+@@ "ExclusiveGateway_0i09ijx" :> ExclusiveOr
+@@ "SubProcess_1agd6n3" :> SubProcess
+@@ "IntermediateThrowEvent_0b4rm53" :> ThrowMessageIntermediateEvent
+@@ "EndEvent_10gqkzy" :> NoneEndEvent
+@@ "BoundaryEvent_19y0yk9" :> MessageBoundaryEvent
+@@ "EndEvent_17rlcaz" :> NoneEndEvent
+@@ "StartEvent_0qomvov" :> NoneStartEvent
+@@ "IntermediateThrowEvent_0xjpikb" :> CatchMessageIntermediateEvent
+@@ "IntermediateThrowEvent_0neineb" :> CatchMessageIntermediateEvent
+@@ "Task_002ndsu" :> SendTask
+@@ "Task_1ne4gpy" :> SendTask
+@@ "EndEvent_1vkzo14" :> NoneEndEvent
+
+CatE ==
+   "MessageFlow_0knd10s" :> MessageFlow
+@@ "MessageFlow_1yfhhru" :> MessageFlow
+@@ "MessageFlow_1m551dh" :> MessageFlow
+@@ "MessageFlow_1goz1mt" :> MessageFlow
+@@ "MessageFlow_04an7oz" :> MessageFlow
+@@ "MessageFlow_0joml9p" :> MessageFlow
+@@ "MessageFlow_18qwt5e" :> MessageFlow
+@@ "SequenceFlow_1uwq0b6" :> ConditionalSeqFlow
+@@ "SequenceFlow_0b6ku63" :> DefaultSeqFlow
+@@ "SequenceFlow_0sfyd5z" :> NormalSeqFlow
+@@ "SequenceFlow_016h32p" :> NormalSeqFlow
+@@ "SequenceFlow_1rma3l8" :> NormalSeqFlow
+@@ "SequenceFlow_1dptcxp" :> NormalSeqFlow
+@@ "SequenceFlow_1h5h7h5" :> NormalSeqFlow
+@@ "SequenceFlow_0ljbxox" :> NormalSeqFlow
+@@ "SequenceFlow_1qku5do" :> NormalSeqFlow
+@@ "SequenceFlow_1pk6qce" :> NormalSeqFlow
+@@ "SequenceFlow_0ybs6n8" :> NormalSeqFlow
+@@ "SequenceFlow_1fn4lqy" :> NormalSeqFlow
+@@ "SequenceFlow_0b34324" :> NormalSeqFlow
+@@ "SequenceFlow_0mdvaai" :> NormalSeqFlow
+@@ "SequenceFlow_13z4ilm" :> ConditionalSeqFlow
+@@ "SequenceFlow_0rfye55" :> DefaultSeqFlow
+@@ "SequenceFlow_0yhi6sc" :> NormalSeqFlow
+@@ "SequenceFlow_1yvkisw" :> NormalSeqFlow
+@@ "SequenceFlow_1oyuvjd" :> NormalSeqFlow
+@@ "SequenceFlow_17r8ru7" :> NormalSeqFlow
+@@ "SequenceFlow_1j6r6o5" :> NormalSeqFlow
+@@ "SequenceFlow_0bejayl" :> NormalSeqFlow
+@@ "SequenceFlow_0ot5p93" :> NormalSeqFlow
+@@ "SequenceFlow_023db5j" :> NormalSeqFlow
+
+LOCAL preEdges ==
+  [ i \in {} |-> {}]
+PreEdges(n,e) == preEdges[n,e]
+
+PreNodes(n,e) == { target[ee] : ee \in preEdges[n,e] }
+          \union { nn \in { source[ee] : ee \in preEdges[n,e] } : CatN[nn] \in { NoneStartEvent, MessageStartEvent } }
+
+BoundaryEvent ==
+   "BoundaryEvent_0qlhw6m" :> [ attachedTo |-> "Task_07u875a", cancelActivity |-> TRUE ]
+@@ "BoundaryEvent_19y0yk9" :> [ attachedTo |-> "SubProcess_1agd6n3", cancelActivity |-> TRUE ]
+
+WF == INSTANCE PWSWellFormed
+ASSUME WF!WellTyped
+ASSUME WF!WellFormedness
+
+ConstraintNode == TRUE \* none
+ConstraintEdge == TRUE \* none
+Constraint == TRUE     \* none
+INSTANCE PWSConstraints
+
+INSTANCE PWSSemantics
+
+================================================================
+
diff --git a/models/bpmn-origin/tla_from_bpmn/e039TravelAgency.tla b/models/bpmn-origin/tla_from_bpmn/e039TravelAgency.tla
new file mode 100644
index 0000000..3b2c5e0
--- /dev/null
+++ b/models/bpmn-origin/tla_from_bpmn/e039TravelAgency.tla
@@ -0,0 +1,136 @@
+---------------- MODULE e039TravelAgency ----------------
+
+EXTENDS TLC, PWSTypes
+
+VARIABLES nodemarks, edgemarks, net
+
+ContainRel ==
+  "Customer_" :> { "Task_1v9s881", "StartEvent_1", "Task_07u875a", "EndEvent_055yt9k", "EndEvent_0u6deep", "IntermediateThrowEvent_12d113r", "Task_1q91vog" }
+  @@ "TravelAgency_" :> { "StartEvent_1f3jj6d", "ExclusiveGateway_1dc5v3z", "Task_1bn6n5q", "IntermediateThrowEvent_0xjpikb", "EndEvent_10gqkzy", "Task_1ne4gpy", "Task_002ndsu", "IntermediateThrowEvent_0neineb", "ExclusiveGateway_0i09ijx" }
+
+Node == {
+  "Customer_","TravelAgency_","Task_1v9s881","StartEvent_1","Task_07u875a","EndEvent_055yt9k","EndEvent_0u6deep","IntermediateThrowEvent_12d113r","Task_1q91vog","StartEvent_1f3jj6d","ExclusiveGateway_1dc5v3z","Task_1bn6n5q","IntermediateThrowEvent_0xjpikb","EndEvent_10gqkzy","Task_1ne4gpy","Task_002ndsu","IntermediateThrowEvent_0neineb","ExclusiveGateway_0i09ijx"
+}
+
+Edge == {
+  "MessageFlow_0knd10s","MessageFlow_1yfhhru","MessageFlow_1m551dh","MessageFlow_1goz1mt","MessageFlow_04an7oz","SequenceFlow_1dptcxp","SequenceFlow_1h5h7h5","SequenceFlow_0ljbxox","SequenceFlow_1qku5do","SequenceFlow_1qtcxep","SequenceFlow_1njgdzy","SequenceFlow_11rxzkm","SequenceFlow_00s838q","SequenceFlow_0n80biv","SequenceFlow_1rlj8av","SequenceFlow_0rfye55","SequenceFlow_13z4ilm","SequenceFlow_0mdvaai","SequenceFlow_0b34324","SequenceFlow_1fn4lqy"
+}
+
+Message == { "Offer", "Travel", "Confirmation", "Payment", "Ticket" }
+
+msgtype ==
+      "MessageFlow_0knd10s" :> "Offer"
+  @@ "MessageFlow_1yfhhru" :> "Travel"
+  @@ "MessageFlow_1m551dh" :> "Confirmation"
+  @@ "MessageFlow_1goz1mt" :> "Payment"
+  @@ "MessageFlow_04an7oz" :> "Ticket"
+
+source ==
+   "MessageFlow_0knd10s" :> "Task_1bn6n5q"
+@@ "MessageFlow_1yfhhru" :> "Task_1v9s881"
+@@ "MessageFlow_1m551dh" :> "Task_002ndsu"
+@@ "MessageFlow_1goz1mt" :> "Task_1q91vog"
+@@ "MessageFlow_04an7oz" :> "Task_1ne4gpy"
+@@ "SequenceFlow_1dptcxp" :> "Task_1v9s881"
+@@ "SequenceFlow_1h5h7h5" :> "Task_1q91vog"
+@@ "SequenceFlow_0ljbxox" :> "IntermediateThrowEvent_12d113r"
+@@ "SequenceFlow_1qku5do" :> "EndEvent_0u6deep"
+@@ "SequenceFlow_1qtcxep" :> "StartEvent_1"
+@@ "SequenceFlow_1njgdzy" :> "Task_07u875a"
+@@ "SequenceFlow_11rxzkm" :> "Task_1ne4gpy"
+@@ "SequenceFlow_00s838q" :> "Task_002ndsu"
+@@ "SequenceFlow_0n80biv" :> "IntermediateThrowEvent_0neineb"
+@@ "SequenceFlow_1rlj8av" :> "IntermediateThrowEvent_0xjpikb"
+@@ "SequenceFlow_0rfye55" :> "ExclusiveGateway_0i09ijx"
+@@ "SequenceFlow_13z4ilm" :> "ExclusiveGateway_0i09ijx"
+@@ "SequenceFlow_0mdvaai" :> "Task_1bn6n5q"
+@@ "SequenceFlow_0b34324" :> "ExclusiveGateway_1dc5v3z"
+@@ "SequenceFlow_1fn4lqy" :> "StartEvent_1f3jj6d"
+
+target ==
+   "MessageFlow_0knd10s" :> "Task_07u875a"
+@@ "MessageFlow_1yfhhru" :> "IntermediateThrowEvent_0xjpikb"
+@@ "MessageFlow_1m551dh" :> "EndEvent_0u6deep"
+@@ "MessageFlow_1goz1mt" :> "IntermediateThrowEvent_0neineb"
+@@ "MessageFlow_04an7oz" :> "IntermediateThrowEvent_12d113r"
+@@ "SequenceFlow_1dptcxp" :> "Task_1q91vog"
+@@ "SequenceFlow_1h5h7h5" :> "IntermediateThrowEvent_12d113r"
+@@ "SequenceFlow_0ljbxox" :> "EndEvent_0u6deep"
+@@ "SequenceFlow_1qku5do" :> "EndEvent_055yt9k"
+@@ "SequenceFlow_1qtcxep" :> "Task_07u875a"
+@@ "SequenceFlow_1njgdzy" :> "Task_1v9s881"
+@@ "SequenceFlow_11rxzkm" :> "EndEvent_10gqkzy"
+@@ "SequenceFlow_00s838q" :> "Task_1ne4gpy"
+@@ "SequenceFlow_0n80biv" :> "Task_002ndsu"
+@@ "SequenceFlow_1rlj8av" :> "IntermediateThrowEvent_0neineb"
+@@ "SequenceFlow_0rfye55" :> "IntermediateThrowEvent_0xjpikb"
+@@ "SequenceFlow_13z4ilm" :> "ExclusiveGateway_1dc5v3z"
+@@ "SequenceFlow_0mdvaai" :> "ExclusiveGateway_0i09ijx"
+@@ "SequenceFlow_0b34324" :> "Task_1bn6n5q"
+@@ "SequenceFlow_1fn4lqy" :> "ExclusiveGateway_1dc5v3z"
+
+CatN ==
+   "Customer_" :> Process
+@@ "TravelAgency_" :> Process
+@@ "Task_1v9s881" :> SendTask
+@@ "StartEvent_1" :> NoneStartEvent
+@@ "Task_07u875a" :> ReceiveTask
+@@ "EndEvent_055yt9k" :> NoneEndEvent
+@@ "EndEvent_0u6deep" :> CatchMessageIntermediateEvent
+@@ "IntermediateThrowEvent_12d113r" :> CatchMessageIntermediateEvent
+@@ "Task_1q91vog" :> SendTask
+@@ "StartEvent_1f3jj6d" :> NoneStartEvent
+@@ "ExclusiveGateway_1dc5v3z" :> ExclusiveOr
+@@ "Task_1bn6n5q" :> SendTask
+@@ "IntermediateThrowEvent_0xjpikb" :> CatchMessageIntermediateEvent
+@@ "EndEvent_10gqkzy" :> TerminateEndEvent
+@@ "Task_1ne4gpy" :> SendTask
+@@ "Task_002ndsu" :> SendTask
+@@ "IntermediateThrowEvent_0neineb" :> CatchMessageIntermediateEvent
+@@ "ExclusiveGateway_0i09ijx" :> ExclusiveOr
+
+CatE ==
+   "MessageFlow_0knd10s" :> MessageFlow
+@@ "MessageFlow_1yfhhru" :> MessageFlow
+@@ "MessageFlow_1m551dh" :> MessageFlow
+@@ "MessageFlow_1goz1mt" :> MessageFlow
+@@ "MessageFlow_04an7oz" :> MessageFlow
+@@ "SequenceFlow_1dptcxp" :> NormalSeqFlow
+@@ "SequenceFlow_1h5h7h5" :> NormalSeqFlow
+@@ "SequenceFlow_0ljbxox" :> NormalSeqFlow
+@@ "SequenceFlow_1qku5do" :> NormalSeqFlow
+@@ "SequenceFlow_1qtcxep" :> NormalSeqFlow
+@@ "SequenceFlow_1njgdzy" :> NormalSeqFlow
+@@ "SequenceFlow_11rxzkm" :> NormalSeqFlow
+@@ "SequenceFlow_00s838q" :> NormalSeqFlow
+@@ "SequenceFlow_0n80biv" :> NormalSeqFlow
+@@ "SequenceFlow_1rlj8av" :> NormalSeqFlow
+@@ "SequenceFlow_0rfye55" :> DefaultSeqFlow
+@@ "SequenceFlow_13z4ilm" :> ConditionalSeqFlow
+@@ "SequenceFlow_0mdvaai" :> NormalSeqFlow
+@@ "SequenceFlow_0b34324" :> NormalSeqFlow
+@@ "SequenceFlow_1fn4lqy" :> NormalSeqFlow
+
+LOCAL preEdges ==
+  [ i \in {} |-> {}]
+PreEdges(n,e) == preEdges[n,e]
+
+PreNodes(n,e) == { target[ee] : ee \in preEdges[n,e] }
+          \union { nn \in { source[ee] : ee \in preEdges[n,e] } : CatN[nn] \in { NoneStartEvent, MessageStartEvent } }
+
+BoundaryEvent ==
+  [ i \in {} |-> {}]
+
+WF == INSTANCE PWSWellFormed
+ASSUME WF!WellTyped
+ASSUME WF!WellFormedness
+
+ConstraintNode == TRUE \* none
+ConstraintEdge == TRUE \* none
+Constraint == TRUE     \* none
+INSTANCE PWSConstraints
+
+INSTANCE PWSSemantics
+
+================================================================
+