From f76a951b6078ac435c68acf350f595353b9a8ee3 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 17 Sep 2025 09:23:29 +0000
Subject: [PATCH 01/22] Initial plan


From 228c86a58f20936741c65d760d75b12aa0961bad Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 17 Sep 2025 09:41:46 +0000
Subject: [PATCH 02/22] Enhance validateBasePetriConfig with AdConfig-based
 bounds checking

Co-authored-by: jvoigtlaender <5853832+jvoigtlaender@users.noreply.github.com>
---
 modelling-tasks.cabal                         |  2 +-
 package.yaml                                  |  1 +
 .../Auxiliary/PetriValidation.hs              | 32 ++++++++++++++++++-
 .../ActivityDiagram/SelectPetriSpec.hs        | 13 +++++++-
 4 files changed, 45 insertions(+), 3 deletions(-)

diff --git a/modelling-tasks.cabal b/modelling-tasks.cabal
index 110fa195d..e58ff0bc1 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.Util
       Modelling.ActivityDiagram.Auxiliary.Parser
       Modelling.ActivityDiagram.Config
@@ -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 fde56ad9b..cf456117e 100644
--- a/package.yaml
+++ b/package.yaml
@@ -78,6 +78,7 @@ library:
   exposed-modules:
     - Modelling.ActivityDiagram.ActionSequences
     - Modelling.ActivityDiagram.Alloy
+    - Modelling.ActivityDiagram.Auxiliary.PetriValidation
     - Modelling.ActivityDiagram.Auxiliary.Util
     - Modelling.ActivityDiagram.Auxiliary.Parser
     - Modelling.ActivityDiagram.Config
diff --git a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
index c8ab598fd..e65e47847 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,30 @@ 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
+
 -- | Base validation logic common to multiple Petri-based configurations
 validateBasePetriConfig
   :: Config.AdConfig
@@ -35,6 +59,12 @@ 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.
+      |]
   | otherwise
     = Nothing
 
diff --git a/test/Modelling/ActivityDiagram/SelectPetriSpec.hs b/test/Modelling/ActivityDiagram/SelectPetriSpec.hs
index a92372806..01a572946 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, forkJoinPairs, activityFinalNodes, flowFinalNodes),
   defaultAdConfig,
   )
 
@@ -25,3 +25,14 @@ 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

From de133730c2d4a60361bbf8dc00e7acee8eaa81f7 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 17 Sep 2025 09:53:53 +0000
Subject: [PATCH 03/22] Add upper bound validation to validateBasePetriConfig

Co-authored-by: jvoigtlaender <5853832+jvoigtlaender@users.noreply.github.com>
---
 .../Auxiliary/PetriValidation.hs              | 33 +++++++++++++++++++
 .../ActivityDiagram/SelectPetriSpec.hs        | 17 +++++++++-
 2 files changed, 49 insertions(+), 1 deletion(-)

diff --git a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
index e65e47847..c7ce2cdff 100644
--- a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
+++ b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
@@ -38,6 +38,33 @@ calculateMinimumPetriNodes adConfig =
     
   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 (each action becomes a transition, plus places before/after)
+    maxActionNodes = snd (Config.actionLimits adConfig)
+    
+    -- Maximum object nodes (each becomes a place)
+    maxObjectNodes = snd (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
+    
+    -- Cycles can add additional auxiliary nodes (rough estimate: 1 per cycle)
+    cycleNodes = Config.cycles adConfig
+    
+  in initialNodes + maxActionNodes + maxObjectNodes + finalNodes + forkJoinNodes + decisionMergeNodes + cycleNodes
+
 -- | Base validation logic common to multiple Petri-based configurations
 validateBasePetriConfig
   :: Config.AdConfig
@@ -65,6 +92,12 @@ validateBasePetriConfig adConfig countOfPetriNodesBounds maxInstances presenceOf
       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 > 0 && 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}.
+      This is calculated from: 1 initial node + ${snd (Config.actionLimits adConfig)} maximum action nodes + ${snd (Config.objectNodeLimits adConfig)} maximum 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 + ${Config.cycles adConfig} cycle auxiliary nodes.
+      |]
   | otherwise
     = Nothing
 
diff --git a/test/Modelling/ActivityDiagram/SelectPetriSpec.hs b/test/Modelling/ActivityDiagram/SelectPetriSpec.hs
index 01a572946..30ee47310 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, activityFinalNodes, flowFinalNodes),
+  AdConfig (actionLimits, objectNodeLimits, forkJoinPairs, decisionMergePairs, activityFinalNodes, flowFinalNodes, cycles),
   defaultAdConfig,
   )
 
@@ -36,3 +36,18 @@ spec =
           countOfPetriNodesBounds = (1, Nothing)  -- Too small for minimum calculation
           }
             `shouldSatisfy` isJust
+    context "when countOfPetriNodesBounds maximum is too large for AdConfig" $
+      it "returns validation error about maximum Petri net nodes" $
+        checkSelectPetriConfig defaultSelectPetriConfig {
+          adConfig = defaultAdConfig {
+            actionLimits = (1, 2),
+            objectNodeLimits = (0, 1),
+            forkJoinPairs = 1,
+            decisionMergePairs = 1,
+            activityFinalNodes = 1,
+            flowFinalNodes = 0,
+            cycles = 0
+            },
+          countOfPetriNodesBounds = (1, Just 50)  -- Too large for maximum calculation
+          }
+            `shouldSatisfy` isJust

From 651ee076e834cc38a0b4d2a571734dd4613eb419 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 17 Sep 2025 10:11:43 +0000
Subject: [PATCH 04/22] Fix EDITORCONFIG violations: remove trailing whitespace
 and fix line length

Co-authored-by: jvoigtlaender <5853832+jvoigtlaender@users.noreply.github.com>
---
 .../Auxiliary/PetriValidation.hs              | 47 +++++++++++--------
 1 file changed, 28 insertions(+), 19 deletions(-)

