defToNFAWithBoundaries :: NFADef NFAWBLabel
                       -> Either String (NFAWithBoundaries Int)
defToNFAWithBoundaries (NFADef is ts fs) = do
    let lSizes@(l, r) = getFirstBoundarySizes ts
    -- Turn the list of transitions into a list of Eithers which are sequenced
    trans <- DT.sequence . runEitherT $ makeTrans lSizes
    let listsToSignalMap = M.fromListWith (M.unionWith S.union)
        lts = LTS . M.map signalsMapToBDD . listsToSignalMap $ trans
        nfa = NFA lts (`inNEL` is) (`elem` fs)
    return $ NFAWithBoundaries nfa l r
  where
    getFirstBoundarySizes (NFATransDef _ (NFAWBLabel l r :| _) _ :| _) =
        (genericLength l, genericLength r)

    makeTrans lSizes = lift (NEL.toList ts) >>= toTrans lSizes

    -- ss, ls and ts are all (non-empty) lists, so we use the list Monad to
    -- construct a single list of pairs from source states to a BDD map.
    toTrans lSizes (NFATransDef srcs ls trgs) = do
        s <- lift $ NEL.toList srcs
        l <- lift $ NEL.toList ls
        converted <- hoistEither $ convertLabel lSizes l
        return (s, M.singleton converted (S.fromList . NEL.toList $ trgs))

    convertLabel :: (Int, Int) -> NFAWBLabel
                 -> Either String (BoundarySignals, BoundarySignals)
    convertLabel (lSize, rSize) (NFAWBLabel ls rs) = do
        check lSize ls True
        check rSize rs False
        Right (toBS ls, toBS rs)
      where
        -- Catch invalid labels
        check size list isLeft = when (genericLength list /= size) $
            Left $ "Invalid length "
                   ++ (if isLeft then "left" else "right")
                   ++ "list: " ++ show list

        -- toBS constructs a BoundarySignals, a Map from Int to (No)Signal
        toBS = foldr go M.empty . zip [0..]

        -- Ignore stars, their variable's value doesn't matter
        go (pos, x) m = let s = case x of
                                    Zero -> Just NoSignal
                                    One -> Just Signal
                                    Star -> Nothing
                        in maybe m (\s' -> M.insert pos s' m) s
defToNFAWithBoundaries :: NFADef NFAWBLabel
                       -> Either String (NFAWithBoundaries Int)
defToNFAWithBoundaries (NFADef is ts fs) = do
    let lSizes@(l, r) = getFirstBoundarySizes ts
    -- Turn the list of transitions into a list of Eithers which are sequenced
    trans <- DT.sequence . runEitherT $ makeTrans lSizes
    let listsToSignalMap = M.fromListWith (M.unionWith S.union)
        lts = LTS . M.map signalsMapToBDD . listsToSignalMap $ trans
        nfa = NFA lts (`inNEL` is) (`elem` fs)
    return $ NFAWithBoundaries nfa l r
  where
    getFirstBoundarySizes (NFATransDef _ (NFAWBLabel l r :| _) _ :| _) =
        (genericLength l, genericLength r)

    makeTrans lSizes = lift (NEL.toList ts) >>= toTrans lSizes

    -- ss, ls and ts are all (non-empty) lists, so we use the list Monad to
    -- construct a single list of pairs from source states to a BDD map.
    toTrans lSizes (NFATransDef srcs ls trgs) = do
        s <- lift $ NEL.toList srcs
        l <- lift $ NEL.toList ls
        converted <- hoistEither $ convertLabel lSizes l
        return (s, M.singleton converted (S.fromList . NEL.toList $ trgs))

    convertLabel :: (Int, Int) -> NFAWBLabel
                 -> Either String (BoundarySignals, BoundarySignals)
    convertLabel (lSize, rSize) (NFAWBLabel ls rs) = do
        check lSize ls True
        check rSize rs False
        Right (toBS ls, toBS rs)
      where
        -- Catch invalid labels
        check size list isLeft = when (genericLength list /= size) $
            Left $ "Invalid length "
                   ++ (if isLeft then "left" else "right")
                   ++ "list: " ++ show list

        -- toBS constructs a BoundarySignals, a Map from Int to (No)Signal
        toBS = foldr go M.empty . zip [0..]

        -- Ignore stars, their variable's value doesn't matter
        go (pos, x) m = let s = case x of
                                    Zero -> Just NoSignal
                                    One -> Just Signal
                                    Star -> Nothing
                        in maybe m (\s' -> M.insert pos s' m) s
defToNFAWithBoundaries (NFADef is ts fs) = do
    let lSizes@(l, r) = getFirstBoundarySizes ts
    -- Turn the list of transitions into a list of Eithers which are sequenced
    trans <- DT.sequence . runEitherT $ makeTrans lSizes
    let listsToSignalMap = M.fromListWith (M.unionWith S.union)
        lts = LTS . M.map signalsMapToBDD . listsToSignalMap $ trans
        nfa = NFA lts (`inNEL` is) (`elem` fs)
    return $ NFAWithBoundaries nfa l r
  where
    getFirstBoundarySizes (NFATransDef _ (NFAWBLabel l r :| _) _ :| _) =
        (genericLength l, genericLength r)

    makeTrans lSizes = lift (NEL.toList ts) >>= toTrans lSizes

    -- ss, ls and ts are all (non-empty) lists, so we use the list Monad to
    -- construct a single list of pairs from source states to a BDD map.
    toTrans lSizes (NFATransDef srcs ls trgs) = do
        s <- lift $ NEL.toList srcs
        l <- lift $ NEL.toList ls
        converted <- hoistEither $ convertLabel lSizes l
        return (s, M.singleton converted (S.fromList . NEL.toList $ trgs))

    convertLabel :: (Int, Int) -> NFAWBLabel
                 -> Either String (BoundarySignals, BoundarySignals)
    convertLabel (lSize, rSize) (NFAWBLabel ls rs) = do
        check lSize ls True
        check rSize rs False
        Right (toBS ls, toBS rs)
      where
        -- Catch invalid labels
        check size list isLeft = when (genericLength list /= size) $
            Left $ "Invalid length "
                   ++ (if isLeft then "left" else "right")
                   ++ "list: " ++ show list

        -- toBS constructs a BoundarySignals, a Map from Int to (No)Signal
        toBS = foldr go M.empty . zip [0..]

        -- Ignore stars, their variable's value doesn't matter
        go (pos, x) m = let s = case x of
                                    Zero -> Just NoSignal
                                    One -> Just Signal
                                    Star -> Nothing
                        in maybe m (\s' -> M.insert pos s' m) s