haal 0.5.0.0 → 0.7.0.0

raw patch · 30 files changed

+1776/−601 lines, 30 filesdep +foldlsetup-changedPVP ok

version bump matches the API change (PVP)

Dependencies added: foldl

API changes (from Hackage documentation)

Files

• CHANGELOG.md +152/−1
• README.md +1/−1
• Setup.hs +1/−0
• app/HaalGen.hs +29/−27
• bench/Bench/BlackBox.hs +51/−20
• bench/Bench/Dot.hs +46/−16
• bench/Bench/EndToEnd.hs +59/−26
• bench/Bench/EquivalenceOracle.hs +70/−34
• bench/Main.hs +7/−6
• examples/demo.hs +2/−1
• examples/div.hs +9/−8
• examples/io.hs +34/−83
• examples/website.hs +4/−4
• haal.cabal +8/−4
• src/Haal/Automaton/DFA.hs +0/−20
• src/Haal/Automaton/MealyAutomaton.hs +83/−2
• src/Haal/Automaton/MooreAutomaton.hs +0/−97
• src/Haal/BlackBox.hs +130/−30
• src/Haal/Dot.hs +157/−48
• src/Haal/EquivalenceOracle/WMethod.hs +15/−3
• src/Haal/EquivalenceOracle/WpMethod.hs +33/−11
• src/Haal/Experiment.hs +136/−69
• src/Haal/Learning/LMstar.hs +14/−16
• src/Haal/Statistics.hs +151/−0
• test/AutomatonSpec.hs +94/−24
• test/DotSpec.hs +129/−0
• test/EquivalenceOracleSpec.hs +82/−17
• test/SULSpec.hs +141/−0
• test/StatisticsSpec.hs +99/−0
• test/Utils.hs +39/−33

@@ -6,7 +6,158 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). -## Unreleased+## 0.7.0.0 - 2026-10-10++This release replaces the built-in statistics with a general mechanism:+experiments report events, and statistics are folds over them. It also makes+`query` overridable, adds a way to compare automata, and removes the Moore and+DFA types. See "Migrating from 0.6" at the end of this entry.++### Added+- `query` is now a method of `Haal.BlackBox.SUL`, with the old behaviour+  (reset, then walk) as its default. A SUL can override it to answer a whole+  query at once, e.g. by sending the whole word in one message. The+  documentation of `query` lists what an override must guarantee.+- `Haal.BlackBox.queryChecked`: `query`, checking that the SUL returned exactly+  one output per input. The learners and oracles query through it, so an+  override that breaks this fails with a clear error instead of corrupting the+  observation table.+- `Haal.Statistics`, with the events an experiment reports (`Event`:+  `PhaseChanged`, `Queried`, `Hypothesis`, `Counterexample`, and `Phase`), the+  `Statistics` record and the `statistics` fold. `statistics` measures the+  membership queries and symbols sent while constructing hypotheses and while+  validating them, and records every hypothesis and counterexample. A+  statistic is a `Control.Foldl.Fold` over events, so statistics combine with+  `<*>` and users can define their own.+- `Haal.Experiment.experimentWith`: run an experiment, reporting every event+  to a monadic handler.+- `Haal.Experiment.measuredExperiment`: run an experiment and a fold over its+  events in one pass, returning the model and the fold's result.+- `Haal.BlackBox.difference`: a shortest input word on which two Mealy+  automata produce different outputs, or `Nothing` if they are equivalent.+- `MealyAutomaton` is a SUL in any monad, not only in `Identity`, so an+  automaton can be learned inside the monad that holds a user's own state.++### Changed (breaking)+- `Haal.Experiment.experiment` returns only the learned model, instead of the+  model and a `Statistics` record.+- `Haal.Experiment.Statistics` is removed; the new `Haal.Statistics.Statistics`+  record, measured with `measuredExperiment statistics`, replaces it. Its+  `hypotheses` include the final one; the number of rounds is+  `rounds stats`, and the number of equivalence queries is+  `length (hypotheses stats)`.+- `query` is a class method now, so a module that imports `SUL (..)` and+  defines its own top-level `query` gets an ambiguity error. Rename the local+  definition (the `io` example renames it to `askProgram`).+- New dependency: `foldl`.++### Removed+- `Haal.Automaton.MooreAutomaton` and `Haal.Automaton.DFA`. No learning+  algorithm in haal produces or uses Moore machines or DFAs, so supporting+  these types on their own was not useful, and their semantics had a known+  quirk (a step emitted the output of the state it left, not the one it+  reached). Support for more kinds of automata will come back properly in a+  future release, together with learning algorithms for them. To learn a DFA+  today, encode it as a Mealy machine with `Bool` outputs, where the output of+  a transition says whether the state it reaches is accepting.++### Migrating from 0.6++```haskell+-- 0.6+(model, stats) = runExperiment (experiment learner oracle) sul+-- statsRounds stats, statsCexs stats, statsHyps stats++-- 0.7: the model only+model = runExperiment (experiment learner oracle) sul++-- 0.7: the model and statistics+(model, stats) = runExperiment (measuredExperiment statistics learner oracle) sul+-- rounds stats, counterexamples stats, hypotheses stats (incl. the final one),+-- learning stats / testing stats: membership queries and symbols per phase++-- 0.7: your own statistics alongside, e.g. the number of events+import qualified Control.Foldl as L+(model, (stats, n)) = runExperiment (measuredExperiment ((,) <$> statistics <*> L.length) learner oracle) sul+```++## 0.6.1.1 - 2026-10-09++### Fixed+- The W-method and the Wp-method (and their random variants) did not test a+  hypothesis with a single state. Such a hypothesis has an empty characterizing+  set, so the W-method and the Wp-method generated no test words at all and+  accepted it without testing, at any depth, and the random Wp-method crashed+  with `Set.elemAt: index out of range`. This happens whenever no single input+  distinguishes the states of the SUL, so learning stopped after the first+  hypothesis with a wrong one-state model. Test words now end with the empty+  word when the characterizing set is empty, which still checks the outputs+  along the rest of the word.+- The second phase of the Wp-method started from the wrong prefixes: the state+  cover without the transition cover instead of the transition cover without+  the state cover. Depth `k` therefore only accounted for about `k - 1` extra+  states. Learned models can now be correct at a lower depth: on four+  `haal-models` protocol models, depth 1 now learns three of them correctly+  (before: none) and depth 2 all four (before: three).++## 0.6.1.0 - 2026-10-05++### Added+- `Haal.BlackBox.query` runs a single query: it resets the SUL, then walks it+  over the given inputs and returns the outputs.++### Fixed+- The SUL is now reset before every membership query and every equivalence+  test case. Before, queries only started from the initial state because the+  library kept returning to the same SUL value. That works for pure automata,+  but a SUL that wraps a stateful system (a running process, a socket) was+  queried from whatever state the previous query left it in, so learning could+  produce wrong models or never terminate. Learning from an automaton that is+  not in its initial state is fixed too.+- The documentation of `Haal.BlackBox.FiniteOrd` said `(Ord, Bounded)` instead+  of `(Ord, Finite)`.++### Changed+- Simplified the examples.++## 0.6.0.0 - 2026-10-03++### Added+- `Haal.Automaton.MealyAutomaton.mkMealyAutomatonTable` builds a Mealy+  automaton with states `0 .. n - 1` from a transition table and an output+  table, each encoded as a `String`, and validates both tables.+- `Haal.Dot.MealyTable` and `Haal.Dot.mealyTable` encode a `ParsedMealy` in+  that table form, rejecting automata with missing or conflicting+  transitions.++### Fixed+- `Haal.Dot.parseDot` again orders states, inputs, and outputs by first+  appearance, as documented. Since 0.5.0.0 it sorted them by name, which+  changed the constructor order and state numbering of generated modules.++### Changed (breaking)+- `Haal.Experiment.Learner` drops its state parameter (`Learner l aut`);+  learners now always produce automata with `Int` states.++### Changed+- `haal-gen` (`Haal.Dot.generateModule`) emits the transition and output+  functions as string-literal tables built with `mkMealyAutomatonTable`,+  instead of one equation per transition, and lists every transition in a+  comment. Generated modules have the same types and behaviour, but compile+  about 2-3 times faster. `generateModule` now rejects incomplete or+  nondeterministic automata, instead of generating functions that fail at+  runtime.+- `Haal.BlackBox.distinguish` returns `[]` immediately when both states are+  equal, instead of exploring the product automaton first. Results are+  unchanged. Its LiquidHaskell spec now states that equal states yield an+  empty word.++### Removed (breaking)+- `Haal.BlackBox.StateID` type alias. Learned automata use `Int` states+  directly, as `haal-gen` and `haal-models` already do; replace any use of+  `StateID` with `Int`.+- `Haal.Experiment.pairwiseWalk` and `Haal.Experiment.execute` are no longer+  exported; use `findCex` instead.  ## 0.5.0.0 - 2026-04-22 

@@ -123,7 +123,7 @@ ghci> mysul = mkMealyAutomaton2 sulTransitions (Set.fromList [S0, S1, S2]) S0  -- Run the experiment-ghci> (learnedmodel, stats) = runExperiment myexperiment mysul+ghci> learnedmodel = runExperiment myexperiment mysul  -- View the learned model ghci> learnedmodel

@@ -1,2 +1,3 @@ import Distribution.Simple+ main = defaultMain

