{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE CPP #-}
{-# 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,
  )

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 (
  ($>>=),
  )
#if !MIN_VERSION_base(4,20,0)
import Data.Foldable                    (Foldable (foldl'))
#endif
import Data.GraphViz                    (GraphvizCommand)

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 = 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