diff --git a/modelling-tasks.cabal b/modelling-tasks.cabal
index dd52f183c..d8bac4354 100644
--- a/modelling-tasks.cabal
+++ b/modelling-tasks.cabal
@@ -147,6 +147,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
diff --git a/src/Modelling/ActivityDiagram/ActionSequences.hs b/src/Modelling/ActivityDiagram/ActionSequences.hs
index 2ae292e9a..48481d67a 100644
--- a/src/Modelling/ActivityDiagram/ActionSequences.hs
+++ b/src/Modelling/ActivityDiagram/ActionSequences.hs
@@ -2,19 +2,21 @@
 module Modelling.ActivityDiagram.ActionSequences (
   validActionSequence,
   generateActionSequence,
+  isActivityFinalPetriNode,
 ) where
 
 import qualified Modelling.ActivityDiagram.Datatype as Ad (
   AdNode (label),
   )
 
-import qualified Data.Set as S (fromList)
+import qualified Data.Set as S (fromList, union, member, empty, toList)
 import qualified Data.Map as M (filter, map, keys, fromList, toList)
 
 import Modelling.ActivityDiagram.Datatype (
   AdNode (..),
   UMLActivityDiagram (..),
-  isActionNode
+  isActionNode,
+  isActivityFinalNode
   )
 
 import Modelling.ActivityDiagram.PetriNet (
@@ -34,7 +36,7 @@ import Modelling.PetriNet.Reach.Type (
   Net(..)
   )
 
-import Modelling.PetriNet.Reach.Step (levels', successors)
+import Modelling.PetriNet.Reach.Step (successors)
 
 import Control.Monad (guard)
 import Data.List (find, union)
@@ -54,7 +56,8 @@ fromPetriLike petri =
 --Generate one valid action sequence to each of the final nodes
 generateActionSequence :: UMLActivityDiagram -> [String]
 generateActionSequence diag =
-  let tSeq = generateActionSequence' diag
+  let activityFinalLabels = map Ad.label $ filter isActivityFinalNode $ nodes diag
+      tSeq = generateActionSequence' diag activityFinalLabels
       tSeqLabels = map (Ad.label . sourceNode) $ filter isNormalPetriNode tSeq
       actions = map
         (\n -> (Ad.label n, name n))
@@ -67,14 +70,46 @@ isNormalPetriNode pk =
     NormalPetriNode {} -> True
     _ -> False
 
+-- Check if a PetriKey corresponds to an Activity Final node
+isActivityFinalPetriNode :: PetriKey -> Bool
+isActivityFinalPetriNode pk =
+  case pk of
+    FinalPetriNode _ srcNode -> isActivityFinalNode srcNode
+    _ -> False
+
 --Generate at one sequence of transitions to each final node
-generateActionSequence' :: UMLActivityDiagram -> [PetriKey]
-generateActionSequence' diag =
+generateActionSequence' :: UMLActivityDiagram -> [Int] -> [PetriKey]
+generateActionSequence' diag activityFinalLabels =
   let petri = fromPetriLike $ convertToPetriNet diag
-      zeroState = State $ M.map (const 0) $ unState $ start petri
-      sequences = fromJust $ find (isJust . lookup zeroState) $ levels' 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]
+      sequences = fromJust $ find (isJust . lookup zeroState) $ levelsAS petri activityFinalLabels
   in reverse $ fromJust $ lookup zeroState sequences
 
+-- Modified version of levels' that handles Activity Final nodes
+levelsAS :: Ord s => Net s PetriKey -> [Int] -> [[(State s, [PetriKey])]]
+levelsAS n activityFinalLabels =
+  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
+        AuxiliaryPetriNode nodeLabel -> nodeLabel `elem` activityFinalLabels
+        _ -> 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, [])]
+
 
 validActionSequence :: [String] -> UMLActivityDiagram -> Bool
 validActionSequence input diag =
