diff --git a/app/Main.hs b/app/Main.hs index 60d904e..a34cbb1 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,8 +1,124 @@ module Main where -import qualified MyLib (someFunc) +import DotParser +import Mealy +import MyLib +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 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 System.Environment +import Text.Megaparsec + +{- + Hacked together, you can view the result with: + + tred relation.dot | dot -Tpng -G"rankdir=BT" > relation.png + + tred is the graphviz tool to remove transitive edges. And the rankdir + attribute flips the graph upside down. +-} main :: IO () main = do - putStrLn "Hello, Haskell!" - MyLib.someFunc + -- Read dot file + [dotFile] <- getArgs + print dotFile + transitions <- mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile + + -- convert to mealy + let machine = convertToMealy transitions + + -- print some basic info + putStrLn $ (show . length $ states machine) <> " states, " <> (show . length $ inputs machine) <> " inputs and " <> (show . length $ outputs machine) <> " outputs" + putStrLn "Small sample:" + print . take 4 . states $ machine + print . take 4 . inputs $ machine + print . take 4 . outputs $ machine + putStrLn "" + + -- DEBUG OUTPUT + -- forM_ (states machine) (\s -> do + -- print s + -- forM_ (inputs machine) (\i -> do + -- putStr " " + -- let (o, t) = behaviour machine s i + -- putStrLn $ "--" <> (show i) <> "/" <> (show o) <> "->" <> (show t) + -- ) + -- ) + + 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) + 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) + + -- Print number of states of each projection + forM_ (Map.assocs projections) (\(o, partition) -> do + print 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 + (equiv, rel) <- flip execStateT (Map.empty, []) $ do + forM_ (Map.assocs 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 + (repr0, _) <- get + when (o1 < o2 && o2 `Map.notMember` repr0) $ do + case (isRefinementOf b1 b2, isRefinementOf b2 b1) of + (True, True) -> do + (repr, ls) <- get + put (Map.insert o2 o1 repr, ls) + (True, False) -> do + (repr, ls) <- get + put (repr, (o1, o2):ls) + (False, True) -> do + (repr, ls) <- get + put (repr, (o2, o1):ls) + (False, False) -> return () + + -- liftIO $ putStr " vs. " + -- liftIO $ print o2 + ) + ) + + putStrLn "" + putStrLn "Equivalences" + forM_ (Map.assocs equiv) (\(o2, o1) -> do + putStrLn $ " " <> (show o2) <> " == " <> (show o1) + ) + + let cleanRel = [(Map.findWithDefault o1 o1 equiv, Map.findWithDefault o2 o2 equiv) | (o1, o2) <- rel] + putStrLn "" + putStrLn "Relation (smaller points to bigger)" + forM_ (nubSort cleanRel) (\(o1, o2) -> do + putStrLn $ " " <> (show o2) <> " -> " <> (show o1) + ) + + return () diff --git a/mealy-decompose.cabal b/mealy-decompose.cabal index f99c345..2d6b628 100644 --- a/mealy-decompose.cabal +++ b/mealy-decompose.cabal @@ -11,7 +11,10 @@ build-type: Simple common stuff build-depends: base ^>=4.19.0.0, - containers + containers, + copar, + data-ordlist, + megaparsec default-language: GHC2021 default-extensions: RecordWildCards @@ -20,10 +23,12 @@ common stuff library import: stuff hs-source-dirs: src - exposed-modules: MyLib + exposed-modules: + MyLib, + Mealy, + DotParser -- other-modules: build-depends: - copar, vector executable mealy-decompose @@ -31,7 +36,8 @@ executable mealy-decompose hs-source-dirs: app main-is: Main.hs build-depends: - mealy-decompose + mealy-decompose, + transformers test-suite mealy-decompose-test import: stuff diff --git a/src/DotParser.hs b/src/DotParser.hs new file mode 100644 index 0000000..a5c798a --- /dev/null +++ b/src/DotParser.hs @@ -0,0 +1,63 @@ +module DotParser where + +import Data.Char (isAlphaNum) +import Data.List.Ordered qualified as OrdList +import Data.Map.Strict qualified as Map +import Data.Void (Void) +import Mealy +import Text.Megaparsec +import Text.Megaparsec.Char +import Text.Megaparsec.Char.Lexer qualified as L + +{- + Parser for Dot files generated by the RERS LearnLib learner. This is not + a fully fledged parser. It is specific to our models. + + Really only parses a single transition. We just collect all succesfull + transitions. This gives all transitions. + + Usage: + transitions <- mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile +-} + +type Stat = String +type Input = String +type Output = String +type Trans = (Stat, Stat, Input, Output) + +type Parser = Parsec Void String + +parseTrans :: Parser Trans +parseTrans = assoc <$> identifier <* symbol "->" <*> identifier <*> brackets parseLabel <* optional (symbol ";") + where + -- defines whitespace and lexemes + sc = L.space space1 empty empty + lexeme = L.lexeme sc + symbol = L.symbol sc + -- state, input, output is any string of alphaNumChar's + isAlphaNumExtra c = isAlphaNum c || c == '.' || c == '-' + alphaNumCharExtra = satisfy isAlphaNumExtra "alphanumeric character or extra" + identifier = lexeme (some alphaNumCharExtra) + -- The label has the shape [label="i/o"] + brackets = between (symbol "[") (symbol "]") + parseLabel = (,) <$> (symbol "label=\"" *> identifier <* symbol "/") <*> (identifier <* symbol "\"") + -- re-associate different parts of the parser + assoc from to (i, o) = (from, to, i, o) + +parseTransFull :: Parser Trans +parseTransFull = space *> parseTrans <* eof + +convertToMealy :: [Trans] -> MealyMachine String String String +convertToMealy l = MealyMachine + { states = states + , inputs = ins + , outputs = outs + , behaviour = \s i -> base Map.! (s, i) + } + where + froms = OrdList.nubSort . fmap (\(a,_,_,_) -> a) $ l + tos = OrdList.nubSort . fmap (\(_,a,_,_) -> a) $ l + ins = OrdList.nubSort . fmap (\(_,_,i,_) -> i) $ l + outs = OrdList.nubSort . fmap (\(_,_,_,o) -> o) $ l + states = froms `OrdList.union` tos + base = Map.fromList . fmap (\(from, to, i, o) -> ((from, i), (o, to))) $ l diff --git a/src/Mealy.hs b/src/Mealy.hs new file mode 100644 index 0000000..0f6a59d --- /dev/null +++ b/src/Mealy.hs @@ -0,0 +1,23 @@ +module Mealy where + +data MealyMachine s i o = MealyMachine + { states :: [s] + , inputs :: [i] + , outputs :: [o] + , behaviour :: s -> i -> (o, s) + } + +exampleMM :: MealyMachine String Char String +exampleMM = + let states = ["q0", "q1", "q2", "q3"] + inputs = ['a', 'b'] + outputs = ["een", "twee", "drie", "vier"] + behaviour "q0" 'a' = ("een", "q1") + behaviour "q1" 'a' = ("drie", "q0") + behaviour "q2" 'a' = ("een", "q3") + behaviour "q3" 'a' = ("drie", "q2") + behaviour "q0" 'b' = ("vier", "q2") + behaviour "q2" 'b' = ("twee", "q0") + behaviour "q1" 'b' = ("vier", "q3") + behaviour "q3" 'b' = ("twee", "q1") + in MealyMachine {..} diff --git a/src/MyLib.hs b/src/MyLib.hs index bd4a184..e3a0aca 100644 --- a/src/MyLib.hs +++ b/src/MyLib.hs @@ -1,46 +1,17 @@ module MyLib where -import Control.Monad (forM) -import Control.Monad.ST (runST) -import Copar.Algorithm (refine) +import Mealy + import Copar.Functors.Polynomial import Copar.RefinementInterface (Label, F1) import Data.CoalgebraEncoding (Encoding(..)) -import Data.Proxy (Proxy(..)) +import Data.Map.Strict qualified as Map import Data.Vector qualified import Data.Vector.Unboxed qualified -import Data.Map.Strict qualified as Map --- import Data.Map.Strict (Map) - -import Data.Set qualified as Set -import Data.Set (Set) - -data MealyMachine s i o = MealyMachine - { states :: Set s - , inputs :: Set i - , outputs :: Set o - , behaviour :: s -> i -> (o, s) - } - -exampleMM :: MealyMachine String Char String -exampleMM = - let states = Set.fromList ["q0", "q1", "q2", "q3"] - inputs = Set.fromList ['a', 'b'] - outputs = Set.fromList ["xx", "xy", "yx", "yy"] - behaviour "q0" 'a' = ("xx", "q1") - behaviour "q1" 'a' = ("yx", "q0") - behaviour "q2" 'a' = ("xx", "q3") - behaviour "q3" 'a' = ("yx", "q2") - behaviour "q0" 'b' = ("xx", "q2") - behaviour "q2" 'b' = ("xy", "q0") - behaviour "q1" 'b' = ("xx", "q3") - behaviour "q3" 'b' = ("xy", "q1") - in MealyMachine {..} - project :: Eq o => MealyMachine s i o -> o -> MealyMachine s i Bool project MealyMachine{..} o = MealyMachine - { outputs = Set.fromList [False, True] + { outputs = [False, True] , behaviour = \s i -> case behaviour s i of (out, s2) -> (out == o, s2) , .. @@ -48,11 +19,11 @@ project MealyMachine{..} o = MealyMachine mealyMachineToEncoding :: (Ord s, Ord i, Ord o) => MealyMachine s i o -> Encoding (Label Polynomial) (F1 Polynomial) mealyMachineToEncoding MealyMachine{..} = - let numStates = Set.size states - numInputs = Set.size inputs - idx2state = Map.fromList $ zip [0..] (Set.toList states) - idx2input = Map.fromList $ zip [0..] (Set.toList inputs) - out2idx = Map.fromList $ zip (Set.toList outputs) [0..] + 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 @@ -62,24 +33,10 @@ mealyMachineToEncoding MealyMachine{..} = } ) eInitState = Nothing - state2idx = Map.fromList $ zip (Set.toList states) [0..] + 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 { .. } - -someFunc :: IO () -someFunc = do - let blocks = runST $ refine (Proxy @Polynomial) (mealyMachineToEncoding exampleMM) True - print blocks - - forM ["xx", "xy", "yx", "yy"] (\o -> do - print o - let blocks = runST $ refine (Proxy @Polynomial) (mealyMachineToEncoding (project exampleMM o)) True - print blocks - ) - - print "Bye" -