{-# 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 (fromList, lookup, memberR)
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,
  checkBaseInstance,
  checkSolutionLength,
  )
import Modelling.PetriNet.Reach.Reach   (
  assertReachPoints,
  isNoLonger,
  levelsWithAlternatives,
  rejectSpaceballsPattern,
  reportReachFor,
  transitionsValid,
  provideSolutionsFeedback,
  validateDrawabilityAndSolutionFiltering,
  )
import Modelling.PetriNet.Reach.Roll    (netLimitsFiltered, simpleConnectionGenerator)
import Modelling.PetriNet.Reach.Step    (executes, executeSequence, 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,
  placesFromOneTo,
  transitionFromNumber,
  transitionsFromOneTo,
  )

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

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

verifyDeadlock
  :: (Ord a, OutputCapable m, Show a)
  => DeadlockInstance a Transition
  -> LangM m
verifyDeadlock :: forall a (m :: * -> *).
(Ord a, OutputCapable m, Show a) =>
DeadlockInstance a Transition -> LangM m
verifyDeadlock inst :: DeadlockInstance a Transition
inst@DeadlockInstance{Bool
Int
Maybe Int
Either (NonEmpty [Transition]) (NonEmpty [Transition])
GraphvizCommand
ExtraText
Net a Transition
drawUsing :: GraphvizCommand
minLength :: Int
noLongerThan :: Maybe Int
petriNet :: Net a Transition
showPlaceNames :: Bool
maxDisplayedSolutions :: Int
shortestSolutions :: Either (NonEmpty [Transition]) (NonEmpty [Transition])
withLengthHint :: Maybe Int
withMinLengthHint :: Bool
addText :: ExtraText
rejectSpaceballsLength :: Maybe Int
rejectSpaceballsLength :: forall s t. DeadlockInstance s t -> Maybe Int
addText :: forall s t. DeadlockInstance s t -> ExtraText
withMinLengthHint :: forall s t. DeadlockInstance s t -> Bool
withLengthHint :: forall s t. DeadlockInstance s t -> Maybe Int
shortestSolutions :: forall s t.
DeadlockInstance s t -> Either (NonEmpty [t]) (NonEmpty [t])
maxDisplayedSolutions :: forall s t. DeadlockInstance s t -> Int
showPlaceNames :: forall s t. DeadlockInstance s t -> Bool
petriNet :: forall s t. DeadlockInstance s t -> Net s t
noLongerThan :: forall s t. DeadlockInstance s t -> Maybe Int
minLength :: forall s t. DeadlockInstance s t -> Int
drawUsing :: forall s t. DeadlockInstance s t -> GraphvizCommand
..} =
  Property -> Net a Transition -> 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 Transition
petriNet
  LangM m -> LangM m -> LangM m
forall a b.
GenericLangM Language m a
-> GenericLangM Language m b -> GenericLangM Language m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Int -> Maybe Int -> Maybe Int -> Maybe Int -> LangM m
forall (m :: * -> *).
OutputCapable m =>
Int -> Maybe Int -> Maybe Int -> Maybe Int -> LangM m
checkBaseInstance Int
minLength Maybe Int
noLongerThan Maybe Int
withLengthHint Maybe Int
rejectSpaceballsLength
  LangM m -> LangM m -> LangM m
forall a b.
GenericLangM Language m a
-> GenericLangM Language m b -> GenericLangM Language m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ([Transition] -> LangM m) -> NonEmpty [Transition] -> LangM m
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ [Transition] -> LangM m
forall {m :: * -> *}.
OutputCapable m =>
[Transition] -> GenericLangM Language m ()
checkSolution (Either (NonEmpty [Transition]) (NonEmpty [Transition])
-> NonEmpty [Transition]
forall a. Either a a -> a
fromEither Either (NonEmpty [Transition]) (NonEmpty [Transition])
shortestSolutions)
  where
    checkSolution :: [Transition] -> GenericLangM Language m ()
checkSolution [Transition]
ts =
      Bool
-> DeadlockInstance a Transition
-> [Transition]
-> GenericLangM Language m ()
forall (m :: * -> *) a.
OutputCapable m =>
Bool -> DeadlockInstance a Transition -> [Transition] -> LangM m
deadlockSyntax Bool
True DeadlockInstance a Transition
inst [Transition]
ts
      GenericLangM Language m ()
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b.
GenericLangM Language m a
-> GenericLangM Language m b -> GenericLangM Language m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Int -> Maybe Int -> [Transition] -> GenericLangM Language m ()
forall (m :: * -> *) t.
OutputCapable m =>
Int -> Maybe Int -> [t] -> LangM m
checkSolutionLength Int
minLength Maybe Int
withLengthHint [Transition]
ts
      GenericLangM Language m ()
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b.
GenericLangM Language m a
-> GenericLangM Language m b -> GenericLangM Language m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
Bool -> GenericLangM l m () -> GenericLangM l m ()
assertion ([Transition] -> Bool
isDeadlockReached [Transition]
ts) (State (Map Language String) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> GenericLangM Language m ())
-> State (Map Language String) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
           String -> State (Map Language String) ()
