{-# LANGUAGE RecordWildCards #-}

-- | Common validation logic for Petri Net configurations (Deadlock and Reach)
module Modelling.PetriNet.Reach.ConfigValidation (
  checkBasicPetriConfig,
  checkRange,
  checkPetriNetSizes,
  checkTransitionLengths,
  checkRejectLongerThanConsistency,
  checkCapacity,
  checkTransitionBehaviorConstraints,
  checkFilterConfigWith,
  checkArrowDensityCrossValidation
) where

import Control.Applicative (Alternative ((<|>)))
import Data.GraphViz.Commands (GraphvizCommand)
import Data.List.Extra (notNull)
import Data.Maybe (fromMaybe, isJust, isNothing)
import Modelling.PetriNet.Reach.Filter (
  FilterConfig (..),
  noFiltering,
  )
import Modelling.PetriNet.Reach.Type (Capacity(..), TransitionBehaviorConstraints(..), ArrowDensityConstraints(..))

-- | Check that a range (low, high) is valid
checkRange
  :: (Num n, Ord n, Show n)
  => String          -- ^ Description of what is being checked
  -> (n, Maybe n)    -- ^ (lower bound, upper bound)
  -> Maybe String
checkRange :: forall n.
(Num n, Ord n, Show n) =>
String -> (n, Maybe n) -> Maybe String
checkRange String
what (n
low, Maybe n
h)
  | n
low n -> n -> Bool
forall a. Ord a => a -> a -> Bool
< n
0 = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"The lower limit for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
what String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" has to be at least 0!"
  | Bool
otherwise = case Maybe n
h of
      Maybe n
Nothing -> Maybe String
forall a. Maybe a
Nothing  -- No upper bound specified, only check lower bound
      Just n
high ->
        if n
high n -> n -> Bool
forall a. Ord a => a -> a -> Bool
< n
low
        then String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"The upper limit (currently " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe n -> String
forall a. Show a => a -> String
show Maybe n
h String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"; second value) for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
what String -> String -> String
forall a. [a] -> [a] -> [a]
++
                   String
" has to be at least as high as its lower limit (currently " String -> String -> String
forall a. [a] -> [a] -> [a]
++ n -> String
forall a. Show a => a -> String
show n
low String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"; first value)!"
        else Maybe String
forall a. Maybe a
Nothing

-- | Check basic Petri net size constraints
checkPetriNetSizes :: Int -> Int -> Maybe String
checkPetriNetSizes :: Int -> Int -> Maybe String
checkPetriNetSizes Int
numPlaces Int
numTransitions
  | Int
numPlaces Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> Maybe String
forall a. a -> Maybe a
Just String
"numPlaces must be positive"
  | Int
numTransitions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> Maybe String
forall a. a -> Maybe a
Just String
"numTransitions must be positive"
  | Bool
otherwise = Maybe String
forall a. Maybe a
Nothing

-- | Check transition length constraints
checkTransitionLengths :: Int -> Int -> Maybe String
checkTransitionLengths :: Int -> Int -> Maybe String
checkTransitionLengths Int
minTransitionLength Int
maxTransitionLength
  | Int
minTransitionLength Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> Maybe String
forall a. a -> Maybe a
Just String
"minTransitionLength must be positive"
  | Int
minTransitionLength Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxTransitionLength = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
    String
"minTransitionLength (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
minTransitionLength String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") cannot be greater than maxTransitionLength (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
maxTransitionLength String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  | Bool
otherwise = Maybe String
forall a. Maybe a
Nothing

-- | Check that capacity is set to Unbounded
checkCapacity :: Capacity s -> Maybe String
checkCapacity :: forall s. Capacity s -> Maybe String
checkCapacity Capacity s
Unbounded = Maybe String
forall a. Maybe a
Nothing
checkCapacity Capacity s
_ = String -> Maybe String
forall a. a -> Maybe a
Just String
"Other choices for 'capacity' than 'Unbounded' are not currently supported for this task type."

-- | Check consistency between rejectLongerThan and other length parameters
checkRejectLongerThanConsistency :: Maybe Int -> Int -> Bool -> Maybe String
checkRejectLongerThanConsistency :: Maybe Int -> Int -> Bool -> Maybe String
checkRejectLongerThanConsistency Maybe Int
rejectLongerThan Int
maxTransitionLength Bool
showLengthHint =
  case Maybe Int
rejectLongerThan of
    Just Int
rejectLength
      | Int
rejectLength Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 -> String -> Maybe String
forall a. a -> Maybe a
Just String
"rejectLongerThan must be positive when specified"
      | Int
rejectLength Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
maxTransitionLength -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$
        String
"rejectLongerThan (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
rejectLength String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") cannot be less than maxTransitionLength (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
maxTransitionLength String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      | Int
rejectLength Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
maxTransitionLength Bool -> Bool -> Bool
&& Bool
showLengthHint -> String -> Maybe String
forall a. a -> Maybe a
Just String
"showLengthHint == True does not make sense when rejectLongerThan equals maxTransitionLength"
      | Bool
otherwise -> Maybe String
forall a. Maybe a
Nothing
    Maybe Int
Nothing -> Maybe String
forall a. Maybe a
Nothing

-- | Check basic Petri net configuration including sizes, lengths, ranges, capacity and draw commands
checkBasicPetriConfig
  :: Int                      -- ^ numPlaces
  -> Int                      -- ^ numTransitions
  -> Capacity s               -- ^ capacity
  -> Int                      -- ^ minTransitionLength
  -> Int                      -- ^ maxTransitionLength
  -> TransitionBehaviorConstraints -- ^ transitionBehaviorConstraints
  -> ArrowDensityConstraints  -- ^ arrowDensityConstraints
  -> [GraphvizCommand]        -- ^ drawCommands
  -> Maybe Int                -- ^ rejectLongerThan
  -> Bool                     -- ^ showLengthHint
  -> Maybe String
checkBasicPetriConfig :: forall s.
Int
-> Int
-> Capacity s
-> Int
-> Int
-> TransitionBehaviorConstraints
-> ArrowDensityConstraints
-> [GraphvizCommand]
-> Maybe Int
-> Bool
-> Maybe String
checkBasicPetriConfig
  Int
numPlaces
  Int
numTransitions
  Capacity s
capacity
  Int
minTransitionLength
  Int
maxTransitionLength
  TransitionBehaviorConstraints
transitionBehaviorConstraints
  ArrowDensityConstraints
arrowDensityConstraints
  [GraphvizCommand]
drawCommands
  Maybe Int
rejectLongerThan
  Bool
showLengthHint =
    Int -> Int -> Maybe String
checkPetriNetSizes Int
numPlaces Int
numTransitions
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Capacity s -> Maybe String
forall s. Capacity s -> Maybe String
checkCapacity Capacity s
capacity
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> Int -> Maybe String
checkTransitionLengths Int
minTransitionLength Int
maxTransitionLength
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int
-> Int
-> ArrowDensityConstraints
-> TransitionBehaviorConstraints
-> Maybe String
checkTransitionBehaviorConstraints
          Int
numPlaces
          Int
numTransitions
          ArrowDensityConstraints
arrowDensityConstraints
          TransitionBehaviorConstraints
transitionBehaviorConstraints
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> (Int, Maybe Int) -> Maybe String
forall n.
(Num n, Ord n, Show n) =>
String -> (n, Maybe n) -> Maybe String
checkRange String
"incomingArrowsPerTransition" (ArrowDensityConstraints -> (Int, Maybe Int)
incomingArrowsPerTransition ArrowDensityConstraints
arrowDensityConstraints)
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> (Int, Maybe Int) -> Maybe String
forall n.
(Num n, Ord n, Show n) =>
String -> (n, Maybe n) -> Maybe String
checkRange String
"outgoingArrowsPerTransition" (ArrowDensityConstraints -> (Int, Maybe Int)
outgoingArrowsPerTransition ArrowDensityConstraints
arrowDensityConstraints)
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> (Int, Maybe Int) -> Maybe String
forall n.
(Num n, Ord n, Show n) =>
String -> (n, Maybe n) -> Maybe String
checkRange String
"incomingArrowsPerPlace" (ArrowDensityConstraints -> (Int, Maybe Int)
incomingArrowsPerPlace ArrowDensityConstraints
arrowDensityConstraints)
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> (Int, Maybe Int) -> Maybe String
forall n.
(Num n, Ord n, Show n) =>
String -> (n, Maybe n) -> Maybe String
checkRange String
"outgoingArrowsPerPlace" (ArrowDensityConstraints -> (Int, Maybe Int)
outgoingArrowsPerPlace ArrowDensityConstraints
arrowDensityConstraints)
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> (Int, Maybe Int) -> Maybe String
forall n.
(Num n, Ord n, Show n) =>
String -> (n, Maybe n) -> Maybe String
checkRange String
"totalArrowsFromPlacesToTransitions" (ArrowDensityConstraints -> (Int, Maybe Int)
totalArrowsFromPlacesToTransitions ArrowDensityConstraints
arrowDensityConstraints)
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> (Int, Maybe Int) -> Maybe String
forall n.
(Num n, Ord n, Show n) =>
String -> (n, Maybe n) -> Maybe String
checkRange String
"totalArrowsFromTransitionsToPlaces" (ArrowDensityConstraints -> (Int, Maybe Int)
totalArrowsFromTransitionsToPlaces ArrowDensityConstraints
arrowDensityConstraints)
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Int -> String -> (Int, Maybe Int) -> Maybe String
forall {a}.
(Ord a, Show a) =>
String -> a -> String -> (a, Maybe a) -> Maybe String
checkRangeVersusCount String
"numPlaces" Int
numPlaces String
"incomingArrowsPerTransition"
          (ArrowDensityConstraints -> (Int, Maybe Int)
incomingArrowsPerTransition ArrowDensityConstraints
arrowDensityConstraints)
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Int -> String -> (Int, Maybe Int) -> Maybe String
forall {a}.
(Ord a, Show a) =>
String -> a -> String -> (a, Maybe a) -> Maybe String
checkRangeVersusCount String
"numPlaces" Int
numPlaces String
"outgoingArrowsPerTransition"
          (ArrowDensityConstraints -> (Int, Maybe Int)
outgoingArrowsPerTransition ArrowDensityConstraints
arrowDensityConstraints)
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Int -> String -> (Int, Maybe Int) -> Maybe String
forall {a}.
(Ord a, Show a) =>
String -> a -> String -> (a, Maybe a) -> Maybe String
checkRangeVersusCount String
"numTransitions" Int
numTransitions String
"incomingArrowsPerPlace"
          (ArrowDensityConstraints -> (Int, Maybe Int)
incomingArrowsPerPlace ArrowDensityConstraints
arrowDensityConstraints)
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Int -> String -> (Int, Maybe Int) -> Maybe String
forall {a}.
(Ord a, Show a) =>
String -> a -> String -> (a, Maybe a) -> Maybe String
checkRangeVersusCount String
"numTransitions" Int
numTransitions String
"outgoingArrowsPerPlace"
          (ArrowDensityConstraints -> (Int, Maybe Int)
outgoingArrowsPerPlace ArrowDensityConstraints
arrowDensityConstraints)
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Int -> String -> (Int, Maybe Int) -> Maybe String
forall {a}.
(Ord a, Show a) =>
String -> a -> String -> (a, Maybe a) -> Maybe String
checkRangeVersusCount String
"numPlaces * numTransitions" (Int
numPlaces Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numTransitions)
          String
"totalArrowsFromPlacesToTransitions"
          (ArrowDensityConstraints -> (Int, Maybe Int)
totalArrowsFromPlacesToTransitions ArrowDensityConstraints
arrowDensityConstraints)
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Int -> String -> (Int, Maybe Int) -> Maybe String
forall {a}.
(Ord a, Show a) =>
String -> a -> String -> (a, Maybe a) -> Maybe String
checkRangeVersusCount String
"numPlaces * numTransitions" (Int
numPlaces Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numTransitions)
          String
"totalArrowsFromTransitionsToPlaces"
          (ArrowDensityConstraints -> (Int, Maybe Int)
totalArrowsFromTransitionsToPlaces ArrowDensityConstraints
arrowDensityConstraints)
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe Int -> Int -> Bool -> Maybe String
checkRejectLongerThanConsistency Maybe Int
rejectLongerThan Int
maxTransitionLength Bool
showLengthHint
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [GraphvizCommand] -> Maybe String
forall {a}. [a] -> Maybe String
checkDrawCommands [GraphvizCommand]
drawCommands
    Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> Int -> ArrowDensityConstraints -> Maybe String
checkArrowDensityCrossValidation Int
numPlaces Int
numTransitions ArrowDensityConstraints
arrowDensityConstraints
  where
    checkDrawCommands :: [a] -> Maybe String
checkDrawCommands [] = String -> Maybe String
forall a. a -> Maybe a
Just String
"drawCommands cannot be empty"
    checkDrawCommands [a]
_  = Maybe String
forall a. Maybe a
Nothing
    checkRangeVersusCount :: String -> a -> String -> (a, Maybe a) -> Maybe String
checkRangeVersusCount String
countName a
count String
what (a
low, Maybe a
h) = case Maybe a
h of
      Maybe a
Nothing ->
        if a
low a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
count
        then String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"The lower limit for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
what String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (currently " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
low String -> String -> String
forall a. [a] -> [a] -> [a]
++
                   String
") cannot exceed " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
countName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (currently " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
count String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        else Maybe String
forall a. Maybe a
Nothing
      Just a
high ->
        if a
high a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
count
        then String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"The upper limit for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
what String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (currently " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
high String -> String -> String
forall a. [a] -> [a] -> [a]
++
                   String
") cannot exceed " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
countName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (currently " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
count String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        else Maybe String
forall a. Maybe a
Nothing

-- | Check filter configuration constraints given the transition length parameters
checkFilterConfigWith
  :: Maybe Int        -- ^ rejectLongerThan
  -> Int              -- ^ minTransitionLength
  -> Int              -- ^ numTransitions (total number of transitions)
  -> FilterConfig     -- ^ filterConfig
  -> Maybe String
checkFilterConfigWith :: Maybe Int -> Int -> Int -> FilterConfig -> Maybe String
checkFilterConfigWith Maybe Int
rejectLongerThan theTransitionLength :: Int
theTransitionLength@Int
minTransitionLength Int
numTransitions filterConfig :: FilterConfig
filterConfig@FilterConfig{Bool
Int
[Int]
Maybe Int
Ratio Int
rejectGroupedRepeats :: Bool
repetitiveSubsequenceThreshold :: Maybe Int
spaceballsPrefixThreshold :: Maybe Int
forbiddenCycleLengths :: [Int]
requireCycleLengthsAny :: [Int]
solutionSetLimit :: Maybe Int
requireSolutionsArePermutations :: Bool
absentTransitionsRequirement :: Int
transitionCoverageRequirement :: Ratio Int
transitionCoverageRequirement :: FilterConfig -> Ratio Int
absentTransitionsRequirement :: FilterConfig -> Int
requireSolutionsArePermutations :: FilterConfig -> Bool
solutionSetLimit :: FilterConfig -> Maybe Int
requireCycleLengthsAny :: FilterConfig -> [Int]
forbiddenCycleLengths :: FilterConfig -> [Int]
spaceballsPrefixThreshold :: FilterConfig -> Maybe Int
repetitiveSubsequenceThreshold :: FilterConfig -> Maybe Int
rejectGroupedRepeats :: FilterConfig -> Bool
..}
  | Maybe Int
rejectLongerThan Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int -> Maybe Int
forall a. a -> Maybe a
Just Int
minTransitionLength
  , FilterConfig
filterConfig FilterConfig -> FilterConfig -> Bool
forall a. Eq a => a -> a -> Bool
/= FilterConfig
noFiltering
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"If transition length is not enforced to one value, filterConfig must be set to "
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ FilterConfig -> String
forall a. Show a => a -> String
show FilterConfig
noFiltering
  | Just Int
repeats <- Maybe Int
repetitiveSubsequenceThreshold
  , Int
repeats Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"repetitiveSubsequenceThreshold has to be set to at least 2 if it is enabled"
  | Just Int
repeats <- Maybe Int
repetitiveSubsequenceThreshold
  , Int
repeats Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
halfTransitionLength
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"repetitiveSubsequenceThreshold must not be higher than half of maxTransitionLength"
  | Bool -> Bool
not ([Int] -> Bool
forall a. Ord a => [a] -> Bool
isSorted [Int]
forbiddenCycleLengths) Bool -> Bool -> Bool
|| Bool -> Bool
not ([Int] -> Bool
forall a. Ord a => [a] -> Bool
isSorted [Int]
requireCycleLengthsAny)
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"forbiddenCycleLengths and requireCycleLengthsAny must each be sorted in ascending order"
  | [Int] -> Bool
forall a. [a] -> Bool
notNull [Int]
forbiddenCycleLengths Bool -> Bool -> Bool
&& [Int] -> Int
forall a. HasCallStack => [a] -> a
head [Int]
forbiddenCycleLengths Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"forbiddenCycleLengths must contain only values greater than 1"
  | [Int] -> Bool
forall a. [a] -> Bool
notNull [Int]
requireCycleLengthsAny Bool -> Bool -> Bool
&& [Int] -> Int
forall a. HasCallStack => [a] -> a
head [Int]
requireCycleLengthsAny Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"requireCycleLengthsAny must contain only positive values"
  | [Int] -> Bool
forall a. [a] -> Bool
notNull [Int]
forbiddenCycleLengths Bool -> Bool -> Bool
&& [Int] -> Int
forall a. HasCallStack => [a] -> a
last [Int]
forbiddenCycleLengths Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
halfTransitionLength
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"forbiddenCycleLengths must not contain values higher than half of maxTransitionLength"
  | [Int] -> Bool
forall a. [a] -> Bool
notNull [Int]
requireCycleLengthsAny Bool -> Bool -> Bool
&& [Int] -> Int
forall a. HasCallStack => [a] -> a
last [Int]
requireCycleLengthsAny Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
halfTransitionLength
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"requireCycleLengthsAny must not contain values higher than half of maxTransitionLength"
  | (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Int
0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/=) (Int -> Bool) -> (Int -> Int) -> Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Int
forall a. Integral a => a -> a -> a
mod Int
theTransitionLength) ([Int]
forbiddenCycleLengths [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
requireCycleLengthsAny)
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"forbiddenCycleLengths and requireCycleLengthsAny must each contain only divisors of the target sequence length"
  | (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
minRequiredTransitions) ([Int]
forbiddenCycleLengths [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
requireCycleLengthsAny)
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"forbiddenCycleLengths or requireCycleLengthsAny contains values that are already impossible due to transitionCoverageRequirement"
  | [Int] -> Bool
hasRedundantMultiples [Int]
forbiddenCycleLengths
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"forbiddenCycleLengths contains redundant multiples (no need to forbid n if k*n for some k>1 is already forbidden)"
  | [Int] -> Bool
hasRedundantMultiples [Int]
requireCycleLengthsAny
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"requireCycleLengthsAny contains redundant multiples (no need to ask e.g. for 'n or 2*n', since asking for '2*n' would suffice)"
  | [Int] -> [Int] -> Bool
hasConflictBetweenForbiddenAndRequired [Int]
forbiddenCycleLengths [Int]
requireCycleLengthsAny
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"requireCycleLengthsAny and forbiddenCycleLengths must not have overlapping or conflicting values"
  | Int
1 Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
requireCycleLengthsAny Bool -> Bool -> Bool
&& Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust Maybe Int
repetitiveSubsequenceThreshold
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"if requireCycleLengthsAny contains 1, repetitiveSubsequenceThreshold should be Nothing \
         \(forbidding repetitive subsequences does not make sense when requiring cycle length 1)"
  | Just Int
spaceballsLength <- Maybe Int
spaceballsPrefixThreshold
  , Int
spaceballsLength Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2 Bool -> Bool -> Bool
|| Int
spaceballsLength Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
theTransitionLength
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"spaceballsPrefixThreshold must be a value from 2 to maxTransitionLength if it is enabled"
  | Just Int
maxSolutions <- Maybe Int
solutionSetLimit
  , Int
maxSolutions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"setting solutionSetLimit to less than 1 does not make sense"
  | Maybe Int
solutionSetLimit Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
  , Bool -> Bool
not Bool
requireSolutionsArePermutations
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"when solutionSetLimit is 1, requireSolutionsArePermutations might as well be set to True"
  | Ratio Int
transitionCoverageRequirement Ratio Int -> Ratio Int -> Bool
forall a. Ord a => a -> a -> Bool
< Ratio Int
0 Bool -> Bool -> Bool
|| Ratio Int
transitionCoverageRequirement Ratio Int -> Ratio Int -> Bool
forall a. Ord a => a -> a -> Bool
> Ratio Int
1
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"transitionCoverageRequirement must be a value from 0 to 1"
  | Int
absentTransitionsRequirement Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
absentTransitionsRequirement Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
numTransitions
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"absentTransitionsRequirement must be non-negative and smaller than the total number of transitions"
  | Int
absentTransitionsRequirement Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxAbsent
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"absentTransitionsRequirement conflicts with transitionCoverageRequirement: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
           String
"at most " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
maxAbsent String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" transitions can be absent given the coverage requirement"
  | Bool
otherwise
  = Maybe String
forall a. Maybe a
Nothing
  where
    halfTransitionLength :: Int
halfTransitionLength = Int
theTransitionLength Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
    minRequiredTransitions :: Int
minRequiredTransitions = Ratio Int -> Int
forall b. Integral b => Ratio Int -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Ratio Int
transitionCoverageRequirement Ratio Int -> Ratio Int -> Ratio Int
forall a. Num a => a -> a -> a
* Int -> Ratio Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
numTransitions)
    maxAbsent :: Int
maxAbsent = Int
numTransitions Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
minRequiredTransitions

    isSorted :: Ord a => [a] -> Bool
    isSorted :: forall a. Ord a => [a] -> Bool
isSorted [] = Bool
True
    isSorted [a
_] = Bool
True
    isSorted (a
x:rest :: [a]
rest@(a
y:[a]
_)) = a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
y Bool -> Bool -> Bool
&& [a] -> Bool
forall a. Ord a => [a] -> Bool
isSorted [a]
rest

    hasRedundantMultiples :: [Int] -> Bool
    hasRedundantMultiples :: [Int] -> Bool
hasRedundantMultiples = [Int] -> [Int] -> Bool
go []
      where
        go :: [Int] -> [Int] -> Bool
        go :: [Int] -> [Int] -> Bool
go [Int]
_ [] = Bool
False
        go [Int]
smallerElements (Int
currentElement : [Int]
remainingElements)
          | (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Int
0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool) -> (Int -> Int) -> Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Int
forall a. Integral a => a -> a -> a
mod Int
currentElement) [Int]
smallerElements = Bool
True
          | Bool
otherwise = [Int] -> [Int] -> Bool
go (Int
currentElement Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
smallerElements) [Int]
remainingElements

    hasConflictBetweenForbiddenAndRequired :: [Int] -> [Int] -> Bool
    hasConflictBetweenForbiddenAndRequired :: [Int] -> [Int] -> Bool
hasConflictBetweenForbiddenAndRequired [Int]
forbidden =
      (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Int
r -> (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Int
f -> Int
f Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) [Int]
forbidden)

-- | Check transition behavior constraints for validity
checkTransitionBehaviorConstraints
  :: Int                               -- ^ numPlaces
  -> Int                               -- ^ numTransitions
  -> ArrowDensityConstraints           -- ^ arrow density constraints
  -> TransitionBehaviorConstraints     -- ^ transition behavior constraints
  -> Maybe String
checkTransitionBehaviorConstraints :: Int
-> Int
-> ArrowDensityConstraints
-> TransitionBehaviorConstraints
-> Maybe String
checkTransitionBehaviorConstraints
  Int
numPlaces
  Int
numTransitions
  ArrowDensityConstraints {(Int, Maybe Int)
incomingArrowsPerTransition :: ArrowDensityConstraints -> (Int, Maybe Int)
outgoingArrowsPerTransition :: ArrowDensityConstraints -> (Int, Maybe Int)
incomingArrowsPerPlace :: ArrowDensityConstraints -> (Int, Maybe Int)
outgoingArrowsPerPlace :: ArrowDensityConstraints -> (Int, Maybe Int)
totalArrowsFromPlacesToTransitions :: ArrowDensityConstraints -> (Int, Maybe Int)
totalArrowsFromTransitionsToPlaces :: ArrowDensityConstraints -> (Int, Maybe Int)
incomingArrowsPerTransition :: (Int, Maybe Int)
outgoingArrowsPerTransition :: (Int, Maybe Int)
incomingArrowsPerPlace :: (Int, Maybe Int)
outgoingArrowsPerPlace :: (Int, Maybe Int)
totalArrowsFromPlacesToTransitions :: (Int, Maybe Int)
totalArrowsFromTransitionsToPlaces :: (Int, Maybe Int)
..}
  TransitionBehaviorConstraints {Maybe Int
Maybe Ordering
allowedTokenChanges :: Maybe Ordering
areNonPreserving :: Maybe Int
areNonPreserving :: TransitionBehaviorConstraints -> Maybe Int
allowedTokenChanges :: TransitionBehaviorConstraints -> Maybe Ordering
..}
  | Just Ordering
EQ <- Maybe Ordering
allowedTokenChanges
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"allowedTokenChanges = Just EQ is meaningless; use areNonPreserving = Just 0 instead"
  | Just Int
numberOfNonPreserving <- Maybe Int
areNonPreserving
  , Int
numberOfNonPreserving Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
numberOfNonPreserving Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
numTransitions
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"areNonPreserving must be non-negative and at most numTransitions when specified"
  | Maybe Int
areNonPreserving Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0
  , Maybe Ordering -> Bool
forall a. Maybe a -> Bool
isJust Maybe Ordering
allowedTokenChanges
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"when areNonPreserving = Just 0 (all transitions token-preserving), allowedTokenChanges = Just ... makes no sense"
  | Maybe Int
areNonPreserving Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0
  , Int
tvLow Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
tnLow
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords
      [ String
"when areNonPreserving = Just 0 (all transitions token-preserving),"
      , String
"totalArrowsFromPlacesToTransitions lower bound (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
tvLow String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      , String
"must equal totalArrowsFromTransitionsToPlaces lower bound (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
tnLow String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      ]
  | Maybe Int
areNonPreserving Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0
  , Just Int
tvHighValue <- Maybe Int
tvHighMaybe
  , Just Int
tnHighValue <- Maybe Int
tnHighMaybe
  , Int
tvHighValue Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
tnHighValue
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords
      [ String
"when areNonPreserving = Just 0 (all transitions token-preserving),"
      , String
"totalArrowsFromPlacesToTransitions upper bound (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
tvHighValue String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      , String
"must equal totalArrowsFromTransitionsToPlaces upper bound (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
tnHighValue String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"), when both are set"
      ]
  | Maybe Int
areNonPreserving Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0
  , Int
vLow Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
nLow
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords
      [ String
"when areNonPreserving = Just 0 (all transitions token-preserving),"
      , String
"incomingArrowsPerTransition lower bound (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
vLow String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      , String
"must equal outgoingArrowsPerTransition lower bound (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
nLow String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      ]
  | Maybe Int
areNonPreserving Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0
  , Just Int
vHighValue <- Maybe Int
vHighMaybe
  , Just Int
nHighValue <- Maybe Int
nHighMaybe
  , Int
vHighValue Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
nHighValue
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords
      [ String
"when areNonPreserving = Just 0 (all transitions token-preserving),"
      , String
"incomingArrowsPerTransition upper bound (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
vHighValue String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      , String
"must equal outgoingArrowsPerTransition upper bound (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
nHighValue String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"), when both are set"
      ]
  | Maybe Ordering
allowedTokenChanges Maybe Ordering -> Maybe Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
LT
  , Int
vLow Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
nLow Bool -> Bool -> Bool
|| Int
vHigh Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
nHigh
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"with allowedTokenChanges = Just LT, the combination of incomingArrowsPerTransition and outgoingArrowsPerTransition is too lax"
  | Maybe Ordering
allowedTokenChanges Maybe Ordering -> Maybe Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
GT
  , Int
vLow Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
nLow Bool -> Bool -> Bool
|| Int
vHigh Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
nHigh
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"with allowedTokenChanges = Just GT, the combination of incomingArrowsPerTransition and outgoingArrowsPerTransition is too lax"
  | Just Ordering
direction <- Maybe Ordering
allowedTokenChanges
  = let
      -- Use fromMaybe to handle both Just and Nothing cases
      -- For lower bound checks: at least 0 non-preserving transitions
      minNonPreserving :: Int
minNonPreserving = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 Maybe Int
areNonPreserving
      -- For upper bound checks: at most all transitions are non-preserving
      maxNonPreserving :: Int
maxNonPreserving = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
numTransitions Maybe Int
areNonPreserving

      -- Calculate differences and limits based on direction
      (Int
lowerDiff, Int
maxPerTransition) = case Ordering
direction of
        Ordering
GT -> (Int
tnLow Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
tvLow, Int
nHigh Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
vLow)
        Ordering
LT -> (Int
tvLow Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
tnLow, Int
vHigh Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nLow)

      maxTotal :: Int
maxTotal = Int
maxNonPreserving Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
maxPerTransition

      -- Check lower bound insufficient arrow difference
      checkLowerInsufficientDiff :: Maybe String
checkLowerInsufficientDiff
        | Int
lowerDiff Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
minNonPreserving
        = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Ordering -> Maybe Int -> Int -> String -> String
forall {a} {p} {a}.
(Show a, Show p, Show a) =>
a -> Maybe a -> p -> String -> String
insufficientArrowDifference Ordering
direction Maybe Int
areNonPreserving Int
lowerDiff String
"lower"
        | Bool
otherwise
        = Maybe String
forall a. Maybe a
Nothing

      -- Check lower bound excessive arrow difference
      checkLowerExcessiveDiff :: Maybe String
checkLowerExcessiveDiff
        | Int
lowerDiff Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxTotal
        = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Ordering -> Maybe Int -> Int -> Int -> String -> String
forall {a}.
Show a =>
Ordering -> Maybe Int -> Int -> a -> String -> String
excessiveArrowDifference Ordering
direction Maybe Int
areNonPreserving Int
maxPerTransition Int
lowerDiff String
"lower"
        | Bool
otherwise
        = Maybe String
forall a. Maybe a
Nothing

      -- Check upper bound insufficient arrow difference
      checkUpperInsufficientDiff :: Maybe String
checkUpperInsufficientDiff = case Ordering
direction of
        Ordering
GT | Just Int
tvHighValue <- Maybe Int
tvHighMaybe
           , let upperDiff :: Int
upperDiff = Int
tnHigh Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
tvHighValue
           , Int
upperDiff Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
minNonPreserving
           -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Ordering -> Maybe Int -> Int -> String -> String
forall {a} {p} {a}.
(Show a, Show p, Show a) =>
a -> Maybe a -> p -> String -> String
insufficientArrowDifference Ordering
direction Maybe Int
areNonPreserving Int
upperDiff String
"upper"
        Ordering
LT | Just Int
tnHighValue <- Maybe Int
tnHighMaybe
           , let upperDiff :: Int
upperDiff = Int
tvHigh Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
tnHighValue
           , Int
upperDiff Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
minNonPreserving
           -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Ordering -> Maybe Int -> Int -> String -> String
forall {a} {p} {a}.
(Show a, Show p, Show a) =>
a -> Maybe a -> p -> String -> String
insufficientArrowDifference Ordering
direction Maybe Int
areNonPreserving Int
upperDiff String
"upper"
        Ordering
_ -> Maybe String
forall a. Maybe a
Nothing

      -- Check upper bound excessive arrow difference
      checkUpperExcessiveDiff :: Maybe String
checkUpperExcessiveDiff = case Ordering
direction of
        Ordering
GT | Just Int
tnHighValue <- Maybe Int
tnHighMaybe
           , let upperDiff :: Int
upperDiff = Int
tnHighValue Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
tvHigh
           , Int
upperDiff Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxTotal
           -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Ordering -> Maybe Int -> Int -> Int -> String -> String
forall {a}.
Show a =>
Ordering -> Maybe Int -> Int -> a -> String -> String
excessiveArrowDifference Ordering
direction Maybe Int
areNonPreserving Int
maxPerTransition Int
upperDiff String
"upper"
        Ordering
LT | Just Int
tvHighValue <- Maybe Int
tvHighMaybe
           , let upperDiff :: Int
upperDiff = Int
tvHighValue Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
tnHigh
           , Int
upperDiff Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxTotal
           -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Ordering -> Maybe Int -> Int -> Int -> String -> String
forall {a}.
Show a =>
Ordering -> Maybe Int -> Int -> a -> String -> String
excessiveArrowDifference Ordering
direction Maybe Int
areNonPreserving Int
maxPerTransition Int
upperDiff String
"upper"
        Ordering
_ -> Maybe String
forall a. Maybe a
Nothing

    in Maybe String
checkLowerInsufficientDiff Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe String
checkLowerExcessiveDiff Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe String
checkUpperInsufficientDiff Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe String
checkUpperExcessiveDiff
  | Maybe Int
areNonPreserving Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0
  , Int
vLow Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
vHigh Bool -> Bool -> Bool
&& Int
nLow Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
nHigh Bool -> Bool -> Bool
&& Int
vLow Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
nLow
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"only areNonPreserving = Just 0 makes sense when incomingArrowsPerTransition and outgoingArrowsPerTransition are all fixed to one value anyway"
  | Bool
otherwise
  = Maybe String
forall a. Maybe a
Nothing
  where
    (Int
vLow, Maybe Int
vHighMaybe) = (Int, Maybe Int)
incomingArrowsPerTransition
    (Int
nLow, Maybe Int
nHighMaybe) = (Int, Maybe Int)
outgoingArrowsPerTransition
    -- Since checkBasicPetriConfig guarantees upper bounds don't exceed numPlaces, we can use numPlaces as the default
    vHigh :: Int
vHigh = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
numPlaces Maybe Int
vHighMaybe
    nHigh :: Int
nHigh = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
numPlaces Maybe Int
nHighMaybe
    (Int
tvLow, Maybe Int
tvHighMaybe) = (Int, Maybe Int)
totalArrowsFromPlacesToTransitions
    (Int
tnLow, Maybe Int
tnHighMaybe) = (Int, Maybe Int)
totalArrowsFromTransitionsToPlaces
    -- For total arrows, use the product of numPlaces * numTransitions as the default upper bound.
    -- This represents the maximum possible number of arrow connections (not counting weights):
    -- each place can have at most one arrow connection to each transition.
    tvHigh :: Int
tvHigh = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (Int
numPlaces Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numTransitions) Maybe Int
tvHighMaybe
    tnHigh :: Int
tnHigh = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (Int
numPlaces Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numTransitions) Maybe Int
tnHighMaybe

    -- Helper function for insufficient arrow difference errors
    insufficientArrowDifference :: a -> Maybe a -> p -> String -> String
insufficientArrowDifference a
direction Maybe a
maybeAreNonPreserving p
actualDifference String
boundType =
      let
        areNonPreservingText :: String
areNonPreservingText = case Maybe a
maybeAreNonPreserving of
          Just a
n -> String
" and areNonPreserving = Just " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n
          Maybe a
Nothing -> String
""
        differenceText :: String
differenceText = if Maybe a -> Bool
forall a. Maybe a -> Bool
isNothing Maybe a
maybeAreNonPreserving
          then String
"cannot be negative"
          else String
"cannot be just " String -> String -> String
forall a. [a] -> [a] -> [a]
++ p -> String
forall a. Show a => a -> String
show p
actualDifference
      in [String] -> String
unwords
        [ String
"with allowedTokenChanges = Just"
        , a -> String
forall a. Show a => a -> String
show a
direction String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
areNonPreservingText String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
","
        , String
boundType
        , String
"bound difference between totalArrowsFromPlacesToTransitions and totalArrowsFromTransitionsToPlaces"
        , String
differenceText
        ]

    -- Helper function for excessive arrow difference errors
    excessiveArrowDifference :: Ordering -> Maybe Int -> Int -> a -> String -> String
excessiveArrowDifference Ordering
direction Maybe Int
maybeAreNonPreserving Int
maxPerTransition a
actualDifference String
boundType =
      let
        maxTotal :: Int
maxTotal = Int
maxPerTransition Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
numTransitions Maybe Int
maybeAreNonPreserving
        areNonPreservingText :: String
areNonPreservingText = case Maybe Int
maybeAreNonPreserving of
          Just Int
n -> String
"areNonPreserving = Just " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
          Maybe Int
Nothing -> String
"numTransitions = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
numTransitions
      in [String] -> String
unwords
        [ String
"with"
        , String
areNonPreservingText
        , String
"and at most"
        , Int -> String
forall a. Show a => a -> String
show Int
maxPerTransition
        , String
"token"
        , if Ordering
direction Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
GT then String
"increase" else String
"decrease"
        , String
"per transition,"
        , String
"overall at most"
        , Int -> String
forall a. Show a => a -> String
show Int
maxTotal
        , String
"token"
        , if Ordering
direction Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
GT then String
"increase" else String
"decrease"
        , String
"is possible,"
        , String
"but"
        , String
boundType
        , String
"bound difference between totalArrowsFromPlacesToTransitions and totalArrowsFromTransitionsToPlaces is"
        , a -> String
forall a. Show a => a -> String
show a
actualDifference
        ]

-- | Check cross-validation of arrow density parameters
checkArrowDensityCrossValidation
  :: Int              -- ^ numPlaces
  -> Int              -- ^ numTransitions
  -> ArrowDensityConstraints
  -> Maybe String
checkArrowDensityCrossValidation :: Int -> Int -> ArrowDensityConstraints -> Maybe String
checkArrowDensityCrossValidation
  Int
numPlaces
  Int
numTransitions
  ArrowDensityConstraints {
    incomingArrowsPerTransition :: ArrowDensityConstraints -> (Int, Maybe Int)
incomingArrowsPerTransition = (Int
incomingPerTransLow, Maybe Int
incomingPerTransHigh),
    outgoingArrowsPerTransition :: ArrowDensityConstraints -> (Int, Maybe Int)
outgoingArrowsPerTransition = (Int
outgoingPerTransLow, Maybe Int
outgoingPerTransHigh),
    incomingArrowsPerPlace :: ArrowDensityConstraints -> (Int, Maybe Int)
incomingArrowsPerPlace = (Int
incomingPerPlaceLow, Maybe Int
incomingPerPlaceHigh),
    outgoingArrowsPerPlace :: ArrowDensityConstraints -> (Int, Maybe Int)
outgoingArrowsPerPlace = (Int
outgoingPerPlaceLow, Maybe Int
outgoingPerPlaceHigh),
    totalArrowsFromPlacesToTransitions :: ArrowDensityConstraints -> (Int, Maybe Int)
totalArrowsFromPlacesToTransitions = (Int
totalPlacesToTransLow, Maybe Int
totalPlacesToTransHigh),
    totalArrowsFromTransitionsToPlaces :: ArrowDensityConstraints -> (Int, Maybe Int)
totalArrowsFromTransitionsToPlaces = (Int
totalTransToPlacesLow, Maybe Int
totalTransToPlacesHigh)
  }
  | let minPlacesToTrans :: Int
minPlacesToTrans = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Int
incomingPerTransLow Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numTransitions) (Int
outgoingPerPlaceLow Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numPlaces)
  , Int
totalPlacesToTransLow Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
minPlacesToTrans
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"given the other settings, totalArrowsFromPlacesToTransitions lower bound (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
totalPlacesToTransLow String -> String -> String
forall a. [a] -> [a] -> [a]
++
           String
") should be at least " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
minPlacesToTrans
  | let maxPlacesToTrans :: Int
maxPlacesToTrans = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Int
incomingPerTransHighBound Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numTransitions) (Int
outgoingPerPlaceHighBound Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numPlaces)
  , let bound :: Int
bound = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
totalPlacesToTransLow Maybe Int
totalPlacesToTransHigh
  , Int
bound Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxPlacesToTrans
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"given the other settings, totalArrowsFromPlacesToTransitions (upper) bound (" String -> String -> String
forall a. [a] -> [a] -> [a]
++
           Int -> String
forall a. Show a => a -> String
show Int
bound String -> String -> String
forall a. [a] -> [a] -> [a]
++
           String
") should be at most " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
maxPlacesToTrans
  | let minTransToPlaces :: Int
minTransToPlaces = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Int
outgoingPerTransLow Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numTransitions) (Int
incomingPerPlaceLow Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numPlaces)
  , Int
totalTransToPlacesLow Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
minTransToPlaces
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"given the other settings, totalArrowsFromTransitionsToPlaces lower bound (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
totalTransToPlacesLow String -> String -> String
forall a. [a] -> [a] -> [a]
++
           String
") should be at least " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
minTransToPlaces
  | let maxTransToPlaces :: Int
maxTransToPlaces = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Int
outgoingPerTransHighBound Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numTransitions) (Int
incomingPerPlaceHighBound Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numPlaces)
  , let bound :: Int
