From 8d54c1a55382a911a60b27d41603c370b65ec659 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Thu, 30 Jun 2016 11:44:25 +0200 Subject: [PATCH] Adds better support for counter membership queries VERY EXPERIMENTAL AND SLOW --- src/ObservationTable.hs | 7 ++++-- src/Teacher.hs | 54 ++++++++++++++++++++--------------------- 2 files changed, 32 insertions(+), 29 deletions(-) diff --git a/src/ObservationTable.hs b/src/ObservationTable.hs index 517da0f..24e0b3b 100644 --- a/src/ObservationTable.hs +++ b/src/ObservationTable.hs @@ -14,7 +14,7 @@ import Control.DeepSeq (NFData, force) import Data.Maybe (fromJust) import Debug.Trace (trace) import GHC.Generics (Generic) -import Prelude (Bool (..), Eq, Ord, Show (..), ($), (++), (.), uncurry) +import Prelude (Bool (..), Eq, Ord, Show (..), ($), (++), (.), uncurry, id) import qualified Prelude () @@ -68,7 +68,10 @@ type BRow i = Row i Bool fillTable :: LearnableAlphabet i => Teacher i -> Set [i] -> Set [i] -> BTable i fillTable teacher sssa ee = Prelude.uncurry union . map2 (map slv) . map2 simplify . partition (\(_, _, f) -> f) $ base where - base = pairsWith (\s e -> (s, e, membership teacher (s++e))) sssa ee + base0 = pairsWith (\s e -> (s++e)) sssa ee + base1 = membership teacher base0 + base1b s e = forAll id $ mapFilter (\(i,f) -> maybeIf (i `eq` (s++e)) f) base1 + base = pairsWith (\s e -> (s, e, base1b s e)) sssa ee map2 f (a, b) = (f a, f b) slv (a,b,f) = ((a,b), fromJust . solve $ f) diff --git a/src/Teacher.hs b/src/Teacher.hs index 39a4f6e..1b51833 100644 --- a/src/Teacher.hs +++ b/src/Teacher.hs @@ -19,7 +19,6 @@ import Control.Monad.Identity (Identity(..)) import Control.Monad (when) import Data.IORef (IORef, readIORef, newIORef, writeIORef) import System.IO.Unsafe (unsafePerformIO) -import qualified Data.Set as Set -- Used in the IO teacher import System.Console.Haskeline @@ -31,7 +30,7 @@ import Text.Read (readMaybe) data Teacher i = Teacher -- Given a sequence, check whether it is in the language -- Assumed to be equivariant - { membership :: [i] -> Formula + { membership :: Set [i] -> Set ([i], Formula) -- Given a hypothesis, returns Nothing when equivalence or a (equivariant) -- set of counter examples. Needs to be quantified over q, because the -- learner may choose the type of the state space. @@ -40,6 +39,13 @@ data Teacher i = Teacher , alphabet :: Set i } +-- In order to count membership queries, I had to have the set of inputs +-- instead of just mere inputs... It's a bit annoying, since it doesn't +-- look like Angluin like this... But this is the best I can do in NLambda +-- Here is a function to make it element-wise again: +foreachQuery :: NominalType i => ([i] -> Formula) -> Set[i] -> Set ([i], Formula) +foreachQuery f qs = map (\q -> (q, f q)) qs + -- We provide three ways to construct teachers: -- 1. Fully automatic -- 2. Fully interactive (via IO) @@ -49,7 +55,7 @@ data Teacher i = Teacher -- Only works for DFAs for now, as those can be checked for equivalence teacherWithTarget :: (NominalType i, NominalType q) => Automaton q i -> Teacher i teacherWithTarget aut = Teacher - { membership = automaticMembership aut + { membership = foreachQuery $ automaticMembership aut , equivalent = automaticEquivalent bisim aut , alphabet = automaticAlphabet aut } @@ -58,7 +64,7 @@ teacherWithTarget aut = Teacher -- Might work for NFAs, not really tested teacherWithTargetNonDet :: (Show i, Show q, NominalType i, NominalType q) => Int -> Automaton q i -> Teacher i teacherWithTargetNonDet n aut = Teacher - { membership = automaticMembership aut + { membership = foreachQuery $ automaticMembership aut , equivalent = automaticEquivalent (bisimNonDet n) aut , alphabet = automaticAlphabet aut } @@ -70,7 +76,7 @@ teacherWithTargetNonDet n aut = Teacher -- consider the whole orbit generated by it. teacherWithIO :: Teacher Atom teacherWithIO = Teacher - { membership = ioMembership + { membership = foreachQuery ioMembership , equivalent = ioEquivalent , alphabet = atoms } @@ -79,7 +85,7 @@ teacherWithIO = Teacher -- Useful as long as you don't have an equivalence check, For example for G-NFAs teacherWithTargetAndIO :: NominalType q => Automaton q Atom -> Teacher Atom teacherWithTargetAndIO aut = Teacher - { membership = automaticMembership aut + { membership = foreachQuery $ automaticMembership aut , equivalent = ioEquivalent , alphabet = atoms } @@ -88,7 +94,7 @@ teacherWithTargetAndIO aut = Teacher -- Useful for debugging and so on, but *very very hacky*! countingTeacher :: (Show i, NominalType i) => Teacher i -> Teacher i countingTeacher delegate = Teacher - { membership = \q -> increaseMQ q `seq` membership delegate q + { membership = \qs -> increaseMQ qs `seq` membership delegate qs , equivalent = \a -> increaseEQ a `seq` equivalent delegate a , alphabet = alphabet delegate } @@ -101,32 +107,26 @@ countingTeacher delegate = Teacher return j {-# NOINLINE increaseMQ #-} increaseMQ q = unsafePerformIO $ do - -- new <- notInCache q - -- when new $ do - l <- readIORef mqCounter - let len = length q - let sup = length $ leastSupport q - let l2 = (len, sup) : l - writeIORef mqCounter l2 - -- {-# NOINLINE cache #-} - -- cache = unsafePerformIO $ newIORef Set.empty - -- {-# NOINLINE notInCache #-} - -- notInCache q = do - -- oldCache <- readIORef cache - -- case q `Set.member` oldCache of - -- True -> return False - -- False -> do - -- let newCache = Set.insert q oldCache - -- writeIORef cache newCache - -- return True + new <- newOrbitsInCache q + l <- readIORef mqCounter + let l2 = fromVariant new : l + writeIORef mqCounter l2 + {-# NOINLINE cache #-} + cache = unsafePerformIO $ newIORef empty + {-# NOINLINE newOrbitsInCache #-} + newOrbitsInCache qs = do + oldCache <- readIORef cache + let newQs = qs \\ oldCache + writeIORef cache (oldCache `union` qs) + return $ setOrbitsNumber newQs -- HACK: Counts number of equivalence queries eqCounter :: IORef Int {-# NOINLINE eqCounter #-} eqCounter = unsafePerformIO $ newIORef 0 --- HACK: Keeps track of membership queries with: length, size of support -mqCounter :: IORef [(Int, Int)] +-- HACK: Keeps track of membership queries with: # orbits per 'query' +mqCounter :: IORef [Int] {-# NOINLINE mqCounter #-} mqCounter = unsafePerformIO $ newIORef []