haal 0.4.0.0 → 0.4.0.1
raw patch · 5 files changed
+259/−112 lines, 5 filesdep +liquidhaskelldep ~basedep ~containersdep ~mtl
Dependencies added: liquidhaskell
Dependency ranges changed: base, containers, mtl, process, random, vector
Files
- CHANGELOG.md +13/−1
- haal.cabal +23/−14
- src/Haal/BlackBox.hs +23/−2
- src/Haal/EquivalenceOracle/RandomWalk.hs +2/−2
- src/Haal/Learning/LMstar.hs +198/−93
CHANGELOG.md view
@@ -8,7 +8,19 @@ ## Unreleased -## 0.4.0.0 - 2026-03-16 +## 0.4.0.1 - 2026-03-17++### Added+- Optional `liquid` Cabal flag (`--flag haal:liquid`) to enable LiquidHaskell+ verification without requiring it as a dependency for normal builds.++### Verified+- `Haal.BlackBox`: `walk` produces outputs of length equal to the input length.+- `Haal.Learning.LMstar`: `ObservationTable` invariant that all entries in+ `mappingT` map to non-empty output lists, preserved across `updateMap`,+ `makeConsistent`, `makeClosed`, and `initializeOT`.++## 0.4.0.0 - 2026-03-16 ### Changed - Changed the types of oracles' constructors from `<Oracle>` to `Either String <Oracle>`
haal.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: haal-version: 0.4.0.0+version: 0.4.0.1 synopsis: A Haskell library for Active Automata Learning. description: Please see the README on GitHub at <https://github.com/steve-anunknown/haal#readme> category: Model Learning@@ -26,6 +26,11 @@ type: git location: https://github.com/steve-anunknown/haal +flag liquid+ description: Enable LiquidHaskell verification+ manual: True+ default: False+ library exposed-modules: Haal.Automaton.DFA@@ -47,12 +52,16 @@ src ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints build-depends:- base >=4.18.3 && <4.21- , containers ==0.6.*+ base >=4.18.3 && <4.19+ , containers >=0.6.7 && <0.7 , mtl >=2.3.1 && <2.4- , random ==1.2.1.*- , vector ==0.13.1.*+ , random >=1.3.1 && <1.4+ , vector >=0.13.2 && <0.14 default-language: Haskell2010+ if flag(liquid)+ cpp-options: -DLIQUID+ build-depends:+ liquidhaskell executable demo main-is: demo.hs@@ -65,7 +74,7 @@ ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints build-depends: base- , containers ==0.6.*+ , containers , haal default-language: Haskell2010 @@ -81,7 +90,7 @@ build-depends: base , haal- , mtl >=2.3.1 && <2.4+ , mtl default-language: Haskell2010 executable io@@ -96,8 +105,8 @@ build-depends: base , haal- , mtl >=2.3.1 && <2.4- , process >=1.6.19 && <1.6.25+ , mtl+ , process >=1.6.19 && <1.7 default-language: Haskell2010 executable website@@ -112,7 +121,7 @@ build-depends: base , haal- , process >=1.6.19 && <1.6.25+ , process >=1.6.19 && <1.7 default-language: Haskell2010 test-suite haal-test@@ -130,10 +139,10 @@ ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N build-depends: QuickCheck- , base >=4.18.3 && <4.21- , containers ==0.6.*+ , base >=4.18.3 && <4.19+ , containers , haal , hspec- , mtl >=2.3.1 && <2.4- , random ==1.2.1.*+ , mtl+ , random default-language: Haskell2010
src/Haal/BlackBox.hs view
@@ -1,7 +1,13 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-}+#ifdef LIQUID+{-# OPTIONS_GHC -fplugin=LiquidHaskell+ -fplugin-opt=LiquidHaskell:--prune-unsorted+ -fplugin-opt=LiquidHaskell:--no-termination #-}+#endif {- | This module defines the BlackBox type class as well as the Automaton and SUL sub classes.@@ -50,12 +56,15 @@ -- | Finite is an alias for (Enum, Bounded). type Finite i = (Enum i, Bounded i)+ -- | FiniteEq is an alias for (Eq, Finite). type FiniteEq i = (Eq i, Finite i)+ -- | FiniteOrd is an alias for (Ord, Bounded). type FiniteOrd i = (Ord i, Finite i) -- | Generalization of 'step' that operates on a list of inputs.+{-@ walk :: (SUL sul m) => sul i o -> xs:[i] -> m (sul i o, {ys:[o] | len ys == len xs}) @-} walk :: (SUL sul m) => sul i o -> [i] -> m (sul i o, [o]) walk sul [] = pure (sul, []) walk sul (x : xs) = do@@ -63,13 +72,25 @@ (sul'', os) <- walk sul' xs pure (sul'', o : os) +{-@ rangeIN :: (Enum i, Bounded i) => sul i o -> {is:[i] | len is > 0} @-}+rangeIN :: (Finite i) => sul i o -> [i]+rangeIN _ = minBound : [succ minBound .. maxBound]++{-@ rangeOUT :: (Enum o, Bounded o) => sul i o -> {os:[o] | len os > 0} @-}+rangeOUT :: (Finite o) => sul i o -> [o]+rangeOUT _ = minBound : [succ minBound .. maxBound]++{-@ assume Set.fromList :: Ord a => xs:[a] -> {s:Set.Set a | len xs > 0 => Set.size s > 0} @-}+ -- | Return a Set containing only the valid inputs of the SUL.+{-@ inputs :: (Ord i, Enum i, Bounded i) => sul i o -> {is:Set.Set i | Set.size is > 0} @-} inputs :: (FiniteOrd i) => sul i o -> Set.Set i-inputs _ = Set.fromList [minBound .. maxBound]+inputs x = Set.fromList $ rangeIN x -- | Return a Set containing only the valid outputs of the SUL.+{-@ outputs :: (Ord o, Enum o, Bounded o) => sul i o -> {os:Set.Set o | Set.size os > 0} @-} outputs :: (FiniteOrd o) => sul i o -> Set.Set o-outputs _ = Set.fromList [minBound .. maxBound]+outputs x = Set.fromList $ rangeOUT x {- | The 'Automaton' type class extends the 'SUL' type class and adds support for automata operations. Automatons are models, not programs,
src/Haal/EquivalenceOracle/RandomWalk.hs view
@@ -12,7 +12,7 @@ import Haal.Experiment import System.Random ( Random (randomR, randomRs),- RandomGen (split),+ SplitGen (splitGen), StdGen, ) @@ -36,7 +36,7 @@ -- | Generates a random walk for the automaton. randomWalkSuite :: (FiniteOrd a) => RandomWalk -> sul a o -> (RandomWalk, [[a]]) randomWalkSuite (RandomWalk (RandomWalkConfig{rwlGen = g, rwlMaxSteps = maxS, rwlRestart = restartP})) aut =- let (g1, g2) = split g+ let (g1, g2) = splitGen g alphabet = V.fromList . Set.toList $ inputs aut randomInputs = take maxS $ randomRs (0, V.length alphabet - 1) g1 inputSequence = map (alphabet V.!) randomInputs
src/Haal/Learning/LMstar.hs view
@@ -1,19 +1,27 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wno-redundant-constraints #-}+#ifdef LIQUID+{-# OPTIONS_GHC -fplugin=LiquidHaskell+ -fplugin-opt=LiquidHaskell:--prune-unsorted+ -fplugin-opt=LiquidHaskell:--no-termination #-}+#endif -- | This module implements the LM* algorithm for learning Mealy automata. module Haal.Learning.LMstar ( lmstar, LMstar,+ LMstarState (..), LMstarConfig (..), mkLMstar, ) where -import Control.Monad (foldM, forM)+import Control.Monad (foldM) import Control.Monad.Reader (MonadReader (ask), MonadTrans (lift))+import Data.Foldable (find) import qualified Data.List as List import qualified Data.Map as Map import qualified Data.Maybe as Maybe@@ -22,30 +30,80 @@ import Haal.BlackBox import Haal.Experiment +{-@ ignore otRefinePlus @-}+{-@ ignore otRefineAngluin @-}+{-@ ignore lmstar @-}++{-@ die :: {v:String | false} -> a @-}+die :: String -> a+die = error++{-@ headLH :: {v:[a] | len v > 0} -> a @-}+headLH :: [a] -> a+headLH [] = die "impossible: headLH called with empty list"+headLH (x : _) = x++{-@ dropLH :: xs:[a] -> {v:Int | 0 <= v && v < len xs} -> {r:[a] | len r = len xs - v} @-}+dropLH :: [a] -> Int -> [a]+dropLH list number+ | number >= length list = die "impossible: dropLH called with number larger than list length"+ | otherwise = drop number list+ -- | The 'ObservationTable' type is a data type for storing the observation table of the LM* algorithm.++{-@ data ObservationTable i o = ObservationTable+ { prefixSetS :: Set.Set [i]+ , suffixSetE :: Set.Set {v:[i] | len v > 0}+ , mappingT :: Map.Map ([i], [i]) {v:[o] | len v > 0}+ , prefixSetSI :: Set.Set {v:[i] | len v > 0}+ } @-} data ObservationTable i o = ObservationTable { prefixSetS :: Set.Set [i]+ -- ^ sm = prefix closed set over @i@ , suffixSetE :: Set.Set [i]- , mappingT :: Map.Map ([i], [i]) o- , -- more fields to avoid recomputing- prefixSetSI :: Set.Set [i]+ -- ^ em = suffix closed set over @i@, excluding the empty word+ , mappingT :: Map.Map ([i], [i]) [o]+ -- ^ tm = finite mapping from (sm U (sm * I)) X em -> @o@++ , prefixSetSI :: Set.Set [i]+ -- ^ sm * I = one-symbol extension of sm } deriving (Show) +{-@ assume Set.difference :: forall <p :: a -> Bool>.+ Ord a => Set.Set (a<p>) -> Set.Set a -> Set.Set (a<p>)+@-}+{-@ assume Set.cartesianProduct :: forall <p1 :: a -> Bool, p2 :: b -> Bool>.+ (Ord a, Ord b) => Set.Set (a<p1>) -> Set.Set (b<p2>) -> Set.Set (a<p1>, b<p2>)+@-}+ {- | The 'LMstarConfig' type is a configuration type for the LM* algorithm. It allows the user to choose between the original LM* algorithm and the LM+ algorithm. -} data LMstarConfig = Star | Plus --- | The 'LMstar' type is a wrapper around the 'ObservationTable' type and represents the LM* algorithm.-data LMstar i o = LMstar (ObservationTable i o) | LMplus (ObservationTable i o)+-- | The 'LMstarState' type tracks whether the observation table has been initialized.+data LMstarState i o = Uninit | Init (ObservationTable i o)+ deriving (Show) -{- | The 'mkLMstar' function creates a new instance of the 'LMstar' type. It holds a dummy value-so that the user does not have to provide an initial observation table.--}+{-@ measure _isUninit @-}+_isUninit :: LMstarState i o -> Bool+_isUninit Uninit = True+_isUninit _ = False++{-@ measure _lmState @-}+_lmState :: LMstar i o -> LMstarState i o+_lmState (LMstar s) = s+_lmState (LMplus s) = s++-- | The 'LMstar' type wraps an 'LMstarState' and represents the LM* algorithm.+data LMstar i o = LMstar (LMstarState i o) | LMplus (LMstarState i o)++-- | The 'mkLMstar' function creates a new uninitialized instance of the 'LMstar' type.++{-@ mkLMstar :: LMstarConfig -> {v:LMstar i o | _isUninit (_lmState v)} @-} mkLMstar :: LMstarConfig -> LMstar i o-mkLMstar Star = LMstar (error "this is invisible")-mkLMstar Plus = LMplus (error "this is invisible")+mkLMstar Star = LMstar Uninit+mkLMstar Plus = LMplus Uninit -- | The 'equivalentRows' function checks if two rows in the observation table are equivalent. equivalentRows :: forall i o. (Ord i, Eq o) => ObservationTable i o -> [i] -> [i] -> Bool@@ -63,18 +121,17 @@ ExperimentT (sul i o) m (ObservationTable i o) initializeOT = do sul <- ask- let alph = List.map (: []) $ Set.toList $ inputs sul+ let+ alph = List.map (: []) $ Set.toList $ inputs sul sm = Set.singleton []+ {-@ sm_I :: Set.Set {v:[i] | len v = 1} @-} sm_I = Set.fromList alph+ {-@ em :: Set.Set {v:[i] | len v = 1} @-} em = Set.fromList alph- domain = Set.toList $ (sm `Set.union` sm_I) `Set.cartesianProduct` em- -- monadic mapping because walk is in m- tmList <- forM domain $ \(in1, in2) -> do- sul0 <- lift $ reset sul- (_, outs) <- lift $ walk sul0 (in1 ++ in2)- pure ((in1, in2), last outs)-- let tm = Map.fromList tmList+ {-@ domain :: Set.Set ([i], {v:[i] | len v = 1}) @-}+ domain = (sm `Set.union` sm_I) `Set.cartesianProduct` em+ sulR <- lift $ reset sul+ tm <- lift $ updateMap Map.empty domain sulR return ( ObservationTable@@ -86,6 +143,8 @@ ) -- | The 'equivalenceClasses' function computes the equivalence classes of the observation table.++{-@ equivalenceClasses :: (FiniteOrd i, Eq o) => ObservationTable i o -> Map.Map [i] [[i]] @-} equivalenceClasses :: forall i o. (FiniteOrd i, Eq o) =>@@ -109,51 +168,72 @@ (SUL sul m, FiniteOrd i, Eq o, Monad m) => LMstar i o -> ExperimentT (sul i o) m (LMstar i o, MealyAutomaton StateID i o)-lmstar (LMstar ot) = case otIsClosed ot of+lmstar (LMstar (Init ot)) = case otIsClosed ot of [] -> case otIsConsistent ot of ([], []) -> case makeHypothesis ot of- Just hyp -> return (LMstar ot, hyp)- Nothing -> error "LM*: invariant violation — makeHypothesis failed on closed consistent table"+ Just hyp -> return (LMstar (Init ot), hyp)+ Nothing -> die "LM*: invariant violation — makeHypothesis failed on closed consistent table" inc' -> do ot' <- makeConsistent ot inc'- lmstar (LMstar ot')+ lmstar (LMstar (Init ot')) inc -> do ot' <- makeClosed ot inc- lmstar (LMstar ot')-lmstar (LMplus ot) = case otIsClosed ot of+ lmstar (LMstar (Init ot'))+lmstar (LMplus (Init ot)) = case otIsClosed ot of [] -> case makeHypothesis ot of- Just hyp -> return (LMplus ot, hyp)- Nothing -> error "LM+: invariant violation — makeHypothesis failed on closed table"+ Just hyp -> return (LMplus (Init ot), hyp)+ Nothing -> die "LM+: invariant violation — makeHypothesis failed on closed table" inc -> do ot' <- makeClosed ot inc- lmstar (LMplus ot')+ lmstar (LMplus (Init ot'))+lmstar (LMstar Uninit) = die "lmstar called before initialize"+lmstar (LMplus Uninit) = die "lmstar called before initialize" --- | The 'otIsClosed' function checks if the observation table is closed.+{- | The 'otIsClosed' function checks if the observation table is closed.+The observation table is closed if every prefix of `prefixSetSI` belongs+to the same equivalence class as some prefix of `prefixSetS`. If the observation+table is closed, it returns an empty list, whereas if it is not, it returns the+problematic prefix from `prefixSetSI` that does not have the same equivalence class+as any prefix from `prefixSetS`.+-} otIsClosed :: forall i o. (FiniteOrd i, Eq o) => ObservationTable i o -> [i] otIsClosed ot = Maybe.fromMaybe [] exists where sm = prefixSetS ot sm_I = prefixSetSI ot - exists = List.find (\x -> not $ any (equivalentRows ot x) sm) sm_I+ exists = find (\x -> not $ any (equivalentRows ot x) sm) sm_I --- | The 'otIsConsistent' function checks if the observation table is consistent.+{- | The 'otIsConsistent' function checks if the observation table is consistent.+Returns @([], [])@ if consistent, otherwise returns @([a], e)@ where @a@ is the+distinguishing letter and @e@ is an existing suffix witnessing the inconsistency,+so that @[a] ++ e@ can be added to E.+-} otIsConsistent :: forall i o. (FiniteOrd i, Eq o) => ObservationTable i o -> ([i], [i]) otIsConsistent ot = Maybe.fromMaybe ([], []) condition where alph = [minBound .. maxBound] :: [i] sm = Set.toList $ prefixSetS ot+ em = Set.toList $ suffixSetE ot - equivalentPairs = [(r1, r2) | r1 <- sm, r2 <- sm, r1 /= r2, equivalentRows ot r1 r2]+ equivalentPairs = [(r1, r2) | r1 <- sm, r2 <- sm, r1 <= r2, equivalentRows ot r1 r2] - condition =- List.find- ( \(a, b) ->- any- (\x -> not (equivalentRows ot (a ++ [x]) (b ++ [x])))- alph- )- equivalentPairs+ condition = do+ (s1, s2) <-+ find+ ( \(s1, s2) ->+ any (\x -> not (equivalentRows ot (s1 ++ [x]) (s2 ++ [x]))) alph+ )+ equivalentPairs+ x <-+ find+ (\x -> not (equivalentRows ot (s1 ++ [x]) (s2 ++ [x])))+ alph+ e <-+ find+ (\e -> Map.lookup (s1 ++ [x], e) (mappingT ot) /= Map.lookup (s2 ++ [x], e) (mappingT ot))+ em+ return ([x], e) -- | The 'otRefineAngluin' function refines the observation table based on a counterexample, according to Angluin's algorithm. otRefineAngluin ::@@ -182,6 +262,8 @@ the default 'StateID' type defined in the 'Experiment' module for representing the automaton states. Returns 'Nothing' if the observation table is malformed (invariant violated). -}++{-@ makeHypothesis :: (FiniteOrd i, Eq o) => ObservationTable i o -> Maybe (MealyAutomaton StateID i o) @-} makeHypothesis :: forall i o. (FiniteOrd i, Eq o) => ObservationTable i o -> Maybe (MealyAutomaton StateID i o) makeHypothesis ot = do startId <- getStateId []@@ -198,15 +280,14 @@ repList = Map.keys equivMap numStates = length repList repToId = Map.fromList (zip repList [0 ..])+ idToRep = Map.fromList (zip [0 ..] repList) alphaList = [minBound .. maxBound] :: [i] getStateId :: [i] -> Maybe StateID getStateId s = List.find (equivalentRows ot s) repList >>= flip Map.lookup repToId repAt :: StateID -> Maybe [i]- repAt sid- | sid >= 0 && sid < numStates = Just (repList !! sid)- | otherwise = Nothing+ repAt sid = Map.lookup sid idToRep buildDeltaEntry :: (StateID, i) -> Maybe ((StateID, i), StateID) buildDeltaEntry (sid, i) = do@@ -217,10 +298,15 @@ buildLambdaEntry :: (StateID, i) -> Maybe ((StateID, i), o) buildLambdaEntry (sid, i) = do rep <- repAt sid- o <- Map.lookup (rep, [i]) (mappingT ot)- return ((sid, i), o)+ out <- Map.lookup (rep, [i]) (mappingT ot)+ return ((sid, i), headLH out) -- | The 'makeConsistent' function makes the observation table consistent by adding missing prefixes.++{-@ makeConsistent :: (FiniteOrd i, SUL sul m) =>+ ObservationTable i o ->+ ({v:[i] | len v = 1}, {v:[i] | len v >= 1}) ->+ ExperimentT (sul i o) m (ObservationTable i o) @-} makeConsistent :: forall i o sul m. (FiniteOrd i, SUL sul m) =>@@ -228,33 +314,25 @@ ([i], [i]) -> ExperimentT (sul i o) m (ObservationTable i o) makeConsistent ot ([], []) = return ot-makeConsistent ot (column, symbol) = do+makeConsistent ot (symbol, column) = do sul <- ask let query = symbol ++ column- -- prefices = [take n query | n <- [1 .. length query]]-- -- only the query itself must be inserted.- -- the suffixes are already members. em = suffixSetE ot em' = query `Set.insert` em- sm = prefixSetS ot sm_I = prefixSetSI ot- tm = mappingT ot-- missing = (sm `Set.union` sm_I) `Set.cartesianProduct` em'- missing' = map (uncurry (++)) $ Set.toList missing-- outs <- lift $ forM missing' (walk sul)-- let- outs' = map (last . snd) outs- tm' = foldr (\((a, b), o) -> Map.insert (a, b) o) tm (zip (Set.toList missing) outs')+ missing = (sm `Set.union` sm_I) `Set.cartesianProduct` Set.singleton query+ tm' <- lift $ updateMap tm missing sul return (ObservationTable{prefixSetS = sm, suffixSetE = em', mappingT = tm', prefixSetSI = sm_I}) -- | The 'makeClosed' function makes the observation table closed by adding missing suffixes.++{-@ makeClosed :: (FiniteOrd i, SUL sul m) =>+ ObservationTable i o ->+ {v:[i] | len v > 0} ->+ ExperimentT (sul i o) m (ObservationTable i o) @-} makeClosed :: forall sul i o m. (FiniteOrd i, SUL sul m) =>@@ -264,37 +342,42 @@ makeClosed ot [] = return ot makeClosed ot inc = do sul <- ask- let- alph = Set.toList $ inputs sul+ let alph = inputs sul sm = prefixSetS ot em = suffixSetE ot tm = mappingT ot sm' = inc `Set.insert` sm- sm_I' = Set.fromList [w ++ [a] | w <- Set.toList sm', a <- alph]- outs <- lift $ forM (Set.toList em) (walk sul)- let mappings = [((inc ++ [s], e), last (snd o)) | s <- alph, (e, o) <- zip (Set.toList em) outs]- tm' = List.foldr (uncurry Map.insert) tm mappings+ sm_I' = Set.map (\(w, a) -> w ++ [a]) (sm' `Set.cartesianProduct` alph)+ newPrefixes = Set.map (\a -> inc ++ [a]) alph+ missing = newPrefixes `Set.cartesianProduct` em+ tm' <- lift $ updateMap tm missing sul return (ObservationTable{prefixSetS = sm', suffixSetE = em, mappingT = tm', prefixSetSI = sm_I'}) instance Learner LMstar MealyAutomaton StateID where initialize (LMstar _) = do- LMstar <$> initializeOT+ LMstar . Init <$> initializeOT initialize (LMplus _) = do- LMplus <$> initializeOT+ LMplus . Init <$> initializeOT - refine (LMstar ot) cex = do+ refine (LMstar (Init ot)) cex = do ot' <- otRefineAngluin ot cex- return (LMstar ot')- refine (LMplus ot) cex = do+ return (LMstar (Init ot'))+ refine (LMplus (Init ot)) cex = do ot' <- otRefinePlus ot cex- return (LMplus ot')+ return (LMplus (Init ot'))+ refine (LMstar Uninit) _ = initialize (LMstar Uninit)+ refine (LMplus Uninit) _ = initialize (LMplus Uninit) - learn (LMstar ot) = lmstar (LMstar ot)- learn (LMplus ot) = lmstar (LMplus ot)+ learn = lmstar {- | The 'otRefinePlus' function refines the observation table based on a counterexample, according to the LM+ algorithm, which is an improvement over Angluin's algorithm. -}++{-@ otRefinePlus :: (FiniteOrd i, SUL sul m) =>+ ObservationTable i o ->+ [i] ->+ ExperimentT (sul i o) m (ObservationTable i o) @-} otRefinePlus :: forall sul i o m. (FiniteOrd i, SUL sul m) =>@@ -314,26 +397,48 @@ suffixes = List.tails cex pairs = List.reverse $ List.zip prefixes suffixes wrapped = List.find (\x -> Set.member (fst x) sm || Set.member (fst x) sm_I) pairs- (_, suffix) = Maybe.fromMaybe (error "failed to update observation table") wrapped- -- the suffix is the distinguishing suffix. insert all suffixes expect from the empty one- newSuffixes = em `Set.difference` Set.fromList (init $ List.tails suffix)- em' = List.foldr Set.insert em newSuffixes- missing = (sm `Set.union` sm_I) `Set.cartesianProduct` newSuffixes- tm' <- lift $ updateMap tm missing sul- return (ObservationTable{prefixSetS = sm, suffixSetE = em', mappingT = tm', prefixSetSI = sm_I})+ case wrapped of+ Nothing -> return ot+ -- TODO: suffix triggers liquid haskell false+ Just (_, suffix) -> do+ let+ -- the suffix is the distinguishing suffix. insert all non-empty tails not already in E+ newSuffixes = Set.fromList (init $ List.tails suffix) `Set.difference` em+ em' = List.foldr Set.insert em newSuffixes+ missing = (sm `Set.union` sm_I) `Set.cartesianProduct` newSuffixes+ tm' <- lift $ updateMap tm missing sul+ return (ObservationTable{prefixSetS = sm, suffixSetE = em', mappingT = tm', prefixSetSI = sm_I}) +{-@ insertStep+ :: (Ord i, SUL sul m, Monad m)+ => sul i o+ -> Map.Map ([i],[i]) {v:[o] | len v > 0}+ -> ([i], {b:[i] | len b > 0})+ -> m (Map.Map ([i],[i]) {v:[o] | len v > 0}) @-}+insertStep ::+ (Ord i, SUL sul m, Monad m) =>+ sul i o ->+ Map.Map ([i], [i]) [o] ->+ ([i], [i]) ->+ m (Map.Map ([i], [i]) [o])+insertStep thesul acc (a, b) = do+ (_, outs) <- walk thesul (a ++ b)+ -- the table is prefix closed, so no need to store+ -- the whole length of outs, just the output that corresponds+ -- to the suffix+ pure (Map.insert (a, b) (dropLH outs (length a)) acc)++{-@ updateMap+ :: (Ord i, SUL sul m, Monad m)+ => Map.Map ([i],[i]) {v:[o] | len v > 0}+ -> Set.Set ([i], {v:[i] | len v > 0})+ -> sul i o+ -> m (Map.Map ([i],[i]) {v:[o] | len v > 0}) @-} updateMap :: (Ord i, SUL sul m, Monad m) =>- Map.Map ([i], [i]) o ->+ Map.Map ([i], [i]) [o] -> Set.Set ([i], [i]) -> sul i o ->- m (Map.Map ([i], [i]) o)+ m (Map.Map ([i], [i]) [o]) updateMap themap thestuff thesul =- foldM- ( \acc (a, b) -> do- (_, outs) <- walk thesul (a ++ b)- let o = last outs- pure (Map.insert (a, b) o acc)- )- themap- thestuff+ foldM (insertStep thesul) themap thestuff