{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TupleSections #-}

{-|
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 where

import qualified Control.Monad.Trans              as Monad (lift)
import qualified Data.Map                         as M (fromList)
import qualified Data.Set                         as S (fromList, toList)

import Capabilities.Cache               (MonadCache)
import Capabilities.Diagrams            (MonadDiagrams)
import Capabilities.Graphviz            (MonadGraphviz)
import Modelling.PetriNet.Reach.Draw    (drawToFile, isPetriDrawable)
import Modelling.PetriNet.Reach.Property (
  Property (Default),
  validate,
  )
import Modelling.PetriNet.Reach.ConfigValidation (
  checkBasicPetriConfig,
  )
import Modelling.PetriNet.Reach.Reach   (
  assertReachPoints,
  isNoLonger,
  reportReachFor,
  transitionsValid,
  )
import Modelling.PetriNet.Reach.Roll    (netLimits)
import Modelling.PetriNet.Reach.Step    (deadlocks, deadlocks', executes, successors)
import Modelling.PetriNet.Reach.Type (
  Capacity (Unbounded),
  Net (..),
  Place (..),
  ShowPlace (ShowPlace),
  ShowTransition (ShowTransition),
  State (State),
  Transition (..),
  TransitionsList (TransitionsList),
  bimapNet,
  example,
  hasIsolatedNodes,
  )

import Control.Applicative              (Alternative)
import Control.OutputCapable.Blocks (
  LangM,
  OutputCapable,
  Rated,
  english,
  german,
  translate,
  yesNo,
  )
import Control.OutputCapable.Blocks.Generic (
  ($>>),
  ($>>=),
  )
import Data.Bifunctor                   (Bifunctor (second))
import Data.Either.Combinators          (whenRight)
import Control.Functor.Trans            (FunctorTrans (lift))
import Control.Monad                    (guard, replicateM)
import Control.Monad.Catch              (MonadCatch, MonadThrow)
import Control.Monad.Extra              (findM, maybeM)
import Control.Monad.Random             (MonadRandom, evalRandT, mkStdGen)
import Data.GraphViz                    (GraphvizCommand (..))
import Data.List                        (maximumBy)
import Data.Maybe                       (fromMaybe)
import Data.Ord                         (comparing)
import Data.Typeable                    (Typeable)
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
    )
  => 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) =>
FilePath -> DeadlockInstance s t -> LangM m
deadlockTask 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 -> FilePath
-> Maybe Int
-> Maybe Int
-> Int
-> Bool
-> Maybe (Either FilePath FilePath)
-> GenericLangM Language m ()
forall (m :: * -> *).
OutputCapable m =>
FilePath
-> Maybe Int
-> Maybe Int
-> Int
-> Bool
-> Maybe (Either FilePath FilePath)
-> LangM m
reportReachFor
    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
     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
      | DeadlockInstance ShowPlace ShowTransition -> Bool
forall s t. DeadlockInstance s t -> Bool
showSolution DeadlockInstance ShowPlace ShowTransition
deadlockInstance
      = FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just (FilePath -> Maybe FilePath) -> FilePath -> Maybe FilePath
forall a b. (a -> b) -> a -> b
$ TransitionsList -> FilePath
forall a. Show a => a -> FilePath
show (TransitionsList -> FilePath) -> TransitionsList -> FilePath
forall a b. (a -> b) -> a -> b
$ [Transition] -> TransitionsList
TransitionsList ([Transition] -> TransitionsList)
-> [Transition] -> TransitionsList
forall a b. (a -> b) -> a -> b
$ DeadlockInstance Place Transition -> [Transition]
forall s t. Ord s => DeadlockInstance s t -> [t]
deadlockSolution DeadlockInstance Place Transition
deadlock
      | Bool
otherwise
      = Maybe FilePath
forall a. Maybe a
Nothing

deadlockSolution :: Ord s => DeadlockInstance s t -> [t]
deadlockSolution :: forall s t. Ord s => DeadlockInstance s t -> [t]
deadlockSolution = [t] -> [t]
forall a. [a] -> [a]
reverse ([t] -> [t])
-> (DeadlockInstance s t -> [t]) -> DeadlockInstance s t -> [t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State s, [t]) -> [t]
forall a b. (a, b) -> b
snd ((State s, [t]) -> [t])
-> (DeadlockInstance s t -> (State s, [t]))
-> DeadlockInstance s t
-> [t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(State s, [t])] -> (State s, [t])
forall a. HasCallStack => [a] -> a
head ([(State s, [t])] -> (State s, [t]))
-> (DeadlockInstance s t -> [(State s, [t])])
-> DeadlockInstance s t
-> (State s, [t])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(State s, [t])]] -> [(State s, [t])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(State s, [t])]] -> [(State s, [t])])
-> (DeadlockInstance s t -> [[(State s, [t])]])
-> DeadlockInstance s t
-> [(State s, [t])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Net s t -> [[(State s, [t])]]
forall s t. Ord s => Net s t -> [[(State s, [t])]]
deadlocks' (Net s t -> [[(State s, [t])]])
-> (DeadlockInstance s t -> Net s t)
-> DeadlockInstance s t
-> [[(State s, [t])]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeadlockInstance s t -> Net s t
forall s t. DeadlockInstance s t -> Net s t
petriNet

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 -> Bool
showSolution      :: Bool,
  forall s t. DeadlockInstance s t -> Maybe Int
withLengthHint    :: Maybe Int,
  forall s t. DeadlockInstance s t -> Bool
withMinLengthHint :: Bool
  } 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, Typeable)

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
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
showSolution :: forall s t. DeadlockInstance s t -> Bool
drawUsing :: GraphvizCommand
minLength :: Int
noLongerThan :: Maybe Int
petriNet :: Net s t
showPlaceNames :: Bool
showSolution :: Bool
withLengthHint :: Maybe Int
withMinLengthHint :: Bool
..} = 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,
    showSolution :: Bool
