{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE CPP #-}
#if !MIN_VERSION_base(4,18,0)
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DerivingStrategies #-}
#endif
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-|
originally from Autotool (https://gitlab.imn.htwk-leipzig.de/autotool/all0)
based on revision: ad25a990816a162fdd13941ff889653f22d6ea0a
based on file: collection/src/Petri/Deadlock.hs
-}
module Modelling.PetriNet.Reach.Deadlock (
  -- * Types
  DeadlockInstance(..),
  DeadlockConfig(..),
  checkDeadlockConfig,

  -- * Generation
  generateDeadlock,

  -- * Task creation
  deadlockTask,
  verifyDeadlock,

  -- * Evaluation
  deadlockEvaluation,
  deadlockSyntax,
  deadlockInitial,

  -- * Configuration
  defaultDeadlockConfig,
  defaultDeadlockInstance,

  -- * Utilities
  bimapDeadlockInstance,
  toShowDeadlockInstance,
  exampleInstance,
) where

import qualified Data.Bimap                       as BM (lookup)
import qualified Data.Map                         as M (fromList)
import qualified Data.Set                         as S (fromList, toList)

import Autolib.Reader                   (Reader)
import Autolib.ToDoc                    (ToDoc)
import Data.List.NonEmpty                 (NonEmpty((:|)))

import Capabilities.Cache               (MonadCache)
import Capabilities.Diagrams            (MonadDiagrams)
import Capabilities.Graphviz            (MonadGraphviz)
import Modelling.PetriNet.Reach.Draw    (drawToFile)
import Modelling.PetriNet.Reach.Filter (
  FilterConfig (..),
  defaultFilterConfig,
  )
import Modelling.PetriNet.Reach.Property (
  Property (Default),
  validate,
  )
import Modelling.PetriNet.Reach.ConfigValidation (
  checkBasicPetriConfig,
  checkFilterConfigWith,
  )
import Modelling.PetriNet.Reach.Reach   (
  assertReachPoints,
  isNoLonger,
  levelsWithAlternatives,
  rejectSpaceballsPattern,
  reportReachFor,
  transitionsValid,
  provideSolutionsFeedback,
  validateDrawabilityAndSolutionFiltering,
  )
import Modelling.PetriNet.Reach.Roll    (netLimitsFiltered, simpleConnectionGenerator, generateValidConnection, generateFusableConnections)
import Modelling.PetriNet.Reach.Step    (executes, successors)
import Modelling.PetriNet.Reach.Type (
  ArrowDensityConstraints(..),
  Capacity (Unbounded),
  Net (..),
  Place (..),
  ShowPlace (ShowPlace),
  ShowTransition (ShowTransition),
  State (State),
  Transition (..),
  TransitionBehaviorConstraints,
  TransitionsList (TransitionsList),
  bimapNet,
  countFusableTransitionsConsuming,
  countFusableTransitionsProducing,
  example,
  noArrowDensityConstraints,
  noTransitionBehaviorConstraints,
  )

import Control.Applicative              (Alternative, (<|>))
import Control.OutputCapable.Blocks (
  LangM,
  OutputCapable,
  Rated,
  english,
  german,
  translate,
  yesNo,
  )
import Data.Ratio                       ((%))

import Control.OutputCapable.Blocks.Generic (
  ($>>),
  ($>>=),
  )
import Data.Bifunctor                   (bimap)
import Data.Either.Combinators          (whenRight)
import Control.Functor.Trans            (FunctorTrans (lift))
import Control.Monad                    (guard)
import Control.Monad.Catch              (MonadCatch, MonadThrow)
import Control.Monad.Extra              (whenJust)
import Control.Monad.Random             (evalRandT, mkStdGen)
import Control.Monad.Trans.Maybe        (MaybeT (MaybeT), runMaybeT)
import Control.Monad.Trans.Random       (RandT)
import Data.Maybe                       (fromMaybe)
import System.Random.Internal           (StdGen)
import Data.GraphViz                    (GraphvizCommand (..))
#if !MIN_VERSION_base(4,18,0)
import Data.Typeable                    (Typeable)
#endif
import GHC.Generics                     (Generic)

verifyDeadlock
  :: (OutputCapable m, Show a, Show t, Ord t, Ord a)
  => DeadlockInstance a t
  -> LangM m
verifyDeadlock :: forall (m :: * -> *) a t.
(OutputCapable m, Show a, Show t, Ord t, Ord a) =>
DeadlockInstance a t -> LangM m
verifyDeadlock = Property -> Net a t -> LangM m
forall a t (m :: * -> *).
(Ord a, Ord t, OutputCapable m, Show a, Show t) =>
Property -> Net a t -> LangM m
validate Property
Default (Net a t -> LangM m)
-> (DeadlockInstance a t -> Net a t)
-> DeadlockInstance a t
-> LangM m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeadlockInstance a t -> Net a t
forall s t. DeadlockInstance s t -> Net s t
petriNet

deadlockTask
  :: (
    MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    Ord s,
    Ord t,
    OutputCapable m,
    Show s,
    Show t
    )
  => Bool
  -> FilePath
  -> DeadlockInstance s t
  -> LangM m
deadlockTask :: forall (m :: * -> *) s t.
(MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m,
 Ord s, Ord t, OutputCapable m, Show s, Show t) =>
Bool -> FilePath -> DeadlockInstance s t -> LangM m
deadlockTask Bool
showInputHelp FilePath
path DeadlockInstance s t
inst = do
  m FilePath -> GenericLangM Language m FilePath
forall (f :: * -> *) a.
Functor f =>
f a -> GenericLangM Language f a
forall (t :: (* -> *) -> * -> *) (f :: * -> *) a.
(FunctorTrans t, Functor f) =>
f a -> t f a
lift (Bool -> FilePath -> GraphvizCommand -> Net s t -> m FilePath
forall s t (m :: * -> *).
(Ord s, Ord t, Show s, Show t, MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m) =>
Bool -> FilePath -> GraphvizCommand -> Net s t -> m FilePath
drawToFile (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ DeadlockInstance s t -> Bool
forall s t. DeadlockInstance s t -> Bool
showPlaceNames DeadlockInstance s t
inst) FilePath
path (DeadlockInstance s t -> GraphvizCommand
forall s t. DeadlockInstance s t -> GraphvizCommand
drawUsing DeadlockInstance s t
inst) (DeadlockInstance s t -> Net s t
forall s t. DeadlockInstance s t -> Net s t
petriNet DeadlockInstance s t
inst))
  GenericLangM Language m FilePath
-> (FilePath -> GenericLangM Language m ())
-> GenericLangM Language m ()
forall (m :: * -> *) l a b.
Monad m =>
GenericLangM l m a
-> (a -> GenericLangM l m b) -> GenericLangM l m b
$>>= \FilePath
img ->
    Bool
-> FilePath
-> Maybe Int
-> Maybe Int
-> Int
-> Bool
-> Maybe (Either FilePath FilePath)
-> GenericLangM Language m ()
forall (m :: * -> *).
OutputCapable m =>
Bool
-> FilePath
-> Maybe Int
-> Maybe Int
-> Int
-> Bool
-> Maybe (Either FilePath FilePath)
-> LangM m
reportReachFor
    Bool
showInputHelp
    FilePath
img
    (DeadlockInstance s t -> Maybe Int
forall s t. DeadlockInstance s t -> Maybe Int
noLongerThan DeadlockInstance s t
inst)
    (DeadlockInstance s t -> Maybe Int
forall s t. DeadlockInstance s t -> Maybe Int
withLengthHint DeadlockInstance s t
inst)
    (DeadlockInstance s t -> Int
forall s t. DeadlockInstance s t -> Int
minLength DeadlockInstance s t
inst)
    (DeadlockInstance s t -> Bool
forall s t. DeadlockInstance s t -> Bool
withMinLengthHint DeadlockInstance s t
inst)
    Maybe (Either FilePath FilePath)
forall a. Maybe a
Nothing

deadlockInitial :: DeadlockInstance s Transition -> TransitionsList
deadlockInitial :: forall s. DeadlockInstance s Transition -> TransitionsList
deadlockInitial = [Transition] -> TransitionsList
TransitionsList ([Transition] -> TransitionsList)
-> (DeadlockInstance s Transition -> [Transition])
-> DeadlockInstance s Transition
-> TransitionsList
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Transition] -> [Transition]
forall a. [a] -> [a]
reverse ([Transition] -> [Transition])
-> (DeadlockInstance s Transition -> [Transition])
-> DeadlockInstance s Transition
-> [Transition]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Transition -> [Transition]
forall a. Set a -> [a]
S.toList (Set Transition -> [Transition])
-> (DeadlockInstance s Transition -> Set Transition)
-> DeadlockInstance s Transition
-> [Transition]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Net s Transition -> Set Transition
forall s t. Net s t -> Set t
transitions (Net s Transition -> Set Transition)
-> (DeadlockInstance s Transition -> Net s Transition)
-> DeadlockInstance s Transition
-> Set Transition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeadlockInstance s Transition -> Net s Transition
forall s t. DeadlockInstance s t -> Net s t
petriNet

deadlockSyntax
  :: OutputCapable m
  => DeadlockInstance Place Transition
  -> [Transition]
  -> LangM m
deadlockSyntax :: forall (m :: * -> *).
OutputCapable m =>
DeadlockInstance Place Transition -> [Transition] -> LangM m
deadlockSyntax DeadlockInstance Place Transition
inst [Transition]
ts =
  do Net Place Transition -> [Transition] -> LangM m