bound = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
totalTransToPlacesLow Maybe Int
totalTransToPlacesHigh
  , Int
bound Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxTransToPlaces
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"given the other settings, totalArrowsFromTransitionsToPlaces (upper) bound (" String -> String -> String
forall a. [a] -> [a] -> [a]
++
           Int -> String
forall a. Show a => a -> String
show Int
bound String -> String -> String
forall a. [a] -> [a] -> [a]
++
           String
") should be at most " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
maxTransToPlaces
  | Int
incomingPerTransLow Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numTransitions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
outgoingPerPlaceHighBound Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numPlaces
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"incomingArrowsPerTransition lower bound times numTransitions " String -> String -> String
forall a. [a] -> [a] -> [a]
++
           String
"exceeds maximum possible arrows based on outgoingArrowsPerPlace (or numTransitions) times numPlaces"
  | Int
outgoingPerTransLow Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numTransitions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
incomingPerPlaceHighBound Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numPlaces
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"outgoingArrowsPerTransition lower bound times numTransitions " String -> String -> String
forall a. [a] -> [a] -> [a]
++
           String
"exceeds maximum possible arrows based on incomingArrowsPerPlace (or numTransitions) times numPlaces"
  | Bool
otherwise = Maybe String
forall a. Maybe a
Nothing
  where
    incomingPerTransHighBound :: Int
incomingPerTransHighBound = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
numPlaces Maybe Int
incomingPerTransHigh
    outgoingPerTransHighBound :: Int
outgoingPerTransHighBound = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
numPlaces Maybe Int
outgoingPerTransHigh
    incomingPerPlaceHighBound :: Int
incomingPerPlaceHighBound = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
numTransitions Maybe Int
incomingPerPlaceHigh
    outgoingPerPlaceHighBound :: Int
outgoingPerPlaceHighBound = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
numTransitions Maybe Int
outgoingPerPlaceHigh