showSolution      = Bool
showSolution,
    withLengthHint :: Maybe Int
withLengthHint    = Maybe Int
withLengthHint,
    withMinLengthHint :: Bool
withMinLengthHint = Bool
withMinLengthHint
    }

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

data DeadlockConfig = DeadlockConfig {
  DeadlockConfig -> Int
numPlaces :: Int,
  DeadlockConfig -> Int
numTransitions :: Int,
  DeadlockConfig -> Capacity Place
capacity :: Capacity Place,
  DeadlockConfig -> [GraphvizCommand]
drawCommands        :: [GraphvizCommand],
  DeadlockConfig -> Int
maxTransitionLength :: Int,
  DeadlockConfig -> Int
minTransitionLength :: Int,
  DeadlockConfig -> (Int, Maybe Int)
postconditionsRange :: (Int, Maybe Int),
  DeadlockConfig -> (Int, Maybe Int)
preconditionsRange  :: (Int, Maybe Int),
  DeadlockConfig -> Bool
printSolution       :: Bool,
  DeadlockConfig -> Maybe Int
rejectLongerThan    :: Maybe Int,
  DeadlockConfig -> Bool
showLengthHint      :: Bool,
  DeadlockConfig -> Bool
showMinLengthHint   :: Bool,
  DeadlockConfig -> Bool
showPlaceNamesInNet :: Bool
  }
  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, Typeable)

defaultDeadlockConfig :: DeadlockConfig
defaultDeadlockConfig :: DeadlockConfig
defaultDeadlockConfig =
  DeadlockConfig {
  numPlaces :: Int
numPlaces = Int
4,
  numTransitions :: Int
numTransitions = Int
4,
  capacity :: Capacity Place
Modelling.PetriNet.Reach.Deadlock.capacity = Capacity Place
forall s. Capacity s
Unbounded,
  drawCommands :: [GraphvizCommand]
drawCommands        = [GraphvizCommand
Dot, GraphvizCommand
Neato, GraphvizCommand
TwoPi, GraphvizCommand
Circo, GraphvizCommand
Fdp, GraphvizCommand
Sfdp, GraphvizCommand
Osage, GraphvizCommand
Patchwork],
  maxTransitionLength :: Int
maxTransitionLength = Int
10,
  minTransitionLength :: Int
minTransitionLength = Int
8,
  postconditionsRange :: (Int, Maybe Int)
postconditionsRange = (Int
0, Maybe Int
forall a. Maybe a
Nothing),
  preconditionsRange :: (Int, Maybe Int)
preconditionsRange  = (Int
0, Maybe Int
forall a. Maybe a
Nothing),
  printSolution :: Bool
printSolution       = Bool
False,
  rejectLongerThan :: Maybe Int
rejectLongerThan    = Maybe Int
forall a. Maybe a
Nothing,
  showLengthHint :: Bool
showLengthHint      = Bool
True,
  showMinLengthHint :: Bool
showMinLengthHint   = Bool
True,
  showPlaceNamesInNet :: Bool
showPlaceNamesInNet = Bool
False
  }

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,
  showSolution :: Bool