forall (m :: * -> *) s.
OutputCapable m =>
Net s Transition -> [Transition] -> LangM m
transitionsValid (DeadlockInstance Place Transition -> Net Place Transition
forall s t. DeadlockInstance s t -> Net s t
petriNet DeadlockInstance Place Transition
inst) [Transition]
ts
     Maybe Int -> [Transition] -> LangM m
forall (m :: * -> *) a.
OutputCapable m =>
Maybe Int -> [a] -> LangM m
isNoLonger (DeadlockInstance Place Transition -> Maybe Int
forall s t. DeadlockInstance s t -> Maybe Int
noLongerThan DeadlockInstance Place Transition
inst) [Transition]
ts
     Maybe Int -> [Transition] -> LangM m
forall t (m :: * -> *).
(Enum t, Eq t, OutputCapable m, Show t) =>
Maybe Int -> [t] -> LangM m
rejectSpaceballsPattern (DeadlockInstance Place Transition -> Maybe Int
forall s t. DeadlockInstance s t -> Maybe Int
rejectSpaceballsLength DeadlockInstance Place Transition
inst) [Transition]
ts
     pure ()

deadlockEvaluation
  :: (
    Alternative m,
    MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    OutputCapable m
    )
  => FilePath
  -> DeadlockInstance Place Transition
  -> [Transition]
  -> Rated m
deadlockEvaluation :: forall (m :: * -> *).
(Alternative m, MonadCache m, MonadDiagrams m, MonadGraphviz m,
 MonadThrow m, OutputCapable m) =>
FilePath
-> DeadlockInstance Place Transition -> [Transition] -> Rated m
deadlockEvaluation FilePath
path DeadlockInstance Place Transition
deadlock [Transition]
ts =
  FilePath
-> GraphvizCommand
-> Net ShowPlace ShowTransition
-> [ShowTransition]
-> LangM' m (Either Int (State ShowPlace))
forall (m :: * -> *) s t.
(Alternative m, MonadCache m, MonadDiagrams m, MonadGraphviz m,
 MonadThrow m, Ord s, Ord t, OutputCapable m, Show s, Show t) =>
FilePath
-> GraphvizCommand
-> Net s t
-> [t]
-> LangM' m (Either Int (State s))
executes FilePath
path (DeadlockInstance ShowPlace ShowTransition -> GraphvizCommand
forall s t. DeadlockInstance s t -> GraphvizCommand
drawUsing DeadlockInstance ShowPlace ShowTransition
deadlockInstance) Net ShowPlace ShowTransition
n ((Transition -> ShowTransition) -> [Transition] -> [ShowTransition]
forall a b. (a -> b) -> [a] -> [b]
map Transition -> ShowTransition
ShowTransition [Transition]
ts)
  LangM' m (Either Int (State ShowPlace))
-> (Either Int (State ShowPlace)
    -> GenericLangM Language m Rational)
-> GenericLangM Language m Rational
forall (m :: * -> *) l a b.
Monad m =>
GenericLangM l m a
-> (a -> GenericLangM l m b) -> GenericLangM l m b
$>>= \Either Int (State ShowPlace)
eitherOutcome ->
    Either Int (State ShowPlace)
-> (State ShowPlace -> GenericLangM Language m ())
-> GenericLangM Language m ()
forall (m :: * -> *) a b.
Applicative m =>
Either a b -> (b -> m ()) -> m ()
whenRight Either Int (State ShowPlace)
eitherOutcome (\State ShowPlace
outcome ->
      Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall (m :: * -> *). OutputCapable m => Bool -> LangM m -> LangM m
yesNo ([(ShowTransition, State ShowPlace)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(ShowTransition, State ShowPlace)] -> Bool)
-> [(ShowTransition, State ShowPlace)] -> Bool
forall a b. (a -> b) -> a -> b
$ Net ShowPlace ShowTransition
-> State ShowPlace -> [(ShowTransition, State ShowPlace)]
forall s t. Ord s => Net s t -> State s -> [(t, State s)]
successors Net ShowPlace ShowTransition
n State ShowPlace
outcome)
      (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State (Map Language FilePath) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l FilePath) () -> GenericLangM l m ()
translate (State (Map Language FilePath) () -> GenericLangM Language m ())
-> State (Map Language FilePath) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
          FilePath -> State (Map Language FilePath) ()
english FilePath
"All transitions disabled in reached marking?"
          FilePath -> State (Map Language FilePath) ()
german FilePath
"Alle Transitionen deaktiviert in erreichter Markierung?"
      )
  GenericLangM Language m ()
-> GenericLangM Language m Rational
-> GenericLangM Language m Rational
forall (m :: * -> *) l a b.
Monad m =>
GenericLangM l m a -> GenericLangM l m b -> GenericLangM l m b
$>> Maybe FilePath
-> (DeadlockInstance ShowPlace ShowTransition
    -> State ShowPlace -> Bool)
-> (DeadlockInstance ShowPlace ShowTransition -> Int)
-> DeadlockInstance ShowPlace ShowTransition
-> [Transition]
-> Either Int (State ShowPlace)
-> GenericLangM Language m Rational
forall (m :: * -> *) i a b.
OutputCapable m =>
Maybe FilePath
-> (i -> a -> Bool)
-> (i -> Int)
-> i
-> [b]
-> Either Int a
-> Rated m
assertReachPoints
    Maybe FilePath
aSolution
    ((State ShowPlace -> Bool)
-> DeadlockInstance ShowPlace ShowTransition
-> State ShowPlace
-> Bool
forall a b. a -> b -> a
const ((State ShowPlace -> Bool)
 -> DeadlockInstance ShowPlace ShowTransition
 -> State ShowPlace
 -> Bool)
-> (State ShowPlace -> Bool)
-> DeadlockInstance ShowPlace ShowTransition
-> State ShowPlace
-> Bool
forall a b. (a -> b) -> a -> b
$ [(ShowTransition, State ShowPlace)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(ShowTransition, State ShowPlace)] -> Bool)
-> (State ShowPlace -> [(ShowTransition, State ShowPlace)])
-> State ShowPlace
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Net ShowPlace ShowTransition
-> State ShowPlace -> [(ShowTransition, State ShowPlace)]
forall s t. Ord s => Net s t -> State s -> [(t, State s)]
successors Net ShowPlace ShowTransition
n)
    DeadlockInstance ShowPlace ShowTransition -> Int
forall s t. DeadlockInstance s t -> Int
minLength
    DeadlockInstance ShowPlace ShowTransition
deadlockInstance
    [Transition]
ts
    Either Int (State ShowPlace)
eitherOutcome
  where
    deadlockInstance :: DeadlockInstance ShowPlace ShowTransition
deadlockInstance = DeadlockInstance Place Transition
-> DeadlockInstance ShowPlace ShowTransition
toShowDeadlockInstance DeadlockInstance Place Transition
deadlock
    n :: Net ShowPlace ShowTransition
n = DeadlockInstance ShowPlace ShowTransition
-> Net ShowPlace ShowTransition
forall s t. DeadlockInstance s t -> Net s t
petriNet DeadlockInstance ShowPlace ShowTransition
deadlockInstance
    aSolution :: Maybe FilePath
aSolution = Int
-> Either (NonEmpty [Transition]) (NonEmpty [Transition])
-> Maybe FilePath
provideSolutionsFeedback (DeadlockInstance Place Transition -> Int
forall s t. DeadlockInstance s t -> Int
maxDisplayedSolutions DeadlockInstance Place Transition
deadlock) (DeadlockInstance Place Transition
-> Either (NonEmpty [Transition]) (NonEmpty [Transition])
forall s t.
DeadlockInstance s t -> Either (NonEmpty [t]) (NonEmpty [t])
shortestSolutions DeadlockInstance Place Transition
deadlock)

