Fix Activity Final node handling in ActionSequences functions

modelling-tasks.cabal

@@ -150,6 +150,7 @@ test-suite modelling-tasks-test
   type: exitcode-stdio-1.0
   main-is: Main.hs
   other-modules:
+      Modelling.ActivityDiagram.ActionSequencesActivityFinalSpec
       Modelling.ActivityDiagram.ActionSequencesSpec
       Modelling.ActivityDiagram.AlloySpec
       Modelling.ActivityDiagram.Auxiliary.ParserSpec

src/Modelling/ActivityDiagram/ActionSequences.hs

@@ -8,15 +8,23 @@ module Modelling.ActivityDiagram.ActionSequences (
   actionRepetitionDistance,
   netAndMap,
   computeActionSequenceLevels,
+  getActionsLeadingToActivityFinals,
   isFinalPetriNode
 ) where
 
-import qualified Data.Set as S (fromList, singleton, insert, notMember)
+import qualified Modelling.ActivityDiagram.Datatype as Ad (
+  AdNode (label),
+  )
+
+import qualified Data.Set as S (fromList, union, member, empty, toList, singleton, insert, notMember)
 import qualified Data.Map as M (filter, map, keys, fromList, toList)
 
 import Modelling.ActivityDiagram.Datatype (
   AdNode (..),
-  UMLActivityDiagram (..)
+  UMLActivityDiagram (..),
+  AdConnection (..),
+  isActionNode,
+  isActivityFinalNode
   )
 
 import Modelling.ActivityDiagram.PetriNet (
@@ -36,12 +44,10 @@ import Modelling.PetriNet.Reach.Type (
   Net(..)
   )
 
-import Modelling.PetriNet.Reach.Reach (levelsWithAlternatives)
 import Modelling.PetriNet.Reach.Step (successors)
 
-import Control.Monad (guard)
+import qualified Control.Monad as Monad (guard)
 import Control.Monad.Random (MonadRandom, uniform)
-import Data.Bifunctor (second)
 import Data.List (union)
 import Data.List.Extra (nubOrd)
 import Data.Maybe (mapMaybe, isJust)
@@ -60,17 +66,19 @@ fromPetriLike petri =
 -- | Generate a valid action sequence reaching each of the final nodes
 generateActionSequence :: UMLActivityDiagram -> [String]
 generateActionSequence diag =
-  head $ generateActionSequencesWithPetri (convertToPetriNet diag) Nothing
+  head $ generateActionSequencesWithPetri diag (convertToPetriNet diag) Nothing
 
 -- | Generate valid action sequences, using a pre-computed Petri net.
 -- The returned list may be infinite or some of its tails even diverge,
 -- if no length constraints are passed.
 generateActionSequencesWithPetri
-  :: PetriLike Node PetriKey
+  :: UMLActivityDiagram
+  -> PetriLike Node PetriKey
   -> Maybe (Int, Int)  -- Optional (minLength, maxLength) constraints
   -> [[String]]
-generateActionSequencesWithPetri =
-  generateSequencesWithLevels (map (map (second head)) . levelsWithAlternatives)
+generateActionSequencesWithPetri diag =
+  let actionsLeadingToActivityFinals = getActionsLeadingToActivityFinals diag
+  in generateSequencesWithLevels (levelsAS actionsLeadingToActivityFinals)
 
 -- | Generate one valid action sequence with repetition, using a pre-computed Petri net.
 -- This version allows cycle exploration to generate sequences with repeated actions.
@@ -98,7 +106,9 @@ generateSequencesWithLevels
   -> [[String]]
 generateSequencesWithLevels levelsFunction petriLike maybeLengthBounds =
   let petri = fromPetriLike petriLike
-      zeroState = State $ M.map (const 0) $ unState $ start petri
+      -- Use all places in the network to create the zero state for consistency
+      allPlaces = S.toList $ places petri
+      zeroState = State $ M.fromList [(p, 0) | p <- allPlaces]
       relevantLevels = maybe id (\(minLength, maxLength) -> take (5 * maxLength) . drop minLength) maybeLengthBounds
                        $ levelsFunction petri
       convertAndFilterSequence transitionSequence =
@@ -110,16 +120,56 @@ generateSequencesWithLevels levelsFunction petriLike maybeLengthBounds =
              _ -> Just actionSequence
   in [ reverse a | level <- relevantLevels, (s, p) <- level, s == zeroState, Just a <- [convertAndFilterSequence p] ]
 
+-- Variant of levelsWithAlternatives that computes only one path per state, while handling Activity Final nodes
+levelsAS :: Ord s => [Int] -> Net s PetriKey -> [[(State s, [PetriKey])]]
+levelsAS actionsLeadingToActivityFinals n =
+  let -- Create zero state using all places in the network for consistency
+      allPlaces = S.toList $ places n
+      zeroState = State $ M.fromList [(p, 0) | p <- allPlaces]
+      -- Check if a transition corresponds to Activity Final
+      isActivityFinalTransition t = case t of
+        -- For normal petri nodes, check if the action leads to Activity Final
+        NormalPetriNode {sourceNode = adNode} ->
+          isActionNode adNode && Ad.label adNode `elem` actionsLeadingToActivityFinals
+        -- For final petri nodes, check if it's an Activity Final
+        FinalPetriNode {sourceNode = adNode} -> isActivityFinalNode adNode
+        _ -> False
+      f _ [] = []
+      f done xs =
+        let done' = S.fromList (map fst xs) `S.union` done
+            next = M.toList $ M.fromList [ (finalState, t:p) |
+                (x,p) <- xs,
+                (t,y) <- successors n x,
+                -- If this is an Activity Final transition, use consistent zero state
+                let finalState = if isActivityFinalTransition t then zeroState else y,
+                not $ S.member finalState done'
+              ]
+         in xs : f done' next
+  in f S.empty [(start n, [])]
+
+-- Get Action nodes that are immediately followed by Activity Final nodes
+getActionsLeadingToActivityFinals :: UMLActivityDiagram -> [Int]
+getActionsLeadingToActivityFinals (UMLActivityDiagram adNodes adConnections) =
+  let activityFinalLabels = map Ad.label $ filter isActivityFinalNode adNodes
+      -- Find action nodes that directly connect to Activity Final nodes
+      directConnections = [(from conn, to conn) | conn <- adConnections,
+                          to conn `elem` activityFinalLabels]
+      actionNodeLabels = map Ad.label $ filter isActionNode adNodes
+      actionsDirectlyToActivityFinals = [fromLabel | (fromLabel, _) <- directConnections,
+                                        fromLabel `elem` actionNodeLabels]
+  in actionsDirectlyToActivityFinals
 
 validActionSequence :: [String] -> UMLActivityDiagram -> Bool
-validActionSequence input =
-  uncurry (validActionSequenceWithPetri input) . netAndMap . convertToPetriNet
+validActionSequence input diag =
+  uncurry (validActionSequenceWithPetri input diag) $ netAndMap $ convertToPetriNet diag
 
 -- | Check if an action sequence is valid, using a pre-computed Petri net.
-validActionSequenceWithPetri :: [String] -> Net PetriKey PetriKey -> [(String, PetriKey)] -> Bool
-validActionSequenceWithPetri input net actionNameToPetriKey =
+validActionSequenceWithPetri :: [String] -> UMLActivityDiagram -> Net PetriKey PetriKey -> [(String, PetriKey)] -> Bool
+validActionSequenceWithPetri input diag net actionNameToPetriKey =
   let zeroState = State $ M.map (const 0) $ unState $ start net
-      levels = computeActionSequenceLevels input net actionNameToPetriKey
+      levels = computeActionSequenceLevels input net actionNameToPetriKey actionsLeadingToActivityFinals
+      -- Get Action nodes that lead directly to Activity Final nodes
+      actionsLeadingToActivityFinals = getActionsLeadingToActivityFinals diag
   in any (isJust . lookup zeroState) levels
 
 netAndMap :: PetriLike Node PetriKey -> (Net PetriKey PetriKey, [(String, PetriKey)])
@@ -130,13 +180,13 @@ netAndMap petri =
   in (fromPetriLike petri, actionNameToPetriKey)
 
 -- | Common computation for action sequence validation.
-computeActionSequenceLevels :: [String] -> Net PetriKey PetriKey -> [(String, PetriKey)] -> [[(State PetriKey, [PetriKey])]]
-computeActionSequenceLevels input net actionNameToPetriKey =
+computeActionSequenceLevels :: [String] -> Net PetriKey PetriKey -> [(String, PetriKey)] -> [Int] -> [[(State PetriKey, [PetriKey])]]
+computeActionSequenceLevels input net actionNameToPetriKey actionsLeadingToActivityFinals =
   let -- Convert input action names to PetriKeys
       input' = mapMaybe (`lookup` actionNameToPetriKey) input
       -- Extract all action PetriKeys
       actions = map snd actionNameToPetriKey
-      levels = levelsCheckAS input' actions net
+      levels = levelsCheckAS input' actions net actionsLeadingToActivityFinals
   in levels
 
 -- | Check if a PetriKey represents a final node transition
@@ -145,14 +195,27 @@ isFinalPetriNode (FinalPetriNode {}) = True
 isFinalPetriNode _ = False
 
 
-levelsCheckAS :: [PetriKey] -> [PetriKey] -> Net PetriKey PetriKey-> [[(State PetriKey, [PetriKey])]]
-levelsCheckAS input actions n =
-  let g h xs = M.toList $
+levelsCheckAS :: [PetriKey] -> [PetriKey] -> Net PetriKey PetriKey -> [Int] -> [[(State PetriKey, [PetriKey])]]
+levelsCheckAS input actions n actionsLeadingToActivityFinals =
+  let -- Create zero state using all places in the network for consistency
+      allPlaces = S.toList $ places n
+      zeroState = State $ M.fromList [(p, 0) | p <- allPlaces]
+      -- Check if a transition corresponds to Activity Final
+      isActivityFinalTransition t = case t of
+        -- For normal petri nodes, check if the action leads to Activity Final
+        NormalPetriNode {sourceNode = adNode} ->
+          isActionNode adNode && Ad.label adNode `elem` actionsLeadingToActivityFinals
+        -- For final petri nodes, check if it's an Activity Final
+        FinalPetriNode {sourceNode = adNode} -> isActivityFinalNode adNode
+        _ -> False
+      g h xs = M.toList $
         M.fromList $ do
           (x, p) <- xs
           (t, y) <- successors n x
-          guard $ h t
-          return (y, t : p)
+          Monad.guard $ h t
+          -- If this is an Activity Final transition, immediately go to zero state
+          let finalState = if isActivityFinalTransition t then zeroState else y
+          return (finalState, t : p)
       f _ [] = []
       f [] xs =
         let next = g (`notElem` actions) xs               -- No further actions should be processed if no input is left

src/Modelling/ActivityDiagram/EnterAS.hs

@@ -34,6 +34,7 @@ import Modelling.ActivityDiagram.ActionSequences (
   generateActionSequencesWithPetri,
   netAndMap,
   computeActionSequenceLevels,
+  getActionsLeadingToActivityFinals,
   isFinalPetriNode,
   )
 import Modelling.ActivityDiagram.Auxiliary.ActionSequences (actionSequencesAlloy)
@@ -210,9 +211,9 @@ newtype EnterASSolution = EnterASSolution {
   sampleSolution :: [String]
 } deriving (Show, Eq)
 
-enterActionSequence :: PetriLike Node PetriKey -> EnterASSolution
-enterActionSequence petri =
-  EnterASSolution {sampleSolution = head $ generateActionSequencesWithPetri petri Nothing}
+enterActionSequence :: UMLActivityDiagram -> PetriLike Node PetriKey -> EnterASSolution
+enterActionSequence ad petri =
+  EnterASSolution {sampleSolution = head $ generateActionSequencesWithPetri ad petri Nothing}
 
 enterASTask
   :: (MonadPlantUml m, MonadWriteFile m, OutputCapable m)
@@ -280,11 +281,12 @@ enterASEvaluation
   -> [String]
   -> Rated m
 enterASEvaluation task sub = do
-  let objectNames = map name $ filter isObjectNode $ nodes $ activityDiagram task
+  let diag = activityDiagram task
+      objectNames = map name $ filter isObjectNode $ nodes diag
       objectNamesInSubmission = nubOrd $ sub `intersect` objectNames
       (net, actionNameToPetriKey) = netAndMap (petriNet task)
       zeroState = State $ M.map (const 0) $ unState $ start net
-      levels = computeActionSequenceLevels sub net actionNameToPetriKey
+      levels = computeActionSequenceLevels sub net actionNameToPetriKey (getActionsLeadingToActivityFinals diag)
       reachesZeroState = any (isJust . lookup zeroState) levels
       correct = null objectNamesInSubmission && reachesZeroState
       points = if correct then 1 else 0
@@ -362,7 +364,7 @@ getEnterASTask config = do
           drawSettings = defaultPlantUmlConfig {
             suppressBranchConditions = hideBranchConditions config
             },
-          sampleSequence = sampleSolution $ enterActionSequence petri,
+          sampleSequence = sampleSolution $ enterActionSequence x petri,
           noLongerThan = rejectLongerThan config,
           showSolution = printSolution config,
           addText = extraText config

src/Modelling/ActivityDiagram/SelectAS.hs

@@ -227,7 +227,7 @@ selectActionSequence withRepetition numberOfWrongSequences lengthBounds ad = May
     (True, Nothing) -> return Nothing
     (False, _) ->
       let
-        validSequences = generateActionSequencesWithPetri petri (Just lengthBounds)
+        validSequences = generateActionSequencesWithPetri ad petri (Just lengthBounds)
       in
         if null validSequences
         then
@@ -239,7 +239,7 @@ selectActionSequence withRepetition numberOfWrongSequences lengthBounds ad = May
     Just correctSequence -> do
       let (net, actionNameToPetriKey) = netAndMap petri
           allWrongCandidates =
-            filter (\actionSeq -> not (validActionSequenceWithPetri actionSeq net actionNameToPetriKey)) $
+            filter (\actionSeq -> not (validActionSequenceWithPetri actionSeq ad net actionNameToPetriKey)) $
             (if withRepetition then nubOrd else id) $
             permutations correctSequence
       -- Early check: reject if insufficient candidates

test/Modelling/ActivityDiagram/ActionSequencesActivityFinalSpec.hs

@@ -0,0 +1,77 @@
+module Modelling.ActivityDiagram.ActionSequencesActivityFinalSpec where
+
+import Modelling.ActivityDiagram.ActionSequences (validActionSequence)
+
+import Modelling.ActivityDiagram.Datatype (
+  UMLActivityDiagram(..),
+  AdNode (..),
+  AdConnection (..)
+  )
+
+import Test.Hspec(Spec, context, describe, it, shouldBe)
+
+spec :: Spec
+spec =
+  describe "ActionSequences with Activity Final nodes" $ do
+    context "fork diagram with Activity Final" $ do
+      it "validates sequence ['A','B'] that reaches Activity Final and terminates all flows" $
+        validActionSequence ["A","B"] testDiagramForkActivityFinal `shouldBe` True
+      it "rejects incomplete sequence ['A'] that doesn't reach termination" $
+        validActionSequence ["A"] testDiagramForkActivityFinal `shouldBe` False
+      it "validates sequence ['A','C','B'] where Activity Final terminates all flows" $
+        validActionSequence ["A","C","B"] testDiagramForkActivityFinal `shouldBe` True
+    context "fork diagram with Activity Final through Object nodes" $ do
+      it "validates sequence ['A','B'] that reaches Activity Final through Object node" $
+        validActionSequence ["A","B"] testDiagramForkActivityFinalWithObjects `shouldBe` True
+      it "rejects sequence ['A','C'] that only reaches Flow Final through Object node" $
+        validActionSequence ["A","C"] testDiagramForkActivityFinalWithObjects `shouldBe` False
+      it "validates sequence ['A','C','B'] where Activity Final terminates all flows after Flow Final" $
+        validActionSequence ["A","C","B"] testDiagramForkActivityFinalWithObjects `shouldBe` True
+
+-- Fork diagram with Activity Final through Object nodes
+testDiagramForkActivityFinalWithObjects :: UMLActivityDiagram
+testDiagramForkActivityFinalWithObjects = UMLActivityDiagram
+  { nodes =
+    [ AdInitialNode { label = 1 }
+    , AdActionNode { label = 2, name = "A" }
+    , AdForkNode { label = 3 }
+    , AdActionNode { label = 4, name = "B" }
+    , AdActionNode { label = 5, name = "C" }
+    , AdObjectNode { label = 6, name = "ObjB" }  -- Object node before Activity Final
+    , AdObjectNode { label = 7, name = "ObjC" }  -- Object node before Flow Final
+    , AdActivityFinalNode { label = 8 }
+    , AdFlowFinalNode { label = 9 }
+    ]
+  , connections =
+    [ AdConnection { from = 1, to = 2, guard = "" }
+    , AdConnection { from = 2, to = 3, guard = "" }
+    , AdConnection { from = 3, to = 4, guard = "" }  -- Fork -> B
+    , AdConnection { from = 3, to = 5, guard = "" }  -- Fork -> C
+    , AdConnection { from = 4, to = 6, guard = "" }  -- B -> ObjB
+    , AdConnection { from = 5, to = 7, guard = "" }  -- C -> ObjC
+    , AdConnection { from = 6, to = 8, guard = "" }  -- ObjB -> Activity Final
+    , AdConnection { from = 7, to = 9, guard = "" }  -- ObjC -> Flow Final
+    ]
+  }
+
+-- Fork diagram: Initial -> A -> Fork -> (B -> Activity Final, C -> Flow Final)
+testDiagramForkActivityFinal :: UMLActivityDiagram
+testDiagramForkActivityFinal = UMLActivityDiagram
+  { nodes =
+    [ AdInitialNode { label = 1 }
+    , AdActionNode { label = 2, name = "A" }
+    , AdForkNode { label = 3 }
+    , AdActionNode { label = 4, name = "B" }
+    , AdActionNode { label = 5, name = "C" }
+    , AdActivityFinalNode { label = 6 }
+    , AdFlowFinalNode { label = 7 }
+    ]
+  , connections =
+    [ AdConnection { from = 1, to = 2, guard = "" }
+    , AdConnection { from = 2, to = 3, guard = "" }
+    , AdConnection { from = 3, to = 4, guard = "" }
+    , AdConnection { from = 3, to = 5, guard = "" }
+    , AdConnection { from = 4, to = 6, guard = "" }  -- B leads to Activity Final
+    , AdConnection { from = 5, to = 7, guard = "" }  -- C leads to Flow Final
+    ]
+  }