english String
"Solution sequence leads to a deadlock state?"
           String -> State (Map Language String) ()
german String
"Lösungssequenz führt zu einem Deadlock-Zustand?")
    isDeadlockReached :: [Transition] -> Bool
isDeadlockReached = Bool -> (State a -> Bool) -> Maybe (State a) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ([(Transition, State a)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Transition, State a)] -> Bool)
-> (State a -> [(Transition, State a)]) -> State a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Net a Transition -> State a -> [(Transition, State a)]
forall s t. Ord s => Net s t -> State s -> [(t, State s)]
successors Net a Transition
petriNet) (Maybe (State a) -> Bool)
-> ([Transition] -> Maybe (State a)) -> [Transition] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Net a Transition -> [Transition] -> Maybe (State a)
forall t s. (Eq t, Ord s) => Net s t -> [t] -> Maybe (State s)
executeSequence Net a Transition
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 -> String -> DeadlockInstance s t -> LangM m
deadlockTask Bool
showInputHelp String
path DeadlockInstance s t
inst = do
  m String -> GenericLangM Language m String
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 -> Bool -> String -> GraphvizCommand -> Net s t -> m String
forall s t (m :: * -> *).
(Ord s, Ord t, Show s, Show t, MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m) =>
Bool -> Bool -> String -> GraphvizCommand -> Net s t -> m String
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) Bool
False String
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 String
-> (String -> 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
$>>= \String
img ->
    Bool
-> String
-> Maybe Int
-> Maybe Int
-> Int
-> Bool
-> Maybe (Either String String)
-> ExtraText
-> GenericLangM Language m ()
forall (m :: * -> *).
OutputCapable m =>
Bool
-> String
-> Maybe Int
-> Maybe Int
-> Int
-> Bool
-> Maybe (Either String String)
-> ExtraText
-> LangM m
reportReachFor
    Bool
showInputHelp
    String
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 String String)
forall a. Maybe a
Nothing
    (DeadlockInstance s t -> ExtraText
forall s t. DeadlockInstance s t -> ExtraText
addText DeadlockInstance s t
inst)

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
  => Bool
  -- ^ Whether to do a full check. If False, only check for Spaceballs pattern.
  -> DeadlockInstance a Transition
  -> [Transition]
  -> LangM m
deadlockSyntax :: forall (m :: * -> *) a.
OutputCapable m =>
Bool -> DeadlockInstance a Transition -> [Transition] -> LangM m
deadlockSyntax Bool
fullCheck DeadlockInstance a Transition
inst [Transition]
ts =
 Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
fullCheck (
  do Net a Transition -> [Transition] -> GenericLangM Language m ()
forall (m :: * -> *) s.
OutputCapable m =>
Net s Transition -> [Transition] -> LangM m
transitionsValid (DeadlockInstance a Transition -> Net a Transition
forall s t. DeadlockInstance s t -> Net s t
petriNet DeadlockInstance a Transition
inst) [Transition]
ts
     Maybe Int -> [Transition] -> GenericLangM Language m ()
forall (m :: * -> *) a.
OutputCapable m =>
Maybe Int -> [a] -> LangM m
isNoLonger (DeadlockInstance a Transition -> Maybe Int
forall s t. DeadlockInstance s t -> Maybe Int
noLongerThan DeadlockInstance a Transition
inst) [Transition]
ts
     pure ()
 )
 GenericLangM Language m ()
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b.
GenericLangM Language m a
-> GenericLangM Language m b -> GenericLangM Language m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Maybe Int -> [Transition] -> GenericLangM Language m ()
forall t (m :: * -> *).
(Eq t, OutputCapable m, Sequential t, Show t) =>
Maybe Int -> [t] -> LangM m
rejectSpaceballsPattern (DeadlockInstance a Transition -> Maybe Int
forall s t. DeadlockInstance s t -> Maybe Int
rejectSpaceballsLength DeadlockInstance a Transition
inst) [Transition]
ts

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) =>
String
-> DeadlockInstance Place Transition -> [Transition] -> Rated m
deadlockEvaluation String
path DeadlockInstance Place Transition
deadlock [Transition]
ts =
  String
