Kleine optimalisaties en bisimulatie uitrekenen voor EQOracle

app/LStarMain.hs

@@ -1,5 +1,6 @@
 module Main where
 
+import Bisimulation (bisimulation2)
 import DotParser
 import LStar
 import Mealy
@@ -7,11 +8,12 @@ import Mealy
 import Control.Monad (when)
 import Control.Monad.Trans.Class
 import Control.Monad.Trans.State.Strict
-import System.Environment
-import System.IO
+import Data.Map.Strict qualified as Map
 import Data.Maybe (mapMaybe)
+import System.Environment
 import Text.Megaparsec
 
+
 debugOutput :: Bool
 debugOutput = False
 
@@ -28,33 +30,39 @@ main = do
   transitions <- mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile
 
   let machine = convertToMealy transitions
+      alphabet = inputs machine
+      tInit = initialState machine
+      tOut s i = fst (behaviour machine s i)
+      tTrans s i = snd (behaviour machine s i)
+
       mq0 = semanticsForState machine (initialState machine)
       mq = countingMQ (\w -> when debugOutput (print w) >> return (mq0 w))
 
   let loop table = do
         lift $ putStrLn "Making the table closed and consistent"
         (table2, b) <- makeClosedAndConsistentA mq table
-        let (_, size, _, _) = createHypothesis table2
+        let (hInit, size, hTransMap, hOutMap) = createHypothesis table2
+            hTrans s i = hTransMap Map.! (s, i)
+            hOut s i = hOutMap Map.! (s, i)
+            res = bisimulation2 alphabet tOut tTrans tInit hOut hTrans hInit
 
-        inp <- lift $ do
-          putStrLn (if b then "Table changed" else "Table did not changed")
-          putStrLn (show size <> " states")
-          putStr "> "
-          hFlush stdout
-          getLine
+        lift $ putStrLn (if b then "Table changed" else "Table did not changed")
+        lift $ putStrLn (show size <> " states")
 
-        if inp == ""
-          then return size
-          else do
-            let cex = read inp
+        case res of
+          Nothing -> do
+            lift $ putStrLn "Done learning!"
+            return size
+          Just cex -> do
+            lift $ putStrLn "CEX:" >> print cex
             table3 <- processCounterexampleA cex mq table2
             loop table3
 
       learner = do
-        table <- initialiseA (inputs machine) mq
+        table <- initialiseA alphabet mq
         loop table
 
   (a, b) <- runStateT learner 0
 
-  print a
-  putStrLn $ "MQs: " <> show b
+  putStrLn $ "Size: " <> show a
+  putStrLn $ "MQs:  " <> show b

mealy-decompose.cabal

@@ -24,6 +24,7 @@ library
   import: stuff
   hs-source-dirs: src
   exposed-modules:
+    Bisimulation,
     DotParser,
     DotWriter,
     LStar,

src/Bisimulation.hs

@@ -0,0 +1,58 @@
+module Bisimulation where
+
+import Data.List (find)
+import Data.Map.Strict qualified as Map
+import Data.Sequence qualified as Seq
+
+
+-- Dit is niet de echte union-find datastructuur (niet efficient),
+-- maar wel erg simpel en beter dan niks.
+newtype UnionFind x = MkUnionFind { unUnionFind :: Map.Map x x }
+
+empty :: UnionFind x
+empty = MkUnionFind Map.empty
+
+root :: Ord x => x -> UnionFind x -> x
+root x uf = case Map.lookup x . unUnionFind $ uf of
+  Nothing -> x
+  Just y -> root y uf
+
+equivalent :: Ord x => x -> x -> UnionFind x -> Bool
+equivalent x y uf = root x uf == root y uf
+
+-- Ik zou eigenlijk naar de grootte van de boompjes moeten kijken
+equate :: Ord x => x -> x -> UnionFind x -> UnionFind x
+equate x y uf =
+  let rx = root x uf
+      ry = root y uf
+  in case rx == ry of
+    True -> uf
+    False -> MkUnionFind . Map.insert rx ry . unUnionFind $ uf
+
+
+-- Bisimulatie in 1 machine
+bisimulation :: (Eq o, Ord s) => [i] -> (s -> i -> o) -> (s -> i -> s) -> s -> s -> Maybe [i]
+bisimulation alphabet output transition x y = go (Seq.singleton ([], x, y)) empty
+  where
+    go Seq.Empty _ = Nothing
+    go ((rpath, a, b) Seq.:<| queue) !visited
+      -- Skip the equal nodes
+      | a == b = go queue visited
+      -- Skip nodes deemed equivalent
+      | equivalent a b visited = go queue visited
+      -- Of not visited, check output and add successors to queue
+      | otherwise =
+        case find (\i -> output a i /= output b i) alphabet of
+          -- Found an input which leads to different outputs => return difference
+          Just i -> Just (reverse (i : rpath))
+          -- Else, we continue the search
+          Nothing ->
+            let succesors = Seq.fromList $ fmap (\i -> (i:rpath, transition a i, transition b i)) alphabet
+            in go (queue <> succesors) (equate a b visited)
+
+-- Bisimulatie in verschillende machines
+bisimulation2 :: (Eq o, Ord s, Ord t) => [i] -> (s -> i -> o) -> (s -> i -> s) -> s -> (t -> i -> o) -> (t -> i -> t) -> t -> Maybe [i]
+bisimulation2 alphabet output1 transition1 x output2 transition2 y = bisimulation alphabet (either output1 output2) transition (Left x) (Right y)
+  where
+    transition (Left s) i = Left (transition1 s i)
+    transition (Right t) i = Right (transition2 t i)

