Moved some bits around

app/Main.hs

@@ -2,21 +2,17 @@ module Main where
 
 import DotParser
 import Mealy
-import MyLib
+import MealyRefine
 
-import Control.Monad.IO.Class (liftIO)
+-- import Control.Monad.IO.Class (liftIO)
-import Control.Monad.Trans.State.Strict
+-- import Control.Monad.Trans.State.Strict
-import Control.Monad (forM_, when)
+import Control.Monad (forM_)
-import Control.Monad.ST (runST)
+-- import Data.Map.Strict qualified as Map
-import Copar.Algorithm (refine)
-import Copar.Functors.Polynomial (Polynomial)
-import Data.Map.Strict qualified as Map
 import Data.Maybe (mapMaybe)
 import Data.Partition (isRefinementOf, numBlocks)
-import Data.Proxy (Proxy(..))
+-- import Data.Semigroup (Arg(..))
-import Data.Semigroup (Arg(..))
+-- import Data.Set qualified as Set
-import Data.Set qualified as Set
+-- import Data.List.Ordered (nubSort)
-import Data.List.Ordered (nubSort)
 import System.Environment
 import Text.Megaparsec
 
@@ -44,7 +40,6 @@ main = do
   print . take 4 . states $ machine
   print . take 4 . inputs $ machine
   print . take 4 . outputs $ machine
-  putStrLn ""
 
   -- DEBUG OUTPUT
   -- forM_ (states machine) (\s -> do
@@ -56,39 +51,40 @@ main = do
   --     )
   --   )
 
-  let printPartition p = putStrLn $ "  number of states = " <> show (numBlocks p)
+  let printPartition p = putStrLn $ "number of states = " <> show (numBlocks p)
 
   -- Minimise input, so we know the actual number of states
-  printPartition (runST $ refine (Proxy @Polynomial) (mealyMachineToEncoding machine) True)
+  printPartition (refineMealy (mealyMachineToEncoding machine))
   putStrLn ""
 
   -- Then compute each projection
-  let minimiseProjection o = runST $ refine (Proxy @Polynomial) (mealyMachineToEncoding (project machine o)) True
+  -- I did some manual preprocessing, these are the only interesting bits
-      outs = outputs machine
+  let outs = ["10", "10-O9", "2.2", "3.0", "3.1", "3.10", "3.12", "3.13", "3.14", "3.16", "3.17", "3.18", "3.19", "3.2", "3.20", "3.21", "3.3", "3.4", "3.6", "3.7", "3.8", "3.9", "5.0", "5.1", "5.12", "5.13", "5.17", "5.2", "5.21", "5.23", "5.6", "5.7", "5.8", "5.9", "quiescence"]
-      projections = Map.fromSet minimiseProjection (Set.fromList outs)
+      -- outs = outputs machine
+      projections0 = allProjections machine outs
+      projections = zip outs $ fmap refineMealy projections0
 
   -- Print number of states of each projection
