Restructures Main and also implemented input decomposition

app/Main.hs

@@ -1,4 +1,6 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
 
 module Main where
 
@@ -10,6 +12,7 @@ import Mealy
 import MealyRefine
 import Merger
 
+import Control.Monad (when)
 import Data.Bifunctor
 import Data.List (sortOn)
 import Data.List.Ordered (nubSort)
@@ -20,109 +23,77 @@ import Data.Text qualified as T
 import Data.Text.IO qualified as T
 import Data.Text.Lazy.IO qualified as TL
 import Data.Tuple (swap)
-import Debug.Trace (traceMarkerIO)
 import System.Environment
 
--- | This functions inverts a map. In the new map the values are lists.
+extraChecks :: Bool
-converseRelation :: Ord b => Map.Map a b -> Map.Map b [a]
+extraChecks = False
-converseRelation = Map.fromListWith (++) . fmap (second pure . swap) . Map.assocs
 
 main :: IO ()
 main = do
-  -- Read dot file
+  -- READING INPUT
+  ----------------
   ls <- getArgs
   let dotFile = case ls of
         [x] -> x
         _ -> error "Please provide exactly one argument (filepath of dot file)"
 
-  traceMarkerIO "read input"
+  putStrLn $ "reading " <> dotFile
-
-  putStr "reading " >> putStrLn dotFile
   machine <- readDotFile dotFile
 
-  -- print some basic info
+  -- PREPROCESSING
-  putStrLn $ (show . length $ states machine) <> " states, " <> (show . length $ inputs machine) <> " inputs and " <> (show . length $ outputs machine) <> " outputs"
+  ----------------
+  let (outputFuns, reverseFuns) = preprocess machine
+  printBasics outputFuns reverseFuns machine
 
-  traceMarkerIO "start minimisation"
+  -- MINIMISING EACH COMPONENT
+  ----------------------------
+  let mappedOutputFuns o = [(i, (o ==) . f) | (i, f) <- outputFuns]
+      projections = [(o, refineFuns (mappedOutputFuns o) reverseFuns (states machine)) | o <- (outputs machine)]
 
-  let
+  putStrLn $ "\nComponents " <> show (length (outputs machine))
-    printPartition p = putStrLn $ "number of states = " <> show (numBlocks p)
+  mapM_ (\(o, p) -> putStr "  " >> T.putStr o >> putStr " has size " >> print (numBlocks p)) projections
 
-  let
+  -- REDUCING NUMBER OF COMPONENTS
-    outputFuns = [(i, fun) | i <- inputs machine, let fun s = fst (behaviour machine s i)]
+  -- by checking which partitions are equivalent
-    reverseTransitionMaps i = Map.fromListWith (++) [(t, [s]) | s <- states machine, let t = snd (behaviour machine s i)]
+  ----------------------------------------------
-    reverseFuns = [(i, fun) | i <- inputs machine, let mm = reverseTransitionMaps i, let fun s = Map.findWithDefault [] s mm]
+  let (equiv, uniqPartitions) = equivalenceClasses comparePartitions projections
 
-  -- Minimise input, so we know the actual number of states
+  putStrLn $ "\nRepresentatives " <> show (length uniqPartitions)
-  printPartition (refineFuns outputFuns reverseFuns (states machine))
-  putStrLn ""
-
-  traceMarkerIO "start minimisation for each component"
-
-  -- Then compute each projection
-  let
-    outs = outputs machine
-    mappedOutputFuns o = [(i, (o ==) . f) | (i, f) <- outputFuns]
-    projections = [(o, refineFuns (mappedOutputFuns o) reverseFuns (states machine)) | o <- outs]
-
-  -- Print number of states of each projection
-  mapM_
-    ( \(o, partition) -> do
-        T.putStr o
-        putStr " -> "
-        printPartition partition
-    )
-    projections
-
-  traceMarkerIO "component equivalences"
-
-  -- First we check for equivalent partitions, so that we skip redundant work.
-  let
-    (equiv, uniqPartitions) = equivalenceClasses comparePartitions projections
-
-  putStrLn ""
-  putStrLn "Representatives"
   print . fmap fst $ uniqPartitions
 