src/LStar.hs

@@ -5,7 +5,6 @@ module LStar where
 
 import Control.Monad.Trans.Class
 import Control.Monad.Trans.State.Strict
-
 import Data.Foldable (minimumBy)
 import Data.Functor.Identity
 import Data.List (tails, stripPrefix)
@@ -15,12 +14,15 @@ import Data.Ord (comparing)
 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.
+-- Een woord is niets anders dan een lijst. Ik heb geprobeerd of Data.Sequence
+-- sneller is, maar dat lijkt niet zo te zijn. Dus het blijft [i] voor gemak.
 type Word i = [i]
+cons = (:)
+snoc w a = w <> [a]
 
 -- 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
@@ -53,15 +55,14 @@ row LStarState{..} prefix = Map.fromSet (\suffix -> content Map.! (prefix <> suf
 
 -- 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.
+-- later meteen een automaat kunnen bouwen. Dit zorgt ook voor minder werk
+-- als we opnieuw closedness moeten uitrekenen.
 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
+    extendedRowIndices = [ra | r <- Set.toList rowIndices, a <- alphabet, let ra = r `snoc` a, ra `Set.notMember` rowIndices]
     upperRows = Set.map (row table) rowIndices
-    defects = [r | r <- Set.toList extendedRowIndices, row table r `Set.notMember` upperRows]
+    defects = [r | r <- 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
@@ -71,7 +72,7 @@ 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]))
+    differenceOfRows r1 r2 a = differenceOfMaps (row table (r1 `snoc` a)) (row table (r2 `snoc` 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
@@ -85,9 +86,9 @@ createHypothesis table@LStarState{..} = (initialState, Map.size row2IntMap, tran
     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 []
+    transitions = Map.fromList [((row2Int r, a), row2Int (r `snoc` a)) | r <- rowIndicesLs, a <- alphabet]
+    outputs = Map.fromList [((row2Int r, a), o) | r <- rowIndicesLs, a <- alphabet, let o = content Map.! (r `snoc` a)]
+    initialState = row2Int mempty
 
 
 -----------------------------------------
@@ -96,14 +97,14 @@ createHypothesis table@LStarState{..} = (initialState, Map.size row2IntMap, tran
 -- 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
+initialiseA alphabet mq = initialiseWithA alphabet [mempty] (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]
+    rowIdcsExt = rowIndices <> Set.fromList [r `snoc` 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
@@ -115,7 +116,7 @@ addRowsA newRowIndices mq table@LStarState{..} = (\newContent -> table
   { content = content <> newContent
   , rowIndices = rowIndices <> newRowIndicesSet }) <$> contentA
   where
-    newRowIndicesExt = Set.fromList [r <> [a] | r <- newRowIndices, a <- alphabet]
+    newRowIndicesExt = Set.fromList [r `snoc` 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
@@ -127,7 +128,7 @@ addColumnsA newColIndices mq table@LStarState{..} = (\newContent -> table
   { content = content <> newContent
   , colIndices = colIndices <> newColIndicesSet }) <$> contentA
   where
-    newColIndicesExt = Set.fromList [[a] <> c | c <- newColIndices, a <- alphabet]
+    newColIndicesExt = Set.fromList [a `cons` 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
@@ -149,7 +150,7 @@ makeConsistentA :: (Monad f, Ord i, Eq o) => MQ f i o -> LStarState i o -> f (LS
 makeConsistentA mq = loop False where
   loop acc table = case inconsistencies table of
     [] -> pure (table, acc)
-    (a, w):_ -> addColumnsA [a:w] mq table >>= loop True
+    (a, w):_ -> addColumnsA [a `cons` 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