{-# LANGUAGE DuplicateRecordFields #-}
module Modelling.ActivityDiagram.ActionSequences (
  validActionSequence,
  generateActionSequence,
) where

import qualified Modelling.ActivityDiagram.Datatype as Ad (
  AdNode (label),
  )

import qualified Data.Set as S (fromList)
import qualified Data.Map as M (filter, map, keys, fromList, toList)

import Modelling.ActivityDiagram.Datatype (
  AdNode (..),
  UMLActivityDiagram (..),
  isActionNode
  )

import Modelling.ActivityDiagram.PetriNet (
  PetriKey(..),
  convertToPetriNet
  )

import Modelling.PetriNet.Types (
  PetriLike(..),
  Node(..),
  isPlaceNode, isTransitionNode
  )

import Modelling.PetriNet.Reach.Type (
  State(..),
  Capacity(..),
  Net(..)
  )

import Modelling.PetriNet.Reach.Step (levels', successors)

import Control.Monad (guard)
import Data.List (find, union)
import Data.Maybe(mapMaybe, isJust, fromJust)


fromPetriLike :: Ord a => PetriLike Node a -> Net a a
fromPetriLike :: forall a. Ord a => PetriLike Node a -> Net a a
fromPetriLike PetriLike Node a
petri =
  Net {
      places :: Set a
places = [a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList ([a] -> Set a) -> [a] -> Set a
forall a b. (a -> b) -> a -> b
$ Map a (Node a) -> [a]
forall k a. Map k a -> [k]
M.keys (Map a (Node a) -> [a]) -> Map a (Node a) -> [a]
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 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
petri,
      transitions :: Set a
transitions = [a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList ([a] -> Set a) -> [a] -> Set a
forall a b. (a -> b) -> a -> b
$ Map a (Node a) -> [a]
forall k a. Map k a -> [k]
M.keys (Map a (Node a) -> [a]) -> Map a (Node a) -> [a]
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 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
petri,
      connections :: [Connection a a]
connections = ((a, Node a) -> Connection a a)
-> [(a, Node a)] -> [Connection a a]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
t,Node a
n) -> (Map a Int -> [a]
forall k a. Map k a -> [k]
M.keys (Map a Int -> [a]) -> Map a Int -> [a]
forall a b. (a -> b) -> a -> b
$ Node a -> Map a Int
forall a. Node a -> Map a Int
flowIn Node a
n, a
t, Map a Int -> [a]
forall k a. Map k a -> [k]
M.keys (Map a Int -> [a]) -> Map a Int -> [a]
forall a b. (a -> b) -> a -> b
$ Node a -> Map a Int
forall a. Node a -> Map a Int
flowOut Node a
n)) ([(a, Node a)] -> [Connection a a])
-> [(a, Node a)] -> [Connection a a]
forall a b. (a -> b) -> a -> b
$ Map a (Node a) -> [(a, Node a)]
forall k a. Map k a -> [(k, a)]
M.toList (Map a (Node a) -> [(a, Node a)])
-> Map a (Node a) -> [(a, Node a)]
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 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
petri,
      capacity :: Capacity a
capacity = Capacity a
forall s. Capacity s
Unbounded,
      start :: State a
start = State {unState :: Map a Int
unState = (Node a -> Int) -> Map a (Node a) -> Map a Int
forall a b k. (a -> b) -> Map k a -> Map k b
M.map Node a -> Int
forall a. Node a -> Int
initial (Map a (Node a) -> Map a Int) -> Map a (Node a) -> Map a Int
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 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
petri}
  }

--Generate one valid action sequence to each of the final nodes
generateActionSequence :: UMLActivityDiagram -> [String]
generateActionSequence :: UMLActivityDiagram -> [String]
generateActionSequence UMLActivityDiagram
diag =
  let tSeq :: [PetriKey]
tSeq = UMLActivityDiagram -> [PetriKey]
generateActionSequence' UMLActivityDiagram
diag
      tSeqLabels :: [Int]
tSeqLabels = (PetriKey -> Int) -> [PetriKey] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (AdNode -> Int
Ad.label (AdNode -> Int) -> (PetriKey -> AdNode) -> PetriKey -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriKey -> AdNode
sourceNode) ([PetriKey] -> [Int]) -> [PetriKey] -> [Int]
forall a b. (a -> b) -> a -> b
$ (PetriKey -> Bool) -> [PetriKey] -> [PetriKey]
forall a. (a -> Bool) -> [a] -> [a]
filter PetriKey -> Bool
isNormalPetriNode [PetriKey]
tSeq
      actions :: [(Int, String)]
actions = (AdNode -> (Int, String)) -> [AdNode] -> [(Int, String)]
forall a b. (a -> b) -> [a] -> [b]
map
        (\AdNode
n -> (AdNode -> Int
Ad.label AdNode
n, AdNode -> String
name AdNode
n))
        ([AdNode] -> [(Int, String)]) -> [AdNode] -> [(Int, String)]
forall a b. (a -> b) -> a -> b
$ (AdNode -> Bool) -> [AdNode] -> [AdNode]
forall a. (a -> Bool) -> [a] -> [a]
filter AdNode -> Bool
isActionNode ([AdNode] -> [AdNode]) -> [AdNode] -> [AdNode]
forall a b. (a -> b) -> a -> b
$ UMLActivityDiagram -> [AdNode]
nodes UMLActivityDiagram
diag
  in (Int -> Maybe String) -> [Int] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Int -> [(Int, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(Int, String)]
actions) [Int]
tSeqLabels

isNormalPetriNode :: PetriKey -> Bool
isNormalPetriNode :: PetriKey -> Bool
isNormalPetriNode PetriKey
pk =
  case PetriKey
pk of
    NormalPetriNode {} -> Bool
True
    PetriKey
_ -> Bool
False

--Generate at one sequence of transitions to each final node
generateActionSequence' :: UMLActivityDiagram -> [PetriKey]
generateActionSequence' :: UMLActivityDiagram -> [PetriKey]
generateActionSequence' UMLActivityDiagram
diag =
  let petri :: Net PetriKey PetriKey
petri = PetriLike Node PetriKey -> Net PetriKey PetriKey
forall a. Ord a => PetriLike Node a -> Net a a
fromPetriLike (PetriLike Node PetriKey -> Net PetriKey PetriKey)
-> PetriLike Node PetriKey -> Net PetriKey PetriKey
forall a b. (a -> b) -> a -> b
$ UMLActivityDiagram -> PetriLike Node PetriKey
forall (p :: (* -> *) -> * -> *) (n :: * -> *).
Net p n =>
UMLActivityDiagram -> p n PetriKey
convertToPetriNet UMLActivityDiagram
diag
      zeroState :: State PetriKey
zeroState = Map PetriKey Int -> State PetriKey
forall s. Map s Int -> State s
State (Map PetriKey Int -> State PetriKey)
-> Map PetriKey Int -> State PetriKey
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Map PetriKey Int -> Map PetriKey Int
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Int -> Int -> Int
forall a b. a -> b -> a
const Int
0) (Map PetriKey Int -> Map PetriKey Int)
-> Map PetriKey Int -> Map PetriKey Int
forall a b. (a -> b) -> a -> b
$ State PetriKey -> Map PetriKey Int
forall s. State s -> Map s Int
unState (State PetriKey -> Map PetriKey Int)
-> State PetriKey -> Map PetriKey Int
forall a b. (a -> b) -> a -> b
$ Net PetriKey PetriKey -> State PetriKey
forall s t. Net s t -> State s
start Net PetriKey PetriKey
petri
      sequences :: [(State PetriKey, [PetriKey])]
sequences = Maybe [(State PetriKey, [PetriKey])]
-> [(State PetriKey, [PetriKey])]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe [(State PetriKey, [PetriKey])]
 -> [(State PetriKey, [PetriKey])])