-  forM_ (Map.assocs projections) (\(o, partition) -> do
+  forM_ projections (\(o, partition) -> do
-    print o
+    putStr $ o <> " -> "
     printPartition partition
-    putStrLn ""
     )
 
-  -- Consider all pairs
+  {-
-  let keys = Map.argSet projections
-      pairs = Set.cartesianProduct keys keys
-      distinctPairs = Set.filter (\(Arg o1 _, Arg o2 _) -> o1 < o2) pairs -- bit inefficient
 
   -- Check refinement relations for all pairs
+  -- This is a bit messy, it skips machines which are equivalent
+  -- to earlier checked machines, so we thread some state through this
+  -- computation. (And I also want some IO for debugging purposes.)
   (equiv, rel) <- flip execStateT (Map.empty, []) $ do
-    forM_ (Map.assocs projections) (\(o1, b1) -> do
+    forM_ projections (\(o1, b1) -> do
       (repr, _) <- get
       if o1 `Map.member` repr
         then do
           liftIO . putStrLn $ "skip " <> (show o1) <> " |-> " <> (show (repr Map.! o1))
         else do
           liftIO $ print o1
-          forM_ (Map.assocs projections) (\(o2, b2) -> do
+          forM_ projections (\(o2, b2) -> do
             (repr0, _) <- get
             when (o1 < o2 && o2 `Map.notMember` repr0) $ do
               case (isRefinementOf b1 b2, isRefinementOf b2 b1) of
@@ -122,3 +118,5 @@ main = do
     )
 
   return ()
+
+  -}

mealy-decompose.cabal

@@ -24,10 +24,9 @@ library
   import: stuff
   hs-source-dirs: src
   exposed-modules:
-    MyLib,
+    DotParser,
     Mealy,
-    DotParser
+    MealyRefine
-  -- other-modules:
   build-depends:
     vector
 

src/MealyRefine.hs

@@ -0,0 +1,84 @@
+module MealyRefine where
+
+import Mealy
+
+import Control.Monad.ST (runST)
+import Copar.Algorithm (refine)
+import Copar.Functors.Polynomial (Polynomial, PolyF1(..))
+import Copar.RefinementInterface (Label, F1)
+import Data.Bool (bool)
+import Data.CoalgebraEncoding (Encoding(..))
+import Data.Map.Strict qualified as Map
+import Data.Partition (Partition)
+import Data.Proxy (Proxy(..))
+import Data.Vector qualified
+import Data.Vector.Unboxed qualified
+
+project :: Eq o => MealyMachine s i o -> o -> MealyMachine s i Bool
+project MealyMachine{..} o = MealyMachine
+  { outputs = [False, True]
+  , behaviour = \s i -> case behaviour s i of
+      (out, s2) -> (out == o, s2)
+  , ..
+  }
+
+-- We will project to all (relevant) outputs. Since a lot of data is shared
+-- among those mealy machines, I do this in one function. The static parts
+-- are converted only once. Only "eStructure" (the state-labels) are different
+-- for each projection.
+allProjections :: (Ord s, Ord i, Eq o) => MealyMachine s i o -> [o] -> [Encoding (Label Polynomial) (F1 Polynomial)]
+allProjections MealyMachine{..} outs = fmap mkEncoding outs
+  where
+    numStates = length states
+    numInputs = length inputs
+    idx2state = Map.fromList $ zip [0..] states
+    state2idx = Map.fromList $ zip states [0..]
+    idx2input = Map.fromList $ zip [0..] inputs
+    stateInputIndex n = n `divMod` numInputs -- inverse of \(s, i) -> s * numInputs + i
+    edgesFrom = Data.Vector.Unboxed.generate (numStates * numInputs) (fst . stateInputIndex)
+    edgesLabel = Data.Vector.generate (numStates * numInputs) (snd . stateInputIndex)
+    edgesTo = Data.Vector.Unboxed.generate (numStates * numInputs) ((state2idx Map.!) . snd . (\(s, i) -> behaviour (idx2state Map.! s) (idx2input Map.! i)) . stateInputIndex)
+    bool2Int = bool 0 1
+    structure o = Data.Vector.generate numStates
+      (\s -> PolyF1
+        { polyF1Summand = 0 -- There is only one summand
+        , polyF1Variables = numInputs -- This many transitions per state
+        , polyF1Constants = Data.Vector.Unboxed.generate numInputs
+          (\i -> bool2Int . (o==) . fst $ (behaviour (idx2state Map.! s) (idx2input Map.! i)))
+        }
+      )
+    mkEncoding o = Encoding
+      { eStructure = structure o
+      , eInitState = Nothing
+      , eEdgesFrom = edgesFrom
+      , eEdgesLabel = edgesLabel
+      , eEdgesTo = edgesTo
+      }
+
+-- Refine a encoded mealy machine
+refineMealy :: Encoding (Label Polynomial) (F1 Polynomial) -> Partition
+refineMealy machine = runST $ refine (Proxy @Polynomial) machine True
+
+mealyMachineToEncoding :: (Ord s, Ord i, Ord o) => MealyMachine s i o -> Encoding (Label Polynomial) (F1 Polynomial)
+mealyMachineToEncoding MealyMachine{..} =
+  let numStates = length states
+      numInputs = length inputs
+      idx2state = Map.fromList $ zip [0..] states
+      idx2input = Map.fromList $ zip [0..] inputs
+      out2idx = Map.fromList $ zip outputs [0..]
+      eStructure = Data.Vector.generate numStates
+        (\s -> PolyF1
+          { polyF1Summand = 0 -- There is only one summand
+          , polyF1Variables = numInputs -- This many transitions per state
+          , polyF1Constants = Data.Vector.Unboxed.generate numInputs
+            (\i -> out2idx Map.! (fst (behaviour (idx2state Map.! s) (idx2input Map.! i))))
+          }
+        )
+      eInitState = Nothing
+      state2idx = Map.fromList $ zip states [0..]
+      stateInputIndex n = n `divMod` numInputs
+      -- stateInputPair (s, i) = s * numInputs + i
+      eEdgesFrom = Data.Vector.Unboxed.generate (numStates * numInputs) (fst . stateInputIndex)
+      eEdgesLabel = Data.Vector.generate (numStates * numInputs) (snd . stateInputIndex)
+      eEdgesTo = Data.Vector.Unboxed.generate (numStates * numInputs) ((state2idx Map.!) . snd . (\(s, i) -> behaviour (idx2state Map.! s) (idx2input Map.! i)) . stateInputIndex)
+  in Encoding { .. }

src/MyLib.hs

@@ -1,42 +0,0 @@
-module MyLib where
-
-import Mealy
-
-import Copar.Functors.Polynomial
-import Copar.RefinementInterface (Label, F1)
-import Data.CoalgebraEncoding (Encoding(..))
-import Data.Map.Strict qualified as Map
-import Data.Vector qualified
-import Data.Vector.Unboxed qualified
-
-project :: Eq o => MealyMachine s i o -> o -> MealyMachine s i Bool
-project MealyMachine{..} o = MealyMachine
-  { outputs = [False, True]
-  , behaviour = \s i -> case behaviour s i of
-      (out, s2) -> (out == o, s2)
-  , ..
-  }
-
-mealyMachineToEncoding :: (Ord s, Ord i, Ord o) => MealyMachine s i o -> Encoding (Label Polynomial) (F1 Polynomial)
-mealyMachineToEncoding MealyMachine{..} =
-  let numStates = length states
-      numInputs = length inputs
-      idx2state = Map.fromList $ zip [0..] states
-      idx2input = Map.fromList $ zip [0..] inputs
-      out2idx = Map.fromList $ zip outputs [0..]
-      eStructure = Data.Vector.generate numStates
-        (\s -> PolyF1
-          { polyF1Summand = 0 -- There is only one summand
-          , polyF1Variables = numInputs -- This many transitions per state
-          , polyF1Constants = Data.Vector.Unboxed.generate numInputs
-            (\i -> out2idx Map.! (fst (behaviour (idx2state Map.! s) (idx2input Map.! i))))
-          }
-        )
-      eInitState = Nothing
-      state2idx = Map.fromList $ zip states [0..]
-      stateInputIndex n = n `divMod` numInputs
-      -- stateInputPair (s, i) = s * numInputs + i
-      eEdgesFrom = Data.Vector.Unboxed.generate (numStates * numInputs) (fst . stateInputIndex)
-      eEdgesLabel = Data.Vector.generate (numStates * numInputs) (snd . stateInputIndex)
-      eEdgesTo = Data.Vector.Unboxed.generate (numStates * numInputs) ((state2idx Map.!) . snd . (\(s, i) -> behaviour (idx2state Map.! s) (idx2input Map.! i)) . stateInputIndex)
-  in Encoding { .. }