{-# LANGUAGE DuplicateRecordFields #-}
module Modelling.ActivityDiagram.ActionSequences (
  validActionSequence,
  validActionSequenceWithPetri,
  generateActionSequence,
  generateActionSequencesWithPetri,
  generateActionSequenceWithPetriAndRepetition,
  actionRepetitionDistance,
  netAndMap,
  computeActionSequenceLevels,
  isFinalPetriNode
) where

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

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

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 Control.Monad.Random (MonadRandom, uniform)
import Data.List (union)
import Data.List.Extra (nubOrd)
import Data.Maybe (mapMaybe, isJust)


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 a valid action sequence reaching each of the final nodes
generateActionSequence :: UMLActivityDiagram -> [String]
generateActionSequence :: UMLActivityDiagram -> [String]
generateActionSequence UMLActivityDiagram
diag =
  [[String]] -> [String]
forall a. HasCallStack => [a] -> a
head ([[String]] -> [String]) -> [[String]] -> [String]
forall a b. (a -> b) -> a -> b
$ PetriLike Node PetriKey -> Maybe (Int, Int) -> [[String]]
generateActionSequencesWithPetri (UMLActivityDiagram -> PetriLike Node PetriKey
forall (p :: (* -> *) -> * -> *) (n :: * -> *).
Net p n =>
UMLActivityDiagram -> p n PetriKey
convertToPetriNet UMLActivityDiagram
diag) Maybe (Int, Int)
forall a. Maybe a
Nothing

-- | Generate valid action sequences, using a pre-computed Petri net.
-- The returned list may be infinite or some of its tails even diverge,
-- if no length constraints are passed.
generateActionSequencesWithPetri
  :: PetriLike Node PetriKey
  -> Maybe (Int, Int)  -- Optional (minLength, maxLength) constraints
  -> [[String]]
generateActionSequencesWithPetri :: PetriLike Node PetriKey -> Maybe (Int, Int) -> [[String]]
generateActionSequencesWithPetri =
  (Net PetriKey PetriKey -> [[(State PetriKey, [PetriKey])]])
-> PetriLike Node PetriKey -> Maybe (Int, Int) -> [[String]]
generateSequencesWithLevels Net PetriKey PetriKey -> [[(State PetriKey, [PetriKey])]]
forall s t. Ord s => Net s t -> [[(State s, [t])]]
levels'

-- | Generate one valid action sequence with repetition, using a pre-computed Petri net.
-- This version allows cycle exploration to generate sequences with repeated actions.
-- Returns Nothing if no sequence with repetition can be found within the length constraints.
-- Uses randomness to select among sequences with equal maximum repetition distance.
generateActionSequenceWithPetriAndRepetition
  :: MonadRandom m
  => PetriLike Node PetriKey
  -> (Int, Int)  -- (minLength, maxLength) constraints
  -> Maybe (m [String])
generateActionSequenceWithPetriAndRepetition :: forall (m :: * -> *).
MonadRandom m =>
PetriLike Node PetriKey -> (Int, Int) -> Maybe (m [String])
generateActionSequenceWithPetriAndRepetition PetriLike Node PetriKey
petri (Int, Int)
lengthBounds =
  let allActionSequences :: [[String]]
allActionSequences = (Net PetriKey PetriKey -> [[(State PetriKey, [PetriKey])]])
-> PetriLike Node PetriKey -> Maybe (Int, Int) -> [[String]]
generateSequencesWithLevels Net PetriKey PetriKey -> [[(State PetriKey, [PetriKey])]]
forall s t. Ord s => Net s t -> [[(State s, [t])]]
levelsWithCycles PetriLike Node PetriKey
petri ((Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just (Int, Int)
lengthBounds)
      sequencesWithDistances :: [([String], Int)]
sequencesWithDistances = [([String]
seq', Int
d) | [String]
seq' <- [[String]]
allActionSequences, Just Int
d <- [[String] -> Maybe Int
actionRepetitionDistance [String]
seq']]
  in if [([String], Int)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([String], Int)]
sequencesWithDistances
     then Maybe (m [String])
forall a. Maybe a
Nothing
     else
       let maxDist :: Int
maxDist = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (([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)]
sequencesWithDistances
       in m [String] -> Maybe (m [String])
forall a. a -> Maybe a
Just (m [String] -> Maybe (m [String]))
-> m [String] -> Maybe (m [String])
forall a b. (a -> b) -> a -> b
$ [[String]] -> m [String]
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadRandom m) =>
t a -> m a
uniform [[String]
seq' | ([String]
seq', Int
d) <- [([String], Int)]
sequencesWithDistances, Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
maxDist]

-- | Helper to generate sequences using a specific levels function
generateSequencesWithLevels
  :: (Net PetriKey PetriKey -> [[(State PetriKey, [PetriKey])]])
  -> PetriLike Node PetriKey
  -> Maybe (Int, Int)  -- Optional (minLength, maxLength) constraints
  -> [[String]]
generateSequencesWithLevels :: (Net PetriKey PetriKey -> [[(State PetriKey, [PetriKey])]])
-> PetriLike Node PetriKey -> Maybe (Int, Int) -> [[String]]
generateSequencesWithLevels Net PetriKey PetriKey -> [[(State PetriKey, [PetriKey])]]
levelsFunction PetriLike Node PetriKey
petriLike Maybe (Int, Int)
maybeLengthBounds =
  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
petriLike
      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
      relevantLevels :: [[(State PetriKey, [PetriKey])]]
relevantLevels = ([[(State PetriKey, [PetriKey])]]
 -> [[(State PetriKey, [PetriKey])]])
-> ((Int, Int)
    -> [[(State PetriKey, [PetriKey])]]
    -> [[(State PetriKey, [PetriKey])]])
-> Maybe (Int, Int)
-> [[(State PetriKey, [PetriKey])]]
-> [[(State PetriKey, [PetriKey])]]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [[(State PetriKey, [PetriKey])]]
-> [[(State PetriKey, [PetriKey])]]
forall a. a -> a
id (\(Int
minLength, Int
maxLength) -> Int
-> [[(State PetriKey, [PetriKey])]]
-> [[(State PetriKey, [PetriKey])]]
forall a. Int -> [a] -> [a]
take (Int
5 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
maxLength) ([[(State PetriKey, [PetriKey])]]
 -> [[(State PetriKey, [PetriKey])]])
-> ([[(State PetriKey, [PetriKey])]]
    -> [[(State PetriKey, [PetriKey])]])
-> [[(State PetriKey, [PetriKey])]]
-> [[(State PetriKey, [PetriKey])]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> [[(State PetriKey, [PetriKey])]]
-> [[(State PetriKey, [PetriKey])]]
forall a. Int -> [a] -> [a]
drop Int
minLength) Maybe (Int, Int)
maybeLengthBounds
                       ([[(State PetriKey, [PetriKey])]]
 -> [[(State PetriKey, [PetriKey])]])
-> [[(State PetriKey, [PetriKey])]]
-> [[(State PetriKey, [PetriKey])]]
forall a b. (a -> b) -> a -> b
$ Net PetriKey PetriKey -> [[(State PetriKey, [PetriKey])]]
levelsFunction Net PetriKey PetriKey
petri
      convertAndFilterSequence :: [PetriKey] -> Maybe [String]
convertAndFilterSequence [PetriKey]
transitionSequence =
        let actionSequence :: [String]
actionSequence = [ String
actionName | NormalPetriNode {$sel:sourceNode:AuxiliaryPetriNode :: PetriKey -> AdNode
sourceNode = AdActionNode {name :: AdNode -> String
name = String
actionName}} <- [PetriKey]
transitionSequence ]
            seqLength :: Int
seqLength = [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
actionSequence
        in case Maybe (Int, Int)
maybeLengthBounds of
             Just (Int
minLength, Int
maxLength) | Int
seqLength Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
minLength Bool -> Bool -> Bool
|| Int
seqLength Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxLength
               -> Maybe [String]
forall a. Maybe a
Nothing
             Maybe (Int, Int)
_ -> [String] -> Maybe [String]
forall a. a -> Maybe a
Just [String]
actionSequence
  in [ [String] -> [String]
forall a. [a] -> [a]
reverse [String]
a | [(State PetriKey, [PetriKey])]
level <- [[(State PetriKey, [PetriKey])]]
relevantLevels, (State PetriKey
s, [PetriKey]
p) <- [(State PetriKey, [PetriKey])]
level, State PetriKey
s State PetriKey -> State PetriKey -> Bool
forall a. Eq a => a -> a -> Bool
== State PetriKey
zeroState, Just [String]
a <- [[PetriKey] -> Maybe [String]
convertAndFilterSequence [PetriKey]
p] ]


validActionSequence :: [String] -> UMLActivityDiagram -> Bool
validActionSequence :: [String] -> UMLActivityDiagram -> Bool
validActionSequence [String]
input =
  (Net PetriKey PetriKey -> [(String, PetriKey)] -> Bool)
-> (Net PetriKey PetriKey, [(String, PetriKey)]) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ([String] -> Net PetriKey PetriKey -> [(String, PetriKey)] -> Bool
validActionSequenceWithPetri [String]
input) ((Net PetriKey PetriKey, [(String, PetriKey)]) -> Bool)
-> (UMLActivityDiagram
    -> (Net PetriKey PetriKey, [(String, PetriKey)]))
-> UMLActivityDiagram
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PetriLike Node PetriKey
-> (Net PetriKey PetriKey, [(String, PetriKey)])
netAndMap (PetriLike Node PetriKey
 -> (Net PetriKey PetriKey, [(String, PetriKey)]))
-> (UMLActivityDiagram -> PetriLike Node PetriKey)
-> UMLActivityDiagram
-> (Net PetriKey PetriKey, [(String, PetriKey)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UMLActivityDiagram -> PetriLike Node PetriKey
forall (p :: (* -> *) -> * -> *) (n :: * -> *).
Net p n =>
UMLActivityDiagram -> p n PetriKey
convertToPetriNet

-- | Check if an action sequence is valid, using a pre-computed Petri net.
validActionSequenceWithPetri :: [String] -> Net PetriKey PetriKey -> [(String, PetriKey)] -> Bool
validActionSequenceWithPetri :: [String] -> Net PetriKey PetriKey -> [(String, PetriKey)] -> Bool
validActionSequenceWithPetri [String]
input Net PetriKey PetriKey
net [(String, PetriKey)]
actionNameToPetriKey =
  let 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
      levels :: [[(State PetriKey, [PetriKey])]]
levels = [String]
-> Net PetriKey PetriKey
-> [(String, PetriKey)]
-> [[(State PetriKey, [PetriKey])]]
computeActionSequenceLevels [String]
input Net PetriKey PetriKey
net [(String, PetriKey)]
actionNameToPetriKey
  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) [[(State PetriKey, [PetriKey])]]
levels

netAndMap :: PetriLike Node PetriKey -> (Net PetriKey PetriKey, [(String, PetriKey)])
netAndMap :: PetriLike Node PetriKey
-> (Net PetriKey PetriKey, [(String, PetriKey)])
netAndMap PetriLike Node PetriKey
petri =
  let -- Build map from action name to PetriKey by directly checking sourceNode
      actionNameToPetriKey :: [(String, PetriKey)]
actionNameToPetriKey =
        [ (String
actionName, PetriKey
k) | k :: PetriKey
k@NormalPetriNode {$sel:sourceNode:AuxiliaryPetriNode :: PetriKey -> AdNode
sourceNode = AdActionNode {name :: AdNode -> String
name = String
actionName}} <- 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 ]
  in (PetriLike Node PetriKey -> Net PetriKey PetriKey
forall a. Ord a => PetriLike Node a -> Net a a
fromPetriLike PetriLike Node PetriKey
petri, [(String, PetriKey)]
actionNameToPetriKey)

-- | Common computation for action sequence validation.
computeActionSequenceLevels :: [String] -> Net PetriKey PetriKey -> [(String, PetriKey)] -> [[(State PetriKey, [PetriKey])]]
computeActionSequenceLevels :: [String]
-> Net PetriKey PetriKey
-> [(String, PetriKey)]
-> [[(State PetriKey, [PetriKey])]]
computeActionSequenceLevels [String]
input Net PetriKey PetriKey
net [(String, PetriKey)]
actionNameToPetriKey =
  let -- Convert input action names to PetriKeys
      input' :: [PetriKey]
input' = (String -> Maybe PetriKey) -> [String] -> [PetriKey]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (String -> [(String, PetriKey)] -> Maybe PetriKey
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, PetriKey)]
actionNameToPetriKey) [String]
input
      -- Extract all action PetriKeys
      actions :: [PetriKey]
actions = ((String, PetriKey) -> PetriKey)
-> [(String, PetriKey)] -> [PetriKey]
forall a b. (a -> b) -> [a] -> [b]
map (String, PetriKey) -> PetriKey
forall a b. (a, b) -> b
snd [(String, PetriKey)]
actionNameToPetriKey
      levels :: [[(State PetriKey, [PetriKey])]]
levels = [PetriKey]
-> [PetriKey]
-> Net PetriKey PetriKey
-> [[(State PetriKey, [PetriKey])]]
levelsCheckAS [PetriKey]
input' [PetriKey]
actions Net PetriKey PetriKey
net
  in [[(State PetriKey, [PetriKey])]]
levels

-- | Check if a PetriKey represents a final node transition
isFinalPetriNode :: PetriKey -> Bool
isFinalPetriNode :: PetriKey -> Bool
isFinalPetriNode (FinalPetriNode {}) = Bool
True
isFinalPetriNode PetriKey
_ = Bool
False


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, [])]

-- | Variant of levels' that manages visited states per path rather than globally.
-- This allows exploring cycles while preventing infinite loops within each path.
levelsWithCycles :: Ord s => Net s t -> [[(State s, [t])]]
levelsWithCycles :: forall s t. Ord s => Net s t -> [[(State s, [t])]]
levelsWithCycles Net s t
n =
  let f :: [(State s, [t], Set (State s))] -> [[(State s, [t])]]
f [] = []
      f [(State s, [t], Set (State s))]
xs = [(State s, [t])]
xs' [(State s, [t])] -> [[(State s, [t])]] -> [[(State s, [t])]]
forall a. a -> [a] -> [a]
: [(State s, [t], Set (State s))] -> [[(State s, [t])]]
f [(State s, [t], Set (State s))]
next'
        where
          xs' :: [(State s, [t])]
xs' = ((State s, [t], Set (State s)) -> (State s, [t]))
-> [(State s, [t], Set (State s))] -> [(State s, [t])]
forall a b. (a -> b) -> [a] -> [b]
map (\(State s
x, [t]
p, Set (State s)
_) -> (State s
x, [t]
p)) [(State s, [t], Set (State s))]
xs
          next' :: [(State s, [t], Set (State s))]
next' = [ (State s
y, t
tt -> [t] -> [t]
forall a. a -> [a] -> [a]
:[t]
p, State s -> Set (State s) -> Set (State s)
forall a. Ord a => a -> Set a -> Set a
S.insert State s
y Set (State s)
visited)
                  | (State s
x, [t]
p, Set (State s)
visited) <- [(State s, [t], Set (State s))]
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
                  , State s
