{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE FlexibleContexts #-}
{-|
originally from Autotool (https://gitlab.imn.htwk-leipzig.de/autotool/all0)
based on revision: ad25a990816a162fdd13941ff889653f22d6ea0a
based on file: collection/src/Petri/Step.hs
-}
module Modelling.PetriNet.Reach.Step where

import qualified Data.Map                         as M (
  insert,
  findWithDefault,
  fromList,
  toList,
  )
import qualified Data.Set                         as S (
  difference,
  empty,
  fromList,
  member,
  toList,
  union,
  )

import Capabilities.Cache               (MonadCache)
import Capabilities.Diagrams            (MonadDiagrams)
import Capabilities.Graphviz            (MonadGraphviz)
import Modelling.PetriNet.Reach.Draw    (drawToFile)
import Modelling.PetriNet.Reach.Type (
  Net (capacity, connections, start),
  State (State),
  allNonNegative,
  conforms,
  )

import Control.Applicative              (Alternative)
import Control.Functor.Trans            (FunctorTrans (lift))
import Control.Monad                    (unless)
import Control.Monad.Catch              (MonadThrow)
import Control.OutputCapable.Blocks (
  GenericOutputCapable (image, indent, paragraph, refuse, text),
  LangM',
  OutputCapable,
  ($=<<),
  english,
  german,
  recoverWith,
  translate,
  unLangM,
  )
import Control.OutputCapable.Blocks.Generic (
  ($>>=),
  )
import Data.Foldable                    (foldl')
import Data.GraphViz                    (GraphvizCommand)

deadlocks :: Ord s => Net s t -> [[State s]]
deadlocks :: forall s t. Ord s => Net s t -> [[State s]]
deadlocks Net s t
n = ([State s] -> [State s]) -> [[State s]] -> [[State s]]
forall a b. (a -> b) -> [a] -> [b]
map ((State s -> Bool) -> [State s] -> [State s]
forall a. (a -> Bool) -> [a] -> [a]
filter ([(t, State s)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(t, State s)] -> Bool)
-> (State s -> [(t, State s)]) -> State s -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Net s t -> State s -> [(t, State s)]
forall s t. Ord s => Net s t -> State s -> [(t, State s)]
successors Net s t
n)) (Net s t -> [[State s]]
forall s t. Ord s => Net s t -> [[State s]]
levels Net s t
n)

{-|
The returned trace for each state is in reversed order,
i.e., undoing the firing on the returned deadlock state
in order of the returned transitions list
leads to the initial state of the net.
(Only states of and traces to deadlocks are returned.)
-}
deadlocks' :: Ord s => Net s t -> [[(State s, [t])]]
deadlocks' :: forall s t. Ord s => Net s t -> [[(State s, [t])]]
deadlocks' Net s t
n = ([(State s, [t])] -> [(State s, [t])])
-> [[(State s, [t])]] -> [[(State s, [t])]]
forall a b. (a -> b) -> [a] -> [b]
map (((State s, [t]) -> Bool) -> [(State s, [t])] -> [(State s, [t])]
forall a. (a -> Bool) -> [a] -> [a]
filter ([(t, State s)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(t, State s)] -> Bool)
-> ((State s, [t]) -> [(t, State s)]) -> (State s, [t]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Net s t -> State s -> [(t, State s)]
forall s t. Ord s => Net s t -> State s -> [(t, State s)]
successors Net s t
n (State s -> [(t, State s)])
-> ((State s, [t]) -> State s) -> (State s, [t]) -> [(t, State s)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State s, [t]) -> State s
forall a b. (a, b) -> a
fst)) (Net s t -> [[(State s, [t])]]
forall s t. Ord s => Net s t -> [[(State s, [t])]]
levels' Net s t
n)

levels :: Ord s => Net s t -> [[State s]]
levels :: forall s t. Ord s => Net s t -> [[State s]]
levels Net s t
n =
  let f :: Set (State s) -> [State s] -> [[State s]]
f Set (State s)
_    [] = []
      f Set (State s)
done [State s]
xs =
        let done' :: Set (State s)
done' = Set (State s) -> Set (State s) -> Set (State s)
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (State s)
done (Set (State s) -> Set (State s)) -> Set (State s) -> Set (State s)
forall a b. (a -> b) -> a -> b
$ [State s] -> Set (State s)
forall a. Ord a => [a] -> Set a
S.fromList [State s]
xs
            next :: Set (State s)
next = [State s] -> Set (State s)
forall a. Ord a => [a] -> Set a
S.fromList [ State s
y | State s
x <- [State s]
xs, (t
_,State s
y) <- Net s t -> State s -> [(t, State s)]
forall s t. Ord s => Net s t -> State s -> [(t, State s)]
successors Net s t
n State s
x]
         in [State s]
xs [State s] -> [[State s]] -> [[State s]]
forall a. a -> [a] -> [a]
:
            Set (State s) -> [State s] -> [[State s]]
f
              Set (State s)
done'
              (Set (State s) -> [State s]
forall a. Set a -> [a]
S.toList (Set (State s) -> [State s]) -> Set (State s) -> [State s]
forall a b. (a -> b) -> a -> b
$ Set (State s) -> Set (State s) -> Set (State s)
forall a. Ord a => Set a -> Set a -> Set a
S.difference Set (State s)
next Set (State s)
done')
  in Set (State s) -> [State s] -> [[State s]]
f Set (State s)
forall a. Set a
S.empty [Net s t -> State s
forall s t. Net s t -> State s
start Net s t
n]

{-|
The returned trace for each state is in reversed order,
i.e., undoing the firing on the returned target state
in order of the returned transitions list
leads to the initial state of the net.
-}
levels'
  :: Ord s
  => Net s t
  -> [[(State s, [t])]]
levels' :: forall s t. Ord s => Net s t -> [[(State s, [t])]]
levels' Net s t
n =
  let f :: Set (State s) -> [(State s, [t])] -> [[(State s, [t])]]
f Set (State s)
_    [] = []
      f Set (State s)
done [(State s, [t])]
xs =
        let done' :: Set (State s)
done' = Set (State s) -> Set (State s) -> Set (State s)
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (State s)
done (Set (State s) -> Set (State s)) -> Set (State s) -> Set (State s)
forall a b. (a -> b) -> a -> b
$ [State s] -> Set (State s)
forall a. Ord a => [a] -> Set a
S.fromList ([State s] -> Set (State s)) -> [State s] -> Set (State s)
forall a b. (a -> b) -> a -> b
$ ((State s, [t]) -> State s) -> [(State s, [t])] -> [State s]
forall a b. (a -> b) -> [a] -> [b]
map (State s, [t]) -> State s
forall a b. (a, b) -> a
fst [(State s, [t])]
xs
            next :: [(State s, [t])]
next = Map (State s) [t] -> [(State s, [t])]
forall k a. Map k a -> [(k, a)]
M.toList (Map (State s) [t] -> [(State s, [t])])
-> Map (State s) [t] -> [(State s, [t])]
forall a b. (a -> b) -> a -> b
$ [(State s, [t])] -> Map (State s) [t]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (State s
y, t
tt -> [t] -> [t]
forall a. a -> [a] -> [a]
:[t]
p) |
                (State s
x,[t]
p) <- [(State s, [t])]
xs,
                (t
t,State s
y) <- Net s t -> State s -> [(t, State s)]
forall s t. Ord s => Net s t -> State s -> [(t, State s)]
successors Net s t
n State s
x,
                Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ State s -> Set (State s) -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member State s
y Set (State s)
done'
              ]
         in [(State s, [t])]
xs [(State s, [t])] -> [[(State s, [t])]] -> [[(State s, [t])]]
forall a. a -> [a] -> [a]
: Set (State s) -> [(State s, [t])] -> [[(State s, [t])]]
f Set (State s)
done' [(State s, [t])]
next
  in Set (State s) -> [(State s, [t])] -> [[(State s, [t])]]
f Set (State s)
forall a. Set a
S.empty [(Net s t -> State s
forall s t. Net s t -> State s
start Net s t
n, [])]

equalling :: Eq a => (t -> a) -> t -> t -> Bool
equalling :: forall a t. Eq a => (t -> a) -> t -> t -> Bool
equalling t -> a
f t
x t
y = t -> a
f t
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== t -> a
f t
y

--executesPlain n ts = result $ executes n ts

executes
  :: (
    Alternative m,
    MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    Ord s,
    Ord t,
    OutputCapable m,
    Show s,
    Show t
    )
  => FilePath
  -> GraphvizCommand
  -> Net s t
  -> [t]
  -> LangM' m (Either Int (State s))
executes :: forall (m :: * -> *) s t.
(Alternative m, MonadCache m, MonadDiagrams m, MonadGraphviz m,
 MonadThrow m, Ord s, Ord t, OutputCapable m, Show s, Show t) =>
FilePath
-> GraphvizCommand
-> Net s t
-> [t]
-> LangM' m (Either Int (State s))
executes FilePath
path GraphvizCommand
cmd Net s t
n [t]
ts = (LangM' m (Either Int (State s))
 -> (Int, t) -> LangM' m (Either Int (State s)))
-> LangM' m (Either Int (State s))
-> [(Int, t)]
-> LangM' m (Either Int (State s))
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
  (\LangM' m (Either Int (State s))
z (Int
k, t
t) -> (Int -> LangM' m (Either Int (State s)))
-> (State s -> LangM' m (Either Int (State s)))
-> Either Int (State s)
-> LangM' m (Either Int (State s))
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Either Int (State s) -> LangM' m (Either Int (State s))
forall a. a -> GenericLangM Language m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Int (State s) -> LangM' m (Either Int (State s)))
-> (Int -> Either Int (State s))
-> Int
-> LangM' m (Either Int (State s))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Either Int (State s)
forall a b. a -> Either a b
Left) (Int -> t -> State s -> LangM' m (Either Int (State s))
forall {m :: * -> *} {a}.
(Alternative m, Num a, GenericOutputCapable Language m,
 MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m,
 Show a) =>
a -> t -> State s -> GenericLangM Language m (Either a (State s))
step Int
k t
t) (Either Int (State s) -> LangM' m (Either Int (State s)))
-> m (Either Int (State s)) -> LangM' m (Either Int (State s))
forall (m :: * -> *) a l b.
Monad m =>
(a -> GenericLangM l m b) -> m a -> GenericLangM l m b
$=<< LangM' m (Either Int (State s)) -> m (Either Int (State s))
forall l (m :: * -> *) a. GenericLangM l m a -> m a
unLangM LangM' m (Either Int (State s))
z)
  (Either Int (State s) -> LangM' m (Either Int (State s))
forall a. a -> GenericLangM Language m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Int (State s) -> LangM' m (Either Int (State s)))
-> Either Int (State s) -> LangM' m (Either Int (State s))
forall a b. (a -> b) -> a -> b
$ State s -> Either Int (State s)
forall a b. b -> Either a b
Right (State s -> Either Int (State s))
-> State s -> Either Int (State s)
forall a b. (a -> b) -> a -> b
$ Net s t -> State s
forall s t. Net s t -> State s
start Net s t
n)
  ([Int] -> [t] -> [(Int, t)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1 :: Int ..] [t]
ts)
  where
    step :: a -> t -> State s -> GenericLangM Language m (Either a (State s))
step a
k t
t State s
z = a
-> GenericLangM Language m (State s)
-> GenericLangM Language m (Either a (State s))
forall (m :: * -> *) a l b.
Alternative m =>
a -> GenericLangM l m b -> GenericLangM l m (Either a b)
recoverWith (a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
1) (GenericLangM Language m (State s)
 -> GenericLangM Language m (Either a (State s)))
-> GenericLangM Language m (State s)
-> GenericLangM Language m (Either a (State s))
forall a b. (a -> b) -> a -> b
$ do
      GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State (Map Language FilePath) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l FilePath) () -> GenericLangM l m ()
translate (State (Map Language FilePath) () -> GenericLangM Language m ())
-> State (Map Language FilePath) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
        FilePath -> State (Map Language FilePath) ()
english (FilePath -> State (Map Language FilePath) ())
-> FilePath -> State (Map Language FilePath) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Step " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
k
        FilePath -> State (Map Language FilePath) ()
german (FilePath -> State (Map Language FilePath) ())
-> FilePath -> State (Map Language FilePath) ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Schritt " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
k
      State s
next <- FilePath
-> GraphvizCommand
-> Net s t
-> t
-> State s
-> GenericLangM Language m (State s)
forall (m :: * -> *) a k.
(MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m,
 Ord a, Ord k, OutputCapable m, Show a, Show k) =>
FilePath
-> GraphvizCommand -> Net k a -> a -> State k -> LangM' m (State k)
executeIO FilePath
path GraphvizCommand
cmd Net s t
n t
t State s
z
      pure State s
next

executeIO
  :: (
    MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    Ord a,
    Ord k,
    OutputCapable m,
    Show a,
    Show k
    )
  => FilePath
  -> GraphvizCommand
  -> Net k a
  -> a
  -> State k
  -> LangM' m (State k)
executeIO :: forall (m :: * -> *) a k.
(MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m,
 Ord a, Ord k, OutputCapable m, Show a, Show k) =>
FilePath
-> GraphvizCommand -> Net k a -> a -> State k -> LangM' m (State k)
executeIO FilePath
path GraphvizCommand
cmd Net k a
n a
t State k
z0 = Net k a -> a -> State k -> LangM' m (State k)
forall (m :: * -> *) a k.
(Monad m, Ord a, Ord k, OutputCapable m, Show a, Show k) =>
Net k a -> a -> State k -> LangM' m (State k)
execute Net k a
n a
t State k
z0
  LangM' m (State k)
-> (State k -> LangM' m (State k)) -> LangM' m (State k)
forall (m :: * -> *) l a b.
Monad m =>
GenericLangM l m a
-> (a -> GenericLangM l m b) -> GenericLangM l m b
$>>= \State k
z2 -> m FilePath -> GenericLangM Language m FilePath
forall (f :: * -> *) a.
Functor f =>
f a -> GenericLangM Language f a
forall (t :: (* -> *) -> * -> *) (f :: * -> *) a.
(FunctorTrans t, Functor f) =>
f a -> t f a
lift (Bool -> FilePath -> GraphvizCommand -> Net k a -> m FilePath
forall s t (m :: * -> *).
(Ord s, Ord t, Show s, Show t, MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m) =>
Bool -> FilePath -> GraphvizCommand -> Net s t -> m FilePath
drawToFile Bool
False FilePath
path GraphvizCommand
cmd (Net k a
n {start :: State k
start = State k
z2}))
  GenericLangM Language m FilePath
-> (FilePath -> LangM' m (State k)) -> LangM' m (State k)
forall (m :: * -> *) l a b.
Monad m =>
GenericLangM l m a
-> (a -> GenericLangM l m b) -> GenericLangM l m b
$>>= \FilePath
g -> FilePath -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
FilePath -> GenericLangM l m ()
image FilePath
g
  GenericLangM Language m ()
-> (() -> LangM' m (State k)) -> LangM' m (State k)
forall (m :: * -> *) l a b.
Monad m =>
GenericLangM l m a
-> (a -> GenericLangM l m b) -> GenericLangM l m b
$>>= LangM' m (State k) -> () -> LangM' m (State k)
forall a. a -> () -> a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (State k -> LangM' m (State k)
forall a. a -> GenericLangM Language m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure State k
z2)

execute
  :: (Monad m, Ord a, Ord k, OutputCapable m, Show a, Show k)
  => Net k a
  -> a
  -> State k
  -> LangM' m (State k)
execute :: forall (m :: * -> *) a k.
(Monad m, Ord a, Ord k, OutputCapable m, Show a, Show k) =>
Net k a -> a -> State k -> LangM' m (State k)
execute Net k a
n a
t State k
z0 = do
  GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (FilePath -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
FilePath -> GenericLangM l m ()
text (FilePath -> GenericLangM Language m ())
-> FilePath -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Transition " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
t)
  State k
next <- case [Connection k a]
cs of
    [] -> do
      GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State (Map Language FilePath) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l FilePath) () -> GenericLangM l m ()
translate (State (Map Language FilePath) () -> GenericLangM Language m ())
-> State (Map Language FilePath) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
        FilePath -> State (Map Language FilePath) ()
english FilePath
"does not exist!"
        FilePath -> State (Map Language FilePath) ()
german FilePath
"existiert nicht!"
      pure State k
z0
    [([k]
vor, a
_, [k]
nach)] -> do
      let z1 :: State k
z1 = (Int -> Int) -> [k] -> State k -> State k
forall s. Ord s => (Int -> Int) -> [s] -> State s -> State s
change Int -> Int
forall a. Enum a => a -> a
pred [k]
vor State k
z0
      GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State (Map Language FilePath) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l FilePath) () -> GenericLangM l m ()
translate (State (Map Language FilePath) () -> GenericLangM Language m ())
-> State (Map Language FilePath) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
        FilePath -> State (Map Language FilePath) ()
english FilePath
"Intermediate marking (after collecting tokens)"
        FilePath -> State (Map Language FilePath) ()
german FilePath
"Zwischenmarkierung (nach Einziehen der Marken im Vorbereich)"
      GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
indent (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ FilePath -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
FilePath -> GenericLangM l m ()
text (FilePath -> GenericLangM Language m ())
-> FilePath -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State k -> FilePath
forall a. Show a => a -> FilePath
show State k
z1
      Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (State k -> Bool
forall a. State a -> Bool
allNonNegative State k
z1) (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State (Map Language FilePath) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l FilePath) () -> GenericLangM l m ()
translate (State (Map Language FilePath) () -> GenericLangM Language m ())
-> State (Map Language FilePath) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
        FilePath -> State (Map Language FilePath) ()
english FilePath
"Contains negative token count (transition was not activated)!"
        FilePath -> State (Map Language FilePath) ()
german FilePath
"Enthält negative Markenanzahl (Transition war nicht aktiviert)!"
      let z2 :: State k
z2 = (Int -> Int) -> [k] -> State k -> State k
forall s. Ord s => (Int -> Int) -> [s] -> State s -> State s
change Int -> Int
forall a. Enum a => a -> a
succ [k]
nach State k
z1
      GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State (Map Language FilePath) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l FilePath) () -> GenericLangM l m ()
translate (State (Map Language FilePath) () -> GenericLangM Language m ())
-> State (Map Language FilePath) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
        FilePath -> State (Map Language FilePath) ()
english FilePath
"Final marking (after distributing tokens)"
        FilePath -> State (Map Language FilePath) ()
german FilePath
"Endmarkierung (nach Austeilen der Marken im Nachbereich)"
      GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
indent (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ FilePath -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
FilePath -> GenericLangM l m ()
text (FilePath -> GenericLangM Language m ())
-> FilePath -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State k -> FilePath
forall a. Show a => a -> FilePath
show State k
z2
      Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Capacity k -> State k -> Bool
forall k. Ord k => Capacity k -> State k -> Bool
conforms (Net k a -> Capacity k
forall s t. Net s t -> Capacity s
capacity Net k a
n) State k
z2) (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State (Map Language FilePath) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l FilePath) () -> GenericLangM l m ()
translate (State (Map Language FilePath) () -> GenericLangM Language m ())
-> State (Map Language FilePath) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
        FilePath -> State (Map Language FilePath) ()
english FilePath
"contains more tokens than capacity permits!"
        FilePath -> State (Map Language FilePath) ()
german FilePath
"enthält mehr Marken, als die Kapazität zulässt!"
      pure State k
z2
    [Connection k a]
_ -> LangM' m (State k)
forall a. HasCallStack => a
undefined -- TODO Patern match not required?
  pure State k
next
  where
    cs :: [Connection k a]
cs = [ Connection k a
c | c :: Connection k a
c@([k]
_, a
t', [k]
_) <- Net k a -> [Connection k a]
forall s t. Net s t -> [Connection s t]
connections Net k a
n, a
t' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
t]

successors
  :: Ord s
  => Net s t
  -> State s
  -> [(t, State s)]
successors :: forall s t. Ord s => Net s t -> State s -> [(t, State s)]
successors Net s t
n State s
z0 = [ (t
t, State s
z2) |
    ([s]
vor, t
t, [s]
nach) <- Net s t -> [([s], t, [s])]
forall s t. Net s t -> [Connection s t]
connections Net s t
n,
    let z1 :: State s
z1 = (Int -> Int) -> [s] -> State s -> State s
forall s. Ord s => (Int -> Int) -> [s] -> State s -> State s
change Int -> Int
forall a. Enum a => a -> a
pred [s]
vor State s
z0,
    State s -> Bool
forall a. State a -> Bool
allNonNegative State s
z1,
    let z2 :: State s
z2 = (Int -> Int) -> [s] -> State s -> State s
forall s. Ord s => (Int -> Int) -> [s] -> State s -> State s
change Int -> Int
forall a. Enum a => a -> a
succ [s]
nach State s
z1,
    Capacity s -> State s -> Bool
forall k. Ord k => Capacity k -> State k -> Bool
conforms (Net s t -> Capacity s
forall s t. Net s t -> Capacity s
capacity Net s t
n) State s
z2
  ]

change
  :: Ord s
  => (Int -> Int)
  -> [s]
  -> State s
  -> State s
change :: forall s. Ord s => (Int -> Int) -> [s] -> State s -> State s
change Int -> Int
f [s]
ps (State Map s Int
z) =
  Map s Int -> State s
forall s. Map s Int -> State s
State (Map s Int -> State s) -> Map s Int -> State s
forall a b. (a -> b) -> a -> b
$ (Map s Int -> s -> Map s Int) -> Map s Int -> [s] -> Map s Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
    (\Map s Int
z' s
p -> s -> Int -> Map s Int -> Map s Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert s
p (Int -> Int
f (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Int -> s -> Map s Int -> Int
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault Int
0 s
p Map s Int
z') Map s Int
z')
    Map s Int
z
    [s]
ps