From 8a66ccaec5fcc184a6ec6ad299cc3e20bb08fb59 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Fri, 14 Aug 2020 20:11:59 +0200 Subject: [PATCH] Rewrote nominal NL* for better performance, by specialising for Booleans --- bench/Bench.hs | 1 + nominal-lstar.cabal | 1 - src/Angluin.hs | 1 - src/Bollig.hs | 66 +++++++++++++++++++++++++++++++++------------ src/NLStar.hs | 60 ----------------------------------------- 5 files changed, 50 insertions(+), 79 deletions(-) delete mode 100644 src/NLStar.hs diff --git a/bench/Bench.hs b/bench/Bench.hs index 70956b1..73bd42b 100644 --- a/bench/Bench.hs +++ b/bench/Bench.hs @@ -10,6 +10,7 @@ import Gauge.Main.Options myConfig = defaultConfig { quickMode = True , includeFirstIter = True + , csvFile = Just "bench.csv" } main = defaultMainWith myConfig [ diff --git a/nominal-lstar.cabal b/nominal-lstar.cabal index 3a98aaa..6726f91 100644 --- a/nominal-lstar.cabal +++ b/nominal-lstar.cabal @@ -31,7 +31,6 @@ library Examples.Residual, Examples.RunningExample, Examples.Stack, - NLStar, ObservationTable, Teacher, Teachers.Teacher, diff --git a/src/Angluin.hs b/src/Angluin.hs index c286761..7cb098f 100644 --- a/src/Angluin.hs +++ b/src/Angluin.hs @@ -9,7 +9,6 @@ import Data.List (inits, tails) import Debug.Trace import NLambda import Prelude (Bool (..), Maybe (..), id, show, ($), (++), (.)) -import qualified Prelude hiding () justOne :: (Contextual a, NominalType a) => Set a -> Set a justOne s = mapFilter id . orbit [] . element $ s diff --git a/src/Bollig.hs b/src/Bollig.hs index 328cb74..24d5638 100644 --- a/src/Bollig.hs +++ b/src/Bollig.hs @@ -8,8 +8,7 @@ import Teacher import Debug.Trace import NLambda -import Prelude (Bool (..), Int, Maybe (..), fst, snd, ($), (++), (.), (<=)) -import qualified Prelude hiding () +import Prelude (Bool (..), Int, Maybe (..), ($), (++), (.)) -- Comparing two graphs of a function is inefficient in NLambda, -- because we do not have a map data structure. (So the only way @@ -21,17 +20,14 @@ import qualified Prelude hiding () brow :: (NominalType i) => Table i Bool -> [i] -> Set [i] brow t is = mapFilter (\((a,b),c) -> maybeIf (eq is a /\ fromBool c) b) t -rfsaClosednessTest3 :: LearnableAlphabet i => State i -> TestResult i -rfsaClosednessTest3 State{..} = case solve (isEmpty defect) of +rfsaClosednessTest :: LearnableAlphabet i => Set (Set [i]) -> State i -> TestResult i +rfsaClosednessTest primesUpp State{..} = case solve (isEmpty defect) of Just True -> Succes Just False -> trace "Not closed" $ Failed defect empty Nothing -> trace "@@@ Unsolved Formula (rfsaClosednessTest) @@@" $ Failed defect empty where defect = filter (\ua -> brow t ua `neq` sum (filter (`isSubsetOf` brow t ua) primesUpp)) ssa - primesUpp = filter (\r -> isNotEmpty r /\ r `neq` sum (filter (`isSubsetOf` r) (allRows \\ orbit [] r))) allRowsUpp - allRowsUpp = map (brow t) ss - allRows = allRowsUpp `union` map (brow t) ssa rfsaConsistencyTest :: LearnableAlphabet i => State i -> TestResult i rfsaConsistencyTest State{..} = case solve (isEmpty defect) of @@ -45,22 +41,58 @@ rfsaConsistencyTest State{..} = case solve (isEmpty defect) of -- Note that we do not have the same type of states as the angluin algorithm. -- We have Set [i] instead of BRow i. (However, They are isomorphic.) -constructHypothesisBollig :: NominalType i => State i -> Automaton (Set [i]) i -constructHypothesisBollig State{..} = automaton q a d i f +constructHypothesisBollig :: NominalType i => Set (Set [i]) -> State i -> Automaton (Set [i]) i +constructHypothesisBollig primesUpp State{..} = automaton q aa d i f where q = primesUpp - a = aa i = filter (`isSubsetOf` brow t []) q f = filter (`contains` []) q d0 = triplesWithFilter (\s a s2 -> maybeIf (brow t s2 `isSubsetOf` brow t (s ++ [a])) (brow t s, a, brow t s2)) ss aa ss d = filter (\(q1, _, q2) -> q1 `member` q /\ q2 `member` q) d0 - primesUpp = filter (\r -> isNotEmpty r /\ r `neq` sum (filter (`isSubsetOf` r) (allRows \\ orbit [] r))) allRowsUpp - allRowsUpp = map (brow t) ss - allRows = allRowsUpp `union` map (brow t) ssa -makeCompleteBollig :: LearnableAlphabet i => TableCompletionHandler i -makeCompleteBollig = makeCompleteWith [rfsaClosednessTest3, rfsaConsistencyTest] +--makeCompleteBollig :: LearnableAlphabet i => TableCompletionHandler i +--makeCompleteBollig = makeCompleteWith [rfsaClosednessTest, rfsaConsistencyTest] learnBollig :: LearnableAlphabet i => Int -> Int -> Teacher i -> Automaton (Set [i]) i -learnBollig k n teacher = learn makeCompleteBollig useCounterExampleMP constructHypothesisBollig teacher initial - where initial = constructEmptyState k n teacher +--learnBollig k n teacher = learn makeCompleteBollig useCounterExampleMP constructHypothesisBollig teacher initial +-- where initial = constructEmptyState k n teacher + +learnBollig k n teacher = learnBolligLoop teacher (constructEmptyState k n teacher) + +learnBolligLoop teacher s1@State{..} = + let + allRowsUpp = map (brow t) ss + allRows = allRowsUpp `union` map (brow t) ssa + primesUpp = filter (\r -> isNotEmpty r /\ r `neq` sum (filter (`isSubsetOf` r) (allRows \\ orbit [] r))) allRowsUpp + + -- No worry, these are computed lazily + closednessRes = rfsaClosednessTest primesUpp s1 + consistencyRes = rfsaConsistencyTest s1 + h = constructHypothesisBollig primesUpp s1 + in + trace "1. Making it rfsa closed" $ + case closednessRes of + Failed newRows _ -> + let state2 = simplify $ addRows teacher newRows s1 in + learnBolligLoop teacher state2 + Succes -> + trace "1. Making it rfsa consistent" $ + case consistencyRes of + Failed _ newColumns -> + let state2 = simplify $ addColumns teacher newColumns s1 in + learnBolligLoop teacher state2 + Succes -> + traceShow h $ + trace "3. Equivalent? " $ + eqloop s1 h + where + eqloop s2 h = case equivalent teacher h of + Nothing -> trace "Yes" h + Just ces -> trace "No" $ + if isTrue . isEmpty $ realces h ces + then eqloop s2 h + else + let s3 = useCounterExampleMP teacher s2 ces in + learnBolligLoop teacher s3 + realces h ces = NLambda.filter (\(ce, a) -> a `neq` accepts h ce) $ membership teacher ces + diff --git a/src/NLStar.hs b/src/NLStar.hs deleted file mode 100644 index e176f17..0000000 --- a/src/NLStar.hs +++ /dev/null @@ -1,60 +0,0 @@ -{-# language RecordWildCards #-} -module NLStar where - -import AbstractLStar -import Angluin -import Bollig -import ObservationTable -import Teacher - -import Debug.Trace -import NLambda -import Prelude hiding (and, curry, filter, lookup, map, not, sum) - -{- This is not NL* from the Bollig et al paper. This is a very naive - approximation. You see, the consistency in their paper is quite weak, - and in fact does not determine a well defined automaton (the constructed - automaton does not even agree with the table of observations). They fix - it by adding counter examples as columns instead of rows. This way the - teacher will point out inconsistencies and columns are added then. - - Here, I propose an algorithm which does not check consistency at all! - Sounds a bit crazy, but the teacher kind of takes care of that. Of course - I do not know whether this will terminate. But it's nice to experiment with. - Also I do not 'minimize' the NFA by taking only prime rows. Saves a lot of - checking but makes the result not minimal (whatever that would mean). It - is quite fast, however ;-). - - THIS IS NOT USED IN THE PAPER. --} - --- We can determine its completeness with the following --- It returns all witnesses (of the form sa) for incompleteness - -{- Disabled, didn't work anymore, and I don't know what it does -nonDetClosednessTest :: NominalType i => State i -> TestResult i -nonDetClosednessTest State{..} = case solve (isEmpty defect) of - Just True -> Succes - Just False -> trace "Not closed" $ Failed defect empty - where - allRows = map (row t) ss - hasSum r = r `eq` rowUnion (sublangs r allRows) - defect = filter (not . hasSum . row t) ssa - -constructHypothesisNonDet :: NominalType i => State i -> Automaton (BRow i) i -constructHypothesisNonDet State{..} = automaton q a d i f - where - q = map (row t) ss - a = aa - d = triplesWithFilter (\s a s2 -> maybeIf (row t s2 `sublang` rowa t s a) (row t s, a, row t s2)) ss aa ss - i = singleton $ row t [] - f = mapFilter (\s -> maybeIf (tableAt t s []) (row t s)) ss - -makeCompleteNonDet :: LearnableAlphabet i => TableCompletionHandler i -makeCompleteNonDet = makeCompleteWith [nonDetClosednessTest] - --- Default: use counter examples in columns, which is slightly faster -learnNonDet :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i -learnNonDet teacher = learn makeCompleteNonDet useCounterExampleMP constructHypothesisNonDet teacher initial - where initial = constructEmptyState 0 0 teacher --}