From 18e0b2f4d618e23096229972c30a20f6733c2245 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Wed, 22 Nov 2023 12:20:54 +0100 Subject: [PATCH] Moved some bits around --- app/Main.hs | 52 +++++++++++++-------------- mealy-decompose.cabal | 5 ++- src/MealyRefine.hs | 84 +++++++++++++++++++++++++++++++++++++++++++ src/MyLib.hs | 42 ---------------------- 4 files changed, 111 insertions(+), 72 deletions(-) create mode 100644 src/MealyRefine.hs delete mode 100644 src/MyLib.hs diff --git a/app/Main.hs b/app/Main.hs index a34cbb1..20b1a2c 100644 --- a/app/Main.hs +++ b/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.Trans.State.Strict -import Control.Monad (forM_, when) -import Control.Monad.ST (runST) -import Copar.Algorithm (refine) -import Copar.Functors.Polynomial (Polynomial) -import Data.Map.Strict qualified as Map +-- import Control.Monad.IO.Class (liftIO) +-- import Control.Monad.Trans.State.Strict +import Control.Monad (forM_) +-- 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.Set qualified as Set -import Data.List.Ordered (nubSort) +-- import Data.Semigroup (Arg(..)) +-- import Data.Set qualified as Set +-- 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 - outs = outputs machine - projections = Map.fromSet minimiseProjection (Set.fromList outs) + -- I did some manual preprocessing, these are the only interesting bits + 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"] + -- 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 - print o + forM_ projections (\(o, partition) -> do + 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 () + + -} diff --git a/mealy-decompose.cabal b/mealy-decompose.cabal index 2d6b628..9b1b634 100644 --- a/mealy-decompose.cabal +++ b/mealy-decompose.cabal @@ -24,10 +24,9 @@ library import: stuff hs-source-dirs: src exposed-modules: - MyLib, + DotParser, Mealy, - DotParser - -- other-modules: + MealyRefine build-depends: vector diff --git a/src/MealyRefine.hs b/src/MealyRefine.hs new file mode 100644 index 0000000..2ff98bc --- /dev/null +++ b/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 { .. } diff --git a/src/MyLib.hs b/src/MyLib.hs deleted file mode 100644 index e3a0aca..0000000 --- a/src/MyLib.hs +++ /dev/null @@ -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 { .. }