{-# LANGUAGE QuasiQuotes #-}
-- | Common validation logic for ActivityDiagram Petri-based tasks
module Modelling.ActivityDiagram.Auxiliary.PetriValidation (
  validatePetriConfig,
  validateBasePetriConfig
) where

import qualified Modelling.ActivityDiagram.Config as Config (
  AdConfig (activityFinalNodes, flowFinalNodes, actionLimits, forkJoinPairs, cycles),
  )

import Control.Applicative (Alternative ((<|>)))
import Data.GraphViz.Commands (GraphvizCommand(..))
import Data.Maybe (isJust, fromJust)
import Data.String.Interpolate (iii)

-- | Base validation logic common to multiple Petri-based configurations
validateBasePetriConfig
  :: Config.AdConfig
  -> (Int, Maybe Int)  -- countOfPetriNodesBounds
  -> Maybe Integer  -- maxInstances
  -> Maybe Bool  -- presenceOfSinkTransitionsForFinals
  -> Maybe String
validateBasePetriConfig :: AdConfig
-> (Int, Maybe Int) -> Maybe Integer -> Maybe Bool -> Maybe String
validateBasePetriConfig AdConfig
adConfig (Int, Maybe Int)
countOfPetriNodesBounds Maybe Integer
maxInstances Maybe Bool
presenceOfSinkTransitionsForFinals
  | AdConfig -> Int
Config.activityFinalNodes AdConfig
adConfig Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"There is at most one 'activityFinalNode' allowed."
  | AdConfig -> Int
Config.activityFinalNodes AdConfig
adConfig Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1 Bool -> Bool -> Bool
&& AdConfig -> Int
Config.flowFinalNodes AdConfig
adConfig Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"There is no 'flowFinalNode' allowed if there is an 'activityFinalNode'."
  | (Int, Maybe Int) -> Int
forall a b. (a, b) -> a
fst (Int, Maybe Int)
countOfPetriNodesBounds Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"'countOfPetriNodesBounds' must not contain negative values"
  | Just Int
high <- (Int, Maybe Int) -> Maybe Int
forall a b. (a, b) -> b
snd (Int, Maybe Int)
countOfPetriNodesBounds, (Int, Maybe Int) -> Int
forall a b. (a, b) -> a
fst (Int, Maybe Int)
countOfPetriNodesBounds Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
high
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"the second value of 'countOfPetriNodesBounds' must not be smaller than its first value"
  | Maybe Integer -> Bool
forall a. Maybe a -> Bool
isJust Maybe Integer
maxInstances Bool -> Bool -> Bool
&& Maybe Integer -> Integer
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Integer
maxInstances Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
1
    = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'maxInstances' must either be set to a positive value or to Nothing"
  | Just Bool
False <- Maybe Bool
presenceOfSinkTransitionsForFinals,
    (Int, Int) -> Int
forall a b. (a, b) -> a
fst (AdConfig -> (Int, Int)
Config.actionLimits AdConfig
adConfig) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ AdConfig -> Int
Config.forkJoinPairs AdConfig
adConfig Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1
    = String -> Maybe String
forall a. a -> Maybe a
Just String
"The option 'presenceOfSinkTransitionsForFinals = Just False' can only be achieved if the number of Actions, Fork Nodes and Join Nodes together is positive"
  | Bool
otherwise
    = Maybe String
forall a. Maybe a
Nothing

-- | Common validation logic for configurations that share Petri-related parameters
validatePetriConfig
  :: Config.AdConfig
  -> (Int, Maybe Int)  -- countOfPetriNodesBounds
  -> Maybe Integer  -- maxInstances
  -> [GraphvizCommand]  -- petriLayout
  -> Maybe Bool  -- auxiliaryPetriNodeAbsent
  -> Maybe Bool  -- presenceOfSinkTransitionsForFinals
  -> Maybe Bool  -- withActivityFinalInForkBlocks
  -> Maybe String
validatePetriConfig :: AdConfig
-> (Int, Maybe Int)
-> Maybe Integer
-> [GraphvizCommand]
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe String
validatePetriConfig
  AdConfig
adConfig
  (Int, Maybe Int)
countOfPetriNodesBounds
  Maybe Integer
maxInstances
  [GraphvizCommand]
petriLayout
  Maybe Bool
auxiliaryPetriNodeAbsent
  Maybe Bool
presenceOfSinkTransitionsForFinals
  Maybe Bool
withActivityFinalInForkBlocks =
  AdConfig
-> (Int, Maybe Int) -> Maybe Integer -> Maybe Bool -> Maybe String
validateBasePetriConfig AdConfig
adConfig (Int, Maybe Int)
countOfPetriNodesBounds Maybe Integer
maxInstances Maybe Bool
presenceOfSinkTransitionsForFinals
  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
validatePetriConfigSpecific
  where
    validatePetriConfigSpecific :: Maybe String
validatePetriConfigSpecific
      | Maybe Bool
auxiliaryPetriNodeAbsent Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Bool -> Bool -> Bool
&& AdConfig -> Int
Config.cycles AdConfig
adConfig Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
      = String -> Maybe String
forall a. a -> Maybe a
Just [iii|
        Setting the parameter 'auxiliaryPetriNodeAbsent' to True
        prohibits having more than 0 cycles
        |]
      | Maybe Bool
withActivityFinalInForkBlocks Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False Bool -> Bool -> Bool
&& AdConfig -> Int
Config.activityFinalNodes AdConfig
adConfig Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
        = String -> Maybe String
forall a. a -> Maybe a
Just String
"Setting the parameter 'withActivityFinalInForkBlocks' to False prohibits having more than 1 'activityFinalNodes'"
      | Maybe Bool
withActivityFinalInForkBlocks Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Bool -> Bool -> Bool
&& AdConfig -> Int
Config.activityFinalNodes AdConfig
adConfig Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
        = String -> Maybe String
forall a. a -> Maybe a
Just String
"Setting the parameter 'withActivityFinalInForkBlocks' to True implies that there are 'activityFinalNodes'"
      | [GraphvizCommand] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GraphvizCommand]
petriLayout
        = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'petriLayout' can not be the empty list"
      | (GraphvizCommand -> Bool) -> [GraphvizCommand] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (GraphvizCommand -> [GraphvizCommand] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [GraphvizCommand
Dot, GraphvizCommand
Neato, GraphvizCommand
TwoPi, GraphvizCommand
Circo, GraphvizCommand
Fdp]) [GraphvizCommand]
petriLayout
        = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'petriLayout' can only contain the options Dot, Neato, TwoPi, Circo and Fdp"
      | Bool
otherwise
        = Maybe String
forall a. Maybe a
Nothing