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

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

import qualified Data.Map                         as M (
  elems,
  filter,
  fromListWith,
  keysSet,
  null,
  )
import qualified Data.Set                         as S (
  difference,
  member,
  null,
  size,
  )

import Modelling.PetriNet.Reach.Step    (execute)
import Modelling.PetriNet.Reach.Type (
  Net (capacity, connections, places, start, transitions),
  Capacity (..),
  State (unState),
  allNonNegative,
  conforms,
  )

import Control.Monad                    (foldM, unless, when)
import Control.Monad.Identity           (Identity (runIdentity))
import Control.OutputCapable.Blocks (
  GenericOutputCapable (indent, paragraph, refuse, text),
  LangM,
  Language,
  OutputCapable,
  )
import Control.OutputCapable.Blocks.Generic (
  evalLangM,
  )
import Data.Either                      (fromLeft)
import Data.Foldable                    (for_)
import Data.Typeable                    (Typeable)
import GHC.Generics                     (Generic)

data Property
  = Default
  | MaxNumPlaces Int
  | MaxNumTransitions Int
  | MaxEdgeMultiplicity Int
  | MaxInitialTokens Int
  | Capacity (Capacity ())
  deriving (Typeable, (forall x. Property -> Rep Property x)
-> (forall x. Rep Property x -> Property) -> Generic Property
forall x. Rep Property x -> Property
forall x. Property -> Rep Property x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Property -> Rep Property x
from :: forall x. Property -> Rep Property x
$cto :: forall x. Rep Property x -> Property
to :: forall x. Rep Property x -> Property
Generic)

validates
  :: (Foldable f, Ord a, Ord b, OutputCapable m, Show a, Show b)
  => f Property
  -> Net a b
  -> LangM m
validates :: forall (f :: * -> *) a b (m :: * -> *).
(Foldable f, Ord a, Ord b, OutputCapable m, Show a, Show b) =>
f Property -> Net a b -> LangM m
validates f Property
props Net a b
n = f Property
-> (Property -> GenericLangM Language m ())
-> GenericLangM Language m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ f Property
props ((Property -> GenericLangM Language m ())
 -> GenericLangM Language m ())
-> (Property -> GenericLangM Language m ())
-> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ \Property
prop -> Property -> Net a b -> GenericLangM Language m ()
forall a t (m :: * -> *).
(Ord a, Ord t, OutputCapable m, Show a, Show t) =>
Property -> Net a t -> LangM m
validate Property
prop Net a b
n

validate
  :: (Ord a, Ord t, OutputCapable m, Show a, Show t)
  => Property
  -> Net a t
  -> LangM m
validate :: forall a t (m :: * -> *).
(Ord a, Ord t, OutputCapable m, Show a, Show t) =>
Property -> Net a t -> LangM m
validate Property
p Net a t
n = case Property
p of
  MaxNumPlaces Int
m -> String -> Int -> Int -> LangM m
forall a (m :: * -> *).
(Ord a, OutputCapable m, Show a) =>
String -> a -> a -> LangM m
guardBound
    String
"Anzahl der Stellen"
    (Set a -> Int
forall a. Set a -> Int
S.size (Set a -> Int) -> Set a -> Int
forall a b. (a -> b) -> a -> b
$ Net a t -> Set a
forall s t. Net s t -> Set s
places Net a t
n)
    Int
m
  MaxNumTransitions Int
m -> String -> Int -> Int -> LangM m
forall a (m :: * -> *).
(Ord a, OutputCapable m, Show a) =>
String -> a -> a -> LangM m
guardBound
    String
"Anzahl der Transitionen"
    (Set t -> Int
forall a. Set a -> Int
S.size (Set t -> Int) -> Set t -> Int
forall a b. (a -> b) -> a -> b
$ Net a t -> Set t
forall s t. Net s t -> Set t
transitions Net a t
n)
    Int
m
  MaxInitialTokens Int
