diff --git a/models/bpmn-origin/png/e040TravelAgency.png b/models/bpmn-origin/png/e040TravelAgency.png index f05523f..c257a52 100644 Binary files a/models/bpmn-origin/png/e040TravelAgency.png and b/models/bpmn-origin/png/e040TravelAgency.png differ diff --git a/models/bpmn-origin/src/e040TravelAgency.bpmn b/models/bpmn-origin/src/e040TravelAgency.bpmn index a6aa7db..585bdb6 100644 --- a/models/bpmn-origin/src/e040TravelAgency.bpmn +++ b/models/bpmn-origin/src/e040TravelAgency.bpmn @@ -1,5 +1,5 @@ - + modified from "A Classification of BPMN Collaborations based on Safeness and Soundness Notions", EXPRESS/SOS 2018. @@ -9,8 +9,8 @@ - + @@ -34,7 +34,7 @@ SequenceFlow_0b6ku63 SequenceFlow_016h32p - + SequenceFlow_1rma3l8 @@ -78,10 +78,6 @@ - - - - @@ -95,7 +91,7 @@ SequenceFlow_1yvkisw - SequenceFlow_0yhi6sc + Flow_1n9oaui SequenceFlow_1yvkisw SequenceFlow_17r8ru7 @@ -127,46 +123,70 @@ - - SequenceFlow_0b34324 - SequenceFlow_0p2zcuo - - - SequenceFlow_1fn4lqy - SequenceFlow_0p2zcuo - SequenceFlow_0b34324 - - - SequenceFlow_1fn4lqy + + + Flow_136sol6 + + Flow_0ugr6x2 + + + Flow_0ugr6x2 + Flow_14ugxng + Flow_11b0t0o + + + + Flow_11b0t0o + Flow_14ugxng + + + + + + Flow_136sol6 - - SequenceFlow_1ey63mn - + + + + Flow_0y4msh1 + - SequenceFlow_1ey63mn - SequenceFlow_0yhi6sc - + Flow_0y4msh1 + Flow_1n9oaui + - - + - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + @@ -175,12 +195,6 @@ - - - - - - @@ -204,238 +218,246 @@ - - + + - + - - + + - - + + - + + + + - - + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - + + - + - - - - - - - - - + + - - - - - - - - - - - + + - + - - - - - - - - - - - + + - - - - - - + + + + + + + + + + - - - + + + - - - + + + + - - - + + + + - - - + + + + + + + + + - - - - - - - - - + + - + - - - - - - - - - - - - - - - - + + - - - - - - - - - - + + + - - - + + + - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - + + + + + + - - - + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - - - - - - - - - - - - - - - - + + + + + - + - - - - - - - diff --git a/models/bpmn-origin/tla_from_bpmn/e040TravelAgency.tla b/models/bpmn-origin/tla_from_bpmn/e040TravelAgency.tla index 608d950..b42c494 100644 --- a/models/bpmn-origin/tla_from_bpmn/e040TravelAgency.tla +++ b/models/bpmn-origin/tla_from_bpmn/e040TravelAgency.tla @@ -5,23 +5,24 @@ EXTENDS TLC, PWSTypes VARIABLES nodemarks, edgemarks, net Interest == - "Customer_" :> { "Ticket", "NoMore", "Offer", "Confirmation" } + "Customer_" :> { "NoMore", "Ticket", "Offer", "Confirmation" } @@ "TravelAgency_" :> { "Abort", "Payment", "Travel" } 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" } + "Activity_0re3cuj" :> { "Event_0e98cce", "ExclusiveGateway_1dc5v3z", "Task_1bn6n5q" } + @@ "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_" :> { "BoundaryEvent_19y0yk9", "EndEvent_17rlcaz", "EndEvent_10gqkzy", "SubProcess_1agd6n3", "Task_1bn6n5q", "ExclusiveGateway_1dc5v3z", "StartEvent_1f3jj6d", "BoundaryEvent_0j1yvnw", "IntermediateThrowEvent_0b4rm53" } + @@ "TravelAgency_" :> { "BoundaryEvent_19y0yk9", "EndEvent_17rlcaz", "EndEvent_10gqkzy", "SubProcess_1agd6n3", "Activity_0re3cuj", "StartEvent_1f3jj6d", "BoundaryEvent_0j1yvnw", "IntermediateThrowEvent_0b4rm53" } 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","BoundaryEvent_19y0yk9","EndEvent_17rlcaz","EndEvent_10gqkzy","SubProcess_1agd6n3","Task_1bn6n5q","ExclusiveGateway_1dc5v3z","StartEvent_1f3jj6d","BoundaryEvent_0j1yvnw","IntermediateThrowEvent_0b4rm53","StartEvent_0qomvov","IntermediateThrowEvent_0xjpikb","IntermediateThrowEvent_0neineb","Task_002ndsu","Task_1ne4gpy","EndEvent_1vkzo14" + "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","BoundaryEvent_19y0yk9","EndEvent_17rlcaz","EndEvent_10gqkzy","SubProcess_1agd6n3","Activity_0re3cuj","StartEvent_1f3jj6d","BoundaryEvent_0j1yvnw","IntermediateThrowEvent_0b4rm53","StartEvent_0qomvov","IntermediateThrowEvent_0xjpikb","IntermediateThrowEvent_0neineb","Task_002ndsu","Task_1ne4gpy","EndEvent_1vkzo14","Event_0e98cce","ExclusiveGateway_1dc5v3z","Task_1bn6n5q" } 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_0p2zcuo","SequenceFlow_1fn4lqy","SequenceFlow_0b34324","SequenceFlow_0yhi6sc","SequenceFlow_1yvkisw","SequenceFlow_1oyuvjd","SequenceFlow_1ey63mn","SequenceFlow_17r8ru7","SequenceFlow_1j6r6o5","SequenceFlow_0bejayl","SequenceFlow_0ot5p93","SequenceFlow_023db5j" + "MessageFlow_0knd10s","MessageFlow_1yfhhru","MessageFlow_1m551dh","MessageFlow_1goz1mt","MessageFlow_04an7oz","MessageFlow_18qwt5e","Flow_03c8rm0","SequenceFlow_1uwq0b6","SequenceFlow_0b6ku63","SequenceFlow_0sfyd5z","SequenceFlow_016h32p","SequenceFlow_1rma3l8","SequenceFlow_1dptcxp","SequenceFlow_1h5h7h5","SequenceFlow_0ljbxox","SequenceFlow_1qku5do","SequenceFlow_1pk6qce","SequenceFlow_0ybs6n8","SequenceFlow_1yvkisw","SequenceFlow_1oyuvjd","Flow_136sol6","Flow_0y4msh1","Flow_1n9oaui","SequenceFlow_17r8ru7","SequenceFlow_1j6r6o5","SequenceFlow_0bejayl","SequenceFlow_0ot5p93","SequenceFlow_023db5j","Flow_0ugr6x2","Flow_11b0t0o","Flow_14ugxng" } -Message == { "Offer", "Travel", "Confirmation", "Payment", "Ticket", "NoMore", "Abort" } +Message == { "Offer", "Travel", "Confirmation", "Payment", "Ticket", "Abort", "NoMore" } msgtype == "MessageFlow_0knd10s" :> "Offer" @@ -29,8 +30,8 @@ msgtype == @@ "MessageFlow_1m551dh" :> "Confirmation" @@ "MessageFlow_1goz1mt" :> "Payment" @@ "MessageFlow_04an7oz" :> "Ticket" - @@ "MessageFlow_0joml9p" :> "NoMore" @@ "MessageFlow_18qwt5e" :> "Abort" + @@ "Flow_03c8rm0" :> "NoMore" source == "MessageFlow_0knd10s" :> "Task_1bn6n5q" @@ -38,8 +39,8 @@ source == @@ "MessageFlow_1m551dh" :> "Task_002ndsu" @@ "MessageFlow_1goz1mt" :> "Task_1q91vog" @@ "MessageFlow_04an7oz" :> "Task_1ne4gpy" -@@ "MessageFlow_0joml9p" :> "IntermediateThrowEvent_0b4rm53" @@ "MessageFlow_18qwt5e" :> "IntermediateThrowEvent_02q48nh" +@@ "Flow_03c8rm0" :> "IntermediateThrowEvent_0b4rm53" @@ "SequenceFlow_1uwq0b6" :> "ExclusiveGateway_192ovii" @@ "SequenceFlow_0b6ku63" :> "ExclusiveGateway_192ovii" @@ "SequenceFlow_0sfyd5z" :> "Task_07u875a" @@ -51,18 +52,19 @@ source == @@ "SequenceFlow_1qku5do" :> "EndEvent_0u6deep" @@ "SequenceFlow_1pk6qce" :> "BoundaryEvent_0qlhw6m" @@ "SequenceFlow_0ybs6n8" :> "IntermediateThrowEvent_02q48nh" -@@ "SequenceFlow_0p2zcuo" :> "Task_1bn6n5q" -@@ "SequenceFlow_1fn4lqy" :> "StartEvent_1f3jj6d" -@@ "SequenceFlow_0b34324" :> "ExclusiveGateway_1dc5v3z" -@@ "SequenceFlow_0yhi6sc" :> "IntermediateThrowEvent_0b4rm53" @@ "SequenceFlow_1yvkisw" :> "SubProcess_1agd6n3" @@ "SequenceFlow_1oyuvjd" :> "BoundaryEvent_19y0yk9" -@@ "SequenceFlow_1ey63mn" :> "BoundaryEvent_0j1yvnw" +@@ "Flow_136sol6" :> "StartEvent_1f3jj6d" +@@ "Flow_0y4msh1" :> "BoundaryEvent_0j1yvnw" +@@ "Flow_1n9oaui" :> "IntermediateThrowEvent_0b4rm53" @@ "SequenceFlow_17r8ru7" :> "StartEvent_0qomvov" @@ "SequenceFlow_1j6r6o5" :> "IntermediateThrowEvent_0xjpikb" @@ "SequenceFlow_0bejayl" :> "IntermediateThrowEvent_0neineb" @@ "SequenceFlow_0ot5p93" :> "Task_002ndsu" @@ "SequenceFlow_023db5j" :> "Task_1ne4gpy" +@@ "Flow_0ugr6x2" :> "Event_0e98cce" +@@ "Flow_11b0t0o" :> "ExclusiveGateway_1dc5v3z" +@@ "Flow_14ugxng" :> "Task_1bn6n5q" target == "MessageFlow_0knd10s" :> "Task_07u875a" @@ -70,8 +72,8 @@ target == @@ "MessageFlow_1m551dh" :> "EndEvent_0u6deep" @@ "MessageFlow_1goz1mt" :> "IntermediateThrowEvent_0neineb" @@ "MessageFlow_04an7oz" :> "IntermediateThrowEvent_12d113r" -@@ "MessageFlow_0joml9p" :> "BoundaryEvent_0qlhw6m" @@ "MessageFlow_18qwt5e" :> "BoundaryEvent_19y0yk9" +@@ "Flow_03c8rm0" :> "BoundaryEvent_0qlhw6m" @@ "SequenceFlow_1uwq0b6" :> "Task_1v9s881" @@ "SequenceFlow_0b6ku63" :> "ExclusiveGateway_0wgdt1i" @@ "SequenceFlow_0sfyd5z" :> "ExclusiveGateway_192ovii" @@ -83,18 +85,19 @@ target == @@ "SequenceFlow_1qku5do" :> "EndEvent_055yt9k" @@ "SequenceFlow_1pk6qce" :> "IntermediateThrowEvent_02q48nh" @@ "SequenceFlow_0ybs6n8" :> "EndEvent_0syu44v" -@@ "SequenceFlow_0p2zcuo" :> "ExclusiveGateway_1dc5v3z" -@@ "SequenceFlow_1fn4lqy" :> "ExclusiveGateway_1dc5v3z" -@@ "SequenceFlow_0b34324" :> "Task_1bn6n5q" -@@ "SequenceFlow_0yhi6sc" :> "SubProcess_1agd6n3" @@ "SequenceFlow_1yvkisw" :> "EndEvent_10gqkzy" @@ "SequenceFlow_1oyuvjd" :> "EndEvent_17rlcaz" -@@ "SequenceFlow_1ey63mn" :> "IntermediateThrowEvent_0b4rm53" +@@ "Flow_136sol6" :> "Activity_0re3cuj" +@@ "Flow_0y4msh1" :> "IntermediateThrowEvent_0b4rm53" +@@ "Flow_1n9oaui" :> "SubProcess_1agd6n3" @@ "SequenceFlow_17r8ru7" :> "IntermediateThrowEvent_0xjpikb" @@ "SequenceFlow_1j6r6o5" :> "IntermediateThrowEvent_0neineb" @@ "SequenceFlow_0bejayl" :> "Task_002ndsu" @@ "SequenceFlow_0ot5p93" :> "Task_1ne4gpy" @@ "SequenceFlow_023db5j" :> "EndEvent_1vkzo14" +@@ "Flow_0ugr6x2" :> "ExclusiveGateway_1dc5v3z" +@@ "Flow_11b0t0o" :> "Task_1bn6n5q" +@@ "Flow_14ugxng" :> "ExclusiveGateway_1dc5v3z" CatN == "Customer_" :> Process @@ -115,8 +118,7 @@ CatN == @@ "EndEvent_17rlcaz" :> NoneEndEvent @@ "EndEvent_10gqkzy" :> NoneEndEvent @@ "SubProcess_1agd6n3" :> SubProcess -@@ "Task_1bn6n5q" :> SendTask -@@ "ExclusiveGateway_1dc5v3z" :> ExclusiveOr +@@ "Activity_0re3cuj" :> SubProcess @@ "StartEvent_1f3jj6d" :> NoneStartEvent @@ "BoundaryEvent_0j1yvnw" :> TimerBoundaryEvent @@ "IntermediateThrowEvent_0b4rm53" :> ThrowMessageIntermediateEvent @@ -126,6 +128,9 @@ CatN == @@ "Task_002ndsu" :> SendTask @@ "Task_1ne4gpy" :> SendTask @@ "EndEvent_1vkzo14" :> NoneEndEvent +@@ "Event_0e98cce" :> NoneStartEvent +@@ "ExclusiveGateway_1dc5v3z" :> ExclusiveOr +@@ "Task_1bn6n5q" :> SendTask CatE == "MessageFlow_0knd10s" :> MessageFlow @@ -133,8 +138,8 @@ CatE == @@ "MessageFlow_1m551dh" :> MessageFlow @@ "MessageFlow_1goz1mt" :> MessageFlow @@ "MessageFlow_04an7oz" :> MessageFlow -@@ "MessageFlow_0joml9p" :> MessageFlow @@ "MessageFlow_18qwt5e" :> MessageFlow +@@ "Flow_03c8rm0" :> MessageFlow @@ "SequenceFlow_1uwq0b6" :> ConditionalSeqFlow @@ "SequenceFlow_0b6ku63" :> DefaultSeqFlow @@ "SequenceFlow_0sfyd5z" :> NormalSeqFlow @@ -146,18 +151,19 @@ CatE == @@ "SequenceFlow_1qku5do" :> NormalSeqFlow @@ "SequenceFlow_1pk6qce" :> NormalSeqFlow @@ "SequenceFlow_0ybs6n8" :> NormalSeqFlow -@@ "SequenceFlow_0p2zcuo" :> NormalSeqFlow -@@ "SequenceFlow_1fn4lqy" :> NormalSeqFlow -@@ "SequenceFlow_0b34324" :> NormalSeqFlow -@@ "SequenceFlow_0yhi6sc" :> NormalSeqFlow @@ "SequenceFlow_1yvkisw" :> NormalSeqFlow @@ "SequenceFlow_1oyuvjd" :> NormalSeqFlow -@@ "SequenceFlow_1ey63mn" :> NormalSeqFlow +@@ "Flow_136sol6" :> NormalSeqFlow +@@ "Flow_0y4msh1" :> NormalSeqFlow +@@ "Flow_1n9oaui" :> NormalSeqFlow @@ "SequenceFlow_17r8ru7" :> NormalSeqFlow @@ "SequenceFlow_1j6r6o5" :> NormalSeqFlow @@ "SequenceFlow_0bejayl" :> NormalSeqFlow @@ "SequenceFlow_0ot5p93" :> NormalSeqFlow @@ "SequenceFlow_023db5j" :> NormalSeqFlow +@@ "Flow_0ugr6x2" :> NormalSeqFlow +@@ "Flow_11b0t0o" :> NormalSeqFlow +@@ "Flow_14ugxng" :> NormalSeqFlow LOCAL preEdges == [ i \in {} |-> {}] @@ -169,7 +175,7 @@ PreNodes(n,e) == { target[ee] : ee \in preEdges[n,e] } BoundaryEvent == "BoundaryEvent_0qlhw6m" :> [ attachedTo |-> "Task_07u875a", cancelActivity |-> TRUE ] @@ "BoundaryEvent_19y0yk9" :> [ attachedTo |-> "SubProcess_1agd6n3", cancelActivity |-> TRUE ] -@@ "BoundaryEvent_0j1yvnw" :> [ attachedTo |-> "Task_1bn6n5q", cancelActivity |-> TRUE ] +@@ "BoundaryEvent_0j1yvnw" :> [ attachedTo |-> "Activity_0re3cuj", cancelActivity |-> TRUE ] WF == INSTANCE PWSWellFormed ASSUME WF!WellTyped diff --git a/src/Fbpmn/Analysis/Tla/IO/Tla.hs b/src/Fbpmn/Analysis/Tla/IO/Tla.hs index 503ac9f..84a7cf9 100644 --- a/src/Fbpmn/Analysis/Tla/IO/Tla.hs +++ b/src/Fbpmn/Analysis/Tla/IO/Tla.hs @@ -253,7 +253,7 @@ encodeBpmnBoundaryEventsToTla g = [text| |] where sbes = relationTla beToTla bes - bes = nodesTs g [MessageBoundaryEvent, TimerBoundaryEvent] + bes = nodesTs g [MessageBoundaryEvent, TimerBoundaryEvent] beToTla e = case (catN g !? e, attached g !? e) of (Just MessageBoundaryEvent, Just spid) -> [text|$side :> [ attachedTo |-> $sspid, cancelActivity |-> $scae ]|] @@ -267,7 +267,8 @@ encodeBpmnBoundaryEventsToTla g = [text| side = show e sspid = show spid scae = boolToTLA $ fromMaybe True (isInterrupt g !? e) - _ -> "" + (Just _ , _) -> "" + (Nothing, _) -> "" trueTla :: Text trueTla = "TRUE" diff --git a/src/Fbpmn/BpmnGraph/IO/Bpmn.hs b/src/Fbpmn/BpmnGraph/IO/Bpmn.hs index b763cbc..d08c629 100644 --- a/src/Fbpmn/BpmnGraph/IO/Bpmn.hs +++ b/src/Fbpmn/BpmnGraph/IO/Bpmn.hs @@ -114,7 +114,8 @@ pCx = hasChildren (nE "conditionExpression") pIx :: Element -> Bool pIx e = case findAttr (nA "cancelActivity") e of Just "false" -> False - _ -> True -- cancelActivity by default + Just _ -> True -- cancelActivity by default + Nothing -> True -- cancelActivity by default -- timer events pTimex :: Element -> Bool pTimex = hasChildren (nE "timerEventDefinition") @@ -126,17 +127,18 @@ pTimerDefinitionType' e = case () of | otherwise -> Nothing pTimerDefinitionValue' :: Element -> Maybe TimerValue pTimerDefinitionValue' e = do - contents <- elContent <$> eval - content1 <- listToMaybe contents - case content1 of - Text cdata -> Just $ cdData cdata - _ -> Nothing - where - eval = case () of - _ | hasChildren (nE "timeDate") e -> findChild (nE "timeDate") e - | hasChildren (nE "timeDuration") e -> findChild (nE "timeDuration") e - | hasChildren (nE "timeCycle") e -> findChild (nE "timeCycle") e - | otherwise -> Nothing + contents <- elContent <$> eval + content1 <- listToMaybe contents + case content1 of + Text cdata -> Just $ cdData cdata + Elem _ -> Nothing + CRef _ -> Nothing + where + eval = case () of + _ | hasChildren (nE "timeDate") e -> findChild (nE "timeDate") e + | hasChildren (nE "timeDuration") e -> findChild (nE "timeDuration") e + | hasChildren (nE "timeCycle") e -> findChild (nE "timeCycle") e + | otherwise -> Nothing pTimerDefinitionType :: Element -> Maybe TimerDefinitionType pTimerDefinitionType e = pTimerDefinitionType' =<< findChild (nE "timerEventDefinition") e @@ -204,9 +206,9 @@ pTBE :: [Element] -> Element -> Maybe NodeType pTBE es e = if pBE es e && pTimex e then Just TimerBoundaryEvent else Nothing pCancelActivity :: Element -> Bool pCancelActivity e = case findAttr (nA "cancelActivity") e of - Just "true" -> True Just "false" -> False - _ -> True -- boundary events are interrupting by default + Just _ -> True -- boundary events are interrupting by default + Nothing -> True -- boundary events are interrupting by default -- time-related events pTE :: [Element] -> Element -> Bool diff --git a/theories/tla/PWSSemantics.tla b/theories/tla/PWSSemantics.tla index 5309021..ff828fc 100644 --- a/theories/tla/PWSSemantics.tla +++ b/theories/tla/PWSSemantics.tla @@ -28,7 +28,7 @@ subprocess_may_complete(n) == /\ \E ee \in ContainRel[n] : /\ CatN[ee] \in EndEventType /\ nodemarks[ee] >= 1 - /\ \A x \in ContainRel[n] : nodemarks[x] >= 1 => CatN[x] \in EndEventType + /\ \A x \in ContainRel[n] : CatN[x] \in EndEventType \/ nodemarks[x] = 0 (* ---- none start event ---- *) @@ -57,26 +57,20 @@ timerstart_complete(n) == (* ---- message start event ---- *) -messagestart_start(n) == - /\ CatN[n] = MessageStartEvent - /\ nodemarks[n] = 0 - /\ \E e \in intype(MessageFlowType, n) : - /\ edgemarks[e] >= 1 - /\ Network!receive(ProcessOf(source[e]), ProcessOf(n), msgtype[e]) - /\ edgemarks' = [ edgemarks EXCEPT ![e] = @ - 1 ] - /\ nodemarks' = [ nodemarks EXCEPT ![n] = @ + 1 ] - messagestart_complete(n) == /\ CatN[n] = MessageStartEvent /\ nodemarks[n] >= 1 + /\ \E em \in intype(MessageFlowType, n) : + /\ edgemarks[em] >= 1 + /\ Network!receive(ProcessOf(source[em]), ProcessOf(n), msgtype[em]) + /\ edgemarks' = [ e \in DOMAIN edgemarks |-> + IF e \in outtype(SeqFlowType, n) THEN edgemarks[e] + 1 + ELSE IF e = em THEN edgemarks[e] - 1 + ELSE edgemarks[e] ] /\ \E p \in Processes : /\ n \in ContainRel[p] /\ nodemarks[p] = 0 \* No multi-instance /\ nodemarks' = [ nodemarks EXCEPT ![n] = @ - 1, ![p] = @ + 1 ] - /\ edgemarks' = [ e \in DOMAIN edgemarks |-> - IF e \in outtype(SeqFlowType, n) THEN edgemarks[e] + 1 - ELSE edgemarks[e] ] - /\ Network!unchanged (* ---- none end event, terminate end event ---- *) @@ -443,7 +437,7 @@ process_complete(n) == FALSE step(n) == CASE CatN[n] = NoneStartEvent -> nonestart_complete(n) [] CatN[n] = TimerStartEvent -> timerstart_complete(n) - [] CatN[n] = MessageStartEvent -> messagestart_start(n) \/ messagestart_complete(n) + [] CatN[n] = MessageStartEvent -> messagestart_complete(n) [] CatN[n] = NoneEndEvent -> noneend_start(n) [] CatN[n] = TerminateEndEvent -> terminateend_start(n) [] CatN[n] = MessageEndEvent -> messageend_start(n) @@ -466,7 +460,7 @@ Next == \E n \in Node : step(n) Init == /\ nodemarks = [ n \in Node |-> - IF CatN[n] \in {NoneStartEvent,TimerStartEvent} /\ (\E p \in Processes : n \in ContainRel[p]) THEN 1 + IF CatN[n] \in StartEventType /\ (\E p \in Processes : n \in ContainRel[p]) THEN 1 ELSE 0 ] /\ edgemarks = [ e \in Edge |-> 0 ] /\ Network!init @@ -507,8 +501,8 @@ NoAbnormalTermination == \A n \in Node : CatN[n] = TerminateEndEvent => [](nodemarks[n] = 0) (* No messages are eventually left in transit. *) -NoUndeliveredMessages == LET msgflows == { ee \in Edge : CatE[ee] \in MessageFlowType } IN - (\E e \in msgflows : edgemarks[e] > 0) ~> (\A e \in msgflows : edgemarks[e] = 0) +NoUndeliveredMessages == <>[](LET msgflows == { ee \in Edge : CatE[ee] \in MessageFlowType } IN + \A e \in msgflows : edgemarks[e] = 0) \* Any message is eventually delivered. \* NoUndeliveredMessages2 == @@ -523,10 +517,11 @@ NoUndeliveredMessages == LET msgflows == { ee \in Edge : CatE[ee] \in MessageFlo SafeCollaboration == [](\A e \in Edge : CatE[e] \in SeqFlowType => edgemarks[e] <= 1) -(* A process is sound if there are no token on inside edges, and one token only on EndEvents. *) +(* A process is sound if there are no token on inside edges, and one token only on EndEvents. Start events are ignored. *) LOCAL SoundProcessInt(p) == /\ \A e \in Edge : source[e] \in ContainRel[p] /\ target[e] \in ContainRel[p] => edgemarks[e] = 0 /\ \A n \in ContainRel[p] : + \/ CatN[n] \in StartEventType \/ nodemarks[n] = 0 \/ nodemarks[n] = 1 /\ CatN[n] \in EndEventType @@ -534,11 +529,11 @@ SoundProcess(p) == <> SoundProcessInt(p) (* All processes are sound and there are no undelivered messages. *) SoundCollaboration == - <>(/\ \A n \in Node : CatN[n] = Process => SoundProcessInt(n) - /\ \A e \in Edge : CatE[e] \in MessageFlowType => edgemarks[e] = 0) + <>[](/\ \A n \in Node : CatN[n] = Process => SoundProcessInt(n) + /\ \A e \in Edge : CatE[e] \in MessageFlowType => edgemarks[e] = 0) (* Like SoundCollaboration, but ignore messages in transit. *) MessageRelaxedSoundCollaboration == - <>(/\ \A n \in Node : CatN[n] = Process => SoundProcessInt(n)) + <>[](\A n \in Node : CatN[n] = Process => SoundProcessInt(n)) ================================================================