diff --git a/modelling-tasks.cabal b/modelling-tasks.cabal index 7ff7144a5..90daca81d 100644 --- a/modelling-tasks.cabal +++ b/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 diff --git a/src/Modelling/ActivityDiagram/ActionSequences.hs b/src/Modelling/ActivityDiagram/ActionSequences.hs index b391aa03c..e217adec8 100644 --- a/src/Modelling/ActivityDiagram/ActionSequences.hs +++ b/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 diff --git a/src/Modelling/ActivityDiagram/EnterAS.hs b/src/Modelling/ActivityDiagram/EnterAS.hs index 26a943fcb..4cd489d8c 100644 --- a/src/Modelling/ActivityDiagram/EnterAS.hs +++ b/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 diff --git a/src/Modelling/ActivityDiagram/SelectAS.hs b/src/Modelling/ActivityDiagram/SelectAS.hs index 29ced293a..5931d6471 100644 --- a/src/Modelling/ActivityDiagram/SelectAS.hs +++ b/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 diff --git a/test/Modelling/ActivityDiagram/ActionSequencesActivityFinalSpec.hs b/test/Modelling/ActivityDiagram/ActionSequencesActivityFinalSpec.hs new file mode 100644 index 000000000..41eb63cae --- /dev/null +++ b/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 + ] + }