-> 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) =>
String
-> GraphvizCommand
-> Net s t
-> [t]
-> LangM' m (Either Int (State s))
executes String
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 String) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> GenericLangM Language m ())
-> State (Map Language String) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
          String -> State (Map Language String) ()
english String
"All transitions disabled in reached marking?"
          String -> State (Map Language String) ()
german String
"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 String
-> (DeadlockInstance ShowPlace ShowTransition
    -> State ShowPlace -> Bool)
-> (DeadlockInstance ShowPlace ShowTransition -> Int)
-> DeadlockInstance ShowPlace ShowTransition
-> Int
-> Either Int (State ShowPlace)
-> GenericLangM Language m Rational
forall (m :: * -> *) i a.
OutputCapable m =>
Maybe String
-> (i -> a -> Bool)
-> (i -> Int)
-> i
-> Int
-> Either Int a
-> Rated m
assertReachPoints
    Maybe String
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] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [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 String
aSolution = Int
-> Either (NonEmpty [Transition]) (NonEmpty [Transition])
-> Maybe String
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,
  forall s t. DeadlockInstance s t -> ExtraText
addText           :: ExtraText,
  -- | 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 -> String
(Int -> DeadlockInstance s t -> ShowS)
-> (DeadlockInstance s t -> String)
-> ([DeadlockInstance s t] -> ShowS)
-> Show (DeadlockInstance s t)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([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 -> String
$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 -> String
show :: DeadlockInstance s t -> String
$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
ExtraText
Net s t
rejectSpaceballsLength :: forall s t. DeadlockInstance s t -> Maybe Int
addText :: forall s t. DeadlockInstance s t -> ExtraText
withMinLengthHint :: forall s t. DeadlockInstance s t -> Bool
withLengthHint :: forall s t. DeadlockInstance s t -> Maybe Int
shortestSolutions :: forall s t.
DeadlockInstance s t -> Either (NonEmpty [t]) (NonEmpty [t])
maxDisplayedSolutions :: forall s t. DeadlockInstance s t -> Int
showPlaceNames :: forall s t. DeadlockInstance s t -> Bool
petriNet :: forall s t. DeadlockInstance s t -> Net s t
noLongerThan :: forall s t. DeadlockInstance s t -> Maybe Int
minLength :: forall s t. DeadlockInstance s t -> Int
drawUsing :: forall s t. DeadlockInstance s t -> GraphvizCommand
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
addText :: ExtraText
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,
    addText :: ExtraText
addText           = ExtraText
addText,
    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,
  DeadlockConfig -> ExtraText
extraText           :: ExtraText,
  -- | 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 -> String
(Int -> DeadlockConfig -> ShowS)
-> (DeadlockConfig -> String)
-> ([DeadlockConfig] -> ShowS)
-> Show DeadlockConfig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DeadlockConfig -> ShowS
showsPrec :: Int -> DeadlockConfig -> ShowS
$cshow :: DeadlockConfig -> String
show :: DeadlockConfig -> String
$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
1,
  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,
  extraText :: ExtraText
extraText           = ExtraText
NoExtraText,
  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
1,
  shortestSolutions :: Either (NonEmpty [Transition]) (NonEmpty [Transition])
shortestSolutions = NonEmpty [Transition]
-> Either (NonEmpty [Transition]) (NonEmpty [Transition])
forall a b. a -> Either a b
Left ([
    Int -> Transition
transitionFromNumber Int
3, Int -> Transition
transitionFromNumber Int
3, Int -> Transition
transitionFromNumber Int
3,
    Int -> Transition
transitionFromNumber Int
2, Int -> Transition
transitionFromNumber Int
2, Int -> Transition
transitionFromNumber Int
2
    ] [Transition] -> [[Transition]] -> NonEmpty [Transition]
forall a. a -> [a] -> NonEmpty a
:| []),
  withLengthHint :: Maybe Int
withLengthHint    = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
9,
  withMinLengthHint :: Bool
withMinLengthHint = Bool
True,
  addText :: ExtraText
addText           = ExtraText
NoExtraText,
  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 String
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
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"fusable transitions requirements must not be negative and together cannot exceed numTransitions or numPlaces"
  | Bool
otherwise
  = Maybe Int -> (Int, Maybe Int) -> String -> String -> Maybe String
forall {a} {a} {a}.
(Ord a, Ord a, Num a, Num a, Num a, Eq a) =>
Maybe a -> (a, Maybe a) -> String -> String -> Maybe String
checkConflicts Maybe Int
maybeConsuming (Int, Maybe Int)
incomingArrowsPerTransition String
"Consuming" String
"incomingArrowsPerTransition"
    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, Maybe Int) -> String -> String -> Maybe String
forall {a} {a} {a}.
(Ord a, Ord a, Num a, Num a, Num a, Eq a) =>
Maybe a -> (a, Maybe a) -> String -> String -> Maybe String
checkConflicts Maybe Int
maybeProducing (Int, Maybe Int)
outgoingArrowsPerTransition String
"Producing" String
"outgoingArrowsPerTransition"
    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, Maybe Int) -> String -> String -> Maybe String
forall {a} {a} {a}.
(Ord a, Ord a, Num a, Num a, Num a, Eq a) =>
Maybe a -> (a, Maybe a) -> String -> String -> Maybe String
checkConflicts Maybe Int
maybeConsuming (Int, Maybe Int)
outgoingArrowsPerPlace String
"Consuming" String
"outgoingArrowsPerPlace"
    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, Maybe Int) -> String -> String -> Maybe String
