From 7b41e7d97ca80a4d5c016765ad39a2078086eb74 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Thu, 25 Feb 2021 14:19:55 +0100 Subject: [PATCH] Faster version of the nominal NL* algorithm by specialising the observation table to Booleans --- .gitignore | 2 + bench/Bench.hs | 2 + nominal-lstar.cabal | 1 + src/Bollig.hs | 25 +++++++---- src/BooleanObservationTable.hs | 77 ++++++++++++++++++++++++++++++++++ src/ObservationTableClass.hs | 6 +-- src/SimpleObservationTable.hs | 19 ++++----- 7 files changed, 110 insertions(+), 22 deletions(-) create mode 100644 src/BooleanObservationTable.hs diff --git a/.gitignore b/.gitignore index 4394b95..07ae264 100644 --- a/.gitignore +++ b/.gitignore @@ -4,5 +4,7 @@ dist/ *.hi *.prof *.code-workspace +.stack-work +.vscode bench.csv diff --git a/bench/Bench.hs b/bench/Bench.hs index 444b34d..51e29ed 100644 --- a/bench/Bench.hs +++ b/bench/Bench.hs @@ -24,6 +24,7 @@ import NLambda Examples.example4 is not used, because it takes a bit too long. -} +myConfig :: Config myConfig = defaultConfig { quickMode = True , includeFirstIter = True @@ -36,6 +37,7 @@ stackBound = 4 doublewordBound = 3 nlastpositionBound = 4 +main :: IO () main = defaultMainWith myConfig [ bgroup "NomLStarR" [ bgroup "Fifo" $ diff --git a/nominal-lstar.cabal b/nominal-lstar.cabal index 777da0e..c3793c3 100644 --- a/nominal-lstar.cabal +++ b/nominal-lstar.cabal @@ -21,6 +21,7 @@ library AbstractLStar, Angluin, Bollig, + BooleanObservationTable, Examples, Examples.Contrived, Examples.ContrivedNFAs, diff --git a/src/Bollig.hs b/src/Bollig.hs index 53b4ef0..0384d4e 100644 --- a/src/Bollig.hs +++ b/src/Bollig.hs @@ -1,14 +1,17 @@ +{-# language FlexibleContexts #-} {-# language PartialTypeSignatures #-} +{-# language TypeFamilies #-} {-# OPTIONS_GHC -Wno-partial-type-signatures #-} module Bollig where import AbstractLStar +import qualified BooleanObservationTable as BOT import ObservationTableClass -import SimpleObservationTable +import qualified SimpleObservationTable as SOT import Teacher import Data.List (tails) -import Debug.Trace +import Debug.Trace (trace, traceShow) import NLambda hiding (alphabet) import Prelude (Bool (..), Int, Maybe (..), Show (..), snd, ($), (++), (.)) @@ -31,7 +34,7 @@ mqToBool teacher words = answer answer = map (setB True) inw `union` map (setB False) outw setB b (w, _) = (w, b) -rfsaClosednessTest :: NominalType i => Set (BRow i) -> BTable i -> TestResult i +rfsaClosednessTest :: (NominalType i, _) => Set (Row table) -> table -> TestResult i rfsaClosednessTest primesUpp t = case solve (isEmpty defect) of Just True -> Succes Just False -> trace "Not closed" $ Failed defect empty @@ -40,7 +43,7 @@ rfsaClosednessTest primesUpp t = case solve (isEmpty defect) of where defect = filter (\ua -> row t ua `neq` sum (filter (`isSubsetOf` row t ua) primesUpp)) (rowsExt t) -rfsaConsistencyTest :: NominalType i => BTable i -> TestResult i +rfsaConsistencyTest :: (NominalType i, _) => table -> TestResult i rfsaConsistencyTest t = case solve (isEmpty defect) of Just True -> Succes Just False -> trace "Not consistent" $ Failed empty defect @@ -51,7 +54,7 @@ rfsaConsistencyTest t = case solve (isEmpty defect) of defect = triplesWithFilter (\(u1, u2) a v -> maybeIf (not (tableAt2 (u1 ++ [a]) v) /\ tableAt2 (u2 ++ [a]) v) (a:v)) candidates (alph t) (cols t) tableAt2 s e = singleton True `eq` tableAt t s e -constructHypothesisBollig :: NominalType i => Set (BRow i) -> BTable i -> Automaton (BRow i) i +constructHypothesisBollig :: (NominalType i, _) => Set (Row table) -> table -> Automaton (Row table) i constructHypothesisBollig primesUpp t = automaton q (alph t) d i f where q = primesUpp @@ -63,16 +66,20 @@ constructHypothesisBollig primesUpp t = automaton q (alph t) d i f -- Adds all suffixes as columns -- TODO: do actual Rivest and Schapire -addCounterExample :: NominalType i => MQ i Bool -> Set [i] -> BTable i -> BTable i +addCounterExample :: (NominalType i, _) => MQ i Bool -> Set [i] -> table -> table addCounterExample mq ces t = let newColumns = sum . map (fromList . tails) $ ces newColumnsRed = newColumns \\ cols t in addColumns mq newColumnsRed t -learnBollig :: (NominalType i, _) => Int -> Int -> Teacher i -> Automaton (BRow i) i -learnBollig k n teacher = learnBolligLoop teacher (initialBTableSize (mqToBool teacher) (alphabet teacher) k n) +-- Slow version +learnBolligOld :: (NominalType i, _) => Int -> Int -> Teacher i -> Automaton (Row (SOT.BTable i)) i +learnBolligOld k n teacher = learnBolligLoop teacher (SOT.initialBTableSize (mqToBool teacher) (alphabet teacher) k n) -learnBolligLoop :: (NominalType i, _) => Teacher i -> BTable i -> Automaton (BRow i) i +learnBollig :: (NominalType i, _) => Int -> Int -> Teacher i -> Automaton (Row (BOT.Table i)) i +learnBollig k n teacher = learnBolligLoop teacher (BOT.initialBTableSize (mqToBool teacher) (alphabet teacher) k n) + +learnBolligLoop :: (NominalType i, _) => Teacher i -> table -> Automaton (Row table) i learnBolligLoop teacher t = let -- These simplify's do speed up diff --git a/src/BooleanObservationTable.hs b/src/BooleanObservationTable.hs new file mode 100644 index 0000000..378f5bd --- /dev/null +++ b/src/BooleanObservationTable.hs @@ -0,0 +1,77 @@ +{-# language DeriveAnyClass #-} +{-# language DeriveGeneric #-} +{-# language FlexibleInstances #-} +{-# language MultiParamTypeClasses #-} +{-# language RecordWildCards #-} +{-# language TypeFamilies #-} + +module BooleanObservationTable where + +import ObservationTableClass + +import GHC.Generics (Generic) +import NLambda +import Prelude (Bool (..), Eq, Int, Ord, Show (..), (++), (.)) +import qualified Prelude () + +-- Helper function +mqToSubset :: NominalType i => (Set [i] -> Set ([i], Bool)) -> Set [i] -> Set [i] +mqToSubset mq = mapFilter (\(i, o) -> maybeIf (fromBool o) i) . mq + +-- A table is nothing more than a part of the language. +-- Invariant: content is always a subset of +-- `rows * columns` union `rows * alph * columns`. +data Table i = Table + { content :: Set [i] + , rowIndices :: Set (RowIndex i) + , colIndices :: Set (ColumnIndex i) + , aa :: Set i + } + deriving (Show, Ord, Eq, Generic, NominalType, Conditional, Contextual) + +-- Currently, it may ask redundant membership queries +instance (NominalType i, Contextual i) => ObservationTable (Table i) i Bool where + type Row (Table i) = Set [i] + rows = rowIndices + cols = colIndices + alph = aa + row Table{..} r = filter (\e -> (r ++ e) `member` content) colIndices + rowEps Table{..} = intersection content colIndices + tableAt Table{..} r c = ite ((r ++ c) `member` content) (singleton True) (singleton False) + + addRows mq newRows t@Table{..} = + t { content = content `union` newContent + , rowIndices = rowIndices `union` newRows + } + where + newRowsExt = pairsWith (\r a -> r ++ [a]) newRows aa + newPart = pairsWith (++) (newRows `union` newRowsExt) colIndices + newContent = mqToSubset mq newPart + + addColumns mq newColumns t@Table{..} = + t { content = content `union` newContent + , colIndices = colIndices `union` newColumns + } + where + newColumnsExt = pairsWith (:) aa newColumns + newPart = pairsWith (++) rowIndices (newColumns `union` newColumnsExt) + newContent = mqToSubset mq newPart + + +initialBTableWith :: NominalType i => MQ i Bool -> Set i -> Set (RowIndex i) -> Set (ColumnIndex i) -> Table i +initialBTableWith mq alphabet newRows newColumns = Table + { content = content + , rowIndices = newRows + , colIndices = newColumns + , aa = alphabet + } + where + newColumnsExt = pairsWith (:) alphabet newColumns + domain = pairsWith (++) newRows (newColumns `union` newColumnsExt) + content = mqToSubset mq domain + +initialBTable :: NominalType i => MQ i Bool -> Set i -> Table i +initialBTable mq alphabet = initialBTableWith mq alphabet (singleton []) (singleton []) + +initialBTableSize :: NominalType i => MQ i Bool -> Set i -> Int -> Int -> Table i +initialBTableSize mq alphabet rs cs = initialBTableWith mq alphabet (replicateSetUntil rs alphabet) (replicateSetUntil cs alphabet) diff --git a/src/ObservationTableClass.hs b/src/ObservationTableClass.hs index 0b0b351..6212bd3 100644 --- a/src/ObservationTableClass.hs +++ b/src/ObservationTableClass.hs @@ -1,9 +1,9 @@ -{-# language TypeFamilies #-} {-# language FunctionalDependencies #-} +{-# language TypeFamilies #-} module ObservationTableClass where -import NLambda +import NLambda (NominalType, Set, pairsWith) import Prelude ((++)) -- Words are indices to our table @@ -23,7 +23,7 @@ class (NominalType table, NominalType i, NominalType o) => ObservationTable tabl cols :: table -> Set (ColumnIndex i) alph :: table -> Set i row :: table -> RowIndex i -> Row table - + -- perhaps not needed tableAt :: table -> RowIndex i -> ColumnIndex i -> Set o diff --git a/src/SimpleObservationTable.hs b/src/SimpleObservationTable.hs index 7bf5d70..4ad4854 100644 --- a/src/SimpleObservationTable.hs +++ b/src/SimpleObservationTable.hs @@ -1,22 +1,21 @@ {-# language DeriveAnyClass #-} {-# language DeriveGeneric #-} -{-# language RecordWildCards #-} {-# language FlexibleInstances #-} {-# language MultiParamTypeClasses #-} -{-# language TypeFamilies #-} {-# language PartialTypeSignatures #-} +{-# language RecordWildCards #-} +{-# language TypeFamilies #-} {-# OPTIONS_GHC -Wno-partial-type-signatures #-} module SimpleObservationTable where import ObservationTableClass -import NLambda hiding (fromJust) - -import GHC.Generics (Generic) -import Prelude (Bool (..), Eq, Int, Ord, Show (..), fst, (++), (.)) -import qualified Prelude () import Data.Coerce (coerce) +import GHC.Generics (Generic) +import NLambda +import Prelude (Bool (..), Eq, Int, Ord, Show (..), fst, (++)) +import qualified Prelude () -- We represent functions as their graphs @@ -30,10 +29,10 @@ dom = map fst -- Invariant: content is always defined for elements in -- `rows * columns` and `rows * alph * columns`. data Table i o = Table - { content :: Fun [i] o + { content :: Fun [i] o , rowIndices :: Set (RowIndex i) , colIndices :: Set (ColumnIndex i) - , aa :: Set i + , aa :: Set i } deriving (Show, Ord, Eq, Generic, NominalType, Conditional, Contextual) @@ -94,7 +93,7 @@ instance (NominalType i) => ObservationTable (BTable i) i Bool where row (B Table{..}) r = let lang = mapFilter (\(i, o) -> maybeIf (fromBool o) i) content in filter (\a -> lang `contains` (r ++ a)) colIndices rowEps (B Table{..}) = mapFilter (\(i, o) -> maybeIf (fromBool o /\ i `member` colIndices) i) content - + --addRows mq newRows = B . addRows mq newRows . unB addRows = coerce (addRows :: _ => _ -> _ -> Table i Bool -> Table i Bool) --addColumns mq newColumns = B . addColumns mq newColumns . unB