data DeadlockInstance s t = DeadlockInstance {
  forall s t. DeadlockInstance s t -> GraphvizCommand
drawUsing         :: GraphvizCommand,
  forall s t. DeadlockInstance s t -> Int
minLength         :: Int,
  forall s t. DeadlockInstance s t -> Maybe Int
noLongerThan      :: Maybe Int,
  forall s t. DeadlockInstance s t -> Net s t
petriNet          :: Net s t,
  forall s t. DeadlockInstance s t -> Bool
showPlaceNames    :: Bool,
  forall s t. DeadlockInstance s t -> Int
maxDisplayedSolutions :: Int,
  -- | Solutions to the deadlock task.
  -- 'Left' contains (some) shortest solutions when no filtering is applied.
  -- 'Right' contains all solutions when filtering is applied.
  -- Note: 'Left' may not contain all shortest solutions, only up to 'maxDisplayedSolutions'.
  forall s t.
DeadlockInstance s t -> Either (NonEmpty [t]) (NonEmpty [t])
shortestSolutions :: Either (NonEmpty [t]) (NonEmpty [t]),
  forall s t. DeadlockInstance s t -> Maybe Int
withLengthHint    :: Maybe Int,
  forall s t. DeadlockInstance s t -> Bool
withMinLengthHint :: Bool,
  -- | Minimum length of Spaceballs PIN pattern to reject during syntax checking.
  -- If set to @Just n@, sequences starting with @n@ or more consecutive transitions
  -- (e.g., @[t1, t2, t3, t4]@) will be rejected.
  forall s t. DeadlockInstance s t -> Maybe Int
rejectSpaceballsLength :: Maybe Int
  } deriving ((forall x. DeadlockInstance s t -> Rep (DeadlockInstance s t) x)
-> (forall x. Rep (DeadlockInstance s t) x -> DeadlockInstance s t)
-> Generic (DeadlockInstance s t)
forall x. Rep (DeadlockInstance s t) x -> DeadlockInstance s t
forall x. DeadlockInstance s t -> Rep (DeadlockInstance s t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s t x. Rep (DeadlockInstance s t) x -> DeadlockInstance s t
forall s t x. DeadlockInstance s t -> Rep (DeadlockInstance s t) x
$cfrom :: forall s t x. DeadlockInstance s t -> Rep (DeadlockInstance s t) x
from :: forall x. DeadlockInstance s t -> Rep (DeadlockInstance s t) x
$cto :: forall s t x. Rep (DeadlockInstance s t) x -> DeadlockInstance s t
to :: forall x. Rep (DeadlockInstance s t) x -> DeadlockInstance s t
Generic, ReadPrec [DeadlockInstance s t]
ReadPrec (DeadlockInstance s t)
Int -> ReadS (DeadlockInstance s t)
ReadS [DeadlockInstance s t]
(Int -> ReadS (DeadlockInstance s t))
-> ReadS [DeadlockInstance s t]
-> ReadPrec (DeadlockInstance s t)
-> ReadPrec [DeadlockInstance s t]
-> Read (DeadlockInstance s t)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadPrec [DeadlockInstance s t]
forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadPrec (DeadlockInstance s t)
forall s t.
(Read s, Read t, Ord s, Ord t) =>
Int -> ReadS (DeadlockInstance s t)
forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadS [DeadlockInstance s t]
$creadsPrec :: forall s t.
(Read s, Read t, Ord s, Ord t) =>
Int -> ReadS (DeadlockInstance s t)
readsPrec :: Int -> ReadS (DeadlockInstance s t)
$creadList :: forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadS [DeadlockInstance s t]
readList :: ReadS [DeadlockInstance s t]
$creadPrec :: forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadPrec (DeadlockInstance s t)
readPrec :: ReadPrec (DeadlockInstance s t)
$creadListPrec :: forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadPrec [DeadlockInstance s t]
readListPrec :: ReadPrec [DeadlockInstance s t]
Read, Int -> DeadlockInstance s t -> ShowS
[DeadlockInstance s t] -> ShowS
DeadlockInstance s t -> FilePath
(Int -> DeadlockInstance s t -> ShowS)
-> (DeadlockInstance s t -> FilePath)
-> ([DeadlockInstance s t] -> ShowS)
-> Show (DeadlockInstance s t)
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
forall s t.
(Show s, Show t) =>
Int -> DeadlockInstance s t -> ShowS
forall s t. (Show s, Show t) => [DeadlockInstance s t] -> ShowS
forall s t. (Show s, Show t) => DeadlockInstance s t -> FilePath
$cshowsPrec :: forall s t.
(Show s, Show t) =>
Int -> DeadlockInstance s t -> ShowS
showsPrec :: Int -> DeadlockInstance s t -> ShowS
$cshow :: forall s t. (Show s, Show t) => DeadlockInstance s t -> FilePath
show :: DeadlockInstance s t -> FilePath
$cshowList :: forall s t. (Show s, Show t) => [DeadlockInstance s t] -> ShowS
showList :: [DeadlockInstance s t] -> ShowS
Show, Parser [DeadlockInstance s t]
Parser (DeadlockInstance s t)
Int -> Parser (DeadlockInstance s t)
Parser (DeadlockInstance s t)
-> (Int -> Parser (DeadlockInstance s t))
-> Parser (DeadlockInstance s t)
-> (Int -> Parser (DeadlockInstance s t))
-> Parser [DeadlockInstance s t]
-> Reader (DeadlockInstance s t)
forall a.
Parser a
-> (Int -> Parser a)
-> Parser a
-> (Int -> Parser a)
-> Parser [a]
-> Reader a
forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser [DeadlockInstance s t]
forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser (DeadlockInstance s t)
forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Int -> Parser (DeadlockInstance s t)
$catomic_reader :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser (DeadlockInstance s t)
atomic_reader :: Parser (DeadlockInstance s t)
$catomic_readerPrec :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Int -> Parser (DeadlockInstance s t)
atomic_readerPrec :: Int -> Parser (DeadlockInstance s t)
$creader :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser (DeadlockInstance s t)
reader :: Parser (DeadlockInstance s t)
$creaderPrec :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Int -> Parser (DeadlockInstance s t)
readerPrec :: Int -> Parser (DeadlockInstance s t)
$creaderList :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser [DeadlockInstance s t]
readerList :: Parser [DeadlockInstance s t]
Reader, Int -> DeadlockInstance s t -> Doc
[DeadlockInstance s t] -> Doc
(Int -> DeadlockInstance s t -> Doc)
-> ([DeadlockInstance s t] -> Doc) -> ToDoc (DeadlockInstance s t)
forall a. (Int -> a -> Doc) -> ([a] -> Doc) -> ToDoc a
forall s t.
(ToDoc s, ToDoc t) =>
Int -> DeadlockInstance s t -> Doc
forall s t. (ToDoc s, ToDoc t) => [DeadlockInstance s t] -> Doc
$ctoDocPrec :: forall s t.
(ToDoc s, ToDoc t) =>
Int -> DeadlockInstance s t -> Doc
toDocPrec :: Int -> DeadlockInstance s t -> Doc
$ctoDocList :: forall s t. (ToDoc s, ToDoc t) => [DeadlockInstance s t] -> Doc
toDocList :: [DeadlockInstance s t] -> Doc
ToDoc)
#if !MIN_VERSION_base(4,18,0)
  deriving Typeable
#endif

bimapDeadlockInstance
  :: (Ord a, Ord b)
  => (s -> a)
  -> (t -> b)
  -> DeadlockInstance s t
  -> DeadlockInstance a b
bimapDeadlockInstance :: forall a b s t.
(Ord a, Ord b) =>
(s -> a)
-> (t -> b) -> DeadlockInstance s t -> DeadlockInstance a b
bimapDeadlockInstance s -> a
f t -> b
g DeadlockInstance {Bool
Int
Maybe Int
Either (NonEmpty [t]) (NonEmpty [t])
GraphvizCommand
Net s t
petriNet :: forall s t. DeadlockInstance s t -> Net s t
showPlaceNames :: forall s t. DeadlockInstance s t -> Bool
drawUsing :: forall s t. DeadlockInstance s t -> GraphvizCommand
noLongerThan :: forall s t. DeadlockInstance s t -> Maybe Int
withLengthHint :: forall s t. DeadlockInstance s t -> Maybe Int
minLength :: forall s t. DeadlockInstance s t -> Int
withMinLengthHint :: forall s t. DeadlockInstance s t -> Bool
rejectSpaceballsLength :: forall s t. DeadlockInstance s t -> Maybe Int
maxDisplayedSolutions :: forall s t. DeadlockInstance s t -> Int
shortestSolutions :: forall s t.
DeadlockInstance s t -> Either (NonEmpty [t]) (NonEmpty [t])
drawUsing :: GraphvizCommand
minLength :: Int
noLongerThan :: Maybe Int
petriNet :: Net s t
showPlaceNames :: Bool
maxDisplayedSolutions :: Int
shortestSolutions :: Either (NonEmpty [t]) (NonEmpty [t])
withLengthHint :: Maybe Int
withMinLengthHint :: Bool
rejectSpaceballsLength :: Maybe Int
..} = DeadlockInstance {
    drawUsing :: GraphvizCommand
drawUsing         = GraphvizCommand
drawUsing,
    minLength :: Int
minLength         = Int
minLength,
    noLongerThan :: Maybe Int
noLongerThan      = Maybe Int
noLongerThan,
    petriNet :: Net a b
petriNet          = (s -> a) -> (t -> b) -> Net s t -> Net a b
forall a b s t.
(Ord a, Ord b) =>
(s -> a) -> (t -> b) -> Net s t -> Net a b
bimapNet s -> a
f t -> b
g Net s t
petriNet,
    showPlaceNames :: Bool
showPlaceNames    = Bool
showPlaceNames,
    maxDisplayedSolutions :: Int
maxDisplayedSolutions = Int
maxDisplayedSolutions,
    shortestSolutions :: Either (NonEmpty [b]) (NonEmpty [b])
shortestSolutions = (NonEmpty [t] -> NonEmpty [b])
-> (NonEmpty [t] -> NonEmpty [b])
-> Either (NonEmpty [t]) (NonEmpty [t])
-> Either (NonEmpty [b]) (NonEmpty [b])
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (([t] -> [b]) -> NonEmpty [t] -> NonEmpty [b]
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((t -> b) -> [t] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map t -> b
g)) (([t] -> [b]) -> NonEmpty [t] -> NonEmpty [b]
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((t -> b) -> [t] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map t -> b
g)) Either (NonEmpty [t]) (NonEmpty [t])
shortestSolutions,
    withLengthHint :: Maybe Int
withLengthHint    = Maybe Int
withLengthHint,
    withMinLengthHint :: Bool
withMinLengthHint = Bool
withMinLengthHint,
    rejectSpaceballsLength :: Maybe Int
rejectSpaceballsLength = Maybe Int
rejectSpaceballsLength
    }

toShowDeadlockInstance
  :: DeadlockInstance Place Transition
  -> DeadlockInstance ShowPlace ShowTransition
toShowDeadlockInstance :: DeadlockInstance Place Transition
-> DeadlockInstance ShowPlace ShowTransition
toShowDeadlockInstance = (Place -> ShowPlace)
-> (Transition -> ShowTransition)
-> DeadlockInstance Place Transition
-> DeadlockInstance ShowPlace ShowTransition
forall a b s t.
(Ord a, Ord b) =>
(s -> a)
-> (t -> b) -> DeadlockInstance s t -> DeadlockInstance a b
bimapDeadlockInstance Place -> ShowPlace
ShowPlace Transition -> ShowTransition
ShowTransition

-- | Configuration for deadlock task generation.
-- Note: The two kinds of fusable transition/place situations (consuming-fusable and producing-fusable)
-- are guaranteed to be non-overlapping. No transition will be both consuming-fusable and producing-fusable
-- and no such transitions will share a fusing-relevant place.
data DeadlockConfig = DeadlockConfig {
  DeadlockConfig -> Int
numPlaces :: Int,
  DeadlockConfig -> Int
numTransitions :: Int,
  DeadlockConfig -> Capacity Place
capacity :: Capacity Place,
  -- | Graph layout commands to choose from (randomly selected during generation)
  DeadlockConfig -> [GraphvizCommand]
graphLayouts :: [GraphvizCommand],
  DeadlockConfig -> Int
maxTransitionLength :: Int,
  DeadlockConfig -> Int
minTransitionLength :: Int,
  DeadlockConfig -> TransitionBehaviorConstraints
transitionBehaviorConstraints :: TransitionBehaviorConstraints,
  DeadlockConfig -> ArrowDensityConstraints
arrowDensityConstraints :: ArrowDensityConstraints,
  DeadlockConfig -> Int
maxPrintedSolutions :: Int,
  DeadlockConfig -> Maybe Int
rejectLongerThan    :: Maybe Int,
  DeadlockConfig -> Bool
showLengthHint      :: Bool,
  DeadlockConfig -> Bool
showMinLengthHint   :: Bool,
  DeadlockConfig -> Bool
showPlaceNamesInNet :: Bool,
  -- | Require exactly this many transitions with exactly one input place,
  -- which is exclusively consumed from by that transition.
  -- If @Nothing@, no constraint on fusable transitions consuming.
  DeadlockConfig -> Maybe Int
fusableTransitionsConsumingAreExactly :: Maybe Int,
  -- | Require exactly this many transitions with exactly one output place,
  -- which is exclusively produced to by that transition.
  -- If @Nothing@, no constraint on fusable transitions producing.
  DeadlockConfig -> Maybe Int
fusableTransitionsProducingAreExactly :: Maybe Int,
  DeadlockConfig -> FilterConfig
filterConfig        :: FilterConfig
  }
  deriving ((forall x. DeadlockConfig -> Rep DeadlockConfig x)
-> (forall x. Rep DeadlockConfig x -> DeadlockConfig)
-> Generic DeadlockConfig
forall x. Rep DeadlockConfig x -> DeadlockConfig
forall x. DeadlockConfig -> Rep DeadlockConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DeadlockConfig -> Rep DeadlockConfig x
from :: forall x. DeadlockConfig -> Rep DeadlockConfig x
$cto :: forall x. Rep DeadlockConfig x -> DeadlockConfig
to :: forall x. Rep DeadlockConfig x -> DeadlockConfig
Generic, ReadPrec [DeadlockConfig]
ReadPrec DeadlockConfig
Int -> ReadS DeadlockConfig
ReadS [DeadlockConfig]
(Int -> ReadS DeadlockConfig)
-> ReadS [DeadlockConfig]
-> ReadPrec DeadlockConfig
-> ReadPrec [DeadlockConfig]
-> Read DeadlockConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS DeadlockConfig
readsPrec :: Int -> ReadS DeadlockConfig
$creadList :: ReadS [DeadlockConfig]
readList :: ReadS [DeadlockConfig]
$creadPrec :: ReadPrec DeadlockConfig
readPrec :: ReadPrec DeadlockConfig
$creadListPrec :: ReadPrec [DeadlockConfig]
readListPrec :: ReadPrec [DeadlockConfig]
Read, Int -> DeadlockConfig -> ShowS
[DeadlockConfig] -> ShowS
DeadlockConfig -> FilePath
(Int -> DeadlockConfig -> ShowS)
-> (DeadlockConfig -> FilePath)
-> ([DeadlockConfig] -> ShowS)
-> Show DeadlockConfig
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DeadlockConfig -> ShowS
showsPrec :: Int -> DeadlockConfig -> ShowS
$cshow :: DeadlockConfig -> FilePath
show :: DeadlockConfig -> FilePath
$cshowList :: [DeadlockConfig] -> ShowS
showList :: [DeadlockConfig] -> ShowS
Show)
#if !MIN_VERSION_base(4,18,0)
  deriving Typeable
#endif

defaultDeadlockConfig :: DeadlockConfig
defaultDeadlockConfig :: DeadlockConfig
defaultDeadlockConfig =
  DeadlockConfig {
  numPlaces :: Int
numPlaces = Int
6,
  numTransitions :: Int
numTransitions = Int
6,
  capacity :: Capacity Place
Modelling.PetriNet.Reach.Deadlock.capacity = Capacity Place
forall s. Capacity s
Unbounded,
  graphLayouts :: [GraphvizCommand]
graphLayouts = [GraphvizCommand
Dot, GraphvizCommand
Neato, GraphvizCommand
TwoPi, GraphvizCommand
Circo, GraphvizCommand
Fdp, GraphvizCommand
Sfdp, GraphvizCommand
Osage, GraphvizCommand
Patchwork],
  maxTransitionLength :: Int
maxTransitionLength = Int
8,
  minTransitionLength :: Int
minTransitionLength = Int
8,
  transitionBehaviorConstraints :: TransitionBehaviorConstraints
transitionBehaviorConstraints = TransitionBehaviorConstraints
noTransitionBehaviorConstraints,
  arrowDensityConstraints :: ArrowDensityConstraints
arrowDensityConstraints = ArrowDensityConstraints
noArrowDensityConstraints,
  maxPrintedSolutions :: Int
maxPrintedSolutions = Int
0,
  rejectLongerThan :: Maybe Int
rejectLongerThan    = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
8,
  showLengthHint :: Bool
showLengthHint      = Bool
False,
  showMinLengthHint :: Bool
showMinLengthHint   = Bool
True,
  showPlaceNamesInNet :: Bool
showPlaceNamesInNet = Bool
False,
  fusableTransitionsConsumingAreExactly :: Maybe Int
fusableTransitionsConsumingAreExactly = Maybe Int
forall a. Maybe a
Nothing,
  fusableTransitionsProducingAreExactly :: Maybe Int
fusableTransitionsProducingAreExactly = Maybe Int
forall a. Maybe a
Nothing,
  filterConfig :: FilterConfig
filterConfig        = FilterConfig
defaultFilterConfig { solutionSetLimit = Nothing, forbiddenCycleLengths = [4], requireCycleLengthsAny = [], transitionCoverageRequirement = 1 % 2 }
  }

defaultDeadlockInstance :: DeadlockInstance Place Transition
defaultDeadlockInstance :: DeadlockInstance Place Transition
defaultDeadlockInstance = DeadlockInstance {
  drawUsing :: GraphvizCommand
drawUsing         = GraphvizCommand
Circo,
  minLength :: Int
minLength         = Int
6,
  noLongerThan :: Maybe Int
noLongerThan      = Maybe Int
forall a. Maybe a
Nothing,
  petriNet :: Net Place Transition
petriNet          = (Net Place Transition, State Place) -> Net Place Transition
forall a b. (a, b) -> a
fst (Net Place Transition, State Place)
example,
  showPlaceNames :: Bool
showPlaceNames    = Bool
False,
  maxDisplayedSolutions :: Int
maxDisplayedSolutions = Int
0,
  shortestSolutions :: Either (NonEmpty [Transition]) (NonEmpty [Transition])
shortestSolutions = NonEmpty [Transition]
-> Either (NonEmpty [Transition]) (NonEmpty [Transition])
forall a b. a -> Either a b
Left ([] [Transition] -> [[Transition]] -> NonEmpty [Transition]
forall a. a -> [a] -> NonEmpty a
:| []), -- TO DO: add a solution
  withLengthHint :: Maybe Int
withLengthHint    = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
9,
  withMinLengthHint :: Bool
withMinLengthHint = Bool
True,
  rejectSpaceballsLength :: Maybe Int
rejectSpaceballsLength = Maybe Int
forall a. Maybe a
Nothing
  }

checkFusableNodeConfig
  :: Maybe Int  -- ^ fusableTransitionsConsumingAreExactly
  -> Maybe Int  -- ^ fusableTransitionsProducingAreExactly
  -> Int        -- ^ numTransitions
  -> Int        -- ^ numPlaces
  -> ArrowDensityConstraints
  -> Maybe String
checkFusableNodeConfig :: Maybe Int
-> Maybe Int
-> Int
-> Int
-> ArrowDensityConstraints
-> Maybe FilePath
checkFusableNodeConfig Maybe Int
maybeConsuming Maybe Int
maybeProducing Int
numTrans Int
numPlaces 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)
totalArrowsFromTransitionsToPlaces :: ArrowDensityConstraints -> (Int, Maybe Int)
totalArrowsFromPlacesToTransitions :: ArrowDensityConstraints -> (Int, Maybe Int)
outgoingArrowsPerPlace :: ArrowDensityConstraints -> (Int, Maybe Int)
incomingArrowsPerPlace :: ArrowDensityConstraints -> (Int, Maybe Int)
outgoingArrowsPerTransition :: ArrowDensityConstraints -> (Int, Maybe Int)
incomingArrowsPerTransition :: ArrowDensityConstraints -> (Int, Maybe Int)
..}
  | let relevantConsumingCount :: Int
