> {-# OPTIONS_HADDOCK show-extensions #-}
> {-# Language CPP #-}

#if !defined(MIN_VERSION_base)
# define MIN_VERSION_base(a,b,c) 0
#endif

> {-|
> Module    : Traversals
> Copyright : (c) 2017-2023 Jim Rogers and Dakotah Lambert
> License   : MIT
>
> Find paths through an automaton.
> -}
> module LTK.Traversals
>        ( Path(..)
>        , word
>        , isAcyclic
>        , initialsPaths
>        , initialsNDPath
>        , rejectingPaths
>        , acyclicPaths
>        , extensions
>        , boundedCycleExtensions
>        , nondeterministicAcyclicExtensions
>        ) where

#if !MIN_VERSION_base(4,8,0)
> import Data.Monoid (Monoid, mappend, mconcat, mempty)
#endif
#if MIN_VERSION_base(4,9,0)
#if !MIN_VERSION_base(4,11,0)
> import Data.Semigroup (Semigroup, (<>))
#endif
#endif
> import Data.Set (Set)

> import LTK.FSA

A Path is
* a sequence of labels in inverse order of edges in the path
* the terminal state of the path
 --- This is a Maybe (State n) allowing for an adjoined identity (empty path)
     making Path a monoid wrt concatenation (append).
* the multiset of states along the path
 --- this allows us to determine how many times a state has been entered on
     the path, which is exactly the number of times a cycle starting and
     ending at that state has been traversed.
* the length of the path (depth of the terminal state)

> -- |A path through an 'FSA'.
> data Path n e
>     = Path
>       { -- |Edge labels are gathered in reverse order,
>         -- so 'labels' is a reversed string.
>         forall n e. Path n e -> [Symbol e]
labels        :: [Symbol e]
>         -- |Current 'State', if any.
>       , forall n e. Path n e -> Maybe (State n)
endstate      :: Maybe (State n)
>         -- |States seen so far, with multiplicity.
>       , forall n e. Path n e -> Multiset (State n)
stateMultiset :: Multiset (State n)
>         -- |The number of edges taken so far.
>       , forall n e. Path n e -> Integer
depth         :: Integer
>       }
>     deriving (Path n e -> Path n e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n e. (Eq e, Eq n) => Path n e -> Path n e -> Bool
/= :: Path n e -> Path n e -> Bool
$c/= :: forall n e. (Eq e, Eq n) => Path n e -> Path n e -> Bool
== :: Path n e -> Path n e -> Bool
$c== :: forall n e. (Eq e, Eq n) => Path n e -> Path n e -> Bool
Eq, Int -> Path n e -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n e. (Show e, Show n) => Int -> Path n e -> ShowS
forall n e. (Show e, Show n) => [Path n e] -> ShowS
forall n e. (Show e, Show n) => Path n e -> String
showList :: [Path n e] -> ShowS
$cshowList :: forall n e. (Show e, Show n) => [Path n e] -> ShowS
show :: Path n e -> String
$cshow :: forall n e. (Show e, Show n) => Path n e -> String
showsPrec :: Int -> Path n e -> ShowS
$cshowsPrec :: forall n e. (Show e, Show n) => Int -> Path n e -> ShowS
Show)

> -- |The reversal of the 'labels' of the 'Path'.
> word :: Path n e -> [Symbol e]
> word :: forall n e. Path n e -> [Symbol e]
word = forall a. [a] -> [a]
Prelude.reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Path n e -> [Symbol e]
labels

In order to have a Multiset of Path, Path must be Ord:

> instance (Ord e, Ord n) => Ord (Path n e)
>     where compare :: Path n e -> Path n e -> Ordering
compare Path n e
p1 Path n e
p2
>               = forall a. Monoid a => [a] -> a
mconcat [forall a. Ord a => a -> a -> Ordering
compare Integer
d1 Integer
d2, forall a. Ord a => a -> a -> Ordering
compare [Symbol e]
l1 [Symbol e]
l2, forall a. Ord a => a -> a -> Ordering
compare Maybe (State n)
e1 Maybe (State n)
e2]
>               where (Maybe (State n)
e1, [Symbol e]
l1, Integer
d1)  =  (forall n e. Path n e -> Maybe (State n)
endstate Path n e
p1, forall n e. Path n e -> [Symbol e]
labels Path n e
p1, forall n e. Path n e -> Integer
depth Path n e
p1)
>                     (Maybe (State n)
e2, [Symbol e]
l2, Integer
d2)  =  (forall n e. Path n e -> Maybe (State n)
endstate Path n e
p2, forall n e. Path n e -> [Symbol e]
labels Path n e
p2, forall n e. Path n e -> Integer
depth Path n e
p2)

> appendPath :: Ord n => Path n e -> Path n e -> Path n e
> appendPath :: forall n e. Ord n => Path n e -> Path n e -> Path n e
appendPath (Path [Symbol e]
xs1 Maybe (State n)
q1 Multiset (State n)
qs1 Integer
d1) (Path [Symbol e]
xs2 Maybe (State n)
q2 Multiset (State n)
qs2 Integer
d2)
>     = Path { labels :: [Symbol e]
labels         =  [Symbol e]
xs1 forall a. [a] -> [a] -> [a]
++ [Symbol e]
xs2
>            , endstate :: Maybe (State n)
endstate       =  forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) Maybe (State n)
q1 Maybe (State n)
q2
>            , stateMultiset :: Multiset (State n)
stateMultiset  =  Multiset (State n)
qs1 forall c a. Container c a => c -> c -> c
`union` Multiset (State n)
qs2
>            , depth :: Integer
depth          =  Integer
d1 forall a. Num a => a -> a -> a
+ Integer
d2
>            }

#if MIN_VERSION_base(4,9,0)
Semigroup instance to satisfy base-4.9

> instance (Ord n) => Semigroup (Path n e) where
>     <> :: Path n e -> Path n e -> Path n e
(<>) = forall n e. Ord n => Path n e -> Path n e -> Path n e
appendPath
#endif

> instance (Ord n) => Monoid (Path n e) where
>     mempty :: Path n e
mempty = forall n e.
[Symbol e]
-> Maybe (State n) -> Multiset (State n) -> Integer -> Path n e
Path [] forall a. Maybe a
Nothing forall c a. Container c a => c
empty Integer
0
#if MIN_VERSION_base(4,11,0)
> -- mappend will eventually be removed
#elif MIN_VERSION_base(4,9,0)
>     mappend = (<>)
#else
>     mappend = appendPath
#endif

The extensions of a path p are paths extending p by a single edge

> extend :: (Ord e, Ord n) =>
>           Path n e -> Set (Transition n e) -> Set (Path n e)
> extend :: forall e n.
(Ord e, Ord n) =>
Path n e -> Set (Transition n e) -> Set (Path n e)
extend Path n e
p = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (\Transition n e
t ->
>                  Path { labels :: [Symbol e]
labels    =  forall n e. Transition n e -> Symbol e
edgeLabel Transition n e
t forall a. a -> [a] -> [a]
: forall n e. Path n e -> [Symbol e]
labels Path n e
p
>                       , endstate :: Maybe (State n)
endstate  =  forall a. a -> Maybe a
Just (forall n e. Transition n e -> State n
destination Transition n e
t)
>                       , stateMultiset :: Multiset (State n)
stateMultiset
>                             = forall n e. Transition n e -> State n
destination Transition n e
t forall c a. Container c a => a -> c -> c
`insert` forall n e. Path n e -> Multiset (State n)
stateMultiset Path n e
p
>                       , depth :: Integer
depth     = forall n e. Path n e -> Integer
depth Path n e
p forall a. Num a => a -> a -> a
+ Integer
1
>                       }
>                 )

The nondeterministic extensions of a path p are paths extending p
by a single edge nondeterminstically.  That is, the states of the
path are sets.

> nondeterministicExtend :: (Ord e, Ord n) =>
>                           Path (Set n) e -> Set (Transition n e) ->
>                           Set (Path (Set n) e)
> nondeterministicExtend :: forall e n.
(Ord e, Ord n) =>
Path (Set n) e -> Set (Transition n e) -> Set (Path (Set n) e)
nondeterministicExtend Path (Set n) e
p Set (Transition n e)
ts
>     | forall c a. Container c a => c -> Bool
isEmpty Set (Transition n e)
ts = forall c a. Container c a => a -> c
singleton Path (Set n) e
p
>     | Bool
otherwise
>         = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap
>           (\Set (Transition n e)
xs ->
>            let newState :: State (Set n)
newState  =  forall n. n -> State n
State forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse forall {c} {e}. Container c n => Transition n e -> c -> c
f forall c a. Container c a => c
empty Set (Transition n e)
xs
>            in Path (Set n) e
p { labels :: [Symbol e]
labels    =  forall (l :: * -> *) a. Linearizable l => l a -> a
chooseOne (forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n e. Transition n e -> Symbol e
edgeLabel Set (Transition n e)
xs) forall a. a -> [a] -> [a]
: forall n e. Path n e -> [Symbol e]
labels Path (Set n) e
p
>                 , endstate :: Maybe (State (Set n))
endstate  =  forall a. a -> Maybe a
Just State (Set n)
newState
>                 , stateMultiset :: Multiset (State (Set n))
stateMultiset
>                       =  forall c a. Container c a => a -> c -> c
insert State (Set n)
newState (forall n e. Path n e -> Multiset (State n)
stateMultiset Path (Set n) e
p)
>                 , depth :: Integer
depth     =  forall n e. Path n e -> Integer
depth Path (Set n) e
p forall a. Num a => a -> a -> a
+ Integer
1
>                 }
>           ) Set (Set (Transition n e))
tgroups
>     where tgroups :: Set (Set (Transition n e))
tgroups = forall a n. (Ord a, Ord n) => (n -> a) -> Set n -> Set (Set n)
partitionBy forall n e. Transition n e -> Symbol e
edgeLabel Set (Transition n e)
ts
>           connectable :: n -> Bool
connectable
>               = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a b. a -> b -> a
const Bool
False) (forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel) (forall n e. Path n e -> Maybe (State n)
endstate Path (Set n) e
p)
>           f :: Transition n e -> c -> c
f Transition n e
x = if n -> Bool
connectable forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel forall a b. (a -> b) -> a -> b
$ forall n e. Transition n e -> State n
source Transition n e
x
>                 then forall c a. Container c a => a -> c -> c
insert (forall n. State n -> n
nodeLabel forall a b. (a -> b) -> a -> b
$ forall n e. Transition n e -> State n
destination Transition n e
x)
>                 else forall a. a -> a
id

