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

import Control.Applicative (Alternative ((<|>)))
import Data.GraphViz.Commands (GraphvizCommand)
import Modelling.PetriNet.Reach.Type (Capacity(..))

-- | 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
  -> (Int, Maybe Int)         -- ^ preconditionsRange
  -> (Int, Maybe Int)         -- ^ postconditionsRange
  -> [GraphvizCommand]        -- ^ drawCommands
  -> Maybe Int                -- ^ rejectLongerThan
  -> Bool                     -- ^ showLengthHint
  -> Maybe String
checkBasicPetriConfig :: forall s.
Int
-> Int
-> Capacity s
-> Int
-> Int
-> (Int, Maybe Int)
-> (Int, Maybe Int)
-> [GraphvizCommand]
-> Maybe Int
-> Bool
-> Maybe String
checkBasicPetriConfig
  Int
numPlaces
  Int
numTransitions
  Capacity s
capacity
  Int
minTransitionLength
  Int
maxTransitionLength
  (Int, Maybe Int)
preconditionsRange
  (Int, Maybe Int)
postconditionsRange
  [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
<|> String -> (Int, Maybe Int) -> Maybe String
forall n.
(Num n, Ord n, Show n) =>
String -> (n, Maybe n) -> Maybe String
checkRange String
"preconditionsRange" (Int, Maybe Int)
preconditionsRange
    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
"postconditionsRange" (Int, Maybe Int)
postconditionsRange
    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
  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