@@ -1,37 +1,39 @@--- | haal-gen: generate a Haskell module from a Mealy automaton in DOT format.------ Usage:---   haal-gen <dotfile> <ModuleName> <valueName>------ The generated module is written to stdout.+{- | haal-gen: generate a Haskell module from a Mealy automaton in DOT format.++Usage:+  haal-gen <dotfile> <ModuleName> <valueName>++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)+import Haal.Dot (generateModule, parseDot, parsedWarnings)  helpText :: String-helpText = unlines-    [ "haal-gen - generate a Haskell module from a Mealy automaton in DOT format"-    , ""-    , "Usage:"-    , "  haal-gen <dotfile> <ModuleName> <valueName>"-    , ""-    , "Arguments:"-    , "  <dotfile>     Path to a DOT file (AALpy or LearnLib format)"-    , "  <ModuleName>  Fully qualified Haskell module name (e.g. My.Module.Name)"-    , "  <valueName>   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"-    ]+helpText =+    unlines+        [ "haal-gen - generate a Haskell module from a Mealy automaton in DOT format"+        , ""+        , "Usage:"+        , "  haal-gen <dotfile> <ModuleName> <valueName>"+        , ""+        , "Arguments:"+        , "  <dotfile>     Path to a DOT file (AALpy or LearnLib format)"+        , "  <ModuleName>  Fully qualified Haskell module name (e.g. My.Module.Name)"+        , "  <valueName>   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@@ -54,7 +56,7 @@         Right pm -> do             mapM_ (hPutStrLn stderr . ("haal-gen: warning: " ++)) (parsedWarnings pm)             case generateModule modName valName pm of-                Left err  -> do+                Left err -> do                     hPutStrLn stderr ("haal-gen: " ++ err)                     exitFailure                 Right hsrc -> putStr hsrc

@@ -3,9 +3,9 @@ module Bench.BlackBox (blackBoxBenchmarks) where  import Control.DeepSeq (NFData)-import GHC.Generics (Generic) import qualified Data.Map as Map import qualified Data.Set as Set+import GHC.Generics (Generic) import Test.Tasty.Bench (Benchmark, bench, bgroup, nf)  import Haal.Automaton.MealyAutomaton (MealyAutomaton, mkMealyAutomaton)@@ -13,14 +13,17 @@  -- | Input alphabet for benchmark automata. data In = IA | IB | IC | ID deriving (Show, Eq, Ord, Enum, Bounded, Generic)+ instance NFData In  -- | Output alphabet for benchmark automata. data Out = OX | OY | OZ | OW deriving (Show, Eq, Ord, Enum, Bounded, Generic)+ instance NFData Out  -- | States for benchmark automata. data St = S0 | S1 | S2 | S3 | S4 | S5 | S6 | S7 deriving (Show, Eq, Ord, Enum, Bounded, Generic)+ instance NFData St  -- | A deterministic 8-state Mealy automaton with fixed transitions.@@ -28,28 +31,56 @@ benchAutomaton = mkMealyAutomaton delta lambda (Set.fromList [S0 .. S7]) S0   where     transMap :: Map.Map (St, In) (St, Out)-    transMap = Map.fromList-        [ ((S0, IA), (S1, OX)), ((S0, IB), (S2, OY)), ((S0, IC), (S3, OZ)), ((S0, ID), (S4, OW))-        , ((S1, IA), (S5, OY)), ((S1, IB), (S0, OX)), ((S1, IC), (S6, OW)), ((S1, ID), (S7, OZ))-        , ((S2, IA), (S3, OZ)), ((S2, IB), (S4, OX)), ((S2, IC), (S7, OY)), ((S2, ID), (S1, OW))-        , ((S3, IA), (S6, OW)), ((S3, IB), (S5, OZ)), ((S3, IC), (S0, OX)), ((S3, ID), (S2, OY))-        , ((S4, IA), (S7, OX)), ((S4, IB), (S6, OW)), ((S4, IC), (S1, OY)), ((S4, ID), (S0, OZ))-        , ((S5, IA), (S2, OZ)), ((S5, IB), (S7, OY)), ((S5, IC), (S4, OX)), ((S5, ID), (S3, OW))-        , ((S6, IA), (S4, OY)), ((S6, IB), (S1, OX)), ((S6, IC), (S5, OZ)), ((S6, ID), (S0, OW))-        , ((S7, IA), (S0, OW)), ((S7, IB), (S3, OZ)), ((S7, IC), (S2, OY)), ((S7, ID), (S6, OX))-        ]+    transMap =+        Map.fromList+            [ ((S0, IA), (S1, OX))+            , ((S0, IB), (S2, OY))+            , ((S0, IC), (S3, OZ))+            , ((S0, ID), (S4, OW))+            , ((S1, IA), (S5, OY))+            , ((S1, IB), (S0, OX))+            , ((S1, IC), (S6, OW))+            , ((S1, ID), (S7, OZ))+            , ((S2, IA), (S3, OZ))+            , ((S2, IB), (S4, OX))+            , ((S2, IC), (S7, OY))+            , ((S2, ID), (S1, OW))+            , ((S3, IA), (S6, OW))+            , ((S3, IB), (S5, OZ))+            , ((S3, IC), (S0, OX))+            , ((S3, ID), (S2, OY))+            , ((S4, IA), (S7, OX))+            , ((S4, IB), (S6, OW))+            , ((S4, IC), (S1, OY))+            , ((S4, ID), (S0, OZ))+            , ((S5, IA), (S2, OZ))+            , ((S5, IB), (S7, OY))+            , ((S5, IC), (S4, OX))+            , ((S5, ID), (S3, OW))+            , ((S6, IA), (S4, OY))+            , ((S6, IB), (S1, OX))+            , ((S6, IC), (S5, OZ))+            , ((S6, ID), (S0, OW))+            , ((S7, IA), (S0, OW))+            , ((S7, IB), (S3, OZ))+            , ((S7, IC), (S2, OY))+            , ((S7, ID), (S6, OX))+            ]      delta s i = fst (transMap Map.! (s, i))     lambda s i = snd (transMap Map.! (s, i))  blackBoxBenchmarks :: Benchmark-blackBoxBenchmarks = bgroup "BlackBox"-    [ bgroup "8-state"-        [ bench "reachable" $ nf reachable benchAutomaton-        , bench "accessSequences" $ nf accessSequences benchAutomaton-        , bench "globalCharacterizingSet" $ nf globalCharacterizingSet benchAutomaton-        , bench "localCharacterizingSet/S0" $ nf (localCharacterizingSet benchAutomaton) S0-        , bench "distinguish/S0-S1" $ nf (distinguish benchAutomaton S0) S1-        , bench "distinguish/S0-S7" $ nf (distinguish benchAutomaton S0) S7+blackBoxBenchmarks =+    bgroup+        "BlackBox"+        [ bgroup+            "8-state"+            [ bench "reachable" $ nf reachable benchAutomaton+            , bench "accessSequences" $ nf accessSequences benchAutomaton+            , bench "globalCharacterizingSet" $ nf globalCharacterizingSet benchAutomaton+            , bench "localCharacterizingSet/S0" $ nf (localCharacterizingSet benchAutomaton) S0+            , bench "distinguish/S0-S1" $ nf (distinguish benchAutomaton S0) S1+            , bench "distinguish/S0-S7" $ nf (distinguish benchAutomaton S0) S7+            ]         ]-    ]

@@ -4,9 +4,9 @@ module Bench.Dot (dotBenchmarks) where  import Control.DeepSeq (NFData (rnf))-import GHC.Generics (Generic) import qualified Data.Map as Map import qualified Data.Set as Set+import GHC.Generics (Generic) import Test.Tasty.Bench (Benchmark, bench, bgroup, nf)  import Haal.Automaton.MealyAutomaton (MealyAutomaton, mkMealyAutomaton)@@ -14,14 +14,17 @@  -- | Input alphabet for benchmark automata. data In = IA | IB | IC | ID deriving (Show, Eq, Ord, Enum, Bounded, Generic)+ instance NFData In  -- | Output alphabet for benchmark automata. data Out = OX | OY | OZ | OW deriving (Show, Eq, Ord, Enum, Bounded, Generic)+ instance NFData Out  -- | States for benchmark automata. data St = S0 | S1 | S2 | S3 | S4 | S5 | S6 | S7 deriving (Show, Eq, Ord, Enum, Bounded, Generic)+ instance NFData St  instance NFData ParsedMealy where@@ -32,16 +35,41 @@ benchAutomaton = mkMealyAutomaton delta lambda (Set.fromList [S0 .. S7]) S0   where     transMap :: Map.Map (St, In) (St, Out)-    transMap = Map.fromList-        [ ((S0, IA), (S1, OX)), ((S0, IB), (S2, OY)), ((S0, IC), (S3, OZ)), ((S0, ID), (S4, OW))-        , ((S1, IA), (S5, OY)), ((S1, IB), (S0, OX)), ((S1, IC), (S6, OW)), ((S1, ID), (S7, OZ))-        , ((S2, IA), (S3, OZ)), ((S2, IB), (S4, OX)), ((S2, IC), (S7, OY)), ((S2, ID), (S1, OW))-        , ((S3, IA), (S6, OW)), ((S3, IB), (S5, OZ)), ((S3, IC), (S0, OX)), ((S3, ID), (S2, OY))-        , ((S4, IA), (S7, OX)), ((S4, IB), (S6, OW)), ((S4, IC), (S1, OY)), ((S4, ID), (S0, OZ))-        , ((S5, IA), (S2, OZ)), ((S5, IB), (S7, OY)), ((S5, IC), (S4, OX)), ((S5, ID), (S3, OW))-        , ((S6, IA), (S4, OY)), ((S6, IB), (S1, OX)), ((S6, IC), (S5, OZ)), ((S6, ID), (S0, OW))-        , ((S7, IA), (S0, OW)), ((S7, IB), (S3, OZ)), ((S7, IC), (S2, OY)), ((S7, ID), (S6, OX))-        ]+    transMap =+        Map.fromList+            [ ((S0, IA), (S1, OX))+            , ((S0, IB), (S2, OY))+            , ((S0, IC), (S3, OZ))+            , ((S0, ID), (S4, OW))+            , ((S1, IA), (S5, OY))+            , ((S1, IB), (S0, OX))+            , ((S1, IC), (S6, OW))+            , ((S1, ID), (S7, OZ))+            , ((S2, IA), (S3, OZ))+            , ((S2, IB), (S4, OX))+            , ((S2, IC), (S7, OY))+            , ((S2, ID), (S1, OW))+            , ((S3, IA), (S6, OW))+            , ((S3, IB), (S5, OZ))+            , ((S3, IC), (S0, OX))+            , ((S3, ID), (S2, OY))+            , ((S4, IA), (S7, OX))+            , ((S4, IB), (S6, OW))+            , ((S4, IC), (S1, OY))+            , ((S4, ID), (S0, OZ))+            , ((S5, IA), (S2, OZ))+            , ((S5, IB), (S7, OY))+            , ((S5, IC), (S4, OX))+            , ((S5, ID), (S3, OW))+            , ((S6, IA), (S4, OY))+            , ((S6, IB), (S1, OX))+            , ((S6, IC), (S5, OZ))+            , ((S6, ID), (S0, OW))+            , ((S7, IA), (S0, OW))+            , ((S7, IB), (S3, OZ))+            , ((S7, IC), (S2, OY))+            , ((S7, ID), (S6, OX))+            ]      delta s i = fst (transMap Map.! (s, i))     lambda s i = snd (transMap Map.! (s, i))@@ -53,8 +81,10 @@     Left err -> error ("benchDotString: " ++ err)  dotBenchmarks :: Benchmark-dotBenchmarks = bgroup "Dot"-    [ bench "mealyToDot/8-state" $ nf mealyToDot benchAutomaton-    , bench "parseDot/8-state" $ nf parseDot benchDotString-    , bench "roundtrip/8-state" $ nf (parseDot . either error id . mealyToDot) benchAutomaton-    ]+dotBenchmarks =+    bgroup+        "Dot"+        [ bench "mealyToDot/8-state" $ nf mealyToDot benchAutomaton+        , bench "parseDot/8-state" $ nf parseDot benchDotString+        , bench "roundtrip/8-state" $ nf (parseDot . either error id . mealyToDot) benchAutomaton+        ]

@@ -3,9 +3,9 @@ module Bench.EndToEnd (endToEndBenchmarks) where  import Control.DeepSeq (NFData)-import GHC.Generics (Generic) import qualified Data.Map as Map import qualified Data.Set as Set+import GHC.Generics (Generic) import Test.Tasty.Bench (Benchmark, bench, bgroup, whnf)  import Haal.Automaton.MealyAutomaton (MealyAutomaton, mkMealyAutomaton)@@ -16,14 +16,17 @@  -- | Input alphabet for benchmark automata. data In = IA | IB | IC | ID deriving (Show, Eq, Ord, Enum, Bounded, Generic)+ instance NFData In  -- | Output alphabet for benchmark automata. data Out = OX | OY | OZ | OW deriving (Show, Eq, Ord, Enum, Bounded, Generic)+ instance NFData Out  -- | States for the SUL (target automaton). data St = S0 | S1 | S2 | S3 | S4 | S5 | S6 | S7 deriving (Show, Eq, Ord, Enum, Bounded, Generic)+ instance NFData St  -- | A deterministic 8-state Mealy automaton used as the SUL.@@ -31,16 +34,41 @@ benchAutomaton = mkMealyAutomaton delta lambda (Set.fromList [S0 .. S7]) S0   where     transMap :: Map.Map (St, In) (St, Out)-    transMap = Map.fromList-        [ ((S0, IA), (S1, OX)), ((S0, IB), (S2, OY)), ((S0, IC), (S3, OZ)), ((S0, ID), (S4, OW))-        , ((S1, IA), (S5, OY)), ((S1, IB), (S0, OX)), ((S1, IC), (S6, OW)), ((S1, ID), (S7, OZ))-        , ((S2, IA), (S3, OZ)), ((S2, IB), (S4, OX)), ((S2, IC), (S7, OY)), ((S2, ID), (S1, OW))-        , ((S3, IA), (S6, OW)), ((S3, IB), (S5, OZ)), ((S3, IC), (S0, OX)), ((S3, ID), (S2, OY))-        , ((S4, IA), (S7, OX)), ((S4, IB), (S6, OW)), ((S4, IC), (S1, OY)), ((S4, ID), (S0, OZ))-        , ((S5, IA), (S2, OZ)), ((S5, IB), (S7, OY)), ((S5, IC), (S4, OX)), ((S5, ID), (S3, OW))-        , ((S6, IA), (S4, OY)), ((S6, IB), (S1, OX)), ((S6, IC), (S5, OZ)), ((S6, ID), (S0, OW))-        , ((S7, IA), (S0, OW)), ((S7, IB), (S3, OZ)), ((S7, IC), (S2, OY)), ((S7, ID), (S6, OX))-        ]+    transMap =+        Map.fromList+            [ ((S0, IA), (S1, OX))+            , ((S0, IB), (S2, OY))+            , ((S0, IC), (S3, OZ))+            , ((S0, ID), (S4, OW))+            , ((S1, IA), (S5, OY))+            , ((S1, IB), (S0, OX))+            , ((S1, IC), (S6, OW))+            , ((S1, ID), (S7, OZ))+            , ((S2, IA), (S3, OZ))+            , ((S2, IB), (S4, OX))+            , ((S2, IC), (S7, OY))+            , ((S2, ID), (S1, OW))+            , ((S3, IA), (S6, OW))+            , ((S3, IB), (S5, OZ))+            , ((S3, IC), (S0, OX))+            , ((S3, ID), (S2, OY))+            , ((S4, IA), (S7, OX))+            , ((S4, IB), (S6, OW))+            , ((S4, IC), (S1, OY))+            , ((S4, ID), (S0, OZ))+            , ((S5, IA), (S2, OZ))+            , ((S5, IB), (S7, OY))+            , ((S5, IC), (S4, OX))+            , ((S5, ID), (S3, OW))+            , ((S6, IA), (S4, OY))+            , ((S6, IB), (S1, OX))+            , ((S6, IC), (S5, OZ))+            , ((S6, ID), (S0, OW))+            , ((S7, IA), (S0, OW))+            , ((S7, IB), (S3, OZ))+            , ((S7, IC), (S2, OY))+            , ((S7, ID), (S6, OX))+            ]      delta s i = fst (transMap Map.! (s, i))     lambda s i = snd (transMap Map.! (s, i))@@ -51,20 +79,25 @@ wpmethod :: Int -> WpMethod wpmethod d = either error id (mkWpMethod (WpMethodConfig d)) --- | Run a full learning experiment (init -> learn -> test -> refine -> converge).--- Uses whnf since MealyAutomaton contains functions that cannot be NFData.+{- | Run a full learning experiment (init -> learn -> test -> refine -> converge).+Uses whnf since MealyAutomaton contains functions that cannot be NFData.+-} endToEndBenchmarks :: Benchmark-endToEndBenchmarks = bgroup "EndToEnd"-    [ bgroup "LMstar"-        [ bench "WMethod/depth=1" $-            whnf (runExperiment (experiment (mkLMstar Star) (wmethod 1))) benchAutomaton-        , bench "WpMethod/depth=1" $-            whnf (runExperiment (experiment (mkLMstar Star) (wpmethod 1))) benchAutomaton-        ]-    , bgroup "LMplus"-        [ bench "WMethod/depth=1" $-            whnf (runExperiment (experiment (mkLMstar Plus) (wmethod 1))) benchAutomaton-        , bench "WpMethod/depth=1" $-            whnf (runExperiment (experiment (mkLMstar Plus) (wpmethod 1))) benchAutomaton+endToEndBenchmarks =+    bgroup+        "EndToEnd"+        [ bgroup+            "LMstar"+            [ bench "WMethod/depth=1" $+                whnf (runExperiment (experiment (mkLMstar Star) (wmethod 1))) benchAutomaton+            , bench "WpMethod/depth=1" $+                whnf (runExperiment (experiment (mkLMstar Star) (wpmethod 1))) benchAutomaton+            ]+        , bgroup+            "LMplus"+            [ bench "WMethod/depth=1" $+                whnf (runExperiment (experiment (mkLMstar Plus) (wmethod 1))) benchAutomaton+            , bench "WpMethod/depth=1" $+                whnf (runExperiment (experiment (mkLMstar Plus) (wpmethod 1))) benchAutomaton+            ]         ]-    ]

@@ -3,9 +3,9 @@ module Bench.EquivalenceOracle (equivalenceOracleBenchmarks) where  import Control.DeepSeq (NFData)-import GHC.Generics (Generic) import qualified Data.Map as Map import qualified Data.Set as Set+import GHC.Generics (Generic) import Test.Tasty.Bench (Benchmark, bench, bgroup, nf)  import Haal.Automaton.MealyAutomaton (MealyAutomaton, mkMealyAutomaton)@@ -15,14 +15,17 @@  -- | Input alphabet for benchmark automata. data In = IA | IB | IC | ID deriving (Show, Eq, Ord, Enum, Bounded, Generic)+ instance NFData In  -- | Output alphabet for benchmark automata. data Out = OX | OY | OZ | OW deriving (Show, Eq, Ord, Enum, Bounded, Generic)+ instance NFData Out  -- | States for benchmark automata. data St = S0 | S1 | S2 | S3 | S4 | S5 | S6 | S7 deriving (Show, Eq, Ord, Enum, Bounded, Generic)+ instance NFData St  -- | A deterministic 8-state Mealy automaton with fixed transitions.@@ -30,16 +33,41 @@ benchAutomaton = mkMealyAutomaton delta lambda (Set.fromList [S0 .. S7]) S0   where     transMap :: Map.Map (St, In) (St, Out)-    transMap = Map.fromList-        [ ((S0, IA), (S1, OX)), ((S0, IB), (S2, OY)), ((S0, IC), (S3, OZ)), ((S0, ID), (S4, OW))-        , ((S1, IA), (S5, OY)), ((S1, IB), (S0, OX)), ((S1, IC), (S6, OW)), ((S1, ID), (S7, OZ))-        , ((S2, IA), (S3, OZ)), ((S2, IB), (S4, OX)), ((S2, IC), (S7, OY)), ((S2, ID), (S1, OW))-        , ((S3, IA), (S6, OW)), ((S3, IB), (S5, OZ)), ((S3, IC), (S0, OX)), ((S3, ID), (S2, OY))-        , ((S4, IA), (S7, OX)), ((S4, IB), (S6, OW)), ((S4, IC), (S1, OY)), ((S4, ID), (S0, OZ))-        , ((S5, IA), (S2, OZ)), ((S5, IB), (S7, OY)), ((S5, IC), (S4, OX)), ((S5, ID), (S3, OW))-        , ((S6, IA), (S4, OY)), ((S6, IB), (S1, OX)), ((S6, IC), (S5, OZ)), ((S6, ID), (S0, OW))-        , ((S7, IA), (S0, OW)), ((S7, IB), (S3, OZ)), ((S7, IC), (S2, OY)), ((S7, ID), (S6, OX))-        ]+    transMap =+        Map.fromList+            [ ((S0, IA), (S1, OX))+            , ((S0, IB), (S2, OY))+            , ((S0, IC), (S3, OZ))+            , ((S0, ID), (S4, OW))+            , ((S1, IA), (S5, OY))+            , ((S1, IB), (S0, OX))+            , ((S1, IC), (S6, OW))+            , ((S1, ID), (S7, OZ))+            , ((S2, IA), (S3, OZ))+            , ((S2, IB), (S4, OX))+            , ((S2, IC), (S7, OY))+            , ((S2, ID), (S1, OW))+            , ((S3, IA), (S6, OW))+            , ((S3, IB), (S5, OZ))+            , ((S3, IC), (S0, OX))+            , ((S3, ID), (S2, OY))+            , ((S4, IA), (S7, OX))+            , ((S4, IB), (S6, OW))+            , ((S4, IC), (S1, OY))+            , ((S4, ID), (S0, OZ))+            , ((S5, IA), (S2, OZ))+            , ((S5, IB), (S7, OY))+            , ((S5, IC), (S4, OX))+            , ((S5, ID), (S3, OW))+            , ((S6, IA), (S4, OY))+            , ((S6, IB), (S1, OX))+            , ((S6, IC), (S5, OZ))+            , ((S6, ID), (S0, OW))+            , ((S7, IA), (S0, OW))+            , ((S7, IB), (S3, OZ))+            , ((S7, IC), (S2, OY))+            , ((S7, ID), (S6, OX))+            ]      delta s i = fst (transMap Map.! (s, i))     lambda s i = snd (transMap Map.! (s, i))@@ -51,29 +79,37 @@ wpmethod d = either error id (mkWpMethod (WpMethodConfig d))  equivalenceOracleBenchmarks :: Benchmark-equivalenceOracleBenchmarks = bgroup "EquivalenceOracle"-    [ bgroup "WMethod"-        [ bgroup "testSuite"-            [ bench "depth=1" $ nf (\w -> snd (testSuite w benchAutomaton)) (wmethod 1)-            , bench "depth=2" $ nf (\w -> snd (testSuite w benchAutomaton)) (wmethod 2)-            , bench "depth=3" $ nf (\w -> snd (testSuite w benchAutomaton)) (wmethod 3)-            ]-        , bgroup "suiteSize"-            [ bench "depth=1" $ nf (\w -> wmethodSuiteSize w benchAutomaton) (wmethod 1)-            , bench "depth=2" $ nf (\w -> wmethodSuiteSize w benchAutomaton) (wmethod 2)-            , bench "depth=3" $ nf (\w -> wmethodSuiteSize w benchAutomaton) (wmethod 3)-            ]-        ]-    , bgroup "WpMethod"-        [ bgroup "testSuite"-            [ bench "depth=1" $ nf (\w -> snd (testSuite w benchAutomaton)) (wpmethod 1)-            , bench "depth=2" $ nf (\w -> snd (testSuite w benchAutomaton)) (wpmethod 2)-            , bench "depth=3" $ nf (\w -> snd (testSuite w benchAutomaton)) (wpmethod 3)+equivalenceOracleBenchmarks =+    bgroup+        "EquivalenceOracle"+        [ bgroup+            "WMethod"+            [ bgroup+                "testSuite"+                [ bench "depth=1" $ nf (\w -> snd (testSuite w benchAutomaton)) (wmethod 1)+                , bench "depth=2" $ nf (\w -> snd (testSuite w benchAutomaton)) (wmethod 2)+                , bench "depth=3" $ nf (\w -> snd (testSuite w benchAutomaton)) (wmethod 3)+                ]+            , bgroup+                "suiteSize"+                [ bench "depth=1" $ nf (\w -> wmethodSuiteSize w benchAutomaton) (wmethod 1)+                , bench "depth=2" $ nf (\w -> wmethodSuiteSize w benchAutomaton) (wmethod 2)+                , bench "depth=3" $ nf (\w -> wmethodSuiteSize w benchAutomaton) (wmethod 3)+                ]             ]-        , bgroup "suiteSize"-            [ bench "depth=1" $ nf (\w -> wpmethodSuiteSize w benchAutomaton) (wpmethod 1)-            , bench "depth=2" $ nf (\w -> wpmethodSuiteSize w benchAutomaton) (wpmethod 2)-            , bench "depth=3" $ nf (\w -> wpmethodSuiteSize w benchAutomaton) (wpmethod 3)+        , bgroup+            "WpMethod"+            [ bgroup+                "testSuite"+                [ bench "depth=1" $ nf (\w -> snd (testSuite w benchAutomaton)) (wpmethod 1)+                , bench "depth=2" $ nf (\w -> snd (testSuite w benchAutomaton)) (wpmethod 2)+                , bench "depth=3" $ nf (\w -> snd (testSuite w benchAutomaton)) (wpmethod 3)+                ]+            , bgroup+                "suiteSize"+                [ bench "depth=1" $ nf (\w -> wpmethodSuiteSize w benchAutomaton) (wpmethod 1)+                , bench "depth=2" $ nf (\w -> wpmethodSuiteSize w benchAutomaton) (wpmethod 2)+                , bench "depth=3" $ nf (\w -> wpmethodSuiteSize w benchAutomaton) (wpmethod 3)+                ]             ]         ]-    ]

@@ -8,9 +8,10 @@ import Bench.EquivalenceOracle (equivalenceOracleBenchmarks)  main :: IO ()-main = defaultMain-    [ blackBoxBenchmarks-    , equivalenceOracleBenchmarks-    , dotBenchmarks-    , endToEndBenchmarks-    ]+main =+    defaultMain+        [ blackBoxBenchmarks+        , equivalenceOracleBenchmarks+        , dotBenchmarks+        , endToEndBenchmarks+        ]

@@ -5,6 +5,7 @@ import Haal.EquivalenceOracle.WMethod import Haal.Experiment import Haal.Learning.LMstar+import Haal.Statistics (statistics)  -- Define input, output, and state types data Input = A | B deriving (Show, Eq, Ord, Enum, Bounded)@@ -23,7 +24,7 @@     Right oracle' -> oracle'  -- Set up the experiment.-myexperiment = experiment learner oracle+myexperiment = measuredExperiment statistics learner oracle  -- Define the Mealy system under learning. Remember that automata can act as suls. mysul = mkMealyAutomaton2 sulTransitions (Set.fromList [S0, S1, S2]) S0

@@ -1,12 +1,13 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} +import Control.Monad.Identity (Identity) import Haal.Automaton.MealyAutomaton-import Haal.BlackBox (SUL (..), StateID)+import Haal.BlackBox (SUL (..)) import Haal.EquivalenceOracle.WpMethod (WpMethod, WpMethodConfig (..), mkWpMethod) import Haal.Experiment import Haal.Learning.LMstar (LMstar, LMstarConfig (Star), mkLMstar)-import Control.Monad.Identity (Identity)+import Haal.Statistics (Statistics, statistics)  -- main logic divisible :: Integer -> Bool@@ -83,15 +84,15 @@ learner = mkLMstar Star  oracle :: WpMethod-oracle = case mkWpMethod (WpMethodConfig 3) of -    Left msg -> error msg +oracle = case mkWpMethod (WpMethodConfig 3) of+    Left msg -> error msg     Right oracle' -> oracle' -exper :: Experiment (Program Binary Bool) (MealyAutomaton StateID Binary Bool, Statistics MealyAutomaton StateID Binary Bool)-exper = experiment learner oracle+exper :: ExperimentT (Program Binary Bool) Identity (MealyAutomaton Int Binary Bool, Statistics MealyAutomaton Binary Bool)+exper = measuredExperiment statistics learner oracle -theModel :: MealyAutomaton StateID Binary Bool-theStats :: Statistics MealyAutomaton StateID Binary Bool+theModel :: MealyAutomaton Int Binary Bool+theStats :: Statistics MealyAutomaton Binary Bool (theModel, theStats) = runExperiment exper sul  main :: IO ()

@@ -1,108 +1,59 @@ -- we will attempt to reproduce the `div.hs` learning experiment, -- but this time, instead of using a haskell function as a SUL,--- we will use an actual program that performs IO, whose input and--- output alphabet we know.--- the output alphabet is just bool--- the input alphabet is binary+-- we will use an actual program that performs IO.+-- the program reads an integer from stdin and prints whether it is+-- divisible by 3, so its output alphabet is just bool.+-- the input alphabet is binary, as in `div.hs`. {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} -import Data.Functor ((<&>))-import Haal.Automaton.MealyAutomaton-import Haal.BlackBox-import Haal.EquivalenceOracle.WpMethod-import Haal.Experiment-import Haal.Learning.LMstar+import Haal.BlackBox (SUL (..))+import Haal.EquivalenceOracle.WpMethod (WpMethodConfig (..), mkWpMethod)+import Haal.Experiment (measuredExperiment, runExperimentT)+import Haal.Learning.LMstar (LMstarConfig (Star), mkLMstar)+import Haal.Statistics (statistics) import System.Process (readProcess)  -- Note that this is relative to the project root. Otherwise--- the executable will not be found-source :: String+-- the executable will not be found. Build it first with+--   ghc examples/divisible3.hs+source :: FilePath source = "./examples/divisible3" -inputMap :: Int -> String-inputMap num = show num ++ "\n"--innerQuery :: String -> IO String-innerQuery = readProcess source []--outputMap :: String -> Bool-outputMap = read--query :: Int -> IO Bool-query = (<&> outputMap) . innerQuery . inputMap- data Binary = B0 | B1 deriving (Show, Eq, Ord, Enum, Bounded) --- now we are in the position to use binary digits to construct integers.--- we need a mapper that maps from binary digits to integers that the program can actually use+-- the bits seen so far are read as a binary number, most significant+-- bit first. the history is stored newest bit first, so the head of the+-- list is the least significant bit.+convert :: [Binary] -> Integer+convert = foldr (\b acc -> toInteger (fromEnum b) + 2 * acc) 0 -convert :: (Num a) => [Binary] -> a-convert [] = 0-convert [B0] = 0-convert [B1] = 1-convert (b : bs) = convert [b] + 2 * convert bs+-- ask the external program about the number the bits represent+askProgram :: [Binary] -> IO Bool+askProgram bits = read <$> readProcess source [] (show (convert bits) ++ "\n") --- this time, in contrast to div.hs, a Program performs IO actions,--- instead of purely returning the computes values-data Program i o = Program-    { theStep :: i -> IO (Program i o, o)-    , theReset :: IO (Program i o)-    , buffer :: [i]-    }+-- the program itself is stateless, so the SUL keeps the inputs it has+-- received since the last reset and queries the program with all of them+-- on every step.+data Program i o = Program ([i] -> IO o) [i]  instance SUL Program IO where-    step = theStep-    reset = theReset--wrapped :: [Binary] -> IO Bool-wrapped = query . convert--mkProg :: [Binary] -> Program Binary Bool-mkProg buf =-    Program-        { theStep = \x -> do-            let newBuf = x : buf-            o <- wrapped newBuf-            return (mkProg newBuf, o)-        , theReset = return (mkProg [])-        , buffer = buf-        }+    step (Program f buf) x = do+        let buf' = x : buf+        o <- f buf'+        return (Program f buf', o)+    reset (Program f _) = return (Program f []) --- construct a sul with an empty buffer sul :: Program Binary Bool-sul = mkProg []--learner :: LMstar Binary Bool-learner = mkLMstar Star--oracle :: WpMethod-oracle = case mkWpMethod (WpMethodConfig 3) of -    Left msg -> error msg -    Right oracle' -> oracle'--exper ::-    ExperimentT-        (Program Binary Bool)-        IO-        ( MealyAutomaton-            StateID-            Binary-            Bool-        , Statistics-            MealyAutomaton-            StateID-            Binary-            Bool-        )-exper = experiment learner oracle-+sul = Program askProgram []  main :: IO () main = do-    (theModel, theStats) <- runExperimentT exper sul+    oracle <- either fail return (mkWpMethod (WpMethodConfig 3))+    let learner = mkLMstar Star+    (theModel, theStats) <- runExperimentT (measuredExperiment statistics learner oracle) sul     putStrLn "Learning Experiment"     putStrLn "==================="-    putStrLn "System Under Learning: \\x -> x `mod` 3 == 0"+    putStrLn "System Under Learning: ./examples/divisible3"     putStrLn $ "Learned Model: " ++ show theModel     putStrLn $ "Experiment Statistics: " ++ show theStats

@@ -3,7 +3,7 @@  import qualified Data.List as List import Haal.BlackBox-import Haal.EquivalenceOracle.WMethod (WMethodConfig (..), mkWMethod)+import Haal.EquivalenceOracle.WpMethod import Haal.Experiment import Haal.Learning.LMstar import System.Process (readProcess)@@ -85,8 +85,8 @@ --------------------------------------------------------------------------------  learner = mkLMstar Star-teacher = case mkWMethod (WMethodConfig 2) of -    Left msg -> error msg +teacher = case mkWpMethod (WpMethodConfig 1) of+    Left msg -> error msg     Right oracle -> oracle exper = experiment learner teacher @@ -110,5 +110,5 @@                 , notFound = NotFoundTag                 } ::                 WebsiteSUL Page PageTag-    (model, _) <- runExperimentT exper website+    model <- runExperimentT exper website     putStrLn $ "Learned Model: " ++ show model

@@ -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.38.0. -- -- see: https://github.com/sol/hpack  name:           haal-version:        0.5.0.0+version:        0.7.0.0 synopsis:       A Haskell library for Active Automata Learning. description:    Please see the README on GitHub at <https://github.com/steve-anunknown/haal#readme> category:       Model Learning@@ -33,9 +33,7 @@  library   exposed-modules:-      Haal.Automaton.DFA       Haal.Automaton.MealyAutomaton-      Haal.Automaton.MooreAutomaton       Haal.BlackBox       Haal.Dot       Haal.EquivalenceOracle.CombinedOracle@@ -45,6 +43,7 @@       Haal.EquivalenceOracle.WpMethod       Haal.Experiment       Haal.Learning.LMstar+      Haal.Statistics   other-modules:       Paths_haal   autogen-modules:@@ -55,6 +54,7 @@   build-depends:       base >=4.18.3 && <5     , containers >=0.6.7 && <0.8+    , foldl >=1.4.18 && <1.5     , mtl >=2.3.1 && <2.4     , random >=1.3.1 && <1.4     , vector >=0.13.2 && <0.14@@ -144,7 +144,10 @@   main-is: Spec.hs   other-modules:       AutomatonSpec+      DotSpec       EquivalenceOracleSpec+      StatisticsSpec+      SULSpec       Utils       Paths_haal   autogen-modules:@@ -156,6 +159,7 @@       QuickCheck     , base >=4.18.3 && <5     , containers+    , foldl     , haal     , hspec     , mtl

@@ -1,20 +0,0 @@-{-# LANGUAGE ScopedTypeVariables #-}-{-# OPTIONS_GHC -Wno-missing-export-lists #-}-{-# OPTIONS_GHC -Wno-unused-top-binds #-}---- | This module implements a simple deterministic finite automaton (DFA).-module Haal.Automaton.DFA (-    DFA,-    mkDFA,-)-where--import qualified Data.Set as Set-import Haal.Automaton.MooreAutomaton---- | 'DFA' is just a synonym for a 'MooreAutomaton' with 'Bool' type of output'.-type DFA state input = MooreAutomaton state input Bool---- | Constructor for a 'DFA' value.-mkDFA :: (s -> i -> s) -> (s -> Bool) -> Set.Set s -> s -> DFA s i-mkDFA = mkMooreAutomaton

@@ -7,16 +7,18 @@     MealyAutomaton,     mkMealyAutomaton,     mkMealyAutomaton2,+    mkMealyAutomatonTable,     mealyDelta,     mealyLambda,     mealyTransitions, ) where +import Data.Char (ord) import qualified Data.Map as Map import qualified Data.Set as Set+import qualified Data.Vector.Unboxed as VU import Haal.BlackBox-import Control.Monad.Identity (Identity)  {- | The 'MealyAutomaton' data type is parameterised by the @input@, @output@ and @state@ types  which play the role of the input alphabet, output alphabet and set of states respectively.@@ -60,6 +62,80 @@         , mealyStates = sts         } +{- | The 'mkMealyAutomatonTable' constructor returns a 'MealyAutomaton' with states+@0 .. n - 1@ from a transition table and an output table, each encoded as a 'String'+in which every 'Char' stands for the number @'ord' c@.++  @mkMealyAutomatonTable n initS deltaTable lambdaTable@ expects both tables to hold+  one entry per state and input, in row-major order: the entry at position+  @s * k + j@, where @k@ is the number of inputs and @j@ is the position of the input+  in @[minBound .. maxBound]@, describes state @s@ on that input. An entry of+  @deltaTable@ is the next state, and an entry of @lambdaTable@ is the position of+  the output in @[minBound .. maxBound]@.++  String literals compile far faster than large pattern matches, which is why+  @haal-gen@ emits its models in this form.++  Returns @'Left' err@ if the number of states is not positive, the initial state is+  out of range, a table has the wrong length, or an entry is out of range. Applying+  the resulting transition functions to a state outside @0 .. n - 1@ is an error.+-}+{-# INLINEABLE mkMealyAutomatonTable #-}+mkMealyAutomatonTable ::+    forall i o.+    (Finite i, Finite o) =>+    Int ->+    Int ->+    String ->+    String ->+    Either String (MealyAutomaton Int i o)+mkMealyAutomatonTable n initS deltaTable lambdaTable = do+    -- Only this wrapper is specialised at each use site (it is INLINABLE), so+    -- that lookups call 'fromEnum' and 'toEnum' directly rather than through+    -- a dictionary. Everything else happens in the monomorphic+    -- 'decodeTables', which keeps the specialised code, and therefore the+    -- compile time of each generated model, small.+    (sts, deltaV, lambdaV) <- decodeTables n numI numO initS deltaTable lambdaTable+    let index s i = s * numI + (fromEnum i - firstI)+        delta s i = deltaV VU.! index s i+        lambda s i = toEnum (firstO + lambdaV VU.! index s i)+    return (mkMealyAutomaton delta lambda sts initS)+  where+    firstI = fromEnum (minBound :: i)+    numI = fromEnum (maxBound :: i) - firstI + 1+    firstO = fromEnum (minBound :: o)+    numO = fromEnum (maxBound :: o) - firstO + 1++{- | Validate and decode the tables of 'mkMealyAutomatonTable', given the+number of states, inputs, and outputs and the initial state.+-}+{-# NOINLINE decodeTables #-}+decodeTables ::+    Int ->+    Int ->+    Int ->+    Int ->+    String ->+    String ->+    Either String (Set.Set Int, VU.Vector Int, VU.Vector Int)+decodeTables n numI numO initS deltaTable lambdaTable+    | n <= 0 = Left "the automaton must have at least one state"+    | initS < 0 || initS >= n =+        Left ("initial state " ++ show initS ++ " is not in 0 .. " ++ show (n - 1))+    | VU.length deltaV /= size =+        Left ("transition table has " ++ show (VU.length deltaV) ++ " entries, expected " ++ show size)+    | VU.length lambdaV /= size =+        Left ("output table has " ++ show (VU.length lambdaV) ++ " entries, expected " ++ show size)+    | VU.any (>= n) deltaV =+        Left "transition table refers to a state that does not exist"+    | VU.any (>= numO) lambdaV =+        Left "output table refers to an output that does not exist"+    | otherwise = Right (Set.fromDistinctAscList [0 .. n - 1], deltaV, lambdaV)+  where+    size = n * numI+    deltaV = VU.fromList (map ord deltaTable)+    lambdaV = VU.fromList (map ord lambdaTable)+ {- | Performs a step in the automaton and returns a tuple containing the automaton with a modified state as well as the output produced by the transition. -}@@ -73,7 +149,12 @@ mealyReset :: MealyAutomaton s i o -> MealyAutomaton s i o mealyReset m = m{mealyCurrentS = mealyInitialS m} -instance SUL (MealyAutomaton s) Identity where+{- | An automaton is a SUL in any monad. Stepping it is pure, so it never uses+the monad; this lets the automaton be learned inside whatever monad the+experiment runs in, e.g. a 'Control.Monad.State.StateT' holding user-defined+statistics.+-}+instance (Monad m) => SUL (MealyAutomaton s) m where     step sul i = return (mealyStep sul i)     reset = return . mealyReset 

@@ -1,97 +0,0 @@-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE ScopedTypeVariables #-}---- | This module implements a Moore automaton.-module Haal.Automaton.MooreAutomaton (-    MooreAutomaton,-    mkMooreAutomaton,-    mooreTransitions,-)-where--import qualified Data.Map as Map-import qualified Data.Set as Set-import Haal.BlackBox-import Control.Monad.Identity (Identity)--data MooreAutomaton state input output = MooreAutomaton-    { mooreDelta :: state -> input -> state-    , mooreLambda :: state -> output-    , mooreInitialS :: state-    , mooreCurrentS :: state-    , mooreStates :: Set.Set state-    }--{- | The 'mkMooreAutomaton' constructor returns a 'MooreAutomaton' by requiring the 'mooreDelta'-function, the 'mooreLambda' function and the initial state 'mooreInitialS'.--}-mkMooreAutomaton :: (s -> i -> s) -> (s -> o) -> Set.Set s -> s -> MooreAutomaton s i o-mkMooreAutomaton delta lambda sts initS =-    MooreAutomaton-        { mooreDelta = delta-        , mooreLambda = lambda-        , mooreInitialS = initS-        , mooreCurrentS = initS-        , mooreStates = sts-        }--{- | Performs a step in the automaton and returns a tuple containing the automaton with a modified-state as well as the output produced by the transition.--}-mooreStep :: MooreAutomaton s i o -> i -> (MooreAutomaton s i o, o)-mooreStep m i = (m{mooreCurrentS = nextState}, output)-  where-    nextState = mooreDelta m (mooreCurrentS m) i-    output = mooreLambda m (mooreCurrentS m)---- | Resets the automaton to its initial state.-mooreReset :: MooreAutomaton s i o -> MooreAutomaton s i o-mooreReset m = m{mooreCurrentS = mooreInitialS m}--instance SUL (MooreAutomaton s) Identity where-    step sul i = return (mooreStep sul i)-    reset = return . mooreReset--{- | Returns a map describing the combined behaviour of the 'mooreDelta'-and 'mooreLambda' functions.--}-mooreTransitions ::-    forall i o s.-    (FiniteOrd s, FiniteOrd i) =>-    MooreAutomaton s i o ->-    Map.Map (s, i) (s, o)-mooreTransitions m = Map.fromList [((s, i), (delta s i, lambda s)) | s <- domainS, i <- domainI]-  where-    delta = mooreDelta m-    lambda = mooreLambda m-    domainS = Set.toList $ mooreStates m-    domainI = Set.toList $ inputs m--instance Automaton MooreAutomaton s where-    transitions = mooreTransitions-    current = mooreCurrentS-    states = mooreStates-    update m s = m{mooreCurrentS = s}--instance-    ( Show i-    , Show o-    , Show s-    , FiniteOrd s-    , FiniteOrd i-    ) =>-    Show (MooreAutomaton s i o)-    where-    show m =-        "{\n\tCurrent State: "-            ++ show currentS-            ++ ",\n\tInitial State: "-            ++ show initialS-            ++ ",\n\tTransitions: "-            ++ show transs-            ++ "\n}"-      where-        transs = mooreTransitions m-        initialS = initial m-        currentS = current m

@@ -7,6 +7,7 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskell                 -fplugin-opt=LiquidHaskell:--prune-unsorted                 -fplugin-opt=LiquidHaskell:--no-termination #-}+{- HLINT ignore "Use error" -} #endif  {- | This module defines the BlackBox type class as well as the Automaton and SUL@@ -15,13 +16,13 @@ module Haal.BlackBox (     Automaton (..),     SUL (..),-    StateID,     Finite,     FiniteEq,     FiniteOrd,     inputs,     outputs,     walk,+    queryChecked,     stepPure,     walkPure,     resetPure,@@ -31,39 +32,95 @@     localCharacterizingSet,     globalCharacterizingSet,     reachable,+    difference, ) where +import Control.Exception (ErrorCall (..), throw) import Control.Monad.Identity (Identity, runIdentity) import qualified Data.Bifunctor as Bif import qualified Data.List as List import qualified Data.Map as Map+import Data.Maybe (fromMaybe) import qualified Data.Set as Set -{- | The 'StateID' type is an alias for an integer that represents the state of the automaton.- - It is used as a default type for the state of learned automata.--}-type StateID = Int- {- | The 'SUL' type class defines the basic interface for a black box automaton.-It provides methods to step through the automaton and retrieve the current state.+It provides methods to step through the automaton and reset it to its initial state. It also requires a monad m, that may be 'Identity' in case of a pure SUL, or 'IO' in case of an external program that performs IO.++Active automata learning requires queries to be independent, so the library+calls 'reset' before every membership query and every equivalence test case+(see 'query'). 'reset' must therefore bring the system back to its initial+state, and the library always continues with the value that 'reset' and 'step'+return. This supports two kinds of SULs:++* persistent ones, such as pure automata, where 'step' returns a new value and+  leaves the old one unchanged;+* stateful ones, such as a driver for a running process or a socket, where+  'step' and 'reset' change the external system and may return the same handle. -} class (Monad m) => SUL sul m where     step :: sul i o -> i -> m (sul i o, o)     reset :: sul i o -> m (sul i o)+    {-# MINIMAL step, reset #-} +    -- | Run a single query: reset the SUL, then feed it the inputs and collect the+    --     outputs. Every query the library sends to a SUL goes through this method, so+    --     that queries are independent of each other.+    --+    --     Override it when a SUL can answer a whole query more efficiently than step by+    --     step, e.g. by sending the whole word in one message. An override must:+    --+    --     * start from the initial state, like 'reset' does;+    --     * return exactly one output per input;+    --     * agree with 'reset' followed by 'walk'.+    --+    --     The library checks the number of outputs at runtime (see 'queryChecked').+    query :: sul i o -> [i] -> m [o]+    query sul is = do+        sul' <- reset sul+        (_, os) <- walk sul' is+        pure os++{- | 'query', checking that the SUL returned exactly one output per input.+A 'SUL' instance may override 'query', and the learners rely on this property,+so they query through this function. A violation is a bug in the instance and+fails with an error naming the expected and actual number of outputs.+-}++{-@ queryChecked :: (SUL sul m) => sul i o -> xs:[i] -> m {ys:[o] | len ys == len xs} @-}+queryChecked :: (SUL sul m) => sul i o -> [i] -> m [o]+queryChecked sul xs = do+    os <- query sul xs+    if length os == length xs+        then pure os+        else contractViolation (length xs) (length os)++{- | Fail because a 'query' override broke its contract. Unlike an @impossible@+error, this one is reachable. LiquidHaskell gives 'error' a @false@ precondition,+so this throws an t'ErrorCall' directly instead, which behaves the same at runtime.+-}+contractViolation :: Int -> Int -> a+contractViolation expected actual =+    throw . ErrorCall $+        "Haal.BlackBox.queryChecked: the SUL returned "+            ++ show actual+            ++ " outputs for a query of "+            ++ show expected+            ++ " inputs; an overridden 'query' must return one output per input"+ -- | Finite is an alias for (Enum, Bounded). type Finite i = (Enum i, Bounded i)  -- | FiniteEq is an alias for (Eq, Finite). type FiniteEq i = (Eq i, Finite i) --- | FiniteOrd is an alias for (Ord, Bounded).+-- | FiniteOrd is an alias for (Ord, Finite). type FiniteOrd i = (Ord i, Finite i)  -- | Generalization of 'step' that operates on a list of inputs.+ {-@ walk :: (SUL sul m) => sul i o -> xs:[i] -> m (sul i o, {ys:[o] | len ys == len xs}) @-} walk :: (SUL sul m) => sul i o -> [i] -> m (sul i o, [o]) walk sul [] = pure (sul, [])@@ -83,11 +140,13 @@ {-@ assume Set.fromList :: Ord a => xs:[a] -> {s:Set.Set a | len xs > 0 => Set.size s > 0} @-}  -- | Return a Set containing only the valid inputs of the SUL.+ {-@ inputs :: (Ord i, Enum i, Bounded i) => sul i o -> {is:Set.Set i | Set.size is > 0} @-} inputs :: (FiniteOrd i) => sul i o -> Set.Set i inputs x = Set.fromList $ rangeIN x  -- | Return a Set containing only the valid outputs of the SUL.+ {-@ outputs :: (Ord o, Enum o, Bounded o) => sul i o -> {os:Set.Set o | Set.size os > 0} @-} outputs :: (FiniteOrd o) => sul i o -> Set.Set o outputs x = Set.fromList $ rangeOUT x@@ -110,6 +169,8 @@ stepPure sul i = runIdentity (step sul i)  -- | Pure instance of 'walk'.++{-@ walkPure :: (SUL sul Identity) => sul i o -> is:[i] -> (sul i o, {os:[o] | len os == len is})@-} walkPure :: (SUL sul Identity) => sul i o -> [i] -> (sul i o, [o]) walkPure sul i = runIdentity (walk sul i) @@ -164,32 +225,35 @@         newVisited = foldr (Set.insert . fst) visited successors         newQueue = successors -{- | Returns an input sequence that distinguishes the given states in-the given automaton.--}-distinguish ::-    ( Automaton aut s-    , FiniteOrd i-    , Ord s+differenceFrom ::+    ( FiniteOrd i+    , FiniteOrd s+    , FiniteOrd s'     , Eq o+    , Automaton aut1 s+    , Automaton aut2 s'     ) =>-    aut s i o ->-    s ->+    aut1 s i o ->     s ->-    [i]-distinguish m s1 s2 = explore Map.empty [(s1, s2, [])]+    aut2 s' i o ->+    s' ->+    Maybe [i]+differenceFrom aut1 s1 aut2 s2 = explore Map.empty [(s1, s2, [])]   where-    alphabet = Set.toList (inputs m)+    alphabet = Set.toList (inputs aut1)+    stepAndCurrent mo i = Bif.first current (stepPure mo i) -    explore _ [] = []-    explore visited ((q1, q2, prefix) : queue)-        | Just symbol <- discrepancy = reverse (symbol : prefix)-        | otherwise = explore newVisited (queue ++ newQueue)+    explore _ [] = Nothing+    explore visited ((q1, q2, prefix) : queue) =+        if (q1, q2) `Map.member` visited+            then explore visited queue+            else case discrepancy of+                Just symbol -> Just $ reverse (symbol : prefix)+                Nothing -> explore newVisited (queue ++ newQueue)       where         newVisited = Map.insert (q1, q2) prefix visited-        mo1 = update m q1-        mo2 = update m q2-+        mo1 = update aut1 q1+        mo2 = update aut2 q2         (nextStates1, outputs1) = unzip $ map (stepAndCurrent mo1) alphabet         (nextStates2, outputs2) = unzip $ map (stepAndCurrent mo2) alphabet @@ -198,13 +262,49 @@         appended = map (: prefix) alphabet          toBeVisited = Map.fromList $ zip (zip nextStates1 nextStates2) appended-         newQueue = [(s1', s2', p) | ((s1', s2'), p) <- Map.toList toBeVisited, (s1', s2') `Map.notMember` visited] -    stepAndCurrent mo i = Bif.first current (stepPure mo i)+{- | Finds a distinguishing sequence between two automata starting from their+ - initial states.+-}+difference ::+    ( FiniteOrd i+    , FiniteOrd s+    , FiniteOrd s'+    , Eq o+    , Automaton aut1 s+    , Automaton aut2 s'+    ) =>+    aut1 s i o ->+    aut2 s' i o ->+    Maybe [i]+difference aut1 aut2 = differenceFrom aut1 (initial aut1) aut2 (initial aut2) +{- | Returns an input sequence that distinguishes the given states in+the given automaton.+-}++{-@ distinguish :: (Automaton aut s, FiniteOrd i, Ord s, Eq o) =>+      aut s i o ->+      s1:s ->+      s2:s ->+      {is:[i] | s1 == s2 ==> len is = 0}+@-}+distinguish ::+    ( Automaton aut s+    , FiniteOrd s+    , FiniteOrd i+    , Eq o+    ) =>+    aut s i o ->+    s ->+    s ->+    [i]+distinguish _ s1 s2 | s1 == s2 = []+distinguish m s1 s2 = fromMaybe [] $ differenceFrom m s1 m s2+ {- | Returns a set of lists of inputs that can be used to distinguish between the given state and- - any other state of the automaton.+- any other state of the automaton. -} localCharacterizingSet ::     ( Automaton aut s

@@ -5,10 +5,12 @@     mealyToDot,     ParsedMealy (..),     parseDot,+    MealyTable (..),+    mealyTable,     generateModule, ) where -import Data.Char (isAlphaNum, isDigit, isLower, isSpace, toUpper)+import Data.Char (chr, isAlphaNum, isDigit, isLower, isSpace, ord, toUpper) import Data.List (intercalate, isInfixOf, isPrefixOf) import qualified Data.Map.Strict as Map import Data.Maybe (mapMaybe)@@ -115,9 +117,9 @@     if initSt `Set.notMember` allStateSet         then Left ("Initial state '" ++ initSt ++ "' does not appear in any transition")         else do-            let stateOrder = initSt : Set.toList (Set.delete initSt allStateSet)-                inputSyms = Set.toList . Set.fromList $ map (\(_, i, _, _) -> i) trans-                outputSyms = Set.toList . Set.fromList $ map (\(_, _, _, o) -> o) trans+            let stateOrder = ordNub (initSt : concatMap (\(s, _, d, _) -> [s, d]) trans)+                inputSyms = ordNub $ map (\(_, i, _, _) -> i) trans+                outputSyms = ordNub $ map (\(_, _, _, o) -> o) trans                 warnings = slashWarnings inputSyms outputSyms             return                 ParsedMealy@@ -130,6 +132,85 @@                     }  -- ---------------------------------------------------------------------------+-- Transition tables+-- ---------------------------------------------------------------------------++{- | A complete, deterministic Mealy automaton in the table encoding expected+  by 'Haal.Automaton.MealyAutomaton.mkMealyAutomatonTable'.++  States, inputs, and outputs are numbered by their position in+  'parsedStates', 'parsedInputs', and 'parsedOutputs', so the initial state+  is always @0@. The entry at position @s * k + j@ of each table, where @k@+  is the number of inputs, describes state @s@ on input @j@, encoded as the+  'Char' with that code point.+-}+data MealyTable = MealyTable+    { tableStates :: Int+    -- ^ The number of states.+    , tableDelta :: String+    -- ^ The next state of each transition.+    , tableLambda :: String+    -- ^ The output of each transition.+    }+    deriving (Show, Eq)++{- | Encode a 'ParsedMealy' as a 'MealyTable'.++  Returns @'Left' err@ if some state has no transition, or more than one+  distinct transition, for some input, or if the automaton is too large for+  the encoding (every number must be a code point below @0xD800@).+-}+mealyTable :: ParsedMealy -> Either String MealyTable+mealyTable pm+    | length stateNames > maxCode || length (parsedOutputs pm) > maxCode =+        Left ("Automaton is too large for the table encoding (at most " ++ show maxCode ++ " states and outputs)")+    | not (null conflicts) =+        Left ("Nondeterministic automaton:\n" ++ unlines (map describeConflict conflicts))+    | not (null missing) =+        Left $+            "Incomplete automaton: "+                ++ show (length missing)+                ++ " missing transition(s), e.g.\n"+                ++ unlines (map describeMissing (take 10 missing))+    | otherwise =+        Right+            MealyTable+                { tableStates = length stateNames+                , tableDelta = map (chr . fst) entries+                , tableLambda = map (chr . snd) entries+                }+  where+    maxCode = 0xD800+    stateNames = parsedStates pm+    inputNames = parsedInputs pm+    stateIdx = Map.fromList (zip stateNames [0 :: Int ..])+    inputIdx = Map.fromList (zip inputNames [0 :: Int ..])+    outputIdx = Map.fromList (zip (parsedOutputs pm) [0 :: Int ..])++    -- Every name is in its index map, since all three lists are built from+    -- 'parsedTrans' by 'parseDot'.+    byKey =+        Map.fromListWith+            Set.union+            [ ((stateIdx Map.! src, inputIdx Map.! inp), Set.singleton (stateIdx Map.! dst, outputIdx Map.! out))+            | (src, inp, dst, out) <- parsedTrans pm+            ]+    conflicts = [(k, Set.toList ts) | (k, ts) <- Map.toList byKey, Set.size ts > 1]+    keys = [(s, i) | s <- [0 .. length stateNames - 1], i <- [0 .. length inputNames - 1]]+    missing = filter (`Map.notMember` byKey) keys+    entries = [t | k <- keys, t <- take 1 (foldMap Set.toList (Map.lookup k byKey))]++    nameOf names = \x -> Map.findWithDefault "?" x (Map.fromList (zip [0 :: Int ..] names))+    stateName = nameOf stateNames+    inputName = nameOf inputNames+    outputName = nameOf (parsedOutputs pm)+    describeMissing (s, i) = "  state " ++ show (stateName s) ++ ", input " ++ show (inputName i)+    describeConflict ((s, i), ts) =+        describeMissing (s, i)+            ++ " → "+            ++ intercalate ", " [show (stateName d) ++ " / " ++ show (outputName o) | (d, o) <- ts]++-- --------------------------------------------------------------------------- -- Code generator -- --------------------------------------------------------------------------- @@ -141,25 +222,23 @@   * A @data \<modName\>Input@ type whose constructors are the sanitized input     symbols, deriving @Show, Eq, Ord, Enum, Bounded@.   * A @data \<modName\>Output@ type, similarly for output symbols.-  * A value @valName :: MealyAutomaton Int \<modName\>Input \<modName\>Output@.+  * A value @valName :: MealyAutomaton Int \<modName\>Input \<modName\>Output@,+    built with 'Haal.Automaton.MealyAutomaton.mkMealyAutomatonTable' from the+    'MealyTable' of @pm@, preceded by a comment listing every transition.    Returns @'Left' err@ if two distinct symbols sanitize to the same-  constructor name.+  constructor name, or if 'mealyTable' rejects the automaton. -} 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"+    table <- mealyTable pm+    let n = tableStates table+        k = length inputCons+        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."@@ -169,8 +248,7 @@             , "    , " ++ valName             , "    ) where"             , ""-            , "import qualified Data.Set as Set"-            , "import Haal.Automaton.MealyAutomaton (MealyAutomaton, mkMealyAutomaton)"+            , "import Haal.Automaton.MealyAutomaton (MealyAutomaton, mkMealyAutomatonTable)"             , ""             , "data " ++ inputType             ]@@ -179,18 +257,19 @@                    , "data " ++ outputType                    ]                 ++ enumDecl outputCons-                ++ [ ""-                   , valName ++ " :: MealyAutomaton Int " ++ inputType ++ " " ++ outputType-                   , valName-                        ++ " = mkMealyAutomaton delta lambda (Set.fromList [0.."-                        ++ show (n - 1)-                        ++ "]) 0"+                ++ [""]+                ++ transitionComment inputCons outputCons table+                ++ [ valName ++ " :: MealyAutomaton Int " ++ inputType ++ " " ++ outputType+                   , valName ++ " ="+                   , "    case mkMealyAutomatonTable " ++ show n ++ " 0 deltaTable lambdaTable of"+                   , "        Right m -> m"+                   , "        Left err -> error (\"haal-gen: invalid transition table: \" ++ err)"                    , "  where"+                   , "    deltaTable ="                    ]-                ++ map ("    " ++) deltaLines-                ++ ["    delta _ _ = error \"haal-gen: undefined transition\""]-                ++ map ("    " ++) lambdaLines-                ++ ["    lambda _ _ = error \"haal-gen: undefined transition\""]+                ++ stringRows k (tableDelta table)+                ++ ["    lambdaTable ="]+                ++ stringRows k (tableLambda table)  -- --------------------------------------------------------------------------- -- Code generation helpers@@ -203,31 +282,48 @@         ++ 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+{- | A block comment listing every transition of the table, one state at a+  time, so that the generated module stays readable.+-}+transitionComment :: [String] -> [String] -> MealyTable -> [String]+transitionComment inputCons outputCons table =+    ["{- Transitions (state  input -> next state / output):"]+        ++ concat (zipWith stateLines [0 :: Int ..] (chunksOf k entries))+        ++ ["-}"]   where-    si = stateIdx Map.! src-    di = stateIdx Map.! dst-    ic = inputConMap Map.! inp+    k = length inputCons+    entries = zip (tableDelta table) (tableLambda table)+    width = maximum (0 : map length inputCons)+    stateLines s row =+        [ "    " ++ pad 5 (if j == 0 then show s else "") ++ pad width inp ++ " -> " ++ show (ord d) ++ " / " ++ out+        | (j, inp, (d, o)) <- zip3 [0 :: Int ..] inputCons row+        , out <- take 1 (drop (ord o) outputCons)+        ]+    pad w str = str ++ replicate (w - length str + 1) ' ' -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+{- | Render a table as an indented string literal with one row of @k@+  entries per line, joined by string gaps. Every entry is written as a+  numeric escape, so that each row reads as a list of numbers.+-}+stringRows :: Int -> String -> [String]+stringRows k str = case chunksOf k str of+    [] -> ["        \"\""]+    rows ->+        [ "        " ++ open ++ concatMap escape row ++ close+        | (j, row) <- zip [0 :: Int ..] rows+        , let open = if j == 0 then "\"" else "\\"+              close = if j == length rows - 1 then "\"" else "\\"+        ]   where-    si = stateIdx Map.! src-    ic = inputConMap Map.! inp-    oc = outputConMap Map.! out+    escape c = '\\' : show (ord c) +chunksOf :: Int -> [a] -> [[a]]+chunksOf k xs+    | k <= 0 = []+    | otherwise = case splitAt k xs of+        ([], _) -> []+        (chunk, rest) -> chunk : chunksOf k rest+ {- | Sanitize a list of symbols to valid Haskell constructor names using the   given prefix, failing if two distinct symbols would produce the same name. -}@@ -276,6 +372,19 @@ -- --------------------------------------------------------------------------- -- Parser helpers -- ---------------------------------------------------------------------------++{- | Remove duplicates, keeping the first occurrence of each element, in+  @O(n log n)@. Symbols and states keep the order in which they first appear+  in the DOT file, so that regenerating a model keeps its constructor order+  and state numbering.+-}+ordNub :: (Ord a) => [a] -> [a]+ordNub = go Set.empty+  where+    go _ [] = []+    go seen (x : xs)+        | x `Set.member` seen = go seen xs+        | otherwise = x : go (Set.insert x seen) xs  slashWarnings :: [String] -> [String] -> [String] slashWarnings inputs outputs =

@@ -50,7 +50,7 @@   where     alphabet = Set.size $ inputs aut     accessSeqs = Map.size $ accessSequences aut-    characterizingSet = Set.size $ globalCharacterizingSet aut+    characterizingSet = Set.size $ testSuffixes (globalCharacterizingSet aut)     transitionCover = accessSeqs * alphabet     size = sum [transitionCover * (alphabet ^ n) * characterizingSet | n <- [0 .. d]] @@ -68,7 +68,7 @@   where     alphabet = Set.toList $ inputs aut     accessSeqs = accessSequences aut-    characterizingSet = Set.toList $ globalCharacterizingSet aut+    characterizingSet = Set.toList $ testSuffixes (globalCharacterizingSet aut)     transitionCover = [a ++ [inp] | a <- Map.elems accessSeqs, inp <- alphabet]     middlesByDepth = [replicateM n alphabet | n <- [0 .. d]]     suite =@@ -114,7 +114,7 @@     (RandomWMethod, [[i]]) randomWMethodSuite (RandomWMethod (RandomWMethodConfig g wpr wl)) aut =     let prefixes = Map.elems $ accessSequences aut-        suffixes = Set.toList $ globalCharacterizingSet aut+        suffixes = Set.toList $ testSuffixes (globalCharacterizingSet aut)         alphaVec = Vec.fromList . Set.toList $ inputs aut         genWord =             if wl == 0@@ -134,3 +134,15 @@  instance EquivalenceOracle RandomWMethod where     testSuite = randomWMethodSuite++{- | The suffixes that test words end with: the given characterizing set, or+just the empty word when that set is empty. A hypothesis with a single state+has an empty characterizing set (there is nothing to distinguish), and without+the empty word it would get no test words at all, so it would be accepted+without any testing. Ending a test word with the empty word still checks the+outputs along the rest of the word.+-}+testSuffixes :: Set.Set [i] -> Set.Set [i]+testSuffixes w+    | Set.null w = Set.singleton []+    | otherwise = w

@@ -16,8 +16,16 @@ import Control.Monad.State (MonadState (state), State, runState) import qualified Data.Map as Map import qualified Data.Set as Set-import Haal.BlackBox-import Haal.Experiment+import Haal.BlackBox (+    Automaton (current, states),+    FiniteOrd,+    accessSequences,+    globalCharacterizingSet,+    inputs,+    localCharacterizingSet,+    walk,+ )+import Haal.Experiment (EquivalenceOracle (..)) import System.Random (Random (randomR), StdGen)  -- | The 'WpMethodConfig' type is used to configure the Wp-method equivalence oracle.@@ -53,17 +61,18 @@     stateCover = accessSequences aut     localSufSizes =         Map.fromAscList-            [ (st, Set.size (localCharacterizingSet aut st))+            [ (st, Set.size (testSuffixes (localCharacterizingSet aut st)))             | st <- Set.toAscList (states aut)             ]-    globalSufSize = Set.size (globalCharacterizingSet aut)+    globalSufSize = Set.size (testSuffixes (globalCharacterizingSet aut))     transitionCover =         Set.fromList             [ acc ++ [a]             | acc <- Map.elems stateCover             , a <- alphabetList             ]-    difference = Set.fromList (Map.elems stateCover) `Set.difference` transitionCover+    -- the transitions that do not already lead to a state of the state cover+    difference = transitionCover `Set.difference` Set.fromList (Map.elems stateCover)      -- Closed form: |S| * |W| * (1 + |Σ| + ... + |Σ|^d)     firstPhaseSize =@@ -98,18 +107,19 @@     stateCover = accessSequences aut     localSuf =         Map.fromAscList-            [ (st, localCharacterizingSet aut st) | st <- Set.toAscList $ states aut+            [ (st, testSuffixes (localCharacterizingSet aut st)) | st <- Set.toAscList $ states aut             ]-    globalSuf = globalCharacterizingSet aut+    globalSuf = testSuffixes (globalCharacterizingSet aut)      transitionCover =         [ acc ++ [a]         | acc <- Map.elems stateCover         , a <- Set.toList alphabet         ]+    -- the transitions that do not already lead to a state of the state cover     difference =-        Set.fromList (Map.elems stateCover)-            `Set.difference` Set.fromList transitionCover+        Set.fromList transitionCover+            `Set.difference` Set.fromList (Map.elems stateCover)      firstPhase =         concat@@ -187,9 +197,9 @@         prefixes = accessSequences aut         localSuf =             Map.fromAscList-                [ (st, localCharacterizingSet aut st) | st <- Set.toAscList $ states aut+                [ (st, testSuffixes (localCharacterizingSet aut st)) | st <- Set.toAscList $ states aut                 ]-        globalSuf = globalCharacterizingSet aut+        globalSuf = testSuffixes (globalCharacterizingSet aut)          (suite, genfinal) = runState (replicateM lim genTestCase) g @@ -229,3 +239,15 @@  instance EquivalenceOracle RandomWpMethod where     testSuite = randomWpMethodSuite++{- | The suffixes that test words end with: the given characterizing set, or+just the empty word when that set is empty. A hypothesis with a single state+has an empty characterizing set (there is nothing to distinguish), and without+the empty word it would get no test words at all, so it would be accepted+without any testing. Ending a test word with the empty word still checks the+outputs along the rest of the word.+-}+testSuffixes :: Set.Set [i] -> Set.Set [i]+testSuffixes w+    | Set.null w = Set.singleton []+    | otherwise = w

@@ -1,5 +1,7 @@+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE UndecidableInstances #-}  {- | This module exports the basic types, classes and functions that are required to@@ -10,13 +12,12 @@     ExperimentT,     Learner (..),     EquivalenceOracle (..),-    Statistics (..),     experiment,-    runExperiment,-    pairwiseWalk,-    execute,     findCex,+    runExperiment,     runExperimentT,+    experimentWith,+    measuredExperiment, ) where  import Control.Monad.Reader (@@ -25,10 +26,14 @@     Reader,     ReaderT (runReaderT),     runReader,+    withReaderT,  )+import Control.Monad.State (StateT, modify', runStateT) +import Control.Foldl (Fold (..)) import Control.Monad.Identity import Haal.BlackBox+import Haal.Statistics (Event (..), Phase (Learning, Testing))  {- | The 'EquivalenceOracle' type class defines the interface for equivalence oracles. Instances of this class should provide methods to generate a test suite@@ -49,7 +54,7 @@ refine the learner with a counterexample, and learn an automaton. The type @l@ determines the type of automaton @aut@ that is learned. -}-class Learner l aut s | l -> aut s where+class Learner l aut | l -> aut where     initialize ::         ( SUL sul m         , FiniteOrd i@@ -67,13 +72,12 @@         ExperimentT (sul i o) m (l i o)     learn ::         ( SUL sul m-        , Automaton aut s+        , Automaton aut Int         , FiniteOrd i-        , FiniteOrd s         , FiniteOrd o         ) =>         l i o ->-        ExperimentT (sul i o) m (l i o, aut s i o)+        ExperimentT (sul i o) m (l i o, aut Int i o)  {- | The 'ExperimentT' type is a monad transformer that allows for running experiments in a reader monad. This may prove useful for@@ -98,56 +102,141 @@ runExperiment :: Reader r a -> r -> a runExperiment = runReader -{- | The 'Statistics' data type is parameterized by the type of model being learned-and the state, input and output types of the model. Its purpose is to keep track of-different experimental stats. For the time being, only the number of rounds 'statsRounds',-the counterexamples 'statsCexs' and the intermediate hypotheses 'statsHyps' are being kept-track of.+{- | The learning loop, reporting the events it sees itself (phases,+hypotheses, counterexamples) to the given function. It can't observe+membership queries. -}-data Statistics aut s i o = Statistics-    { statsRounds :: Int-    , statsCexs :: [[i]]-    , statsHyps :: [aut s i o]-    }-    deriving (Show)+loop ::+    ( EquivalenceOracle oracle+    , Learner learner aut+    , FiniteOrd i+    , FiniteOrd o+    , Automaton aut Int+    , SUL sul m+    ) =>+    (Event aut i o -> m ()) ->+    learner i o ->+    oracle ->+    ExperimentT (sul i o) m (aut Int i o)+loop emit learner oracle = do+    lift (emit (PhaseChanged Learning))+    initializedLearner <- initialize learner+    let inner le orc = do+            (learner', aut) <- learn le+            lift (emit (Hypothesis aut))+            lift (emit (PhaseChanged Testing))+            (oracle', cex) <- findCex orc aut+            case cex of+                ([], []) -> return aut+                (ce, _) -> do+                    lift (emit (Counterexample ce))+                    lift (emit (PhaseChanged Learning))+                    refinedLearner <- refine learner' ce+                    inner refinedLearner oracle'+    inner initializedLearner oracle --- | Empty 'Statistics' value.-mkStats :: Statistics aut s i o-mkStats = Statistics 0 [] []+{- | 'Observed' is going to be used by the experiments. It wraps the SUL+and reports the queries to the experiment loop.+-}+data Observed m sul i o = Observed (sul i o) ([i] -> [o] -> m ()) +instance (SUL sul m) => SUL (Observed m sul) m where+    step :: Observed m sul i o -> i -> m (Observed m sul i o, o)+    step (Observed sul report) input = do+        (sul', output) <- step sul input+        return (Observed sul' report, output)+    reset :: Observed m sul i o -> m (Observed m sul i o)+    reset (Observed sul report) = (`Observed` report) <$> reset sul+    query :: Observed m sul i o -> [i] -> m [o]+    query (Observed sul report) is = do+        os <- query sul is+        report is os+        return os++{- | The 'experimentWith' function is 'experiment', reporting every 'Event' to+the given function, in the experiment's monad: the phases ('PhaseChanged'), every+query sent to the SUL ('Queried'), every hypothesis ('Hypothesis') and every+counterexample ('Counterexample'). The experiment starts in the 'Learning'+phase, enters 'Testing' before each hypothesis is validated, and goes back to+'Learning' after each counterexample. For statistics, 'measuredExperiment' is+usually more convenient.+-}+experimentWith ::+    ( EquivalenceOracle oracle+    , Learner learner aut+    , FiniteOrd i+    , FiniteOrd o+    , Automaton aut Int+    , SUL sul m+    ) =>+    (Event aut i o -> m ()) ->+    learner i o ->+    oracle ->+    ExperimentT (sul i o) m (aut Int i o)+experimentWith emit learner oracle =+    withReaderT (\sul -> Observed sul (\is os -> emit (Queried is os))) (loop emit learner oracle)++-- | A SUL lifted into 'StateT', so that 'measuredExperiment' can keep its state there.+newtype Lifted sul i o = Lifted (sul i o)++instance (SUL sul m) => SUL (Lifted sul) (StateT x m) where+    step :: Lifted sul i o -> i -> StateT x m (Lifted sul i o, o)+    step (Lifted sul) input = do+        (sul', output) <- lift (step sul input)+        return (Lifted sul', output)+    reset :: Lifted sul i o -> StateT x m (Lifted sul i o)+    reset (Lifted sul) = Lifted <$> lift (reset sul)+    query :: Lifted sul i o -> [i] -> StateT x m [o]+    query (Lifted sul) = lift . query sul++{- | The 'measuredExperiment' function is 'experiment', also returning a+statistic: a 'Control.Foldl.Fold' over the experiment's events (see+"Haal.Statistics"). 'Haal.Statistics.statistics' measures the usual ones;+combine it with folds of your own through the 'Applicative' instance of 'Fold':++> runExperiment (measuredExperiment statistics learner oracle) sul+> runExperiment (measuredExperiment ((,) <$> statistics <*> myFold) learner oracle) sul+-}+measuredExperiment ::+    ( EquivalenceOracle oracle+    , Learner learner aut+    , FiniteOrd i+    , FiniteOrd o+    , Automaton aut Int+    , SUL sul m+    ) =>+    Fold (Event aut i o) r ->+    learner i o ->+    oracle ->+    ExperimentT (sul i o) m (aut Int i o, r)+measuredExperiment (Fold stepFold x0 done) learner oracle = do+    sul <- ask+    let measured = runReaderT (experimentWith (\e -> modify' (`stepFold` e)) learner oracle) (Lifted sul)+    (model, x) <- lift (runStateT measured x0)+    return (model, done x)+ {- | The 'experiment' function returns an 'Experiment' that can be run with the 'runExperiment' function. It takes a learner and an equivalence oracle and then requires a system under learning (SUL) to run the experiment. -} experiment ::-    ( SUL sul m-    , Automaton aut s-    , Learner learner aut s-    , EquivalenceOracle oracle+    ( EquivalenceOracle oracle+    , Learner learner aut     , FiniteOrd i-    , FiniteOrd s     , FiniteOrd o+    , Automaton aut Int+    , SUL sul m     ) =>     learner i o ->     oracle ->-    ExperimentT (sul i o) m (aut s i o, Statistics aut s i o)-experiment learner oracle = do-    initializedLearner <- initialize learner-    let inner le orc stats = do-            (learner', aut) <- learn le-            (oracle', cex) <- findCex orc aut-            case cex of-                ([], []) -> return (aut, stats)-                (ce, _) -> do-                    refinedLearner <- refine learner' ce-                    let rounds = statsRounds stats-                        cexs = statsCexs stats-                        hyps = statsHyps stats-                        stats' = Statistics (rounds + 1) (ce : cexs) (aut : hyps)-                    inner refinedLearner oracle' stats'-    inner initializedLearner oracle mkStats+    ExperimentT (sul i o) m (aut Int i o)+experiment = loop (\_ -> return ()) --- | The 'execute' function executes the test suite of an oracle, given a SUL and an automaton.+{- | The 'execute' function executes the test suite of an oracle, given a SUL and an automaton.+Every test case is run from the initial state of both the SUL and the automaton. It returns+the first test case on which they disagree, together with the outputs of the SUL, or a pair+of empty lists if they agree on every test case.+-} execute ::     ( SUL sul m     , Automaton aut s@@ -160,32 +249,10 @@     m ([i], [o]) execute _ _ [] = return ([], []) execute theSul theAut (s : ss) = do-    continue <- pairwiseWalk theSul theAut s-    if continue+    out <- queryChecked theSul s+    if out == runIdentity (query theAut s)         then execute theSul theAut ss-        else do-            (_, out) <- walk theSul s-            return (s, out)--{- | The 'pairwiseWalk' function executes a test case on both the SUL and the automaton-simultaneously, checking if the outputs are the same.--}-pairwiseWalk ::-    ( SUL sul m-    , Automaton aut s-    , Ord i-    , Eq o-    ) =>-    sul i o ->-    aut s i o ->-    [i] ->-    m Bool-pairwiseWalk _ _ [] = return True-pairwiseWalk theSul theAut (s : ss) = do-    (sul', out1) <- step theSul s-    let (aut', out2) = runIdentity (step theAut s)-    rest <- pairwiseWalk sul' aut' ss-    return $ out1 == out2 && rest+        else return (s, out)  {- | The 'findCex' function executes the test suite of each oracle to the automaton and SUL.

@@ -130,8 +130,7 @@         em = Set.fromList alph         {-@ domain :: Set.Set ([i], {v:[i] | len v = 1}) @-}         domain = (sm `Set.union` sm_I) `Set.cartesianProduct` em-    sulR <- lift $ reset sul-    tm <- lift $ updateMap Map.empty domain sulR+    tm <- lift $ updateMap Map.empty domain sul      return         ( ObservationTable@@ -153,7 +152,6 @@ equivalenceClasses ot = go Map.empty sm   where     sm = prefixSetS ot-    sm_I = prefixSetSI ot     go acc s         | Set.null s = acc         | otherwise =@@ -167,7 +165,7 @@     forall sul i o m.     (SUL sul m, FiniteOrd i, Ord o, Monad m) =>     LMstar i o ->-    ExperimentT (sul i o) m (LMstar i o, MealyAutomaton StateID i o)+    ExperimentT (sul i o) m (LMstar i o, MealyAutomaton Int i o) lmstar (LMstar (Init ot)) = case otIsClosed ot of     [] -> case otIsConsistent ot of         ([], []) -> case makeHypothesis ot of@@ -268,12 +266,12 @@     return ot'  {- | The 'makeHypothesis' function constructs a Mealy automaton from the observation table. It uses-the default 'StateID' type defined in the 'Experiment' module for representing the automaton states.+the default 'Int' type defined in the 'Experiment' module for representing the automaton states. Returns 'Nothing' if the observation table is malformed (invariant violated). -} -{-@ makeHypothesis :: (FiniteOrd i, Eq o) => ObservationTable i o -> Maybe (MealyAutomaton StateID i o) @-}-makeHypothesis :: forall i o. (FiniteOrd i, Eq o) => ObservationTable i o -> Maybe (MealyAutomaton StateID i o)+{-@ makeHypothesis :: (FiniteOrd i, Eq o) => ObservationTable i o -> Maybe (MealyAutomaton Int i o) @-}+makeHypothesis :: forall i o. (FiniteOrd i, Eq o) => ObservationTable i o -> Maybe (MealyAutomaton Int i o) makeHypothesis ot = do     startId <- getStateId []     let stateInputPairs = [(sid, i) | sid <- [0 .. numStates - 1], i <- alphaList]@@ -292,19 +290,19 @@     idToRep = Map.fromList (zip [0 ..] repList)     alphaList = [minBound .. maxBound] :: [i] -    getStateId :: [i] -> Maybe StateID+    getStateId :: [i] -> Maybe Int     getStateId s = List.find (equivalentRows ot s) repList >>= flip Map.lookup repToId -    repAt :: StateID -> Maybe [i]+    repAt :: Int -> Maybe [i]     repAt sid = Map.lookup sid idToRep -    buildDeltaEntry :: (StateID, i) -> Maybe ((StateID, i), StateID)+    buildDeltaEntry :: (Int, i) -> Maybe ((Int, i), Int)     buildDeltaEntry (sid, i) = do         rep <- repAt sid         target <- getStateId (rep ++ [i])         return ((sid, i), target) -    buildLambdaEntry :: (StateID, i) -> Maybe ((StateID, i), o)+    buildLambdaEntry :: (Int, i) -> Maybe ((Int, i), o)     buildLambdaEntry (sid, i) = do         rep <- repAt sid         out <- Map.lookup (rep, [i]) (mappingT ot)@@ -326,13 +324,13 @@ makeConsistent ot (symbol, column) = do     sul <- ask     let-        query = symbol ++ column+        suffix = symbol ++ column         em = suffixSetE ot-        em' = query `Set.insert` em+        em' = suffix `Set.insert` em         sm = prefixSetS ot         sm_I = prefixSetSI ot         tm = mappingT ot-        missing = (sm `Set.union` sm_I) `Set.cartesianProduct` Set.singleton query+        missing = (sm `Set.union` sm_I) `Set.cartesianProduct` Set.singleton suffix     tm' <- lift $ updateMap tm missing sul     return (ObservationTable{prefixSetS = sm, suffixSetE = em', mappingT = tm', prefixSetSI = sm_I}) @@ -362,7 +360,7 @@     tm' <- lift $ updateMap tm missing sul     return (ObservationTable{prefixSetS = sm', suffixSetE = em, mappingT = tm', prefixSetSI = sm_I'}) -instance Learner LMstar MealyAutomaton StateID where+instance Learner LMstar MealyAutomaton where     initialize (LMstar _) = do         LMstar . Init <$> initializeOT     initialize (LMplus _) = do@@ -431,7 +429,7 @@     ([i], [i]) ->     m (Map.Map ([i], [i]) [o]) insertStep thesul acc (a, b) = do-    (_, outs) <- walk thesul (a ++ b)+    outs <- queryChecked thesul (a ++ b)     -- the table is prefix closed, so no need to store     -- the whole length of outs, just the output that corresponds     -- to the suffix

@@ -0,0 +1,151 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}+#ifdef LIQUID+-- GHC unboxes the strict Int fields of 'Tally' when optimising, which+-- LiquidHaskell cannot match against the data refinement, so verification+-- builds keep them boxed. Remove once this is fixed upstream:+-- https://github.com/ucsd-progsys/liquidhaskell/issues/2629+{-# OPTIONS_GHC -fplugin=LiquidHaskell+                -fplugin-opt=LiquidHaskell:--prune-unsorted+                -fno-unbox-small-strict-fields #-}+#endif++{- | Statistics for learning experiments.++An experiment emits an 'Event' at every step that matters for statistics: when+it changes 'Phase', for every query sent to the SUL, for every hypothesis and for+every counterexample. A statistic is a fold over these events, a+'Control.Foldl.Fold' from the @foldl@ package. Folds combine with their+'Applicative' instance into a single fold that still runs in one pass, so any+number of statistics can be measured at once:++> (model, stats) = runExperiment (measuredExperiment statistics learner oracle) sul++'statistics' measures what most experiments report: the membership queries and+symbols sent while constructing hypotheses and while validating them, and every+hypothesis and counterexample. Combine it with folds of your own:++> runExperiment (measuredExperiment ((,) <$> statistics <*> myFold) learner oracle) sul++See 'Haal.Experiment.measuredExperiment' and 'Haal.Experiment.experimentWith'.+Users define their own statistics as folds, e.g. with 'Control.Foldl.premap'+and 'Control.Foldl.prefilter' over the folds of @foldl@, and can test one by+running it over a list of events with 'Control.Foldl.fold'.+-}+module Haal.Statistics (+    -- * Events+    Phase (..),+    Event (..),++    -- * Statistics+    Statistics (..),+    Tally (..),+    statistics,+    total,+    rounds,+)+where++import qualified Control.Foldl as L++-- | The phase of a learning experiment.+data Phase+    = -- | The learner is constructing or refining a hypothesis.+      Learning+    | -- | The oracle is validating a hypothesis. This is the equivalence query,+      -- approximated by conformance testing, which sends test cases to the SUL+      -- as membership queries.+      Testing+    deriving (Show, Eq)++-- | Something that happened during an experiment.+data Event aut i o+    = -- | The experiment entered a phase.+      PhaseChanged Phase+    | -- | A query was sent to the SUL, with its inputs and outputs.+      Queried [i] [o]+    | -- | The learner produced a hypothesis (every one, including the final one).+      Hypothesis (aut Int i o)+    | -- | The oracle found a counterexample.+      Counterexample [i]++{- | The number of queries and symbols sent to a SUL. The fields are strict,+because an experiment sends a great number of queries.+-}+data Tally = Tally {queries :: !Int, symbols :: !Int} deriving (Show, Eq)++{-@ data Tally = Tally {queries :: Nat, symbols :: Nat} @-}++{- | The statistics of an experiment, measured by 'statistics'. The number of+equivalence queries is the number of hypotheses: each hypothesis is validated+once.+-}+data Statistics aut i o = Statistics+    { learning :: !Tally+    -- ^ Membership queries during hypothesis construction+    , testing :: !Tally+    -- ^ Membership queries during hypothesis validation+    , hypotheses :: [aut Int i o]+    -- ^ Every hypothesis, including the final one, most recent first+    , counterexamples :: [[i]]+    -- ^ Every counterexample, most recent first+    }++deriving instance (Show (aut Int i o), Show i) => Show (Statistics aut i o)+deriving instance (Eq (aut Int i o), Eq i) => Eq (Statistics aut i o)++{-@ data Statistics aut i o = Statistics+      { learning        :: Tally+      , testing         :: Tally+      , hypotheses      :: [aut Int i o]+      , counterexamples :: [[i]]+      } @-}++-- | Queries and symbols of both phases together.++{-@ total :: s:Statistics aut i o -> {t:Tally | queries t == queries (learning s) + queries (testing s)+                                             && symbols t == symbols (learning s) + symbols (testing s)} @-}+total :: Statistics aut i o -> Tally+total s = Tally (queries l + queries t) (symbols l + symbols t)+  where+    l = learning s+    t = testing s++-- | The number of rounds, i.e. of counterexamples found.+rounds :: Statistics aut i o -> Int+rounds = length . counterexamples++{- | Add queries and symbols to the tally of a phase. Verified by LiquidHaskell:+the total grows by exactly the given amounts, and the tally of the other phase+is untouched.+-}++{-@ tick :: p:Phase -> q:Nat -> n:Nat -> s:Statistics aut i o+         -> {r:Statistics aut i o | queries (learning r) + queries (testing r) == queries (learning s) + queries (testing s) + q+                                 && symbols (learning r) + symbols (testing r) == symbols (learning s) + symbols (testing s) + n+                                 && (p == Learning => (queries (testing r) == queries (testing s)+                                                       && symbols (testing r) == symbols (testing s)))+                                 && (p == Testing  => (queries (learning r) == queries (learning s)+                                                       && symbols (learning r) == symbols (learning s)))} @-}+tick :: Phase -> Int -> Int -> Statistics aut i o -> Statistics aut i o+tick p q n s = case p of+    Learning -> s{learning = add (learning s)}+    Testing -> s{testing = add (testing s)}+  where+    add (Tally q0 n0) = Tally (q0 + q) (n0 + n)++-- | The state of 'statistics': the current phase and the statistics so far.+data Acc aut i o = Acc !Phase !(Statistics aut i o)++{- | Measure the 'Statistics' of an experiment: the membership queries and+symbols sent in each phase, and every hypothesis and counterexample.+-}+statistics :: L.Fold (Event aut i o) (Statistics aut i o)+statistics = L.Fold step (Acc Learning (Statistics (Tally 0 0) (Tally 0 0) [] [])) (\(Acc _ s) -> s)+  where+    step (Acc _ s) (PhaseChanged p) = Acc p s+    step (Acc p s) (Queried is _) = Acc p (tick p 1 (length is) s)+    step (Acc p s) (Hypothesis aut) = Acc p s{hypotheses = aut : hypotheses s}+    step (Acc p s) (Counterexample cex) = Acc p s{counterexamples = cex : counterexamples s}

@@ -6,6 +6,8 @@ ) where +import Control.Monad (replicateM)+import Control.Monad.Identity (runIdentity) import qualified Data.List as List import qualified Data.Map as Map import qualified Data.Maybe as Maybe@@ -14,32 +16,32 @@     MealyAutomaton (..),     mealyDelta,     mealyLambda,+    mkMealyAutomaton,  ) import Haal.BlackBox-import Test.Hspec (Spec, context, describe, it)-import Test.QuickCheck (Property, property, (==>))-import Utils (Input, Mealy (..), NonMinimalMealy (..), Output, State, statesAreEquivalent)-import Control.Monad.Identity (runIdentity)+import Test.Hspec (Spec, context, describe, it, shouldBe)+import Test.QuickCheck (Property, forAll, property, (.&&.), (===), (==>))+import Utils (Input (..), Mealy (..), NonMinimalMealy (..), Output (..), genState, statesAreEquivalent)  -- The global characterizing set of a non minimal mealy automaton contains--- the empty list. This will fail if the 'State' type has less than 6-7 constructors+-- the empty list. This will fail if 'stateSpace' has fewer than 6-7 states -- because a lot of test cases will be discarded.-prop_emptyListInCharacterizingSet :: NonMinimalMealy -> State -> State -> Property+prop_emptyListInCharacterizingSet :: NonMinimalMealy -> Int -> Int -> Property prop_emptyListInCharacterizingSet (NonMinimalMealy automaton) s1 s2 =     statesAreEquivalent automaton s1 s2         && s1             /= s2-                ==> []-                `Set.member` globalCharacterizingSet automaton+        ==> []+            `Set.member` globalCharacterizingSet automaton  -- Two states that are not equivalent can be distinguished.-prop_existsDistinguishingSequence :: Mealy State Input Output -> State -> State -> Property+prop_existsDistinguishingSequence :: Mealy Input Output -> Int -> Int -> Property prop_existsDistinguishingSequence (Mealy automaton) s1 s2 =-    not (statesAreEquivalent automaton s1 s2)-        ==> output1-        /= output2-        && output1 /= []-        && output2 /= []+    not (statesAreEquivalent automaton s1 s2) ==>+        output1+            /= output2+            && output1 /= []+            && output2 /= []   where     dist = distinguish automaton s1 s2     (_, output1) = runIdentity $ walk (update automaton s1) dist@@ -47,7 +49,7 @@  -- The map returned by 'mealyTransitions' is equivalent to the 'mealyLambda' -- and 'mealyDelta' functions of the automaton.-prop_mappingEquivalentToFunctions :: Mealy State Input Output -> Bool+prop_mappingEquivalentToFunctions :: Mealy Input Output -> Bool prop_mappingEquivalentToFunctions (Mealy automaton) =     let transs = transitions automaton         alphabet = Set.toList $ inputs automaton@@ -62,7 +64,7 @@      in mapOutputs == funOutputs  -- The access sequences returned by 'mealyAccessSequences' cover all reachable states.-prop_completeAccessSequences :: Mealy State Input Output -> Property+prop_completeAccessSequences :: Mealy Input Output -> Property prop_completeAccessSequences (Mealy automaton) = sts == rsts ==> allin   where     seqs = accessSequences automaton@@ -71,11 +73,12 @@     allin = all (`Map.member` seqs) rsts  -- The access sequences returned by 'mealyAccessSequences' are the shortest-prop_shortestAccessSequences :: Mealy State Input Output -> State -> State -> Property+prop_shortestAccessSequences :: Mealy Input Output -> Int -> Int -> Property prop_shortestAccessSequences (Mealy automaton) s1 s2 =     s1 `Set.member` rsts         && s2 `Set.member` rsts-        && existsS1toS2 ==> List.length seq2 <= List.length seq1 + 1+        && existsS1toS2+        ==> List.length seq2 <= List.length seq1 + 1   where     rsts = reachable automaton     transs = transitions automaton@@ -91,19 +94,84 @@         Nothing -> False         Just _ -> True +{- | A counter modulo 5 that outputs 'Y' when input 'A' makes it wrap around and+'X' otherwise; every other input resets it.+-}+counter :: MealyAutomaton Int Input Output+counter = mkMealyAutomaton delta lambda (Set.fromList [0 .. 4]) 0+  where+    delta s A = (s + 1) `mod` 5+    delta _ _ = 0+    lambda 4 A = Y+    lambda _ _ = X++-- | 'counter' with its states renumbered, so a different but equivalent automaton.+renumberedCounter :: MealyAutomaton Int Input Output+renumberedCounter = mkMealyAutomaton delta lambda (Set.fromList [10 .. 14]) 10+  where+    delta s A = 10 + (s - 10 + 1) `mod` 5+    delta _ _ = 10+    lambda 14 A = Y+    lambda _ _ = X++-- | A single state that always outputs 'X'.+oneState :: MealyAutomaton Int Input Output+oneState = mkMealyAutomaton (\_ _ -> 0) (\_ _ -> X) (Set.fromList [0]) 0++-- | The outputs of an automaton on a word, from its initial state.+run :: MealyAutomaton Int Input Output -> [Input] -> [Output]+run aut = snd . walkPure (resetPure aut)++{- | The word 'difference' returns is a shortest witness: the two automata+differ on its last output, and agree on every word one symbol shorter. Outputs+are prefix-closed, so they then agree on every shorter word too. Witnesses of+more than 5 symbols are only checked for the first part, to keep the+enumeration small.+-}+prop_differenceIsShortestWitness :: Mealy Input Output -> Mealy Input Output -> Property+prop_differenceIsShortestWitness (Mealy a) (Mealy b) = case difference a b of+    Nothing -> property True+    Just w ->+        let (oa, ob) = (run a w, run b w)+            shorter = replicateM (length w - 1) [minBound .. maxBound]+            agreeOnShorter = length w > 5 || all (\v -> run a v == run b v) shorter+         in (last oa /= last ob) === True .&&. agreeOnShorter === True++-- | An automaton has no difference with itself.+prop_noDifferenceWithItself :: Mealy Input Output -> Property+prop_noDifferenceWithItself (Mealy a) = difference a a === Nothing+ spec :: Spec spec = do+    describe "BlackBox.difference" $ do+        it "finds the shortest word on which the counter and a one-state automaton differ" $ do+            let w = difference counter oneState+            w `shouldBe` Just [A, A, A, A, A]+            fmap (run counter) w `shouldBe` Just [X, X, X, X, Y]+        it "finds no difference between an automaton and itself" $+            difference counter counter `shouldBe` Nothing+        it "finds no difference between equivalent automata with different states" $+            difference counter renumberedCounter `shouldBe` Nothing+        it "returns a shortest witness" $+            property prop_differenceIsShortestWitness+        it "returns nothing for an automaton compared with itself" $+            property prop_noDifferenceWithItself+     describe "Blackbox.distinguish for MealyAutomaton" $         context "if 2 automatons states are not equivalent" $             it "returns an input sequence that distinguishes them" $-                property-                    prop_existsDistinguishingSequence+                property $ \aut ->+                    forAll genState $ \s1 ->+                        forAll genState $ \s2 ->+                            prop_existsDistinguishingSequence aut s1 s2      describe "BlackBox.globalCharacterizingSet for MealyAutomaton" $         context "if the automaton contains at least 2 equivalent states" $             it "returns a set that contains the empty list" $-                property-                    prop_emptyListInCharacterizingSet+                property $ \aut ->+                    forAll genState $ \s1 ->+                        forAll genState $ \s2 ->+                            prop_emptyListInCharacterizingSet aut s1 s2      describe "MealyAutomaton.mealyTransitions" $         it "returns a map equivalent to the transition and output functions of the model" $@@ -116,5 +184,7 @@                 prop_completeAccessSequences          it "returns a map from reachable states to shortest list of inputs that access them" $-            property-                prop_shortestAccessSequences+            property $ \aut ->+                forAll genState $ \s1 ->+                    forAll genState $ \s2 ->+                        prop_shortestAccessSequences aut s1 s2

@@ -0,0 +1,129 @@+-- | This module tests the DOT parser and the table encoding used by haal-gen.+module DotSpec (+    spec,+)+where++import Data.Char (chr, ord)+import Data.Either (isLeft)+import Data.List (isInfixOf)+import qualified Data.Map as Map+import qualified Data.Set as Set+import Haal.Automaton.MealyAutomaton (+    MealyAutomaton,+    mealyTransitions,+    mkMealyAutomatonTable,+ )+import Haal.BlackBox (initial, states)+import Haal.Dot+import Test.Hspec (Spec, describe, it, shouldBe, shouldSatisfy)+import Test.QuickCheck (Property, counterexample, property, (===))+import Utils (Input, Mealy (..), Output)++-- A small automaton whose states and symbols appear out of alphabetical order.+smallDot :: String+smallDot =+    unlines+        [ "digraph g {"+        , "\t__start0 [label=\"\" shape=none];"+        , "\ts0 [label=\"s0\"];"+        , "\ts0 -> s2 [label=\"b/x\"];"+        , "\ts0 -> s1 [label=\"a/y\"];"+        , "\ts1 -> s1 [label=\"b/x\"];"+        , "\ts1 -> s0 [label=\"a/x\"];"+        , "\ts2 -> s2 [label=\"a/y\"];"+        , "\ts2 -> s0 [label=\"b/y\"];"+        , "\t__start0 -> s0;"+        , "}"+        ]++-- 'smallDot' with the line of one transition replaced.+smallDotWith :: String -> String -> String+smallDotWith old new = unlines [if l == old then new else l | l <- lines smallDot]++-- Encode an automaton with states 0 .. n - 1 as tables, without 'Haal.Dot'.+-- 'mealyTransitions' is ordered by (state, input), which is row-major order.+encode :: MealyAutomaton Int Input Output -> (Int, String, String)+encode m = (Set.size (states m), map (chr . fst) entries, map (chr . fromEnum . snd) entries)+  where+    entries = Map.elems (mealyTransitions m)++prop_tableRoundTrip :: Mealy Input Output -> Property+prop_tableRoundTrip (Mealy m) =+    let (n, deltaTable, lambdaTable) = encode m+     in mkMealyAutomatonTable n (initial m) deltaTable lambdaTable === Right m++-- Every transition of a serialized automaton is reproduced by its table.+prop_mealyTableMatchesParsed :: Mealy Input Output -> Property+prop_mealyTableMatchesParsed (Mealy m) =+    case mealyToDot m >>= parseDot of+        Left err -> counterexample err False+        Right pm -> case mealyTable pm of+            Left err -> counterexample err False+            Right t ->+                let index names = Map.fromList (zip names [0 :: Int ..])+                    stateIdx = index (parsedStates pm)+                    inputIdx = index (parsedInputs pm)+                    outputIdx = index (parsedOutputs pm)+                    n = length (parsedStates pm)+                    k = length (parsedInputs pm)+                    keys = [(s, i) | s <- [0 .. n - 1], i <- [0 .. k - 1]]+                    decoded =+                        Map.fromList (zip keys (zip (map ord (tableDelta t)) (map ord (tableLambda t))))+                    expected =+                        Map.fromList+                            [ ((stateIdx Map.! src, inputIdx Map.! inp), (stateIdx Map.! dst, outputIdx Map.! out))+                            | (src, inp, dst, out) <- parsedTrans pm+                            ]+                 in (tableStates t, length (tableDelta t), length (tableLambda t), decoded)+                        === (n, n * k, n * k, expected)++spec :: Spec+spec = do+    describe "MealyAutomaton.mkMealyAutomatonTable" $ do+        it "rebuilds an automaton from its tables" $+            property prop_tableRoundTrip+        it "rejects tables of the wrong length" $+            (mkMealyAutomatonTable 1 0 "\0\0\0" "\0\0\0\0" :: Either String (MealyAutomaton Int Input Output))+                `shouldSatisfy` isLeft+        it "rejects transitions to states that do not exist" $+            (mkMealyAutomatonTable 1 0 "\0\0\0\1" "\0\0\0\0" :: Either String (MealyAutomaton Int Input Output))+                `shouldSatisfy` isLeft+        it "rejects outputs that do not exist" $+            (mkMealyAutomatonTable 1 0 "\0\0\0\0" "\0\0\0\4" :: Either String (MealyAutomaton Int Input Output))+                `shouldSatisfy` isLeft+        it "rejects an initial state that does not exist" $+            (mkMealyAutomatonTable 1 1 "\0\0\0\0" "\0\0\0\0" :: Either String (MealyAutomaton Int Input Output))+                `shouldSatisfy` isLeft+        it "rejects an automaton without states" $+            (mkMealyAutomatonTable 0 0 "" "" :: Either String (MealyAutomaton Int Input Output))+                `shouldSatisfy` isLeft++    describe "Dot.parseDot" $+        it "keeps states and symbols in order of first appearance" $+            fmap (\pm -> (parsedStates pm, parsedInputs pm, parsedOutputs pm)) (parseDot smallDot)+                `shouldBe` Right (["s0", "s2", "s1"], ["b", "a"], ["x", "y"])++    describe "Dot.mealyTable" $ do+        it "encodes a small automaton in row-major order" $+            (parseDot smallDot >>= mealyTable)+                `shouldBe` Right (MealyTable 3 "\1\2\0\1\2\0" "\0\1\1\1\0\0")+        it "reproduces every transition of a serialized automaton" $+            property prop_mealyTableMatchesParsed+        it "rejects an automaton with a missing transition" $+            (parseDot (smallDotWith "\ts2 -> s0 [label=\"b/y\"];" "") >>= mealyTable)+                `shouldSatisfy` either ("Incomplete" `isInfixOf`) (const False)+        it "rejects an automaton with conflicting transitions" $+            (parseDot (smallDot ++ "\ts2 -> s1 [label=\"b/y\"];\n") >>= mealyTable)+                `shouldSatisfy` either ("Nondeterministic" `isInfixOf`) (const False)+        it "accepts a duplicated identical transition" $+            (parseDot (smallDot ++ "\ts2 -> s0 [label=\"b/y\"];\n") >>= mealyTable)+                `shouldBe` (parseDot smallDot >>= mealyTable)++    describe "Dot.generateModule" $ do+        it "builds the automaton from tables" $+            (parseDot smallDot >>= generateModule "Small" "small")+                `shouldSatisfy` either (const False) ("mkMealyAutomatonTable 3 0 deltaTable lambdaTable" `isInfixOf`)+        it "rejects an incomplete automaton" $+            (parseDot (smallDotWith "\ts2 -> s0 [label=\"b/y\"];" "") >>= generateModule "Small" "small")+                `shouldSatisfy` isLeft

@@ -3,35 +3,100 @@ ) where  import Control.Monad.Reader-import Haal.EquivalenceOracle.WMethod (wmethodSuiteSize)+import qualified Data.Set as Set+import Haal.Automaton.MealyAutomaton (MealyAutomaton, mkMealyAutomaton)+import Haal.BlackBox (states)+import Haal.EquivalenceOracle.WMethod (+    RandomWMethodConfig (..),+    WMethodConfig (..),+    mkRandomWMethod,+    mkWMethod,+    wmethodSuiteSize,+ )+import Haal.EquivalenceOracle.WpMethod (+    RandomWpMethodConfig (..),+    WpMethodConfig (..),+    mkRandomWpMethod,+    mkWpMethod,+ ) import Haal.Experiment-import Test.Hspec (Spec, context, describe, it)+import Haal.Learning.LMstar (LMstarConfig (..), mkLMstar)+import System.Random (mkStdGen)+import Test.Hspec (Spec, context, describe, it, shouldBe, shouldNotBe, shouldSatisfy) import Test.QuickCheck (Property, property, (==>)) import Utils  -- Generic identity and difference properties-prop_identity :: (OracleWrapper w oracle) => Mealy State Input Output -> w -> Bool+prop_identity :: (OracleWrapper w oracle) => Mealy Input Output -> w -> Bool prop_identity (Mealy aut) w = ([], []) == snd (runReader (findCex (unwrap w) aut) aut) -prop_difference :: (OracleWrapper w oracle) => Mealy State Input Output -> Mealy State Input Output -> w -> Property+prop_difference :: (OracleWrapper w oracle) => Mealy Input Output -> Mealy Input Output -> w -> Property prop_difference (Mealy aut1) (Mealy aut2) w =     aut1 /= aut2 ==> ([], []) /= snd (runReader (findCex (unwrap w) aut1) aut2)  -- WMethod-specific cardinality law-prop_WMethodCardinality :: ArbWMethod -> Mealy State Input Output -> Bool+prop_WMethodCardinality :: ArbWMethod -> Mealy Input Output -> Bool prop_WMethodCardinality (ArbWMethod wm) (Mealy aut) =     length (snd (testSuite wm aut)) == wmethodSuiteSize wm aut +{- | A counter modulo 5 that outputs 'Y' when input 'A' makes it wrap around and+'X' otherwise; every other input resets it. No single input tells its states+apart, so the first hypothesis of LM* has one state.+-}+counter :: MealyAutomaton Int Input Output+counter = mkMealyAutomaton delta lambda (Set.fromList [0 .. 4]) 0+  where+    delta s A = (s + 1) `mod` 5+    delta _ _ = 0+    lambda 4 A = Y+    lambda _ _ = X++-- | A hypothesis with a single state, which always outputs 'X'.+oneState :: MealyAutomaton Int Input Output+oneState = mkMealyAutomaton (\_ _ -> 0) (\_ _ -> X) (Set.fromList [0]) 0++-- | The test suite an oracle generates for the one-state hypothesis.+suiteForOneState :: (EquivalenceOracle oracle) => Either String oracle -> [[Input]]+suiteForOneState = either error (\o -> snd (testSuite o oneState))++-- | The counterexample an oracle finds for the one-state hypothesis of 'counter'.+cexForOneState :: (EquivalenceOracle oracle) => Either String oracle -> [Input]+cexForOneState = either error (\o -> fst (snd (runReader (findCex o oneState) counter)))+ spec :: Spec spec = do+    describe "A hypothesis with a single state" $ do+        -- Its characterizing set is empty. The oracles used to build no test+        -- words from it (W, Wp) or crash on it (random Wp).+        it "gets a non-empty W-method test suite" $+            suiteForOneState (mkWMethod (WMethodConfig 1)) `shouldNotBe` []+        it "gets a non-empty Wp-method test suite" $+            suiteForOneState (mkWpMethod (WpMethodConfig 1)) `shouldNotBe` []+        -- Summing the lengths generates every test word, which is where the+        -- random Wp-method crashed.+        it "gets a non-empty random W-method test suite" $+            sum (map length (suiteForOneState (mkRandomWMethod (RandomWMethodConfig (mkStdGen 1) 20 6))))+                `shouldSatisfy` (> 0)+        it "gets a non-empty random Wp-method test suite" $+            sum (map length (suiteForOneState (mkRandomWpMethod (RandomWpMethodConfig (mkStdGen 1) 4 3 20))))+                `shouldSatisfy` (> 0)+        it "is refuted by the W-method with enough extra states" $+            cexForOneState (mkWMethod (WMethodConfig 4)) `shouldNotBe` []+        it "is refuted by the Wp-method with enough extra states" $+            cexForOneState (mkWpMethod (WpMethodConfig 4)) `shouldNotBe` []+        it "does not stop LM* from learning all states of the counter" $ do+            let oracle = either error id (mkWMethod (WMethodConfig 4))+                model = runExperiment (experiment (mkLMstar Star) oracle) counter+            Set.size (states model) `shouldBe` 5+     describe "WMethod Equivalence Oracle" $ do         context "when two automatons differ" $             it "WMethod returns Just" $-                property (prop_difference :: Mealy State Input Output -> Mealy State Input Output -> ArbWMethod -> Property)+                property (prop_difference :: Mealy Input Output -> Mealy Input Output -> ArbWMethod -> Property)          context "when two automatons are the same" $             it "WMethod returns Nothing" $-                property (prop_identity :: Mealy State Input Output -> ArbWMethod -> Bool)+                property (prop_identity :: Mealy Input Output -> ArbWMethod -> Bool)          it "computes the correct WMethod test suite size" $             property prop_WMethodCardinality@@ -39,44 +104,44 @@     describe "WpMethod Equivalence Oracle" $ do         context "when two automatons differ" $             it "WpMethod returns Just" $-                property (prop_difference :: Mealy State Input Output -> Mealy State Input Output -> ArbWpMethod -> Property)+                property (prop_difference :: Mealy Input Output -> Mealy Input Output -> ArbWpMethod -> Property)          context "when two automatons are the same" $             it "WpMethod returns Nothing" $-                property (prop_identity :: Mealy State Input Output -> ArbWpMethod -> Bool)+                property (prop_identity :: Mealy Input Output -> ArbWpMethod -> Bool)      describe "RandomWords Equivalence Oracle" $ do         context "when two automatons differ" $             it "RandomWords returns Just" $-                property (prop_difference :: Mealy State Input Output -> Mealy State Input Output -> ArbRandomWords -> Property)+                property (prop_difference :: Mealy Input Output -> Mealy Input Output -> ArbRandomWords -> Property)          context "when two automatons are the same" $             it "RandomWords returns Nothing" $-                property (prop_identity :: Mealy State Input Output -> ArbRandomWords -> Bool)+                property (prop_identity :: Mealy Input Output -> ArbRandomWords -> Bool)      describe "RandomWalk Equivalence Oracle" $ do         context "when two automatons differ" $             it "RandomWalk returns Just" $-                property (prop_difference :: Mealy State Input Output -> Mealy State Input Output -> ArbRandomWalk -> Property)+                property (prop_difference :: Mealy Input Output -> Mealy Input Output -> ArbRandomWalk -> Property)          context "when two automatons are the same" $             it "RandomWalk returns Nothing" $-                property (prop_identity :: Mealy State Input Output -> ArbRandomWalk -> Bool)+                property (prop_identity :: Mealy Input Output -> ArbRandomWalk -> Bool)      describe "RandomWMethod Equivalence Oracle" $ do         context "when two automatons differ" $             it "RandomWMethod returns Just" $-                property (prop_difference :: Mealy State Input Output -> Mealy State Input Output -> ArbRandomWMethod -> Property)+                property (prop_difference :: Mealy Input Output -> Mealy Input Output -> ArbRandomWMethod -> Property)          context "when two automatons are the same" $             it "RandomWMethod returns Nothing" $-                property (prop_identity :: Mealy State Input Output -> ArbRandomWMethod -> Bool)+                property (prop_identity :: Mealy Input Output -> ArbRandomWMethod -> Bool)      describe "RandomWpMethod Equivalence Oracle" $ do         context "when two automatons differ" $             it "RandomWpMethod returns Just" $-                property (prop_difference :: Mealy State Input Output -> Mealy State Input Output -> ArbRandomWpMethod -> Property)+                property (prop_difference :: Mealy Input Output -> Mealy Input Output -> ArbRandomWpMethod -> Property)          context "when two automatons are the same" $             it "RandomWpMethod returns Nothing" $-                property (prop_identity :: Mealy State Input Output -> ArbRandomWpMethod -> Bool)+                property (prop_identity :: Mealy Input Output -> ArbRandomWpMethod -> Bool)

