Enhance validateBasePetriConfig with AdConfig-based bounds checking

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,

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],

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,

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

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

src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs

@@ -6,14 +6,63 @@ 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 ((<|>)))
 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
 

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