From 21194d2bfd023e4d827c9980d382d27238a72232 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Wed, 30 Jan 2019 18:24:14 +0100 Subject: [PATCH] More types of automata for minimisation --- app/ExampleAutomata.hs | 58 ++++++++++- app/FileAutomata.hs | 232 +++++++++++++++++++++++++++++++++++++++++ app/IO.hs | 3 +- app/Minimise.hs | 27 +++-- ons-hs.cabal | 4 + 5 files changed, 315 insertions(+), 9 deletions(-) create mode 100644 app/FileAutomata.hs diff --git a/app/ExampleAutomata.hs b/app/ExampleAutomata.hs index 15aae19..aeb35d4 100644 --- a/app/ExampleAutomata.hs +++ b/app/ExampleAutomata.hs @@ -21,15 +21,18 @@ import Data.Foldable (fold) import qualified GHC.Generics as GHC import Prelude as P hiding (map, product, words, filter, foldr) --- All example automata follow below + +atoms = rationals -- words of length <= m words m = fold $ go (m+1) (singleOrbit []) where go 0 _ = [] - go k acc = acc : go (k-1) (productWith (:) rationals acc) + go k acc = acc : go (k-1) (productWith (:) atoms acc) fromKeys f = Map.fromSet f . Set.fromOrbitList +ltPair = filter (\(a, b) -> a < b) $ product atoms atoms + data DoubleWord = Store [Atom] | Check [Atom] | Accept | Reject deriving (Eq, Ord, GHC.Generic) @@ -99,3 +102,54 @@ fifoAut n = Automaton {..} where | a == b = Just (FifoS l1 l2) | otherwise = Nothing transition = fromKeys (uncurry trans) $ product states fifoAlph + + +data Lint a = Lint_start | Lint_single a | Lint_full a a | Lint_semi a a | Lint_error + deriving (Eq, Ord, Show, GHC.Generic) + deriving Nominal via Generic (Lint a) + +lintExample ::Automaton (Lint Atom) Atom +lintExample = Automaton {..} where + states = fromList [Lint_start, Lint_error] + <> map Lint_single atoms + <> map (uncurry Lint_full) ltPair + <> map (uncurry Lint_semi) ltPair + initialState = Lint_start + acc (Lint_full _ _) = True + acc _ = False + acceptance = fromKeys acc states + trans Lint_start a = Lint_single a + trans (Lint_single a) b + | a < b = Lint_full a b + | otherwise = Lint_error + trans (Lint_full a b) c + | a < c && c < b = Lint_semi c b + | otherwise = Lint_error + trans (Lint_semi a b) c + | a < c && c < b = Lint_full a c + | otherwise = Lint_error + trans Lint_error _ = Lint_error + transition = fromKeys (uncurry trans) $ product states atoms + + +data Lmax a = Lmax_start | Lmax_single a | Lmax_double a a + deriving (Eq, Ord, Show, GHC.Generic) + deriving Nominal via Generic (Lmax a) + +lmaxExample :: Automaton (Lmax Atom) Atom +lmaxExample = Automaton {..} where + states = singleOrbit Lmax_start + <> map Lmax_single atoms + <> productWith Lmax_double atoms atoms + initialState = Lmax_start + acc (Lmax_double a b) = a == b + acc _ = False + acceptance = fromKeys acc states + trans Lmax_start a = Lmax_single a + trans (Lmax_single a) b = Lmax_double a b + trans (Lmax_double b c) a + | b >= c = Lmax_double b a + | otherwise = Lmax_double c a + transition = fromKeys (uncurry trans) $ product states atoms + + diff --git a/app/FileAutomata.hs b/app/FileAutomata.hs new file mode 100644 index 0000000..4acb325 --- /dev/null +++ b/app/FileAutomata.hs @@ -0,0 +1,232 @@ +{-# language DuplicateRecordFields #-} +{-# language FlexibleContexts #-} +{-# language RecordWildCards #-} + +module FileAutomata + ( fileAutomaton + , formulaAutomaton + ) where + +import qualified Data.Map as M +import Data.Map ((!)) +import Data.Void (Void) +import Control.Monad.Combinators.Expr +import System.Exit (exitFailure) +import Text.Megaparsec as P +import Text.Megaparsec.Char as P +import qualified Text.Megaparsec.Char.Lexer as L + +import OrbitList +import Nominal (Atom) +import Nominal.Class +import Support (Support, def) +import Automata +import qualified EquivariantSet as Set +import qualified EquivariantMap as Map + +import Prelude hiding (map, product, filter) +import qualified Prelude as P + + +-- *************** +-- ** Utilities ** +-- *************** +atoms = rationals + +-- words of length == n +replicateAtoms 0 = singleOrbit [] +replicateAtoms n = productWith (:) atoms (replicateAtoms (n-1)) + +fromKeys f = Map.fromSet f . Set.fromOrbitList + +sortedAtoms n = singleOrbit (def n) + + +-- ************************** +-- ** File data structures ** +-- ************************** +type Var = (Bool, Int) -- state/input + index +type Loc = Int +type Label = Int +type Dimension = Int +type MapStr = [Ordering] +type MapSup = [Bool] + +data AutomatonDescr = AutomatonD + { alphSize :: Int + , statesSize :: Int + , alph :: [(Label, Dimension)] + , locations :: [(Loc, Dimension, Bool)] + , trans :: [(Loc, Label, MapStr, Loc, MapSup)] + } deriving Show + +data Form + = Lit Char Var Var -- '<', '=', '>' + | And Form Form + | Or Form Form + | Not Form + deriving Show + +data FAutomatonDescr = FAutomaton + { alphSize :: Int + , statesSize :: Int + , alph :: [(Label, Dimension)] + , locations :: [(Loc, Dimension, Bool)] + , trans :: [(Loc, Label, Form, Loc, [Var])] + } deriving Show + + +-- ****************** +-- ** File parsers ** +-- ****************** +type Parser = Parsec Void String + +-- space consumer and lexer +sc = L.space space1 P.empty P.empty +lexeme = L.lexeme sc +symbol = L.symbol sc + +-- some basic parsers +parens = between (symbol "(") (symbol ")") +arrow = symbol "->" +integer = lexeme L.decimal +boolean = lexeme binDigitChar + +alphP :: Parser (Label, Dimension) +alphP = (,) <$> integer <*> integer + +stateP :: Parser (Loc, Dimension, Bool) +stateP = toS <$> integer <*> integer <*> boolean where + toS s d a = (s, d, a == '1') + +transP :: Parser (Loc, Label, MapStr, Loc, MapSup) +transP = toT <$> integer <*> integer <*> lexeme (many upperChar) <* arrow <*> integer <*> lexeme (many binDigitChar) where + toT s a ms t sup = (s, a, fmap conv ms, t, fmap ('1' ==) sup) + conv 'A' = LT + conv 'B' = GT + conv 'C' = EQ + +p :: Parser AutomatonDescr +p = do + symbol "Automaton" + alphSize <- integer + statesSize <- integer + symbol "Alphabet" + alph <- count alphSize alphP + symbol "States" + locations <- count statesSize stateP + symbol "Delta" + trans <- many transP + return AutomatonD {..} + +var :: Parser Var +var = lexeme (toV <$> lowerChar <*> many digitChar) where + toV 'x' str = (False, read str) -- state var + toV 'y' str = (True, read str) -- input var + +transFP :: Parser (Loc, Label, Form, Loc, [Var]) +transFP = toT <$> integer <*> integer <*> formP <* arrow <*> integer <*> many var where + toT s a f t vs = (s, a, f, t, vs) + +litP :: Parser Form +litP = toL <$> var <*> lexeme asciiChar <*> var where + toL v1 c v2 = Lit c v1 v2 + +formP :: Parser Form +formP = makeExprParser bTerm bOperators where + bOperators = + [ [ Prefix (Not <$ symbol "not") ] + , [ InfixL (And <$ symbol "and") + , InfixL (Or <$ symbol "or" ) ] + ] + bTerm = parens formP <|> litP + +fp :: Parser FAutomatonDescr +fp = do + symbol "FAutomaton" + alphSize <- integer + statesSize <- integer + symbol "Alphabet" + alph <- count alphSize alphP + symbol "States" + locations <- count statesSize stateP + symbol "Delta" + trans <- many transFP + return FAutomaton {..} + + +-- ***************************** +-- ** Conversion to Automaton ** +-- ***************************** +descriptionToOns :: AutomatonDescr -> (Automaton (Int, Support) (Int, Support), OrbitList (Int, Support)) +descriptionToOns AutomatonD{..} = (Automaton{..}, alphabet) where + states = mconcat [map (\w -> (l, w)) (sortedAtoms d) | (l, d, _) <- locations] + alphabet = mconcat [map (\w -> (l, w)) (sortedAtoms d) | (l, d) <- alph] + initialState = error "No initial state" + sDim = M.fromList [(l, (sortedAtoms d, b)) | (l, d, b) <- locations] + aDim = M.fromList [(l, sortedAtoms d) | (l, d) <- alph] + dims mStr = (P.length . P.filter (/= GT) $ mStr, P.length . P.filter (/= LT) $ mStr) + dims2 bv = P.length . P.filter id $ bv + -- The files are exactly encoded in the way the library works + -- But it means we have to get our hand dirty... + transition = Map.EqMap . M.fromList $ [ (key, (val, bStr)) + | (s, l, mStr, t, bStr) <- trans + , let (sd, ad) = dims mStr + , let k1 = OrbPair (OrbRec s) (OrbRec sd) (replicate sd GT) + , let k2 = OrbPair (OrbRec l) (OrbRec ad) (replicate ad GT) + , let key = OrbPair (OrbRec k1) (OrbRec k2) mStr + , let val = OrbPair (OrbRec t) (OrbRec (dims2 bStr)) (replicate (dims2 bStr) GT) ] + acc (s, w) = let (_, b) = sDim ! s in b + acceptance = fromKeys acc states + +-- This is very similar to the NLambda code, but instead of Formula +-- we use the standard Bool type. +formToOns :: Form -> [Atom] -> [Atom] -> Bool +formToOns (Lit c (b1, n1) (b2, n2)) xs ys = op c (xys b1 !! n1) (xys b2 !! n2) + where + xys False = xs + xys True = ys + op '<' = (<) + op '=' = (==) + op '>' = (>) +formToOns (And f1 f2) xs ys = formToOns f1 xs ys && formToOns f2 xs ys +formToOns (Or f1 f2) xs ys = formToOns f1 xs ys || formToOns f2 xs ys +formToOns (Not f) xs ys = not (formToOns f xs ys) + +varsToOns vars xs ys = [xys b !! n | (b, n) <- vars] where + xys False = xs + xys True = ys + +fdescriptionToOns :: FAutomatonDescr -> (Automaton (Int, [Atom]) (Int, [Atom]), OrbitList (Int, [Atom])) +fdescriptionToOns FAutomaton{..} = (Automaton{..}, alphabet) where + states = mconcat [map (\w -> (l, w)) (replicateAtoms d) | (l, d, _) <- locations] + alphabet = mconcat [map (\w -> (l, w)) (replicateAtoms d) | (l, d) <- alph] + initialState = error "No initial state" + sDim = M.fromList [(l, (replicateAtoms d, b)) | (l, d, b) <- locations] + aDim = M.fromList [(l, replicateAtoms d) | (l, d) <- alph] + transition = Map.fromList . mconcat $ [toList . map (\(xs, ys) -> (((s, xs), (l, ys)), (t, varsToOns vars xs ys))) . filter (\(xs, ys) -> formToOns phi xs ys) $ product (fst (sDim ! s)) (aDim ! l) | (s, l, phi, t, vars) <- trans] + acc (s, w) = let (_, b) = sDim ! s in b + acceptance = fromKeys acc states + + +-- ************************** +-- ** Actual file handling ** +-- ************************** +fileAutomaton file = do + result <- runParser p file <$> readFile file + case result of + Left bundle -> do + putStr (errorBundlePretty bundle) + exitFailure + Right autDescription -> do + return $ descriptionToOns autDescription + +formulaAutomaton file = do + result <- runParser fp file <$> readFile file + case result of + Left bundle -> do + putStr (errorBundlePretty bundle) + exitFailure + Right autDescription -> do + return $ fdescriptionToOns autDescription + diff --git a/app/IO.hs b/app/IO.hs index 3d39ab1..c244241 100644 --- a/app/IO.hs +++ b/app/IO.hs @@ -41,7 +41,8 @@ instance ToStr a => ToStr (Maybe a) where instance (Nominal q, Nominal a, ToStr q, ToStr a) => ToStr (Automaton q a) where toStr Automaton{..} = "{ states = " ++ toStr (L.toList states) ++ - ", initialState = " ++ toStr initialState ++ + -- HACK: Some automata have no initial state, this avoids crashing + --", initialState = " ++ toStr initialState ++ ", acceptance = " ++ toStr (M.toList acceptance) ++ ", transition = " ++ toStr (M.toList transition) ++ " }" diff --git a/app/Minimise.hs b/app/Minimise.hs index 2875faf..0f2898e 100644 --- a/app/Minimise.hs +++ b/app/Minimise.hs @@ -7,6 +7,7 @@ {-# OPTIONS_GHC -Wno-partial-type-signatures #-} import ExampleAutomata +import FileAutomata import IO import Quotient import OrbitList @@ -14,12 +15,15 @@ import EquivariantMap ((!)) import qualified EquivariantMap as Map import qualified EquivariantSet as Set +import System.Environment +import System.IO + import Prelude as P hiding (map, product, words, filter, foldr) -- Version A: works on equivalence relations -minimiseA :: _ => Automaton q a -> OrbitList a -> Automaton _ a -minimiseA Automaton{..} alph = Automaton +minimiseA :: _ => OrbitList a -> Automaton q a -> Automaton _ a +minimiseA alph Automaton{..} = Automaton { states = states2 , initialState = phi ! initialState , acceptance = Map.fromList . fmap (\(s, b) -> (phi ! s, b)) . Map.toList $ acceptance @@ -45,8 +49,8 @@ minimiseA Automaton{..} alph = Automaton -- Version B: works on quotient maps -minimiseB :: _ => Automaton q a -> OrbitList a -> Automaton _ a -minimiseB Automaton{..} alph = Automaton +minimiseB :: _ => OrbitList a -> Automaton q a -> Automaton _ a +minimiseB alph Automaton{..} = Automaton { states = map fst stInf , initialState = phiInf ! initialState , acceptance = Map.fromList . fmap (\(s, b) -> (phiInf ! s, b)) . Map.toList $ acceptance @@ -73,5 +77,16 @@ minimiseB Automaton{..} alph = Automaton main :: IO () main = do - putStrLn . toStr $ (minimiseB (doubleWordAut 4) rationals) - -- putStrLn . toStr $ (minimiseB (fifoAut 4) fifoAlph) + f:w <- getArgs + case f of + "Lmax" -> putStrLn . toStr . minimiseB rationals $ lmaxExample + "Lint" -> putStrLn . toStr . minimiseB rationals $ lintExample + "Fifo" -> putStrLn . toStr . minimiseB fifoAlph $ fifoAut (read (P.head w) :: Int) + "DoubleWord" -> putStrLn . toStr . minimiseB rationals $ doubleWordAut (read (P.head w) :: Int) + "File" -> do + let m f = fileAutomaton f >>= \(aut, alph) -> putStrLn . toStr . minimiseB alph $ aut + mapM_ m w + "Formula" -> do + (aut, alph) <- formulaAutomaton (P.head w) + putStrLn . toStr . minimiseB alph $ aut + diff --git a/ons-hs.cabal b/ons-hs.cabal index c693f4c..39e3bbc 100644 --- a/ons-hs.cabal +++ b/ons-hs.cabal @@ -56,9 +56,13 @@ executable ons-hs-minimise hs-source-dirs: app main-is: Minimise.hs build-depends: base + , containers + , megaparsec , mtl , ons-hs + , parser-combinators other-modules: ExampleAutomata + , FileAutomata , IO ghc-options: -O2 default-language: Haskell2010