> {-# 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 t'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 t'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
(Path n e -> Path n e -> Bool)
-> (Path n e -> Path n e -> Bool) -> Eq (Path n e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n e. (Eq e, Eq n) => 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
/= :: Path n e -> Path n e -> Bool
Eq, Int -> Path n e -> ShowS
[Path n e] -> ShowS
Path n e -> String
(Int -> Path n e -> ShowS)
-> (Path n e -> String) -> ([Path n e] -> ShowS) -> Show (Path n e)
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
$cshowsPrec :: forall n e. (Show e, Show n) => Int -> Path n e -> ShowS
showsPrec :: Int -> Path n e -> ShowS
$cshow :: forall n e. (Show e, Show n) => Path n e -> String
show :: Path n e -> String
$cshowList :: forall n e. (Show e, Show n) => [Path n e] -> ShowS
showList :: [Path n e] -> ShowS
Show)

> -- |The reversal of the 'labels' of the t'Path'.
> word :: Path n e -> [Symbol e]
> word :: forall n e. Path n e -> [Symbol e]
word = [Symbol e] -> [Symbol e]
forall a. [a] -> [a]
Prelude.reverse ([Symbol e] -> [Symbol e])
-> (Path n e -> [Symbol e]) -> Path n e -> [Symbol e]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Path n e -> [Symbol e]
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
>               = [Ordering] -> Ordering
forall a. Monoid a => [a] -> a
mconcat [Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
d1 Integer
d2, [Symbol e] -> [Symbol e] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare [Symbol e]
l1 [Symbol e]
l2, Maybe (State n) -> Maybe (State n) -> Ordering
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)  =  (Path n e -> Maybe (State n)
forall n e. Path n e -> Maybe (State n)
endstate Path n e
p1, Path n e -> [Symbol e]
forall n e. Path n e -> [Symbol e]
labels Path n e
p1, Path n e -> Integer
forall n e. Path n e -> Integer
depth Path n e
p1)
>                     (Maybe (State n)
e2, [Symbol e]
l2, Integer
d2)  =  (Path n e -> Maybe (State n)
forall n e. Path n e -> Maybe (State n)
endstate Path n e
p2, Path n e -> [Symbol e]
forall n e. Path n e -> [Symbol e]
labels Path n e
p2, Path n e -> Integer
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 [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ [Symbol e]
xs2
>            , endstate :: Maybe (State n)
endstate       =  (Maybe (State n) -> Maybe (State n))
-> (State n -> Maybe (State n) -> Maybe (State n))
-> Maybe (State n)
-> Maybe (State n)
-> Maybe (State n)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe (State n) -> Maybe (State n)
forall a. a -> a
id (Maybe (State n) -> Maybe (State n) -> Maybe (State n)
forall a b. a -> b -> a
const (Maybe (State n) -> Maybe (State n) -> Maybe (State n))
-> (State n -> Maybe (State n))
-> State n
-> Maybe (State n)
-> Maybe (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State n -> Maybe (State n)
forall a. a -> Maybe a
Just) Maybe (State n)
q1 Maybe (State n)
q2
>            , stateMultiset :: Multiset (State n)
stateMultiset  =  Multiset (State n)
qs1 Multiset (State n) -> Multiset (State n) -> Multiset (State n)
forall c a. Container c a => c -> c -> c
`union` Multiset (State n)
qs2
>            , depth :: Integer
depth          =  Integer
d1 Integer -> Integer -> Integer
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
(<>) = 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 = [Symbol e]
-> Maybe (State n) -> Multiset (State n) -> Integer -> Path n e
forall n e.
[Symbol e]
-> Maybe (State n) -> Multiset (State n) -> Integer -> Path n e
Path [] Maybe (State n)
forall a. Maybe a
Nothing Multiset (State n)
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 = (Transition n e -> Path n e)
-> Set (Transition n e) -> Set (Path n e)
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    =  Transition n e -> Symbol e
forall n e. Transition n e -> Symbol e
edgeLabel Transition n e
t Symbol e -> [Symbol e] -> [Symbol e]
forall a. a -> [a] -> [a]
: Path n e -> [Symbol e]
forall n e. Path n e -> [Symbol e]
labels Path n e
p
>                       , endstate :: Maybe (State n)
endstate  =  State n -> Maybe (State n)
forall a. a -> Maybe a
Just (Transition n e -> State n
forall n e. Transition n e -> State n
destination Transition n e
t)
>                       , stateMultiset :: Multiset (State n)
stateMultiset
>                             = Transition n e -> State n
forall n e. Transition n e -> State n
destination Transition n e
t State n -> Multiset (State n) -> Multiset (State n)
forall c a. Container c a => a -> c -> c
`insert` Path n e -> Multiset (State n)
forall n e. Path n e -> Multiset (State n)
stateMultiset Path n e
p
>                       , depth :: Integer
depth     = Path n e -> Integer
forall n e. Path n e -> Integer
depth Path n e
p Integer -> Integer -> Integer
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
>     | Set (Transition n e) -> Bool
forall c a. Container c a => c -> Bool
isEmpty Set (Transition n e)
ts = Path (Set n) e -> Set (Path (Set n) e)
forall c a. Container c a => a -> c
singleton Path (Set n) e
p
>     | Bool
otherwise
>         = (Set (Transition n e) -> Path (Set n) e)
-> Set (Set (Transition n e)) -> Set (Path (Set n) e)
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  =  Set n -> State (Set n)
forall n. n -> State n
State (Set n -> State (Set n)) -> Set n -> State (Set n)
forall a b. (a -> b) -> a -> b
$ (Transition n e -> Set n -> Set n)
-> Set n -> Set (Transition n e) -> Set n
forall a b. (a -> b -> b) -> b -> Set a -> b
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse Transition n e -> Set n -> Set n
forall {c} {e}. Container c n => Transition n e -> c -> c
f Set n
forall c a. Container c a => c
empty Set (Transition n e)
xs
>            in Path (Set n) e
p { labels    =  chooseOne (tmap edgeLabel xs) : labels p
>                 , endstate  =  Just newState
>                 , stateMultiset
>                       =  insert newState (stateMultiset p)
>                 , depth     =  depth p + 1
>                 }
>           ) Set (Set (Transition n e))
tgroups
>     where tgroups :: Set (Set (Transition n e))
tgroups = (Transition n e -> Symbol e)
-> Set (Transition n e) -> Set (Set (Transition n e))
forall a n. (Ord a, Ord n) => (n -> a) -> Set n -> Set (Set n)
partitionBy Transition n e -> Symbol e
forall n e. Transition n e -> Symbol e
edgeLabel Set (Transition n e)
ts
>           connectable :: n -> Bool
connectable
>               = (n -> Bool)
-> (State (Set n) -> n -> Bool)
-> Maybe (State (Set n))
-> n
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bool -> n -> Bool
forall a b. a -> b -> a
const Bool
False) (Set n -> n -> Bool
forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn (Set n -> n -> Bool)
-> (State (Set n) -> Set n) -> State (Set n) -> n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (Set n) -> Set n
forall n. State n -> n
nodeLabel) (Path (Set n) e -> Maybe (State (Set n))
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 (n -> Bool) -> (State n -> n) -> State n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State n -> n
forall n. State n -> n
nodeLabel (State n -> Bool) -> State n -> Bool
forall a b. (a -> b) -> a -> b
$ Transition n e -> State n
forall n e. Transition n e -> State n
source Transition n e
x
>                 then n -> c -> c
forall c a. Container c a => a -> c -> c
insert (State n -> n
forall n. State n -> n
nodeLabel (State n -> n) -> State n -> n
forall a b. (a -> b) -> a -> b
$ Transition n e -> State n
forall n e. Transition n e -> State n
destination Transition n e
x)
>                 else c -> c
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
>     = Path n e -> Set (Transition n e) -> Set (Path n e)
forall e n.
(Ord e, Ord n) =>
Path n e -> Set (Transition n e) -> Set (Path n e)
extend Path n e
p (Set (Transition n e) -> Set (Path n e))
-> (Set (Transition n e) -> Set (Transition n e))
-> Set (Transition n e)
-> Set (Path n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Transition n e -> Bool)
-> Set (Transition n e) -> Set (Transition n e)
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep ((Maybe (State n) -> Maybe (State n) -> Bool
forall a. Eq a => a -> a -> Bool
== Path n e -> Maybe (State n)
forall n e. Path n e -> Maybe (State n)
endstate Path n e
p) (Maybe (State n) -> Bool)
-> (Transition n e -> Maybe (State n)) -> Transition n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State n -> Maybe (State n)
forall a. a -> Maybe a
Just (State n -> Maybe (State n))
-> (Transition n e -> State n) -> Transition n e -> Maybe (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition n e -> State n
forall n e. Transition n e -> State n
source) (Set (Transition n e) -> Set (Path n e))
-> Set (Transition n e) -> Set (Path n e)
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (Transition n e)
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
>     = Path n e -> Set (Transition n e) -> Set (Path n e)
forall e n.
(Ord e, Ord n) =>
Path n e -> Set (Transition n e) -> Set (Path n e)
extend Path n e
p (Set (Transition n e) -> Set (Path n e))
-> (Set (Transition n e) -> Set (Transition n e))
-> Set (Transition n e)
-> Set (Path n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>       (Transition n e -> Bool)
-> Set (Transition n e) -> Set (Transition n e)
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep ((Transition n e -> Bool)
-> (Transition n e -> Bool) -> Transition n e -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
both
>             (Multiset (State n) -> State n -> Bool
forall c a. (Container c a, Eq a) => c -> a -> Bool
isNotIn (Path n e -> Multiset (State n)
forall n e. Path n e -> Multiset (State n)
stateMultiset Path n e
p) (State n -> Bool)
-> (Transition n e -> State n) -> Transition n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition n e -> State n
forall n e. Transition n e -> State n
destination)
>             ((Maybe (State n) -> Maybe (State n) -> Bool
forall a. Eq a => a -> a -> Bool
== Path n e -> Maybe (State n)
forall n e. Path n e -> Maybe (State n)
endstate Path n e
p) (Maybe (State n) -> Bool)
-> (Transition n e -> Maybe (State n)) -> Transition n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State n -> Maybe (State n)
forall a. a -> Maybe a
Just (State n -> Maybe (State n))
-> (Transition n e -> State n) -> Transition n e -> Maybe (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition n e -> State n
forall n e. Transition n e -> State n
source)) (Set (Transition n e) -> Set (Path n e))
-> Set (Transition n e) -> Set (Path n e)
forall a b. (a -> b) -> a -> b
$
>       FSA n e -> Set (Transition n e)
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
>     = (Path (Set n) e -> Bool)
-> Set (Path (Set n) e) -> Set (Path (Set n) e)
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep
>       (\Path (Set n) e
a ->
>        Bool -> (State (Set n) -> Bool) -> Maybe (State (Set n)) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
1) (Integer -> Bool)
-> (State (Set n) -> Integer) -> State (Set n) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Multiset (State (Set n)) -> State (Set n) -> Integer
forall a. Ord a => Multiset a -> a -> Integer
multiplicity (Path (Set n) e -> Multiset (State (Set n))
forall n e. Path n e -> Multiset (State n)
stateMultiset Path (Set n) e
a)) (Path (Set n) e -> Maybe (State (Set n))
forall n e. Path n e -> Maybe (State n)
endstate Path (Set n) e
a)
>       ) (Set (Path (Set n) e) -> Set (Path (Set n) e))
-> (Path (Set n) e -> Set (Path (Set n) e))
-> Path (Set n) e
-> Set (Path (Set n) e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Path (Set n) e -> Set (Transition n e) -> Set (Path (Set n) e))
-> Set (Transition n e) -> Path (Set n) e -> Set (Path (Set n) e)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Path (Set n) e -> Set (Transition n e) -> Set (Path (Set n) e)
forall e n.
(Ord e, Ord n) =>
Path (Set n) e -> Set (Transition n e) -> Set (Path (Set n) e)
nondeterministicExtend (FSA n e -> Set (Transition n e)
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
>     = Path n e -> Set (Transition n e) -> Set (Path n e)
forall e n.
(Ord e, Ord n) =>
Path n e -> Set (Transition n e) -> Set (Path n e)
extend Path n e
p (Set (Transition n e) -> Set (Path n e))
-> (Set (Transition n e) -> Set (Transition n e))
-> Set (Transition n e)
-> Set (Path n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>       (Transition n e -> Bool)
-> Set (Transition n e) -> Set (Transition n e)
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep ((Transition n e -> Bool)
-> (Transition n e -> Bool) -> Transition n e -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
both
>             ((Maybe (State n) -> Maybe (State n) -> Bool
forall a. Eq a => a -> a -> Bool
== Path n e -> Maybe (State n)
forall n e. Path n e -> Maybe (State n)
endstate Path n e
p) (Maybe (State n) -> Bool)
-> (Transition n e -> Maybe (State n)) -> Transition n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State n -> Maybe (State n)
forall a. a -> Maybe a
Just (State n -> Maybe (State n))
-> (Transition n e -> State n) -> Transition n e -> Maybe (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition n e -> State n
forall n e. Transition n e -> State n
source)
>             ((Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
b) (Integer -> Bool)
-> (Transition n e -> Integer) -> Transition n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Multiset (State n) -> State n -> Integer
forall a. Ord a => Multiset a -> a -> Integer
multiplicity (Path n e -> Multiset (State n)
forall n e. Path n e -> Multiset (State n)
stateMultiset Path n e
p) (State n -> Integer)
-> (Transition n e -> State n) -> Transition n e -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition n e -> State n
forall n e. Transition n e -> State n
destination)) (Set (Transition n e) -> Set (Path n e))
-> Set (Transition n e) -> Set (Path n e)
forall a b. (a -> b) -> a -> b
$
>       FSA n e -> Set (Transition n e)
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 = (State n -> Path n e) -> Set (State n) -> Set (Path n e)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap State n -> Path n e
forall {n} {e}. Ord n => State n -> Path n e
iPath (Set (State n) -> Set (Path n e))
-> (FSA n e -> Set (State n)) -> FSA n e -> Set (Path n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
initials
>     where iPath :: State n -> Path n e
iPath State n
s = [Symbol e]
-> Maybe (State n) -> Multiset (State n) -> Integer -> Path n e
forall n e.
[Symbol e]
-> Maybe (State n) -> Multiset (State n) -> Integer -> Path n e
Path [] (State n -> Maybe (State n)
forall a. a -> Maybe a
Just State n
s) (State n -> Multiset (State n)
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 = [Symbol e]
forall c a. Container c a => c
empty
>                           , endstate :: Maybe (State (Set n))
endstate = State (Set n) -> Maybe (State (Set n))
forall a. a -> Maybe a
Just State (Set n)
istate
>                           , stateMultiset :: Multiset (State (Set n))
stateMultiset = State (Set n) -> Multiset (State (Set n))
forall c a. Container c a => a -> c
singleton State (Set n)
istate
>                           , depth :: Integer
depth = Integer
0
>                           }
>     where istate :: State (Set n)
istate = Set n -> State (Set n)
forall n. n -> State n
State (Set n -> State (Set n)) -> Set n -> State (Set n)
forall a b. (a -> b) -> a -> b
$ (State n -> n) -> Set (State n) -> Set n
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap State n -> n
forall n. State n -> n
nodeLabel (FSA n e -> Set (State n)
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 = (b -> Bool) -> a -> b -> Bool
forall a b. a -> b -> a
const (Bool -> b -> Bool
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
>     | Set (Path n e) -> Bool
forall c a. Container c a => c -> Bool
isEmpty Set (Path n e)
open     =  Set (Path n e)
closed
>     | Path n e -> Integer
forall n e. Path n e -> Integer
depth Path n e
p Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
bound  =  (FSA n e -> Path n e -> Bool)
-> FSA n e
-> Integer
-> Set (Path n e)
-> Set (Path n e)
-> Set (Path n e)
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        =  (FSA n e -> Path n e -> Bool)
-> FSA n e
-> Integer
-> Set (Path n e)
-> Set (Path n e)
-> Set (Path n e)
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) -> Set (Path n e) -> Set (Path n e)
forall c a. Container c a => c -> c -> c
union Set (Path n e)
ps (Set (Path n e) -> Set (Path n e))
-> Set (Path n e) -> Set (Path n e)
forall a b. (a -> b) -> a -> b
$ FSA n e -> Path n e -> Set (Path n e)
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) = Set (Path n e) -> (Path n e, Set (Path n e))
forall a. Set a -> (a, Set a)
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   =  Path n e -> Set (Path n e) -> Set (Path n e)
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 Set (Path n e) -> Set (Path n e) -> Bool
forall a. Eq a => a -> a -> Bool
== Set (Path n e)
forall c a. Container c a => c
empty  =  Set (Path n e)
closed
>     | Bool
otherwise      =  (FSA n e -> Path n e -> Bool)
-> FSA n e -> Set (Path n e) -> Set (Path n e) -> Set (Path n e)
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) -> Set (Path n e) -> Set (Path n e)
forall c a. Container c a => c -> c -> c
union Set (Path n e)
ps (Set (Path n e) -> Set (Path n e))
-> Set (Path n e) -> Set (Path n e)
forall a b. (a -> b) -> a -> b
$ FSA n e -> Path n e -> Set (Path n e)
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) = Set (Path n e) -> (Path n e, Set (Path n e))
forall a. Set a -> (a, Set a)
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   =  Path n e -> Set (Path n e) -> Set (Path n e)
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 = (FSA n e -> Path n e -> Bool)
-> FSA n e -> Set (Path n e) -> Set (Path n e) -> Set (Path n e)
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
forall a b. a -> b -> Bool
truth FSA n e
fsa (FSA n e -> Set (Path n e)
forall e n. (Ord e, Ord n) => FSA n e -> Set (Path n e)
initialsPaths FSA n e
fsa) Set (Path n e)
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 = (FSA n e -> Path n e -> Bool)
-> FSA n e
-> Integer
-> Set (Path n e)
-> Set (Path n e)
-> Set (Path n e)
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
forall {n} {e} {e}. Ord n => FSA n e -> Path n e -> Bool
rejecting
>                            FSA n e
fsa Integer
bound (FSA n e -> Set (Path n e)
forall e n. (Ord e, Ord n) => FSA n e -> Set (Path n e)
initialsPaths FSA n e
fsa) Set (Path n e)
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 = Maybe (State n) -> Set (Maybe (State n)) -> Bool
forall c a. (Container c a, Eq a) => a -> c -> Bool
doesNotContain (Path n e -> Maybe (State n)
forall n e. Path n e -> Maybe (State n)
endstate Path n e
p) (Set (Maybe (State n)) -> Bool)
-> (Set (State n) -> Set (Maybe (State n)))
-> Set (State n)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                           (State n -> Maybe (State n))
-> Set (State n) -> Set (Maybe (State n))
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap State n -> Maybe (State n)
forall a. a -> Maybe a
Just (Set (State n) -> Bool) -> Set (State n) -> Bool
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (State n)
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 = Set (Path n e) -> Bool
forall c a. Container c a => c -> Bool
isEmpty
>               (Set (Path n e) -> Bool) -> Set (Path n e) -> Bool
forall a b. (a -> b) -> a -> b
$ (FSA n e -> Path n e -> Bool)
-> FSA n e
-> Integer
-> Set (Path n e)
-> Set (Path n e)
-> Set (Path n e)
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
forall {n} {p} {e}. Ord n => p -> Path n e -> Bool
hasCycle FSA n e
f (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (FSA n e -> Set (Path n e)
forall e n. (Ord e, Ord n) => FSA n e -> Set (Path n e)
initialsPaths FSA n e
f) Set (Path n e)
forall c a. Container c a => c
empty
>     where hasCycle :: p -> Path n e -> Bool
hasCycle p
_ = Set Integer -> Set Integer -> Bool
forall a. Eq a => a -> a -> Bool
(/=) (Integer -> Set Integer
forall c a. Container c a => a -> c
singleton Integer
1)
>                        (Set Integer -> Bool)
-> (Path n e -> Set Integer) -> Path n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Multiset (State n) -> Set Integer
forall a. Ord a => Multiset a -> Set Integer
multiplicities
>                        (Multiset (State n) -> Set Integer)
-> (Path n e -> Multiset (State n)) -> Path n e -> Set Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Path n e -> Multiset (State n)
forall n e. Path n e -> Multiset (State n)
stateMultiset
>           n :: Integer
n = Set (State n) -> Integer
forall a b. Integral a => Set b -> a
forall (c :: * -> *) a b. (Collapsible c, Integral a) => c b -> a
size (Set (State n) -> Integer) -> Set (State n) -> Integer
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (State n)
forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
f