diff --git a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
index c7ce2cdff..25f262dbb 100644
--- a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
+++ b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
@@ -20,22 +20,22 @@ 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)  
+
+    -- 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
@@ -44,25 +44,25 @@ calculateMaximumPetriNodes adConfig =
   let
     -- At least one initial node (always 1 place)
     initialNodes = 1
-    
+
     -- Maximum action nodes (each action becomes a transition, plus places before/after)
     maxActionNodes = snd (Config.actionLimits adConfig)
-    
+
     -- Maximum object nodes (each becomes a place)
     maxObjectNodes = snd (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)  
+
+    -- Decision/Merge pairs (each pair adds auxiliary nodes: roughly 2 nodes per pair)
     decisionMergeNodes = Config.decisionMergePairs adConfig * 2
-    
+
     -- Cycles can add additional auxiliary nodes (rough estimate: 1 per cycle)
     cycleNodes = Config.cycles adConfig
-    
+
   in initialNodes + maxActionNodes + maxObjectNodes + finalNodes + forkJoinNodes + decisionMergeNodes + cycleNodes
 
 -- | Base validation logic common to multiple Petri-based configurations
@@ -88,15 +88,24 @@ validateBasePetriConfig adConfig countOfPetriNodesBounds maxInstances presenceOf
     = 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. 
+      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.
+      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 > 0 && high > calculateMaximumPetriNodes adConfig
     = Just [iii|
-      The maximum value of 'countOfPetriNodesBounds' (${high}) is too large. 
+      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}.
-      This is calculated from: 1 initial node + ${snd (Config.actionLimits adConfig)} maximum action nodes + ${snd (Config.objectNodeLimits adConfig)} maximum 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 + ${Config.cycles adConfig} cycle auxiliary nodes.
+      This is calculated from: 1 initial node + ${snd (Config.actionLimits adConfig)} maximum action nodes +
+      ${snd (Config.objectNodeLimits adConfig)} maximum 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 +
+      ${Config.cycles adConfig} cycle auxiliary nodes.
       |]
   | otherwise
     = Nothing

From 7800e8f660f86c5d7d424018c940cdc983365a57 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 17 Sep 2025 10:56:29 +0000
Subject: [PATCH 05/22] Fix string interpolation and make upper bound
 validation more lenient

Co-authored-by: jvoigtlaender <5853832+jvoigtlaender@users.noreply.github.com>
---
 .../Auxiliary/PetriValidation.hs              | 59 ++++++++++---------
 1 file changed, 32 insertions(+), 27 deletions(-)

diff --git a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
index 25f262dbb..335ef415f 100644
--- a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
+++ b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
@@ -12,7 +12,7 @@ import qualified Modelling.ActivityDiagram.Config as Config (
 import Control.Applicative (Alternative ((<|>)))
 import Data.GraphViz.Commands (GraphvizCommand(..))
 import Data.Maybe (isJust, fromJust)
-import Data.String.Interpolate (iii)
+import Data.String.Interpolate (i)
 
 -- | Calculate minimum number of Petri net nodes based on AdConfig values
 calculateMinimumPetriNodes :: Config.AdConfig -> Int
@@ -39,6 +39,7 @@ calculateMinimumPetriNodes adConfig =
   in initialNodes + minActionNodes + minObjectNodes + finalNodes + forkJoinNodes + decisionMergeNodes
 
 -- | Calculate maximum number of Petri net nodes based on AdConfig values
+-- This is a conservative upper bound estimate for validation purposes
 calculateMaximumPetriNodes :: Config.AdConfig -> Int
 calculateMaximumPetriNodes adConfig =
   let
@@ -46,7 +47,8 @@ calculateMaximumPetriNodes adConfig =
     initialNodes = 1
 
     -- Maximum action nodes (each action becomes a transition, plus places before/after)
-    maxActionNodes = snd (Config.actionLimits adConfig)
+    -- In practice, each action can create additional auxiliary places/transitions
+    maxActionNodes = snd (Config.actionLimits adConfig) * 3  -- More generous estimate
 
     -- Maximum object nodes (each becomes a place)
     maxObjectNodes = snd (Config.objectNodeLimits adConfig)
@@ -54,16 +56,19 @@ calculateMaximumPetriNodes 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
+    -- Fork/Join pairs (each pair adds auxiliary nodes: conservative estimate 4 per pair)
+    forkJoinNodes = Config.forkJoinPairs adConfig * 4
 
-    -- Decision/Merge pairs (each pair adds auxiliary nodes: roughly 2 nodes per pair)
-    decisionMergeNodes = Config.decisionMergePairs adConfig * 2
+    -- Decision/Merge pairs (each pair adds auxiliary nodes: conservative estimate 4 per pair)
+    decisionMergeNodes = Config.decisionMergePairs adConfig * 4
+
+    -- Cycles can add additional auxiliary nodes (conservative estimate: 3 per cycle)
+    cycleNodes = Config.cycles adConfig * 3
 
-    -- Cycles can add additional auxiliary nodes (rough estimate: 1 per cycle)
-    cycleNodes = Config.cycles adConfig
+    -- Additional buffer for complex conversions
+    conversionBuffer = 5
 
-  in initialNodes + maxActionNodes + maxObjectNodes + finalNodes + forkJoinNodes + decisionMergeNodes + cycleNodes
+  in initialNodes + maxActionNodes + maxObjectNodes + finalNodes + forkJoinNodes + decisionMergeNodes + cycleNodes + conversionBuffer
 
 -- | Base validation logic common to multiple Petri-based configurations
 validateBasePetriConfig
@@ -87,25 +92,25 @@ validateBasePetriConfig adConfig countOfPetriNodesBounds maxInstances presenceOf
     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 [i|
+      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 > 0 && 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}.
-      This is calculated from: 1 initial node + ${snd (Config.actionLimits adConfig)} maximum action nodes +
-      ${snd (Config.objectNodeLimits adConfig)} maximum 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 +
-      ${Config.cycles adConfig} cycle auxiliary nodes.
+    = Just [i|
+      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}.
+      This is a conservative estimate calculated from: 1 initial node + #{snd (Config.actionLimits adConfig) * 3} action-related nodes +
+      #{snd (Config.objectNodeLimits adConfig)} object nodes +
+      #{Config.activityFinalNodes adConfig + Config.flowFinalNodes adConfig} final nodes +
+      #{Config.forkJoinPairs adConfig * 4} fork/join auxiliary nodes +
+      #{Config.decisionMergePairs adConfig * 4} decision/merge auxiliary nodes +
+      #{Config.cycles adConfig * 3} cycle auxiliary nodes + 5 conversion buffer.
       |]
   | otherwise
     = Nothing
