{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# Language DeriveTraversable #-}
{-# Language DuplicateRecordFields #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE StandaloneDeriving #-}
{-|
This module provides types to represent Petri nets.

A Petri net is a mathematical modelling language.
It is used to describe distributed systems.
Another name for Petri net is place / transition (PT) net.

The 'Modelling.PetriNet.Types' module defines basic type class instances and
functions to work on and transform Petri net representations.
-}
module Modelling.PetriNet.Types (
  AdvConfig (..),
  AlloyConfig (..),
  BasicConfig (..),
  Change,
  ChangeConfig (..),
  Concurrent (..),
  Conflict,
  ConflictConfig (..),
  Drawable,
  DrawSettings (..),
  FindConcurrencyConfig (..),
  FindConflictConfig (..),
  GraphConfig (..),
  InvalidPetriNetException (..),
  Net (..),
  Node (..),
  Petri (..),
  PetriChange (..),
  PetriConflict (..),
  PetriConflict' (..),
  PetriLike (..),
  PetriMath (..),
  PetriNode (..),
  PickConcurrencyConfig (..),
  PickConflictConfig (..),
  SimpleNode (..),
  SimplePetriLike,
  SimplePetriNet,
  allDrawSettings,
  checkBasicConfig,
  checkChangeConfig,
  checkGraphLayouts,
  checkPetriNodeCount,
  defaultAdvConfig,
  defaultAlloyConfig,
  defaultBasicConfig,
  defaultChangeConfig,
  defaultFindConcurrencyConfig,
  defaultFindConflictConfig,
  defaultGraphConfig,
  defaultPickConcurrencyConfig,
  defaultPickConflictConfig,
  drawSettingsWithCommand,
  lAdvConfig,
  lAlloyConfig,
  lAtLeastActive,
  lBasicConfig,
  lChangeConfig,
  lConflictConfig,
  lConflictPlaces,
  lConflictTrans,
  lExtraText,
  lFlowOverall,
  lGraphConfig,
  lGraphLayouts,
  lHidePlaceNames,
  lHideTransitionNames,
  lHideWeight1,
  lIsConnected,
  lMaxFlowPerEdge,
  lMaxTokensPerPlace,
  lPlaces,
  lPrintSolution,
  lTokensOverall,
  lTransitions,
  lUniqueConflictPlace,
  mapChange,
  maybeInitial,
  petriLikeToPetri,
  placeNames,
  shuffleNames,
  transformNet,
  transitionNames,
  transitionPairShow,
  ) where

import qualified Modelling.PetriNet.Reach.Type    as Petri (Transition)

import qualified Data.Bimap                       as BM (fromList, lookup)
import qualified Data.Map.Lazy                    as M (
  adjust,
  alter,
  delete,
  elems,
  empty,
  filter,
  foldrWithKey,
  insert,
  keys,
  keysSet,
  lookup,
  mapKeys,
  member,
  null,
  size,
  )
import qualified Data.Set                         as S (empty, union)

import Modelling.Auxiliary.Common       (lensRulesL)
import Modelling.PetriNet.Reach.Type    (Place, ShowTransition (ShowTransition))

import Control.Lens                     (makeLensesWith)
import Control.Monad                    ((<=<))
import Control.Monad.Catch              (Exception, MonadThrow (throwM))
import Control.Monad.Random             (RandT, RandomGen)
import Control.Monad.Trans              (MonadTrans(lift))
import Control.OutputCapable.Blocks     (Language)
import Data.Bimap                       (Bimap)
import Data.Data                        (Data)
import Data.GraphViz.Attributes.Complete (GraphvizCommand (..))
import Data.Map.Lazy                    (Map)
import Data.Maybe                       (fromMaybe)
import GHC.Generics                     (Generic)
import System.Random.Shuffle            (shuffleM)
import Data.Bifoldable                  (Bifoldable (bifoldMap))
import Data.Bifunctor                   (Bifunctor (bimap))
import Data.Bitraversable               (Bitraversable (bitraverse))

data AlloyConfig = AlloyConfig {
  AlloyConfig -> Maybe Integer
maxInstances :: Maybe Integer,
  AlloyConfig -> Maybe Int
timeout      :: Maybe Int
  }
  deriving (Int -> AlloyConfig -> ShowS
[AlloyConfig] -> ShowS
AlloyConfig -> String
(Int -> AlloyConfig -> ShowS)
-> (AlloyConfig -> String)
-> ([AlloyConfig] -> ShowS)
-> Show AlloyConfig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AlloyConfig -> ShowS
showsPrec :: Int -> AlloyConfig -> ShowS
$cshow :: AlloyConfig -> String
show :: AlloyConfig -> String
$cshowList :: [AlloyConfig] -> ShowS
showList :: [AlloyConfig] -> ShowS
Show, ReadPrec [AlloyConfig]
ReadPrec AlloyConfig
Int -> ReadS AlloyConfig
ReadS [AlloyConfig]
(Int -> ReadS AlloyConfig)
-> ReadS [AlloyConfig]
-> ReadPrec AlloyConfig
-> ReadPrec [AlloyConfig]
-> Read AlloyConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS AlloyConfig
readsPrec :: Int -> ReadS AlloyConfig
$creadList :: ReadS [AlloyConfig]
readList :: ReadS [AlloyConfig]
$creadPrec :: ReadPrec AlloyConfig
readPrec :: ReadPrec AlloyConfig
$creadListPrec :: ReadPrec [AlloyConfig]
readListPrec :: ReadPrec [AlloyConfig]
Read, (forall x. AlloyConfig -> Rep AlloyConfig x)
-> (forall x. Rep AlloyConfig x -> AlloyConfig)
-> Generic AlloyConfig
forall x. Rep AlloyConfig x -> AlloyConfig
forall x. AlloyConfig -> Rep AlloyConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AlloyConfig -> Rep AlloyConfig x
from :: forall x. AlloyConfig -> Rep AlloyConfig x
$cto :: forall x. Rep AlloyConfig x -> AlloyConfig
to :: forall x. Rep AlloyConfig x -> AlloyConfig
Generic)

defaultAlloyConfig :: AlloyConfig
defaultAlloyConfig :: AlloyConfig
defaultAlloyConfig = AlloyConfig {
  $sel:maxInstances:AlloyConfig :: Maybe Integer
maxInstances = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
100,
  $sel:timeout:AlloyConfig :: Maybe Int
timeout      = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
50000000
  }

{-|
A 'PetriChange' where nodes are labelled by strings.
-}
type Change = PetriChange String

{-|
A 'PetriChange' describes the changes on a 'PetriLike' graph by mapping 'PlaceNode's
to token changes and origins of an edge to a mapping from their targets to flow
changes.
-}
data PetriChange a = Change {
  -- | The token change 'Map': Mapping places to changes of their tokens.
  forall a. PetriChange a -> Map a Int
tokenChange :: Map a Int,
  -- | The flow change 'Map': Mapping source nodes to a mapping from target
  --   nodes to the flow change (if any) at the edge between source and target.
  forall a. PetriChange a -> Map a (Map a Int)
flowChange  :: Map a (Map a Int)
  }
  deriving (PetriChange a -> PetriChange a -> Bool
(PetriChange a -> PetriChange a -> Bool)
-> (PetriChange a -> PetriChange a -> Bool) -> Eq (PetriChange a)
forall a. Eq a => PetriChange a -> PetriChange a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => PetriChange a -> PetriChange a -> Bool
== :: PetriChange a -> PetriChange a -> Bool
$c/= :: forall a. Eq a => PetriChange a -> PetriChange a -> Bool
/= :: PetriChange a -> PetriChange a -> Bool
Eq, (forall x. PetriChange a -> Rep (PetriChange a) x)
-> (forall x. Rep (PetriChange a) x -> PetriChange a)
-> Generic (PetriChange a)
forall x. Rep (PetriChange a) x -> PetriChange a
forall x. PetriChange a -> Rep (PetriChange a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (PetriChange a) x -> PetriChange a
forall a x. PetriChange a -> Rep (PetriChange a) x
$cfrom :: forall a x. PetriChange a -> Rep (PetriChange a) x
from :: forall x. PetriChange a -> Rep (PetriChange a) x
$cto :: forall a x. Rep (PetriChange a) x -> PetriChange a
to :: forall x. Rep (PetriChange a) x -> PetriChange a
Generic, Int -> PetriChange a -> ShowS
[PetriChange a] -> ShowS
PetriChange a -> String
(Int -> PetriChange a -> ShowS)
-> (PetriChange a -> String)
-> ([PetriChange a] -> ShowS)
-> Show (PetriChange a)
forall a. Show a => Int -> PetriChange a -> ShowS
forall a. Show a => [PetriChange a] -> ShowS
forall a. Show a => PetriChange a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> PetriChange a -> ShowS
showsPrec :: Int -> PetriChange a -> ShowS
$cshow :: forall a. Show a => PetriChange a -> String
show :: PetriChange a -> String
$cshowList :: forall a. Show a => [PetriChange a] -> ShowS
showList :: [PetriChange a] -> ShowS
Show)

{-|
This function acts like 'fmap' on other 'Functor's.

Note that 'Change' is not a true 'Functor' and thus 'mapChange' is not a true
'fmap' because an 'Ord' instance is required for 'Change's first type parameter
for 'mapChange' to work, furthermore (and that is the original reason),
'mapChange' uses 'M.mapKeys' internally in order to apply the mapping.
Thus, the user of 'mapChange' is responsible to ensure that the transformation
preserves uniqueness on all used keys.
-}
mapChange :: Ord b => (a -> b) -> PetriChange a -> PetriChange b
mapChange :: forall b a. Ord b => (a -> b) -> PetriChange a -> PetriChange b
mapChange a -> b
f (Change Map a Int
tc Map a (Map a Int)
fc) =
  Map b Int -> Map b (Map b Int) -> PetriChange b
forall a. Map a Int -> Map a (Map a Int) -> PetriChange a
Change ((a -> b) -> Map a Int -> Map b Int
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> b
f Map a Int
tc) ((a -> b) -> Map a (Map b Int) -> Map b (Map b Int)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> b
f (Map a (Map b Int) -> Map b (Map b Int))
-> Map a (Map b Int) -> Map b (Map b Int)
forall a b. (a -> b) -> a -> b
$ (a -> b) -> Map a Int -> Map b Int
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> b
f (Map a Int -> Map b Int) -> Map a (Map a Int) -> Map a (Map b Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map a (Map a Int)
fc)

{-|
A 'PetriConflict' describes a conflict between two transitions.
It occurs when the number of tokens at the source place are not enough to fire
both transitions (both are having the same source place).
-}
data PetriConflict p t = Conflict {
  -- | The pair of transitions in conflict.
  forall p t. PetriConflict p t -> (t, t)
conflictTrans :: (t, t),
  -- | The set of source nodes having not enough tokens to fire both transitions.
  forall p t. PetriConflict p t -> [p]
conflictPlaces :: [p]
  }
  deriving ((forall a b. (a -> b) -> PetriConflict p a -> PetriConflict p b)
-> (forall a b. a -> PetriConflict p b -> PetriConflict p a)
-> Functor (PetriConflict p)
forall a b. a -> PetriConflict p b -> PetriConflict p a
forall a b. (a -> b) -> PetriConflict p a -> PetriConflict p b
forall p a b. a -> PetriConflict p b -> PetriConflict p a
forall p a b. (a -> b) -> PetriConflict p a -> PetriConflict p b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall p a b. (a -> b) -> PetriConflict p a -> PetriConflict p b
fmap :: forall a b. (a -> b) -> PetriConflict p a -> PetriConflict p b
$c<$ :: forall p a b. a -> PetriConflict p b -> PetriConflict p a
<$ :: forall a b. a -> PetriConflict p b -> PetriConflict p a
Functor, (forall x. PetriConflict p t -> Rep (PetriConflict p t) x)
-> (forall x. Rep (PetriConflict p t) x -> PetriConflict p t)
-> Generic (PetriConflict p t)
forall x. Rep (PetriConflict p t) x -> PetriConflict p t
forall x. PetriConflict p t -> Rep (PetriConflict p t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall p t x. Rep (PetriConflict p t) x -> PetriConflict p t
forall p t x. PetriConflict p t -> Rep (PetriConflict p t) x
$cfrom :: forall p t x. PetriConflict p t -> Rep (PetriConflict p t) x
from :: forall x. PetriConflict p t -> Rep (PetriConflict p t) x
$cto :: forall p t x. Rep (PetriConflict p t) x -> PetriConflict p t
to :: forall x. Rep (PetriConflict p t) x -> PetriConflict p t
Generic, ReadPrec [PetriConflict p t]
ReadPrec (PetriConflict p t)
Int -> ReadS (PetriConflict p t)
ReadS [PetriConflict p t]
(Int -> ReadS (PetriConflict p t))
-> ReadS [PetriConflict p t]
-> ReadPrec (PetriConflict p t)
-> ReadPrec [PetriConflict p t]
-> Read (PetriConflict p t)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall p t. (Read t, Read p) => ReadPrec [PetriConflict p t]
forall p t. (Read t, Read p) => ReadPrec (PetriConflict p t)
forall p t. (Read t, Read p) => Int -> ReadS (PetriConflict p t)
forall p t. (Read t, Read p) => ReadS [PetriConflict p t]
$creadsPrec :: forall p t. (Read t, Read p) => Int -> ReadS (PetriConflict p t)
readsPrec :: Int -> ReadS (PetriConflict p t)
$creadList :: forall p t. (Read t, Read p) => ReadS [PetriConflict p t]
readList :: ReadS [PetriConflict p t]
$creadPrec :: forall p t. (Read t, Read p) => ReadPrec (PetriConflict p t)
readPrec :: ReadPrec (PetriConflict p t)
$creadListPrec :: forall p t. (Read t, Read p) => ReadPrec [PetriConflict p t]
readListPrec :: ReadPrec [PetriConflict p t]
Read, Int -> PetriConflict p t -> ShowS
[PetriConflict p t] -> ShowS
PetriConflict p t -> String
(Int -> PetriConflict p t -> ShowS)
-> (PetriConflict p t -> String)
-> ([PetriConflict p t] -> ShowS)
-> Show (PetriConflict p t)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall p t. (Show t, Show p) => Int -> PetriConflict p t -> ShowS
forall p t. (Show t, Show p) => [PetriConflict p t] -> ShowS
forall p t. (Show t, Show p) => PetriConflict p t -> String
$cshowsPrec :: forall p t. (Show t, Show p) => Int -> PetriConflict p t -> ShowS
showsPrec :: Int -> PetriConflict p t -> ShowS
$cshow :: forall p t. (Show t, Show p) => PetriConflict p t -> String
show :: PetriConflict p t -> String
$cshowList :: forall p t. (Show t, Show p) => [PetriConflict p t] -> ShowS
showList :: [PetriConflict p t] -> ShowS
Show)

makeLensesWith lensRulesL ''PetriConflict

{-|
A 'PetriConflict' where nodes are labelled by strings.
-}
type Conflict = PetriConflict Place Petri.Transition

newtype PetriConflict' x = PetriConflict' {
  forall x. PetriConflict' x -> PetriConflict x x
toPetriConflict :: PetriConflict x x
  }
  deriving ((forall x. PetriConflict' x -> Rep (PetriConflict' x) x)
-> (forall x. Rep (PetriConflict' x) x -> PetriConflict' x)
-> Generic (PetriConflict' x)
forall x. Rep (PetriConflict' x) x -> PetriConflict' x
forall x. PetriConflict' x -> Rep (PetriConflict' x) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall x x. Rep (PetriConflict' x) x -> PetriConflict' x
forall x x. PetriConflict' x -> Rep (PetriConflict' x) x
$cfrom :: forall x x. PetriConflict' x -> Rep (PetriConflict' x) x
from :: forall x. PetriConflict' x -> Rep (PetriConflict' x) x
$cto :: forall x x. Rep (PetriConflict' x) x -> PetriConflict' x
to :: forall x. Rep (PetriConflict' x) x -> PetriConflict' x
Generic, ReadPrec [PetriConflict' x]
ReadPrec (PetriConflict' x)
Int -> ReadS (PetriConflict' x)
ReadS [PetriConflict' x]
(Int -> ReadS (PetriConflict' x))
-> ReadS [PetriConflict' x]
-> ReadPrec (PetriConflict' x)
-> ReadPrec [PetriConflict' x]
-> Read (PetriConflict' x)
forall x. Read x => ReadPrec [PetriConflict' x]
forall x. Read x => ReadPrec (PetriConflict' x)
forall x. Read x => Int -> ReadS (PetriConflict' x)
forall x. Read x => ReadS [PetriConflict' x]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall x. Read x => Int -> ReadS (PetriConflict' x)
readsPrec :: Int -> ReadS (PetriConflict' x)
$creadList :: forall x. Read x => ReadS [PetriConflict' x]
readList :: ReadS [PetriConflict' x]
$creadPrec :: forall x. Read x => ReadPrec (PetriConflict' x)
readPrec :: ReadPrec (PetriConflict' x)
$creadListPrec :: forall x. Read x => ReadPrec [PetriConflict' x]
readListPrec :: ReadPrec [PetriConflict' x]
Read, Int -> PetriConflict' x -> ShowS
[PetriConflict' x] -> ShowS
PetriConflict' x -> String
(Int -> PetriConflict' x -> ShowS)
-> (PetriConflict' x -> String)
-> ([PetriConflict' x] -> ShowS)
-> Show (PetriConflict' x)
forall x. Show x => Int -> PetriConflict' x -> ShowS
forall x. Show x => [PetriConflict' x] -> ShowS
forall x. Show x => PetriConflict' x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall x. Show x => Int -> PetriConflict' x -> ShowS
showsPrec :: Int -> PetriConflict' x -> ShowS
$cshow :: forall x. Show x => PetriConflict' x -> String
show :: PetriConflict' x -> String
$cshowList :: forall x. Show x => [PetriConflict' x] -> ShowS
showList :: [PetriConflict' x] -> ShowS
Show)

instance Functor PetriConflict' where
  fmap :: forall a b. (a -> b) -> PetriConflict' a -> PetriConflict' b
fmap a -> b
f = PetriConflict b b -> PetriConflict' b
forall x. PetriConflict x x -> PetriConflict' x
PetriConflict' (PetriConflict b b -> PetriConflict' b)
-> (PetriConflict' a -> PetriConflict b b)
-> PetriConflict' a
-> PetriConflict' b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> (a -> b) -> PetriConflict a a -> PetriConflict b b
forall a b c d.
(a -> b) -> (c -> d) -> PetriConflict a c -> PetriConflict b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
f a -> b
f (PetriConflict a a -> PetriConflict b b)
-> (PetriConflict' a -> PetriConflict a a)
-> PetriConflict' a
-> PetriConflict b b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriConflict' a -> PetriConflict a a
forall x. PetriConflict' x -> PetriConflict x x
toPetriConflict

instance Foldable PetriConflict' where
  foldMap :: forall m a. Monoid m => (a -> m) -> PetriConflict' a -> m
foldMap a -> m
f = (a -> m) -> (a -> m) -> PetriConflict a a -> m
forall m a b.
Monoid m =>
(a -> m) -> (b -> m) -> PetriConflict a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap a -> m
f a -> m
f (PetriConflict a a -> m)
-> (PetriConflict' a -> PetriConflict a a) -> PetriConflict' a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriConflict' a -> PetriConflict a a
forall x. PetriConflict' x -> PetriConflict x x
toPetriConflict

instance Traversable PetriConflict' where
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PetriConflict' a -> f (PetriConflict' b)
traverse a -> f b
f = (PetriConflict b b -> PetriConflict' b)
-> f (PetriConflict b b) -> f (PetriConflict' b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PetriConflict b b -> PetriConflict' b
forall x. PetriConflict x x -> PetriConflict' x
PetriConflict' (f (PetriConflict b b) -> f (PetriConflict' b))
-> (PetriConflict' a -> f (PetriConflict b b))
-> PetriConflict' a
-> f (PetriConflict' b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f b)
-> (a -> f b) -> PetriConflict a a -> f (PetriConflict b b)
forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c)
-> (b -> f d) -> PetriConflict a b -> f (PetriConflict c d)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse a -> f b
f a -> f b
f (PetriConflict a a -> f (PetriConflict b b))
-> (PetriConflict' a -> PetriConflict a a)
-> PetriConflict' a
-> f (PetriConflict b b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriConflict' a -> PetriConflict a a
forall x. PetriConflict' x -> PetriConflict x x
toPetriConflict

instance Bifunctor PetriConflict where
  bimap :: forall a b c d.
(a -> b) -> (c -> d) -> PetriConflict a c -> PetriConflict b d
bimap a -> b
f c -> d
g (Conflict (c, c)
ts [a]
as) = (d, d) -> [b] -> PetriConflict b d
forall p t. (t, t) -> [p] -> PetriConflict p t
Conflict ((c -> d) -> (c -> d) -> (c, c) -> (d, d)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap c -> d
g c -> d
g (c, c)
ts) ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
f [a]
as)

instance Bifoldable PetriConflict where
  bifoldMap :: forall m a b.
Monoid m =>
(a -> m) -> (b -> m) -> PetriConflict a b -> m
bifoldMap a -> m
f b -> m
g (Conflict (b, b)
ts [a]
as) = (a -> m) -> [a] -> m
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f [a]
as m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (b -> m) -> (b -> m) -> (b, b) -> m
forall m a b. Monoid m => (a -> m) -> (b -> m) -> (a, b) -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap b -> m
g b -> m
g (b, b)
ts

instance Bitraversable PetriConflict where
  bitraverse :: forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c)
-> (b -> f d) -> PetriConflict a b -> f (PetriConflict c d)
bitraverse a -> f c
f b -> f d
g (Conflict (b, b)
ts [a]
as) = (d, d) -> [c] -> PetriConflict c d
forall p t. (t, t) -> [p] -> PetriConflict p t
Conflict
    ((d, d) -> [c] -> PetriConflict c d)
-> f (d, d) -> f ([c] -> PetriConflict c d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (b -> f d) -> (b -> f d) -> (b, b) -> f (d, d)
forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c) -> (b -> f d) -> (a, b) -> f (c, d)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse b -> f d
g b -> f d
g (b, b)
ts
    f ([c] -> PetriConflict c d) -> f [c] -> f (PetriConflict c d)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f c) -> [a] -> f [c]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> f c
f [a]
as

newtype Concurrent a = Concurrent (a, a)
  deriving ((forall m. Monoid m => Concurrent m -> m)
-> (forall m a. Monoid m => (a -> m) -> Concurrent a -> m)
-> (forall m a. Monoid m => (a -> m) -> Concurrent a -> m)
-> (forall a b. (a -> b -> b) -> b -> Concurrent a -> b)
-> (forall a b. (a -> b -> b) -> b -> Concurrent a -> b)
-> (forall b a. (b -> a -> b) -> b -> Concurrent a -> b)
-> (forall b a. (b -> a -> b) -> b -> Concurrent a -> b)
-> (forall a. (a -> a -> a) -> Concurrent a -> a)
-> (forall a. (a -> a -> a) -> Concurrent a -> a)
-> (forall a. Concurrent a -> [a])
-> (forall a. Concurrent a -> Bool)
-> (forall a. Concurrent a -> Int)
-> (forall a. Eq a => a -> Concurrent a -> Bool)
-> (forall a. Ord a => Concurrent a -> a)
-> (forall a. Ord a => Concurrent a -> a)
-> (forall a. Num a => Concurrent a -> a)
-> (forall a. Num a => Concurrent a -> a)
-> Foldable Concurrent
forall a. Eq a => a -> Concurrent a -> Bool
forall a. Num a => Concurrent a -> a
forall a. Ord a => Concurrent a -> a
forall m. Monoid m => Concurrent m -> m
forall a. Concurrent a -> Bool
forall a. Concurrent a -> Int
forall a. Concurrent a -> [a]
forall a. (a -> a -> a) -> Concurrent a -> a
forall m a. Monoid m => (a -> m) -> Concurrent a -> m
forall b a. (b -> a -> b) -> b -> Concurrent a -> b
forall a b. (a -> b -> b) -> b -> Concurrent a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Concurrent m -> m
fold :: forall m. Monoid m => Concurrent m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Concurrent a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Concurrent a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Concurrent a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Concurrent a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Concurrent a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Concurrent a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Concurrent a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Concurrent a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Concurrent a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Concurrent a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Concurrent a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Concurrent a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Concurrent a -> a
foldr1 :: forall a. (a -> a -> a) -> Concurrent a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Concurrent a -> a
foldl1 :: forall a. (a -> a -> a) -> Concurrent a -> a
$ctoList :: forall a. Concurrent a -> [a]
toList :: forall a. Concurrent a -> [a]
$cnull :: forall a. Concurrent a -> Bool
null :: forall a. Concurrent a -> Bool
$clength :: forall a. Concurrent a -> Int
length :: forall a. Concurrent a -> Int
$celem :: forall a. Eq a => a -> Concurrent a -> Bool
elem :: forall a. Eq a => a -> Concurrent a -> Bool
$cmaximum :: forall a. Ord a => Concurrent a -> a
maximum :: forall a. Ord a => Concurrent a -> a
$cminimum :: forall a. Ord a => Concurrent a -> a
minimum :: forall a. Ord a => Concurrent a -> a
$csum :: forall a. Num a => Concurrent a -> a
sum :: forall a. Num a => Concurrent a -> a
$cproduct :: forall a. Num a => Concurrent a -> a
product :: forall a. Num a => Concurrent a -> a
Foldable, (forall a b. (a -> b) -> Concurrent a -> Concurrent b)
-> (forall a b. a -> Concurrent b -> Concurrent a)
-> Functor Concurrent
forall a b. a -> Concurrent b -> Concurrent a
forall a b. (a -> b) -> Concurrent a -> Concurrent b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Concurrent a -> Concurrent b
fmap :: forall a b. (a -> b) -> Concurrent a -> Concurrent b
$c<$ :: forall a b. a -> Concurrent b -> Concurrent a
<$ :: forall a b. a -> Concurrent b -> Concurrent a
Functor, (forall x. Concurrent a -> Rep (Concurrent a) x)
-> (forall x. Rep (Concurrent a) x -> Concurrent a)
-> Generic (Concurrent a)
forall x. Rep (Concurrent a) x -> Concurrent a
forall x. Concurrent a -> Rep (Concurrent a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Concurrent a) x -> Concurrent a
forall a x. Concurrent a -> Rep (Concurrent a) x
$cfrom :: forall a x. Concurrent a -> Rep (Concurrent a) x
from :: forall x. Concurrent a -> Rep (Concurrent a) x
$cto :: forall a x. Rep (Concurrent a) x -> Concurrent a
to :: forall x. Rep (Concurrent a) x -> Concurrent a
Generic, ReadPrec [Concurrent a]
ReadPrec (Concurrent a)
Int -> ReadS (Concurrent a)
ReadS [Concurrent a]
(Int -> ReadS (Concurrent a))
-> ReadS [Concurrent a]
-> ReadPrec (Concurrent a)
-> ReadPrec [Concurrent a]
-> Read (Concurrent a)
forall a. Read a => ReadPrec [Concurrent a]
forall a. Read a => ReadPrec (Concurrent a)
forall a. Read a => Int -> ReadS (Concurrent a)
forall a. Read a => ReadS [Concurrent a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall a. Read a => Int -> ReadS (Concurrent a)
readsPrec :: Int -> ReadS (Concurrent a)
$creadList :: forall a. Read a => ReadS [Concurrent a]
readList :: ReadS [Concurrent a]
$creadPrec :: forall a. Read a => ReadPrec (Concurrent a)
readPrec :: ReadPrec (Concurrent a)
$creadListPrec :: forall a. Read a => ReadPrec [Concurrent a]
readListPrec :: ReadPrec [Concurrent a]
Read, Int -> Concurrent a -> ShowS
[Concurrent a] -> ShowS
Concurrent a -> String
(Int -> Concurrent a -> ShowS)
-> (Concurrent a -> String)
-> ([Concurrent a] -> ShowS)
-> Show (Concurrent a)
forall a. Show a => Int -> Concurrent a -> ShowS
forall a. Show a => [Concurrent a] -> ShowS
forall a. Show a => Concurrent a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Concurrent a -> ShowS
showsPrec :: Int -> Concurrent a -> ShowS
$cshow :: forall a. Show a => Concurrent a -> String
show :: Concurrent a -> String
$cshowList :: forall a. Show a => [Concurrent a] -> ShowS
showList :: [Concurrent a] -> ShowS
Show, Functor Concurrent
Foldable Concurrent
Functor Concurrent
-> Foldable Concurrent
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Concurrent a -> f (Concurrent b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Concurrent (f a) -> f (Concurrent a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Concurrent a -> m (Concurrent b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Concurrent (m a) -> m (Concurrent a))
-> Traversable Concurrent
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Concurrent (m a) -> m (Concurrent a)
forall (f :: * -> *) a.
Applicative f =>
Concurrent (f a) -> f (Concurrent a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Concurrent a -> m (Concurrent b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Concurrent a -> f (Concurrent b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Concurrent a -> f (Concurrent b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Concurrent a -> f (Concurrent b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Concurrent (f a) -> f (Concurrent a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Concurrent (f a) -> f (Concurrent a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Concurrent a -> m (Concurrent b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Concurrent a -> m (Concurrent b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
Concurrent (m a) -> m (Concurrent a)
sequence :: forall (m :: * -> *) a.
Monad m =>
Concurrent (m a) -> m (Concurrent a)
Traversable)

class Show (n String) => PetriNode n where
  initialTokens     :: n a -> Int

  {-|
  Whether the 'Node' is a 'PlaceNode'.
  -}
  isPlaceNode       :: n a -> Bool

  {-|
  Whether the 'PetriNode' is a 'TransitionNode'.
  -}
  isTransitionNode  :: n a -> Bool

  {-|
  This function acts like 'fmap' on other 'Functor's.

  Note that 'PetriNode' is not necessarily a true 'Functor' and thus 'mapNode'
  is not a true 'fmap' because an 'Ord' instance is required for 'Node's
  first type parameter for 'mapNode' to work,
  furthermore (and that is the original reason), 'mapNode' usually
  uses 'M.mapKeys' internally in order to apply the mapping. Thus, the user of
  'mapNode' is responsible to ensure that the transformation preserves uniqueness
  on all used keys.
  -}
  mapNode           :: Ord b => (a -> b) -> n a -> n b

  {-|
  This function acts like 'traverse' on 'Traversable'.

  Not that 'PetriNode' is not necessarily 'Traversable' itself as it requires
  an 'Ord' instance for the result type within the 'Applicative'
  of its first argument, the applicative lifting transformation function.
  This behaviour occurs, because the traversal changes the keys of the underlying
  'Map'.
  Transformations on this map require a specific traversal 'traverseKeyMap'.

  The user is responsible to ensure uniqueness of the keys after the traversal.
  Note, that the order of values could also change if the transformation is not
  order-preserving.
  -}
  traverseNode      :: (Applicative f, Ord b) => (a -> f b) -> n a -> f (n b)

{-|
A node is part of a Petri like graph (see 'PetriLike').
Each node stores its predecessor and successor nodes together with their weight
in the fields 'flowIn' and 'flowOut' respectively.
Additionally 'PlaceNode's have a value of initial tokens.
-}
data Node a =
  PlaceNode {
  -- | initial tokens of a 'PlaceNode'
  forall a. Node a -> Int
initial :: Int,
  -- | successor nodes
  forall a. Node a -> Map a Int
flowIn  :: Map a Int,
  -- | predecessor nodes
  forall a. Node a -> Map a Int
flowOut :: Map a Int
  } |
  TransitionNode {
  flowIn  :: Map a Int,
  flowOut :: Map a Int
  }
  deriving (Typeable (Node a)
Typeable (Node a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Node a -> c (Node a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Node a))
-> (Node a -> Constr)
-> (Node a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Node a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Node a)))
-> ((forall b. Data b => b -> b) -> Node a -> Node a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Node a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Node a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Node a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Node a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Node a -> m (Node a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Node a -> m (Node a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Node a -> m (Node a))
-> Data (Node a)
Node a -> Constr
Node a -> DataType
(forall b. Data b => b -> b) -> Node a -> Node a
forall {a}. (Data a, Ord a) => Typeable (Node a)
forall a. (Data a, Ord a) => Node a -> Constr
forall a. (Data a, Ord a) => Node a -> DataType
forall a.
(Data a, Ord a) =>
(forall b. Data b => b -> b) -> Node a -> Node a
forall a u.
(Data a, Ord a) =>
Int -> (forall d. Data d => d -> u) -> Node a -> u
forall a u.
(Data a, Ord a) =>
(forall d. Data d => d -> u) -> Node a -> [u]
forall a r r'.
(Data a, Ord a) =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Node a -> r
forall a r r'.
(Data a, Ord a) =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Node a -> r
forall a (m :: * -> *).
(Data a, Ord a, Monad m) =>
(forall d. Data d => d -> m d) -> Node a -> m (Node a)
forall a (m :: * -> *).
(Data a, Ord a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Node a -> m (Node a)
forall a (c :: * -> *).
(Data a, Ord a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Node a)
forall a (c :: * -> *).
(Data a, Ord a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Node a -> c (Node a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Ord a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Node a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Ord a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Node a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Node a -> u
forall u. (forall d. Data d => d -> u) -> Node a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Node a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Node a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Node a -> m (Node a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Node a -> m (Node a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Node a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Node a -> c (Node a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Node a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Node a))
$cgfoldl :: forall a (c :: * -> *).
(Data a, Ord a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Node a -> c (Node a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Node a -> c (Node a)
$cgunfold :: forall a (c :: * -> *).
(Data a, Ord a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Node a)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Node a)
$ctoConstr :: forall a. (Data a, Ord a) => Node a -> Constr
toConstr :: Node a -> Constr
$cdataTypeOf :: forall a. (Data a, Ord a) => Node a -> DataType
dataTypeOf :: Node a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Ord a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Node a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Node a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Ord a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Node a))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Node a))
$cgmapT :: forall a.
(Data a, Ord a) =>
(forall b. Data b => b -> b) -> Node a -> Node a
gmapT :: (forall b. Data b => b -> b) -> Node a -> Node a
$cgmapQl :: forall a r r'.
(Data a, Ord a) =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Node a -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Node a -> r
$cgmapQr :: forall a r r'.
(Data a, Ord a) =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Node a -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Node a -> r
$cgmapQ :: forall a u.
(Data a, Ord a) =>
(forall d. Data d => d -> u) -> Node a -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Node a -> [u]
$cgmapQi :: forall a u.
(Data a, Ord a) =>
Int -> (forall d. Data d => d -> u) -> Node a -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Node a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Ord a, Monad m) =>
(forall d. Data d => d -> m d) -> Node a -> m (Node a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Node a -> m (Node a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, Ord a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Node a -> m (Node a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Node a -> m (Node a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, Ord a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Node a -> m (Node a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Node a -> m (Node a)
Data, Node a -> Node a -> Bool
(Node a -> Node a -> Bool)
-> (Node a -> Node a -> Bool) -> Eq (Node a)
forall a. Eq a => Node a -> Node a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Node a -> Node a -> Bool
== :: Node a -> Node a -> Bool
$c/= :: forall a. Eq a => Node a -> Node a -> Bool
/= :: Node a -> Node a -> Bool
Eq, (forall x. Node a -> Rep (Node a) x)
-> (forall x. Rep (Node a) x -> Node a) -> Generic (Node a)
forall x. Rep (Node a) x -> Node a
forall x. Node a -> Rep (Node a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Node a) x -> Node a
forall a x. Node a -> Rep (Node a) x
$cfrom :: forall a x. Node a -> Rep (Node a) x
from :: forall x. Node a -> Rep (Node a) x
$cto :: forall a x. Rep (Node a) x -> Node a
to :: forall x. Rep (Node a) x -> Node a
Generic, ReadPrec [Node a]
ReadPrec (Node a)
Int -> ReadS (Node a)
ReadS [Node a]
(Int -> ReadS (Node a))
-> ReadS [Node a]
-> ReadPrec (Node a)
-> ReadPrec [Node a]
-> Read (Node a)
forall a. (Ord a, Read a) => ReadPrec [Node a]
forall a. (Ord a, Read a) => ReadPrec (Node a)
forall a. (Ord a, Read a) => Int -> ReadS (Node a)
forall a. (Ord a, Read a) => ReadS [Node a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall a. (Ord a, Read a) => Int -> ReadS (Node a)
readsPrec :: Int -> ReadS (Node a)
$creadList :: forall a. (Ord a, Read a) => ReadS [Node a]
readList :: ReadS [Node a]
$creadPrec :: forall a. (Ord a, Read a) => ReadPrec (Node a)
readPrec :: ReadPrec (Node a)
$creadListPrec :: forall a. (Ord a, Read a) => ReadPrec [Node a]
readListPrec :: ReadPrec [Node a]
Read, Int -> Node a -> ShowS
[Node a] -> ShowS
Node a -> String
(Int -> Node a -> ShowS)
-> (Node a -> String) -> ([Node a] -> ShowS) -> Show (Node a)
forall a. Show a => Int -> Node a -> ShowS
forall a. Show a => [Node a] -> ShowS
forall a. Show a => Node a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Node a -> ShowS
showsPrec :: Int -> Node a -> ShowS
$cshow :: forall a. Show a => Node a -> String
show :: Node a -> String
$cshowList :: forall a. Show a => [Node a] -> ShowS
showList :: [Node a] -> ShowS
Show)

instance PetriNode Node where
  initialTokens :: forall a. Node a -> Int
initialTokens PlaceNode {Int
$sel:initial:PlaceNode :: forall a. Node a -> Int
initial :: Int
initial} = Int
initial
  initialTokens TransitionNode {} =
    String -> Int
forall a. HasCallStack => String -> a
error String
"A TransitionNode does not have initial tokens!"

  isPlaceNode :: forall a. Node a -> Bool
isPlaceNode PlaceNode {} = Bool
True
  isPlaceNode Node a
_            = Bool
False

  isTransitionNode :: forall a. Node a -> Bool
isTransitionNode TransitionNode {} = Bool
True
  isTransitionNode Node a
_                 = Bool
False

  mapNode :: forall b a. Ord b => (a -> b) -> Node a -> Node b
mapNode a -> b
f (PlaceNode Int
s Map a Int
i Map a Int
o) =
    Int -> Map b Int -> Map b Int -> Node b
forall a. Int -> Map a Int -> Map a Int -> Node a
PlaceNode Int
s ((a -> b) -> Map a Int -> Map b Int
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> b
f Map a Int
i) ((a -> b) -> Map a Int -> Map b Int
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> b
f Map a Int
o)
  mapNode a -> b
f (TransitionNode Map a Int
i Map a Int
o) =
    Map b Int -> Map b Int -> Node b
forall a. Map a Int -> Map a Int -> Node a
TransitionNode ((a -> b) -> Map a Int -> Map b Int
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> b
f Map a Int
i) ((a -> b) -> Map a Int -> Map b Int
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> b
f Map a Int
o)

  traverseNode :: forall (f :: * -> *) b a.
(Applicative f, Ord b) =>
(a -> f b) -> Node a -> f (Node b)
traverseNode a -> f b
f (PlaceNode Int
s Map a Int
i Map a Int
o) =
    Int -> Map b Int -> Map b Int -> Node b
forall a. Int -> Map a Int -> Map a Int -> Node a
PlaceNode Int
s (Map b Int -> Map b Int -> Node b)
-> f (Map b Int) -> f (Map b Int -> Node b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> Map a Int -> f (Map b Int)
forall (f :: * -> *) k2 k1 a.
(Applicative f, Ord k2) =>
(k1 -> f k2) -> Map k1 a -> f (Map k2 a)
traverseKeyMap a -> f b
f Map a Int
i f (Map b Int -> Node b) -> f (Map b Int) -> f (Node b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f b) -> Map a Int -> f (Map b Int)
forall (f :: * -> *) k2 k1 a.
(Applicative f, Ord k2) =>
(k1 -> f k2) -> Map k1 a -> f (Map k2 a)
traverseKeyMap a -> f b
f Map a Int
o
  traverseNode a -> f b
f (TransitionNode Map a Int
i Map a Int
o) =
    Map b Int -> Map b Int -> Node b
forall a. Map a Int -> Map a Int -> Node a
TransitionNode (Map b Int -> Map b Int -> Node b)
-> f (Map b Int) -> f (Map b Int -> Node b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> Map a Int -> f (Map b Int)
forall (f :: * -> *) k2 k1 a.
(Applicative f, Ord k2) =>
(k1 -> f k2) -> Map k1 a -> f (Map k2 a)
traverseKeyMap a -> f b
f Map a Int
i f (Map b Int -> Node b) -> f (Map b Int) -> f (Node b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f b) -> Map a Int -> f (Map b Int)
forall (f :: * -> *) k2 k1 a.
(Applicative f, Ord k2) =>
(k1 -> f k2) -> Map k1 a -> f (Map k2 a)
traverseKeyMap a -> f b
f Map a Int
o

data SimpleNode a =
  SimplePlace {
  forall a. SimpleNode a -> Int
initial           :: Int,
  forall a. SimpleNode a -> Map a Int
flowOut           :: Map a Int
  } |
  SimpleTransition {
  flowOut           :: Map a Int
  }
  deriving (Typeable (SimpleNode a)
Typeable (SimpleNode a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> SimpleNode a -> c (SimpleNode a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (SimpleNode a))
-> (SimpleNode a -> Constr)
-> (SimpleNode a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (SimpleNode a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (SimpleNode a)))
-> ((forall b. Data b => b -> b) -> SimpleNode a -> SimpleNode a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SimpleNode a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SimpleNode a -> r)
-> (forall u. (forall d. Data d => d -> u) -> SimpleNode a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SimpleNode a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SimpleNode a -> m (SimpleNode a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SimpleNode a -> m (SimpleNode a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SimpleNode a -> m (SimpleNode a))
-> Data (SimpleNode a)
SimpleNode a -> Constr
SimpleNode a -> DataType
(forall b. Data b => b -> b) -> SimpleNode a -> SimpleNode a
forall {a}. (Data a, Ord a) => Typeable (SimpleNode a)
forall a. (Data a, Ord a) => SimpleNode a -> Constr
forall a. (Data a, Ord a) => SimpleNode a -> DataType
forall a.
(Data a, Ord a) =>
(forall b. Data b => b -> b) -> SimpleNode a -> SimpleNode a
forall a u.
(Data a, Ord a) =>
Int -> (forall d. Data d => d -> u) -> SimpleNode a -> u
forall a u.
(Data a, Ord a) =>
(forall d. Data d => d -> u) -> SimpleNode a -> [u]
forall a r r'.
(Data a, Ord a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SimpleNode a -> r
forall a r r'.
(Data a, Ord a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SimpleNode a -> r
forall a (m :: * -> *).
(Data a, Ord a, Monad m) =>
(forall d. Data d => d -> m d) -> SimpleNode a -> m (SimpleNode a)
forall a (m :: * -> *).
(Data a, Ord a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SimpleNode a -> m (SimpleNode a)
forall a (c :: * -> *).
(Data a, Ord a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SimpleNode a)
forall a (c :: * -> *).
(Data a, Ord a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SimpleNode a -> c (SimpleNode a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Ord a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SimpleNode a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Ord a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SimpleNode a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SimpleNode a -> u
forall u. (forall d. Data d => d -> u) -> SimpleNode a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SimpleNode a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SimpleNode a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SimpleNode a -> m (SimpleNode a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SimpleNode a -> m (SimpleNode a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SimpleNode a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SimpleNode a -> c (SimpleNode a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (SimpleNode a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SimpleNode a))
$cgfoldl :: forall a (c :: * -> *).
(Data a, Ord a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SimpleNode a -> c (SimpleNode a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SimpleNode a -> c (SimpleNode a)
$cgunfold :: forall a (c :: * -> *).
(Data a, Ord a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SimpleNode a)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SimpleNode a)
$ctoConstr :: forall a. (Data a, Ord a) => SimpleNode a -> Constr
toConstr :: SimpleNode a -> Constr
$cdataTypeOf :: forall a. (Data a, Ord a) => SimpleNode a -> DataType
dataTypeOf :: SimpleNode a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Ord a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SimpleNode a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (SimpleNode a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Ord a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SimpleNode a))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SimpleNode a))
$cgmapT :: forall a.
(Data a, Ord a) =>
(forall b. Data b => b -> b) -> SimpleNode a -> SimpleNode a
gmapT :: (forall b. Data b => b -> b) -> SimpleNode a -> SimpleNode a
$cgmapQl :: forall a r r'.
(Data a, Ord a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SimpleNode a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SimpleNode a -> r
$cgmapQr :: forall a r r'.
(Data a, Ord a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SimpleNode a -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SimpleNode a -> r
$cgmapQ :: forall a u.
(Data a, Ord a) =>
(forall d. Data d => d -> u) -> SimpleNode a -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SimpleNode a -> [u]
$cgmapQi :: forall a u.
(Data a, Ord a) =>
Int -> (forall d. Data d => d -> u) -> SimpleNode a -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SimpleNode a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Ord a, Monad m) =>
(forall d. Data d => d -> m d) -> SimpleNode a -> m (SimpleNode a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SimpleNode a -> m (SimpleNode a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, Ord a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SimpleNode a -> m (SimpleNode a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SimpleNode a -> m (SimpleNode a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, Ord a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SimpleNode a -> m (SimpleNode a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SimpleNode a -> m (SimpleNode a)
Data, SimpleNode a -> SimpleNode a -> Bool
(SimpleNode a -> SimpleNode a -> Bool)
-> (SimpleNode a -> SimpleNode a -> Bool) -> Eq (SimpleNode a)
forall a. Eq a => SimpleNode a -> SimpleNode a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => SimpleNode a -> SimpleNode a -> Bool
== :: SimpleNode a -> SimpleNode a -> Bool
$c/= :: forall a. Eq a => SimpleNode a -> SimpleNode a -> Bool
/= :: SimpleNode a -> SimpleNode a -> Bool
Eq, (forall x. SimpleNode a -> Rep (SimpleNode a) x)
-> (forall x. Rep (SimpleNode a) x -> SimpleNode a)
-> Generic (SimpleNode a)
forall x. Rep (SimpleNode a) x -> SimpleNode a
forall x. SimpleNode a -> Rep (SimpleNode a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (SimpleNode a) x -> SimpleNode a
forall a x. SimpleNode a -> Rep (SimpleNode a) x
$cfrom :: forall a x. SimpleNode a -> Rep (SimpleNode a) x
from :: forall x. SimpleNode a -> Rep (SimpleNode a) x
$cto :: forall a x. Rep (SimpleNode a) x -> SimpleNode a
to :: forall x. Rep (SimpleNode a) x -> SimpleNode a
Generic, ReadPrec [SimpleNode a]
ReadPrec (SimpleNode a)
Int -> ReadS (SimpleNode a)
ReadS [SimpleNode a]
(Int -> ReadS (SimpleNode a))
-> ReadS [SimpleNode a]
-> ReadPrec (SimpleNode a)
-> ReadPrec [SimpleNode a]
-> Read (SimpleNode a)
forall a. (Ord a, Read a) => ReadPrec [SimpleNode a]
forall a. (Ord a, Read a) => ReadPrec (SimpleNode a)
forall a. (Ord a, Read a) => Int -> ReadS (SimpleNode a)
forall a. (Ord a, Read a) => ReadS [SimpleNode a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall a. (Ord a, Read a) => Int -> ReadS (SimpleNode a)
readsPrec :: Int -> ReadS (SimpleNode a)
$creadList :: forall a. (Ord a, Read a) => ReadS [SimpleNode a]
readList :: ReadS [SimpleNode a]
$creadPrec :: forall a. (Ord a, Read a) => ReadPrec (SimpleNode a)
readPrec :: ReadPrec (SimpleNode a)
$creadListPrec :: forall a. (Ord a, Read a) => ReadPrec [SimpleNode a]
readListPrec :: ReadPrec [SimpleNode a]
Read, Int -> SimpleNode a -> ShowS
[SimpleNode a] -> ShowS
SimpleNode a -> String
(Int -> SimpleNode a -> ShowS)
-> (SimpleNode a -> String)
-> ([SimpleNode a] -> ShowS)
-> Show (SimpleNode a)
forall a. Show a => Int -> SimpleNode a -> ShowS
forall a. Show a => [SimpleNode a] -> ShowS
forall a. Show a => SimpleNode a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> SimpleNode a -> ShowS
showsPrec :: Int -> SimpleNode a -> ShowS
$cshow :: forall a. Show a => SimpleNode a -> String
show :: SimpleNode a -> String
$cshowList :: forall a. Show a => [SimpleNode a] -> ShowS
showList :: [SimpleNode a] -> ShowS
Show)

instance PetriNode SimpleNode where
  initialTokens :: forall a. SimpleNode a -> Int
initialTokens SimplePlace {Int
$sel:initial:SimplePlace :: forall a. SimpleNode a -> Int
initial :: Int
initial} = Int
initial
  initialTokens SimpleTransition {} =
    String -> Int
forall a. HasCallStack => String -> a
error String
"A SimpleTransition does not have initial tokens!"

  isPlaceNode :: forall a. SimpleNode a -> Bool
isPlaceNode SimplePlace {} = Bool
True
  isPlaceNode SimpleNode a
_         = Bool
False

  isTransitionNode :: forall a. SimpleNode a -> Bool
isTransitionNode SimpleTransition {} = Bool
True
  isTransitionNode SimpleNode a
_              = Bool
False

  mapNode :: forall b a. Ord b => (a -> b) -> SimpleNode a -> SimpleNode b
mapNode a -> b
f (SimplePlace Int
s Map a Int
o) =
    Int -> Map b Int -> SimpleNode b
forall a. Int -> Map a Int -> SimpleNode a
SimplePlace Int
s ((a -> b) -> Map a Int -> Map b Int
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> b
f Map a Int
o)
  mapNode a -> b
f (SimpleTransition Map a Int
o) =
    Map b Int -> SimpleNode b
forall a. Map a Int -> SimpleNode a
SimpleTransition ((a -> b) -> Map a Int -> Map b Int
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> b
f Map a Int
o)

  traverseNode :: forall (f :: * -> *) b a.
(Applicative f, Ord b) =>
(a -> f b) -> SimpleNode a -> f (SimpleNode b)
traverseNode a -> f b
f (SimplePlace Int
s Map a Int
o)    =
    Int -> Map b Int -> SimpleNode b
forall a. Int -> Map a Int -> SimpleNode a
SimplePlace Int
s (Map b Int -> SimpleNode b) -> f (Map b Int) -> f (SimpleNode b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> Map a Int -> f (Map b Int)
forall (f :: * -> *) k2 k1 a.
(Applicative f, Ord k2) =>
(k1 -> f k2) -> Map k1 a -> f (Map k2 a)
traverseKeyMap a -> f b
f Map a Int
o
  traverseNode a -> f b
f (SimpleTransition Map a Int
o) =
    Map b Int -> SimpleNode b
forall a. Map a Int -> SimpleNode a
SimpleTransition (Map b Int -> SimpleNode b) -> f (Map b Int) -> f (SimpleNode b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> Map a Int -> f (Map b Int)
forall (f :: * -> *) k2 k1 a.
(Applicative f, Ord k2) =>
(k1 -> f k2) -> Map k1 a -> f (Map k2 a)
traverseKeyMap a -> f b
f Map a Int
o

{-|
Returns 'Just' the 'initial' tokens of the given node, if it is a place 'PetriNode',
otherwise it returns 'Nothing'.
-}
maybeInitial :: PetriNode n => n a -> Maybe Int
maybeInitial :: forall (n :: * -> *) a. PetriNode n => n a -> Maybe Int
maybeInitial n a
n
  | n a -> Bool
forall a. n a -> Bool
forall (n :: * -> *) a. PetriNode n => n a -> Bool
isPlaceNode n a
n = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ n a -> Int
forall a. n a -> Int
forall (n :: * -> *) a. PetriNode n => n a -> Int
initialTokens n a
n
  | Bool
otherwise     = Maybe Int
forall a. Maybe a
Nothing

{-|
A specific traversal for 'Map's changing the keys rather than values.
That is why, the result requires an 'Ord' instance.
It calls 'traverseKeyAndValueMap' but transforms only the keys.
-}
traverseKeyMap
  :: (Applicative f, Ord k2)
  => (k1 -> f k2) -- ^ transformation on keys
  -> Map k1 a
  -> f (Map k2 a)
traverseKeyMap :: forall (f :: * -> *) k2 k1 a.
(Applicative f, Ord k2) =>
(k1 -> f k2) -> Map k1 a -> f (Map k2 a)
traverseKeyMap k1 -> f k2
f = (k1 -> f k2) -> (a -> f a) -> Map k1 a -> f (Map k2 a)
forall (f :: * -> *) k2 k1 a b.
(Applicative f, Ord k2) =>
(k1 -> f k2) -> (a -> f b) -> Map k1 a -> f (Map k2 b)
traverseKeyAndValueMap k1 -> f k2
f a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

{-|
A specific traversal for 'Map's transforming its keys and its values.
That is why, the result requires an 'Ord' instance on the resulting key values
type.
The traversal happens by inserting every changed key value pair into a new map.
-}
traverseKeyAndValueMap
  :: (Applicative f, Ord k2)
  => (k1 -> f k2) -- ^ transformation function on keys
  -> (a -> f b)   -- ^ transformation function on values
  -> Map k1 a
  -> f (Map k2 b)
traverseKeyAndValueMap :: forall (f :: * -> *) k2 k1 a b.
(Applicative f, Ord k2) =>
(k1 -> f k2) -> (a -> f b) -> Map k1 a -> f (Map k2 b)
traverseKeyAndValueMap k1 -> f k2
f a -> f b
g =
  (k1 -> a -> f (Map k2 b) -> f (Map k2 b))
-> f (Map k2 b) -> Map k1 a -> f (Map k2 b)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey k1 -> a -> f (Map k2 b) -> f (Map k2 b)
insertApplicativeKeyValue (Map k2 b -> f (Map k2 b)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map k2 b
forall k a. Map k a
M.empty)
  where
    insertApplicativeKeyValue :: k1 -> a -> f (Map k2 b) -> f (Map k2 b)
insertApplicativeKeyValue k1
k a
x f (Map k2 b)
rs = k2 -> b -> Map k2 b -> Map k2 b
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (k2 -> b -> Map k2 b -> Map k2 b)
-> f k2 -> f (b -> Map k2 b -> Map k2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> k1 -> f k2
f k1
k f (b -> Map k2 b -> Map k2 b) -> f b -> f (Map k2 b -> Map k2 b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> f b
g a
x f (Map k2 b -> Map k2 b) -> f (Map k2 b) -> f (Map k2 b)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Map k2 b)
rs

class (PetriNode n, Show (p n String)) => Net p n where
  emptyNet :: p n a
  {-|
  Inserts 'flow' into the 'Net' by connecting the provided source and target
  by the given flow.
  If no 'PetriNode' for the given source or target exists within the 'Net'
  no 'flow' is added to the 'Net'
  If 'flow' between source and target exists already it is replaced.
  -}
  alterFlow
    :: Ord a
    => a
    -- ^ source
    -> Int
    -- ^ the flow
    -> a
    -- ^ target
    -> p n a
    -> p n a

  {-|
  Inserts a 'PetriNode' into the 'Net' given the desired key,

   * a place node with the desired initial tokes if Just such are provided,
   * a transition node otherwise.

  If the desired key already exists, the targeted 'PetriNode' is replaced
  without affecting preexisting 'flow'.
  (use 'deleteNode' first if you desire to clear related flow)
  -}
  alterNode
    :: Ord a
    => a
    -- ^ node key
    -> Maybe Int
    -- ^ initial tokens
    -> p n a
    -> p n a

  {-|
  Removes the flow going from the first given key to the second one..
  -}
  deleteFlow        :: Ord a => a -> a -> p n a -> p n a

  {-|
  Removes the 'PetriNode' associated with the key and all connections going
  from or to the removed node.
  -}
  deleteNode        :: Ord a => a -> p n a -> p n a
  flow              :: Ord a => a -> a -> p n a -> Maybe Int
  nodes             :: Ord a => p n a -> Map a (n a)
  outFlow           :: Ord a => a -> p n a -> Map a Int
  mapNet            :: Ord b => (a -> b) -> p n a -> p n b
  traverseNet       :: (Applicative f, Ord b) => (a -> f b) -> p n a -> f (p n b)

updateNode
  :: (Map a Int -> Map b Int)
  -> (Map a Int -> Map b Int)
  -> Node a
  -> Node b
updateNode :: forall a b.
(Map a Int -> Map b Int)
-> (Map a Int -> Map b Int) -> Node a -> Node b
updateNode Map a Int -> Map b Int
g Map a Int -> Map b Int
h (PlaceNode Int
t Map a Int
i Map a Int
o)    = Int -> Map b Int -> Map b Int -> Node b
forall a. Int -> Map a Int -> Map a Int -> Node a
PlaceNode Int
t (Map a Int -> Map b Int
g Map a Int
i) (Map a Int -> Map b Int
h Map a Int
o)
updateNode Map a Int -> Map b Int
g Map a Int -> Map b Int
h (TransitionNode Map a Int
i Map a Int
o) = Map b Int -> Map b Int -> Node b
forall a. Map a Int -> Map a Int -> Node a
TransitionNode (Map a Int -> Map b Int
g Map a Int
i) (Map a Int -> Map b Int
h Map a Int
o)

adjustAll :: Ord a => (b -> b) -> Maybe [a] -> Map a b -> Map a b
adjustAll :: forall a b. Ord a => (b -> b) -> Maybe [a] -> Map a b -> Map a b
adjustAll b -> b
f Maybe [a]
ns Map a b
m = (a -> Map a b -> Map a b) -> Map a b -> [a] -> Map a b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((b -> b) -> a -> Map a b -> Map a b
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust b -> b
f) Map a b
m ([a] -> Map a b) -> [a] -> Map a b
forall a b. (a -> b) -> a -> b
$ Maybe [a] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat Maybe [a]
ns

{-|
A Petri like graph consists of nodes which might have connections between each
other.

The 'PetriLike' graph is a valid Petri net only if

 * 'PlaceNode's are only successors of 'TransitionNode's
 * 'TransitionNode's are only successors of 'PlaceNode's
 * the initial marking is valid (i.e., all initial tokens are nonnegative)
 * every weight is greater than zero
-}
newtype PetriLike n a = PetriLike {
  -- | the 'Map' of all nodes the Petri net like graph is made of
  forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes :: Map a (n a)
  } deriving (Typeable (PetriLike n a)
Typeable (PetriLike n a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> PetriLike n a -> c (PetriLike n a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (PetriLike n a))
-> (PetriLike n a -> Constr)
-> (PetriLike n a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (PetriLike n a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (PetriLike n a)))
-> ((forall b. Data b => b -> b) -> PetriLike n a -> PetriLike n a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PetriLike n a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PetriLike n a -> r)
-> (forall u. (forall d. Data d => d -> u) -> PetriLike n a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> PetriLike n a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> PetriLike n a -> m (PetriLike n a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> PetriLike n a -> m (PetriLike n a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> PetriLike n a -> m (PetriLike n a))
-> Data (PetriLike n a)
PetriLike n a -> Constr
PetriLike n a -> DataType
(forall b. Data b => b -> b) -> PetriLike n a -> PetriLike n a
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PetriLike n a -> u
forall u. (forall d. Data d => d -> u) -> PetriLike n a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PetriLike n a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PetriLike n a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> PetriLike n a -> m (PetriLike n a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PetriLike n a -> m (PetriLike n a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PetriLike n a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PetriLike n a -> c (PetriLike n a)
forall {n :: * -> *} {a}.
(Typeable n, Data a, Data (n a), Ord a) =>
Typeable (PetriLike n a)
forall (n :: * -> *) a.
(Typeable n, Data a, Data (n a), Ord a) =>
PetriLike n a -> Constr
forall (n :: * -> *) a.
(Typeable n, Data a, Data (n a), Ord a) =>
PetriLike n a -> DataType
forall (n :: * -> *) a.
(Typeable n, Data a, Data (n a), Ord a) =>
(forall b. Data b => b -> b) -> PetriLike n a -> PetriLike n a
forall (n :: * -> *) a u.
(Typeable n, Data a, Data (n a), Ord a) =>
Int -> (forall d. Data d => d -> u) -> PetriLike n a -> u
forall (n :: * -> *) a u.
(Typeable n, Data a, Data (n a), Ord a) =>
(forall d. Data d => d -> u) -> PetriLike n a -> [u]
forall (n :: * -> *) a r r'.
(Typeable n, Data a, Data (n a), Ord a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PetriLike n a -> r
forall (n :: * -> *) a r r'.
(Typeable n, Data a, Data (n a), Ord a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PetriLike n a -> r
forall (n :: * -> *) a (m :: * -> *).
(Typeable n, Data a, Data (n a), Ord a, Monad m) =>
(forall d. Data d => d -> m d)
-> PetriLike n a -> m (PetriLike n a)
forall (n :: * -> *) a (m :: * -> *).
(Typeable n, Data a, Data (n a), Ord a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> PetriLike n a -> m (PetriLike n a)
forall (n :: * -> *) a (c :: * -> *).
(Typeable n, Data a, Data (n a), Ord a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PetriLike n a)
forall (n :: * -> *) a (c :: * -> *).
(Typeable n, Data a, Data (n a), Ord a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PetriLike n a -> c (PetriLike n a)
forall (n :: * -> *) a (t :: * -> *) (c :: * -> *).
(Typeable n, Data a, Data (n a), Ord a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PetriLike n a))
forall (n :: * -> *) a (t :: * -> * -> *) (c :: * -> *).
(Typeable n, Data a, Data (n a), Ord a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PetriLike n a))
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (PetriLike n a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PetriLike n a))
$cgfoldl :: forall (n :: * -> *) a (c :: * -> *).
(Typeable n, Data a, Data (n a), Ord a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PetriLike n a -> c (PetriLike n a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PetriLike n a -> c (PetriLike n a)
$cgunfold :: forall (n :: * -> *) a (c :: * -> *).
(Typeable n, Data a, Data (n a), Ord a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PetriLike n a)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PetriLike n a)
$ctoConstr :: forall (n :: * -> *) a.
(Typeable n, Data a, Data (n a), Ord a) =>
PetriLike n a -> Constr
toConstr :: PetriLike n a -> Constr
$cdataTypeOf :: forall (n :: * -> *) a.
(Typeable n, Data a, Data (n a), Ord a) =>
PetriLike n a -> DataType
dataTypeOf :: PetriLike n a -> DataType
$cdataCast1 :: forall (n :: * -> *) a (t :: * -> *) (c :: * -> *).
(Typeable n, Data a, Data (n a), Ord a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PetriLike n a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (PetriLike n a))
$cdataCast2 :: forall (n :: * -> *) a (t :: * -> * -> *) (c :: * -> *).
(Typeable n, Data a, Data (n a), Ord a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PetriLike n a))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PetriLike n a))
$cgmapT :: forall (n :: * -> *) a.
(Typeable n, Data a, Data (n a), Ord a) =>
(forall b. Data b => b -> b) -> PetriLike n a -> PetriLike n a
gmapT :: (forall b. Data b => b -> b) -> PetriLike n a -> PetriLike n a
$cgmapQl :: forall (n :: * -> *) a r r'.
(Typeable n, Data a, Data (n a), Ord a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PetriLike n a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PetriLike n a -> r
$cgmapQr :: forall (n :: * -> *) a r r'.
(Typeable n, Data a, Data (n a), Ord a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PetriLike n a -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PetriLike n a -> r
$cgmapQ :: forall (n :: * -> *) a u.
(Typeable n, Data a, Data (n a), Ord a) =>
(forall d. Data d => d -> u) -> PetriLike n a -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> PetriLike n a -> [u]
$cgmapQi :: forall (n :: * -> *) a u.
(Typeable n, Data a, Data (n a), Ord a) =>
Int -> (forall d. Data d => d -> u) -> PetriLike n a -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PetriLike n a -> u
$cgmapM :: forall (n :: * -> *) a (m :: * -> *).
(Typeable n, Data a, Data (n a), Ord a, Monad m) =>
(forall d. Data d => d -> m d)
-> PetriLike n a -> m (PetriLike n a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> PetriLike n a -> m (PetriLike n a)
$cgmapMp :: forall (n :: * -> *) a (m :: * -> *).
(Typeable n, Data a, Data (n a), Ord a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> PetriLike n a -> m (PetriLike n a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PetriLike n a -> m (PetriLike n a)
$cgmapMo :: forall (n :: * -> *) a (m :: * -> *).
(Typeable n, Data a, Data (n a), Ord a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> PetriLike n a -> m (PetriLike n a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PetriLike n a -> m (PetriLike n a)
Data, PetriLike n a -> PetriLike n a -> Bool
(PetriLike n a -> PetriLike n a -> Bool)
-> (PetriLike n a -> PetriLike n a -> Bool) -> Eq (PetriLike n a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (n :: * -> *) a.
(Eq a, Eq (n a)) =>
PetriLike n a -> PetriLike n a -> Bool
$c== :: forall (n :: * -> *) a.
(Eq a, Eq (n a)) =>
PetriLike n a -> PetriLike n a -> Bool
== :: PetriLike n a -> PetriLike n a -> Bool
$c/= :: forall (n :: * -> *) a.
(Eq a, Eq (n a)) =>
PetriLike n a -> PetriLike n a -> Bool
/= :: PetriLike n a -> PetriLike n a -> Bool
Eq, (forall x. PetriLike n a -> Rep (PetriLike n a) x)
-> (forall x. Rep (PetriLike n a) x -> PetriLike n a)
-> Generic (PetriLike n a)
forall x. Rep (PetriLike n a) x -> PetriLike n a
forall x. PetriLike n a -> Rep (PetriLike n a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (n :: * -> *) a x. Rep (PetriLike n a) x -> PetriLike n a
forall (n :: * -> *) a x. PetriLike n a -> Rep (PetriLike n a) x
$cfrom :: forall (n :: * -> *) a x. PetriLike n a -> Rep (PetriLike n a) x
from :: forall x. PetriLike n a -> Rep (PetriLike n a) x
$cto :: forall (n :: * -> *) a x. Rep (PetriLike n a) x -> PetriLike n a
to :: forall x. Rep (PetriLike n a) x -> PetriLike n a
Generic, ReadPrec [PetriLike n a]
ReadPrec (PetriLike n a)
Int -> ReadS (PetriLike n a)
ReadS [PetriLike n a]
(Int -> ReadS (PetriLike n a))
-> ReadS [PetriLike n a]
-> ReadPrec (PetriLike n a)
-> ReadPrec [PetriLike n a]
-> Read (PetriLike n a)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall (n :: * -> *) a.
(Ord a, Read a, Read (n a)) =>
ReadPrec [PetriLike n a]
forall (n :: * -> *) a.
(Ord a, Read a, Read (n a)) =>
ReadPrec (PetriLike n a)
forall (n :: * -> *) a.
(Ord a, Read a, Read (n a)) =>
Int -> ReadS (PetriLike n a)
forall (n :: * -> *) a.
(Ord a, Read a, Read (n a)) =>
ReadS [PetriLike n a]
$creadsPrec :: forall (n :: * -> *) a.
(Ord a, Read a, Read (n a)) =>
Int -> ReadS (PetriLike n a)
readsPrec :: Int -> ReadS (PetriLike n a)
$creadList :: forall (n :: * -> *) a.
(Ord a, Read a, Read (n a)) =>
ReadS [PetriLike n a]
readList :: ReadS [PetriLike n a]
$creadPrec :: forall (n :: * -> *) a.
(Ord a, Read a, Read (n a)) =>
ReadPrec (PetriLike n a)
readPrec :: ReadPrec (PetriLike n a)
$creadListPrec :: forall (n :: * -> *) a.
(Ord a, Read a, Read (n a)) =>
ReadPrec [PetriLike n a]
readListPrec :: ReadPrec [PetriLike n a]
Read, Int -> PetriLike n a -> ShowS
[PetriLike n a] -> ShowS
PetriLike n a -> String
(Int -> PetriLike n a -> ShowS)
-> (PetriLike n a -> String)
-> ([PetriLike n a] -> ShowS)
-> Show (PetriLike n a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: * -> *) a.
(Show a, Show (n a)) =>
Int -> PetriLike n a -> ShowS
forall (n :: * -> *) a.
(Show a, Show (n a)) =>
[PetriLike n a] -> ShowS
forall (n :: * -> *) a.
(Show a, Show (n a)) =>
PetriLike n a -> String
$cshowsPrec :: forall (n :: * -> *) a.
(Show a, Show (n a)) =>
Int -> PetriLike n a -> ShowS
showsPrec :: Int -> PetriLike n a -> ShowS
$cshow :: forall (n :: * -> *) a.
(Show a, Show (n a)) =>
PetriLike n a -> String
show :: PetriLike n a -> String
$cshowList :: forall (n :: * -> *) a.
(Show a, Show (n a)) =>
[PetriLike n a] -> ShowS
showList :: [PetriLike n a] -> ShowS
Show)

instance Net PetriLike Node where
  emptyNet :: forall a. PetriLike Node a
emptyNet = Map a (Node a) -> PetriLike Node a
forall (n :: * -> *) a. Map a (n a) -> PetriLike n a
PetriLike Map a (Node a)
forall k a. Map k a
M.empty

  flow :: forall a. Ord a => a -> a -> PetriLike Node a -> Maybe Int
flow a
x a
y = (a -> Map a Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
y (Map a Int -> Maybe Int)
-> (Node a -> Map a Int) -> Node a -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node a -> Map a Int
forall a. Node a -> Map a Int
flowOutN) (Node a -> Maybe Int)
-> (PetriLike Node a -> Maybe (Node a))
-> PetriLike Node a
-> Maybe Int
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (a -> Map a (Node a) -> Maybe (Node a)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
x (Map a (Node a) -> Maybe (Node a))
-> (PetriLike Node a -> Map a (Node a))
-> PetriLike Node a
-> Maybe (Node a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriLike Node a -> Map a (Node a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes)

  nodes :: forall a. Ord a => PetriLike Node a -> Map a (Node a)
nodes = PetriLike Node a -> Map a (Node a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes

  deleteFlow :: forall a. Ord a => a -> a -> PetriLike Node a -> PetriLike Node a
deleteFlow a
x a
y (PetriLike Map a (Node a)
ns) = Map a (Node a) -> PetriLike Node a
forall (n :: * -> *) a. Map a (n a) -> PetriLike n a
PetriLike
    (Map a (Node a) -> PetriLike Node a)
-> (Map a (Node a) -> Map a (Node a))
-> Map a (Node a)
-> PetriLike Node a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Node a -> Node a) -> a -> Map a (Node a) -> Map a (Node a)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust ((Map a Int -> Map a Int)
-> (Map a Int -> Map a Int) -> Node a -> Node a
forall a b.
(Map a Int -> Map b Int)
-> (Map a Int -> Map b Int) -> Node a -> Node b
updateNode Map a Int -> Map a Int
forall a. a -> a
id (a -> Map a Int -> Map a Int
forall k a. Ord k => k -> Map k a -> Map k a
M.delete a
y)) a
x
    (Map a (Node a) -> Map a (Node a))
-> (Map a (Node a) -> Map a (Node a))
-> Map a (Node a)
-> Map a (Node a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Node a -> Node a) -> a -> Map a (Node a) -> Map a (Node a)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust ((Map a Int -> Map a Int)
-> (Map a Int -> Map a Int) -> Node a -> Node a
forall a b.
(Map a Int -> Map b Int)
-> (Map a Int -> Map b Int) -> Node a -> Node b
updateNode (a -> Map a Int -> Map a Int
forall k a. Ord k => k -> Map k a -> Map k a
M.delete a
x) Map a Int -> Map a Int
forall a. a -> a
id) a
y
    (Map a (Node a) -> PetriLike Node a)
-> Map a (Node a) -> PetriLike Node a
forall a b. (a -> b) -> a -> b
$ Map a (Node a)
ns

  deleteNode :: forall a. Ord a => a -> PetriLike Node a -> PetriLike Node a
deleteNode a
x (PetriLike Map a (Node a)
ns) = Map a (Node a) -> PetriLike Node a
forall (n :: * -> *) a. Map a (n a) -> PetriLike n a
PetriLike
    (Map a (Node a) -> PetriLike Node a)
-> (Map a (Node a) -> Map a (Node a))
-> Map a (Node a)
-> PetriLike Node a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Node a -> Node a) -> Maybe [a] -> Map a (Node a) -> Map a (Node a)
forall a b. Ord a => (b -> b) -> Maybe [a] -> Map a b -> Map a b
adjustAll ((Map a Int -> Map a Int)
-> (Map a Int -> Map a Int) -> Node a -> Node a
forall a b.
(Map a Int -> Map b Int)
-> (Map a Int -> Map b Int) -> Node a -> Node b
updateNode Map a Int -> Map a Int
forall a. a -> a
id (a -> Map a Int -> Map a Int
forall k a. Ord k => k -> Map k a -> Map k a
M.delete a
x)) (Map a Int -> [a]
forall k a. Map k a -> [k]
M.keys (Map a Int -> [a]) -> (Node a -> Map a Int) -> Node a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node a -> Map a Int
forall a. Node a -> Map a Int
flowIn (Node a -> [a]) -> Maybe (Node a) -> Maybe [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Node a)
n)
    (Map a (Node a) -> Map a (Node a))
-> (Map a (Node a) -> Map a (Node a))
-> Map a (Node a)
-> Map a (Node a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Node a -> Node a) -> Maybe [a] -> Map a (Node a) -> Map a (Node a)
forall a b. Ord a => (b -> b) -> Maybe [a] -> Map a b -> Map a b
adjustAll ((Map a Int -> Map a Int)
-> (Map a Int -> Map a Int) -> Node a -> Node a
forall a b.
(Map a Int -> Map b Int)
-> (Map a Int -> Map b Int) -> Node a -> Node b
updateNode (a -> Map a Int -> Map a Int
forall k a. Ord k => k -> Map k a -> Map k a
M.delete a
x) Map a Int -> Map a Int
forall a. a -> a
id) (Map a Int -> [a]
forall k a. Map k a -> [k]
M.keys (Map a Int -> [a]) -> (Node a -> Map a Int) -> Node a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node a -> Map a Int
forall a. Node a -> Map a Int
flowOutN (Node a -> [a]) -> Maybe (Node a) -> Maybe [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Node a)
n)
    (Map a (Node a) -> Map a (Node a))
-> (Map a (Node a) -> Map a (Node a))
-> Map a (Node a)
-> Map a (Node a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Map a (Node a) -> Map a (Node a)
forall k a. Ord k => k -> Map k a -> Map k a
M.delete a
x
    (Map a (Node a) -> PetriLike Node a)
-> Map a (Node a) -> PetriLike Node a
forall a b. (a -> b) -> a -> b
$ Map a (Node a)
ns
    where
      n :: Maybe (Node a)
n = a -> Map a (Node a) -> Maybe (Node a)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
x Map a (Node a)
ns

  alterFlow :: forall a.
Ord a =>
a -> Int -> a -> PetriLike Node a -> PetriLike Node a
alterFlow a
x Int
f a
y = Map a (Node a) -> PetriLike Node a
forall (n :: * -> *) a. Map a (n a) -> PetriLike n a
PetriLike
    (Map a (Node a) -> PetriLike Node a)
-> (PetriLike Node a -> Map a (Node a))
-> PetriLike Node a
-> PetriLike Node a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Node a -> Node a) -> a -> Map a (Node a) -> Map a (Node a)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust ((Map a Int -> Map a Int)
-> (Map a Int -> Map a Int) -> Node a -> Node a
forall a b.
(Map a Int -> Map b Int)
-> (Map a Int -> Map b Int) -> Node a -> Node b
updateNode Map a Int -> Map a Int
forall a. a -> a
id (a -> Int -> Map a Int -> Map a Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert a
y Int
f)) a
x
    (Map a (Node a) -> Map a (Node a))
-> (PetriLike Node a -> Map a (Node a))
-> PetriLike Node a
-> Map a (Node a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Node a -> Node a) -> a -> Map a (Node a) -> Map a (Node a)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust ((Map a Int -> Map a Int)
-> (Map a Int -> Map a Int) -> Node a -> Node a
forall a b.
(Map a Int -> Map b Int)
-> (Map a Int -> Map b Int) -> Node a -> Node b
updateNode (a -> Int -> Map a Int -> Map a Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert a
x Int
f) Map a Int -> Map a Int
forall a. a -> a
id) a
y
    (Map a (Node a) -> Map a (Node a))
-> (PetriLike Node a -> Map a (Node a))
-> PetriLike Node a
-> Map a (Node a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriLike Node a -> Map a (Node a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes

  alterNode :: forall a.
Ord a =>
a -> Maybe Int -> PetriLike Node a -> PetriLike Node a
alterNode a
x Maybe Int
mt = Map a (Node a) -> PetriLike Node a
forall (n :: * -> *) a. Map a (n a) -> PetriLike n a
PetriLike (Map a (Node a) -> PetriLike Node a)
-> (PetriLike Node a -> Map a (Node a))
-> PetriLike Node a
-> PetriLike Node a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe (Node a) -> Maybe (Node a))
-> a -> Map a (Node a) -> Map a (Node a)
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
M.alter Maybe (Node a) -> Maybe (Node a)
forall {a}. Maybe (Node a) -> Maybe (Node a)
alterNode' a
x (Map a (Node a) -> Map a (Node a))
-> (PetriLike Node a -> Map a (Node a))
-> PetriLike Node a
-> Map a (Node a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriLike Node a -> Map a (Node a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes
    where
      alterNode' :: Maybe (Node a) -> Maybe (Node a)
alterNode' = Node a -> Maybe (Node a)
forall a. a -> Maybe a
Just (Node a -> Maybe (Node a))
-> (Maybe (Node a) -> Node a) -> Maybe (Node a) -> Maybe (Node a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node a -> Maybe (Node a) -> Node a
forall a. a -> Maybe a -> a
fromMaybe
        ((Map a Int -> Map a Int -> Node a)
-> (Int -> Map a Int -> Map a Int -> Node a)
-> Maybe Int
-> Map a Int
-> Map a Int
-> Node a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Map a Int -> Map a Int -> Node a
forall a. Map a Int -> Map a Int -> Node a
TransitionNode Int -> Map a Int -> Map a Int -> Node a
forall a. Int -> Map a Int -> Map a Int -> Node a
PlaceNode Maybe Int
mt Map a Int
forall k a. Map k a
M.empty Map a Int
forall k a. Map k a
M.empty)

  outFlow :: forall a. Ord a => a -> PetriLike Node a -> Map a Int
outFlow a
x = Map a Int -> (Node a -> Map a Int) -> Maybe (Node a) -> Map a Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Map a Int
forall k a. Map k a
M.empty Node a -> Map a Int
forall a. Node a -> Map a Int
flowOutN (Maybe (Node a) -> Map a Int)
-> (PetriLike Node a -> Maybe (Node a))
-> PetriLike Node a
-> Map a Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Map a (Node a) -> Maybe (Node a)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
x (Map a (Node a) -> Maybe (Node a))
-> (PetriLike Node a -> Map a (Node a))
-> PetriLike Node a
-> Maybe (Node a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriLike Node a -> Map a (Node a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes

  mapNet :: forall b a.
Ord b =>
(a -> b) -> PetriLike Node a -> PetriLike Node b
mapNet = (a -> b) -> PetriLike Node a -> PetriLike Node b
forall b (n :: * -> *) a.
(Ord b, PetriNode n) =>
(a -> b) -> PetriLike n a -> PetriLike n b
mapPetriLike
  traverseNet :: forall (f :: * -> *) b a.
(Applicative f, Ord b) =>
(a -> f b) -> PetriLike Node a -> f (PetriLike Node b)
traverseNet = (a -> f b) -> PetriLike Node a -> f (PetriLike Node b)
forall (f :: * -> *) b (n :: * -> *) a.
(Applicative f, Ord b, PetriNode n) =>
(a -> f b) -> PetriLike n a -> f (PetriLike n b)
traversePetriLike

flowOutN :: Node a -> Map a Int
flowOutN :: forall a. Node a -> Map a Int
flowOutN PlaceNode {Map a Int
flowOut :: forall a. Node a -> Map a Int
flowOut :: Map a Int
flowOut} = Map a Int
flowOut
flowOutN TransitionNode {Map a Int
flowOut :: forall a. Node a -> Map a Int
flowOut :: Map a Int
flowOut} = Map a Int
flowOut

instance Net PetriLike SimpleNode where
  emptyNet :: forall a. PetriLike SimpleNode a
emptyNet = Map a (SimpleNode a) -> PetriLike SimpleNode a
forall (n :: * -> *) a. Map a (n a) -> PetriLike n a
PetriLike Map a (SimpleNode a)
forall k a. Map k a
M.empty

  flow :: forall a. Ord a => a -> a -> PetriLike SimpleNode a -> Maybe Int
flow a
x a
y = (a -> Map a Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
y (Map a Int -> Maybe Int)
-> (SimpleNode a -> Map a Int) -> SimpleNode a -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleNode a -> Map a Int
forall a. SimpleNode a -> Map a Int
flowOutSN) (SimpleNode a -> Maybe Int)
-> (PetriLike SimpleNode a -> Maybe (SimpleNode a))
-> PetriLike SimpleNode a
-> Maybe Int
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (a -> Map a (SimpleNode a) -> Maybe (SimpleNode a)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
x (Map a (SimpleNode a) -> Maybe (SimpleNode a))
-> (PetriLike SimpleNode a -> Map a (SimpleNode a))
-> PetriLike SimpleNode a
-> Maybe (SimpleNode a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriLike SimpleNode a -> Map a (SimpleNode a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes)

  nodes :: forall a. Ord a => PetriLike SimpleNode a -> Map a (SimpleNode a)
nodes = PetriLike SimpleNode a -> Map a (SimpleNode a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes

  deleteFlow :: forall a.
Ord a =>
a -> a -> PetriLike SimpleNode a -> PetriLike SimpleNode a
deleteFlow a
x a
y (PetriLike Map a (SimpleNode a)
ns) = Map a (SimpleNode a) -> PetriLike SimpleNode a
forall (n :: * -> *) a. Map a (n a) -> PetriLike n a
PetriLike
    (Map a (SimpleNode a) -> PetriLike SimpleNode a)
-> (Map a (SimpleNode a) -> Map a (SimpleNode a))
-> Map a (SimpleNode a)
-> PetriLike SimpleNode a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleNode a -> SimpleNode a)
-> a -> Map a (SimpleNode a) -> Map a (SimpleNode a)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust ((Map a Int -> Map a Int) -> SimpleNode a -> SimpleNode a
forall a b.
(Map a Int -> Map b Int) -> SimpleNode a -> SimpleNode b
updateSimpleNode (a -> Map a Int -> Map a Int
forall k a. Ord k => k -> Map k a -> Map k a
M.delete a
y)) a
x
    (Map a (SimpleNode a) -> PetriLike SimpleNode a)
-> Map a (SimpleNode a) -> PetriLike SimpleNode a
forall a b. (a -> b) -> a -> b
$ Map a (SimpleNode a)
ns

  deleteNode :: forall a.
Ord a =>
a -> PetriLike SimpleNode a -> PetriLike SimpleNode a
deleteNode a
x PetriLike SimpleNode a
ns = Map a (SimpleNode a) -> PetriLike SimpleNode a
forall (n :: * -> *) a. Map a (n a) -> PetriLike n a
PetriLike
    (Map a (SimpleNode a) -> PetriLike SimpleNode a)
-> (PetriLike SimpleNode a -> Map a (SimpleNode a))
-> PetriLike SimpleNode a
-> PetriLike SimpleNode a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleNode a -> SimpleNode a)
-> Maybe [a] -> Map a (SimpleNode a) -> Map a (SimpleNode a)
forall a b. Ord a => (b -> b) -> Maybe [a] -> Map a b -> Map a b
adjustAll ((Map a Int -> Map a Int) -> SimpleNode a -> SimpleNode a
forall a b.
(Map a Int -> Map b Int) -> SimpleNode a -> SimpleNode b
updateSimpleNode ((Map a Int -> Map a Int) -> SimpleNode a -> SimpleNode a)
-> (Map a Int -> Map a Int) -> SimpleNode a -> SimpleNode a
forall a b. (a -> b) -> a -> b
$ a -> Map a Int -> Map a Int
forall k a. Ord k => k -> Map k a -> Map k a
M.delete a
x) ([a] -> Maybe [a]
forall a. a -> Maybe a
Just ([a] -> Maybe [a]) -> [a] -> Maybe [a]
forall a b. (a -> b) -> a -> b
$ Map a (SimpleNode a) -> [a]
forall k a. Map k a -> [k]
M.keys (Map a (SimpleNode a) -> [a]) -> Map a (SimpleNode a) -> [a]
forall a b. (a -> b) -> a -> b
$ PetriLike SimpleNode a -> Map a (SimpleNode a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes PetriLike SimpleNode a
ns)
    (Map a (SimpleNode a) -> Map a (SimpleNode a))
-> (PetriLike SimpleNode a -> Map a (SimpleNode a))
-> PetriLike SimpleNode a
-> Map a (SimpleNode a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Map a (SimpleNode a) -> Map a (SimpleNode a)
forall k a. Ord k => k -> Map k a -> Map k a
M.delete a
x
    (Map a (SimpleNode a) -> Map a (SimpleNode a))
-> (PetriLike SimpleNode a -> Map a (SimpleNode a))
-> PetriLike SimpleNode a
-> Map a (SimpleNode a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriLike SimpleNode a -> Map a (SimpleNode a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes
    (PetriLike SimpleNode a -> PetriLike SimpleNode a)
-> PetriLike SimpleNode a -> PetriLike SimpleNode a
forall a b. (a -> b) -> a -> b
$ PetriLike SimpleNode a
ns

  alterFlow :: forall a.
Ord a =>
a -> Int -> a -> PetriLike SimpleNode a -> PetriLike SimpleNode a
alterFlow a
x Int
f a
y = Map a (SimpleNode a) -> PetriLike SimpleNode a
forall (n :: * -> *) a. Map a (n a) -> PetriLike n a
PetriLike
    (Map a (SimpleNode a) -> PetriLike SimpleNode a)
-> (PetriLike SimpleNode a -> Map a (SimpleNode a))
-> PetriLike SimpleNode a
-> PetriLike SimpleNode a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleNode a -> SimpleNode a)
-> a -> Map a (SimpleNode a) -> Map a (SimpleNode a)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
M.adjust ((Map a Int -> Map a Int) -> SimpleNode a -> SimpleNode a
forall a b.
(Map a Int -> Map b Int) -> SimpleNode a -> SimpleNode b
updateSimpleNode (a -> Int -> Map a Int -> Map a Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert a
y Int
f)) a
x
    (Map a (SimpleNode a) -> Map a (SimpleNode a))
-> (PetriLike SimpleNode a -> Map a (SimpleNode a))
-> PetriLike SimpleNode a
-> Map a (SimpleNode a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriLike SimpleNode a -> Map a (SimpleNode a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes

  alterNode :: forall a.
Ord a =>
a -> Maybe Int -> PetriLike SimpleNode a -> PetriLike SimpleNode a
alterNode a
x Maybe Int
mt = Map a (SimpleNode a) -> PetriLike SimpleNode a
forall (n :: * -> *) a. Map a (n a) -> PetriLike n a
PetriLike (Map a (SimpleNode a) -> PetriLike SimpleNode a)
-> (PetriLike SimpleNode a -> Map a (SimpleNode a))
-> PetriLike SimpleNode a
-> PetriLike SimpleNode a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe (SimpleNode a) -> Maybe (SimpleNode a))
-> a -> Map a (SimpleNode a) -> Map a (SimpleNode a)
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
M.alter Maybe (SimpleNode a) -> Maybe (SimpleNode a)
forall {a}. Maybe (SimpleNode a) -> Maybe (SimpleNode a)
alterNode' a
x (Map a (SimpleNode a) -> Map a (SimpleNode a))
-> (PetriLike SimpleNode a -> Map a (SimpleNode a))
-> PetriLike SimpleNode a
-> Map a (SimpleNode a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriLike SimpleNode a -> Map a (SimpleNode a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes
    where
      alterNode' :: Maybe (SimpleNode a) -> Maybe (SimpleNode a)
alterNode' = SimpleNode a -> Maybe (SimpleNode a)
forall a. a -> Maybe a
Just (SimpleNode a -> Maybe (SimpleNode a))
-> (Maybe (SimpleNode a) -> SimpleNode a)
-> Maybe (SimpleNode a)
-> Maybe (SimpleNode a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleNode a -> Maybe (SimpleNode a) -> SimpleNode a
forall a. a -> Maybe a -> a
fromMaybe
        ((Map a Int -> SimpleNode a)
-> (Int -> Map a Int -> SimpleNode a)
-> Maybe Int
-> Map a Int
-> SimpleNode a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Map a Int -> SimpleNode a
forall a. Map a Int -> SimpleNode a
SimpleTransition Int -> Map a Int -> SimpleNode a
forall a. Int -> Map a Int -> SimpleNode a
SimplePlace Maybe Int
mt Map a Int
forall k a. Map k a
M.empty)

  outFlow :: forall a. Ord a => a -> PetriLike SimpleNode a -> Map a Int
outFlow a
x = Map a Int
-> (SimpleNode a -> Map a Int) -> Maybe (SimpleNode a) -> Map a Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Map a Int
forall k a. Map k a
M.empty SimpleNode a -> Map a Int
forall a. SimpleNode a -> Map a Int
flowOutSN (Maybe (SimpleNode a) -> Map a Int)
-> (PetriLike SimpleNode a -> Maybe (SimpleNode a))
-> PetriLike SimpleNode a
-> Map a Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Map a (SimpleNode a) -> Maybe (SimpleNode a)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
x (Map a (SimpleNode a) -> Maybe (SimpleNode a))
-> (PetriLike SimpleNode a -> Map a (SimpleNode a))
-> PetriLike SimpleNode a
-> Maybe (SimpleNode a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriLike SimpleNode a -> Map a (SimpleNode a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes

  mapNet :: forall b a.
Ord b =>
(a -> b) -> PetriLike SimpleNode a -> PetriLike SimpleNode b
mapNet = (a -> b) -> PetriLike SimpleNode a -> PetriLike SimpleNode b
forall b (n :: * -> *) a.
(Ord b, PetriNode n) =>
(a -> b) -> PetriLike n a -> PetriLike n b
mapPetriLike
  traverseNet :: forall (f :: * -> *) b a.
(Applicative f, Ord b) =>
(a -> f b) -> PetriLike SimpleNode a -> f (PetriLike SimpleNode b)
traverseNet = (a -> f b) -> PetriLike SimpleNode a -> f (PetriLike SimpleNode b)
forall (f :: * -> *) b (n :: * -> *) a.
(Applicative f, Ord b, PetriNode n) =>
(a -> f b) -> PetriLike n a -> f (PetriLike n b)
traversePetriLike

flowOutSN :: SimpleNode a -> Map a Int
flowOutSN :: forall a. SimpleNode a -> Map a Int
flowOutSN SimplePlace {Map a Int
flowOut :: forall a. SimpleNode a -> Map a Int
flowOut :: Map a Int
flowOut} = Map a Int
flowOut
flowOutSN SimpleTransition {Map a Int
flowOut :: forall a. SimpleNode a -> Map a Int
flowOut :: Map a Int
flowOut} = Map a Int
flowOut

updateSimpleNode :: (Map a Int -> Map b Int) -> SimpleNode a -> SimpleNode b
updateSimpleNode :: forall a b.
(Map a Int -> Map b Int) -> SimpleNode a -> SimpleNode b
updateSimpleNode Map a Int -> Map b Int
g (SimplePlace Int
t Map a Int
o)    = Int -> Map b Int -> SimpleNode b
forall a. Int -> Map a Int -> SimpleNode a
SimplePlace Int
t (Map a Int -> Map b Int
g Map a Int
o)
updateSimpleNode Map a Int -> Map b Int
g (SimpleTransition Map a Int
o) = Map b Int -> SimpleNode b
forall a. Map a Int -> SimpleNode a
SimpleTransition (Map a Int -> Map b Int
g Map a Int
o)

type SimplePetriLike = PetriLike SimpleNode
type SimplePetriNet = SimplePetriLike String

{-|
A 'Functor' like 'fmap' on 'PetriLike'.

Note that 'PetriLike' is not a true 'Functor' as it requires the resulting type
to be an instance of 'Ord', because it uses 'M.mapKeys' in order to apply the
mapping on internal keys.

Thus, the user of 'mapPetriLike' is responsible to preserve uniqueness of values
(otherwise values might be lost after applying the mapping). Furthermore, if the
transformation is not order-preserving, the order of keys within 'Map's might
be changed.
-}
mapPetriLike
  :: (Ord b, PetriNode n)
  => (a -> b)
  -> PetriLike n a
  -> PetriLike n b
mapPetriLike :: forall b (n :: * -> *) a.
(Ord b, PetriNode n) =>
(a -> b) -> PetriLike n a -> PetriLike n b
mapPetriLike a -> b
f PetriLike n a
x = Map b (n b) -> PetriLike n b
forall (n :: * -> *) a. Map a (n a) -> PetriLike n a
PetriLike (Map b (n b) -> PetriLike n b) -> Map b (n b) -> PetriLike n b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> Map a (n b) -> Map b (n b)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> b
f (Map a (n b) -> Map b (n b)) -> Map a (n b) -> Map b (n b)
forall a b. (a -> b) -> a -> b
$ (a -> b) -> n a -> n b
forall b a. Ord b => (a -> b) -> n a -> n b
forall (n :: * -> *) b a.
(PetriNode n, Ord b) =>
(a -> b) -> n a -> n b
mapNode a -> b
f (n a -> n b) -> Map a (n a) -> Map a (n b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PetriLike n a -> Map a (n a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes PetriLike n a
x

{-|
A 'Traversable' like 'traverse' on 'PetriLike'.

Note that 'PetriLike' is not a true 'Traversable' as it requires the resulting
type to be an instance of 'Ord', because it uses 'traverseKeyAndValueMap' which
requires this constraint due to changing keys of 'Map's.

Thus, the user is responsible to preserve uniqueness of keys.
Furthermore, the order of keys might be changed if the transformation is not
order-preserving.
-}
traversePetriLike
  :: (Applicative f, Ord b, PetriNode n)
  => (a -> f b)
  -> PetriLike n a
  -> f (PetriLike n b)
traversePetriLike :: forall (f :: * -> *) b (n :: * -> *) a.
(Applicative f, Ord b, PetriNode n) =>
(a -> f b) -> PetriLike n a -> f (PetriLike n b)
traversePetriLike a -> f b
f PetriLike n a
x =
  Map b (n b) -> PetriLike n b
forall (n :: * -> *) a. Map a (n a) -> PetriLike n a
PetriLike (Map b (n b) -> PetriLike n b)
-> f (Map b (n b)) -> f (PetriLike n b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> (n a -> f (n b)) -> Map a (n a) -> f (Map b (n b))
forall (f :: * -> *) k2 k1 a b.
(Applicative f, Ord k2) =>
(k1 -> f k2) -> (a -> f b) -> Map k1 a -> f (Map k2 b)
traverseKeyAndValueMap a -> f b
f ((a -> f b) -> n a -> f (n b)
forall (n :: * -> *) (f :: * -> *) b a.
(PetriNode n, Applicative f, Ord b) =>
(a -> f b) -> n a -> f (n b)
forall (f :: * -> *) b a.
(Applicative f, Ord b) =>
(a -> f b) -> n a -> f (n b)
traverseNode a -> f b
f) (PetriLike n a -> Map a (n a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes PetriLike n a
x)

transitionNames :: (Net p n, Ord k) => p n k -> [k]
transitionNames :: forall (p :: (* -> *) -> * -> *) (n :: * -> *) k.
(Net p n, Ord k) =>
p n k -> [k]
transitionNames = Map k (n k) -> [k]
forall k a. Map k a -> [k]
M.keys (Map k (n k) -> [k]) -> (p n k -> Map k (n k)) -> p n k -> [k]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n k -> Bool) -> Map k (n k) -> Map k (n k)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter n k -> Bool
forall a. n a -> Bool
forall (n :: * -> *) a. PetriNode n => n a -> Bool
isTransitionNode (Map k (n k) -> Map k (n k))
-> (p n k -> Map k (n k)) -> p n k -> Map k (n k)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p n k -> Map k (n k)
forall a. Ord a => p n a -> Map a (n a)
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
p n a -> Map a (n a)
nodes

placeNames :: (Net p n, Ord k) => p n k -> [k]
placeNames :: forall (p :: (* -> *) -> * -> *) (n :: * -> *) k.
(Net p n, Ord k) =>
p n k -> [k]
placeNames = Map k (n k) -> [k]
forall k a. Map k a -> [k]
M.keys (Map k (n k) -> [k]) -> (p n k -> Map k (n k)) -> p n k -> [k]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n k -> Bool) -> Map k (n k) -> Map k (n k)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter n k -> Bool
forall a. n a -> Bool
forall (n :: * -> *) a. PetriNode n => n a -> Bool
isPlaceNode (Map k (n k) -> Map k (n k))
-> (p n k -> Map k (n k)) -> p n k -> Map k (n k)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p n k -> Map k (n k)
forall a. Ord a => p n a -> Map a (n a)
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
p n a -> Map a (n a)
nodes

shuffleNames
  :: (MonadThrow m, Net p n, Ord a, RandomGen g)
  => p n a
  -> RandT g m (p n a, Bimap a a)
shuffleNames :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) a g.
(MonadThrow m, Net p n, Ord a, RandomGen g) =>
p n a -> RandT g m (p n a, Bimap a a)
shuffleNames p n a
pl = do
  let ts :: [a]
ts = p n a -> [a]
forall (p :: (* -> *) -> * -> *) (n :: * -> *) k.
(Net p n, Ord k) =>
p n k -> [k]
transitionNames p n a
pl
      ps :: [a]
ps = p n a -> [a]
forall (p :: (* -> *) -> * -> *) (n :: * -> *) k.
(Net p n, Ord k) =>
p n k -> [k]
placeNames p n a
pl
  [a]
ts' <- [a] -> RandT g m [a]
forall (m :: * -> *) a. MonadRandom m => [a] -> m [a]
shuffleM [a]
ts
  [a]
ps' <- [a] -> RandT g m [a]
forall (m :: * -> *) a. MonadRandom m => [a] -> m [a]
shuffleM [a]
ps
  let mapping :: Bimap a a
mapping = [(a, a)] -> Bimap a a
forall a b. (Ord a, Ord b) => [(a, b)] -> Bimap a b
BM.fromList ([(a, a)] -> Bimap a a) -> [(a, a)] -> Bimap a a
forall a b. (a -> b) -> a -> b
$ [a] -> [a] -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([a]
ps [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
ts) ([a]
ps' [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
ts')
  m (p n a, Bimap a a) -> RandT g m (p n a, Bimap a a)
forall (m :: * -> *) a. Monad m => m a -> RandT g m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (p n a, Bimap a a) -> RandT g m (p n a, Bimap a a))
-> m (p n a, Bimap a a) -> RandT g m (p n a, Bimap a a)
forall a b. (a -> b) -> a -> b
$ (,Bimap a a
mapping) (p n a -> (p n a, Bimap a a)) -> m (p n a) -> m (p n a, Bimap a a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> m a) -> p n a -> m (p n a)
forall (f :: * -> *) b a.
(Applicative f, Ord b) =>
(a -> f b) -> p n a -> f (p n b)
forall (p :: (* -> *) -> * -> *) (n :: * -> *) (f :: * -> *) b a.
(Net p n, Applicative f, Ord b) =>
(a -> f b) -> p n a -> f (p n b)
traverseNet (a -> Bimap a a -> m a
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
a -> Bimap a b -> m b
`BM.lookup` Bimap a a
mapping) p n a
pl

transformNet
  :: (Net p n, Net p' n', Ord a)
  => p n a
  -> p' n' a
transformNet :: forall (p :: (* -> *) -> * -> *) (n :: * -> *)
       (p' :: (* -> *) -> * -> *) (n' :: * -> *) a.
(Net p n, Net p' n', Ord a) =>
p n a -> p' n' a
transformNet p n a
ns =
  (p' n' a -> [a] -> p' n' a) -> [a] -> p' n' a -> p' n' a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> p' n' a -> p' n' a) -> p' n' a -> [a] -> p' n' a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> p' n' a -> p' n' a
forall {p :: (* -> *) -> * -> *} {n :: * -> *}.
Net p n =>
a -> p n a -> p n a
insertFlows) (Map a (n a) -> [a]
forall k a. Map k a -> [k]
M.keys Map a (n a)
ns')
  (p' n' a -> p' n' a) -> p' n' a -> p' n' a
forall a b. (a -> b) -> a -> b
$ (a -> n a -> p' n' a -> p' n' a)
-> p' n' a -> Map a (n a) -> p' n' a
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey a -> n a -> p' n' a -> p' n' a
forall {p :: (* -> *) -> * -> *} {n :: * -> *} {a} {n :: * -> *}
       {a}.
(Net p n, Ord a, PetriNode n) =>
a -> n a -> p n a -> p n a
fromSimpleNode p' n' a
forall a. p' n' a
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a. Net p n => p n a
emptyNet Map a (n a)
ns'
  where
    ns' :: Map a (n a)
ns' = p n a -> Map a (n a)
forall a. Ord a => p n a -> Map a (n a)
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
p n a -> Map a (n a)
nodes p n a
ns
    insertFlows :: a -> p n a -> p n a
insertFlows a
k p n a
xs = (a -> Int -> p n a -> p n a) -> p n a -> Map a Int -> p n a
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey ((Int -> a -> p n a -> p n a) -> a -> Int -> p n a -> p n a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> Int -> a -> p n a -> p n a
forall a. Ord a => a -> Int -> a -> p n a -> p n a
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
a -> Int -> a -> p n a -> p n a
alterFlow a
k)) p n a
xs (a -> p n a -> Map a Int
forall a. Ord a => a -> p n a -> Map a Int
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
a -> p n a -> Map a Int
outFlow a
k p n a
ns)
    fromSimpleNode :: a -> n a -> p n a -> p n a
fromSimpleNode a
k n a
n = a -> Maybe Int -> p n a -> p n a
forall a. Ord a => a -> Maybe Int -> p n a -> p n a
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
a -> Maybe Int -> p n a -> p n a
alterNode a
k (n a -> Maybe Int
forall (n :: * -> *) a. PetriNode n => n a -> Maybe Int
maybeInitial n a
n)

data InvalidPetriNetException
  = FlowFromATransitionIsZeroOrLess
  | FlowToATransitionIsZeroOrLess
  | PlaceWithNegativeTokenNumber
  | RelatedNodesOfPlacesContainPlaces
  | RelatedNodesOfTransitionsContainTransitions
  deriving Int -> InvalidPetriNetException -> ShowS
[InvalidPetriNetException] -> ShowS
InvalidPetriNetException -> String
(Int -> InvalidPetriNetException -> ShowS)
-> (InvalidPetriNetException -> String)
-> ([InvalidPetriNetException] -> ShowS)
-> Show InvalidPetriNetException
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> InvalidPetriNetException -> ShowS
showsPrec :: Int -> InvalidPetriNetException -> ShowS
$cshow :: InvalidPetriNetException -> String
show :: InvalidPetriNetException -> String
$cshowList :: [InvalidPetriNetException] -> ShowS
showList :: [InvalidPetriNetException] -> ShowS
Show

instance Exception InvalidPetriNetException

{-|
Transform a 'PetriLike' graph into a 'Petri' net.
It first checks if the given Petri net like graph is indeed a valid Petri net
(see also 'PetriLike'),

* if it is, the Petri net like graph is transformed into a Petri net by
  eliminating references to names of places and transitions at all.
  Instead 'initialMarking' is given by a list (where each position represents
  different places) and transitions ('trans') are given by a lists of token
  change (where, again, each position represents a different place, but the same
  index within 'initialMarking' and 'trans' represents the same place).
* if it is not, an exception is thrown indicating the reason why the given
  Petri net like graph is not a valid Petri net.
-}
petriLikeToPetri :: (MonadThrow m, Ord a) => PetriLike Node a -> m Petri
petriLikeToPetri :: forall (m :: * -> *) a.
(MonadThrow m, Ord a) =>
PetriLike Node a -> m Petri
petriLikeToPetri PetriLike Node a
p = do
  m ()
isValid
  Petri -> m Petri
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Petri -> m Petri) -> Petri -> m Petri
forall a b. (a -> b) -> a -> b
$ Petri {
    initialMarking :: Marking
initialMarking = (Node a -> Int) -> [Node a] -> Marking
forall a b. (a -> b) -> [a] -> [b]
map Node a -> Int
forall a. Node a -> Int
forall (n :: * -> *) a. PetriNode n => n a -> Int
initialTokens ([Node a] -> Marking) -> [Node a] -> Marking
forall a b. (a -> b) -> a -> b
$ Map a (Node a) -> [Node a]
forall k a. Map k a -> [a]
M.elems Map a (Node a)
ps,
    trans :: [Transition]
trans          =
      (Node a -> [Transition] -> [Transition])
-> [Transition] -> Map a (Node a) -> [Transition]
forall a b. (a -> b -> b) -> b -> Map a a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) (Transition -> [Transition] -> [Transition])
-> (Node a -> Transition) -> Node a -> [Transition] -> [Transition]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node a -> Transition
toChangeTuple) [] Map a (Node a)
ts
    }
  where
    ps :: Map a (Node a)
ps = (Node a -> Bool) -> Map a (Node a) -> Map a (Node a)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter Node a -> Bool
forall a. Node a -> Bool
forall (n :: * -> *) a. PetriNode n => n a -> Bool
isPlaceNode (Map a (Node a) -> Map a (Node a))
-> Map a (Node a) -> Map a (Node a)
forall a b. (a -> b) -> a -> b
$ PetriLike Node a -> Map a (Node a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes PetriLike Node a
p
    ts :: Map a (Node a)
ts = (Node a -> Bool) -> Map a (Node a) -> Map a (Node a)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter Node a -> Bool
forall a. Node a -> Bool
forall (n :: * -> *) a. PetriNode n => n a -> Bool
isTransitionNode (Map a (Node a) -> Map a (Node a))
-> Map a (Node a) -> Map a (Node a)
forall a b. (a -> b) -> a -> b
$ PetriLike Node a -> Map a (Node a)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes PetriLike Node a
p
    isValid :: m ()
isValid
      | Bool -> Bool
not (Map a (Node a) -> Bool
forall k a. Map k a -> Bool
M.null (Map a (Node a) -> Bool) -> Map a (Node a) -> Bool
forall a b. (a -> b) -> a -> b
$ (Node a -> Bool) -> Map a (Node a) -> Map a (Node a)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0) (Int -> Bool) -> (Node a -> Int) -> Node a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node a -> Int
forall a. Node a -> Int
forall (n :: * -> *) a. PetriNode n => n a -> Int
initialTokens) Map a (Node a)
ps)
      = InvalidPetriNetException -> m ()
forall e a. Exception e => e -> m a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM InvalidPetriNetException
PlaceWithNegativeTokenNumber
      | (a -> Bool) -> Set a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (a -> Map a (Node a) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map a (Node a)
ts) (Map a (Node a) -> Set a
allRelatedNodes Map a (Node a)
ts)
      = InvalidPetriNetException -> m ()
forall e a. Exception e => e -> m a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM InvalidPetriNetException
RelatedNodesOfTransitionsContainTransitions
      | (a -> Bool) -> Set a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (a -> Map a (Node a) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map a (Node a)
ps) (Map a (Node a) -> Set a
allRelatedNodes Map a (Node a)
ps)
      = InvalidPetriNetException -> m ()
forall e a. Exception e => e -> m a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM InvalidPetriNetException
RelatedNodesOfPlacesContainPlaces
      | (Node a -> Bool) -> Map a (Node a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Int -> Bool) -> Map a Int -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0) (Map a Int -> Bool) -> (Node a -> Map a Int) -> Node a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node a -> Map a Int
forall a. Node a -> Map a Int
flowIn) Map a (Node a)
ts
      = InvalidPetriNetException -> m ()
forall e a. Exception e => e -> m a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM InvalidPetriNetException
FlowToATransitionIsZeroOrLess
      | (Node a -> Bool) -> Map a (Node a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Int -> Bool) -> Map a Int -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0) (Map a Int -> Bool) -> (Node a -> Map a Int) -> Node a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node a -> Map a Int
forall a. Node a -> Map a Int
flowOutN) Map a (Node a)
ts
      = InvalidPetriNetException -> m ()
forall e a. Exception e => e -> m a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM InvalidPetriNetException
FlowFromATransitionIsZeroOrLess
      | Bool
otherwise
      = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    toChangeTuple :: Node a -> Transition
toChangeTuple Node a
n = ((Node a -> Map a Int) -> Node a -> Marking
forall {a} {t}. Num a => (t -> Map a a) -> t -> [a]
toFlowList Node a -> Map a Int
forall a. Node a -> Map a Int
flowIn Node a
n, (Node a -> Map a Int) -> Node a -> Marking
forall {a} {t}. Num a => (t -> Map a a) -> t -> [a]
toFlowList Node a -> Map a Int
forall a. Node a -> Map a Int
flowOutN Node a
n)
    toFlowList :: (t -> Map a a) -> t -> [a]
toFlowList t -> Map a a
f t
n = (a -> Node a -> [a] -> [a]) -> [a] -> Map a (Node a) -> [a]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey
      (\a
k Node a
_ [a]
xs -> a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
0 (a -> Map a a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
k (Map a a -> Maybe a) -> Map a a -> Maybe a
forall a b. (a -> b) -> a -> b
$ t -> Map a a
f t
n) a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs)
      []
      Map a (Node a)
ps
    relatedNodes :: Node a -> Set a
relatedNodes Node a
n = Map a Int -> Set a
forall k a. Map k a -> Set k
M.keysSet (Node a -> Map a Int
forall a. Node a -> Map a Int
flowIn Node a
n) Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`S.union` Map a Int -> Set a
forall k a. Map k a -> Set k
M.keysSet (Node a -> Map a Int
forall a. Node a -> Map a Int
flowOutN Node a
n)
    allRelatedNodes :: Map a (Node a) -> Set a
allRelatedNodes = (Node a -> Set a -> Set a) -> Set a -> Map a (Node a) -> Set a
forall a b. (a -> b -> b) -> b -> Map a a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
      (Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
S.union (Set a -> Set a -> Set a)
-> (Node a -> Set a) -> Node a -> Set a -> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node a -> Set a
forall {a}. Ord a => Node a -> Set a
relatedNodes)
      Set a
forall a. Set a
S.empty

type Marking = [Int]
type Transition = (Marking,Marking)

{-|
Stores a mathematical representation of a Petri net based on a five tuple.
-}
data PetriMath a = PetriMath {
  -- | the five tuple itself
  forall a. PetriMath a -> a
netMath            :: a,
  -- | the places (the first element of the five tuple)
  forall a. PetriMath a -> a
placesMath         :: a,
  -- | the transitions (the second element of the five tuple)
  forall a. PetriMath a -> a
transitionsMath    :: a,
  {- | the token change of each transition
       (the third and fourth element of the five tuple) -}
  forall a. PetriMath a -> [(a, a)]
tokenChangeMath    :: [(a, a)],
  -- | the initial marking (the fifth element of the five tuple)
  forall a. PetriMath a -> a
initialMarkingMath :: a,
  -- | the order of places used for notation of token changes ('tokenChangeMath')
  forall a. PetriMath a -> Maybe a
placeOrderMath     :: Maybe a
  } deriving (Typeable (PetriMath a)
Typeable (PetriMath a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> PetriMath a -> c (PetriMath a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (PetriMath a))
-> (PetriMath a -> Constr)
-> (PetriMath a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (PetriMath a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (PetriMath a)))
-> ((forall b. Data b => b -> b) -> PetriMath a -> PetriMath a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PetriMath a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PetriMath a -> r)
-> (forall u. (forall d. Data d => d -> u) -> PetriMath a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> PetriMath a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PetriMath a -> m (PetriMath a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PetriMath a -> m (PetriMath a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PetriMath a -> m (PetriMath a))
-> Data (PetriMath a)
PetriMath a -> Constr
PetriMath a -> DataType
(forall b. Data b => b -> b) -> PetriMath a -> PetriMath a
forall {a}. Data a => Typeable (PetriMath a)
forall a. Data a => PetriMath a -> Constr
forall a. Data a => PetriMath a -> DataType
forall a.
Data a =>
(forall b. Data b => b -> b) -> PetriMath a -> PetriMath a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> PetriMath a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> PetriMath a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PetriMath a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PetriMath a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> PetriMath a -> m (PetriMath a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> PetriMath a -> m (PetriMath a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PetriMath a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PetriMath a -> c (PetriMath a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PetriMath a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PetriMath a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PetriMath a -> u
forall u. (forall d. Data d => d -> u) -> PetriMath a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PetriMath a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PetriMath a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PetriMath a -> m (PetriMath a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PetriMath a -> m (PetriMath a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PetriMath a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PetriMath a -> c (PetriMath a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (PetriMath a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PetriMath a))
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PetriMath a -> c (PetriMath a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PetriMath a -> c (PetriMath a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PetriMath a)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (PetriMath a)
$ctoConstr :: forall a. Data a => PetriMath a -> Constr
toConstr :: PetriMath a -> Constr
$cdataTypeOf :: forall a. Data a => PetriMath a -> DataType
dataTypeOf :: PetriMath a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (PetriMath a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (PetriMath a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PetriMath a))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (PetriMath a))
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> PetriMath a -> PetriMath a
gmapT :: (forall b. Data b => b -> b) -> PetriMath a -> PetriMath a
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PetriMath a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PetriMath a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PetriMath a -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PetriMath a -> r
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> PetriMath a -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> PetriMath a -> [u]
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> PetriMath a -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PetriMath a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> PetriMath a -> m (PetriMath a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PetriMath a -> m (PetriMath a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> PetriMath a -> m (PetriMath a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PetriMath a -> m (PetriMath a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> PetriMath a -> m (PetriMath a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PetriMath a -> m (PetriMath a)
Data, (forall m. Monoid m => PetriMath m -> m)
-> (forall m a. Monoid m => (a -> m) -> PetriMath a -> m)
-> (forall m a. Monoid m => (a -> m) -> PetriMath a -> m)
-> (forall a b. (a -> b -> b) -> b -> PetriMath a -> b)
-> (forall a b. (a -> b -> b) -> b -> PetriMath a -> b)
-> (forall b a. (b -> a -> b) -> b -> PetriMath a -> b)
-> (forall b a. (b -> a -> b) -> b -> PetriMath a -> b)
-> (forall a. (a -> a -> a) -> PetriMath a -> a)
-> (forall a. (a -> a -> a) -> PetriMath a -> a)
-> (forall a. PetriMath a -> [a])
-> (forall a. PetriMath a -> Bool)
-> (forall a. PetriMath a -> Int)
-> (forall a. Eq a => a -> PetriMath a -> Bool)
-> (forall a. Ord a => PetriMath a -> a)
-> (forall a. Ord a => PetriMath a -> a)
-> (forall a. Num a => PetriMath a -> a)
-> (forall a. Num a => PetriMath a -> a)
-> Foldable PetriMath
forall a. Eq a => a -> PetriMath a -> Bool
forall a. Num a => PetriMath a -> a
forall a. Ord a => PetriMath a -> a
forall m. Monoid m => PetriMath m -> m
forall a. PetriMath a -> Bool
forall a. PetriMath a -> Int
forall a. PetriMath a -> [a]
forall a. (a -> a -> a) -> PetriMath a -> a
forall m a. Monoid m => (a -> m) -> PetriMath a -> m
forall b a. (b -> a -> b) -> b -> PetriMath a -> b
forall a b. (a -> b -> b) -> b -> PetriMath a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => PetriMath m -> m
fold :: forall m. Monoid m => PetriMath m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> PetriMath a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> PetriMath a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> PetriMath a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> PetriMath a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> PetriMath a -> b
foldr :: forall a b. (a -> b -> b) -> b -> PetriMath a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> PetriMath a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> PetriMath a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> PetriMath a -> b
foldl :: forall b a. (b -> a -> b) -> b -> PetriMath a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> PetriMath a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> PetriMath a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> PetriMath a -> a
foldr1 :: forall a. (a -> a -> a) -> PetriMath a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> PetriMath a -> a
foldl1 :: forall a. (a -> a -> a) -> PetriMath a -> a
$ctoList :: forall a. PetriMath a -> [a]
toList :: forall a. PetriMath a -> [a]
$cnull :: forall a. PetriMath a -> Bool
null :: forall a. PetriMath a -> Bool
$clength :: forall a. PetriMath a -> Int
length :: forall a. PetriMath a -> Int
$celem :: forall a. Eq a => a -> PetriMath a -> Bool
elem :: forall a. Eq a => a -> PetriMath a -> Bool
$cmaximum :: forall a. Ord a => PetriMath a -> a
maximum :: forall a. Ord a => PetriMath a -> a
$cminimum :: forall a. Ord a => PetriMath a -> a
minimum :: forall a. Ord a => PetriMath a -> a
$csum :: forall a. Num a => PetriMath a -> a
sum :: forall a. Num a => PetriMath a -> a
$cproduct :: forall a. Num a => PetriMath a -> a
product :: forall a. Num a => PetriMath a -> a
Foldable, (forall a b. (a -> b) -> PetriMath a -> PetriMath b)
-> (forall a b. a -> PetriMath b -> PetriMath a)
-> Functor PetriMath
forall a b. a -> PetriMath b -> PetriMath a
forall a b. (a -> b) -> PetriMath a -> PetriMath b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> PetriMath a -> PetriMath b
fmap :: forall a b. (a -> b) -> PetriMath a -> PetriMath b
$c<$ :: forall a b. a -> PetriMath b -> PetriMath a
<$ :: forall a b. a -> PetriMath b -> PetriMath a
Functor, (forall x. PetriMath a -> Rep (PetriMath a) x)
-> (forall x. Rep (PetriMath a) x -> PetriMath a)
-> Generic (PetriMath a)
forall x. Rep (PetriMath a) x -> PetriMath a
forall x. PetriMath a -> Rep (PetriMath a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (PetriMath a) x -> PetriMath a
forall a x. PetriMath a -> Rep (PetriMath a) x
$cfrom :: forall a x. PetriMath a -> Rep (PetriMath a) x
from :: forall x. PetriMath a -> Rep (PetriMath a) x
$cto :: forall a x. Rep (PetriMath a) x -> PetriMath a
to :: forall x. Rep (PetriMath a) x -> PetriMath a
Generic, ReadPrec [PetriMath a]
ReadPrec (PetriMath a)
Int -> ReadS (PetriMath a)
ReadS [PetriMath a]
(Int -> ReadS (PetriMath a))
-> ReadS [PetriMath a]
-> ReadPrec (PetriMath a)
-> ReadPrec [PetriMath a]
-> Read (PetriMath a)
forall a. Read a => ReadPrec [PetriMath a]
forall a. Read a => ReadPrec (PetriMath a)
forall a. Read a => Int -> ReadS (PetriMath a)
forall a. Read a => ReadS [PetriMath a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall a. Read a => Int -> ReadS (PetriMath a)
readsPrec :: Int -> ReadS (PetriMath a)
$creadList :: forall a. Read a => ReadS [PetriMath a]
readList :: ReadS [PetriMath a]
$creadPrec :: forall a. Read a => ReadPrec (PetriMath a)
readPrec :: ReadPrec (PetriMath a)
$creadListPrec :: forall a. Read a => ReadPrec [PetriMath a]
readListPrec :: ReadPrec [PetriMath a]
Read, Int -> PetriMath a -> ShowS
[PetriMath a] -> ShowS
PetriMath a -> String
(Int -> PetriMath a -> ShowS)
-> (PetriMath a -> String)
-> ([PetriMath a] -> ShowS)
-> Show (PetriMath a)
forall a. Show a => Int -> PetriMath a -> ShowS
forall a. Show a => [PetriMath a] -> ShowS
forall a. Show a => PetriMath a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> PetriMath a -> ShowS
showsPrec :: Int -> PetriMath a -> ShowS
$cshow :: forall a. Show a => PetriMath a -> String
show :: PetriMath a -> String
$cshowList :: forall a. Show a => [PetriMath a] -> ShowS
showList :: [PetriMath a] -> ShowS
Show, Functor PetriMath
Foldable PetriMath
Functor PetriMath
-> Foldable PetriMath
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> PetriMath a -> f (PetriMath b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    PetriMath (f a) -> f (PetriMath a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> PetriMath a -> m (PetriMath b))
-> (forall (m :: * -> *) a.
    Monad m =>
    PetriMath (m a) -> m (PetriMath a))
-> Traversable PetriMath
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
PetriMath (m a) -> m (PetriMath a)
forall (f :: * -> *) a.
Applicative f =>
PetriMath (f a) -> f (PetriMath a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PetriMath a -> m (PetriMath b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PetriMath a -> f (PetriMath b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PetriMath a -> f (PetriMath b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PetriMath a -> f (PetriMath b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
PetriMath (f a) -> f (PetriMath a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
PetriMath (f a) -> f (PetriMath a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PetriMath a -> m (PetriMath b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PetriMath a -> m (PetriMath b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
PetriMath (m a) -> m (PetriMath a)
sequence :: forall (m :: * -> *) a.
Monad m =>
PetriMath (m a) -> m (PetriMath a)
Traversable)

data Petri = Petri
  { Petri -> Marking
initialMarking :: Marking
  , Petri -> [Transition]
trans :: [Transition]
  } deriving (Petri -> Petri -> Bool
(Petri -> Petri -> Bool) -> (Petri -> Petri -> Bool) -> Eq Petri
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Petri -> Petri -> Bool
== :: Petri -> Petri -> Bool
$c/= :: Petri -> Petri -> Bool
/= :: Petri -> Petri -> Bool
Eq, (forall x. Petri -> Rep Petri x)
-> (forall x. Rep Petri x -> Petri) -> Generic Petri
forall x. Rep Petri x -> Petri
forall x. Petri -> Rep Petri x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Petri -> Rep Petri x
from :: forall x. Petri -> Rep Petri x
$cto :: forall x. Rep Petri x -> Petri
to :: forall x. Rep Petri x -> Petri
Generic, ReadPrec [Petri]
ReadPrec Petri
Int -> ReadS Petri
ReadS [Petri]
(Int -> ReadS Petri)
-> ReadS [Petri]
-> ReadPrec Petri
-> ReadPrec [Petri]
-> Read Petri
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Petri
readsPrec :: Int -> ReadS Petri
$creadList :: ReadS [Petri]
readList :: ReadS [Petri]
$creadPrec :: ReadPrec Petri
readPrec :: ReadPrec Petri
$creadListPrec :: ReadPrec [Petri]
readListPrec :: ReadPrec [Petri]
Read, Int -> Petri -> ShowS
[Petri] -> ShowS
Petri -> String
(Int -> Petri -> ShowS)
-> (Petri -> String) -> ([Petri] -> ShowS) -> Show Petri
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Petri -> ShowS
showsPrec :: Int -> Petri -> ShowS
$cshow :: Petri -> String
show :: Petri -> String
$cshowList :: [Petri] -> ShowS
showList :: [Petri] -> ShowS
Show)

data BasicConfig = BasicConfig
  { BasicConfig -> Int
places :: Int
  , BasicConfig -> Int
transitions :: Int
  , BasicConfig -> Int
atLeastActive :: Int
  , BasicConfig -> (Int, Int)
flowOverall :: (Int, Int)
  -- ^ allowed range of flow edge weights in total (over all edges)
  , BasicConfig -> Int
maxTokensPerPlace :: Int
  , BasicConfig -> Int
maxFlowPerEdge :: Int
  , BasicConfig -> (Int, Int)
tokensOverall :: (Int, Int)
  -- ^ allowed range of tokens in total (over all places)
  , BasicConfig -> Maybe Bool
isConnected :: Maybe Bool
  } deriving ((forall x. BasicConfig -> Rep BasicConfig x)
-> (forall x. Rep BasicConfig x -> BasicConfig)
-> Generic BasicConfig
forall x. Rep BasicConfig x -> BasicConfig
forall x. BasicConfig -> Rep BasicConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BasicConfig -> Rep BasicConfig x
from :: forall x. BasicConfig -> Rep BasicConfig x
$cto :: forall x. Rep BasicConfig x -> BasicConfig
to :: forall x. Rep BasicConfig x -> BasicConfig
Generic, ReadPrec [BasicConfig]
ReadPrec BasicConfig
Int -> ReadS BasicConfig
ReadS [BasicConfig]
(Int -> ReadS BasicConfig)
-> ReadS [BasicConfig]
-> ReadPrec BasicConfig
-> ReadPrec [BasicConfig]
-> Read BasicConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS BasicConfig
readsPrec :: Int -> ReadS BasicConfig
$creadList :: ReadS [BasicConfig]
readList :: ReadS [BasicConfig]
$creadPrec :: ReadPrec BasicConfig
readPrec :: ReadPrec BasicConfig
$creadListPrec :: ReadPrec [BasicConfig]
readListPrec :: ReadPrec [BasicConfig]
Read, Int -> BasicConfig -> ShowS
[BasicConfig] -> ShowS
BasicConfig -> String
(Int -> BasicConfig -> ShowS)
-> (BasicConfig -> String)
-> ([BasicConfig] -> ShowS)
-> Show BasicConfig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BasicConfig -> ShowS
showsPrec :: Int -> BasicConfig -> ShowS
$cshow :: BasicConfig -> String
show :: BasicConfig -> String
$cshowList :: [BasicConfig] -> ShowS
showList :: [BasicConfig] -> ShowS
Show)

makeLensesWith lensRulesL ''BasicConfig

defaultBasicConfig :: BasicConfig
defaultBasicConfig :: BasicConfig
defaultBasicConfig = BasicConfig
  { $sel:places:BasicConfig :: Int
places = Int
4
  , $sel:transitions:BasicConfig :: Int
transitions = Int
3
  , $sel:atLeastActive:BasicConfig :: Int
atLeastActive = Int
1
  , $sel:flowOverall:BasicConfig :: (Int, Int)
flowOverall = (Int
6, Int
12)
  , $sel:maxTokensPerPlace:BasicConfig :: Int
maxTokensPerPlace = Int
2
  , $sel:maxFlowPerEdge:BasicConfig :: Int
maxFlowPerEdge = Int
2
  , $sel:tokensOverall:BasicConfig :: (Int, Int)
tokensOverall = (Int
2, Int
7)
  , $sel:isConnected:BasicConfig :: Maybe Bool
isConnected = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
  }

data GraphConfig = GraphConfig {
  GraphConfig -> [GraphvizCommand]
graphLayouts :: [GraphvizCommand],
  GraphConfig -> Bool
hidePlaceNames :: Bool,
  GraphConfig -> Bool
hideTransitionNames :: Bool,
  GraphConfig -> Bool
hideWeight1 :: Bool
  } deriving ((forall x. GraphConfig -> Rep GraphConfig x)
-> (forall x. Rep GraphConfig x -> GraphConfig)
-> Generic GraphConfig
forall x. Rep GraphConfig x -> GraphConfig
forall x. GraphConfig -> Rep GraphConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. GraphConfig -> Rep GraphConfig x
from :: forall x. GraphConfig -> Rep GraphConfig x
$cto :: forall x. Rep GraphConfig x -> GraphConfig
to :: forall x. Rep GraphConfig x -> GraphConfig
Generic, ReadPrec [GraphConfig]
ReadPrec GraphConfig
Int -> ReadS GraphConfig
ReadS [GraphConfig]
(Int -> ReadS GraphConfig)
-> ReadS [GraphConfig]
-> ReadPrec GraphConfig
-> ReadPrec [GraphConfig]
-> Read GraphConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS GraphConfig
readsPrec :: Int -> ReadS GraphConfig
$creadList :: ReadS [GraphConfig]
readList :: ReadS [GraphConfig]
$creadPrec :: ReadPrec GraphConfig
readPrec :: ReadPrec GraphConfig
$creadListPrec :: ReadPrec [GraphConfig]
readListPrec :: ReadPrec [GraphConfig]
Read, Int -> GraphConfig -> ShowS
[GraphConfig] -> ShowS
GraphConfig -> String
(Int -> GraphConfig -> ShowS)
-> (GraphConfig -> String)
-> ([GraphConfig] -> ShowS)
-> Show GraphConfig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GraphConfig -> ShowS
showsPrec :: Int -> GraphConfig -> ShowS
$cshow :: GraphConfig -> String
show :: GraphConfig -> String
$cshowList :: [GraphConfig] -> ShowS
showList :: [GraphConfig] -> ShowS
Show)

defaultGraphConfig :: GraphConfig
defaultGraphConfig :: GraphConfig
defaultGraphConfig = GraphConfig {
  $sel:graphLayouts:GraphConfig :: [GraphvizCommand]
graphLayouts = [GraphvizCommand
Dot, GraphvizCommand
Neato, GraphvizCommand
TwoPi, GraphvizCommand
Circo, GraphvizCommand
Fdp, GraphvizCommand
Sfdp, GraphvizCommand
Osage, GraphvizCommand
Patchwork],
  $sel:hidePlaceNames:GraphConfig :: Bool
hidePlaceNames = Bool
False,
  $sel:hideTransitionNames:GraphConfig :: Bool
hideTransitionNames = Bool
False,
  $sel:hideWeight1:GraphConfig :: Bool
hideWeight1 = Bool
True
  }

makeLensesWith lensRulesL ''GraphConfig

data AdvConfig = AdvConfig
  { AdvConfig -> Maybe Bool
presenceOfSelfLoops :: Maybe Bool
  , AdvConfig -> Maybe Bool
presenceOfSinkTransitions :: Maybe Bool
  , AdvConfig -> Maybe Bool
presenceOfSourceTransitions :: Maybe Bool
  } deriving ((forall x. AdvConfig -> Rep AdvConfig x)
-> (forall x. Rep AdvConfig x -> AdvConfig) -> Generic AdvConfig
forall x. Rep AdvConfig x -> AdvConfig
forall x. AdvConfig -> Rep AdvConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AdvConfig -> Rep AdvConfig x
from :: forall x. AdvConfig -> Rep AdvConfig x
$cto :: forall x. Rep AdvConfig x -> AdvConfig
to :: forall x. Rep AdvConfig x -> AdvConfig
Generic, ReadPrec [AdvConfig]
ReadPrec AdvConfig
Int -> ReadS AdvConfig
ReadS [AdvConfig]
(Int -> ReadS AdvConfig)
-> ReadS [AdvConfig]
-> ReadPrec AdvConfig
-> ReadPrec [AdvConfig]
-> Read AdvConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS AdvConfig
readsPrec :: Int -> ReadS AdvConfig
$creadList :: ReadS [AdvConfig]
readList :: ReadS [AdvConfig]
$creadPrec :: ReadPrec AdvConfig
readPrec :: ReadPrec AdvConfig
$creadListPrec :: ReadPrec [AdvConfig]
readListPrec :: ReadPrec [AdvConfig]
Read, Int -> AdvConfig -> ShowS
[AdvConfig] -> ShowS
AdvConfig -> String
(Int -> AdvConfig -> ShowS)
-> (AdvConfig -> String)
-> ([AdvConfig] -> ShowS)
-> Show AdvConfig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AdvConfig -> ShowS
showsPrec :: Int -> AdvConfig -> ShowS
$cshow :: AdvConfig -> String
show :: AdvConfig -> String
$cshowList :: [AdvConfig] -> ShowS
showList :: [AdvConfig] -> ShowS
Show)

defaultAdvConfig :: AdvConfig
defaultAdvConfig :: AdvConfig
defaultAdvConfig = AdvConfig
  { $sel:presenceOfSelfLoops:AdvConfig :: Maybe Bool
presenceOfSelfLoops = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  , $sel:presenceOfSinkTransitions:AdvConfig :: Maybe Bool
presenceOfSinkTransitions = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  , $sel:presenceOfSourceTransitions:AdvConfig :: Maybe Bool
presenceOfSourceTransitions = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  }

data ChangeConfig = ChangeConfig
  { ChangeConfig -> Int
tokenChangeOverall :: Int
  , ChangeConfig -> Int
maxTokenChangePerPlace :: Int
  , ChangeConfig -> Int
flowChangeOverall :: Int
  , ChangeConfig -> Int
maxFlowChangePerEdge :: Int
  } deriving ((forall x. ChangeConfig -> Rep ChangeConfig x)
-> (forall x. Rep ChangeConfig x -> ChangeConfig)
-> Generic ChangeConfig
forall x. Rep ChangeConfig x -> ChangeConfig
forall x. ChangeConfig -> Rep ChangeConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ChangeConfig -> Rep ChangeConfig x
from :: forall x. ChangeConfig -> Rep ChangeConfig x
$cto :: forall x. Rep ChangeConfig x -> ChangeConfig
to :: forall x. Rep ChangeConfig x -> ChangeConfig
Generic, ReadPrec [ChangeConfig]
ReadPrec ChangeConfig
Int -> ReadS ChangeConfig
ReadS [ChangeConfig]
(Int -> ReadS ChangeConfig)
-> ReadS [ChangeConfig]
-> ReadPrec ChangeConfig
-> ReadPrec [ChangeConfig]
-> Read ChangeConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS ChangeConfig
readsPrec :: Int -> ReadS ChangeConfig
$creadList :: ReadS [ChangeConfig]
readList :: ReadS [ChangeConfig]
$creadPrec :: ReadPrec ChangeConfig
readPrec :: ReadPrec ChangeConfig
$creadListPrec :: ReadPrec [ChangeConfig]
readListPrec :: ReadPrec [ChangeConfig]
Read, Int -> ChangeConfig -> ShowS
[ChangeConfig] -> ShowS
ChangeConfig -> String
(Int -> ChangeConfig -> ShowS)
-> (ChangeConfig -> String)
-> ([ChangeConfig] -> ShowS)
-> Show ChangeConfig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ChangeConfig -> ShowS
showsPrec :: Int -> ChangeConfig -> ShowS
$cshow :: ChangeConfig -> String
show :: ChangeConfig -> String
$cshowList :: [ChangeConfig] -> ShowS
showList :: [ChangeConfig] -> ShowS
Show)

defaultChangeConfig :: ChangeConfig
defaultChangeConfig :: ChangeConfig
defaultChangeConfig = ChangeConfig
  { $sel:tokenChangeOverall:ChangeConfig :: Int
tokenChangeOverall = Int
2
  , $sel:maxTokenChangePerPlace:ChangeConfig :: Int
maxTokenChangePerPlace = Int
1
  , $sel:flowChangeOverall:ChangeConfig :: Int
flowChangeOverall = Int
2
  , $sel:maxFlowChangePerEdge:ChangeConfig :: Int
maxFlowChangePerEdge = Int
1
  }

data ConflictConfig = ConflictConfig {
  -- | to enforce (no) extra places being common preconditions
  -- (but not in conflict) for the transitions in conflict
  ConflictConfig -> Maybe Bool
addConflictCommonPreconditions        :: Maybe Bool,
  -- | to enforce the (non-)existence of conflict distractors
  ConflictConfig -> Maybe Bool
withConflictDistractors               :: Maybe Bool,
  -- | to enforce the (non-)existence of more common preconditions
  -- than places in conflict for at least one distractor
  ConflictConfig -> Maybe Bool
conflictDistractorAddExtraPreconditions :: Maybe Bool,
  -- | to enforce that at least one distractor looks conflict like
  ConflictConfig -> Bool
conflictDistractorOnlyConflictLike    :: Bool,
  -- | to enforce that at least one distractor looks concurrent like
  ConflictConfig -> Bool
conflictDistractorOnlyConcurrentLike  :: Bool
  }
  deriving ((forall x. ConflictConfig -> Rep ConflictConfig x)
-> (forall x. Rep ConflictConfig x -> ConflictConfig)
-> Generic ConflictConfig
forall x. Rep ConflictConfig x -> ConflictConfig
forall x. ConflictConfig -> Rep ConflictConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ConflictConfig -> Rep ConflictConfig x
from :: forall x. ConflictConfig -> Rep ConflictConfig x
$cto :: forall x. Rep ConflictConfig x -> ConflictConfig
to :: forall x. Rep ConflictConfig x -> ConflictConfig
Generic, ReadPrec [ConflictConfig]
ReadPrec ConflictConfig
Int -> ReadS ConflictConfig
ReadS [ConflictConfig]
(Int -> ReadS ConflictConfig)
-> ReadS [ConflictConfig]
-> ReadPrec ConflictConfig
-> ReadPrec [ConflictConfig]
-> Read ConflictConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS ConflictConfig
readsPrec :: Int -> ReadS ConflictConfig
$creadList :: ReadS [ConflictConfig]
readList :: ReadS [ConflictConfig]
$creadPrec :: ReadPrec ConflictConfig
readPrec :: ReadPrec ConflictConfig
$creadListPrec :: ReadPrec [ConflictConfig]
readListPrec :: ReadPrec [ConflictConfig]
Read, Int -> ConflictConfig -> ShowS
[ConflictConfig] -> ShowS
ConflictConfig -> String
(Int -> ConflictConfig -> ShowS)
-> (ConflictConfig -> String)
-> ([ConflictConfig] -> ShowS)
-> Show ConflictConfig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConflictConfig -> ShowS
showsPrec :: Int -> ConflictConfig -> ShowS
$cshow :: ConflictConfig -> String
show :: ConflictConfig -> String
$cshowList :: [ConflictConfig] -> ShowS
showList :: [ConflictConfig] -> ShowS
Show)

defaultConflictConfig :: ConflictConfig
defaultConflictConfig :: ConflictConfig
defaultConflictConfig = ConflictConfig {
  $sel:addConflictCommonPreconditions:ConflictConfig :: Maybe Bool
addConflictCommonPreconditions        = Maybe Bool
forall a. Maybe a
Nothing,
  $sel:withConflictDistractors:ConflictConfig :: Maybe Bool
withConflictDistractors               = Maybe Bool
forall a. Maybe a
Nothing,
  $sel:conflictDistractorAddExtraPreconditions:ConflictConfig :: Maybe Bool
conflictDistractorAddExtraPreconditions = Maybe Bool
forall a. Maybe a
Nothing,
  $sel:conflictDistractorOnlyConflictLike:ConflictConfig :: Bool
conflictDistractorOnlyConflictLike    = Bool
False,
  $sel:conflictDistractorOnlyConcurrentLike:ConflictConfig :: Bool
conflictDistractorOnlyConcurrentLike  = Bool
False
  }

data FindConflictConfig = FindConflictConfig
  { FindConflictConfig -> BasicConfig
basicConfig :: BasicConfig
  , FindConflictConfig -> AdvConfig
advConfig :: AdvConfig
  , FindConflictConfig -> ChangeConfig
changeConfig :: ChangeConfig
  , FindConflictConfig -> ConflictConfig
conflictConfig :: ConflictConfig
  , FindConflictConfig -> GraphConfig
graphConfig :: GraphConfig
  , FindConflictConfig -> Bool
printSolution :: Bool
  , FindConflictConfig -> Maybe Bool
uniqueConflictPlace :: Maybe Bool
  , FindConflictConfig -> AlloyConfig
alloyConfig  :: AlloyConfig
  , FindConflictConfig -> Maybe (Map Language String)
extraText :: Maybe (Map Language String)
  } deriving ((forall x. FindConflictConfig -> Rep FindConflictConfig x)
-> (forall x. Rep FindConflictConfig x -> FindConflictConfig)
-> Generic FindConflictConfig
forall x. Rep FindConflictConfig x -> FindConflictConfig
forall x. FindConflictConfig -> Rep FindConflictConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FindConflictConfig -> Rep FindConflictConfig x
from :: forall x. FindConflictConfig -> Rep FindConflictConfig x
$cto :: forall x. Rep FindConflictConfig x -> FindConflictConfig
to :: forall x. Rep FindConflictConfig x -> FindConflictConfig
Generic, ReadPrec [FindConflictConfig]
ReadPrec FindConflictConfig
Int -> ReadS FindConflictConfig
ReadS [FindConflictConfig]
(Int -> ReadS FindConflictConfig)
-> ReadS [FindConflictConfig]
-> ReadPrec FindConflictConfig
-> ReadPrec [FindConflictConfig]
-> Read FindConflictConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS FindConflictConfig
readsPrec :: Int -> ReadS FindConflictConfig
$creadList :: ReadS [FindConflictConfig]
readList :: ReadS [FindConflictConfig]
$creadPrec :: ReadPrec FindConflictConfig
readPrec :: ReadPrec FindConflictConfig
$creadListPrec :: ReadPrec [FindConflictConfig]
readListPrec :: ReadPrec [FindConflictConfig]
Read, Int -> FindConflictConfig -> ShowS
[FindConflictConfig] -> ShowS
FindConflictConfig -> String
(Int -> FindConflictConfig -> ShowS)
-> (FindConflictConfig -> String)
-> ([FindConflictConfig] -> ShowS)
-> Show FindConflictConfig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FindConflictConfig -> ShowS
showsPrec :: Int -> FindConflictConfig -> ShowS
$cshow :: FindConflictConfig -> String
show :: FindConflictConfig -> String
$cshowList :: [FindConflictConfig] -> ShowS
showList :: [FindConflictConfig] -> ShowS
Show)

makeLensesWith lensRulesL ''FindConflictConfig

defaultFindConflictConfig :: FindConflictConfig
defaultFindConflictConfig :: FindConflictConfig
defaultFindConflictConfig = FindConflictConfig
  { $sel:basicConfig:FindConflictConfig :: BasicConfig
basicConfig = BasicConfig
defaultBasicConfig { $sel:atLeastActive:BasicConfig :: Int
atLeastActive = Int
3 }
  , $sel:advConfig:FindConflictConfig :: AdvConfig
advConfig = AdvConfig
defaultAdvConfig{ $sel:presenceOfSourceTransitions:AdvConfig :: Maybe Bool
presenceOfSourceTransitions = Maybe Bool
forall a. Maybe a
Nothing }
  , $sel:changeConfig:FindConflictConfig :: ChangeConfig
changeConfig = ChangeConfig
defaultChangeConfig
  , $sel:conflictConfig:FindConflictConfig :: ConflictConfig
conflictConfig = ConflictConfig
defaultConflictConfig
  , $sel:graphConfig:FindConflictConfig :: GraphConfig
graphConfig = GraphConfig
defaultGraphConfig { $sel:hidePlaceNames:GraphConfig :: Bool
hidePlaceNames = Bool
True }
  , $sel:printSolution:FindConflictConfig :: Bool
printSolution = Bool
False
  , $sel:uniqueConflictPlace:FindConflictConfig :: Maybe Bool
uniqueConflictPlace = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
  , $sel:alloyConfig:FindConflictConfig :: AlloyConfig
alloyConfig  = AlloyConfig
defaultAlloyConfig
  , $sel:extraText:FindConflictConfig :: Maybe (Map Language String)
extraText = Maybe (Map Language String)
forall a. Maybe a
Nothing
  }

data PickConflictConfig = PickConflictConfig
  { PickConflictConfig -> BasicConfig
basicConfig :: BasicConfig
  , PickConflictConfig -> ChangeConfig
changeConfig :: ChangeConfig
  , PickConflictConfig -> ConflictConfig
conflictConfig :: ConflictConfig
  , PickConflictConfig -> GraphConfig
graphConfig :: GraphConfig
  , PickConflictConfig -> Bool
printSolution :: Bool
  , PickConflictConfig -> Bool
prohibitSourceTransitions :: Bool
  , PickConflictConfig -> Maybe Bool
uniqueConflictPlace :: Maybe Bool
  , PickConflictConfig -> Bool
useDifferentGraphLayouts :: Bool
  , PickConflictConfig -> AlloyConfig
alloyConfig  :: AlloyConfig
  , PickConflictConfig -> Maybe (Map Language String)
extraText :: Maybe (Map Language String)
  } deriving ((forall x. PickConflictConfig -> Rep PickConflictConfig x)
-> (forall x. Rep PickConflictConfig x -> PickConflictConfig)
-> Generic PickConflictConfig
forall x. Rep PickConflictConfig x -> PickConflictConfig
forall x. PickConflictConfig -> Rep PickConflictConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PickConflictConfig -> Rep PickConflictConfig x
from :: forall x. PickConflictConfig -> Rep PickConflictConfig x
$cto :: forall x. Rep PickConflictConfig x -> PickConflictConfig
to :: forall x. Rep PickConflictConfig x -> PickConflictConfig
Generic, ReadPrec [PickConflictConfig]
ReadPrec PickConflictConfig
Int -> ReadS PickConflictConfig
ReadS [PickConflictConfig]
(Int -> ReadS PickConflictConfig)
-> ReadS [PickConflictConfig]
-> ReadPrec PickConflictConfig
-> ReadPrec [PickConflictConfig]
-> Read PickConflictConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS PickConflictConfig
readsPrec :: Int -> ReadS PickConflictConfig
$creadList :: ReadS [PickConflictConfig]
readList :: ReadS [PickConflictConfig]
$creadPrec :: ReadPrec PickConflictConfig
readPrec :: ReadPrec PickConflictConfig
$creadListPrec :: ReadPrec [PickConflictConfig]
readListPrec :: ReadPrec [PickConflictConfig]
Read, Int -> PickConflictConfig -> ShowS
[PickConflictConfig] -> ShowS
PickConflictConfig -> String
(Int -> PickConflictConfig -> ShowS)
-> (PickConflictConfig -> String)
-> ([PickConflictConfig] -> ShowS)
-> Show PickConflictConfig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PickConflictConfig -> ShowS
showsPrec :: Int -> PickConflictConfig -> ShowS
$cshow :: PickConflictConfig -> String
show :: PickConflictConfig -> String
$cshowList :: [PickConflictConfig] -> ShowS
showList :: [PickConflictConfig] -> ShowS
Show)

defaultPickConflictConfig :: PickConflictConfig
defaultPickConflictConfig :: PickConflictConfig
defaultPickConflictConfig = PickConflictConfig
  { $sel:basicConfig:PickConflictConfig :: BasicConfig
basicConfig = BasicConfig
defaultBasicConfig { $sel:atLeastActive:BasicConfig :: Int
atLeastActive = Int
2 }
  , $sel:changeConfig:PickConflictConfig :: ChangeConfig
changeConfig = ChangeConfig
defaultChangeConfig
  , $sel:conflictConfig:PickConflictConfig :: ConflictConfig
conflictConfig = ConflictConfig
defaultConflictConfig
  , $sel:graphConfig:PickConflictConfig :: GraphConfig
graphConfig = GraphConfig
defaultGraphConfig { $sel:hidePlaceNames:GraphConfig :: Bool
hidePlaceNames = Bool
True, $sel:hideTransitionNames:GraphConfig :: Bool
hideTransitionNames = Bool
True }
  , $sel:printSolution:PickConflictConfig :: Bool
printSolution = Bool
False
  , $sel:prohibitSourceTransitions:PickConflictConfig :: Bool
prohibitSourceTransitions = Bool
False
  , $sel:uniqueConflictPlace:PickConflictConfig :: Maybe Bool
uniqueConflictPlace = Maybe Bool
forall a. Maybe a
Nothing
  , $sel:useDifferentGraphLayouts:PickConflictConfig :: Bool
useDifferentGraphLayouts = Bool
False
  , $sel:alloyConfig:PickConflictConfig :: AlloyConfig
alloyConfig  = AlloyConfig
defaultAlloyConfig
  , $sel:extraText:PickConflictConfig :: Maybe (Map Language String)
extraText = Maybe (Map Language String)
forall a. Maybe a
Nothing
  }

data FindConcurrencyConfig = FindConcurrencyConfig
  { FindConcurrencyConfig -> BasicConfig
basicConfig :: BasicConfig
  , FindConcurrencyConfig -> AdvConfig
advConfig :: AdvConfig
  , FindConcurrencyConfig -> ChangeConfig
changeConfig :: ChangeConfig
  , FindConcurrencyConfig -> GraphConfig
graphConfig :: GraphConfig
  , FindConcurrencyConfig -> Bool
printSolution :: Bool
  , FindConcurrencyConfig -> AlloyConfig
alloyConfig  :: AlloyConfig
  , FindConcurrencyConfig -> Maybe (Map Language String)
extraText :: Maybe (Map Language String)
  } deriving ((forall x. FindConcurrencyConfig -> Rep FindConcurrencyConfig x)
-> (forall x. Rep FindConcurrencyConfig x -> FindConcurrencyConfig)
-> Generic FindConcurrencyConfig
forall x. Rep FindConcurrencyConfig x -> FindConcurrencyConfig
forall x. FindConcurrencyConfig -> Rep FindConcurrencyConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FindConcurrencyConfig -> Rep FindConcurrencyConfig x
from :: forall x. FindConcurrencyConfig -> Rep FindConcurrencyConfig x
$cto :: forall x. Rep FindConcurrencyConfig x -> FindConcurrencyConfig
to :: forall x. Rep FindConcurrencyConfig x -> FindConcurrencyConfig
Generic, ReadPrec [FindConcurrencyConfig]
ReadPrec FindConcurrencyConfig
Int -> ReadS FindConcurrencyConfig
ReadS [FindConcurrencyConfig]
(Int -> ReadS FindConcurrencyConfig)
-> ReadS [FindConcurrencyConfig]
-> ReadPrec FindConcurrencyConfig
-> ReadPrec [FindConcurrencyConfig]
-> Read FindConcurrencyConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS FindConcurrencyConfig
readsPrec :: Int -> ReadS FindConcurrencyConfig
$creadList :: ReadS [FindConcurrencyConfig]
readList :: ReadS [FindConcurrencyConfig]
$creadPrec :: ReadPrec FindConcurrencyConfig
readPrec :: ReadPrec FindConcurrencyConfig
$creadListPrec :: ReadPrec [FindConcurrencyConfig]
readListPrec :: ReadPrec [FindConcurrencyConfig]
Read, Int -> FindConcurrencyConfig -> ShowS
[FindConcurrencyConfig] -> ShowS
FindConcurrencyConfig -> String
(Int -> FindConcurrencyConfig -> ShowS)
-> (FindConcurrencyConfig -> String)
-> ([FindConcurrencyConfig] -> ShowS)
-> Show FindConcurrencyConfig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FindConcurrencyConfig -> ShowS
showsPrec :: Int -> FindConcurrencyConfig -> ShowS
$cshow :: FindConcurrencyConfig -> String
show :: FindConcurrencyConfig -> String
$cshowList :: [FindConcurrencyConfig] -> ShowS
showList :: [FindConcurrencyConfig] -> ShowS
Show)

defaultFindConcurrencyConfig :: FindConcurrencyConfig
defaultFindConcurrencyConfig :: FindConcurrencyConfig
defaultFindConcurrencyConfig = FindConcurrencyConfig
  { $sel:basicConfig:FindConcurrencyConfig :: BasicConfig
basicConfig = BasicConfig
defaultBasicConfig { $sel:atLeastActive:BasicConfig :: Int
atLeastActive = Int
3 }
  , $sel:advConfig:FindConcurrencyConfig :: AdvConfig
advConfig = AdvConfig
defaultAdvConfig{ $sel:presenceOfSourceTransitions:AdvConfig :: Maybe Bool
presenceOfSourceTransitions = Maybe Bool
forall a. Maybe a
Nothing }
  , $sel:changeConfig:FindConcurrencyConfig :: ChangeConfig
changeConfig = ChangeConfig
defaultChangeConfig
  , $sel:graphConfig:FindConcurrencyConfig :: GraphConfig
graphConfig = GraphConfig
defaultGraphConfig { $sel:hidePlaceNames:GraphConfig :: Bool
hidePlaceNames = Bool
True }
  , $sel:printSolution:FindConcurrencyConfig :: Bool
printSolution = Bool
False
  , $sel:alloyConfig:FindConcurrencyConfig :: AlloyConfig
alloyConfig  = AlloyConfig
defaultAlloyConfig
  , $sel:extraText:FindConcurrencyConfig :: Maybe (Map Language String)
extraText = Maybe (Map Language String)
forall a. Maybe a
Nothing
  }

data PickConcurrencyConfig = PickConcurrencyConfig
  { PickConcurrencyConfig -> BasicConfig
basicConfig :: BasicConfig
  , PickConcurrencyConfig -> ChangeConfig
changeConfig :: ChangeConfig
  , PickConcurrencyConfig -> GraphConfig
graphConfig :: GraphConfig
  , PickConcurrencyConfig -> Bool
printSolution :: Bool
  , PickConcurrencyConfig -> Bool
prohibitSourceTransitions :: Bool
  , PickConcurrencyConfig -> Bool
useDifferentGraphLayouts :: Bool
  , PickConcurrencyConfig -> AlloyConfig
alloyConfig  :: AlloyConfig
  , PickConcurrencyConfig -> Maybe (Map Language String)
extraText :: Maybe (Map Language String)
  } deriving ((forall x. PickConcurrencyConfig -> Rep PickConcurrencyConfig x)
-> (forall x. Rep PickConcurrencyConfig x -> PickConcurrencyConfig)
-> Generic PickConcurrencyConfig
forall x. Rep PickConcurrencyConfig x -> PickConcurrencyConfig
forall x. PickConcurrencyConfig -> Rep PickConcurrencyConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PickConcurrencyConfig -> Rep PickConcurrencyConfig x
from :: forall x. PickConcurrencyConfig -> Rep PickConcurrencyConfig x
$cto :: forall x. Rep PickConcurrencyConfig x -> PickConcurrencyConfig
to :: forall x. Rep PickConcurrencyConfig x -> PickConcurrencyConfig
Generic, ReadPrec [PickConcurrencyConfig]
ReadPrec PickConcurrencyConfig
Int -> ReadS PickConcurrencyConfig
ReadS [PickConcurrencyConfig]
(Int -> ReadS PickConcurrencyConfig)
-> ReadS [PickConcurrencyConfig]
-> ReadPrec PickConcurrencyConfig
-> ReadPrec [PickConcurrencyConfig]
-> Read PickConcurrencyConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS PickConcurrencyConfig
readsPrec :: Int -> ReadS PickConcurrencyConfig
$creadList :: ReadS [PickConcurrencyConfig]
readList :: ReadS [PickConcurrencyConfig]
$creadPrec :: ReadPrec PickConcurrencyConfig
readPrec :: ReadPrec PickConcurrencyConfig
$creadListPrec :: ReadPrec [PickConcurrencyConfig]
readListPrec :: ReadPrec [PickConcurrencyConfig]
Read, Int -> PickConcurrencyConfig -> ShowS
[PickConcurrencyConfig] -> ShowS
PickConcurrencyConfig -> String
(Int -> PickConcurrencyConfig -> ShowS)
-> (PickConcurrencyConfig -> String)
-> ([PickConcurrencyConfig] -> ShowS)
-> Show PickConcurrencyConfig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PickConcurrencyConfig -> ShowS
showsPrec :: Int -> PickConcurrencyConfig -> ShowS
$cshow :: PickConcurrencyConfig -> String
show :: PickConcurrencyConfig -> String
$cshowList :: [PickConcurrencyConfig] -> ShowS
showList :: [PickConcurrencyConfig] -> ShowS
Show)

defaultPickConcurrencyConfig :: PickConcurrencyConfig
defaultPickConcurrencyConfig :: PickConcurrencyConfig
defaultPickConcurrencyConfig = PickConcurrencyConfig
  { $sel:basicConfig:PickConcurrencyConfig :: BasicConfig
basicConfig = BasicConfig
defaultBasicConfig { $sel:atLeastActive:BasicConfig :: Int
atLeastActive = Int
2 }
  , $sel:changeConfig:PickConcurrencyConfig :: ChangeConfig
changeConfig = ChangeConfig
defaultChangeConfig
  , $sel:graphConfig:PickConcurrencyConfig :: GraphConfig
graphConfig = GraphConfig
defaultGraphConfig { $sel:hidePlaceNames:GraphConfig :: Bool
hidePlaceNames = Bool
True, $sel:hideTransitionNames:GraphConfig :: Bool
hideTransitionNames = Bool
True }
  , $sel:printSolution:PickConcurrencyConfig :: Bool
printSolution = Bool
False
  , $sel:prohibitSourceTransitions:PickConcurrencyConfig :: Bool
prohibitSourceTransitions = Bool
False
  , $sel:useDifferentGraphLayouts:PickConcurrencyConfig :: Bool
useDifferentGraphLayouts = Bool
False
  , $sel:alloyConfig:PickConcurrencyConfig :: AlloyConfig
alloyConfig  = AlloyConfig
defaultAlloyConfig
  , $sel:extraText:PickConcurrencyConfig :: Maybe (Map Language String)
extraText = Maybe (Map Language String)
forall a. Maybe a
Nothing
  }

data DrawSettings = DrawSettings {
  DrawSettings -> Bool
withPlaceNames       :: Bool,
  DrawSettings -> Bool
withSvgHighlighting  :: Bool,
  DrawSettings -> Bool
withTransitionNames  :: Bool,
  DrawSettings -> Bool
with1Weights         :: Bool,
  DrawSettings -> GraphvizCommand
withGraphvizCommand  :: GraphvizCommand
  } deriving (Typeable DrawSettings
Typeable DrawSettings
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> DrawSettings -> c DrawSettings)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DrawSettings)
-> (DrawSettings -> Constr)
-> (DrawSettings -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DrawSettings))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DrawSettings))
-> ((forall b. Data b => b -> b) -> DrawSettings -> DrawSettings)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DrawSettings -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DrawSettings -> r)
-> (forall u. (forall d. Data d => d -> u) -> DrawSettings -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> DrawSettings -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DrawSettings -> m DrawSettings)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DrawSettings -> m DrawSettings)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DrawSettings -> m DrawSettings)
-> Data DrawSettings
DrawSettings -> Constr
DrawSettings -> DataType
(forall b. Data b => b -> b) -> DrawSettings -> DrawSettings
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DrawSettings -> u
forall u. (forall d. Data d => d -> u) -> DrawSettings -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DrawSettings -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DrawSettings -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DrawSettings -> m DrawSettings
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DrawSettings -> m DrawSettings
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DrawSettings
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DrawSettings -> c DrawSettings
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DrawSettings)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DrawSettings)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DrawSettings -> c DrawSettings
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DrawSettings -> c DrawSettings
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DrawSettings
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DrawSettings
$ctoConstr :: DrawSettings -> Constr
toConstr :: DrawSettings -> Constr
$cdataTypeOf :: DrawSettings -> DataType
dataTypeOf :: DrawSettings -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DrawSettings)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DrawSettings)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DrawSettings)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DrawSettings)
$cgmapT :: (forall b. Data b => b -> b) -> DrawSettings -> DrawSettings
gmapT :: (forall b. Data b => b -> b) -> DrawSettings -> DrawSettings
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DrawSettings -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DrawSettings -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DrawSettings -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DrawSettings -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DrawSettings -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> DrawSettings -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DrawSettings -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> DrawSettings -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DrawSettings -> m DrawSettings
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DrawSettings -> m DrawSettings
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DrawSettings -> m DrawSettings
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DrawSettings -> m DrawSettings
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DrawSettings -> m DrawSettings
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DrawSettings -> m DrawSettings
Data, (forall x. DrawSettings -> Rep DrawSettings x)
-> (forall x. Rep DrawSettings x -> DrawSettings)
-> Generic DrawSettings
forall x. Rep DrawSettings x -> DrawSettings
forall x. DrawSettings -> Rep DrawSettings x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DrawSettings -> Rep DrawSettings x
from :: forall x. DrawSettings -> Rep DrawSettings x
$cto :: forall x. Rep DrawSettings x -> DrawSettings
to :: forall x. Rep DrawSettings x -> DrawSettings
Generic, ReadPrec [DrawSettings]
ReadPrec DrawSettings
Int -> ReadS DrawSettings
ReadS [DrawSettings]
(Int -> ReadS DrawSettings)
-> ReadS [DrawSettings]
-> ReadPrec DrawSettings
-> ReadPrec [DrawSettings]
-> Read DrawSettings
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS DrawSettings
readsPrec :: Int -> ReadS DrawSettings
$creadList :: ReadS [DrawSettings]
readList :: ReadS [DrawSettings]
$creadPrec :: ReadPrec DrawSettings
readPrec :: ReadPrec DrawSettings
$creadListPrec :: ReadPrec [DrawSettings]
readListPrec :: ReadPrec [DrawSettings]
Read, Int -> DrawSettings -> ShowS
[DrawSettings] -> ShowS
DrawSettings -> String
(Int -> DrawSettings -> ShowS)
-> (DrawSettings -> String)
-> ([DrawSettings] -> ShowS)
-> Show DrawSettings
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DrawSettings -> ShowS
showsPrec :: Int -> DrawSettings -> ShowS
$cshow :: DrawSettings -> String
show :: DrawSettings -> String
$cshowList :: [DrawSettings] -> ShowS
showList :: [DrawSettings] -> ShowS
Show)

deriving instance Data GraphvizCommand

type Drawable n = (n, DrawSettings)

{-|
Converts a 'GraphConfig' into 'DrawSettings' by choosing
the provided 'GraphvizCommand'.

Raises a runtime error if the provided 'GraphvizCommand' is not in the
'graphLayouts' list of the 'GraphConfig'.
-}
drawSettingsWithCommand :: GraphConfig -> GraphvizCommand -> DrawSettings
drawSettingsWithCommand :: GraphConfig -> GraphvizCommand -> DrawSettings
drawSettingsWithCommand GraphConfig
config GraphvizCommand
c
  | GraphvizCommand
c GraphvizCommand -> [GraphvizCommand] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` GraphConfig -> [GraphvizCommand]
graphLayouts GraphConfig
config = DrawSettings {
      $sel:withPlaceNames:DrawSettings :: Bool
withPlaceNames = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ GraphConfig -> Bool
hidePlaceNames GraphConfig
config,
      $sel:withSvgHighlighting:DrawSettings :: Bool
withSvgHighlighting = Bool
True,
      $sel:withTransitionNames:DrawSettings :: Bool
withTransitionNames = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ GraphConfig -> Bool
hideTransitionNames GraphConfig
config,
      $sel:with1Weights:DrawSettings :: Bool
with1Weights = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ GraphConfig -> Bool
hideWeight1 GraphConfig
config,
      $sel:withGraphvizCommand:DrawSettings :: GraphvizCommand
withGraphvizCommand = GraphvizCommand
c
    }
  | Bool
otherwise = String -> DrawSettings
forall a. HasCallStack => String -> a
error (String -> DrawSettings) -> String -> DrawSettings
forall a b. (a -> b) -> a -> b
$ String
"drawSettingsWithCommand: GraphvizCommand " String -> ShowS
forall a. [a] -> [a] -> [a]
++ GraphvizCommand -> String
forall a. Show a => a -> String
show GraphvizCommand
c
                     String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not in the allowed graphLayouts: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [GraphvizCommand] -> String
forall a. Show a => a -> String
show (GraphConfig -> [GraphvizCommand]
graphLayouts GraphConfig
config)

{-|
Provides a list of all 'DrawSetting' that can be obtained by using
'drawSettingsWithCommand' and all possible 'graphLayout's of the given config.
-}
allDrawSettings :: GraphConfig -> [DrawSettings]
allDrawSettings :: GraphConfig -> [DrawSettings]
allDrawSettings GraphConfig
config =
  (GraphvizCommand -> DrawSettings)
-> [GraphvizCommand] -> [DrawSettings]
forall a b. (a -> b) -> [a] -> [b]
map (GraphConfig -> GraphvizCommand -> DrawSettings
drawSettingsWithCommand GraphConfig
config) ([GraphvizCommand] -> [DrawSettings])
-> [GraphvizCommand] -> [DrawSettings]
forall a b. (a -> b) -> a -> b
$ GraphConfig -> [GraphvizCommand]
graphLayouts GraphConfig
config

transitionPairShow
  :: (Petri.Transition, Petri.Transition)
  -> (ShowTransition, ShowTransition)
transitionPairShow :: (Transition, Transition) -> (ShowTransition, ShowTransition)
transitionPairShow (Transition
t1, Transition
t2) =
  let (Transition
first, Transition
second) = if Transition
t1 Transition -> Transition -> Bool
forall a. Ord a => a -> a -> Bool
<= Transition
t2 then (Transition
t1, Transition
t2) else (Transition
t2, Transition
t1)
  in (Transition -> ShowTransition)
-> (Transition -> ShowTransition)
-> (Transition, Transition)
-> (ShowTransition, ShowTransition)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Transition -> ShowTransition
ShowTransition Transition -> ShowTransition
ShowTransition (Transition
first, Transition
second)

checkBasicConfig :: BasicConfig -> Maybe String
checkBasicConfig :: BasicConfig -> Maybe String
checkBasicConfig BasicConfig{
  Int
$sel:atLeastActive:BasicConfig :: BasicConfig -> Int
atLeastActive :: Int
atLeastActive,
  (Int, Int)
$sel:flowOverall:BasicConfig :: BasicConfig -> (Int, Int)
flowOverall :: (Int, Int)
flowOverall,
  Int
$sel:maxFlowPerEdge:BasicConfig :: BasicConfig -> Int
maxFlowPerEdge :: Int
maxFlowPerEdge,
  Int
$sel:maxTokensPerPlace:BasicConfig :: BasicConfig -> Int
maxTokensPerPlace :: Int
maxTokensPerPlace,
  Int
$sel:places:BasicConfig :: BasicConfig -> Int
places :: Int
places,
  (Int, Int)
$sel:tokensOverall:BasicConfig :: BasicConfig -> (Int, Int)
tokensOverall :: (Int, Int)
tokensOverall,
  Int
$sel:transitions:BasicConfig :: BasicConfig -> Int
transitions :: Int
transitions
  }
 | Int
places Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The number of places must be positive."
 | Int
places Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
8
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"Cannot deal with more than 8 places."
 | Int
transitions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The number of transitions must be positive."
 | Int
transitions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
8
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"Cannot deal with more than 8 transitions."
 | Int
atLeastActive Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'atLeastActive' must be non-negative."
 | Int
atLeastActive Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
transitions
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"There cannot be more active transitions than there are transitions."
 | (Int, Int) -> Int
forall a b. (a, b) -> a
fst (Int, Int)
tokensOverall Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The 'tokensOverall' must be non-negative."
 | (Int -> Int -> Bool) -> (Int, Int) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
(>) (Int, Int)
tokensOverall
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The minimum (first value) of 'tokensOverall' must not be larger than its maximum (second value)."
 | Int
maxTokensPerPlace Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'maxTokensPerPlace' must be non-negative."
 | Int
maxTokensPerPlace Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> (Int, Int) -> Int
forall a b. (a, b) -> b
snd (Int, Int)
tokensOverall
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'maxTokensPerPlace' must not be larger than the maximum 'tokensOverall'."
 | (Int, Int) -> Int
forall a b. (a, b) -> b
snd (Int, Int)
tokensOverall Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
places Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
maxTokensPerPlace
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The maximum 'tokensOverall' is set unreasonably high, given the per-place parameter."
 | (Int, Int) -> Int
forall a b. (a, b) -> a
fst (Int, Int)
flowOverall Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The 'flowOverall' must be non-negative."
 | (Int -> Int -> Bool) -> (Int, Int) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
(>) (Int, Int)
flowOverall
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The minimum (first value) of 'flowOverall' must not be larger than its maximum (second value)."
 | Int
maxFlowPerEdge Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'maxFlowPerEdge' must be positive."
 | (Int, Int) -> Int
forall a b. (a, b) -> b
snd (Int, Int)
flowOverall Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
maxFlowPerEdge
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'maxFlowPerEdge' must not be larger than the maximum 'flowOverall'."
 | (Int, Int) -> Int
forall a b. (a, b) -> b
snd (Int, Int)
flowOverall Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
places Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
transitions Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
maxFlowPerEdge
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The maximum 'flowOverall' is set unreasonably high, given the other parameters."
 | Int
transitions Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
places Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int, Int) -> Int
forall a b. (a, b) -> a
fst (Int, Int)
flowOverall
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The number of transitions and places exceeds the minimum 'flowOverall' too much to create a connected net."
 | Bool
otherwise
  = Maybe String
forall a. Maybe a
Nothing

checkChangeConfig :: BasicConfig -> ChangeConfig -> Maybe String
checkChangeConfig :: BasicConfig -> ChangeConfig -> Maybe String
checkChangeConfig
  BasicConfig {
    Int
$sel:places:BasicConfig :: BasicConfig -> Int
places :: Int
places,
    Int
$sel:transitions:BasicConfig :: BasicConfig -> Int
transitions :: Int
transitions,
    (Int, Int)
$sel:flowOverall:BasicConfig :: BasicConfig -> (Int, Int)
flowOverall :: (Int, Int)
flowOverall,
    Int
$sel:maxTokensPerPlace:BasicConfig :: BasicConfig -> Int
maxTokensPerPlace :: Int
maxTokensPerPlace,
    Int
$sel:maxFlowPerEdge:BasicConfig :: BasicConfig -> Int
maxFlowPerEdge :: Int
maxFlowPerEdge,
    (Int, Int)
$sel:tokensOverall:BasicConfig :: BasicConfig -> (Int, Int)
tokensOverall :: (Int, Int)
tokensOverall
    }
  ChangeConfig {
    Int
$sel:tokenChangeOverall:ChangeConfig :: ChangeConfig -> Int
tokenChangeOverall :: Int
tokenChangeOverall,
    Int
$sel:flowChangeOverall:ChangeConfig :: ChangeConfig -> Int
flowChangeOverall :: Int
flowChangeOverall,
    Int
$sel:maxFlowChangePerEdge:ChangeConfig :: ChangeConfig -> Int
maxFlowChangePerEdge :: Int
maxFlowChangePerEdge,
    Int
$sel:maxTokenChangePerPlace:ChangeConfig :: ChangeConfig -> Int
maxTokenChangePerPlace :: Int
maxTokenChangePerPlace
    }
 | Int
tokenChangeOverall Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'tokenChangeOverall' must be non-negative."
 | Int
maxTokenChangePerPlace Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'maxTokenChangePerPlace' must be non-negative."
 | Int
maxTokenChangePerPlace Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
tokenChangeOverall
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'maxTokenChangePerPlace' must not be larger than 'tokenChangeOverall'."
 | Int
maxTokenChangePerPlace Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxTokensPerPlace
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'maxTokenChangePerPlace' must not be larger than maximum 'tokensPerPlace'."
 | Int
tokenChangeOverall Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* (Int, Int) -> Int
forall a b. (a, b) -> b
snd (Int, Int)
tokensOverall
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'tokenChangeOverall' is set unreasonably high, given the maximal tokens overall."
 | Int
maxTokenChangePerPlace Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
places Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
tokenChangeOverall
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'tokenChangeOverall' is set unreasonably high, given the per-place parameter."
 | Int
flowChangeOverall Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'flowChangeOverall' must be non-negative."
 | Int
maxFlowChangePerEdge Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'maxFlowChangePerEdge' must be non-negative."
 | Int
maxFlowChangePerEdge Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
flowChangeOverall
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'maxFlowChangePerEdge' must not be larger than 'flowChangeOverall'."
 | Int
maxFlowChangePerEdge Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxFlowPerEdge
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'maxFlowChangePerEdge' must not be larger than 'maxFlowPerEdge'."
 | Int
flowChangeOverall Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* (Int, Int) -> Int
forall a b. (a, b) -> b
snd (Int, Int)
flowOverall
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'flowChangeOverall' is set unreasonable high, given the maximal flow overall."
 | Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
places Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
transitions Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
maxFlowChangePerEdge Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
flowChangeOverall
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'flowChangeOverall' is set unreasonably high, given the other parameters."
 | Int -> Bool
forall a. Integral a => a -> Bool
odd Int
tokenChangeOverall Bool -> Bool -> Bool
&& (Int -> Int -> Bool) -> (Int, Int) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Int, Int)
tokensOverall
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"If 'tokenChangeOverall' is odd, then 'tokensOverall' should not contain two equal values (configuration would be unsatisfiable)."
 | Int -> Bool
forall a. Integral a => a -> Bool
odd Int
flowChangeOverall Bool -> Bool -> Bool
&& (Int -> Int -> Bool) -> (Int, Int) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Int, Int)
flowOverall
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"If 'flowChangeOverall' is odd, then 'flowOverall' should not contain two equal values (configuration would be unsatisfiable)."
 | Bool
otherwise
  = Maybe String
forall a. Maybe a
Nothing

checkGraphLayouts :: Bool -> Int -> GraphConfig -> Maybe String
checkGraphLayouts :: Bool -> Int -> GraphConfig -> Maybe String
checkGraphLayouts Bool
useDifferent Int
wrongInstances GraphConfig
gc
  | [GraphvizCommand] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (GraphConfig -> [GraphvizCommand]
graphLayouts GraphConfig
gc)
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"At least one graph layout needs to be provided."
  | Bool
useDifferent Bool -> Bool -> Bool
&& Bool -> Bool
not (Int -> Int -> Bool
hasValidLayoutDistribution Int
numberOfGraphs ([GraphvizCommand] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([GraphvizCommand] -> Int) -> [GraphvizCommand] -> Int
forall a b. (a -> b) -> a -> b
$ GraphConfig -> [GraphvizCommand]
graphLayouts GraphConfig
gc))
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'graphLayout' needs to allow even distribution of graphs when 'useDifferentGraphLayouts' is set."
  | Bool
otherwise
  = Maybe String
forall a. Maybe a
Nothing
  where
    -- Total number of graphs: 1 correct + wrongInstances wrong graphs
    numberOfGraphs :: Int
numberOfGraphs = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
wrongInstances

-- | Check if we can distribute numberOfGraphs graphs among numLayouts layouts
-- such that we use n different layouts where 1 < n <= numLayouts and numberOfGraphs mod n == 0
hasValidLayoutDistribution :: Int -> Int -> Bool
hasValidLayoutDistribution :: Int -> Int -> Bool
hasValidLayoutDistribution Int
numberOfGraphs Int
numLayouts =
  (Int -> Bool) -> Marking -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Int
n -> Int
numberOfGraphs Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) [Int
2..Int
numLayouts]

-- | Check if the count of nodes in a Petri net falls within the given bounds
checkPetriNodeCount :: (Net p n, Ord a) => (Int, Maybe Int) -> p n a -> Bool
checkPetriNodeCount :: forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
(Int, Maybe Int) -> p n a -> Bool
checkPetriNodeCount (Int, Maybe Int)
countOfPetriNodesBounds p n a
petri =
  let count :: Int
count = Map a (n a) -> Int
forall k a. Map k a -> Int
M.size (Map a (n a) -> Int) -> Map a (n a) -> Int
forall a b. (a -> b) -> a -> b
$ p n a -> Map a (n a)
forall a. Ord a => p n a -> Map a (n a)
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
p n a -> Map a (n a)
nodes p n a
petri
  in (Int, Maybe Int) -> Int
forall a b. (a, b) -> a
fst (Int, Maybe Int)
countOfPetriNodesBounds Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
count
     Bool -> Bool -> Bool
&& Bool -> (Int -> Bool) -> Maybe Int -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (Int
count Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<=) ((Int, Maybe Int) -> Maybe Int
forall a b. (a, b) -> b
snd (Int, Maybe Int)
countOfPetriNodesBounds)