forall {a} {a} {a}.
(Ord a, Ord a, Num a, Num a, Num a, Eq a) =>
Maybe a -> (a, Maybe a) -> String -> String -> Maybe String
checkConflicts Maybe Int
maybeProducing (Int, Maybe Int)
incomingArrowsPerPlace String
"Producing" String
"incomingArrowsPerPlace"
    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 -> String -> String -> Maybe String
forall {a}.
Ord a =>
Maybe a -> a -> String -> String -> Maybe String
checkTotalLower Maybe Int
maybeConsuming ((Int, Maybe Int) -> Int
forall a b. (a, b) -> a
fst (Int, Maybe Int)
totalArrowsFromPlacesToTransitions) String
"Consuming" String
"totalArrowsFromPlacesToTransitions"
    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 -> String -> String -> Maybe String
forall {a}.
Ord a =>
Maybe a -> a -> String -> String -> Maybe String
checkTotalLower Maybe Int
maybeProducing ((Int, Maybe Int) -> Int
forall a b. (a, b) -> a
fst (Int, Maybe Int)
totalArrowsFromTransitionsToPlaces) String
"Producing" String
"totalArrowsFromTransitionsToPlaces"
  where
    checkConflicts :: Maybe a -> (a, Maybe a) -> String -> String -> Maybe String
checkConflicts Maybe a
maybeCount (a
minVal, Maybe a
maxVal) String
nodeType String
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
      = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"fusableTransitions" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nodeType String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"AreExactly > 0 conflicts with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
constraintName String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" 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
      = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"fusableTransitions" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nodeType String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"AreExactly > 0 conflicts with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
constraintName String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" maximum = 0"
      | Bool
otherwise = Maybe String
forall a. Maybe a
Nothing
    checkTotalLower :: Maybe a -> a -> String -> String -> Maybe String
checkTotalLower Maybe a
maybeCount a
totalMin String
nodeType String
constraintName
      | Just a
count <- Maybe a
maybeCount, a
totalMin a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
count
      = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"having fewer " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
constraintName String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" than fusableTransitions" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nodeType String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"AreExactly makes no sense"
      | Bool
otherwise = Maybe String
forall a. Maybe a
Nothing

checkDeadlockConfig :: DeadlockConfig -> Maybe String
checkDeadlockConfig :: DeadlockConfig -> Maybe String
checkDeadlockConfig DeadlockConfig {Bool
Int
[GraphvizCommand]
Maybe Int
ExtraText
ArrowDensityConstraints
TransitionBehaviorConstraints
Capacity Place
FilterConfig
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
extraText :: DeadlockConfig -> ExtraText
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
extraText :: ExtraText
fusableTransitionsConsumingAreExactly :: Maybe Int
fusableTransitionsProducingAreExactly :: Maybe Int
filterConfig :: FilterConfig
..} =
  Int
-> Int
-> Capacity Place
-> Int
-> Int
-> TransitionBehaviorConstraints
-> ArrowDensityConstraints
-> [GraphvizCommand]
-> Maybe Int
-> Bool
-> Maybe String
forall s.
Int
-> Int
-> Capacity s
-> Int
-> Int
-> TransitionBehaviorConstraints
-> ArrowDensityConstraints
-> [GraphvizCommand]
-> Maybe Int
-> Bool
-> Maybe String
checkBasicPetriConfig
    Int
numPlaces
    Int
numTransitions
    Capacity Place
capacity
    Int
minTransitionLength
    Int
maxTransitionLength
    TransitionBehaviorConstraints
transitionBehaviorConstraints
    ArrowDensityConstraints
arrowDensityConstraints
    [GraphvizCommand]
graphLayouts
    Maybe Int
rejectLongerThan
    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
<|>
  Maybe Int -> Int -> Int -> FilterConfig -> Maybe String