-  putStrLn ""
+  -- putStrLn "\nEquivalences"
-  putStrLn "Equivalences"
+  -- mapM_ (\(o2, o1) -> putStrLn $ "  " <> show o2 <> " == " <> show o1) (Map.assocs equiv)
-  mapM_
-    ( \(o2, o1) -> do
-        putStrLn $ "  " <> show o2 <> " == " <> show o1
-    )
-    (Map.assocs equiv)
-
-  traceMarkerIO "component lattice"
 
+  -- COMPUTING THE LATTICE OF COMPONENTS
   -- Then we compare each pair of partitions. We only keep the finest
   -- partitions, since the coarse ones don't provide value to us.
+  -------------------------------------------------------------------
   let
     (topMods, downSets) = maximalElements comparePartitions uniqPartitions
     foo (a, b) = (numBlocks b, a)
+    sortedTopMods = (sortOn (negate . fst) . fmap foo $ topMods)
 
-  putStrLn ""
+  putStrLn $ "\nTop modules " <> show (length topMods)
-  putStrLn "Top modules"
+  mapM_ (\(b, o) -> putStr "  " >> T.putStr o >> putStr " has size " >> print b) sortedTopMods
-  mapM_
-    ( \(b, o) -> do
-        putStrLn $ "  " <> show o <> " has size " <> show b
-    )
-    (sortOn (negate . fst) . fmap foo $ topMods)
-
-  traceMarkerIO "heuristic merger"
 
+  -- HEURISTIC MERGING
   -- Then we try to combine paritions, so that we don't end up with
   -- too many components. (Which would be too big to be useful.)
+  -----------------------------------------------------------------
   let strategy MergerStats{..}
         | numberOfComponents <= 4 = Stop
         | otherwise = Continue
 
+  putStrLn $ "\nHeuristic merging"
   projmap <- heuristicMerger topMods strategy
 
-  print projmap
+  putStrLn $ "\nDone"
+  putStrLn $ "  components: " <> show (length projmap)
+  putStrLn $ "  sizes: " <> show (fmap (numBlocks . snd) projmap)
+  putStrLn "Start writing output files"
 
-  traceMarkerIO "output"
+  -- OUTPUT
-
+  ---------
-  -- Now we are going to output the components we found.
   let
     equivInv = converseRelation equiv
     projmapN = zip projmap [1 :: Int ..]
@@ -136,9 +107,8 @@ main = do
         -- Sanity check: compute partition again
         partition = refineMealy proj
 
-      putStrLn ""
+      putStrLn $ "\nComponent " <> show os
-      putStrLn $ "Component " <> show os
+      when extraChecks (putStrLn $ "  Correct? " <> show (comparePartitions p partition))
-      putStrLn $ "Correct? " <> show (comparePartitions p partition)
       putStrLn $ "  Size = " <> show (numBlocks p)
 
       do
@@ -187,3 +157,29 @@ main = do
         TL.writeFile ("results/" <> filename2) content2
 
   mapM_ action projmapN