@@ -88,28 +123,43 @@ validActionSequence input diag =
         $ filter isNormalPetriNode $ M.keys $ allNodes petri
       input' = mapMaybe (`lookup` petriKeyMap) labels
       actions = map snd $ filter (\(l,_) -> l `elem` map snd nameMap) petriKeyMap
-  in length input == length labels && validActionSequence' input' actions petri
+      -- Get Activity Final node labels from original diagram
+      activityFinalLabels = map Ad.label $ filter isActivityFinalNode $ nodes diag
+  in length input == length labels && validActionSequence' input' actions petri activityFinalLabels
 
 
 validActionSequence'
   :: [PetriKey]
   -> [PetriKey]
   -> PetriLike Node PetriKey
+  -> [Int]  -- Activity Final node labels
   -> Bool
-validActionSequence' input actions petri =
+validActionSequence' input actions petri activityFinalLabels =
   let net = fromPetriLike petri
-      zeroState = State $ M.map (const 0) $ unState $ start net
-  in any (isJust . lookup zeroState) (levelsCheckAS input actions net)
-
-
-levelsCheckAS :: [PetriKey] -> [PetriKey] -> Net PetriKey PetriKey-> [[(State PetriKey, [PetriKey])]]
-levelsCheckAS input actions n =
-  let g h xs = M.toList $
+      -- Use all places in the network to create the zero state, not just the start state
+      allPlaces = S.toList $ places net
+      zeroState = State $ M.fromList [(p, 0) | p <- allPlaces]
+  in any (isJust . lookup zeroState) (levelsCheckAS input actions net activityFinalLabels)
+
+
+levelsCheckAS :: [PetriKey] -> [PetriKey] -> Net PetriKey PetriKey -> [Int] -> [[(State PetriKey, [PetriKey])]]
+levelsCheckAS input actions n activityFinalLabels =
+  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 by checking if it's an auxiliary node
+      -- with a label that matches an Activity Final node from the original diagram
+      isActivityFinalTransition t = case t of
+        AuxiliaryPetriNode nodeLabel -> nodeLabel `elem` activityFinalLabels
+        _ -> False
+      g h xs = M.toList $
         M.fromList $ do
           (x, p) <- xs
           (t, y) <- successors n x
           guard $ h t
-          return (y, t : p)
+          -- 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
diff --git a/test/Modelling/ActivityDiagram/ActionSequencesActivityFinalSpec.hs b/test/Modelling/ActivityDiagram/ActionSequencesActivityFinalSpec.hs
new file mode 100644
index 000000000..4ac7c65a5
--- /dev/null
+++ b/test/Modelling/ActivityDiagram/ActionSequencesActivityFinalSpec.hs
@@ -0,0 +1,63 @@
+module Modelling.ActivityDiagram.ActionSequencesActivityFinalSpec where
+
+import Modelling.ActivityDiagram.ActionSequences (generateActionSequence, 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 "simple diagram with Activity Final" $ do
+      it "generates a valid sequence ending at Activity Final" $
+        generateActionSequence testDiagramSimpleActivityFinal `shouldBe` ["A"]
+      it "validates a sequence ending at Activity Final" $
+        validActionSequence ["A"] testDiagramSimpleActivityFinal `shouldBe` True
+    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
+
+-- Simple diagram: Initial -> A -> Activity Final
+testDiagramSimpleActivityFinal :: UMLActivityDiagram
+testDiagramSimpleActivityFinal = UMLActivityDiagram
+  { nodes =
+    [ AdInitialNode { label = 1 }
+    , AdActionNode { label = 2, name = "A" }
+    , AdActivityFinalNode { label = 3 }
+    ]
+  , connections =
+    [ AdConnection { from = 1, to = 2, guard = "" }
+    , AdConnection { from = 2, to = 3, guard = "" }
+    ]
+  }
+
+-- 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
+    ]
+  }