@@ -0,0 +1,141 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}++{- | Regression tests for the reset contract between the library and a SUL.++Active automata learning assumes that queries are independent, i.e. that the+SUL is reset before every membership query and every equivalence test case.+These tests check that the learned model does not depend on the state the SUL+is left in by earlier queries, or on the state it is handed over in.+-}+module SULSpec (+    spec,+) where++import Control.Exception (ErrorCall (..), evaluate)+import Control.Monad.Identity (Identity)+import Data.IORef (IORef, modifyIORef', newIORef, readIORef, writeIORef)+import qualified Data.List as List+import qualified Data.Set as Set+import Haal.Automaton.MealyAutomaton (MealyAutomaton, mkMealyAutomaton)+import Haal.BlackBox+import Haal.EquivalenceOracle.WpMethod (WpMethod, WpMethodConfig (..), mkWpMethod)+import Haal.Experiment (experiment, runExperiment, runExperimentT)+import Haal.Learning.LMstar (LMstarConfig (..), mkLMstar)+import Test.Hspec (Spec, describe, it, shouldThrow)+import Test.QuickCheck (Property, ioProperty, property, within, (===))+import Utils (Input (..), Mealy (..), Output (..))++{- | A SUL that wraps a stateful system. The automaton lives behind an 'IORef',+so 'step' and 'reset' mutate it and hand back the same handle, just like a+driver for a real process or socket would.+-}+newtype RefSUL i o = RefSUL (IORef (MealyAutomaton Int i o))++instance SUL RefSUL IO where+    step h@(RefSUL ref) i = do+        aut <- readIORef ref+        let (aut', o) = stepPure aut i+        writeIORef ref aut'+        return (h, o)+    reset h@(RefSUL ref) = do+        modifyIORef' ref resetPure+        return h++type Model = MealyAutomaton Int Input Output++{- | Without resets the answers to queries depend on earlier queries, so the+oracle can keep finding counterexamples that refinement never fixes, and the+experiment never terminates. Bound every property so that this shows up as a+failure instead of a hang.+-}+terminates :: Property -> Property+terminates = within 5000000++oracle :: WpMethod+oracle = either error id (mkWpMethod (WpMethodConfig 1))++-- | Learn an automaton purely, using the automaton itself as the SUL.+learnPure :: LMstarConfig -> Model -> Model+learnPure cfg aut = runExperiment (experiment (mkLMstar cfg) oracle) aut++-- | Learn an automaton through a 'RefSUL' wrapping it.+learnRef :: LMstarConfig -> Model -> IO Model+learnRef cfg aut = do+    ref <- newIORef aut+    runExperimentT (experiment (mkLMstar cfg) oracle) (RefSUL ref)++{- | A stateful SUL must learn the same model as its pure counterpart. Both+runs ask the same queries, so the answers, and the models, can only differ if+some query is not preceded by a reset.+-}+prop_statefulMatchesPure :: LMstarConfig -> Mealy Input Output -> Property+prop_statefulMatchesPure cfg (Mealy aut) = terminates $ ioProperty $ do+    let aut0 = resetPure aut+    learned <- learnRef cfg aut0+    return (learned === learnPure cfg aut0)++{- | The learned model must not depend on the current state of the SUL it is+given; learning has to start from the initial state. The 'Arbitrary' instance+of 'Mealy' picks a random current state.+-}+prop_currentStateIrrelevant :: LMstarConfig -> Mealy Input Output -> Property+prop_currentStateIrrelevant cfg (Mealy aut) =+    terminates $+        learnPure cfg aut === learnPure cfg (resetPure aut)++{- | A pure SUL that overrides 'query'. With @Correct@ the override computes the+same outputs as the default; with @DropsOutput@ it loses the last output,+breaking the contract of 'query'.+-}+data Override = Correct | DropsOutput++data OverridingSUL i o = OverridingSUL Override (MealyAutomaton Int i o)++instance SUL OverridingSUL Identity where+    step (OverridingSUL ov aut) i =+        let (aut', o) = stepPure aut i+         in return (OverridingSUL ov aut', o)+    reset (OverridingSUL ov aut) = return (OverridingSUL ov (resetPure aut))+    query (OverridingSUL ov aut) xs =+        let os = snd (walkPure (resetPure aut) xs)+         in return $ case ov of+                Correct -> os+                DropsOutput -> List.take (length os - 1) os++-- | A small fixed automaton: it counts @A@s modulo 3 and outputs the count.+counter :: Model+counter = mkMealyAutomaton delta lambda (Set.fromList [0, 1, 2]) 0+  where+    delta s A = (s + 1) `mod` 3+    delta s _ = s+    lambda s A = [X, Y, Z] !! ((s + 1) `mod` 3)+    lambda _ _ = W++learnOverriding :: Override -> Model -> Model+learnOverriding ov aut =+    runExperiment (experiment (mkLMstar Star) oracle) (OverridingSUL ov aut)++isContractViolation :: ErrorCall -> Bool+isContractViolation (ErrorCall msg) = "one output per input" `List.isInfixOf` msg++spec :: Spec+spec = do+    describe "Overriding query" $ do+        it "a correct override learns the same model as the default" $+            learnOverriding Correct counter == learnPure Star counter+        it "an override returning too few outputs fails with a clear error" $+            evaluate (length (show (learnOverriding DropsOutput counter)))+                `shouldThrow` isContractViolation++    describe "Learning through a stateful SUL" $ do+        it "LM* learns the same model as through a pure SUL" $+            property (prop_statefulMatchesPure Star)+        it "LM+ learns the same model as through a pure SUL" $+            property (prop_statefulMatchesPure Plus)++    describe "Learning from a SUL in a non-initial state" $ do+        it "LM* learns the same model as from the initial state" $+            property (prop_currentStateIrrelevant Star)+        it "LM+ learns the same model as from the initial state" $+            property (prop_currentStateIrrelevant Plus)