@@ -133,7 +138,7 @@ validatePetriConfig
   where
     validatePetriConfigSpecific
       | auxiliaryPetriNodeAbsent == Just True && Config.cycles adConfig > 0
-      = Just [iii|
+      = Just [i|
         Setting the parameter 'auxiliaryPetriNodeAbsent' to True
         prohibits having more than 0 cycles
         |]

From e64bef3cf62e594a628bd31b6876e6431af318c1 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 17 Sep 2025 12:19:13 +0000
Subject: [PATCH 06/22] Fix upper bound validation logic: only check if bounds
 are too small, not too large

Co-authored-by: jvoigtlaender <5853832+jvoigtlaender@users.noreply.github.com>
---
 .../Auxiliary/PetriValidation.hs              | 38 +++++++------------
 .../ActivityDiagram/SelectPetriSpec.hs        | 17 ++++-----
 2 files changed, 20 insertions(+), 35 deletions(-)

diff --git a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
index 335ef415f..193085720 100644
--- a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
+++ b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
@@ -39,36 +39,29 @@ calculateMinimumPetriNodes adConfig =
   in initialNodes + minActionNodes + minObjectNodes + finalNodes + forkJoinNodes + decisionMergeNodes
 
 -- | Calculate maximum number of Petri net nodes based on AdConfig values
--- This is a conservative upper bound estimate for validation purposes
 calculateMaximumPetriNodes :: Config.AdConfig -> Int
 calculateMaximumPetriNodes adConfig =
   let
     -- At least one initial node (always 1 place)
     initialNodes = 1
 
-    -- Maximum action nodes (each action becomes a transition, plus places before/after)
-    -- In practice, each action can create additional auxiliary places/transitions
-    maxActionNodes = snd (Config.actionLimits adConfig) * 3  -- More generous estimate
+    -- Maximum action nodes
+    maxActionNodes = snd (Config.actionLimits adConfig)
 
-    -- Maximum object nodes (each becomes a place)
+    -- Maximum object nodes
     maxObjectNodes = snd (Config.objectNodeLimits adConfig)
 
     -- Final nodes (each becomes a place)
     finalNodes = Config.activityFinalNodes adConfig + Config.flowFinalNodes adConfig
 
-    -- Fork/Join pairs (each pair adds auxiliary nodes: conservative estimate 4 per pair)
-    forkJoinNodes = Config.forkJoinPairs adConfig * 4
+    -- Standard nodes (excluding auxiliary nodes)
+    standardNodes = initialNodes + maxActionNodes + maxObjectNodes + finalNodes
 
-    -- Decision/Merge pairs (each pair adds auxiliary nodes: conservative estimate 4 per pair)
-    decisionMergeNodes = Config.decisionMergePairs adConfig * 4
+    -- Auxiliary nodes from Fork/Join pairs, Decision/Merge pairs, and Cycles
+    -- Heuristic: about as many auxiliary nodes as standard nodes
+    auxiliaryNodes = standardNodes
 
-    -- Cycles can add additional auxiliary nodes (conservative estimate: 3 per cycle)
-    cycleNodes = Config.cycles adConfig * 3
-
-    -- Additional buffer for complex conversions
-    conversionBuffer = 5
-
-  in initialNodes + maxActionNodes + maxObjectNodes + finalNodes + forkJoinNodes + decisionMergeNodes + cycleNodes + conversionBuffer
+  in standardNodes + auxiliaryNodes
 
 -- | Base validation logic common to multiple Petri-based configurations
 validateBasePetriConfig
@@ -101,16 +94,11 @@ validateBasePetriConfig adConfig countOfPetriNodesBounds maxInstances presenceOf
       #{Config.forkJoinPairs adConfig * 2} fork/join auxiliary nodes +
       #{Config.decisionMergePairs adConfig * 2} decision/merge auxiliary nodes.
       |]
-  | Just high <- snd countOfPetriNodesBounds, high > 0 && high > calculateMaximumPetriNodes adConfig
+  | Just high <- snd countOfPetriNodesBounds, high > 0 && high < calculateMaximumPetriNodes adConfig
     = Just [i|
-      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}.
-      This is a conservative estimate calculated from: 1 initial node + #{snd (Config.actionLimits adConfig) * 3} action-related nodes +
-      #{snd (Config.objectNodeLimits adConfig)} object nodes +
-      #{Config.activityFinalNodes adConfig + Config.flowFinalNodes adConfig} final nodes +
-      #{Config.forkJoinPairs adConfig * 4} fork/join auxiliary nodes +
-      #{Config.decisionMergePairs adConfig * 4} decision/merge auxiliary nodes +
-      #{Config.cycles adConfig * 3} cycle auxiliary nodes + 5 conversion buffer.
+      The maximum value of 'countOfPetriNodesBounds' (#{high}) is too small.
+      Based on the AdConfig values, the actually achievable number of Petri net nodes can be up to #{calculateMaximumPetriNodes adConfig}.
+      This means the upper bound should be at least #{calculateMaximumPetriNodes adConfig} to allow for all possible configurations.
       |]
   | otherwise
     = Nothing
