diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,16 @@ ## Unreleased +## 0.4.1.0 - 2026-03-21 + +### Added +- Serializer from Mealy Automaton to Dot format. +- haal-gen executable that accepts a .dot file and produces a haskell module + that exports a function for the specified Mealy Automaton, with specific + input and output types, rather than just using String for both. +- haal-models subpackage that exports learned models of tls, mqtt, tcp and dtls + protocols. + ## 0.4.0.2 - 2026-03-17 ### Changed diff --git a/app/HaalGen.hs b/app/HaalGen.hs new file mode 100644 --- /dev/null +++ b/app/HaalGen.hs @@ -0,0 +1,60 @@ +-- | haal-gen: generate a Haskell module from a Mealy automaton in DOT format. +-- +-- Usage: +-- haal-gen +-- +-- The generated module is written to stdout. +module Main (main) where + +import System.Environment (getArgs) +import System.Exit (exitFailure, exitSuccess) +import System.IO (hPutStrLn, stderr) + +import Haal.Dot (parseDot, generateModule, parsedWarnings) + +helpText :: String +helpText = unlines + [ "haal-gen - generate a Haskell module from a Mealy automaton in DOT format" + , "" + , "Usage:" + , " haal-gen " + , "" + , "Arguments:" + , " Path to a DOT file (AALpy or LearnLib format)" + , " Fully qualified Haskell module name (e.g. My.Module.Name)" + , " Name for the generated automaton value (e.g. myAutomaton)" + , "" + , "Output:" + , " Haskell source is written to stdout; warnings and errors to stderr." + , " The generated module contains typed input/output ADTs and a" + , " MealyAutomaton value, ready to import and use with haal." + , "" + , "Example:" + , " haal-gen model.dot Haal.Models.Foo fooModel > src/Haal/Models/Foo.hs" + ] + +main :: IO () +main = do + args <- getArgs + case args of + ["--help"] -> putStr helpText >> exitSuccess + [dotFile, modName, valName] -> run dotFile modName valName + _ -> do + hPutStrLn stderr "Usage: haal-gen " + hPutStrLn stderr "Run 'haal-gen --help' for more information." + exitFailure + +run :: FilePath -> String -> String -> IO () +run dotFile modName valName = do + src <- readFile dotFile + case parseDot src of + Left err -> do + hPutStrLn stderr ("haal-gen: parse error: " ++ err) + exitFailure + Right pm -> do + mapM_ (hPutStrLn stderr . ("haal-gen: warning: " ++)) (parsedWarnings pm) + case generateModule modName valName pm of + Left err -> do + hPutStrLn stderr ("haal-gen: " ++ err) + exitFailure + Right hsrc -> putStr hsrc diff --git a/haal.cabal b/haal.cabal --- a/haal.cabal +++ b/haal.cabal @@ -1,11 +1,11 @@ cabal-version: 2.2 --- This file has been generated from package.yaml by hpack version 0.38.1. +-- This file has been generated from package.yaml by hpack version 0.37.0. -- -- see: https://github.com/sol/hpack name: haal -version: 0.4.0.2 +version: 0.4.1.0 synopsis: A Haskell library for Active Automata Learning. description: Please see the README on GitHub at category: Model Learning @@ -37,6 +37,7 @@ Haal.Automaton.MealyAutomaton Haal.Automaton.MooreAutomaton Haal.BlackBox + Haal.Dot Haal.EquivalenceOracle.CombinedOracle Haal.EquivalenceOracle.RandomWalk Haal.EquivalenceOracle.RandomWords @@ -91,6 +92,20 @@ base , haal , mtl + default-language: Haskell2010 + +executable haal-gen + main-is: HaalGen.hs + other-modules: + Paths_haal + autogen-modules: + Paths_haal + hs-source-dirs: + app + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints + build-depends: + base + , haal default-language: Haskell2010 executable io diff --git a/src/Haal/Dot.hs b/src/Haal/Dot.hs new file mode 100644 --- /dev/null +++ b/src/Haal/Dot.hs @@ -0,0 +1,367 @@ +{- | Serialization, parsing, and code generation for Mealy automata in DOT +format, following the convention used by AALpy and LearnLib. +-} +module Haal.Dot ( + mealyToDot, + ParsedMealy (..), + parseDot, + generateModule, +) where + +import Data.Char (isAlphaNum, isDigit, isLower, isSpace, toUpper) +import Data.List (intercalate, isInfixOf, isPrefixOf, nub) +import qualified Data.Map.Strict as Map +import Data.Maybe (mapMaybe) +import qualified Data.Set as Set + +import Haal.Automaton.MealyAutomaton (MealyAutomaton, mealyTransitions) +import Haal.BlackBox (Automaton (..), FiniteOrd, initial) + +-- --------------------------------------------------------------------------- +-- Serializer +-- --------------------------------------------------------------------------- + +{- | Serialize a 'MealyAutomaton' to a DOT format string. + + The output follows the AALpy\/LearnLib convention: + + * States are rendered as @s0@, @s1@, … in ascending order, with their + 'show' representation as the node label. + * Edge labels have the form @\"input\/output\"@. + * The initial state is indicated by a @__start0@ dummy node. + + Returns @'Left' err@ if any input or output symbol's 'show' representation + contains @\'\/\'@, as that would make the DOT file impossible to parse back + correctly. +-} +mealyToDot :: + (FiniteOrd s, FiniteOrd i, Show s, Show i, Show o) => + MealyAutomaton s i o -> + Either String String +mealyToDot m = do + let badInputs = filter ('/' `elem`) (map (show . snd) (Map.toList inputSet)) + badOutputs = filter ('/' `elem`) (map (show . snd . snd) (Map.toList trans)) + case (badInputs, badOutputs) of + (i : _, _) -> Left ("Input label contains '/': " ++ i) + (_, o : _) -> Left ("Output label contains '/': " ++ o) + _ -> + Right $ + unlines $ + ["digraph haal {"] + ++ zipWith (curry nodeDecl) [0 :: Int ..] sortedStates + ++ map edgeDecl (Map.toList trans) + ++ [ "\t__start0 [label=\"\" shape=none];" + , "\t__start0 -> " ++ nodeId (initial m) ++ " [label=\"\"];" + , "}" + ] + where + sortedStates = Set.toAscList (states m) + stateIndex = Map.fromList (zip sortedStates [0 :: Int ..]) + trans = mealyTransitions m + inputSet = Map.fromList [((s, i), i) | (s, i) <- Map.keys trans] + + nodeId s = "s" ++ show (stateIndex Map.! s) + + nodeDecl (i, s) = + "\ts" ++ show i ++ " [label=\"" ++ show s ++ "\"];" + + edgeDecl ((s, i), (s', o)) = + "\t" + ++ nodeId s + ++ " -> " + ++ nodeId s' + ++ " [label=\"" + ++ show i + ++ "/" + ++ show o + ++ "\"];" + +-- --------------------------------------------------------------------------- +-- Parser +-- --------------------------------------------------------------------------- + +{- | The raw representation of a Mealy automaton parsed from DOT format. + State, input, and output names are kept as 'String's. + States are ordered with the initial state first, then others in order of + first appearance in the transition list. +-} +data ParsedMealy = ParsedMealy + { parsedInitState :: String + , parsedStates :: [String] + , parsedInputs :: [String] + , parsedOutputs :: [String] + , parsedTrans :: [(String, String, String, String)] + -- ^ @(srcState, input, dstState, output)@ + , parsedWarnings :: [String] + } + deriving (Show) + +{- | Parse a DOT format string representing a Mealy automaton. + + Supports the output format of both AALpy and LearnLib: + + * Initial state indicated by @__start0 -> \@ + * Edge labels of the form @\"input\/output\"@ or @\"input \/ output\"@ + (whitespace around @\/@ is stripped) + + Returns @'Left' err@ with a descriptive message on failure. +-} +parseDot :: String -> Either String ParsedMealy +parseDot src = do + let ls = lines src + initSt <- findInit ls + trans <- collectTrans ls + let allStates = nub $ concatMap (\(s, _, d, _) -> [s, d]) trans + if initSt `notElem` allStates + then Left ("Initial state '" ++ initSt ++ "' does not appear in any transition") + else do + let otherStates = filter (/= initSt) allStates + stateOrder = initSt : otherStates + inputSyms = nub $ map (\(_, i, _, _) -> i) trans + outputSyms = nub $ map (\(_, _, _, o) -> o) trans + warnings = slashWarnings inputSyms outputSyms + return + ParsedMealy + { parsedInitState = initSt + , parsedStates = stateOrder + , parsedInputs = inputSyms + , parsedOutputs = outputSyms + , parsedTrans = trans + , parsedWarnings = warnings + } + +-- --------------------------------------------------------------------------- +-- Code generator +-- --------------------------------------------------------------------------- + +{- | Generate a Haskell module from a 'ParsedMealy'. + + @generateModule modName valName pm@ produces source for a module named + @modName@ containing: + + * A @data \Input@ type whose constructors are the sanitized input + symbols, deriving @Show, Eq, Ord, Enum, Bounded@. + * A @data \Output@ type, similarly for output symbols. + * A value @valName :: MealyAutomaton Int \Input \Output@. + + Returns @'Left' err@ if two distinct symbols sanitize to the same + constructor name. +-} +generateModule :: String -> String -> ParsedMealy -> Either String String +generateModule modName valName pm = do + inputCons <- sanitizeAll "In_" "input" (parsedInputs pm) + outputCons <- sanitizeAll "Out_" "output" (parsedOutputs pm) + let stateNames = parsedStates pm + n = length stateNames + stateIdx = Map.fromList (zip stateNames [0 :: Int ..]) + inputConMap = Map.fromList (zip (parsedInputs pm) inputCons) + outputConMap = Map.fromList (zip (parsedOutputs pm) outputCons) + modSuffix = reverse . takeWhile (/= '.') . reverse $ modName + inputType = modSuffix ++ "Input" + outputType = modSuffix ++ "Output" + deltaLines = map (mkDeltaLine stateIdx inputConMap) (parsedTrans pm) + lambdaLines = map (mkLambdaLine stateIdx inputConMap outputConMap) (parsedTrans pm) + return $ + unlines $ + [ "-- Generated by haal-gen. Do not edit manually." + , "module " ++ modName + , " ( " ++ inputType ++ " (..)" + , " , " ++ outputType ++ " (..)" + , " , " ++ valName + , " ) where" + , "" + , "import qualified Data.Set as Set" + , "import Haal.Automaton.MealyAutomaton (MealyAutomaton, mkMealyAutomaton)" + , "" + , "data " ++ inputType + ] + ++ enumDecl inputCons + ++ [ "" + , "data " ++ outputType + ] + ++ enumDecl outputCons + ++ [ "" + , valName ++ " :: MealyAutomaton Int " ++ inputType ++ " " ++ outputType + , valName + ++ " = mkMealyAutomaton delta lambda (Set.fromList [0.." + ++ show (n - 1) + ++ "]) 0" + , " where" + ] + ++ map (" " ++) deltaLines + ++ [" delta _ _ = error \"haal-gen: undefined transition\""] + ++ map (" " ++) lambdaLines + ++ [" lambda _ _ = error \"haal-gen: undefined transition\""] + +-- --------------------------------------------------------------------------- +-- Code generation helpers +-- --------------------------------------------------------------------------- + +enumDecl :: [String] -> [String] +enumDecl [] = [" deriving (Show, Eq, Ord, Enum, Bounded)"] +enumDecl (c : cs) = + [" = " ++ c] + ++ map (" | " ++) cs + ++ [" deriving (Show, Eq, Ord, Enum, Bounded)"] + +mkDeltaLine :: + Map.Map String Int -> + Map.Map String String -> + (String, String, String, String) -> + String +mkDeltaLine stateIdx inputConMap (src, inp, dst, _) = + "delta " ++ show si ++ " " ++ ic ++ " = " ++ show di + where + si = stateIdx Map.! src + di = stateIdx Map.! dst + ic = inputConMap Map.! inp + +mkLambdaLine :: + Map.Map String Int -> + Map.Map String String -> + Map.Map String String -> + (String, String, String, String) -> + String +mkLambdaLine stateIdx inputConMap outputConMap (src, inp, _, out) = + "lambda " ++ show si ++ " " ++ ic ++ " = " ++ oc + where + si = stateIdx Map.! src + ic = inputConMap Map.! inp + oc = outputConMap Map.! out + +{- | Sanitize a list of symbols to valid Haskell constructor names using the + given prefix, failing if two distinct symbols would produce the same name. +-} +sanitizeAll :: String -> String -> [String] -> Either String [String] +sanitizeAll prefix kind syms = + let sanitized = map (sanitizeName prefix) syms + byConName = Map.fromListWith (++) (zip sanitized (map (: []) syms)) + collisions = + [ (con, originals) + | (con, originals) <- Map.toList byConName + , length originals > 1 + ] + in case collisions of + [] -> Right sanitized + cs -> + Left $ + "Colliding " + ++ kind + ++ " constructor names:\n" + ++ unlines + [ " " + ++ intercalate ", " (map show originals) + ++ " → " + ++ con + | (con, originals) <- cs + ] + +{- | Sanitize a symbol string to a valid Haskell constructor name: + replace non-alphanumeric characters with @_@, strip leading\/trailing + underscores, capitalise the first character, prefix with @N@ if it + starts with a digit, and prepend the given prefix. +-} +sanitizeName :: String -> String -> String +sanitizeName prefix s = prefix ++ base + where + s1 = map (\c -> if isAlphaNum c then c else '_') s + s2 = reverse (dropWhile (== '_') (reverse (dropWhile (== '_') s1))) + s3 = if null s2 then "Unknown" else s2 + base = case s3 of + (c : cs) + | isLower c -> toUpper c : cs + | isDigit c -> 'N' : s3 + | otherwise -> s3 + [] -> "Unknown" + +-- --------------------------------------------------------------------------- +-- Parser helpers +-- --------------------------------------------------------------------------- + +slashWarnings :: [String] -> [String] -> [String] +slashWarnings inputs outputs = + [ "Input symbol contains '/': \"" ++ s ++ "\" — label may have been misparsed" + | s <- inputs + , '/' `elem` s + ] + ++ [ "Output symbol contains '/': \"" ++ s ++ "\" — label may have been misparsed" + | s <- outputs + , '/' `elem` s + ] + +findInit :: [String] -> Either String String +findInit ls = + case mapMaybe extractInit ls of + [] -> Left "No initial state marker found (expected '__start0 -> ')" + (s : _) -> Right s + where + extractInit l + | "__start0" `isInfixOf` l && "->" `isInfixOf` l = + let afterArrow = trim $ drop 2 $ snd $ breakOn "->" l + name = takeWhile isStateChar afterArrow + in if null name then Nothing else Just name + | otherwise = Nothing + +collectTrans :: [String] -> Either String [(String, String, String, String)] +collectTrans ls = concat <$> mapM process relevantLines + where + relevantLines = filter isEdgeLine ls + isEdgeLine l = "->" `isInfixOf` l && not ("__start0" `isInfixOf` l) + process l = + case extractLabel l of + Nothing -> Right [] + Just "" -> Right [] + Just lbl -> case splitLabel lbl of + Left err -> Left ("Malformed label \"" ++ lbl ++ "\": " ++ err) + Right (inp, out) -> + case parseEndpoints l of + Nothing -> Left ("Could not parse endpoints in: " ++ trim l) + Just (src, dst) -> Right [(src, inp, dst, out)] + +extractLabel :: String -> Maybe String +extractLabel l = + case findSubstr "label=" l of + Nothing -> Nothing + Just after -> + case dropWhile isSpace after of + '"' : rest -> Just $ takeWhile (/= '"') rest + rest -> Just $ takeWhile (\c -> c /= ',' && c /= ']' && not (isSpace c)) rest + +parseEndpoints :: String -> Maybe (String, String) +parseEndpoints l = + let (srcPart, rest) = breakOn "->" l + src = trim srcPart + afterArrow = trim (drop 2 rest) + dst = trim $ takeWhile (\c -> c /= '[' && c /= ';') afterArrow + in if null src || null dst then Nothing else Just (src, dst) + +splitLabel :: String -> Either String (String, String) +splitLabel lbl = + case breakOn "/" lbl of + (_, []) -> Left "missing '/' separator" + (inp, _ : out) -> + let i = trim inp + o = trim out + in if null i + then Left "empty input" + else Right (i, o) + +findSubstr :: String -> String -> Maybe String +findSubstr _ [] = Nothing +findSubstr needle haystack@(_ : xs) + | needle `isPrefixOf` haystack = Just (drop (length needle) haystack) + | otherwise = findSubstr needle xs + +breakOn :: String -> String -> (String, String) +breakOn _ [] = ([], []) +breakOn needle haystack@(x : xs) + | needle `isPrefixOf` haystack = ([], haystack) + | otherwise = + let (pre, rest) = breakOn needle xs + in (x : pre, rest) + +trim :: String -> String +trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace + +isStateChar :: Char -> Bool +isStateChar c = isAlphaNum c || c == '_' diff --git a/src/Haal/EquivalenceOracle/WMethod.hs b/src/Haal/EquivalenceOracle/WMethod.hs --- a/src/Haal/EquivalenceOracle/WMethod.hs +++ b/src/Haal/EquivalenceOracle/WMethod.hs @@ -21,7 +21,7 @@ import System.Random (Random (randomR), StdGen) -- | The 'WMethodConfig' type is used to configure the W-method equivalence oracle. -data WMethodConfig = WMethodConfig +newtype WMethodConfig = WMethodConfig { wmDepth :: Int -- ^ The number of extra states beyond the hypothesis to account for. } diff --git a/src/Haal/Learning/LMstar.hs b/src/Haal/Learning/LMstar.hs --- a/src/Haal/Learning/LMstar.hs +++ b/src/Haal/Learning/LMstar.hs @@ -54,7 +54,7 @@ {-@ data ObservationTable i o = ObservationTable { prefixSetS :: Set.Set [i] , suffixSetE :: Set.Set {v:[i] | len v > 0} - , mappingT :: Map.Map ([i], [i]) {v:[o] | len v > 0} + , mappingT :: Map.Map ([i], {v:[i] | len v > 0}) {v:[o] | len v > 0} , prefixSetSI :: Set.Set {v:[i] | len v > 0} } @-} data ObservationTable i o = ObservationTable @@ -412,9 +412,9 @@ {-@ insertStep :: (Ord i, SUL sul m, Monad m) => sul i o - -> Map.Map ([i],[i]) {v:[o] | len v > 0} + -> Map.Map ([i],{v:[i] | len v > 0}) {v:[o] | len v > 0} -> ([i], {b:[i] | len b > 0}) - -> m (Map.Map ([i],[i]) {v:[o] | len v > 0}) @-} + -> m (Map.Map ([i],{v:[i] | len v > 0}) {v:[o] | len v > 0}) @-} insertStep :: (Ord i, SUL sul m, Monad m) => sul i o -> @@ -430,10 +430,10 @@ {-@ updateMap :: (Ord i, SUL sul m, Monad m) - => Map.Map ([i],[i]) {v:[o] | len v > 0} + => Map.Map ([i],{v:[i] | len v > 0}) {v:[o] | len v > 0} -> Set.Set ([i], {v:[i] | len v > 0}) -> sul i o - -> m (Map.Map ([i],[i]) {v:[o] | len v > 0}) @-} + -> m (Map.Map ([i],{v:[i] | len v > 0}) {v:[o] | len v > 0}) @-} updateMap :: (Ord i, SUL sul m, Monad m) => Map.Map ([i], [i]) [o] ->