# Automata theory, state reachability in Haskell

I wrote a small library to learn Haskell while studying Automata theory. I have some concerns on my algorithm to evaluate state reachability. That is, I think it might be improved if I can avoid checking paths already excluded in other branches of the search for a valid path. This one recursively checks each path separately.

I hope I didn't forget anything. Other suggestions are obviously welcome!

## Automaton data type

-- | Represents an automaton in the form
--   /G = (X, E, f, Gamma, x_0, X_m)/
--
--   NB: we're not including Gamma in the definition of Automaton
data Automa st ev = Automa {
states     :: [st],             -- ^ /X/, set of states
events     :: [ev],             -- ^ /E/, set of events
mapTrans   :: M.Map (st,ev) st, -- ^ not /f/, but a map of
--   transitions (see 'trans')
initial    :: st,               -- ^ /x_0/, initial state
marked     :: [st]              -- ^ /X_m/, set of marked states


## Reachability function

-- | True if a state can reach another for some string of events.
canReach :: (Ord st, Ord ev)
=> st                   -- ^ starting state 's'
-> st                   -- ^ arrival state 's''
-> Automa st ev
-> Bool
canReach s s' au = canReachExcluding s s' au []

-- | True if a state can reach another for some string of events,
--   excluding passing from specified states.
canReachExcluding :: (Ord st, Ord ev)
=> st                   -- ^ starting state 's'
-> st                   -- ^ arrival state 's''
-> Automa st ev
-> [st]                 -- ^ the states to be excluded
-> Bool
canReachExcluding s s' au ex = s == s' || any (== s') rs
|| any (\x -> canReachExcluding x s' au (s:ex)) rs
where rs = reach1From s au \\ ex

-- | Returns states reachable from specified state in one step.
reach1From :: (Ord st, Ord ev) => st -> Automa st ev -> [st]
reach1From s au = [ trans' (s,e) au | e <- gammaL s au ]


## Accessory functions

-- | Indicator function of active states for an automaton
gamma :: (Ord st, Ord ev)
=> (st,ev)                 -- ^ state-event pair of interest
-> Automa st ev
-> Bool                    -- ^ 'True' if 'ev' is active for 'st'
gamma (s,e) au = M.member (s,e) $mapTrans au -- | Returns a list of active events for a state of a given 'Automa' gammaL :: (Ord st, Ord ev) => st -> Automa st ev -> [ev] gammaL s au = [ e | e <- events au, gamma (s,e) au ] -- | Transition function: where do I get if 'ev' happens when in 'st'? trans :: (Ord st, Ord ev) => (st, ev) -> Automa st ev -> Maybe st trans (s,e) au = M.lookup (s,e)$ mapTrans au

-- | Like 'trans', but to be used if you're sure it's a valid
--   transition (i.e. saves you a 'fromJust').
trans' :: (Ord st, Ord ev) => (st, ev) -> Automa st ev -> st
trans' (s,e) au = fromJust $M.lookup (s,e)$ mapTrans au


1. Is the || any (== s') rs part of canReachExcluding necessary?
2. In the same definition, the part rs = reach1From s au \\ ex takes time linear in the size of ex. Using a set (or hash) instead of a list for ex would probably improve your running time significantly in practice. But of course, that'd likely be at the expense of the clarity of your beautiful program.