@@ -0,0 +1,99 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}++-- | Tests for the statistics of an experiment.+module StatisticsSpec (+    spec,+) where++import qualified Control.Foldl as L+import Control.Monad (forM_)+import Data.IORef (IORef, modifyIORef', newIORef, readIORef, writeIORef)+import qualified Data.Set as Set+import Haal.Automaton.MealyAutomaton (MealyAutomaton, mkMealyAutomaton)+import Haal.BlackBox+import Haal.EquivalenceOracle.WpMethod (WpMethod, WpMethodConfig (..), mkWpMethod)+import Haal.Experiment (experimentWith, measuredExperiment, runExperiment, runExperimentT)+import Haal.Learning.LMstar (LMstarConfig (..), mkLMstar)+import Haal.Statistics+import Test.Hspec (Spec, describe, it, shouldBe, shouldSatisfy)++data I = Tick | Clear deriving (Show, Eq, Ord, Enum, Bounded)+data O = Quiet | Wrap deriving (Show, Eq, Ord, Enum, Bounded)++{- | A counter modulo 5 that outputs 'Wrap' only when it wraps around. LM*'s+first hypothesis cannot tell the states apart, so learning it takes a few+counterexamples, which exercises both phases.+-}+counter :: MealyAutomaton Int I O+counter = mkMealyAutomaton delta lambda (Set.fromList [0 .. 4]) 0+  where+    delta s Tick = (s + 1) `mod` 5+    delta _ Clear = 0+    lambda 4 Tick = Wrap+    lambda _ _ = Quiet++-- | Depth 4: enough to refute LM*'s one-state first hypothesis of the 5-state 'counter'.+oracle :: WpMethod+oracle = either error id (mkWpMethod (WpMethodConfig 4))++{- | A SUL that counts its own resets and steps, per phase, in 'IORef's,+independently of the statistics. Its phase is set from outside. It does not+override 'query', so every query goes through its 'reset' and 'step'.+-}+data Spy i o = Spy+    { spyPhase :: IORef Phase+    , spyCounts :: IORef (Tally, Tally)+    -- ^ resets and steps in the 'Learning' and in the 'Testing' phase+    , spyAut :: MealyAutomaton Int i o+    }++spyTick :: Spy i o -> Int -> Int -> IO ()+spyTick spy r s = do+    p <- readIORef (spyPhase spy)+    let add (Tally r0 s0) = Tally (r0 + r) (s0 + s)+    modifyIORef' (spyCounts spy) $ \(l, t) -> case p of+        Learning -> (add l, t)+        Testing -> (l, add t)++instance SUL Spy IO where+    step spy i = do+        spyTick spy 0 1+        let (aut', o) = stepPure (spyAut spy) i+        return (spy{spyAut = aut'}, o)+    reset spy = do+        spyTick spy 1 0+        return (spy{spyAut = resetPure (spyAut spy)})++spec :: Spec+spec = forM_ [("LM*", Star), ("LM+", Plus)] $ \(name, cfg) -> describe name $ do+    let learner = mkLMstar cfg++    it "counts the same queries and symbols per phase as the SUL counts itself" $ do+        spy <- Spy <$> newIORef Learning <*> newIORef (Tally 0 0, Tally 0 0) <*> pure counter+        events <- newIORef []+        let emit e = do+                case e of+                    PhaseChanged p -> writeIORef (spyPhase spy) p+                    _ -> return ()+                modifyIORef' events (e :)+        _ <- runExperimentT (experimentWith emit learner oracle) spy+        own <- readIORef (spyCounts spy)+        stats <- L.fold statistics . reverse <$> readIORef events+        (learning stats, testing stats) `shouldBe` own+        queries (testing stats) `shouldSatisfy` (> 0)++    it "measuredExperiment gives the same statistics as folding the emitted events" $ do+        events <- newIORef []+        _ <- runExperimentT (experimentWith (\e -> modifyIORef' events (e :)) learner oracle) counter+        folded <- L.fold statistics . reverse <$> readIORef events+        snd (runExperiment (measuredExperiment statistics learner oracle) counter) `shouldBe` folded++    it "combined with another fold, gives the same statistics as on its own" $ do+        let measure stat = runExperiment (measuredExperiment stat learner oracle) counter+            (model, (stats, nEvents)) = measure ((,) <$> statistics <*> L.length)+            (_, alone) = measure statistics+        stats `shouldBe` alone+        nEvents `shouldSatisfy` (> 0)+        rounds stats `shouldSatisfy` (> 0)+        take 1 (hypotheses stats) `shouldBe` [model]