relevantConsumingCount = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 Maybe Int
maybeConsuming
  , let relevantProducingCount :: Int
relevantProducingCount = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 Maybe Int
maybeProducing
  , Int
relevantConsumingCount Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
relevantProducingCount Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
    Bool -> Bool -> Bool
|| Int
relevantConsumingCount Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
relevantProducingCount Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
numTrans Int
numPlaces
  = FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
"fusable transitions requirements must not be negative and together cannot exceed numTransitions or numPlaces"
  | Bool
otherwise
  = Maybe Int
-> (Int, Maybe Int) -> FilePath -> FilePath -> Maybe FilePath
forall {a} {a} {a}.
(Ord a, Ord a, Num a, Num a, Num a, Eq a) =>
Maybe a -> (a, Maybe a) -> FilePath -> FilePath -> Maybe FilePath
checkConflicts Maybe Int
maybeConsuming (Int, Maybe Int)
incomingArrowsPerTransition FilePath
"Consuming" FilePath
"incomingArrowsPerTransition"
    Maybe FilePath -> Maybe FilePath -> Maybe FilePath
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe Int
-> (Int, Maybe Int) -> FilePath -> FilePath -> Maybe FilePath
forall {a} {a} {a}.
(Ord a, Ord a, Num a, Num a, Num a, Eq a) =>
Maybe a -> (a, Maybe a) -> FilePath -> FilePath -> Maybe FilePath
checkConflicts Maybe Int
maybeProducing (Int, Maybe Int)
outgoingArrowsPerTransition FilePath
"Producing" FilePath
"outgoingArrowsPerTransition"
    Maybe FilePath -> Maybe FilePath -> Maybe FilePath
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe Int
-> (Int, Maybe Int) -> FilePath -> FilePath -> Maybe FilePath
forall {a} {a} {a}.
(Ord a, Ord a, Num a, Num a, Num a, Eq a) =>
Maybe a -> (a, Maybe a) -> FilePath -> FilePath -> Maybe FilePath
checkConflicts Maybe Int
maybeConsuming (Int, Maybe Int)
outgoingArrowsPerPlace FilePath
"Consuming" FilePath
"outgoingArrowsPerPlace"
    Maybe FilePath -> Maybe FilePath -> Maybe FilePath
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe Int
-> (Int, Maybe Int) -> FilePath -> FilePath -> Maybe FilePath
forall {a} {a} {a}.
(Ord a, Ord a, Num a, Num a, Num a, Eq a) =>
Maybe a -> (a, Maybe a) -> FilePath -> FilePath -> Maybe FilePath
checkConflicts Maybe Int
maybeProducing (Int, Maybe Int)
incomingArrowsPerPlace FilePath
"Producing" FilePath
"incomingArrowsPerPlace"
    Maybe FilePath -> Maybe FilePath -> Maybe FilePath
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe Int -> Int -> FilePath -> FilePath -> Maybe FilePath
forall {a}.
Ord a =>
Maybe a -> a -> FilePath -> FilePath -> Maybe FilePath
checkTotalLower Maybe Int
maybeConsuming ((Int, Maybe Int) -> Int
forall a b. (a, b) -> a
fst (Int, Maybe Int)
totalArrowsFromPlacesToTransitions) FilePath
"Consuming" FilePath
"totalArrowsFromPlacesToTransitions"
    Maybe FilePath -> Maybe FilePath -> Maybe FilePath
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe Int -> Int -> FilePath -> FilePath -> Maybe FilePath
forall {a}.
Ord a =>
Maybe a -> a -> FilePath -> FilePath -> Maybe FilePath
checkTotalLower Maybe Int
maybeProducing ((Int, Maybe Int) -> Int
forall a b. (a, b) -> a
fst (Int, Maybe Int)
totalArrowsFromTransitionsToPlaces) FilePath
"Producing" FilePath
"totalArrowsFromTransitionsToPlaces"
  where
    checkConflicts :: Maybe a -> (a, Maybe a) -> FilePath -> FilePath -> Maybe FilePath