diff --git a/test/Modelling/ActivityDiagram/SelectPetriSpec.hs b/test/Modelling/ActivityDiagram/SelectPetriSpec.hs
index 30ee47310..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, objectNodeLimits, forkJoinPairs, decisionMergePairs, activityFinalNodes, flowFinalNodes, cycles),
+  AdConfig (actionLimits, objectNodeLimits, forkJoinPairs, activityFinalNodes, flowFinalNodes),
   defaultAdConfig,
   )
 
@@ -36,18 +36,15 @@ spec =
           countOfPetriNodesBounds = (1, Nothing)  -- Too small for minimum calculation
           }
             `shouldSatisfy` isJust
-    context "when countOfPetriNodesBounds maximum is too large for AdConfig" $
-      it "returns validation error about maximum Petri net nodes" $
+    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, 2),
-            objectNodeLimits = (0, 1),
-            forkJoinPairs = 1,
-            decisionMergePairs = 1,
+            actionLimits = (1, 5),  -- Can achieve up to 5 actions
+            objectNodeLimits = (0, 3),  -- Can achieve up to 3 objects
             activityFinalNodes = 1,
-            flowFinalNodes = 0,
-            cycles = 0
+            flowFinalNodes = 0
             },
-          countOfPetriNodesBounds = (1, Just 50)  -- Too large for maximum calculation
+          countOfPetriNodesBounds = (1, Just 8)  -- Too small - achievable is 1+5+3+1 = 10 standard + ~10 auxiliary = ~20
           }
             `shouldSatisfy` isJust

From 3d776b51c3766e788d065cdb25bb56b06eb98f62 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 17 Sep 2025 19:55:43 +0000
Subject: [PATCH 07/22] Use iii for multi-line string interpolations instead of
 i

Co-authored-by: jvoigtlaender <5853832+jvoigtlaender@users.noreply.github.com>
---
 .../ActivityDiagram/Auxiliary/PetriValidation.hs          | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
index 193085720..1dac003a8 100644
--- a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
+++ b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
@@ -12,7 +12,7 @@ import qualified Modelling.ActivityDiagram.Config as Config (
 import Control.Applicative (Alternative ((<|>)))
 import Data.GraphViz.Commands (GraphvizCommand(..))
 import Data.Maybe (isJust, fromJust)
-import Data.String.Interpolate (i)
+import Data.String.Interpolate (iii)
 
 -- | Calculate minimum number of Petri net nodes based on AdConfig values
 calculateMinimumPetriNodes :: Config.AdConfig -> Int
@@ -85,7 +85,7 @@ validateBasePetriConfig adConfig countOfPetriNodesBounds maxInstances presenceOf
     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 [i|
+    = 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 +
@@ -95,7 +95,7 @@ validateBasePetriConfig adConfig countOfPetriNodesBounds maxInstances presenceOf
       #{Config.decisionMergePairs adConfig * 2} decision/merge auxiliary nodes.
       |]
   | Just high <- snd countOfPetriNodesBounds, high > 0 && high < calculateMaximumPetriNodes adConfig
-    = Just [i|
+    = Just [iii|
       The maximum value of 'countOfPetriNodesBounds' (#{high}) is too small.
       Based on the AdConfig values, the actually achievable number of Petri net nodes can be up to #{calculateMaximumPetriNodes adConfig}.
       This means the upper bound should be at least #{calculateMaximumPetriNodes adConfig} to allow for all possible configurations.
@@ -126,7 +126,7 @@ validatePetriConfig
   where
     validatePetriConfigSpecific
       | auxiliaryPetriNodeAbsent == Just True && Config.cycles adConfig > 0
-      = Just [i|
+      = Just [iii|
         Setting the parameter 'auxiliaryPetriNodeAbsent' to True
         prohibits having more than 0 cycles
         |]

From cb310623b15e606f284fb2168fbab573fe66a971 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 17 Sep 2025 20:36:19 +0000
Subject: [PATCH 08/22] Replace countOfPetriNodesBounds (0, Nothing) with
 calculated optimal bounds in examples

Co-authored-by: jvoigtlaender <5853832+jvoigtlaender@users.noreply.github.com>
---
 .../ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs     | 4 ++--
 .../src/Modelling/ActivityDiagram/MatchPetri/Config.hs    | 8 ++++----
 .../src/Modelling/ActivityDiagram/SelectPetri/Config.hs   | 6 +++---
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
index e9f56902b..606e43097 100644
--- a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
@@ -24,7 +24,7 @@ task2023_41 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 2,
     cycles = 0
     },
-  countOfPetriNodesBounds = (0, Nothing),
+  countOfPetriNodesBounds = (19, Just 26),
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,
@@ -50,7 +50,7 @@ task2023_42 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 0,
     cycles = 2
     },
-  countOfPetriNodesBounds = (0, Nothing),
+  countOfPetriNodesBounds = (22, Just 28),
   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 10f50f2f1..52c6a76d5 100644
--- a/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
@@ -24,7 +24,7 @@ task2023_39 = MatchPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (0, Nothing),
+  countOfPetriNodesBounds = (21, Just 30),
   maxInstances = Just 10000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -53,7 +53,7 @@ task2023_40 = MatchPetriConfig {
     flowFinalNodes = 3,
     cycles = 3
     },
-  countOfPetriNodesBounds = (0, Nothing),
+  countOfPetriNodesBounds = (27, Just 34),
   maxInstances = Just 2000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -98,7 +98,7 @@ task2024_70 = MatchPetriConfig {
     flowFinalNodes = 1,
     cycles = 0
     },
-  countOfPetriNodesBounds = (0, Nothing),
+  countOfPetriNodesBounds = (19, Just 30),
   maxInstances = Just 10000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -127,7 +127,7 @@ task2024_71 = MatchPetriConfig {
     flowFinalNodes = 3,
     cycles = 3
     },
-  countOfPetriNodesBounds = (0, Nothing),
+  countOfPetriNodesBounds = (27, Just 34),
   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 23cce10fc..498968663 100644
--- a/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs
@@ -24,7 +24,7 @@ task2023_37 = SelectPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (0, Nothing),
+  countOfPetriNodesBounds = (21, Just 26),
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,
@@ -56,7 +56,7 @@ task2023_38 = SelectPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (0, Nothing),
+  countOfPetriNodesBounds = (16, Just 20),
   maxInstances = Just 1,
   hideNodeNames = True,
   hideBranchConditions = True,
@@ -98,7 +98,7 @@ task2024_44 = SelectPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (0, Nothing),
+  countOfPetriNodesBounds = (16, Just 20),
   maxInstances = Just 2000,
   hideNodeNames = True,
   hideBranchConditions = True,

From f29be56ce46d16d6401ebe0f3f42c191357b4641 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Janis=20Voigtl=C3=A4nder?=
 <jvoigtlaender@users.noreply.github.com>
Date: Wed, 17 Sep 2025 23:33:45 +0200
Subject: [PATCH 09/22] "checking" whether the calculated bounds are really
 tight

---
 .../ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs         | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
index 606e43097..d0083c408 100644
--- a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
@@ -24,7 +24,7 @@ task2023_41 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 2,
     cycles = 0
     },
-  countOfPetriNodesBounds = (19, Just 26),
+  countOfPetriNodesBounds = (20, Just 26),
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,
@@ -50,7 +50,7 @@ task2023_42 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 0,
     cycles = 2
     },
-  countOfPetriNodesBounds = (22, Just 28),
+  countOfPetriNodesBounds = (22, Just 27),
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,

From e342669d6f1b256e688cc0c39d075bc0379cd7f3 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 17 Sep 2025 22:02:35 +0000
Subject: [PATCH 10/22] Tighten all countOfPetriNodesBounds in examples for
 more precise validation

Co-authored-by: jvoigtlaender <5853832+jvoigtlaender@users.noreply.github.com>
---
 .../ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs     | 4 ++--
 .../src/Modelling/ActivityDiagram/MatchPetri/Config.hs    | 8 ++++----
 .../src/Modelling/ActivityDiagram/SelectPetri/Config.hs   | 6 +++---
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
index d0083c408..97322b040 100644
--- a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
@@ -24,7 +24,7 @@ task2023_41 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 2,
     cycles = 0
     },