-> Maybe [(State PetriKey, [PetriKey])]
-> [(State PetriKey, [PetriKey])]
forall a b. (a -> b) -> a -> b
$ ([(State PetriKey, [PetriKey])] -> Bool)
-> [[(State PetriKey, [PetriKey])]]
-> Maybe [(State PetriKey, [PetriKey])]
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Maybe [PetriKey] -> Bool
forall a. Maybe a -> Bool
isJust (Maybe [PetriKey] -> Bool)
-> ([(State PetriKey, [PetriKey])] -> Maybe [PetriKey])
-> [(State PetriKey, [PetriKey])]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State PetriKey
-> [(State PetriKey, [PetriKey])] -> Maybe [PetriKey]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup State PetriKey
zeroState) ([[(State PetriKey, [PetriKey])]]
 -> Maybe [(State PetriKey, [PetriKey])])
-> [[(State PetriKey, [PetriKey])]]
-> Maybe [(State PetriKey, [PetriKey])]
forall a b. (a -> b) -> a -> b
$ Net PetriKey PetriKey -> [[(State PetriKey, [PetriKey])]]
forall s t. Ord s => Net s t -> [[(State s, [t])]]
levels' Net PetriKey PetriKey
petri
  in [PetriKey] -> [PetriKey]
forall a. [a] -> [a]
reverse ([PetriKey] -> [PetriKey]) -> [PetriKey] -> [PetriKey]
forall a b. (a -> b) -> a -> b
$ Maybe [PetriKey] -> [PetriKey]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe [PetriKey] -> [PetriKey]) -> Maybe [PetriKey] -> [PetriKey]
forall a b. (a -> b) -> a -> b
$ State PetriKey
-> [(State PetriKey, [PetriKey])] -> Maybe [PetriKey]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup State PetriKey
zeroState [(State PetriKey, [PetriKey])]
sequences