+
+-- * Helper functions
+
+-- | Computes the predecessors of each state.
+preprocess :: _ => MealyMachine _ _ _ -> _
+preprocess MealyMachine{..} = (outputFuns, reverseFuns)
+ where
+  outputFuns = [(i, fun) | i <- inputs, let fun s = fst (behaviour s i)]
+  reverseTransitionMaps i = Map.fromListWith (++) [(t, [s]) | s <- states, let t = snd (behaviour s i)]
+  reverseFuns = [(i, fun) | i <- inputs, let mm = reverseTransitionMaps i, let fun s = Map.findWithDefault [] s mm]
+
+-- | Prints basic info.
+printBasics :: _ => _ -> _ -> MealyMachine _ _ _ -> IO _
+printBasics outputFuns reverseFuns MealyMachine{..} = do
+  putStrLn $ (show . length $ states) <> " states, " <> (show . length $ inputs) <> " inputs and " <> (show . length $ outputs) <> " outputs"
+  when extraChecks $ do
+    printPartition (refineFuns outputFuns reverseFuns states)
+    putStrLn ""
+
+-- | This functions inverts a map. In the new map the values are lists.
+converseRelation :: Ord b => Map.Map a b -> Map.Map b [a]
+converseRelation = Map.fromListWith (++) . fmap (second pure . swap) . Map.assocs
+
+-- | Prints the number of blocks.
+printPartition :: Partition s -> IO ()
+printPartition p = putStrLn $ "number of states = " <> show (numBlocks p)

app/Playground.hs

@@ -1,10 +1,12 @@
 module Main where
 
 import Bisimulation (bisimulation2)
+import Data.Partition (Block (..), numBlocks)
 import Data.Trie qualified as Trie
-import Data.UnionFind
+import Data.UnionFind (empty, equate, equivalent)
 import DotParser (readDotFile)
 import Mealy (MealyMachine (..), outputFunction, transitionFunction)
+import MealyRefine (refineMealy)
 import SplittingTree (initialPRState, refine)
 import StateIdentifiers (stateIdentifierFor)
 
@@ -14,6 +16,7 @@ import Data.Map.Strict qualified as Map
 import Data.Maybe (isJust)
 import Data.Set qualified as Set
 import System.Environment (getArgs)
+import System.Exit (exitFailure, exitSuccess)
 
 main :: IO ()
 main = do
@@ -58,33 +61,37 @@ mainHSI args = case args of
 
 -- Interleaving composition of restriction to subalphabets
 -- precondigiotn: alph1 and alph2 have no common elements
-interleavingComposition :: Ord i => [i] -> [i] -> MealyMachine s i o -> MealyMachine (s, s) i o
+interleavingComposition :: Ord i => [[i]] -> MealyMachine s i o -> MealyMachine [s] i o
-interleavingComposition alph1 alph2 m =
+interleavingComposition alphs m =
   MealyMachine
     { states = error "states should not be necessary"
-    , inputs = alph1 ++ alph2
+    , inputs = concat alphs
-    , outputs = error "outputs should not be necessary"
+    , outputs = outputs m -- or some subset?
-    , behaviour = \(s1, s2) i ->
+    , behaviour = \ss i ->
         case Map.lookup i alphLookup of
-          Just False -> let (o, t) = behaviour m s1 i in (o, (t, s2))
+          Just idx ->
-          Just True -> let (o, t) = behaviour m s2 i in (o, (s1, t))
+            let (o, t) = behaviour m (ss !! idx) i
+                (p, _ : s) = splitAt idx ss
+             in (o, p ++ [t] ++ s)
           Nothing -> error "symbol not in either alphabet"
-    , initialState = (initialState m, initialState m)
+    , initialState = replicate (length alphs) (initialState m)
     }
  where
-  alphLookup = Map.fromList ([(a, False) | a <- alph1] ++ [(a, True) | a <- alph2])
+  alphLookup = Map.fromList [(i, idx) | (alph, idx) <- zip alphs [0 ..], i <- alph]
 
 mainInputDecomp :: [String] -> IO ()
 mainInputDecomp args = case args of
-  [dotFile] -> run dotFile
+  [dotFile] -> putStrLn ("reading " <> dotFile) >> run dotFile
   _ -> putStrLn "Please provide a dot file"
  where
   run dotFile = do
-    print dotFile
     model <- readDotFile dotFile
+    putStr $ "states: " <> show (length (states model)) <> "; "
+    putStr $ "inputs: " <> show (length (inputs model)) <> "; "
+    putStr $ " outputs: " <> show (length (outputs model)) <> "\n"
 
     let