-  countOfPetriNodesBounds = (20, Just 26),
+  countOfPetriNodesBounds = (20, Just 25),
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,
@@ -50,7 +50,7 @@ task2023_42 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 0,
     cycles = 2
     },
-  countOfPetriNodesBounds = (22, Just 27),
+  countOfPetriNodesBounds = (23, Just 27),
   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 52c6a76d5..4ec800d44 100644
--- a/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
@@ -24,7 +24,7 @@ task2023_39 = MatchPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (21, Just 30),
+  countOfPetriNodesBounds = (22, Just 29),
   maxInstances = Just 10000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -53,7 +53,7 @@ task2023_40 = MatchPetriConfig {
     flowFinalNodes = 3,
     cycles = 3
     },
-  countOfPetriNodesBounds = (27, Just 34),
+  countOfPetriNodesBounds = (28, Just 33),
   maxInstances = Just 2000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -98,7 +98,7 @@ task2024_70 = MatchPetriConfig {
     flowFinalNodes = 1,
     cycles = 0
     },
-  countOfPetriNodesBounds = (19, Just 30),
+  countOfPetriNodesBounds = (20, Just 29),
   maxInstances = Just 10000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -127,7 +127,7 @@ task2024_71 = MatchPetriConfig {
     flowFinalNodes = 3,
     cycles = 3
     },
-  countOfPetriNodesBounds = (27, Just 34),
+  countOfPetriNodesBounds = (28, Just 33),
   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 498968663..5f6f7d73d 100644
--- a/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs
@@ -24,7 +24,7 @@ task2023_37 = SelectPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (21, Just 26),
+  countOfPetriNodesBounds = (22, Just 25),
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,
@@ -56,7 +56,7 @@ task2023_38 = SelectPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (16, Just 20),
+  countOfPetriNodesBounds = (17, Just 19),
   maxInstances = Just 1,
   hideNodeNames = True,
   hideBranchConditions = True,
@@ -98,7 +98,7 @@ task2024_44 = SelectPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (16, Just 20),
+  countOfPetriNodesBounds = (17, Just 19),
   maxInstances = Just 2000,
   hideNodeNames = True,
   hideBranchConditions = True,

From fd5a887d8a0dddafcb574a97129ab0a74f0a0ffd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Janis=20Voigtl=C3=A4nder?=
 <jvoigtlaender@users.noreply.github.com>
Date: Thu, 18 Sep 2025 07:35:28 +0200
Subject: [PATCH 11/22] Update countOfPetriNodesBounds upper limit

---
 example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs b/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs
index 5f6f7d73d..e09c4c8d7 100644
--- a/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs
@@ -24,7 +24,7 @@ task2023_37 = SelectPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (22, Just 25),
+  countOfPetriNodesBounds = (22, Just 26),
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,
@@ -56,7 +56,7 @@ task2023_38 = SelectPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (17, Just 19),
+  countOfPetriNodesBounds = (17, Just 20),
   maxInstances = Just 1,
   hideNodeNames = True,
   hideBranchConditions = True,

From 77e0824cb8903b66a4c80b5e5e2bd6d74c3f7342 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Janis=20Voigtl=C3=A4nder?=
 <jvoigtlaender@users.noreply.github.com>
Date: Thu, 18 Sep 2025 07:37:09 +0200
Subject: [PATCH 12/22] Update countOfPetriNodesBounds values

---
 example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs b/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