checkConflicts Maybe a
maybeCount (a
minVal, Maybe a
maxVal) FilePath
nodeType FilePath
constraintName
      | Just a
count <- Maybe a
maybeCount, a
count a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0, a
minVal a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
1
      = FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just (FilePath -> Maybe FilePath) -> FilePath -> Maybe FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
"fusableTransitions" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
nodeType FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"AreExactly > 0 conflicts with " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
constraintName FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
" minimum > 1"
      | Just a
count <- Maybe a
maybeCount, a
count a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0, Maybe a
maxVal Maybe a -> Maybe a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Maybe a
forall a. a -> Maybe a
Just a
0
      = FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just (FilePath -> Maybe FilePath) -> FilePath -> Maybe FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
"fusableTransitions" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
nodeType FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"AreExactly > 0 conflicts with " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
constraintName FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
" maximum = 0"
      | Bool
otherwise = Maybe FilePath
forall a. Maybe a
Nothing
    checkTotalLower :: Maybe a -> a -> FilePath -> FilePath -> Maybe FilePath
checkTotalLower Maybe a
maybeCount a
totalMin FilePath
nodeType FilePath
constraintName
      | Just a
count <- Maybe a
maybeCount, a
totalMin a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
count
      = FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just (FilePath -> Maybe FilePath) -> FilePath -> Maybe FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
"having fewer " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
constraintName FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
" than fusableTransitions" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
nodeType FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"AreExactly makes no sense"
      | Bool
otherwise = Maybe FilePath
forall a. Maybe a
Nothing

checkDeadlockConfig :: DeadlockConfig -> Maybe String
checkDeadlockConfig :: DeadlockConfig -> Maybe FilePath
checkDeadlockConfig DeadlockConfig {Bool
Int
[GraphvizCommand]
Maybe Int
FilterConfig
ArrowDensityConstraints
TransitionBehaviorConstraints
Capacity Place
numPlaces :: DeadlockConfig -> Int
numTransitions :: DeadlockConfig -> Int
capacity :: DeadlockConfig -> Capacity Place
graphLayouts :: DeadlockConfig -> [GraphvizCommand]
maxTransitionLength :: DeadlockConfig -> Int
minTransitionLength :: DeadlockConfig -> Int
transitionBehaviorConstraints :: DeadlockConfig -> TransitionBehaviorConstraints
arrowDensityConstraints :: DeadlockConfig -> ArrowDensityConstraints
maxPrintedSolutions :: DeadlockConfig -> Int
rejectLongerThan :: DeadlockConfig -> Maybe Int
showLengthHint :: DeadlockConfig -> Bool
showMinLengthHint :: DeadlockConfig -> Bool
showPlaceNamesInNet :: DeadlockConfig -> Bool
fusableTransitionsConsumingAreExactly :: DeadlockConfig -> Maybe Int
fusableTransitionsProducingAreExactly :: DeadlockConfig -> Maybe Int
filterConfig :: DeadlockConfig -> FilterConfig
numPlaces :: Int
numTransitions :: Int
capacity :: Capacity Place
graphLayouts :: [GraphvizCommand]
maxTransitionLength :: Int
minTransitionLength :: Int
transitionBehaviorConstraints :: TransitionBehaviorConstraints
arrowDensityConstraints :: ArrowDensityConstraints
maxPrintedSolutions :: Int
rejectLongerThan :: Maybe Int
showLengthHint :: Bool
showMinLengthHint :: Bool
showPlaceNamesInNet :: Bool
fusableTransitionsConsumingAreExactly :: Maybe Int
fusableTransitionsProducingAreExactly :: Maybe Int
filterConfig :: FilterConfig
..} =
  Int
-> Int
-> Capacity Place
-> Int
-> Int
-> TransitionBehaviorConstraints
-> ArrowDensityConstraints
-> [GraphvizCommand]
-> Maybe Int
-> Bool
-> Maybe FilePath
forall s.
Int
-> Int
-> Capacity s
-> Int
-> Int
-> TransitionBehaviorConstraints
-> ArrowDensityConstraints
-> [GraphvizCommand]
-> Maybe Int
-> Bool
-> Maybe FilePath
checkBasicPetriConfig
    Int
numPlaces
    Int
numTransitions
    Capacity Place
capacity
    Int
minTransitionLength
    Int
maxTransitionLength
    TransitionBehaviorConstraints
transitionBehaviorConstraints
    ArrowDensityConstraints
arrowDensityConstraints
    [GraphvizCommand]
graphLayouts
    Maybe Int
rejectLongerThan
    Bool
showLengthHint
  Maybe FilePath -> Maybe FilePath -> Maybe FilePath
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  Maybe Int -> Int -> Int -> FilterConfig -> Maybe FilePath
checkFilterConfigWith
    Maybe Int
rejectLongerThan
    Int
minTransitionLength
    Int
numTransitions
    FilterConfig