showSolution      = Bool
False,
  withLengthHint :: Maybe Int
withLengthHint    = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
9,
  withMinLengthHint :: Bool
withMinLengthHint = Bool
True
  }

checkDeadlockConfig :: DeadlockConfig -> Maybe String
checkDeadlockConfig :: DeadlockConfig -> Maybe FilePath
checkDeadlockConfig DeadlockConfig {Bool
Int
[GraphvizCommand]
Maybe Int
(Int, Maybe Int)
Capacity Place
numPlaces :: DeadlockConfig -> Int
numTransitions :: DeadlockConfig -> Int
capacity :: DeadlockConfig -> Capacity Place
drawCommands :: DeadlockConfig -> [GraphvizCommand]
maxTransitionLength :: DeadlockConfig -> Int
minTransitionLength :: DeadlockConfig -> Int
postconditionsRange :: DeadlockConfig -> (Int, Maybe Int)
preconditionsRange :: DeadlockConfig -> (Int, Maybe Int)
printSolution :: DeadlockConfig -> Bool
rejectLongerThan :: DeadlockConfig -> Maybe Int
showLengthHint :: DeadlockConfig -> Bool
showMinLengthHint :: DeadlockConfig -> Bool
showPlaceNamesInNet :: DeadlockConfig -> Bool
numPlaces :: Int
numTransitions :: Int
capacity :: Capacity Place
drawCommands :: [GraphvizCommand]
maxTransitionLength :: Int
minTransitionLength :: Int
postconditionsRange :: (Int, Maybe Int)
preconditionsRange :: (Int, Maybe Int)
printSolution :: Bool
rejectLongerThan :: Maybe Int
showLengthHint :: Bool
showMinLengthHint :: Bool
showPlaceNamesInNet :: Bool
..} =
  Int
-> Int
-> Capacity Place
-> Int
-> Int
-> (Int, Maybe Int)
-> (Int, Maybe Int)
-> [GraphvizCommand]
-> Maybe Int
-> Bool
-> Maybe FilePath
forall s.
Int
-> Int
-> Capacity s
-> Int
-> Int
-> (Int, Maybe Int)
-> (Int, Maybe Int)
-> [GraphvizCommand]
-> Maybe Int
-> Bool
-> Maybe FilePath
checkBasicPetriConfig
    Int
numPlaces
    Int
numTransitions
    Capacity Place
capacity
    Int
minTransitionLength
    Int
maxTransitionLength
    (Int, Maybe Int)
preconditionsRange
    (Int, Maybe Int)
postconditionsRange
    [GraphvizCommand]
drawCommands
    Maybe Int
rejectLongerThan
    Bool
showLengthHint

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
(Int, Maybe Int)
Capacity Place
numPlaces :: DeadlockConfig -> Int
numTransitions :: DeadlockConfig -> Int
capacity :: DeadlockConfig -> Capacity Place
drawCommands :: DeadlockConfig -> [GraphvizCommand]
maxTransitionLength :: DeadlockConfig -> Int
minTransitionLength :: DeadlockConfig -> Int
postconditionsRange :: DeadlockConfig -> (Int, Maybe Int)
preconditionsRange :: DeadlockConfig -> (Int, Maybe Int)
printSolution :: DeadlockConfig -> Bool
rejectLongerThan :: DeadlockConfig -> Maybe Int
showLengthHint :: DeadlockConfig -> Bool
showMinLengthHint :: DeadlockConfig -> Bool
showPlaceNamesInNet :: DeadlockConfig -> Bool
numPlaces :: Int
numTransitions :: Int
capacity :: Capacity Place
drawCommands :: [GraphvizCommand]
maxTransitionLength :: Int
minTransitionLength :: Int
postconditionsRange :: (Int, Maybe Int)
preconditionsRange :: (Int, Maybe Int)
printSolution :: Bool
rejectLongerThan :: Maybe Int
showLengthHint :: Bool
showMinLengthHint :: Bool
showPlaceNamesInNet :: Bool
..} Int
seed = do
  (Net Place Transition
petri, GraphvizCommand
cmd) <- Int
-> DeadlockConfig
-> Int
-> m (Net Place Transition, GraphvizCommand)
forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
Int
-> DeadlockConfig
-> Int
-> m (Net Place Transition, GraphvizCommand)
tries Int
1000 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,
    showSolution :: Bool