index 4ec800d44..7adf41741 100644
--- a/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
@@ -24,7 +24,7 @@ task2023_39 = MatchPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (22, Just 29),
+  countOfPetriNodesBounds = (22, Just 30),
   maxInstances = Just 10000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -53,7 +53,7 @@ task2023_40 = MatchPetriConfig {
     flowFinalNodes = 3,
     cycles = 3
     },
-  countOfPetriNodesBounds = (28, Just 33),
+  countOfPetriNodesBounds = (28, Just 34),
   maxInstances = Just 2000,
   hideBranchConditions = True,
   petriLayout = [Fdp],

From bf46f4caa8de7ee748246f855a4d974ca831067d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Janis=20Voigtl=C3=A4nder?=
 <jvoigtlaender@users.noreply.github.com>
Date: Thu, 18 Sep 2025 07:38:09 +0200
Subject: [PATCH 13/22] Update countOfPetriNodesBounds upper limits

---
 .../ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs         | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
index 97322b040..77a90e4a3 100644
--- a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
@@ -24,7 +24,7 @@ task2023_41 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 2,
     cycles = 0
     },
-  countOfPetriNodesBounds = (20, Just 25),
+  countOfPetriNodesBounds = (20, Just 26),
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,
@@ -50,7 +50,7 @@ task2023_42 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 0,
     cycles = 2
     },
-  countOfPetriNodesBounds = (23, Just 27),
+  countOfPetriNodesBounds = (23, Just 28),
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,

From 917a416b970f933a695187acc08d058cdef6ab22 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Janis=20Voigtl=C3=A4nder?=
 <jvoigtlaender@users.noreply.github.com>
Date: Thu, 18 Sep 2025 08:17:08 +0200
Subject: [PATCH 14/22] Update countOfPetriNodesBounds upper limit to 20

---
 example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs b/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs
index e09c4c8d7..13ac876b8 100644
--- a/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs
@@ -98,7 +98,7 @@ task2024_44 = SelectPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (17, Just 19),
+  countOfPetriNodesBounds = (17, Just 20),
   maxInstances = Just 2000,
   hideNodeNames = True,
   hideBranchConditions = True,

From 1e931af0d463074259b9eb46c6dda029ca828124 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Janis=20Voigtl=C3=A4nder?=
 <jvoigtlaender@users.noreply.github.com>
Date: Thu, 18 Sep 2025 08:17:54 +0200
Subject: [PATCH 15/22] Update countOfPetriNodesBounds values in Config.hs

---
 example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs b/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
index 7adf41741..2e072931d 100644
--- a/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
@@ -98,7 +98,7 @@ task2024_70 = MatchPetriConfig {
     flowFinalNodes = 1,
     cycles = 0
     },
-  countOfPetriNodesBounds = (20, Just 29),
+  countOfPetriNodesBounds = (20, Just 30),
   maxInstances = Just 10000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -127,7 +127,7 @@ task2024_71 = MatchPetriConfig {
     flowFinalNodes = 3,
     cycles = 3
     },
-  countOfPetriNodesBounds = (28, Just 33),
+  countOfPetriNodesBounds = (28, Just 34),
   maxInstances = Just 2000,
   hideBranchConditions = True,
   petriLayout = [Fdp],

From c6908d112b7989b89ef9b9f07819c3cf069eedd3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Janis=20Voigtl=C3=A4nder?=
 <jvoigtlaender@users.noreply.github.com>
Date: Wed, 28 Jan 2026 11:54:09 +0100
Subject: [PATCH 16/22] record empirical findings

---
 .../ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs     | 4 ++--
 .../src/Modelling/ActivityDiagram/MatchPetri/Config.hs    | 8 ++++----
 .../src/Modelling/ActivityDiagram/SelectPetri/Config.hs   | 8 ++++----
 3 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
index f61214dd4..d7370728a 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 = (20, Just 26),
+  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 = (23, Just 28),
+  countOfPetriNodesBounds = (23, Just 28),  -- fails to generate, but works with (0, 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 a4b535d3c..c6a2fb546 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 = (22, Just 30),
+  countOfPetriNodesBounds = (22, Just 30),  -- generates successfully
   maxInstances = Just 10000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -54,7 +54,7 @@ task2023_40 = MatchPetriConfig {
     flowFinalNodes = 3,
     cycles = 3
     },
-  countOfPetriNodesBounds = (28, Just 34),
+  countOfPetriNodesBounds = (28, Just 34),  -- fails to generate, but works with (0, Nothing)
   maxInstances = Just 2000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -99,7 +99,7 @@ task2024_70 = MatchPetriConfig {
     flowFinalNodes = 1,
     cycles = 0
     },
-  countOfPetriNodesBounds = (20, Just 30),
+  countOfPetriNodesBounds = (20, Just 30),  -- fails to generate
   maxInstances = Just 10000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -128,7 +128,7 @@ task2024_71 = MatchPetriConfig {
     flowFinalNodes = 3,
     cycles = 3
     },
-  countOfPetriNodesBounds = (28, Just 34),
+  countOfPetriNodesBounds = (28, Just 34),  -- fails to generate
   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 36787005c..b6829dece 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 = (22, Just 26),
+  countOfPetriNodesBounds = (22, Just 26),  -- generates successfully
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,
@@ -57,8 +57,8 @@ task2023_38 = SelectPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (17, Just 20),
-  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 = (17, Just 20),
+  countOfPetriNodesBounds = (17, Just 20),  -- generates successfully
   maxInstances = Just 2000,
   hideNodeNames = True,
   hideBranchConditions = True,

From d011ca2add41a23d35da0ab54eb411901a026314 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Janis=20Voigtl=C3=A4nder?=
 <jvoigtlaender@users.noreply.github.com>
Date: Fri, 30 Jan 2026 13:20:23 +0100
Subject: [PATCH 17/22] record newer findings

---
 .../ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs       | 2 +-
 example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs  | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
index d7370728a..516e90aeb 100644
--- a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
@@ -51,7 +51,7 @@ task2023_42 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 0,
     cycles = 2
     },
