Merge commit 'bc1f3cbfde4bc3896e0750df17726f089fba4c72' into develop

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"

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

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,22 +517,23 @@ 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
 
 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))
 
 ================================================================