showSolution      = Bool
printSolution,
    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
    }

tries
  :: (MonadCatch m, MonadDiagrams m, MonadGraphviz m)
  => Int
  -> DeadlockConfig
  -> Int
  -> m (Net Place Transition, GraphvizCommand)
tries :: forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
Int
-> DeadlockConfig
-> Int
-> m (Net Place Transition, GraphvizCommand)
tries Int
n DeadlockConfig
conf Int
seed = RandT StdGen m (Net Place Transition, GraphvizCommand)
-> m (Net Place Transition, GraphvizCommand)
forall {m :: * -> *} {a}. Monad m => RandT StdGen m a -> m a
eval RandT StdGen m (Net Place Transition, GraphvizCommand)
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)
out = do
      [[(Int, Net Place Transition)]]
xs <- Int
-> RandT StdGen m [(Int, Net Place Transition)]
-> RandT StdGen m [[(Int, Net Place Transition)]]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (RandT StdGen m [(Int, Net Place Transition)]
 -> RandT StdGen m [[(Int, Net Place Transition)]])
-> RandT StdGen m [(Int, Net Place Transition)]
-> RandT StdGen m [[(Int, Net Place Transition)]]
forall a b. (a -> b) -> a -> b
$ DeadlockConfig -> RandT StdGen m [(Int, Net Place Transition)]
forall (m :: * -> *).
MonadRandom m =>
DeadlockConfig -> m [(Int, Net Place Transition)]
try DeadlockConfig
conf
      let (Int
l, Net Place Transition
pn) = ((Int, Net Place Transition)
 -> (Int, Net Place Transition) -> Ordering)
-> [(Int, Net Place Transition)] -> (Int, Net Place Transition)
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy (((Int, Net Place Transition) -> Int)
-> (Int, Net Place Transition)
-> (Int, Net Place Transition)
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Int, Net Place Transition) -> Int
forall a b. (a, b) -> a
fst) ([(Int, Net Place Transition)] -> (Int, Net Place Transition))
-> [(Int, Net Place Transition)] -> (Int, Net Place Transition)
forall a b. (a -> b) -> a -> b
$ [[(Int, Net Place Transition)]] -> [(Int, Net Place Transition)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Int, Net Place Transition)]]
xs
      if Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= DeadlockConfig -> Int
minTransitionLength DeadlockConfig
conf
        then
          RandT StdGen m (Net Place Transition, GraphvizCommand)
-> (GraphvizCommand
    -> RandT StdGen m (Net Place Transition, GraphvizCommand))
-> RandT StdGen m (Maybe GraphvizCommand)
-> RandT StdGen m (Net Place Transition, GraphvizCommand)
forall (m :: * -> *) b a.
Monad m =>
m b -> (a -> m b) -> m (Maybe a) -> m b
maybeM RandT StdGen m (Net Place Transition, GraphvizCommand)
out ((Net Place Transition, GraphvizCommand)
-> RandT StdGen m (Net Place Transition, GraphvizCommand)
forall a. a -> RandT StdGen m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Net Place Transition, GraphvizCommand)
 -> RandT StdGen m (Net Place Transition, GraphvizCommand))
-> (GraphvizCommand -> (Net Place Transition, GraphvizCommand))
-> GraphvizCommand
-> RandT StdGen m (Net Place Transition, GraphvizCommand)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Net Place Transition
pn,))
          (RandT StdGen m (Maybe GraphvizCommand)
 -> RandT StdGen m (Net Place Transition, GraphvizCommand))
-> RandT StdGen m (Maybe GraphvizCommand)
-> RandT StdGen m (Net Place Transition, GraphvizCommand)
forall a b. (a -> b) -> a -> b
$ (GraphvizCommand -> RandT StdGen m Bool)
-> [GraphvizCommand] -> RandT StdGen m (Maybe GraphvizCommand)
forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m (Maybe a)
findM (m Bool -> RandT StdGen m Bool
forall (m :: * -> *) a. Monad m => m a -> RandT StdGen m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Monad.lift (m Bool -> RandT StdGen m Bool)
-> (GraphvizCommand -> m Bool)
-> GraphvizCommand
-> RandT StdGen m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Net Place Transition -> GraphvizCommand -> m Bool
forall (m :: * -> *) s t.
(MonadCatch m, MonadDiagrams m, MonadGraphviz m, Ord s, Ord t,
 Show s, Show t) =>
Net s t -> GraphvizCommand -> m Bool
isPetriDrawable Net Place Transition
pn) ([GraphvizCommand] -> RandT StdGen m (Maybe GraphvizCommand))
-> [GraphvizCommand] -> RandT StdGen m (Maybe GraphvizCommand)
forall a b. (a -> b) -> a -> b
$ DeadlockConfig -> [GraphvizCommand]
drawCommands DeadlockConfig
conf
        else RandT StdGen m (Net Place Transition, GraphvizCommand)