-  countOfPetriNodesBounds = (23, Just 28),  -- fails to generate, but works with (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,
diff --git a/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs b/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
index c6a2fb546..b2b00eaa7 100644
--- a/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
@@ -54,7 +54,7 @@ task2023_40 = MatchPetriConfig {
     flowFinalNodes = 3,
     cycles = 3
     },
-  countOfPetriNodesBounds = (28, Just 34),  -- fails to generate, but works with (0, Nothing)
+  countOfPetriNodesBounds = (28, Just 34),  -- fails to generate, but works with (0, Nothing) and (28, Just 46)
   maxInstances = Just 2000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -99,7 +99,7 @@ task2024_70 = MatchPetriConfig {
     flowFinalNodes = 1,
     cycles = 0
     },
-  countOfPetriNodesBounds = (20, Just 30),  -- fails to generate
+  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 = (28, Just 34),  -- fails to generate
+  countOfPetriNodesBounds = (28, Just 34),  -- fails to generate: NoInstanceAvailable; diverges when (0, Nothing)
   maxInstances = Just 2000,
   hideBranchConditions = True,
   petriLayout = [Fdp],

From 34fa29765585815576bc578da812971dd05dab59 Mon Sep 17 00:00:00 2001
From: Zixin Wu <zixin.wu@uni-due.de>
Date: Mon, 2 Feb 2026 13:17:11 +0100
Subject: [PATCH 18/22] record some empirical results

---
 .../ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs         | 4 ++--
 example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs    | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
index 516e90aeb..3a9673a02 100644
--- a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
@@ -77,7 +77,7 @@ task2024_47 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 2,
     cycles = 0
     },
-  countOfPetriNodesBounds = (21, Just 27),
+  countOfPetriNodesBounds = (21, Just 27), -- generates successfully
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,
@@ -103,7 +103,7 @@ task2024_48 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 0,
     cycles = 2
     },
-  countOfPetriNodesBounds = (31, Just 41),
+  countOfPetriNodesBounds = (31, Just 41), -- generates successfully
   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 b2b00eaa7..5c9c065fe 100644
--- a/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs
@@ -55,7 +55,7 @@ task2023_40 = MatchPetriConfig {
     cycles = 3
     },
   countOfPetriNodesBounds = (28, Just 34),  -- fails to generate, but works with (0, Nothing) and (28, Just 46)
-  maxInstances = Just 2000,
+  maxInstances = Just 2000, -- fails to generate with Nothing, it diverges
   hideBranchConditions = True,
   petriLayout = [Fdp],
   petriSvgHighlighting = True,

From ae9b8f7fa65cefa14cbee04c249526c2fd8c9d83 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Janis=20Voigtl=C3=A4nder?=
 <jvoigtlaender@users.noreply.github.com>
Date: Tue, 3 Feb 2026 11:35:49 +0100
Subject: [PATCH 19/22] more recording from experiments

---
 .../ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs         | 4 ++--
 example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs    | 4 ++--
 example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs   | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
index 3a9673a02..af5cc962f 100644
--- a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
@@ -77,7 +77,7 @@ task2024_47 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 2,
     cycles = 0
     },
-  countOfPetriNodesBounds = (21, Just 27), -- generates successfully
+  countOfPetriNodesBounds = (23, Just 23), -- generates successfully; smaller upper bound than 23 leads to NoInstanceAvailable
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,
@@ -103,7 +103,7 @@ task2024_48 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 0,
     cycles = 2
     },
-  countOfPetriNodesBounds = (31, Just 41), -- generates successfully
+  countOfPetriNodesBounds = (33, Just 33), -- generates successfully; smaller upper bound than 33 leads to NoInstanceAvailable
   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 5c9c065fe..dbbba164c 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 = (22, Just 30),  -- generates successfully
+  countOfPetriNodesBounds = (25, Just 25),  -- generates successfully, but smaller upper bound leads to NoInstanceAvailable
   maxInstances = Just 10000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -54,7 +54,7 @@ task2023_40 = MatchPetriConfig {
     flowFinalNodes = 3,
     cycles = 3
     },
-  countOfPetriNodesBounds = (28, Just 34),  -- fails to generate, but works with (0, Nothing) and (28, Just 46)
+  countOfPetriNodesBounds = (28, Just 34),  -- fails to generate, but works with (0, Nothing) and (28, Just 46) as well as (37, Just 37); upper bound smaller than 37 leads to NoInstanceAvailable
   maxInstances = Just 2000, -- fails to generate with Nothing, it diverges
   hideBranchConditions = True,
   petriLayout = [Fdp],
diff --git a/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs b/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs
index b6829dece..e9bfaf6bd 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 = (22, Just 26),  -- generates successfully
+  countOfPetriNodesBounds = (26, Just 26),  -- generates successfully, but smaller upper bound leads to NoInstanceAvailable
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,
@@ -99,7 +99,7 @@ task2024_44 = SelectPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (17, Just 20),  -- generates successfully
+  countOfPetriNodesBounds = (17, Just 19),  -- generates successfully, but with upper bound smaller than 19 leads to NoInstanceAvailable
   maxInstances = Just 2000,
   hideNodeNames = True,
   hideBranchConditions = True,

From 3606cb403300beadbaeb615d7d12cae09929ae7a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Janis=20Voigtl=C3=A4nder?=
 <jvoigtlaender@users.noreply.github.com>
Date: Tue, 3 Feb 2026 16:12:15 +0100
Subject: [PATCH 20/22] Fix condition for Petri nodes bounds validation

---
 src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
index 1dac003a8..be189381b 100644
--- a/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
+++ b/src/Modelling/ActivityDiagram/Auxiliary/PetriValidation.hs
@@ -94,11 +94,10 @@ validateBasePetriConfig adConfig countOfPetriNodesBounds maxInstances presenceOf
       #{Config.forkJoinPairs adConfig * 2} fork/join auxiliary nodes +
       #{Config.decisionMergePairs adConfig * 2} decision/merge auxiliary nodes.
       |]