validActionSequence :: [String] -> UMLActivityDiagram -> Bool
validActionSequence :: [String] -> UMLActivityDiagram -> Bool
validActionSequence [String]
input UMLActivityDiagram
diag =
  let nameMap :: [(String, Int)]
nameMap = (AdNode -> (String, Int)) -> [AdNode] -> [(String, Int)]
forall a b. (a -> b) -> [a] -> [b]
map
        (\AdNode
n -> (AdNode -> String
name AdNode
n, AdNode -> Int
Ad.label AdNode
n))
        ([AdNode] -> [(String, Int)]) -> [AdNode] -> [(String, Int)]
forall a b. (a -> b) -> a -> b
$ (AdNode -> Bool) -> [AdNode] -> [AdNode]
forall a. (a -> Bool) -> [a] -> [a]
filter AdNode -> Bool
isActionNode ([AdNode] -> [AdNode]) -> [AdNode] -> [AdNode]
forall a b. (a -> b) -> a -> b
$ UMLActivityDiagram -> [AdNode]
nodes UMLActivityDiagram
diag
      labels :: [Int]
labels = (String -> Maybe Int) -> [String] -> [Int]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (String -> [(String, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, Int)]
nameMap) [String]
input
      petri :: PetriLike Node PetriKey
petri = UMLActivityDiagram -> PetriLike Node PetriKey
forall (p :: (* -> *) -> * -> *) (n :: * -> *).
Net p n =>
UMLActivityDiagram -> p n PetriKey
convertToPetriNet UMLActivityDiagram
diag
      petriKeyMap :: [(Int, PetriKey)]
petriKeyMap = (PetriKey -> (Int, PetriKey)) -> [PetriKey] -> [(Int, PetriKey)]
forall a b. (a -> b) -> [a] -> [b]
map
        (\PetriKey
k -> (AdNode -> Int
Ad.label (AdNode -> Int) -> AdNode -> Int
forall a b. (a -> b) -> a -> b
$ PetriKey -> AdNode
sourceNode PetriKey
k, PetriKey
k))
        ([PetriKey] -> [(Int, PetriKey)])
-> [PetriKey] -> [(Int, PetriKey)]
forall a b. (a -> b) -> a -> b
$ (PetriKey -> Bool) -> [PetriKey] -> [PetriKey]
forall a. (a -> Bool) -> [a] -> [a]
filter PetriKey -> Bool
isNormalPetriNode ([PetriKey] -> [PetriKey]) -> [PetriKey] -> [PetriKey]
forall a b. (a -> b) -> a -> b
$ Map PetriKey (Node PetriKey) -> [PetriKey]
forall k a. Map k a -> [k]
M.keys (Map PetriKey (Node PetriKey) -> [PetriKey])
-> Map PetriKey (Node PetriKey) -> [PetriKey]
forall a b. (a -> b) -> a -> b
$ PetriLike Node PetriKey -> Map PetriKey (Node PetriKey)
forall (n :: * -> *) a. PetriLike n a -> Map a (n a)
allNodes PetriLike Node PetriKey
petri
      input' :: [PetriKey]