out

try :: MonadRandom m => DeadlockConfig -> m [(Int, Net Place Transition)]
try :: forall (m :: * -> *).
MonadRandom m =>
DeadlockConfig -> m [(Int, Net Place 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)]
  Net Place Transition
n <- Int
-> Int
-> Int
-> Int
-> [Place]
-> [Transition]
-> Capacity Place
-> m (Net Place Transition)
forall (m :: * -> *) s t.
(MonadRandom m, Ord s, Ord t) =>
Int -> Int -> Int -> Int -> [s] -> [t] -> Capacity s -> m (Net s t)
netLimits Int
vLow Int
vHigh Int
nLow Int
nHigh
      [Place]
ps
      [Transition]
ts
      (DeadlockConfig -> Capacity Place
Modelling.PetriNet.Reach.Deadlock.capacity DeadlockConfig
conf)
  return $ do
    -- Filter out nets with isolated nodes
    Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Net Place Transition -> Bool
forall s t. (Ord s, Ord t) => Net s t -> Bool
hasIsolatedNodes Net Place Transition
n
    let ([(Int, [State Place])]
no,[(Int, [State Place])]
yeah) = ((Int, [State Place]) -> Bool)
-> [(Int, [State Place])]
-> ([(Int, [State Place])], [(Int, [State Place])])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span ([State Place] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([State Place] -> Bool)
-> ((Int, [State Place]) -> [State Place])
-> (Int, [State Place])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, [State Place]) -> [State Place]
forall a b. (a, b) -> b
snd)
          ([(Int, [State Place])]
 -> ([(Int, [State Place])], [(Int, [State Place])]))
-> [(Int, [State Place])]
-> ([(Int, [State Place])], [(Int, [State Place])])
forall a b. (a -> b) -> a -> b
$ Int -> [(Int, [State Place])] -> [(Int, [State Place])]
forall a. Int -> [a] -> [a]
take (DeadlockConfig -> Int
maxTransitionLength DeadlockConfig
conf Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
          ([(Int, [State Place])] -> [(Int, [State Place])])
-> [(Int, [State Place])] -> [(Int, [State Place])]
forall a b. (a -> b) -> a -> b
$ [Int] -> [[State Place]] -> [(Int, [State Place])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..]
          ([[State Place]] -> [(Int, [State Place])])
-> [[State Place]] -> [(Int, [State Place])]
forall a b. (a -> b) -> a -> b
$ Net Place Transition -> [[State Place]]
forall s t. Ord s => Net s t -> [[State s]]
deadlocks Net Place Transition
n
    Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [(Int, [State Place])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, [State Place])]
yeah
    return ([(Int, [State Place])] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, [State Place])]
no, Net Place Transition
n)
  where
    fixMaximum :: (a, Maybe Int) -> (a, Int)
fixMaximum = (Maybe Int -> Int) -> (a, Maybe Int) -> (a, Int)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (DeadlockConfig -> Int
numPlaces DeadlockConfig
conf) (Int -> Int) -> (Maybe Int -> Int) -> Maybe Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. Bounded a => a
maxBound)
    (Int
vLow, Int
vHigh) = (Int, Maybe Int) -> (Int, Int)
forall {a}. (a, Maybe Int) -> (a, Int)
fixMaximum ((Int, Maybe Int) -> (Int, Int)) -> (Int, Maybe Int) -> (Int, Int)
forall a b. (a -> b) -> a -> b
$ DeadlockConfig -> (Int, Maybe Int)
preconditionsRange DeadlockConfig
conf
    (Int
nLow, Int
nHigh) = (Int, Maybe Int) -> (Int, Int)
forall {a}. (a, Maybe Int) -> (a, Int)
fixMaximum ((Int, Maybe Int) -> (Int, Int)) -> (Int, Maybe Int) -> (Int, Int)
forall a b. (a -> b) -> a -> b
$ DeadlockConfig -> (Int, Maybe Int)
postconditionsRange DeadlockConfig
conf

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)]
  }