diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -1,2 +1,3 @@ import Distribution.Simple + main = defaultMain diff --git a/app/HaalGen.hs b/app/HaalGen.hs --- a/app/HaalGen.hs +++ b/app/HaalGen.hs @@ -1,37 +1,39 @@ --- | haal-gen: generate a Haskell module from a Mealy automaton in DOT format. --- --- Usage: --- haal-gen --- --- The generated module is written to stdout. +{- | haal-gen: generate a Haskell module from a Mealy automaton in DOT format. + +Usage: + haal-gen + +The generated module is written to stdout. +-} module Main (main) where import System.Environment (getArgs) import System.Exit (exitFailure, exitSuccess) import System.IO (hPutStrLn, stderr) -import Haal.Dot (parseDot, generateModule, parsedWarnings) +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 " - , "" - , "Arguments:" - , " Path to a DOT file (AALpy or LearnLib format)" - , " Fully qualified Haskell module name (e.g. My.Module.Name)" - , " Name for the generated automaton value (e.g. myAutomaton)" - , "" - , "Output:" - , " Haskell source is written to stdout; warnings and errors to stderr." - , " The generated module contains typed input/output ADTs and a" - , " MealyAutomaton value, ready to import and use with haal." - , "" - , "Example:" - , " haal-gen model.dot Haal.Models.Foo fooModel > src/Haal/Models/Foo.hs" - ] +helpText = + unlines + [ "haal-gen - generate a Haskell module from a Mealy automaton in DOT format" + , "" + , "Usage:" + , " haal-gen " + , "" + , "Arguments:" + , " Path to a DOT file (AALpy or LearnLib format)" + , " Fully qualified Haskell module name (e.g. My.Module.Name)" + , " Name for the generated automaton value (e.g. myAutomaton)" + , "" + , "Output:" + , " Haskell source is written to stdout; warnings and errors to stderr." + , " The generated module contains typed input/output ADTs and a" + , " MealyAutomaton value, ready to import and use with haal." + , "" + , "Example:" + , " haal-gen model.dot Haal.Models.Foo fooModel > src/Haal/Models/Foo.hs" + ] main :: IO () main = do @@ -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 diff --git a/bench/Bench/BlackBox.hs b/bench/Bench/BlackBox.hs --- a/bench/Bench/BlackBox.hs +++ b/bench/Bench/BlackBox.hs @@ -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 + ] ] - ] diff --git a/bench/Bench/Dot.hs b/bench/Bench/Dot.hs --- a/bench/Bench/Dot.hs +++ b/bench/Bench/Dot.hs @@ -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 + ] diff --git a/bench/Bench/EndToEnd.hs b/bench/Bench/EndToEnd.hs --- a/bench/Bench/EndToEnd.hs +++ b/bench/Bench/EndToEnd.hs @@ -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 + ] ] - ] diff --git a/bench/Bench/EquivalenceOracle.hs b/bench/Bench/EquivalenceOracle.hs --- a/bench/Bench/EquivalenceOracle.hs +++ b/bench/Bench/EquivalenceOracle.hs @@ -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) + ] ] ] - ] diff --git a/bench/Main.hs b/bench/Main.hs --- a/bench/Main.hs +++ b/bench/Main.hs @@ -8,9 +8,10 @@ import Bench.EquivalenceOracle (equivalenceOracleBenchmarks) main :: IO () -main = defaultMain - [ blackBoxBenchmarks - , equivalenceOracleBenchmarks - , dotBenchmarks - , endToEndBenchmarks - ] +main = + defaultMain + [ blackBoxBenchmarks + , equivalenceOracleBenchmarks + , dotBenchmarks + , endToEndBenchmarks + ] diff --git a/examples/demo.hs b/examples/demo.hs --- a/examples/demo.hs +++ b/examples/demo.hs @@ -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 diff --git a/examples/div.hs b/examples/div.hs --- a/examples/div.hs +++ b/examples/div.hs @@ -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 () diff --git a/examples/io.hs b/examples/io.hs --- a/examples/io.hs +++ b/examples/io.hs @@ -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 diff --git a/examples/website.hs b/examples/website.hs --- a/examples/website.hs +++ b/examples/website.hs @@ -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 diff --git a/haal.cabal b/haal.cabal --- a/haal.cabal +++ b/haal.cabal @@ -1,11 +1,11 @@ cabal-version: 2.2 --- This file has been generated from package.yaml by hpack version 0.38.1. +-- This file has been generated from package.yaml by hpack version 0.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 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 diff --git a/src/Haal/Automaton/DFA.hs b/src/Haal/Automaton/DFA.hs deleted file mode 100644 --- a/src/Haal/Automaton/DFA.hs +++ /dev/null @@ -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 diff --git a/src/Haal/Automaton/MealyAutomaton.hs b/src/Haal/Automaton/MealyAutomaton.hs --- a/src/Haal/Automaton/MealyAutomaton.hs +++ b/src/Haal/Automaton/MealyAutomaton.hs @@ -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 diff --git a/src/Haal/Automaton/MooreAutomaton.hs b/src/Haal/Automaton/MooreAutomaton.hs deleted file mode 100644 --- a/src/Haal/Automaton/MooreAutomaton.hs +++ /dev/null @@ -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 diff --git a/src/Haal/BlackBox.hs b/src/Haal/BlackBox.hs --- a/src/Haal/BlackBox.hs +++ b/src/Haal/BlackBox.hs @@ -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 diff --git a/src/Haal/Dot.hs b/src/Haal/Dot.hs --- a/src/Haal/Dot.hs +++ b/src/Haal/Dot.hs @@ -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 \Input@ type whose constructors are the sanitized input symbols, deriving @Show, Eq, Ord, Enum, Bounded@. * A @data \Output@ type, similarly for output symbols. - * A value @valName :: MealyAutomaton Int \Input \Output@. + * A value @valName :: MealyAutomaton Int \Input \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 = diff --git a/src/Haal/EquivalenceOracle/WMethod.hs b/src/Haal/EquivalenceOracle/WMethod.hs --- a/src/Haal/EquivalenceOracle/WMethod.hs +++ b/src/Haal/EquivalenceOracle/WMethod.hs @@ -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 diff --git a/src/Haal/EquivalenceOracle/WpMethod.hs b/src/Haal/EquivalenceOracle/WpMethod.hs --- a/src/Haal/EquivalenceOracle/WpMethod.hs +++ b/src/Haal/EquivalenceOracle/WpMethod.hs @@ -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 diff --git a/src/Haal/Experiment.hs b/src/Haal/Experiment.hs --- a/src/Haal/Experiment.hs +++ b/src/Haal/Experiment.hs @@ -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. diff --git a/src/Haal/Learning/LMstar.hs b/src/Haal/Learning/LMstar.hs --- a/src/Haal/Learning/LMstar.hs +++ b/src/Haal/Learning/LMstar.hs @@ -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 diff --git a/src/Haal/Statistics.hs b/src/Haal/Statistics.hs new file mode 100644 --- /dev/null +++ b/src/Haal/Statistics.hs @@ -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} diff --git a/test/AutomatonSpec.hs b/test/AutomatonSpec.hs --- a/test/AutomatonSpec.hs +++ b/test/AutomatonSpec.hs @@ -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 diff --git a/test/DotSpec.hs b/test/DotSpec.hs new file mode 100644 --- /dev/null +++ b/test/DotSpec.hs @@ -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 diff --git a/test/EquivalenceOracleSpec.hs b/test/EquivalenceOracleSpec.hs --- a/test/EquivalenceOracleSpec.hs +++ b/test/EquivalenceOracleSpec.hs @@ -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) diff --git a/test/SULSpec.hs b/test/SULSpec.hs new file mode 100644 --- /dev/null +++ b/test/SULSpec.hs @@ -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) diff --git a/test/StatisticsSpec.hs b/test/StatisticsSpec.hs new file mode 100644 --- /dev/null +++ b/test/StatisticsSpec.hs @@ -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] diff --git a/test/Utils.hs b/test/Utils.hs --- a/test/Utils.hs +++ b/test/Utils.hs @@ -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)