checkFilterConfigWith
    Maybe Int
rejectLongerThan
    Int
minTransitionLength
    Int
numTransitions
    FilterConfig
filterConfig
  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
-> Maybe Int
-> Int
-> Int
-> ArrowDensityConstraints
-> Maybe String
checkFusableNodeConfig
    Maybe Int
fusableTransitionsConsumingAreExactly
    Maybe Int
fusableTransitionsProducingAreExactly
    Int
numTransitions
    Int
numPlaces
    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
<|>
  if Int
maxPrintedSolutions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
    then String -> Maybe String
forall a. a -> Maybe a
Just String
"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 ->
        String -> Maybe String
forall a. a -> Maybe a
Just String
"maxPrintedSolutions cannot be greater than solutionSetLimit"
      Maybe Int
_ -> Maybe String
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
ExtraText
ArrowDensityConstraints
TransitionBehaviorConstraints
Capacity Place
FilterConfig
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
extraText :: DeadlockConfig -> ExtraText
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
extraText :: ExtraText
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,
    addText :: ExtraText
addText           = ExtraText
extraText,
    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]))
forall g.
RandomGen g =>
RandT
  g
  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
      :: RandomGen g => RandT g m (Net Place Transition, GraphvizCommand, Either (NonEmpty [Transition]) (NonEmpty [Transition]))
    out :: forall g.