@@ -1,14 +1,16 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE ScopedTypeVariables #-}+ {- HLINT ignore "Use <$>" -}  module Utils (     statesAreEquivalent,+    stateSpace,+    genState,     NonMinimalMealy (..),     Mealy (..),     Input (..),     Output (..),-    State (..),     ArbWMethod (..),     ArbWpMethod (..),     ArbRandomWords (..),@@ -26,8 +28,8 @@ import qualified Data.Set as Set import Haal.Automaton.MealyAutomaton (     MealyAutomaton,-    mkMealyAutomaton,     mealyTransitions,+    mkMealyAutomaton,  ) import Haal.BlackBox import Haal.EquivalenceOracle.RandomWalk (@@ -45,16 +47,16 @@     RandomWMethodConfig (..),     WMethod,     WMethodConfig (..),-    mkWMethod,     mkRandomWMethod,+    mkWMethod,  ) import Haal.EquivalenceOracle.WpMethod (     RandomWpMethod,     RandomWpMethodConfig (..),     WpMethod,     WpMethodConfig (..),-    mkWpMethod,     mkRandomWpMethod,+    mkWpMethod,  ) import Haal.Experiment (EquivalenceOracle) import System.Random@@ -168,25 +170,23 @@ instance OracleWrapper ArbRandomWpMethod RandomWpMethod where     unwrap (ArbRandomWpMethod o) = o -newtype Mealy s i o = Mealy (MealyAutomaton s i o) deriving (Show)+newtype Mealy i o = Mealy (MealyAutomaton Int i o) deriving (Show)  instance     ( Arbitrary i     , Arbitrary o-    , Arbitrary s     , FiniteOrd i     , FiniteOrd o-    , FiniteOrd s     ) =>-    Arbitrary (Mealy s i o)+    Arbitrary (Mealy i o)     where     arbitrary = do-        let sts = [minBound .. maxBound]+        let sts = stateSpace         delta <- generateDelta sts         lambda <- generateLambda sts -        initialState <- arbitrary-        currentState <- arbitrary+        initialState <- elements sts+        currentState <- elements sts          return             ( Mealy@@ -196,23 +196,23 @@                 )             )       where-        generateDelta :: [s] -> Gen (s -> i -> s)+        generateDelta :: [Int] -> Gen (Int -> i -> Int)         generateDelta sts = do             let-                ins = Set.toList $ inputs (undefined :: MealyAutomaton s i o)+                ins = Set.toList $ inputs (undefined :: MealyAutomaton Int i o)                 complete = [(st, inp) | st <- sts, inp <- ins]                 (numS, numI) = Bif.bimap List.length List.length (sts, ins)             matching <- vectorOf (numS * numI) (choose (0, numS - 1))             let stateOutputs = [sts !! index | index <- matching]                 stateMappings = Map.fromList $ List.zip complete stateOutputs-            fallbackState <- arbitrary :: Gen s+            fallbackState <- elements sts             return $ \s i -> Data.Maybe.fromMaybe fallbackState (Map.lookup (s, i) stateMappings) -        generateLambda :: [s] -> Gen (s -> i -> o)+        generateLambda :: [Int] -> Gen (Int -> i -> o)         generateLambda sts = do             let-                ins = Set.toList $ inputs (undefined :: MealyAutomaton s i o)-                outs = Set.toList $ outputs (undefined :: MealyAutomaton s i o)+                ins = Set.toList $ inputs (undefined :: MealyAutomaton Int i o)+                outs = Set.toList $ outputs (undefined :: MealyAutomaton Int i o)                 complete = [(st, inp) | st <- sts, inp <- ins]                 (numS, numI) = Bif.bimap List.length List.length (sts, ins)                 numO = List.length outs@@ -224,28 +224,34 @@  data Input = A | B | C | D deriving (Show, Eq, Ord, Enum, Bounded) data Output = X | Y | Z | W deriving (Show, Eq, Ord, Enum, Bounded)-data State = S0 | S1 | S2 | S3 | S4 | S5 | S6 | S7 deriving (Show, Eq, Ord, Enum, Bounded) --- Arbitrary instances for Input, Output, and State+{- | The states of the generated test automata. 'NonMinimalMealy' needs at+least 6-7 states, otherwise too many test cases are discarded.+-}+stateSpace :: [Int]+stateSpace = [0 .. 7]++-- | Generate a state that belongs to 'stateSpace'.+genState :: Gen Int+genState = elements stateSpace++-- Arbitrary instances for Input and Output instance Arbitrary Input where     arbitrary = elements [A, B, C, D]  instance Arbitrary Output where     arbitrary = elements [X, Y, Z, W] -instance Arbitrary State where-    arbitrary = elements [S0, S1, S2, S3, S4, S5, S6, S7]--newtype NonMinimalMealy = NonMinimalMealy (MealyAutomaton State Input Output) deriving (Show)+newtype NonMinimalMealy = NonMinimalMealy (MealyAutomaton Int Input Output) deriving (Show)  instance Arbitrary NonMinimalMealy where     arbitrary = do-        let sts = [minBound .. maxBound]+        let sts = stateSpace         delta <- generateDelta sts         lambda <- generateLambda sts -        initialState <- arbitrary :: Gen State-        currentState <- arbitrary :: Gen State+        initialState <- elements sts+        currentState <- elements sts          return             ( NonMinimalMealy@@ -255,10 +261,10 @@                 )             )       where-        generateDelta :: [State] -> Gen (State -> Input -> State)+        generateDelta :: [Int] -> Gen (Int -> Input -> Int)         generateDelta sts = do             let-                ins = Set.toList $ inputs (undefined :: MealyAutomaton State Input Output)+                ins = Set.toList $ inputs (undefined :: MealyAutomaton Int Input Output)                 (numS, numI) = Bif.bimap List.length List.length (sts, ins)                 same = numS `div` 2                 nonMinimal = [(st, inp) | st <- take same sts, inp <- ins]@@ -268,14 +274,14 @@             let stateOutputs1 = [sts !! index | index <- concat (replicate same nonMinimalMatching1)]                 stateOutputs2 = [sts !! index | index <- nonMinimalMatching2]                 nonMinimalMappings = Map.fromList $ List.zip (nonMinimal ++ rest) (stateOutputs1 ++ stateOutputs2)-            fallbackState <- arbitrary :: Gen State+            fallbackState <- elements sts             return $ \s i -> Data.Maybe.fromMaybe fallbackState (Map.lookup (s, i) nonMinimalMappings) -        generateLambda :: [State] -> Gen (State -> Input -> Output)+        generateLambda :: [Int] -> Gen (Int -> Input -> Output)         generateLambda sts = do             let-                ins = Set.toList $ inputs (undefined :: MealyAutomaton State Input Output)-                outs = Set.toList $ outputs (undefined :: MealyAutomaton State Input Output)+                ins = Set.toList $ inputs (undefined :: MealyAutomaton Int Input Output)+                outs = Set.toList $ outputs (undefined :: MealyAutomaton Int Input Output)                 same = numS `div` 2                 nonMinimal = [(st, inp) | st <- take same sts, inp <- ins]                 rest = [(st, inp) | st <- drop same sts, inp <- ins]@@ -290,7 +296,7 @@             return $ \s i -> Data.Maybe.fromMaybe fallbackOutput (Map.lookup (s, i) outputMappings)  -- Two states are equivalent if their delta and lambda functions are equivalent.-statesAreEquivalent :: MealyAutomaton State Input Output -> State -> State -> Bool+statesAreEquivalent :: MealyAutomaton Int Input Output -> Int -> Int -> Bool statesAreEquivalent _ s1 s2 | s1 == s2 = True statesAreEquivalent automaton s1 s2 =     all (\i -> trans Map.! (s1, i) == trans Map.! (s2, i)) (inputs automaton)