input' = (Int -> Maybe PetriKey) -> [Int] -> [PetriKey]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Int -> [(Int, PetriKey)] -> Maybe PetriKey
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(Int, PetriKey)]
petriKeyMap) [Int]
labels
      actions :: [PetriKey]
actions = ((Int, PetriKey) -> PetriKey) -> [(Int, PetriKey)] -> [PetriKey]
forall a b. (a -> b) -> [a] -> [b]
map (Int, PetriKey) -> PetriKey
forall a b. (a, b) -> b
snd ([(Int, PetriKey)] -> [PetriKey])
-> [(Int, PetriKey)] -> [PetriKey]
forall a b. (a -> b) -> a -> b
$ ((Int, PetriKey) -> Bool) -> [(Int, PetriKey)] -> [(Int, PetriKey)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
l,PetriKey
_) -> Int
l Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((String, Int) -> Int) -> [(String, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (String, Int) -> Int
forall a b. (a, b) -> b
snd [(String, Int)]
nameMap) [(Int, PetriKey)]
petriKeyMap
  in [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
input Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
labels Bool -> Bool -> Bool
&& [PetriKey] -> [PetriKey] -> PetriLike Node PetriKey -> Bool
validActionSequence' [PetriKey]
input' [PetriKey]
actions PetriLike Node PetriKey
petri


validActionSequence'
  :: [PetriKey]
  -> [PetriKey]
  -> PetriLike Node PetriKey
  -> Bool
validActionSequence' :: [PetriKey] -> [PetriKey] -> PetriLike Node PetriKey -> Bool
validActionSequence' [PetriKey]
input [PetriKey]
actions PetriLike Node PetriKey
petri =
  let net :: Net PetriKey PetriKey
net = PetriLike Node PetriKey -> Net PetriKey PetriKey
forall a. Ord a => PetriLike Node a -> Net a a
fromPetriLike PetriLike Node PetriKey
petri
      zeroState :: State PetriKey
zeroState = Map PetriKey Int -> State PetriKey
forall s. Map s Int -> State s
State (Map PetriKey Int -> State PetriKey)
-> Map PetriKey Int -> State PetriKey
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Map PetriKey Int -> Map PetriKey Int
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Int -> Int -> Int
forall a b. a -> b -> a
const Int
0) (Map PetriKey Int -> Map PetriKey Int)
-> Map PetriKey Int -> Map PetriKey Int
forall a b. (a -> b) -> a -> b
$ State PetriKey -> Map PetriKey Int
forall s. State s -> Map s Int
unState (State PetriKey -> Map PetriKey Int)
-> State PetriKey -> Map PetriKey Int
forall a b. (a -> b) -> a -> b
$ Net PetriKey PetriKey -> State PetriKey
forall s t. Net s t -> State s
start Net PetriKey PetriKey
net
  in ([(State PetriKey, [PetriKey])] -> Bool)
-> [[(State PetriKey, [PetriKey])]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe [PetriKey] -> Bool
forall a. Maybe a -> Bool
isJust (Maybe [PetriKey] -> Bool)
-> ([(State PetriKey, [PetriKey])] -> Maybe [PetriKey])
-> [(State PetriKey, [PetriKey])]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State PetriKey
-> [(State PetriKey, [PetriKey])] -> Maybe [PetriKey]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup State PetriKey
zeroState) ([PetriKey]
-> [PetriKey]
-> Net PetriKey PetriKey
-> [[(State PetriKey, [PetriKey])]]
levelsCheckAS [PetriKey]
input [PetriKey]
actions Net PetriKey PetriKey
net)


levelsCheckAS :: [PetriKey] -> [PetriKey] -> Net PetriKey PetriKey-> [[(State PetriKey, [PetriKey])]]
levelsCheckAS :: [PetriKey]
-> [PetriKey]
-> Net PetriKey PetriKey
-> [[(State PetriKey, [PetriKey])]]
levelsCheckAS [PetriKey]
input [PetriKey]
actions Net PetriKey PetriKey
n =
  let g :: (PetriKey -> Bool)
-> [(State PetriKey, [PetriKey])] -> [(State PetriKey, [PetriKey])]
g PetriKey -> Bool
h [(State PetriKey, [PetriKey])]
xs = Map (State PetriKey) [PetriKey] -> [(State PetriKey, [PetriKey])]
forall k a. Map k a -> [(k, a)]
M.toList (Map (State PetriKey) [PetriKey] -> [(State PetriKey, [PetriKey])])
-> Map (State PetriKey) [PetriKey]
-> [(State PetriKey, [PetriKey])]
forall a b. (a -> b) -> a -> b
$
        [(State PetriKey, [PetriKey])] -> Map (State PetriKey) [PetriKey]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(State PetriKey, [PetriKey])] -> Map (State PetriKey) [PetriKey])