filterConfig
  Maybe FilePath -> Maybe FilePath -> Maybe FilePath
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  Maybe Int
-> Maybe Int
-> Int
-> Int
-> ArrowDensityConstraints
-> Maybe FilePath
checkFusableNodeConfig
    Maybe Int
fusableTransitionsConsumingAreExactly
    Maybe Int
fusableTransitionsProducingAreExactly
    Int
numTransitions
    Int
numPlaces
    ArrowDensityConstraints
arrowDensityConstraints
  Maybe FilePath -> Maybe FilePath -> Maybe FilePath
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  if Int
maxPrintedSolutions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
    then FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
"maxPrintedSolutions must be non-negative"
    else case FilterConfig -> Maybe Int
solutionSetLimit FilterConfig
filterConfig of
      Just Int
maxSolutions | Int
maxPrintedSolutions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxSolutions ->
        FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
"maxPrintedSolutions cannot be greater than solutionSetLimit"
      Maybe Int
_ -> Maybe FilePath
forall a. Maybe a
Nothing

generateDeadlock
  :: (MonadCatch m, MonadDiagrams m, MonadGraphviz m)
  => DeadlockConfig
  -> Int
  -> m (DeadlockInstance Place Transition)
generateDeadlock :: forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
DeadlockConfig -> Int -> m (DeadlockInstance Place Transition)
generateDeadlock conf :: DeadlockConfig
conf@DeadlockConfig {Bool
Int
[GraphvizCommand]
Maybe Int
FilterConfig
ArrowDensityConstraints
TransitionBehaviorConstraints
Capacity Place
numPlaces :: DeadlockConfig -> Int
numTransitions :: DeadlockConfig -> Int
capacity :: DeadlockConfig -> Capacity Place
graphLayouts :: DeadlockConfig -> [GraphvizCommand]
maxTransitionLength :: DeadlockConfig -> Int
minTransitionLength :: DeadlockConfig -> Int
transitionBehaviorConstraints :: DeadlockConfig -> TransitionBehaviorConstraints
arrowDensityConstraints :: DeadlockConfig -> ArrowDensityConstraints
maxPrintedSolutions :: DeadlockConfig -> Int
rejectLongerThan :: DeadlockConfig -> Maybe Int
showLengthHint :: DeadlockConfig -> Bool
showMinLengthHint :: DeadlockConfig -> Bool
showPlaceNamesInNet :: DeadlockConfig -> Bool
fusableTransitionsConsumingAreExactly :: DeadlockConfig -> Maybe Int
fusableTransitionsProducingAreExactly :: DeadlockConfig -> Maybe Int
filterConfig :: DeadlockConfig -> FilterConfig
numPlaces :: Int
numTransitions :: Int
capacity :: Capacity Place
graphLayouts :: [GraphvizCommand]
maxTransitionLength :: Int
minTransitionLength :: Int
transitionBehaviorConstraints :: TransitionBehaviorConstraints
arrowDensityConstraints :: ArrowDensityConstraints
maxPrintedSolutions :: Int
rejectLongerThan :: Maybe Int
showLengthHint :: Bool
showMinLengthHint :: Bool
showPlaceNamesInNet :: Bool
fusableTransitionsConsumingAreExactly :: Maybe Int
fusableTransitionsProducingAreExactly :: Maybe Int
filterConfig :: FilterConfig
..} Int
seed = do
  (Net Place Transition
petri, GraphvizCommand
cmd, Either (NonEmpty [Transition]) (NonEmpty [Transition])
solutionsList) <- DeadlockConfig
-> Int
-> m (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
DeadlockConfig
-> Int
-> m (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
tries DeadlockConfig
conf Int
seed
  DeadlockInstance Place Transition
-> m (DeadlockInstance Place Transition)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DeadlockInstance {
    drawUsing :: GraphvizCommand
drawUsing         = GraphvizCommand
cmd,
    minLength :: Int
minLength         = Int
minTransitionLength,
    noLongerThan :: Maybe Int
noLongerThan      = Maybe Int
rejectLongerThan,
    petriNet :: Net Place Transition
petriNet          = Net Place Transition
petri,
    showPlaceNames :: Bool
showPlaceNames    = Bool
showPlaceNamesInNet,
    maxDisplayedSolutions :: Int
maxDisplayedSolutions = Int
maxPrintedSolutions,
    shortestSolutions :: Either (NonEmpty [Transition]) (NonEmpty [Transition])
shortestSolutions = Either (NonEmpty [Transition]) (NonEmpty [Transition])
solutionsList,
    withLengthHint :: Maybe Int
withLengthHint    =
      if Bool
showLengthHint then Int -> Maybe Int
forall a. a -> Maybe a
Just Int
maxTransitionLength else Maybe Int
forall a. Maybe a
Nothing,
    withMinLengthHint :: Bool
withMinLengthHint = Bool
showMinLengthHint,
    rejectSpaceballsLength :: Maybe Int
rejectSpaceballsLength = FilterConfig -> Maybe Int
spaceballsPrefixThreshold FilterConfig
filterConfig
    }

tries
  :: forall m. (MonadCatch m, MonadDiagrams m, MonadGraphviz m)
  => DeadlockConfig
  -> Int
  -> m (Net Place Transition, GraphvizCommand, Either (NonEmpty [Transition]) (NonEmpty [Transition]))
tries :: forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
DeadlockConfig
-> Int
-> m (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
tries DeadlockConfig
conf Int
seed = RandT
  StdGen
  m
  (Net Place Transition, GraphvizCommand,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> m (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall {m :: * -> *} {a}. Monad m => RandT StdGen m a -> m a
eval RandT
  StdGen
  m
  (Net Place Transition, GraphvizCommand,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
out
  where
    eval :: RandT StdGen m a -> m a
eval RandT StdGen m a
f = RandT StdGen m a -> StdGen -> m a
forall (m :: * -> *) g a. Monad m => RandT g m a -> g -> m a
evalRandT RandT StdGen m a
f (StdGen -> m a) -> StdGen -> m a
forall a b. (a -> b) -> a -> b
$ Int -> StdGen
mkStdGen Int
seed
    out
      :: RandT StdGen m (Net Place Transition, GraphvizCommand, Either (NonEmpty [Transition]) (NonEmpty [Transition]))
    out :: RandT
  StdGen
  m
  (Net Place Transition, GraphvizCommand,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
out =
      RandT
  StdGen
  m
  (Net Place Transition, GraphvizCommand,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> ((Net Place Transition, GraphvizCommand,
     Either (NonEmpty [Transition]) (NonEmpty [Transition]))
    -> RandT
         StdGen
         m
         (Net Place Transition, GraphvizCommand,
          Either (NonEmpty [Transition]) (NonEmpty [Transition])))
-> Maybe
     (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> RandT
     StdGen
     m
     (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe RandT
  StdGen
  m
  (Net Place Transition, GraphvizCommand,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
out (Net Place Transition, GraphvizCommand,
 Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> RandT
     StdGen
     m
     (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall a. a -> RandT StdGen m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe
   (Net Place Transition, GraphvizCommand,
    Either (NonEmpty [Transition]) (NonEmpty [Transition]))
 -> RandT
      StdGen
      m
      (Net Place Transition, GraphvizCommand,
       Either (NonEmpty [Transition]) (NonEmpty [Transition])))
-> RandT
     StdGen
     m
     (Maybe
        (Net Place Transition, GraphvizCommand,
         Either (NonEmpty [Transition]) (NonEmpty [Transition])))
-> RandT
     StdGen
     m
     (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MaybeT
  (RandT StdGen m)
  (Net Place Transition, GraphvizCommand,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> RandT
     StdGen
     m
     (Maybe
        (Net Place Transition, GraphvizCommand,
         Either (NonEmpty [Transition]) (NonEmpty [Transition])))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (DeadlockConfig
-> MaybeT
     (RandT StdGen m)
     (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
DeadlockConfig
-> MaybeT
     (RandT StdGen m)
     (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
try DeadlockConfig
conf)

try
  :: (MonadCatch m, MonadDiagrams m, MonadGraphviz m)
  => DeadlockConfig
  -> MaybeT (RandT StdGen m) (Net Place Transition, GraphvizCommand, Either (NonEmpty [Transition]) (NonEmpty [Transition]))
try :: forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
DeadlockConfig
-> MaybeT
     (RandT StdGen m)
     (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
try DeadlockConfig
conf = do
    let ps :: [Place]
ps = [Int -> Place
Place Int
1 .. Int -> Place
Place (DeadlockConfig -> Int
numPlaces DeadlockConfig
conf)]
        ts :: [Transition]
ts = [Int -> Transition
Transition Int
1 .. Int -> Transition
Transition (DeadlockConfig -> Int
numTransitions DeadlockConfig
conf)]
        requiredFusableTransitionsConsuming :: Int
requiredFusableTransitionsConsuming = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ DeadlockConfig -> Maybe Int
fusableTransitionsConsumingAreExactly DeadlockConfig
conf
        requiredFusableTransitionsProducing :: Int
requiredFusableTransitionsProducing = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ DeadlockConfig -> Maybe Int
fusableTransitionsProducingAreExactly DeadlockConfig
conf
    -- Pre-generate fusable node connections and bind appropriate version of netLimitsFiltered
    ArrowDensityConstraints
-> Int
-> [Place]
-> [Transition]
-> Capacity Place
-> TransitionBehaviorConstraints
-> RandT StdGen m (Maybe (Net Place Transition))
netGenerator <-
      if Int
requiredFusableTransitionsConsuming Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 Bool -> Bool -> Bool
&& Int
requiredFusableTransitionsProducing Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
      then (ArrowDensityConstraints
 -> Int
 -> [Place]
 -> [Transition]
 -> Capacity Place
 -> TransitionBehaviorConstraints
 -> RandT StdGen m (Maybe (Net Place Transition)))
-> MaybeT
     (RandT StdGen m)
     (ArrowDensityConstraints
      -> Int
      -> [Place]
      -> [Transition]
      -> Capacity Place
      -> TransitionBehaviorConstraints
      -> RandT StdGen m (Maybe (Net Place Transition)))
forall a. a -> MaybeT (RandT StdGen m) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((ArrowDensityConstraints
  -> Int
  -> [Place]
  -> [Transition]
  -> Capacity Place
  -> TransitionBehaviorConstraints
  -> RandT StdGen m (Maybe (Net Place Transition)))
 -> MaybeT
      (RandT StdGen m)
      (ArrowDensityConstraints
       -> Int
       -> [Place]
       -> [Transition]
       -> Capacity Place
       -> TransitionBehaviorConstraints
       -> RandT StdGen m (Maybe (Net Place Transition))))
-> (ArrowDensityConstraints
    -> Int
    -> [Place]
    -> [Transition]
    -> Capacity Place
    -> TransitionBehaviorConstraints
    -> RandT StdGen m (Maybe (Net Place Transition)))
-> MaybeT
     (RandT StdGen m)
     (ArrowDensityConstraints
      -> Int
      -> [Place]
      -> [Transition]
      -> Capacity Place
      -> TransitionBehaviorConstraints
      -> RandT StdGen m (Maybe (Net Place Transition)))
forall a b. (a -> b) -> a -> b
$ (RandT StdGen m [Place]
 -> RandT StdGen m [Place]
 -> Transition
 -> RandT StdGen m (Connection Place Transition))
-> ArrowDensityConstraints
-> Int
-> [Place]
-> [Transition]
-> Capacity Place
-> TransitionBehaviorConstraints
-> RandT StdGen m (Maybe (Net Place Transition))
forall (m :: * -> *) s t.
(MonadRandom m, Ord s, Ord t) =>
(m [s] -> m [s] -> t -> m (Connection s t))
-> ArrowDensityConstraints
-> Int
-> [s]
-> [t]
-> Capacity s
-> TransitionBehaviorConstraints
-> m (Maybe (Net s t))
netLimitsFiltered RandT StdGen m [Place]
-> RandT StdGen m [Place]
-> Transition
-> RandT StdGen m (Connection Place Transition)
forall (m :: * -> *) s t.
Monad m =>
m [s] -> m [s] -> t -> m (Connection s t)
simpleConnectionGenerator
      else do
        (Bimap Transition Place
transitionConsumingBimap, Bimap Transition Place
transitionProducingBimap) <-
          [Place]
-> [Transition]
-> Int
-> Int
-> MaybeT
     (RandT StdGen m) (Bimap Transition Place, Bimap Transition Place)
forall (m :: * -> *) t s.
(MonadRandom m, Ord t, Ord s) =>
[s] -> [t] -> Int -> Int -> m (Bimap t s, Bimap t s)
generateFusableConnections [Place]
ps [Transition]
ts Int
requiredFusableTransitionsConsuming Int
requiredFusableTransitionsProducing
        (ArrowDensityConstraints
 -> Int
 -> [Place]
 -> [Transition]
 -> Capacity Place
 -> TransitionBehaviorConstraints
 -> RandT StdGen m (Maybe (Net Place Transition)))
-> MaybeT
     (RandT StdGen m)
     (ArrowDensityConstraints
      -> Int
      -> [Place]
      -> [Transition]
      -> Capacity Place
      -> TransitionBehaviorConstraints
      -> RandT StdGen m (Maybe (Net Place Transition)))
forall a. a -> MaybeT (RandT StdGen m) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((ArrowDensityConstraints
  -> Int
  -> [Place]
  -> [Transition]
  -> Capacity Place
  -> TransitionBehaviorConstraints
  -> RandT StdGen m (Maybe (Net Place Transition)))
 -> MaybeT
      (RandT StdGen m)
      (ArrowDensityConstraints
       -> Int
       -> [Place]
       -> [Transition]
       -> Capacity Place
       -> TransitionBehaviorConstraints
       -> RandT StdGen m (Maybe (Net Place Transition))))
-> (ArrowDensityConstraints
    -> Int
    -> [Place]
    -> [Transition]
    -> Capacity Place
    -> TransitionBehaviorConstraints
    -> RandT StdGen m (Maybe (Net Place Transition)))
-> MaybeT
     (RandT StdGen m)
     (ArrowDensityConstraints
      -> Int
      -> [Place]
      -> [Transition]
      -> Capacity Place
      -> TransitionBehaviorConstraints
      -> RandT StdGen m (Maybe (Net Place Transition)))
forall a b. (a -> b) -> a -> b
$ (RandT StdGen m [Place]
 -> RandT StdGen m [Place]
 -> Transition
 -> RandT StdGen m (Connection Place Transition))
-> ArrowDensityConstraints
-> Int
-> [Place]
-> [Transition]
-> Capacity Place
-> TransitionBehaviorConstraints
-> RandT StdGen m (Maybe (Net Place Transition))
forall (m :: * -> *) s t.
(MonadRandom m, Ord s, Ord t) =>
(m [s] -> m [s] -> t -> m (Connection s t))
-> ArrowDensityConstraints
-> Int
-> [s]
-> [t]
-> Capacity s
-> TransitionBehaviorConstraints
-> m (Maybe (Net s t))
netLimitsFiltered
          ((RandT StdGen m [Place]
  -> RandT StdGen m [Place]
  -> Transition
  -> RandT StdGen m (Connection Place Transition))
 -> ArrowDensityConstraints
 -> Int
 -> [Place]
 -> [Transition]
 -> Capacity Place
 -> TransitionBehaviorConstraints
 -> RandT StdGen m (Maybe (Net Place Transition)))
-> (RandT StdGen m [Place]
    -> RandT StdGen m [Place]
    -> Transition
    -> RandT StdGen m (Connection Place Transition))
-> ArrowDensityConstraints
-> Int
-> [Place]
-> [Transition]
-> Capacity Place
-> TransitionBehaviorConstraints
-> RandT StdGen m (Maybe (Net Place Transition))
forall a b. (a -> b) -> a -> b
$ \RandT StdGen m [Place]
inputPlacesAction RandT StdGen m [Place]
outputPlacesAction Transition
t -> do
              ([Place]
vor, [Place]
nach) <- Bimap Transition Place
-> Bimap Transition Place
-> RandT StdGen m [Place]
-> RandT StdGen m [Place]
-> Transition
-> RandT StdGen m ([Place], [Place])
forall (m :: * -> *) s t.
(MonadRandom m, Ord s, Ord t) =>
Bimap t s -> Bimap t s -> m [s] -> m [s] -> t -> m ([s], [s])
generateValidConnection Bimap Transition Place
transitionConsumingBimap Bimap Transition Place
transitionProducingBimap RandT StdGen m [Place]
inputPlacesAction RandT StdGen m [Place]
outputPlacesAction Transition
t
              case Transition -> Bimap Transition Place -> Maybe Place
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
a -> Bimap a b -> m b
BM.lookup Transition
t Bimap Transition Place
transitionConsumingBimap of
                Just Place
preVor
                  -> Connection Place Transition
-> RandT StdGen m (Connection Place Transition)
forall a. a -> RandT StdGen m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Place
preVor Place -> [Place] -> [Place]
forall a. a -> [a] -> [a]
: [Place]
vor, Transition
t, [Place]
nach)
                Maybe Place
_
                  -> case Transition -> Bimap Transition Place -> Maybe Place
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
a -> Bimap a b -> m b
BM.lookup Transition
t Bimap Transition Place
transitionProducingBimap of
                       Just Place
preNach
                         -> Connection Place Transition
-> RandT StdGen m (Connection Place Transition)
forall a. a -> RandT StdGen m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Place]
vor, Transition
t, Place
preNach Place -> [Place] -> [Place]
forall a. a -> [a] -> [a]
: [Place]
nach)
                       Maybe Place
_
                         -> Connection Place Transition
-> RandT StdGen m (Connection Place Transition)
forall a. a -> RandT StdGen m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Place]
vor, Transition
t, [Place]
nach)
                -- impossible for both lookups to return Just
    Net Place Transition
n <- RandT StdGen m (Maybe (Net Place Transition))
-> MaybeT (RandT StdGen m) (Net Place Transition)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (RandT StdGen m (Maybe (Net Place Transition))
 -> MaybeT (RandT StdGen m) (Net Place Transition))
-> RandT StdGen m (Maybe (Net Place Transition))
-> MaybeT (RandT StdGen m) (Net Place Transition)
forall a b. (a -> b) -> a -> b
$ ArrowDensityConstraints
-> Int
-> [Place]
-> [Transition]
-> Capacity Place
-> TransitionBehaviorConstraints
-> RandT StdGen m (Maybe (Net Place Transition))
netGenerator
      (DeadlockConfig -> ArrowDensityConstraints
arrowDensityConstraints DeadlockConfig
conf)
      (DeadlockConfig -> Int
numPlaces DeadlockConfig
conf)
      [Place]
ps
      [Transition]
ts
      (DeadlockConfig -> Capacity Place
Modelling.PetriNet.Reach.Deadlock.capacity DeadlockConfig
conf)
      (DeadlockConfig -> TransitionBehaviorConstraints
transitionBehaviorConstraints DeadlockConfig
conf)
    -- Check fusable transitions constraints
    Maybe Int
-> (Int -> MaybeT (RandT StdGen m) ())
-> MaybeT (RandT StdGen m) ()
forall (m :: * -> *) a.
Applicative m =>
Maybe a -> (a -> m ()) -> m ()
whenJust (DeadlockConfig -> Maybe Int
fusableTransitionsConsumingAreExactly DeadlockConfig
conf) ((Int -> MaybeT (RandT StdGen m) ()) -> MaybeT (RandT StdGen m) ())
-> (Int -> MaybeT (RandT StdGen m) ())
-> MaybeT (RandT StdGen m) ()
forall a b. (a -> b) -> a -> b
$ \Int
expected ->
      Bool -> MaybeT (RandT StdGen m) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT (RandT StdGen m) ())
-> Bool -> MaybeT (RandT StdGen m) ()
forall a b. (a -> b) -> a -> b
$ [Connection Place Transition] -> Int
forall s t. Ord s => [([s], t, [s])] -> Int
countFusableTransitionsConsuming (Net Place Transition -> [Connection Place Transition]
forall s t. Net s t -> [Connection s t]
connections Net Place Transition
n) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
expected
    Maybe Int
-> (Int -> MaybeT (RandT StdGen m) ())
-> MaybeT (RandT StdGen m) ()
forall (m :: * -> *) a.
Applicative m =>
Maybe a -> (a -> m ()) -> m ()
whenJust (DeadlockConfig -> Maybe Int
fusableTransitionsProducingAreExactly DeadlockConfig
conf) ((Int -> MaybeT (RandT StdGen m) ()) -> MaybeT (RandT StdGen m) ())
-> (Int -> MaybeT (RandT StdGen m) ())
-> MaybeT (RandT StdGen m) ()
forall a b. (a -> b) -> a -> b
$ \Int
expected ->
      Bool -> MaybeT (RandT StdGen m) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT (RandT StdGen m) ())
-> Bool -> MaybeT (RandT StdGen m) ()
forall a b. (a -> b) -> a -> b
$ [Connection Place Transition] -> Int
forall s t. Ord s => [([s], t, [s])] -> Int
countFusableTransitionsProducing (Net Place Transition -> [Connection Place Transition]
forall s t. Net s t -> [Connection s t]
connections Net Place Transition
n) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
expected
    let deadlockLevels :: [[(State Place, [[Transition]])]]
deadlockLevels = ([(State Place, [[Transition]])]
 -> [(State Place, [[Transition]])])
-> [[(State Place, [[Transition]])]]
-> [[(State Place, [[Transition]])]]
forall a b. (a -> b) -> [a] -> [b]
map (((State Place, [[Transition]]) -> Bool)
-> [(State Place, [[Transition]])]
-> [(State Place, [[Transition]])]
forall a. (a -> Bool) -> [a] -> [a]
filter ([(Transition, State Place)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Transition, State Place)] -> Bool)
-> ((State Place, [[Transition]]) -> [(Transition, State Place)])
-> (State Place, [[Transition]])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Net Place Transition -> State Place -> [(Transition, State Place)]
forall s t. Ord s => Net s t -> State s -> [(t, State s)]
successors Net Place Transition
n (State Place -> [(Transition, State Place)])
-> ((State Place, [[Transition]]) -> State Place)
-> (State Place, [[Transition]])
-> [(Transition, State Place)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State Place, [[Transition]]) -> State Place
forall a b. (a, b) -> a
fst)) (Net Place Transition -> [[(State Place, [[Transition]])]]
forall s t. Ord s => Net s t -> [[(State s, [[t]])]]
levelsWithAlternatives Net Place Transition
n)
        ([[(State Place, [[Transition]])]]
no, [[(State Place, [[Transition]])]]
yeah) = ([(State Place, [[Transition]])] -> Bool)
-> [[(State Place, [[Transition]])]]
-> ([[(State Place, [[Transition]])]],
    [[(State Place, [[Transition]])]])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span [(State Place, [[Transition]])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null
          ([[(State Place, [[Transition]])]]
 -> ([[(State Place, [[Transition]])]],
     [[(State Place, [[Transition]])]]))
-> [[(State Place, [[Transition]])]]
-> ([[(State Place, [[Transition]])]],
    [[(State Place, [[Transition]])]])
forall a b. (a -> b) -> a -> b
$ Int
-> [[(State Place, [[Transition]])]]
-> [[(State Place, [[Transition]])]]
forall a. Int -> [a] -> [a]
take (DeadlockConfig -> Int
maxTransitionLength DeadlockConfig
conf Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
          [[(State Place, [[Transition]])]]
deadlockLevels
    Bool -> MaybeT (RandT StdGen m) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT (RandT StdGen m) ())
-> Bool -> MaybeT (RandT StdGen m) ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [[(State Place, [[Transition]])]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[(State Place, [[Transition]])]]
yeah
    let allShortestSolutions :: [[Transition]]
allShortestSolutions = ([Transition] -> [Transition]) -> [[Transition]] -> [[Transition]]
forall a b. (a -> b) -> [a] -> [b]
map [Transition] -> [Transition]
forall a. [a] -> [a]
reverse ([[Transition]] -> [[Transition]])
-> ([(State Place, [[Transition]])] -> [[Transition]])
-> [(State Place, [[Transition]])]
-> [[Transition]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((State Place, [[Transition]]) -> [[Transition]])
-> [(State Place, [[Transition]])] -> [[Transition]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (State Place, [[Transition]]) -> [[Transition]]
forall a b. (a, b) -> b
snd ([(State Place, [[Transition]])] -> [[Transition]])
-> [(State Place, [[Transition]])] -> [[Transition]]
forall a b. (a -> b) -> a -> b
$ [[(State Place, [[Transition]])]]
-> [(State Place, [[Transition]])]
forall a. HasCallStack => [a] -> a
head [[(State Place, [[Transition]])]]
yeah
    Bool -> MaybeT (RandT StdGen m) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT (RandT StdGen m) ())
-> Bool -> MaybeT (RandT StdGen m) ()
forall a b. (a -> b) -> a -> b
$ [[(State Place, [[Transition]])]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[(State Place, [[Transition]])]]
no Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= DeadlockConfig -> Int
minTransitionLength DeadlockConfig
conf
    (GraphvizCommand
cmd, Either (NonEmpty [Transition]) (NonEmpty [Transition])
solutionsList) <- Net Place Transition
-> [GraphvizCommand]
-> [[Transition]]
-> FilterConfig
-> Int
-> Int
-> MaybeT
     (RandT StdGen m)
     (GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall t (m :: * -> *) p.
(Enum t, MonadCatch m, MonadDiagrams m, MonadGraphviz m, Ord p,
 Ord t, Show p, Show t) =>
Net p t
-> [GraphvizCommand]
-> [[t]]
-> FilterConfig
-> Int
-> Int
-> MaybeT
     (RandT StdGen m)
     (GraphvizCommand, Either (NonEmpty [t]) (NonEmpty [t]))
validateDrawabilityAndSolutionFiltering
      Net Place Transition
n (DeadlockConfig -> [GraphvizCommand]
graphLayouts DeadlockConfig
conf) [[Transition]]
allShortestSolutions
      (DeadlockConfig -> FilterConfig
filterConfig DeadlockConfig
conf) (DeadlockConfig -> Int
numTransitions DeadlockConfig
conf) (DeadlockConfig -> Int
maxPrintedSolutions DeadlockConfig
conf)
    pure (Net Place Transition
n, GraphvizCommand
cmd, Either (NonEmpty [Transition]) (NonEmpty [Transition])
solutionsList)

exampleInstance :: Net Int Int
exampleInstance :: Net Int Int
exampleInstance =
  Net {
  places :: Set Int
places = [Int] -> Set Int
forall a. Ord a => [a] -> Set a
S.fromList [Int
1, Int
2, Int
3, Int
4, Int
5],
  transitions :: Set Int
transitions = [Int] -> Set Int
forall a. Ord a => [a] -> Set a
S.fromList [Int
1, Int
2, Int
3, Int
4, Int
5],
  connections :: [Connection Int Int]
connections = [
      ([Int
1], Int
1, [Int
1, Int
2, Int
3]),
      ([Int
2], Int
2, [Int
3, Int
4]),
      ([Int
3], Int
3, [Int
4, Int
5]),
      ([Int
4], Int
4, [Int
5, Int
1]),
      ([Int
5], Int
5, [Int
1, Int
2]),
      ([Int
1, Int
2, Int
3, Int
4, Int
5], Int
7, [])
      ],
    capacity :: Capacity Int
Modelling.PetriNet.Reach.Type.capacity = Capacity Int
forall s. Capacity s
Unbounded,
    start :: State Int
start = Map Int Int -> State Int
forall s. Map s Int -> State s
State (Map Int Int -> State Int) -> Map Int Int -> State Int
forall a b. (a -> b) -> a -> b
$ [(Int, Int)] -> Map Int Int
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Int
1, Int
1), (Int
2, Int
0), (Int
3, Int
0), (Int
4, Int
0), (Int
5, Int
0)]
  }