RandomGen g =>
RandT
  g
  m
  (Net Place Transition, GraphvizCommand,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
out =
      RandT
  g
  m
  (Net Place Transition, GraphvizCommand,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> ((Net Place Transition, GraphvizCommand,
     Either (NonEmpty [Transition]) (NonEmpty [Transition]))
    -> RandT
         g
         m
         (Net Place Transition, GraphvizCommand,
          Either (NonEmpty [Transition]) (NonEmpty [Transition])))
-> Maybe
     (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> RandT
     g
     m
     (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe RandT
  g
  m
  (Net Place Transition, GraphvizCommand,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall g.
RandomGen g =>
RandT
  g
  m
  (Net Place Transition, GraphvizCommand,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
out (Net Place Transition, GraphvizCommand,
 Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> RandT
     g
     m
     (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall a. a -> RandT g m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe
   (Net Place Transition, GraphvizCommand,
    Either (NonEmpty [Transition]) (NonEmpty [Transition]))
 -> RandT
      g
      m
      (Net Place Transition, GraphvizCommand,
       Either (NonEmpty [Transition]) (NonEmpty [Transition])))
-> RandT
     g
     m
     (Maybe
        (Net Place Transition, GraphvizCommand,
         Either (NonEmpty [Transition]) (NonEmpty [Transition])))
-> RandT
     g
     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 g m)
  (Net Place Transition, GraphvizCommand,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> RandT
     g
     m
     (Maybe
        (Net Place Transition, GraphvizCommand,
         Either (NonEmpty [Transition]) (NonEmpty [Transition])))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (DeadlockConfig
-> MaybeT
     (RandT g m)
     (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall (m :: * -> *) g.
(MonadCatch m, MonadDiagrams m, MonadGraphviz m, RandomGen g) =>
DeadlockConfig
-> MaybeT
     (RandT g m)
     (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
try DeadlockConfig
conf)

try
  :: (MonadCatch m, MonadDiagrams m, MonadGraphviz m, RandomGen g)
  => DeadlockConfig
  -> MaybeT (RandT g m) (Net Place Transition, GraphvizCommand, Either (NonEmpty [Transition]) (NonEmpty [Transition]))
try :: forall (m :: * -> *) g.
(MonadCatch m, MonadDiagrams m, MonadGraphviz m, RandomGen g) =>
DeadlockConfig
-> MaybeT
     (RandT g m)
     (Net Place Transition, GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
try DeadlockConfig
conf = do
    let ps :: [Place]
ps = Int -> [Place]
placesFromOneTo (DeadlockConfig -> Int
numPlaces DeadlockConfig
conf)
        ts :: [Transition]
ts = Int -> [Transition]
transitionsFromOneTo (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 g 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 g m (Maybe (Net Place Transition)))
-> MaybeT
     (RandT g m)
     (ArrowDensityConstraints
      -> Int
      -> [Place]
      -> [Transition]
      -> Capacity Place
      -> TransitionBehaviorConstraints
      -> RandT g m (Maybe (Net Place Transition)))
forall a. a -> MaybeT (RandT g m) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((ArrowDensityConstraints
  -> Int
  -> [Place]
  -> [Transition]
  -> Capacity Place
  -> TransitionBehaviorConstraints
  -> RandT g m (Maybe (Net Place Transition)))
 -> MaybeT
      (RandT g m)
      (ArrowDensityConstraints
       -> Int
       -> [Place]
       -> [Transition]
       -> Capacity Place
       -> TransitionBehaviorConstraints
       -> RandT g m (Maybe (Net Place Transition))))
-> (ArrowDensityConstraints
    -> Int
    -> [Place]
    -> [Transition]
    -> Capacity Place
    -> TransitionBehaviorConstraints
    -> RandT g m (Maybe (Net Place Transition)))
-> MaybeT
     (RandT g m)
     (ArrowDensityConstraints
      -> Int
      -> [Place]
      -> [Transition]
      -> Capacity Place
      -> TransitionBehaviorConstraints
      -> RandT g m (Maybe (Net Place Transition)))
forall a b. (a -> b) -> a -> b
$ (RandT g m [Place]
 -> RandT g m [Place]
 -> Transition
 -> RandT g m (Connection Place Transition))
-> ArrowDensityConstraints
-> Int
-> [Place]
-> [Transition]
-> Capacity Place
-> TransitionBehaviorConstraints
-> RandT g 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 g m [Place]
-> RandT g m [Place]
-> Transition
-> RandT g m (Connection Place Transition)
forall (m :: * -> *) s t.
Monad m =>
m [s] -> m [s] -> t -> m (Connection s t)
simpleConnectionGenerator
      else do
        -- Generate pre-determined fusable node connections:
        -- First, randomly select transitions and places for fusable nodes
        [Transition]
shuffledTransitions <- [Transition] -> MaybeT (RandT g m) [Transition]
forall (m :: * -> *) a. MonadRandom m => [a] -> m [a]
shuffleM [Transition]
ts
        [Place]
shuffledPlaces <- [Place] -> MaybeT (RandT g m) [Place]
forall (m :: * -> *) a. MonadRandom m => [a] -> m [a]
shuffleM [Place]
ps
        let ([Transition]
inputFusableTransitions, [Transition]
remainingTransitions) = Int -> [Transition] -> ([Transition], [Transition])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
requiredFusableTransitionsConsuming [Transition]
shuffledTransitions
            outputFusableTransitions :: [Transition]
outputFusableTransitions = Int -> [Transition] -> [Transition]
forall a. Int -> [a] -> [a]
take Int
requiredFusableTransitionsProducing [Transition]
remainingTransitions
            ([Place]
placesForInputFusableTransitions, [Place]
remainingPlaces) = Int -> [Place] -> ([Place], [Place])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
requiredFusableTransitionsConsuming [Place]
shuffledPlaces
            placesForOutputFusableTransitions :: [Place]
placesForOutputFusableTransitions = Int -> [Place] -> [Place]
forall a. Int -> [a] -> [a]
take Int
requiredFusableTransitionsProducing [Place]
remainingPlaces
        -- Next, create bimaps from fusable transitions to their fusion-relevant places
        let transitionConsumingBimap :: Bimap Transition Place
transitionConsumingBimap = [(Transition, Place)] -> Bimap Transition Place
forall a b. (Ord a, Ord b) => [(a, b)] -> Bimap a b
BM.fromList ([(Transition, Place)] -> Bimap Transition Place)
-> [(Transition, Place)] -> Bimap Transition Place
forall a b. (a -> b) -> a -> b
$ [Transition] -> [Place] -> [(Transition, Place)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Transition]
inputFusableTransitions [Place]
placesForInputFusableTransitions
            transitionProducingBimap :: Bimap Transition Place
transitionProducingBimap = [(Transition, Place)] -> Bimap Transition Place
forall a b. (Ord a, Ord b) => [(a, b)] -> Bimap a b
BM.fromList ([(Transition, Place)] -> Bimap Transition Place)
-> [(Transition, Place)] -> Bimap Transition Place
forall a b. (a -> b) -> a -> b
$ [Transition] -> [Place] -> [(Transition, Place)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Transition]
outputFusableTransitions [Place]
placesForOutputFusableTransitions
        -- Helpers for generating valid connections:
        let isValidInputPlaceUsage :: [Place] -> [Place] -> Bool
isValidInputPlaceUsage =
              if Int
requiredFusableTransitionsConsuming Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
              then \[Place]
_ [Place]
_ -> Bool
True
              else \[Place]
vor [Place]
nach ->
                 -- For each place in vor: if it's a forbidden input place, only allow if vor == nach == [that place]
                 (Place -> Bool) -> [Place] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Place
place -> Bool -> Bool
not (Place -> Bimap Transition Place -> Bool
forall a b. (Ord a, Ord b) => b -> Bimap a b -> Bool
BM.memberR Place
place Bimap Transition Place
transitionConsumingBimap) Bool -> Bool -> Bool
|| ([Place]
vor [Place] -> [Place] -> Bool
forall a. Eq a => a -> a -> Bool
== [Place
place] Bool -> Bool -> Bool
&& [Place]
nach [Place] -> [Place] -> Bool
forall a. Eq a => a -> a -> Bool
== [Place
place])) [Place]
vor
            isValidOutputPlaceUsage :: [Place] -> [Place] -> Bool
isValidOutputPlaceUsage =
              if Int
requiredFusableTransitionsProducing Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
              then \[Place]
_ [Place]
_ -> Bool
True
              else \[Place]
nach [Place]
vor ->
                 -- For each place in nach: if it's a forbidden output place, only allow if vor == nach == [that place]
                 (Place -> Bool) -> [Place] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Place
place -> Bool -> Bool
not (Place -> Bimap Transition Place -> Bool
forall a b. (Ord a, Ord b) => b -> Bimap a b -> Bool
BM.memberR Place
place Bimap Transition Place
transitionProducingBimap) Bool -> Bool -> Bool
|| ([Place]
vor [Place] -> [Place] -> Bool
forall a. Eq a => a -> a -> Bool
== [Place
place] Bool -> Bool -> Bool
&& [Place]
nach [Place] -> [Place] -> Bool
forall a. Eq a => a -> a -> Bool
== [Place
place])) [Place]
nach
        (ArrowDensityConstraints
 -> Int
 -> [Place]
 -> [Transition]
 -> Capacity Place
 -> TransitionBehaviorConstraints
 -> RandT g m (Maybe (Net Place Transition)))
-> MaybeT
     (RandT g m)
     (ArrowDensityConstraints
      -> Int
      -> [Place]
      -> [Transition]
      -> Capacity Place
      -> TransitionBehaviorConstraints
      -> RandT g m (Maybe (Net Place Transition)))
forall a. a -> MaybeT (RandT g m) a
forall (f :: * -> *) a. Applicative f => a -> f a
return ((ArrowDensityConstraints
  -> Int
  -> [Place]
  -> [Transition]
  -> Capacity Place
  -> TransitionBehaviorConstraints
  -> RandT g m (Maybe (Net Place Transition)))
 -> MaybeT
      (RandT g m)
      (ArrowDensityConstraints
       -> Int
       -> [Place]
       -> [Transition]
       -> Capacity Place
       -> TransitionBehaviorConstraints
       -> RandT g m (Maybe (Net Place Transition))))
-> (ArrowDensityConstraints
    -> Int
    -> [Place]
    -> [Transition]
    -> Capacity Place
    -> TransitionBehaviorConstraints
    -> RandT g m (Maybe (Net Place Transition)))
-> MaybeT
     (RandT g m)
     (ArrowDensityConstraints
      -> Int
      -> [Place]
      -> [Transition]
      -> Capacity Place
      -> TransitionBehaviorConstraints
      -> RandT g m (Maybe (Net Place Transition)))
forall a b. (a -> b) -> a -> b
$ (RandT g m [Place]
 -> RandT g m [Place]
 -> Transition
 -> RandT g m (Connection Place Transition))
-> ArrowDensityConstraints
-> Int
-> [Place]
-> [Transition]
-> Capacity Place
-> TransitionBehaviorConstraints
-> RandT g 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 g m [Place]
  -> RandT g m [Place]
  -> Transition
  -> RandT g m (Connection Place Transition))
 -> ArrowDensityConstraints
 -> Int
 -> [Place]
 -> [Transition]
 -> Capacity Place
 -> TransitionBehaviorConstraints
 -> RandT g m (Maybe (Net Place Transition)))
-> (RandT g m [Place]
    -> RandT g m [Place]
    -> Transition
    -> RandT g m (Connection Place Transition))
-> ArrowDensityConstraints
-> Int
-> [Place]
-> [Transition]
-> Capacity Place
-> TransitionBehaviorConstraints
-> RandT g m (Maybe (Net Place Transition))
forall a b. (a -> b) -> a -> b
$ \RandT g m [Place]
inputPlacesAction RandT g m [Place]
outputPlacesAction Transition
t ->
          -- Generate a valid connection for a transition, with retry logic
          let
            vorAction :: RandT g m ([Place], [Place], [Place] -> Bool)
vorAction = 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 -> ([Place], [Place], [Place] -> Bool)
-> RandT g m ([Place], [Place], [Place] -> Bool)
forall a. a -> RandT g m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Place
preVor], [], Place -> [Place] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Place
preVor)  -- If t has a pregenerated input place, prevent that place from appearing in nach
                          Maybe Place
_ -> RandT g m [Place]
inputPlacesAction RandT g m [Place]
-> ([Place] -> ([Place], [Place], [Place] -> Bool))
-> RandT g m ([Place], [Place], [Place] -> Bool)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \[Place]
vor -> ([Place]
vor, [Place]
vor, [Place] -> [Place] -> Bool
isValidInputPlaceUsage [Place]
vor)
            nachAction :: RandT g m ([Place], [Place], [Place] -> Bool)
nachAction = 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 -> ([Place], [Place], [Place] -> Bool)
-> RandT g m ([Place], [Place], [Place] -> Bool)
forall a. a -> RandT g m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Place
preNach], [], Place -> [Place] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Place
preNach)  -- If t has a pregenerated output place, prevent that place from appearing in vor
                           Maybe Place
_ -> RandT g m [Place]
outputPlacesAction RandT g m [Place]
-> ([Place] -> ([Place], [Place], [Place] -> Bool))
-> RandT g m ([Place], [Place], [Place] -> Bool)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \[Place]
nach -> ([Place]
nach, [Place]
nach, [Place] -> [Place] -> Bool
isValidOutputPlaceUsage [Place]
nach)
            go :: RandT g m (Connection Place Transition)
go = do
              ([Place]
vor, [Place]
vorForCheck, [Place] -> Bool
checkInputPlaceUsage) <- RandT g m ([Place], [Place], [Place] -> Bool)
vorAction
              ([Place]
nach, [Place]
nachForCheck, [Place] -> Bool
checkOutputPlaceUsage) <- RandT g m ([Place], [Place], [Place] -> Bool)
nachAction
              if [Place] -> Bool
checkInputPlaceUsage [Place]
nachForCheck Bool -> Bool -> Bool
&& [Place] -> Bool
checkOutputPlaceUsage [Place]
vorForCheck
                then Connection Place Transition
-> RandT g m (Connection Place Transition)
forall a. a -> RandT g m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Place]
vor, Transition
t, [Place]
nach)
                else RandT g m (Connection Place Transition)