-> [(State PetriKey, [PetriKey])]
-> Map (State PetriKey) [PetriKey]
forall a b. (a -> b) -> a -> b
$ do
          (State PetriKey
x, [PetriKey]
p) <- [(State PetriKey, [PetriKey])]
xs
          (PetriKey
t, State PetriKey
y) <- Net PetriKey PetriKey
-> State PetriKey -> [(PetriKey, State PetriKey)]
forall s t. Ord s => Net s t -> State s -> [(t, State s)]
successors Net PetriKey PetriKey
n State PetriKey
x
          Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ PetriKey -> Bool
h PetriKey
t
          (State PetriKey, [PetriKey]) -> [(State PetriKey, [PetriKey])]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (State PetriKey
y, PetriKey
t PetriKey -> [PetriKey] -> [PetriKey]
forall a. a -> [a] -> [a]
: [PetriKey]
p)
      f :: [PetriKey]
-> [(State PetriKey, [PetriKey])]
-> [[(State PetriKey, [PetriKey])]]
f [PetriKey]
_ [] = []
      f [] [(State PetriKey, [PetriKey])]
xs =
        let next :: [(State PetriKey, [PetriKey])]
next = (PetriKey -> Bool)
-> [(State PetriKey, [PetriKey])] -> [(State PetriKey, [PetriKey])]
g (PetriKey -> [PetriKey] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [PetriKey]
actions) [(State PetriKey, [PetriKey])]
xs               -- No further actions should be processed if no input is left
        in [(State PetriKey, [PetriKey])]
xs [(State PetriKey, [PetriKey])]
-> [[(State PetriKey, [PetriKey])]]
-> [[(State PetriKey, [PetriKey])]]
forall a. a -> [a] -> [a]
: [PetriKey]
-> [(State PetriKey, [PetriKey])]
-> [[(State PetriKey, [PetriKey])]]
f [] [(State PetriKey, [PetriKey])]
next
      f (PetriKey
a:[PetriKey]
as) [(State PetriKey, [PetriKey])]
xs =
        let consume :: [(State PetriKey, [PetriKey])]
consume = (PetriKey -> Bool)
-> [(State PetriKey, [PetriKey])] -> [(State PetriKey, [PetriKey])]
g (PetriKey -> PetriKey -> Bool
forall a. Eq a => a -> a -> Bool
==PetriKey
a) [(State PetriKey, [PetriKey])]
xs                          -- Case: Next transition corresponds to input, therefore is processed and removed
            notConsume :: [(State PetriKey, [PetriKey])]
notConsume = (PetriKey -> Bool)
-> [(State PetriKey, [PetriKey])] -> [(State PetriKey, [PetriKey])]
g (PetriKey -> [PetriKey] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [PetriKey]
actions) [(State PetriKey, [PetriKey])]
xs         -- Case: Next transition is not an action, therefore is processed but not removed from input
        in [[(State PetriKey, [PetriKey])]]
-> [[(State PetriKey, [PetriKey])]]
-> [[(State PetriKey, [PetriKey])]]
forall a. Eq a => [a] -> [a] -> [a]
union ([PetriKey]
-> [(State PetriKey, [PetriKey])]
-> [[(State PetriKey, [PetriKey])]]
f [PetriKey]
as [(State PetriKey, [PetriKey])]
consume) ([PetriKey]
-> [(State PetriKey, [PetriKey])]
-> [[(State PetriKey, [PetriKey])]]
f (PetriKey
aPetriKey -> [PetriKey] -> [PetriKey]
forall a. a -> [a] -> [a]
:[PetriKey]
as) [(State PetriKey, [PetriKey])]
notConsume)
  in [PetriKey]
-> [(State PetriKey, [PetriKey])]
-> [[(State PetriKey, [PetriKey])]]
f [PetriKey]
input [(Net PetriKey PetriKey -> State PetriKey
forall s t. Net s t -> State s
start Net PetriKey PetriKey
n, [])]