diff --git a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs index 4e0366d81..2dc49c885 100644 --- a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs +++ b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs @@ -25,7 +25,7 @@ task2023_41 = FindAuxiliaryPetriNodesConfig { flowFinalNodes = 2, cycles = 0 }, - countOfPetriNodesBounds = (0, Nothing), + countOfPetriNodesBounds = (20, Just 26), -- generates successfully maxInstances = Just 2000, hideNodeNames = False, hideBranchConditions = True, @@ -51,7 +51,7 @@ task2023_42 = FindAuxiliaryPetriNodesConfig { flowFinalNodes = 0, cycles = 2 }, - countOfPetriNodesBounds = (0, Nothing), + countOfPetriNodesBounds = (23, Just 28), -- fails to generate, but works with (0, Nothing) and (22, Just 40) maxInstances = Just 2000, hideNodeNames = False, hideBranchConditions = True, @@ -77,7 +77,7 @@ task2024_47 = FindAuxiliaryPetriNodesConfig { flowFinalNodes = 2, cycles = 0 }, - countOfPetriNodesBounds = (21, Just 27), + countOfPetriNodesBounds = (23, Just 23), -- generates successfully; but (0, Just 22) times out with maxInstances = Nothing maxInstances = Just 2000, hideNodeNames = False, hideBranchConditions = True, @@ -103,7 +103,7 @@ task2024_48 = FindAuxiliaryPetriNodesConfig { flowFinalNodes = 0, cycles = 2 }, - countOfPetriNodesBounds = (31, Just 41), + countOfPetriNodesBounds = (33, Just 33), -- generates successfully; but (0, Just 32) times out with maxInstances = Nothing maxInstances = Just 2000, hideNodeNames = False, hideBranchConditions = True, diff --git a/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs b/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs index a7fa2713f..23abe4079 100644 --- a/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs +++ b/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs @@ -25,7 +25,7 @@ task2023_39 = MatchPetriConfig { flowFinalNodes = 2, cycles = 1 }, - countOfPetriNodesBounds = (0, Nothing), + countOfPetriNodesBounds = (25, Just 25), -- generates successfully, but (0, Just 24) times out with maxInstances = Nothing maxInstances = Just 10000, hideBranchConditions = True, petriLayout = [Fdp], @@ -54,8 +54,8 @@ task2023_40 = MatchPetriConfig { flowFinalNodes = 3, cycles = 3 }, - countOfPetriNodesBounds = (0, Nothing), - maxInstances = Just 2000, + countOfPetriNodesBounds = (28, Just 34), -- fails to generate, but works with (37, Just 37); value smaller than 37 leads to NoInstanceAvailable; and (0, Just 36) times out with maxInstances = Nothing + maxInstances = Just 2000, -- fails to generate with Nothing, it diverges hideBranchConditions = True, petriLayout = [Fdp], petriSvgHighlighting = True, @@ -99,7 +99,7 @@ task2024_70 = MatchPetriConfig { flowFinalNodes = 1, cycles = 0 }, - countOfPetriNodesBounds = (0, Nothing), + countOfPetriNodesBounds = (20, Just 30), -- fails to generate, even with (0, Nothing): NoInstanceAvailable maxInstances = Just 10000, hideBranchConditions = True, petriLayout = [Fdp], @@ -128,7 +128,7 @@ task2024_71 = MatchPetriConfig { flowFinalNodes = 3, cycles = 3 }, - countOfPetriNodesBounds = (0, Nothing), + countOfPetriNodesBounds = (28, Just 34), -- fails to generate: NoInstanceAvailable; diverges when (0, Nothing) maxInstances = Just 2000, hideBranchConditions = True, petriLayout = [Fdp], diff --git a/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs b/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs index 5f27f90c9..eaa85f6f4 100644 --- a/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs +++ b/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs @@ -25,7 +25,7 @@ task2023_37 = SelectPetriConfig { flowFinalNodes = 2, cycles = 1 }, - countOfPetriNodesBounds = (0, Nothing), + countOfPetriNodesBounds = (26, Just 26), -- generates successfully, but (0, Just 25) times out with maxInstances = Nothing maxInstances = Just 2000, hideNodeNames = False, hideBranchConditions = True, @@ -57,8 +57,8 @@ task2023_38 = SelectPetriConfig { flowFinalNodes = 2, cycles = 1 }, - countOfPetriNodesBounds = (0, Nothing), - maxInstances = Just 1, + countOfPetriNodesBounds = (17, Just 20), -- generates successfully + maxInstances = Just 2000, hideNodeNames = True, hideBranchConditions = True, hidePetriNodeLabels = True, @@ -99,7 +99,7 @@ task2024_44 = SelectPetriConfig { flowFinalNodes = 2, cycles = 1 }, - countOfPetriNodesBounds = (0, Nothing), + countOfPetriNodesBounds = (17, Just 19), -- generates successfully, but (0, Just 18) times out with maxInstances = Nothing maxInstances = Just 2000, hideNodeNames = True, hideBranchConditions = True, diff --git a/modelling-tasks.cabal b/modelling-tasks.cabal index 7ff7144a5..04d6efd8a 100644 --- a/modelling-tasks.cabal +++ b/modelling-tasks.cabal @@ -34,6 +34,7 @@ library exposed-modules: Modelling.ActivityDiagram.ActionSequences Modelling.ActivityDiagram.Alloy + Modelling.ActivityDiagram.Auxiliary.PetriValidation Modelling.ActivityDiagram.Auxiliary.Parser Modelling.ActivityDiagram.Config Modelling.ActivityDiagram.Datatype @@ -85,7 +86,6 @@ library Modelling.Types other-modules: Modelling.ActivityDiagram.Auxiliary.ActionSequences - Modelling.ActivityDiagram.Auxiliary.PetriValidation Modelling.Auxiliary.Diagrams Modelling.CdOd.Phrasing Modelling.CdOd.Phrasing.Common diff --git a/package.yaml b/package.yaml index a8d200e7d..add539e7b 100644 --- a/package.yaml +++ b/package.yaml @@ -82,6 +82,7 @@ library: exposed-modules: - Modelling.ActivityDiagram.ActionSequences - Modelling.ActivityDiagram.Alloy + - Modelling.ActivityDiagram.Auxiliary.PetriValidation - Modelling.ActivityDiagram.Auxiliary.Parser - Modelling.ActivityDiagram.Config - Modelling.ActivityDiagram.Datatype diff --git a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs index c8ab598fd..be189381b 100644 --- a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs +++ b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs @@ -6,7 +6,7 @@ module Modelling.ActivityDiagram.Auxiliary.PetriValidation ( ) where import qualified Modelling.ActivityDiagram.Config as Config ( - AdConfig (activityFinalNodes, flowFinalNodes, actionLimits, forkJoinPairs, cycles), + AdConfig (activityFinalNodes, flowFinalNodes, actionLimits, objectNodeLimits, forkJoinPairs, decisionMergePairs, cycles), ) import Control.Applicative (Alternative ((<|>))) @@ -14,6 +14,55 @@ import Data.GraphViz.Commands (GraphvizCommand(..)) import Data.Maybe (isJust, fromJust) import Data.String.Interpolate (iii) +-- | Calculate minimum number of Petri net nodes based on AdConfig values +calculateMinimumPetriNodes :: Config.AdConfig -> Int +calculateMinimumPetriNodes adConfig = + let + -- At least one initial node (always 1 place) + initialNodes = 1 + + -- Minimum action nodes (each action becomes a transition, plus places before/after) + minActionNodes = fst (Config.actionLimits adConfig) + + -- Minimum object nodes (each becomes a place) + minObjectNodes = fst (Config.objectNodeLimits adConfig) + + -- Final nodes (each becomes a place) + finalNodes = Config.activityFinalNodes adConfig + Config.flowFinalNodes adConfig + + -- Fork/Join pairs (each pair adds auxiliary nodes: roughly 2 nodes per pair) + forkJoinNodes = Config.forkJoinPairs adConfig * 2 + + -- Decision/Merge pairs (each pair adds auxiliary nodes: roughly 2 nodes per pair) + decisionMergeNodes = Config.decisionMergePairs adConfig * 2 + + in initialNodes + minActionNodes + minObjectNodes + finalNodes + forkJoinNodes + decisionMergeNodes + +-- | Calculate maximum number of Petri net nodes based on AdConfig values +calculateMaximumPetriNodes :: Config.AdConfig -> Int +calculateMaximumPetriNodes adConfig = + let + -- At least one initial node (always 1 place) + initialNodes = 1 + + -- Maximum action nodes + maxActionNodes = snd (Config.actionLimits adConfig) + + -- Maximum object nodes + maxObjectNodes = snd (Config.objectNodeLimits adConfig) + + -- Final nodes (each becomes a place) + finalNodes = Config.activityFinalNodes adConfig + Config.flowFinalNodes adConfig + + -- Standard nodes (excluding auxiliary nodes) + standardNodes = initialNodes + maxActionNodes + maxObjectNodes + finalNodes + + -- Auxiliary nodes from Fork/Join pairs, Decision/Merge pairs, and Cycles + -- Heuristic: about as many auxiliary nodes as standard nodes + auxiliaryNodes = standardNodes + + in standardNodes + auxiliaryNodes + -- | Base validation logic common to multiple Petri-based configurations validateBasePetriConfig :: Config.AdConfig @@ -35,6 +84,21 @@ validateBasePetriConfig adConfig countOfPetriNodesBounds maxInstances presenceOf | Just False <- presenceOfSinkTransitionsForFinals, fst (Config.actionLimits adConfig) + Config.forkJoinPairs adConfig < 1 = Just "The option 'presenceOfSinkTransitionsForFinals = Just False' can only be achieved if the number of Actions, Fork Nodes and Join Nodes together is positive" + | fst countOfPetriNodesBounds > 0 && fst countOfPetriNodesBounds < calculateMinimumPetriNodes adConfig + = Just [iii| + The minimum value of 'countOfPetriNodesBounds' (#{fst countOfPetriNodesBounds}) is too small. + Based on the AdConfig values, the minimum number of Petri net nodes should be at least #{calculateMinimumPetriNodes adConfig}. + This is calculated from: 1 initial node + #{fst (Config.actionLimits adConfig)} minimum action nodes + + #{fst (Config.objectNodeLimits adConfig)} minimum object nodes + + #{Config.activityFinalNodes adConfig + Config.flowFinalNodes adConfig} final nodes + + #{Config.forkJoinPairs adConfig * 2} fork/join auxiliary nodes + + #{Config.decisionMergePairs adConfig * 2} decision/merge auxiliary nodes. + |] + | Just high <- snd countOfPetriNodesBounds, high > calculateMaximumPetriNodes adConfig + = Just [iii| + The maximum value of 'countOfPetriNodesBounds' (#{high}) is too large. + Based on the AdConfig values, the maximum number of Petri net nodes should be at most #{calculateMaximumPetriNodes adConfig}. + |] | otherwise = Nothing diff --git a/test/Modelling/ActivityDiagram/SelectPetriSpec.hs b/test/Modelling/ActivityDiagram/SelectPetriSpec.hs index a92372806..d851fde72 100644 --- a/test/Modelling/ActivityDiagram/SelectPetriSpec.hs +++ b/test/Modelling/ActivityDiagram/SelectPetriSpec.hs @@ -5,7 +5,7 @@ import Modelling.ActivityDiagram.SelectPetri (SelectPetriConfig(..), checkSelect import Test.Hspec (Spec, describe, it, context, shouldBe, shouldSatisfy) import Data.Maybe (isJust) import Modelling.ActivityDiagram.Config ( - AdConfig (actionLimits, forkJoinPairs), + AdConfig (actionLimits, objectNodeLimits, forkJoinPairs, activityFinalNodes, flowFinalNodes), defaultAdConfig, ) @@ -25,3 +25,26 @@ spec = presenceOfSinkTransitionsForFinals = Just False } `shouldSatisfy` isJust + context "when countOfPetriNodesBounds minimum is too small for AdConfig" $ + it "returns validation error about minimum Petri net nodes" $ + checkSelectPetriConfig defaultSelectPetriConfig { + adConfig = defaultAdConfig { + actionLimits = (3, 5), + activityFinalNodes = 1, + flowFinalNodes = 0 + }, + countOfPetriNodesBounds = (1, Nothing) -- Too small for minimum calculation + } + `shouldSatisfy` isJust + context "when countOfPetriNodesBounds maximum is too small for AdConfig" $ + it "returns validation error about maximum Petri net nodes being too small" $ + checkSelectPetriConfig defaultSelectPetriConfig { + adConfig = defaultAdConfig { + actionLimits = (1, 5), -- Can achieve up to 5 actions + objectNodeLimits = (0, 3), -- Can achieve up to 3 objects + activityFinalNodes = 1, + flowFinalNodes = 0 + }, + countOfPetriNodesBounds = (1, Just 8) -- Too small - achievable is 1+5+3+1 = 10 standard + ~10 auxiliary = ~20 + } + `shouldSatisfy` isJust