Basic LStar in Haskell

mealy-decompose.cabal

@@ -27,6 +27,7 @@ library
   exposed-modules:
     DotParser,
     DotWriter,
+    LStar,
     Mealy,
     MealyRefine,
     Merger,

src/LStar.hs

@@ -0,0 +1,209 @@
+module LStar where
+
+-- LStar voor Mealy machines. Input zijn woorden van type i, en output zijn
+-- elementen van type o. (We gebruiken alleen de laatste output.)
+
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.State.Strict
+
+import Data.Foldable (minimumBy)
+import Data.Function (on)
+import Data.Functor.Identity
+import Data.List (tails)
+import Data.Map.Strict qualified as Map
+import Data.Map.Merge.Strict qualified as MapMerge
+import Data.Set qualified as Set
+import Prelude hiding (Word)
+
+-----------------------------------
+-- Datastructuren en basis functies
+
+-- Een woord is niets anders dan een lijst.
+-- TODO: Een keertje uitvogelen of Data.Sequence efficienter is of niet.
+type Word i = [i]
+
+-- Membership queries. Voor Mealy machines levert dat een o op. De parameter
+-- f is voor een monad. Dat is nodig als de membership queries echt moeten
+-- praten met een SUL, of als je bijv. een tellertje wilt bijhouden.
+type MQ f i o = Word i -> f o
+
+-- Invariant: dom(content) = `rows × columns` ∪ `rows × alph × columns`
+-- TODO: misschien hoeven we geen Set datastructuur te gebruiken, maar
+-- volstaan lijsten. Het zou ook met een Trie kunnen.
+data LStarState i o = LStarState
+  { content :: Map.Map (Word i) o
+  , rowIndices :: Set.Set (Word i)
+  , colIndices :: Set.Set (Word i)
+  , alphabet :: [i]
+  }
+  deriving (Eq, Ord, Show, Read)
+
+-- We maken onderscheid in "rij-index" en "rij". De index is het woord wat bij
+-- de rij hoort. De rij zelf is gegeven door de inhoud van de rij, dus een
+-- functie van kolom naar o. Dit doen we met een Map data structuur.
+type Row i o = Map.Map (Word i) o
+
+-- Kent aan een rij-index de rij (content) toe.
+row :: Ord i => LStarState i o -> Word i -> Row i o
+row LStarState{..} prefix = Map.fromSet (\suffix -> content Map.! (prefix <> suffix)) colIndices
+
+
+-----------------
+-- LStar functies
+
+-- Geeft alle rijen waarvoor de tabel nog niet gesloten is.
+-- TODO: toekenning van "lage rij" -> "hoge rij" ook uitrekenen, zodat we
+-- later meteen een automaat kunnen bouwen.
+closednessDefects :: (Ord i, Ord o) => LStarState i o -> [Word i]
+closednessDefects table@LStarState{..} = defects
+  where
+    alphabetSingletons = Set.fromList $ map pure alphabet
+    allExtendedRowIndices = Set.map (uncurry (<>)) $ Set.cartesianProduct rowIndices alphabetSingletons
+    extendedRowIndices = allExtendedRowIndices `Set.difference` rowIndices
+    upperRows = Set.map (row table) rowIndices
+    defects = [r | r <- Set.toList extendedRowIndices, row table r `Set.notMember` upperRows]
+
+-- Geeft alle paren van symbool en kolom (a, s) die toegevoegd moeten worden
+-- om de tabel consistent te maken. Merk op: het paar (a, s) zou vaker voor
+-- kunnen komen als er meerdere equivalente rijen zijn.
+inconsistencies :: (Ord i, Eq o) => LStarState i o -> [(i, Word i)]
+inconsistencies table@LStarState{..} = defects
+  where
+    equivalentPairs = [(r1, r2) | r1 <- Set.toList rowIndices, r2 <- Set.toList rowIndices, r1 < r2, row table r1 == row table r2]
+    defects = [(a, s) | (r1, r2) <- equivalentPairs, a <- alphabet, let d = differenceOfRows r1 r2 a, s <- Map.keys d]
+    differenceOfRows r1 r2 a = differenceOfMaps (row table (r1 <> [a])) (row table (r2 ++ [a]))
+    differenceOfMaps m1 m2 = MapMerge.merge MapMerge.dropMissing MapMerge.dropMissing (MapMerge.zipWithMaybeMatched (\_ x y -> if x == y then Nothing else Just ())) m1 m2
+
+-- Preconditie: tabel is gesloten en consistent
+-- TODO: misschien checken of de automaat uniek is? De constructie van
+-- transitions kiest de eerst-mogelijke successor-state, en misschien zijn
+-- er meer.
+createHypothesis :: (Ord i, Ord o) => LStarState i o -> (Int, Int, Map.Map (Int, i) Int, Map.Map (Int, i) o)
+createHypothesis table@LStarState{..} = (initialState, Map.size row2IntMap, transitions, outputs)
+  where
+    rowIndicesLs = Set.toList rowIndices
+    upperRows = map (row table) $ rowIndicesLs
+    row2IntMap = Map.fromList $ zip upperRows [0..]
+    row2Int = (Map.!) row2IntMap . row table
+    transitions = Map.fromList [((row2Int r, a), row2Int (r <> [a])) | r <- rowIndicesLs, a <- alphabet]
+    outputs = Map.fromList [((row2Int r, a), o) | r <- rowIndicesLs, a <- alphabet, let o = content Map.! (r <> [a])]
+    initialState = row2Int []
+
+
+-----------------------------------------
+-- Initialisatie en observaties toevoegen
+
+-- Een lege tabel heeft altijd een "epsilon-rij" en voor elk symbool een kolom.
+-- (Omdat het Mealy machines zijn.)
+initialiseA :: (Applicative f, Ord i) => [i] -> MQ f i o -> f (LStarState i o)
+initialiseA alphabet mq = initialiseWithA alphabet [[]] (map pure alphabet) mq
+
+-- We kunnen ook een tabel maken met voorgedefinieerde rijen en kolommen.
+initialiseWithA :: (Applicative f, Ord i) => [i] -> [Word i] -> [Word i] -> MQ f i o -> f (LStarState i o)
+initialiseWithA alphabet rowIdcs colIdcs mq = (\content -> LStarState{..}) <$> contentA
+  where
+    rowIndices = Set.fromList rowIdcs
+    rowIdcsExt = rowIndices <> Set.fromList [r <> [a] | r <- rowIdcs, a <- alphabet]
+    colIndices = Set.fromList colIdcs
+    domain = Map.fromSet (const ()) . Set.map (uncurry (<>)) $ Set.cartesianProduct rowIdcsExt colIndices
+    contentA = Map.traverseWithKey (\w _ -> mq w) domain
+
+-- preconditie: newRowIndices is disjunct van de huidige rowIndices en de
+-- vereniging is prefix-gesloten. (Wordt niet gechecked.)
+addRowsA :: (Applicative f, Ord i) => [Word i] -> MQ f i o -> LStarState i o -> f (LStarState i o)
+addRowsA newRowIndices mq table@LStarState{..} = (\newContent -> table
+  { content = content <> newContent
+  , rowIndices = rowIndices <> newRowIndicesSet }) <$> contentA
+  where
+    newRowIndicesExt = Set.fromList [r <> [a] | r <- newRowIndices, a <- alphabet]
+    newRowIndicesSet = Set.fromList newRowIndices
+    newRowIndices2 = (newRowIndicesSet <> newRowIndicesExt) `Set.difference` rowIndices
+    domain = Map.fromSet (const ()) . Set.map (uncurry (<>)) $ Set.cartesianProduct newRowIndices2 colIndices
+    contentA = Map.traverseWithKey (\w _ -> mq w) domain
+
+-- preconditie: zie addRows (?)
+addColumnsA :: (Applicative f, Ord i) => [Word i] -> MQ f i o -> LStarState i o -> f (LStarState i o)
+addColumnsA newColIndices mq table@LStarState{..} = (\newContent -> table
+  { content = content <> newContent
+  , colIndices = colIndices <> newColIndicesSet }) <$> contentA
+  where
+    newColIndicesExt = Set.fromList [[a] <> c | c <- newColIndices, a <- alphabet]
+    newColIndicesSet = Set.fromList newColIndices
+    newColIndices2 = (newColIndicesSet <> newColIndicesExt) `Set.difference` colIndices
+    domain = Map.fromSet (const ()) . Set.map (uncurry (<>)) $ Set.cartesianProduct rowIndices newColIndices2
+    contentA = Map.traverseWithKey (\w _ -> mq w) domain
+
+
+------------------
+-- LStar algoritme
+
+-- geeft True als de tabel is gewijzigd.
+closeA :: (Monad f, Ord i, Ord o) => MQ f i o -> LStarState i o -> f (LStarState i o, Bool)
+closeA mq = loop False where
+  loop acc table = case closednessDefects table of
+    [] -> pure (table, acc)
+    w:_ -> addRowsA [w] mq table >>= loop True
+
+-- geeft True als de tabel is gewijzigd.
+makeConsistentA :: (Monad f, Ord i, Eq o) => MQ f i o -> LStarState i o -> f (LStarState i o, Bool)
+makeConsistentA mq = loop False where
+  loop acc table = case inconsistencies table of
+    [] -> pure (table, acc)
+    (a, w):_ -> addColumnsA [a:w] mq table >>= loop True
+
+makeClosedAndConsistentA :: (Monad f, Ord i, Ord o) => MQ f i o -> LStarState i o -> f (LStarState i o, Bool)
+makeClosedAndConsistentA mq = loop False where
+  loop acc table1 = do
+    (table2, b2) <- closeA mq table1
+    (table3, b3) <- makeConsistentA mq table2
+    if b3
+    then loop True table3
+    else pure (table3, acc || b2)
+
+-- We voegen tegenvoorbeelden toe als kolommen. Dat is vaak het meest
+-- efficient. We houden de kolommen wel suffix-gesloten, dat is iets
+-- eenvoudiger.
+processCounterexampleA :: (Applicative f, Ord i) => Word i -> MQ f i o -> LStarState i o -> f (LStarState i o)
+processCounterexampleA ce mq table@LStarState{..} = addColumnsA newSuffixes mq table where
+  removePrefix [] w2 = Just w2
+  removePrefix _ [] = Nothing
+  removePrefix (a:w1) (b:w2)
+    | a == b = removePrefix w1 w2
+    | otherwise = Nothing
+  shortestSuffix = minimumBy (compare `on` length) [suf | r <- Set.toList rowIndices, Just suf <- [removePrefix r ce]]
+  newSuffixes = filter (not . null) . tails . drop 1 $ shortestSuffix
+
+
+-------------
+-- MQ wrapper
+
+-- Bijhouden hoeveel membership queries er zijn gesteld
+countingMQ :: Monad f => MQ f i o -> MQ (StateT Int f) i o
+countingMQ mq w = modify' succ >> lift (mq w)
+
+
+-----------------------
+-- Minder generieke API
+
+-- Als je geen monad nodig hebt, kun je een simpele membership query omzetten
+-- naar het MQ type.
+simpleMQ :: (Word i -> o) -> MQ Identity i o
+simpleMQ = (.) Identity
+
+initialise :: Ord i => [i] -> (Word i -> o) -> LStarState i o
+initialise alphabet = runIdentity . initialiseA alphabet . simpleMQ
+
+initialiseWith :: Ord i => [i] -> [Word i] -> [Word i] -> (Word i -> o) -> LStarState i o
+initialiseWith alphabet rowIdcs colIdcs = runIdentity . initialiseWithA alphabet rowIdcs colIdcs . simpleMQ
+
+addRows, addColumns :: Ord i => [Word i] -> (Word i -> o) -> LStarState i o -> LStarState i o
+addRows newRowIndices mq = runIdentity . addRowsA newRowIndices (simpleMQ mq)
+addColumns newColIndices mq = runIdentity . addColumnsA newColIndices (simpleMQ mq)
+
+close, makeConsistent, makeClosedAndConsistent :: (Ord i, Ord o) => (Word i -> o) -> LStarState i o -> (LStarState i o, Bool)
+close mq = runIdentity . closeA (simpleMQ mq)
+makeConsistent mq = runIdentity . makeConsistentA (simpleMQ mq)
+makeClosedAndConsistent mq = runIdentity . makeClosedAndConsistentA (simpleMQ mq)
+
+processCounterexample :: Ord i => Word i -> (Word i -> o) -> LStarState i o -> LStarState i o
+processCounterexample ce mq = runIdentity . processCounterexampleA ce (simpleMQ mq)