y State s -> Set (State s) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set (State s)
visited
                  ]
  in [(State s, [t], Set (State s))] -> [[(State s, [t])]]
f [(Net s t -> State s
forall s t. Net s t -> State s
start Net s t
n, [], State s -> Set (State s)
forall a. a -> Set a
S.singleton (Net s t -> State s
forall s t. Net s t -> State s
start Net s t
n))]

{-|
Calculate the maximum distance between any two occurrences of the same action.
Returns Nothing if there are no repeated actions.

For example:

immediate repetition:

>>> actionRepetitionDistance ["A", "A"]
Just 0

1 action between repetitions:

>>> actionRepetitionDistance ["A", "B", "A"]
Just 1

2 actions between repetitions:

>>> actionRepetitionDistance ["A", "B", "C", "A"]
Just 2

no repetitions:

>>> actionRepetitionDistance ["A", "B", "C"]
Nothing
-}
actionRepetitionDistance :: [String] -> Maybe Int
actionRepetitionDistance :: [String] -> Maybe Int
actionRepetitionDistance [String]
actionSequence =
  let maxDistanceForAction :: String -> Maybe a
maxDistanceForAction String
action =
        let indices :: [a]
indices = [a
i | (a
i, String
a) <- [a] -> [String] -> [(a, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a
0..] [String]
actionSequence, String
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
action]
        in if [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
indices Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2
           then Maybe a
forall a. Maybe a
Nothing
           else a -> Maybe a
forall a. a -> Maybe a
Just ([a] -> a
forall a. HasCallStack => [a] -> a
last [a]
indices a -> a -> a
forall a. Num a => a -> a -> a
- [a] -> a
forall a. HasCallStack => [a] -> a
head [a]
indices a -> a -> a
forall a. Num a => a -> a -> a
- a
1)
      distances :: [Int]
distances = [Int
d | String
action <- [String] -> [String]
forall a. Ord a => [a] -> [a]
nubOrd [String]
actionSequence, Just Int
d <- [String -> Maybe Int
forall {a}. (Num a, Enum a) => String -> Maybe a
maxDistanceForAction String
action]]
  in if [Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
distances then Maybe Int
forall a. Maybe a
Nothing else Int -> Maybe Int
forall a. a -> Maybe a
Just ([Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Int]
distances)