m -> String -> Int -> Int -> LangM m
forall a (m :: * -> *).
(Ord a, OutputCapable m, Show a) =>
String -> a -> a -> LangM m
guardBound
    String
"Anzahl der Token in Startmarkierung"
    ([Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ Map a Int -> [Int]
forall k a. Map k a -> [a]
M.elems (Map a Int -> [Int]) -> Map a Int -> [Int]
forall a b. (a -> b) -> a -> b
$ State a -> Map a Int
forall s. State s -> Map s Int
unState (State a -> Map a Int) -> State a -> Map a Int
forall a b. (a -> b) -> a -> b
$ Net a t -> State a
forall s t. Net s t -> State s
start Net a t
n)
    Int
m
  MaxEdgeMultiplicity Int
m ->
    [Connection a t] -> (Connection a t -> LangM m) -> LangM m
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (Net a t -> [Connection a t]
forall s t. Net s t -> [Connection s t]
connections Net a t
n) ((Connection a t -> LangM m) -> LangM m)
-> (Connection a t -> LangM m) -> LangM m
forall a b. (a -> b) -> a -> b
$ \c :: Connection a t
c@([a]
vor, t
_, [a]
nach) -> do
      let badVor :: Map a Int
badVor =
            (Int -> Bool) -> Map a Int -> Map a Int
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
m) (Map a Int -> Map a Int) -> Map a Int -> Map a Int
forall a b. (a -> b) -> a -> b
$
              (Int -> Int -> Int) -> [(a, Int)] -> Map a Int
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) ([(a, Int)] -> Map a Int) -> [(a, Int)] -> Map a Int
forall a b. (a -> b) -> a -> b
$ (a -> (a, Int)) -> [a] -> [(a, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (,Int
1) [a]
vor
          badNach :: Map a Int
badNach =
            (Int -> Bool) -> Map a Int -> Map a Int
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
m) (Map a Int -> Map a Int) -> Map a Int -> Map a Int
forall a b. (a -> b) -> a -> b
$
              (Int -> Int -> Int) -> [(a, Int)] -> Map a Int
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) ([(a, Int)] -> Map a Int) -> [(a, Int)] -> Map a Int
forall a b. (a -> b) -> a -> b
$ (a -> (a, Int)) -> [a] -> [(a, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (,Int
1) [a]
nach
      Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Map a Int -> Bool
forall k a. Map k a -> Bool
M.null Map a Int
badVor) (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$
        LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ do
          LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [
            String
"Verbindung: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Connection a t -> String
forall a. Show a => a -> String
show Connection a t
c,
            String
"Vielfachheit der Eingangskanten zu hoch:"
            ]
          LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
indent (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ Map a Int -> String
forall a. Show a => a -> String
show Map a Int
badVor
          pure ()
      Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Map a Int -> Bool
forall k a. Map k a -> Bool
M.null Map a Int
badNach) (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$
        LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ do
          LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [
            String
"Verbindung: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Connection a t -> String
forall a. Show a => a -> String
show Connection a t
c,
            String
"Vielfachheit der Ausgangskanten zu hoch:"]
          LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
indent (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ Map a Int -> String
forall a. Show a => a -> String
show Map a Int
badNach
          pure ()
      pure ()
  Capacity Capacity ()
cap -> case Capacity ()
cap of
    Bounded Map () Int
_ -> LangM m
forall a. HasCallStack => a
undefined -- TODO: Is this case required?
    Capacity ()
Unbounded ->
      Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Net a t -> Capacity a
forall s t. Net s t -> Capacity s
capacity Net a t
n Capacity a -> Capacity a -> Bool
forall a. Eq a => a -> a -> Bool
/= Capacity a
forall s. Capacity s
Unbounded) (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$
        LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ String
"Als Kapazität ist vorgeschrieben:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Capacity () -> String
forall a. Show a => a -> String
show Capacity ()
cap
    AllBounded Int
b ->
      Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Net a t -> Capacity a
forall s t. Net s t -> Capacity s
capacity Net a t
n Capacity a -> Capacity a -> Bool
forall a. Eq a => a -> a -> Bool
/= Int -> Capacity a
forall s. Int -> Capacity s
AllBounded Int
b) (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$
        LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ String
"Als Kapazität ist vorgeschrieben:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Capacity () -> String
forall a. Show a => a -> String
show Capacity ()
cap
  Property
Default -> do
    Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (State a -> Bool
forall a. State a -> Bool
allNonNegative (State a -> Bool) -> State a -> Bool
forall a b. (a -> b) -> a -> b
$ Net a t -> State a
forall s t. Net s t -> State s
start Net a t
n) (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$
      LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text String
"Startmarkierung enthält negative Anzahl an Marken"
    Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Capacity a -> State a -> Bool
forall k. Ord k => Capacity k -> State k -> Bool
conforms (Net a t -> Capacity a
forall s t. Net s t -> Capacity s
capacity Net a t
n) (Net a t -> State a
forall s t. Net s t -> State s
start Net a t
n)) (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$
      LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$
        String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text String
"Startmarkierung überschreitet Kapazitäten"

    [Connection a t] -> (Connection a t -> LangM m) -> LangM m
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (Net a t -> [Connection a t]
forall s t. Net s t -> [Connection s t]
connections Net a t
n) ((Connection a t -> LangM m) -> LangM m)
-> (Connection a t -> LangM m) -> LangM m
forall a b. (a -> b) -> a -> b
$ \c :: Connection a t
c@([a]
vor, t
t, [a]
nach) -> do
      Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (t -> Set t -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member t
t (Set t -> Bool) -> Set t -> Bool
forall a b. (a -> b) -> a -> b
$ Net a t -> Set t
forall s t. Net s t -> Set t
transitions Net a t
n) (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$
        LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ do
          LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ String
"Verbindung:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Connection a t -> String
forall a. Show a => a -> String
show Connection a t
c
          LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ String
"nicht deklarierte Transition:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
t
          pure ()
      [a] -> (a -> LangM m) -> LangM m
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [a]
vor ((a -> LangM m) -> LangM m) -> (a -> LangM m) -> LangM m
forall a b. (a -> b) -> a -> b
$ \a
v ->
        Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member a
v (Set a -> Bool) -> Set a -> Bool
forall a b. (a -> b) -> a -> b
$ Net a t -> Set a
forall s t. Net s t -> Set s
places Net a t
n) (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$
          LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ do
            LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ String
"Verbindung:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Connection a t -> String
forall a. Show a => a -> String
show Connection a t
c
            LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$
              String
"nicht deklarierte Stelle im Vorbereich:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v
            pure ()
      [a] -> (a -> LangM m) -> LangM m
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [a]
nach ((a -> LangM m) -> LangM m) -> (a -> LangM m) -> LangM m
forall a b. (a -> b) -> a -> b
$ \a
a ->
        Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member a
a (Set a -> Bool) -> Set a -> Bool
forall a b. (a -> b) -> a -> b
$ Net a t -> Set a
forall s t. Net s t -> Set s
places Net a t
n) (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$
          LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ do
            LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ String
"Verbindung:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Connection a t -> String
forall a. Show a => a -> String
show Connection a t
c
            LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$
              String
"nicht deklarierte Stelle im Nachbereich:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a
            pure ()
      pure ()

    case Net a t -> Capacity a
forall s t. Net s t -> Capacity s
capacity Net a t
n of
      Bounded Map a Int
f -> do
        let out :: Set a
out = Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
S.difference (Map a Int -> Set a
forall k a. Map k a -> Set k
M.keysSet Map a Int
f) (Net a t -> Set a
forall s t. Net s t -> Set s
places Net a t
n)
        Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set a -> Bool
forall a. Set a -> Bool
S.null Set a
out) (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$
          LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ do
            LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text String
"nicht definierte Stellen in Kapazitätsfunktion:"
            LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ Set a -> String
forall a. Show a => a -> String
show Set a
out
            pure ()
      Capacity a
_ -> () -> LangM m
forall a. a -> GenericLangM Language m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

    let out :: Set a
out = Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
S.difference (Map a Int -> Set a
forall k a. Map k a -> Set k
M.keysSet (Map a Int -> Set a) -> Map a Int -> Set a
forall a b. (a -> b) -> a -> b
$ State a -> Map a Int
forall s. State s -> Map s Int
unState (State a -> Map a Int) -> State a -> Map a Int
forall a b. (a -> b) -> a -> b
$ Net a t -> State a
forall s t. Net s t -> State s
start Net a t
n) (Net a t -> Set a
forall s t. Net s t -> Set s
places Net a t
n)
    Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set a -> Bool
forall a. Set a -> Bool
S.null Set a
out) (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$
      LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ do
        LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text String
"nicht definierte Stellen der Startmarkierung:"
        LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ Set a -> String
forall a. Show a => a -> String
show Set a
out
        pure ()
    pure ()

guardBound :: (Ord a, OutputCapable m, Show a) => String -> a -> a -> LangM m
guardBound :: forall a (m :: * -> *).
(Ord a, OutputCapable m, Show a) =>
String -> a -> a -> LangM m
guardBound String
name a
actual a
bound =
  Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (a
actual a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
bound) (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
$ 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
$ String -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> GenericLangM Language m ())
-> String -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char
'(' Char -> String -> String
forall a. a -> [a] -> [a]
: a -> String
forall a. Show a => a -> String
show a
actual String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      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
$ String -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> GenericLangM Language m ())
-> String -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ String
" ist höher als die Schranke " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
bound
      pure ()

{-|
Checks if the given predicate @p@ is satisfied after (partial) execution
of the given sequence.
-}
satisfiesAtAnyState
  :: (Ord s, Ord t, Show s, Show t)
  => (State s -> Bool)
  -> Net s t
  -> [t]
  -> Bool
satisfiesAtAnyState :: forall s t.
(Ord s, Ord t, Show s, Show t) =>
(State s -> Bool) -> Net s t -> [t] -> Bool
satisfiesAtAnyState State s -> Bool
p Net s t
n [t]
ts =
  (State s -> Bool
p (Net s t -> State s
forall s t. Net s t -> State s
start Net s t
n) Bool -> Bool -> Bool
||) (Bool -> Bool)
-> (Either Bool (State s) -> Bool) -> Either Bool (State s) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  Bool -> Either Bool (State s) -> Bool
forall a b. a -> Either a b -> a
fromLeft Bool
False (Either Bool (State s) -> Bool) -> Either Bool (State s) -> Bool
forall a b. (a -> b) -> a -> b
$ (State s -> t -> Either Bool (State s))
-> State s -> [t] -> Either Bool (State s)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
    (\State s
z t
t -> case Identity (Maybe (State s)) -> Maybe (State s)
forall a. Identity a -> a
runIdentity (forall l (m :: * -> *) a.
RunnableOutputCapable l m =>
GenericLangM l m a -> RunMonad l m (Maybe a)
evalLangM @Language @Maybe (Net s t -> t -> State s -> GenericLangM Language Maybe (State s)
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 s t
n t
t State s
z)) of
        Maybe (State s)
Nothing -> Bool -> Either Bool (State s)
forall a b. a -> Either a b
Left Bool
False
        Just State s
z' -> if State s -> Bool
p State s
z' then Bool -> Either Bool (State s)
forall a b. a -> Either a b
Left Bool
True else State s -> Either Bool (State s)
forall a. a -> Either Bool a
forall (m :: * -> *) a. Monad m => a -> m a
return State s
z'
    )
    (Net s t -> State s
forall s t. Net s t -> State s
start Net s t
n)
    [t]
ts