-      composition i j = interleavingComposition [i] [j] model
+      composition i j = interleavingComposition [[i], [j]] model
       bisim i j =
         let compo = composition i j
          in bisimulation2
@@ -98,28 +105,59 @@ mainInputDecomp args = case args of
       dependent i j = isJust $ bisim i j
       dependentPairs = [(i, j) | i <- inputs model, j <- inputs model, j > i, dependent i j]
 
-    print $ length (states model)
+    -- The relation dependentPairs is typically not transitive.
-    print $ length (inputs model)
-    print $ length (outputs model)
-
-    putStrLn "Dependent pairs:"
-    print $ length dependentPairs
-
-    let dps = Set.fromList dependentPairs
-        dpsFun i j = i == j || (i, j) `Set.member` dps || (j, i) `Set.member` dps
-        trans =
-          null [(i, j, k) | i <- inputs model, j <- inputs model, dpsFun i j, k <- inputs model, dpsFun j k, not (dpsFun i k)]
-
-    putStrLn "Transitive?"
-    print trans
-
     let closure = foldr (uncurry equate) empty dependentPairs
-        step [] = Nothing
+        step _ [] = Nothing
-        step ls@(i : _) = Just (List.partition (\j -> equivalent i j closure) ls)
+        step clos ls@(i : _) = Just (List.partition (\j -> equivalent i j clos) ls)
-        classes = List.unfoldr step (inputs model)
+        classes = List.unfoldr (step closure) (inputs model)
 
-    mapM_ print classes
     case length classes of
-      0 -> putStrLn "ERROR"
+      0 -> putStrLn "ERROR" >> exitFailure
-      1 -> putStrLn "INDECOMPOSABLE"
+      1 -> putStrLn "INDECOMPOSABLE" >> exitSuccess
       n -> putStrLn ("MAYBE DECOMPOSABLE: " ++ show n ++ " classes")
+
+    let
+      loop currentClosure currentClasses = do
+        let
+          bigCompo = interleavingComposition currentClasses model
+          result = bisimulation2 (inputs model) (outputFunction model) (transitionFunction model) (initialState model) (outputFunction bigCompo) (transitionFunction bigCompo) (initialState bigCompo)
+
+        -- print currentClasses
+        print result
+
+        case result of
+          Nothing -> return currentClasses
+          Just cex -> do
+            let
+              -- The counterexample is always the shortest. I am not completely
+              -- confident that all pairs should be then consideren dependent.
+              newDependentPairs = zip cex (tail cex)
+              newClosure = foldr (uncurry equate) currentClosure newDependentPairs
+              newClasses = List.unfoldr (step newClosure) (inputs model)
+            loop newClosure newClasses
+
+    finalClasses <- loop closure classes
+
+    let
+      reachability initial next = go [initial] Set.empty
+       where
+        go [] visited = visited
+        go (s : todo) visited
+          | Set.member s visited = go todo visited
+          | otherwise = go (todo ++ next s) (Set.insert s visited)
+      minimiseComponent cls =
+        let
+          reachableStates = reachability (initialState model) (\s -> [snd (behaviour model s i) | i <- cls])
+          machine = MealyMachine{states = Set.toList reachableStates, inputs = cls, outputs = outputs model, behaviour = behaviour model, initialState = initialState model}
+          partition = refineMealy machine
+         in
+          partition
+      action cls = do
+        let (Block p) = numBlocks . minimiseComponent $ cls
+        putStr (show cls) >> putStr " of size " >> putStrLn (show p)
+        return (p, p * length cls)
+
+    putStrLn $ "Final classes " <> show (length finalClasses)
+    (stateSizes, transitionSizes) <- unzip <$> mapM action finalClasses
+    putStrLn $ "Total size = " <> show (sum stateSizes)
+    putStrLn $ "Total transitions = " <> show (sum transitionSizes)