go  -- Retry if invalid
          in RandT g m (Connection Place Transition)
go
    Net Place Transition
n <- RandT g m (Maybe (Net Place Transition))
-> MaybeT (RandT g m) (Net Place Transition)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (RandT g m (Maybe (Net Place Transition))
 -> MaybeT (RandT g m) (Net Place Transition))
-> RandT g m (Maybe (Net Place Transition))
-> MaybeT (RandT g m) (Net Place Transition)
forall a b. (a -> b) -> a -> b
$ ArrowDensityConstraints
-> Int
-> [Place]
-> [Transition]
-> Capacity Place
-> TransitionBehaviorConstraints
-> RandT g 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 g m) ()) -> MaybeT (RandT g m) ()
forall (m :: * -> *) a.
Applicative m =>
Maybe a -> (a -> m ()) -> m ()
whenJust (DeadlockConfig -> Maybe Int
fusableTransitionsConsumingAreExactly DeadlockConfig
conf) ((Int -> MaybeT (RandT g m) ()) -> MaybeT (RandT g m) ())
-> (Int -> MaybeT (RandT g m) ()) -> MaybeT (RandT g m) ()
forall a b. (a -> b) -> a -> b
$ \Int
expected ->
      Bool -> MaybeT (RandT g m) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT (RandT g m) ()) -> Bool -> MaybeT (RandT g 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 g m) ()) -> MaybeT (RandT g m) ()
forall (m :: * -> *) a.
Applicative m =>
Maybe a -> (a -> m ()) -> m ()
whenJust (DeadlockConfig -> Maybe Int
fusableTransitionsProducingAreExactly DeadlockConfig
conf) ((Int -> MaybeT (RandT g m) ()) -> MaybeT (RandT g m) ())
-> (Int -> MaybeT (RandT g m) ()) -> MaybeT (RandT g m) ()
forall a b. (a -> b) -> a -> b
$ \Int
expected ->
      Bool -> MaybeT (RandT g m) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT (RandT g m) ()) -> Bool -> MaybeT (RandT g 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 g m) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT (RandT g m) ()) -> Bool -> MaybeT (RandT g 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 g m) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT (RandT g m) ()) -> Bool -> MaybeT (RandT g 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 g m)
     (GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall (m :: * -> *) p t g.
(MonadCatch m, MonadDiagrams m, MonadGraphviz m, Ord p, Ord t,
 RandomGen g, Sequential t, Show p, Show t) =>
Net p t
-> [GraphvizCommand]
-> [[t]]
-> FilterConfig
-> Int
-> Int
-> MaybeT
     (RandT g 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)]
  }