-  | Just high <- snd countOfPetriNodesBounds, high > 0 && high < calculateMaximumPetriNodes adConfig
+  | Just high <- snd countOfPetriNodesBounds, high > calculateMaximumPetriNodes adConfig
     = Just [iii|
-      The maximum value of 'countOfPetriNodesBounds' (#{high}) is too small.
-      Based on the AdConfig values, the actually achievable number of Petri net nodes can be up to #{calculateMaximumPetriNodes adConfig}.
-      This means the upper bound should be at least #{calculateMaximumPetriNodes adConfig} to allow for all possible configurations.
+      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

From 31e4cf40f6c5ac8da89e80f9e80a8ec3c4001a04 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Janis=20Voigtl=C3=A4nder?=
 <jvoigtlaender@users.noreply.github.com>
Date: Wed, 4 Feb 2026 17:32:20 +0100
Subject: [PATCH 21/22] more precise statements

---
 .../ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs         | 4 ++--
 example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs    | 4 ++--
 example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs   | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
index 28b152a75..cea50b141 100644
--- a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
@@ -77,7 +77,7 @@ task2024_47 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 2,
     cycles = 0
     },
-  countOfPetriNodesBounds = (23, Just 23), -- generates successfully; smaller upper bound than 23 leads to NoInstanceAvailable
+  countOfPetriNodesBounds = (23, Just 23), -- generates successfully; smaller value than 23 leads to NoInstanceAvailable
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,
@@ -103,7 +103,7 @@ task2024_48 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 0,
     cycles = 2
     },
-  countOfPetriNodesBounds = (33, Just 33), -- generates successfully; smaller upper bound than 33 leads to NoInstanceAvailable
+  countOfPetriNodesBounds = (33, Just 33), -- generates successfully; smaller value than 33 leads to NoInstanceAvailable
   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 523fa2548..814286458 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 = (25, Just 25),  -- generates successfully, but smaller upper bound leads to NoInstanceAvailable
+  countOfPetriNodesBounds = (25, Just 25),  -- generates successfully, but smaller value than 25 leads to NoInstanceAvailable
   maxInstances = Just 10000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -54,7 +54,7 @@ task2023_40 = MatchPetriConfig {
     flowFinalNodes = 3,
     cycles = 3
     },
-  countOfPetriNodesBounds = (28, Just 34),  -- fails to generate, but works with (0, Nothing) and (28, Just 46) as well as (37, Just 37); upper bound smaller than 37 leads to NoInstanceAvailable
+  countOfPetriNodesBounds = (28, Just 34),  -- fails to generate, but works with (37, Just 37); value smaller than 37 leads to NoInstanceAvailable
   maxInstances = Just 2000, -- fails to generate with Nothing, it diverges
   hideBranchConditions = True,
   petriLayout = [Fdp],
diff --git a/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs b/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs
index b92a04ac0..8a1a52959 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 = (26, Just 26),  -- generates successfully, but smaller upper bound leads to NoInstanceAvailable
+  countOfPetriNodesBounds = (26, Just 26),  -- generates successfully, but smaller value than 26 leads to NoInstanceAvailable
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,

From ae2e60f0ead1dbf22fb8531a3853e3bd8a41a56a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Janis=20Voigtl=C3=A4nder?=
 <jvoigtlaender@users.noreply.github.com>
Date: Thu, 5 Feb 2026 16:10:16 +0100
Subject: [PATCH 22/22] record new information

---
 .../ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs         | 4 ++--
 example/src/Modelling/ActivityDiagram/MatchPetri/Config.hs    | 4 ++--
 example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs   | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
index cea50b141..a0301527b 100644
--- a/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
+++ b/example/src/Modelling/ActivityDiagram/FindAuxiliaryPetriNodes/Config.hs
@@ -77,7 +77,7 @@ task2024_47 = FindAuxiliaryPetriNodesConfig {
     flowFinalNodes = 2,
     cycles = 0
     },
-  countOfPetriNodesBounds = (23, Just 23), -- generates successfully; smaller value than 23 leads to NoInstanceAvailable
+  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 = (33, Just 33), -- generates successfully; smaller value than 33 leads to NoInstanceAvailable
+  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 814286458..99e119ece 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 = (25, Just 25),  -- generates successfully, but smaller value than 25 leads to NoInstanceAvailable
+  countOfPetriNodesBounds = (25, Just 25),  -- generates successfully, but (0, Just 24) times out with maxInstances = Nothing
   maxInstances = Just 10000,
   hideBranchConditions = True,
   petriLayout = [Fdp],
@@ -54,7 +54,7 @@ task2023_40 = MatchPetriConfig {
     flowFinalNodes = 3,
     cycles = 3
     },
-  countOfPetriNodesBounds = (28, Just 34),  -- fails to generate, but works with (37, Just 37); value smaller than 37 leads to NoInstanceAvailable
+  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],
diff --git a/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs b/example/src/Modelling/ActivityDiagram/SelectPetri/Config.hs
index 8a1a52959..4d6a62a34 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 = (26, Just 26),  -- generates successfully, but smaller value than 26 leads to NoInstanceAvailable
+  countOfPetriNodesBounds = (26, Just 26),  -- generates successfully, but (0, Just 25) times out with maxInstances = Nothing
   maxInstances = Just 2000,
   hideNodeNames = False,
   hideBranchConditions = True,
@@ -99,7 +99,7 @@ task2024_44 = SelectPetriConfig {
     flowFinalNodes = 2,
     cycles = 1
     },
-  countOfPetriNodesBounds = (17, Just 19),  -- generates successfully, but with upper bound smaller than 19 leads to NoInstanceAvailable
+  countOfPetriNodesBounds = (17, Just 19),  -- generates successfully, but (0, Just 18) times out with maxInstances = Nothing
   maxInstances = Just 2000,
   hideNodeNames = True,
   hideBranchConditions = True,