> -- |Paths extending a given path by a single edge.
> extensions :: (Ord e, Ord n) =>
>               FSA n e -> Path n e -> Set (Path n e)
> extensions :: forall e n. (Ord e, Ord n) => FSA n e -> Path n e -> Set (Path n e)
extensions FSA n e
fsa Path n e
p
>     = forall e n.
(Ord e, Ord n) =>
Path n e -> Set (Transition n e) -> Set (Path n e)
extend Path n e
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep ((forall a. Eq a => a -> a -> Bool
== forall n e. Path n e -> Maybe (State n)
endstate Path n e
p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Transition n e -> State n
source) forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
fsa

Acyclic extensions of a path are extensions other than back-edges

> acyclicExtensions :: (Ord e, Ord n) => FSA n e -> Path n e -> Set (Path n e)
> acyclicExtensions :: forall e n. (Ord e, Ord n) => FSA n e -> Path n e -> Set (Path n e)
acyclicExtensions FSA n e
fsa Path n e
p
>     = forall e n.
(Ord e, Ord n) =>
Path n e -> Set (Transition n e) -> Set (Path n e)
extend Path n e
p forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>       forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
both
>             (forall c a. (Container c a, Eq a) => c -> a -> Bool
isNotIn (forall n e. Path n e -> Multiset (State n)
stateMultiset Path n e
p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Transition n e -> State n
destination)
>             ((forall a. Eq a => a -> a -> Bool
== forall n e. Path n e -> Maybe (State n)
endstate Path n e
p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Transition n e -> State n
source)) forall a b. (a -> b) -> a -> b
$
>       forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
fsa

> -- |The extensions of a non-deterministic path other than back-edges
> nondeterministicAcyclicExtensions :: (Ord e, Ord n) =>
>                                      FSA n e -> Path (Set n) e ->
>                                      Set (Path (Set n) e)
> nondeterministicAcyclicExtensions :: forall e n.
(Ord e, Ord n) =>
FSA n e -> Path (Set n) e -> Set (Path (Set n) e)
nondeterministicAcyclicExtensions FSA n e
fsa
>     = forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep
>       (\Path (Set n) e
a ->
>        forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((forall a. Ord a => a -> a -> Bool
<= Integer
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => Multiset a -> a -> Integer
multiplicity (forall n e. Path n e -> Multiset (State n)
stateMultiset Path (Set n) e
a)) (forall n e. Path n e -> Maybe (State n)
endstate Path (Set n) e
a)
>       ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall e n.
(Ord e, Ord n) =>
Path (Set n) e -> Set (Transition n e) -> Set (Path (Set n) e)
nondeterministicExtend (forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
fsa)

boundedCycExtensions are extensions other than back-edges to a state that
has been visted more than bound times.  This gives traversals that will
follow cycles at most bound times.  Note that the qualification is that
the multiplicity of the state is $\leq$ bound; states that have not been
visited have multiplicity 0.

> -- |Extensions other than back-edges to a state that has been visited
> -- more than a given number of times.
> boundedCycleExtensions :: (Ord e, Ord n) =>
>                           FSA n e -> Integer -> Path n e -> Set (Path n e)
> boundedCycleExtensions :: forall e n.
(Ord e, Ord n) =>
FSA n e -> Integer -> Path n e -> Set (Path n e)
boundedCycleExtensions FSA n e
fsa Integer
b Path n e
p
>     = forall e n.
(Ord e, Ord n) =>
Path n e -> Set (Transition n e) -> Set (Path n e)
extend Path n e
p forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>       forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
both
>             ((forall a. Eq a => a -> a -> Bool
== forall n e. Path n e -> Maybe (State n)
endstate Path n e
p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Transition n e -> State n
source)
>             ((forall a. Ord a => a -> a -> Bool
<= Integer
b) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => Multiset a -> a -> Integer
multiplicity (forall n e. Path n e -> Multiset (State n)
stateMultiset Path n e
p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Transition n e -> State n
destination)) forall a b. (a -> b) -> a -> b
$
>       forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
fsa

> -- |Initial open list for traversal from initial states.
> initialsPaths :: (Ord e, Ord n) => FSA n e -> Set (Path n e)
> initialsPaths :: forall e n. (Ord e, Ord n) => FSA n e -> Set (Path n e)
initialsPaths = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall {n} {e}. Ord n => State n -> Path n e
iPath forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. FSA n e -> Set (State n)
initials
>     where iPath :: State n -> Path n e
iPath State n
s = forall n e.
[Symbol e]
-> Maybe (State n) -> Multiset (State n) -> Integer -> Path n e
Path [] (forall a. a -> Maybe a
Just State n
s) (forall c a. Container c a => a -> c
singleton State n
s) Integer
0

> -- |Initial open list for non-deterministic traversal from initial states.
> initialsNDPath :: (Ord e, Ord n) => FSA n e -> Path (Set n) e
> initialsNDPath :: forall e n. (Ord e, Ord n) => FSA n e -> Path (Set n) e
initialsNDPath FSA n e
fsa = Path { labels :: [Symbol e]
labels = forall c a. Container c a => c
empty
>                           , endstate :: Maybe (State (Set n))
endstate = forall a. a -> Maybe a
Just State (Set n)
istate
>                           , stateMultiset :: Multiset (State (Set n))
stateMultiset = forall c a. Container c a => a -> c
singleton State (Set n)
istate
>                           , depth :: Integer
depth = Integer
0
>                           }
>     where istate :: State (Set n)
istate = forall n. n -> State n
State forall a b. (a -> b) -> a -> b
$ forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n. State n -> n
nodeLabel (forall n e. FSA n e -> Set (State n)
initials FSA n e
fsa)

> truth :: a -> b -> Bool
> truth :: forall a b. a -> b -> Bool
truth = forall a b. a -> b -> a
const (forall a b. a -> b -> a
const Bool
True)

traversalQDFS:
* First argument is a predicate that is used to filter paths before
  adding them to the closed list
* Remaining args are the FSA, a depth bound, the open list, and
  the closed list
* Paths are not added to the open list unless their depth is <= bound

> traversalQDFS :: (Ord e, Ord n) =>
>                  (FSA n e -> Path n e -> Bool) ->
>                  FSA n e ->
>                  Integer ->
>                  Set (Path n e) ->
>                  Set (Path n e) ->
>                  Set (Path n e)
> traversalQDFS :: forall e n.
(Ord e, Ord n) =>
(FSA n e -> Path n e -> Bool)
-> FSA n e
-> Integer
-> Set (Path n e)
-> Set (Path n e)
-> Set (Path n e)
traversalQDFS FSA n e -> Path n e -> Bool
qf FSA n e
fsa Integer
bound Set (Path n e)
open Set (Path n e)
closed
>     | forall c a. Container c a => c -> Bool
isEmpty Set (Path n e)
open     =  Set (Path n e)
closed
>     | forall n e. Path n e -> Integer
depth Path n e
p forall a. Ord a => a -> a -> Bool
> Integer
bound  =  forall e n.
(Ord e, Ord n) =>
(FSA n e -> Path n e -> Bool)
-> FSA n e
-> Integer
-> Set (Path n e)
-> Set (Path n e)
-> Set (Path n e)
traversalQDFS FSA n e -> Path n e -> Bool
qf FSA n e
fsa Integer
bound Set (Path n e)
ps Set (Path n e)
addIf
>     | Bool
otherwise        =  forall e n.
(Ord e, Ord n) =>
(FSA n e -> Path n e -> Bool)
-> FSA n e
-> Integer
-> Set (Path n e)
-> Set (Path n e)
-> Set (Path n e)
traversalQDFS FSA n e -> Path n e -> Bool
qf FSA n e
fsa Integer
bound
>                           (forall c a. Container c a => c -> c -> c
union Set (Path n e)
ps forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Path n e -> Set (Path n e)
extensions FSA n e
fsa Path n e
p)
>                           Set (Path n e)
addIf
>     where (Path n e
p, Set (Path n e)
ps) = forall (l :: * -> *) a. Linearizable l => l a -> (a, l a)
choose Set (Path n e)
open
>           addIf :: Set (Path n e)
addIf
>               | FSA n e -> Path n e -> Bool
qf FSA n e
fsa Path n e
p   =  forall c a. Container c a => a -> c -> c
insert Path n e
p Set (Path n e)
closed
>               | Bool
otherwise  =  Set (Path n e)
closed

acyclicPathsQ
all paths from the initial open list that are acyclic / and are restricted to
nodes that satisfy the given predicate

> acyclicPathsQ :: (Ord e, Ord n) =>
>                  (FSA n e -> Path n e -> Bool) ->  -- predicate
>                  FSA n e ->                        -- graph
>                  Set (Path n e) ->                 -- open
>                  Set (Path n e) ->                 -- closed
>                  Set (Path n e)
> acyclicPathsQ :: forall e n.
(Ord e, Ord n) =>
(FSA n e -> Path n e -> Bool)
-> FSA n e -> Set (Path n e) -> Set (Path n e) -> Set (Path n e)
acyclicPathsQ FSA n e -> Path n e -> Bool
qf FSA n e
fsa Set (Path n e)
open Set (Path n e)
closed
>     | Set (Path n e)
open forall a. Eq a => a -> a -> Bool
== forall c a. Container c a => c
empty  =  Set (Path n e)
closed
>     | Bool
otherwise      =  forall e n.
(Ord e, Ord n) =>
(FSA n e -> Path n e -> Bool)
-> FSA n e -> Set (Path n e) -> Set (Path n e) -> Set (Path n e)
acyclicPathsQ FSA n e -> Path n e -> Bool
qf FSA n e
fsa
>                         (forall c a. Container c a => c -> c -> c
union Set (Path n e)
ps forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Path n e -> Set (Path n e)
acyclicExtensions FSA n e
fsa Path n e
p)
>                         Set (Path n e)
addIf
>     where (Path n e
p, Set (Path n e)
ps) = forall (l :: * -> *) a. Linearizable l => l a -> (a, l a)
choose Set (Path n e)
open
>           addIf :: Set (Path n e)
addIf
>               | FSA n e -> Path n e -> Bool
qf FSA n e
fsa Path n e
p   =  forall c a. Container c a => a -> c -> c
insert Path n e
p Set (Path n e)
closed
>               | Bool
otherwise  =  Set (Path n e)
closed

> -- |All paths from 'initialsPaths' that do not contain cycles.
> acyclicPaths :: (Ord e, Ord n) => FSA n e -> Set (Path n e)
> acyclicPaths :: forall e n. (Ord e, Ord n) => FSA n e -> Set (Path n e)
acyclicPaths FSA n e
fsa = forall e n.
(Ord e, Ord n) =>
(FSA n e -> Path n e -> Bool)
-> FSA n e -> Set (Path n e) -> Set (Path n e) -> Set (Path n e)
acyclicPathsQ forall a b. a -> b -> Bool
truth FSA n e
fsa (forall e n. (Ord e, Ord n) => FSA n e -> Set (Path n e)
initialsPaths FSA n e
fsa) forall c a. Container c a => c
empty

rejectingPaths fsa bound
= all rejecting Paths of length <= bound

> -- |All paths of length less than or equal to a given bound
> -- that do not end in an accepting state.
> rejectingPaths :: (Ord e, Ord n) => FSA n e -> Integer -> Set (Path n e)
> rejectingPaths :: forall e n. (Ord e, Ord n) => FSA n e -> Integer -> Set (Path n e)
rejectingPaths FSA n e
fsa Integer
bound = forall e n.
(Ord e, Ord n) =>
(FSA n e -> Path n e -> Bool)
-> FSA n e
-> Integer
-> Set (Path n e)
-> Set (Path n e)
-> Set (Path n e)
traversalQDFS forall {n} {e} {e}. Ord n => FSA n e -> Path n e -> Bool
rejecting
>                            FSA n e
fsa Integer
bound (forall e n. (Ord e, Ord n) => FSA n e -> Set (Path n e)
initialsPaths FSA n e
fsa) forall c a. Container c a => c
empty
>     where rejecting :: FSA n e -> Path n e -> Bool
rejecting FSA n e
f Path n e
p = forall c a. (Container c a, Eq a) => a -> c -> Bool
doesNotContain (forall n e. Path n e -> Maybe (State n)
endstate Path n e
p) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                           forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
finals FSA n e
f

> -- |True iff the given FSA contains no reachable cycles.
> --
> -- @since 1.0
> isAcyclic :: (Ord n, Ord e) => FSA n e -> Bool
> isAcyclic :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isAcyclic FSA n e
f = forall c a. Container c a => c -> Bool
isEmpty
>               forall a b. (a -> b) -> a -> b
$ forall e n.
(Ord e, Ord n) =>
(FSA n e -> Path n e -> Bool)
-> FSA n e
-> Integer
-> Set (Path n e)
-> Set (Path n e)
-> Set (Path n e)
traversalQDFS forall {n} {p} {e}. Ord n => p -> Path n e -> Bool
hasCycle FSA n e
f (Integer
n forall a. Num a => a -> a -> a
+ Integer
1) (forall e n. (Ord e, Ord n) => FSA n e -> Set (Path n e)
initialsPaths FSA n e
f) forall c a. Container c a => c
empty
>     where hasCycle :: p -> Path n e -> Bool
hasCycle p
_ = forall a. Eq a => a -> a -> Bool
(/=) (forall c a. Container c a => a -> c
singleton Integer
1)
>                        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => Multiset a -> Set Integer
multiplicities
>                        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Path n e -> Multiset (State n)
stateMultiset
>           n :: Integer
n = forall (c :: * -> *) a b. (Collapsible c, Integral a) => c b -> a
size forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
f