diff --git a/app/Main.hs b/app/Main.hs index 322663b..86f7466 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -2,7 +2,6 @@ import Angluin import Bollig import Examples -import ObservationTable (LearnableAlphabet) import Teacher import NLambda hiding (automaton) @@ -25,7 +24,7 @@ data Aut = Fifo Int | Stack Int | Running Int | NFA1 | Bollig Int | NonResidual deriving (Show, Read) -- existential wrapper -data A = forall q i . (LearnableAlphabet i, Read i, NominalType q, Show q) => A (Automaton q i) +data A = forall q i . (NominalType i, Contextual i, Show i, Read i, NominalType q, Show q) => A (Automaton q i) {- HLINT ignore "Redundant $" -} mainExample :: String -> String -> String -> IO () diff --git a/nominal-lstar.cabal b/nominal-lstar.cabal index c3793c3..26a7751 100644 --- a/nominal-lstar.cabal +++ b/nominal-lstar.cabal @@ -30,7 +30,6 @@ library Examples.Residual, Examples.RunningExample, Examples.Stack, - ObservationTable, ObservationTableClass, SimpleObservationTable, Teacher, diff --git a/src/AbstractLStar.hs b/src/AbstractLStar.hs index 6f230a9..07b9bc4 100644 --- a/src/AbstractLStar.hs +++ b/src/AbstractLStar.hs @@ -1,79 +1,7 @@ -{-# language RecordWildCards #-} module AbstractLStar where -import ObservationTable -import Teacher - -import Debug.Trace import NLambda -type TableCompletionHandler i = Teacher i -> State i -> State i -type CounterExampleHandler i = Teacher i -> State i -> Set [i] -> State i -type HypothesisConstruction i hq = State i -> Automaton hq i - data TestResult i = Succes -- test succeeded, no changes required | Failed (Set [i]) (Set [i]) -- test failed, change: add rows + columns - --- Simple loop which performs tests such as closedness and consistency --- on the table and makes changes if needed. Will (hopefully) reach a --- fixed point, i.e. a complete table. -makeCompleteWith :: LearnableAlphabet i - => [State i -> TestResult i] - -> Teacher i -> State i -> State i -makeCompleteWith tests teacher state0 = go tests state0 - where - -- All tests succeeded, then the state is stable - go [] state = state - -- We still have tests to perform - go (t:ts) state = case t state of - -- If the test succeeded, we continue with the next one - Succes -> go ts state - -- Otherwise we add the changes - Failed newRows newColumns -> - let state2 = simplify $ addRows teacher newRows state in - let state3 = simplify $ addColumns teacher newColumns state2 in - -- restart the whole business - makeCompleteWith tests teacher state3 - --- Simple general learning loop: 1. make the table complete 2. construct --- hypothesis 3. ask teacher. Repeat until done. If the teacher is adequate --- termination implies correctness. -learn :: (NominalType hq, Show hq, LearnableAlphabet i) - => TableCompletionHandler i - -> CounterExampleHandler i - -> HypothesisConstruction i hq - -> Teacher i - -> State i - -> Automaton hq i -learn makeComplete handleCounterExample constructHypothesis teacher s = - trace "##################" $ - trace "1. Making it complete and consistent" $ - let s2 = makeComplete teacher s in - trace "2. Constructing hypothesis" $ - let h = constructHypothesis s2 in - traceShow h $ - trace "3. Equivalent? " $ - eqloop s2 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 = handleCounterExample teacher s2 ces in - learn makeComplete handleCounterExample constructHypothesis teacher s3 - realces h ces = NLambda.filter (\(ce, a) -> a `neq` accepts h ce) $ membership teacher ces - --- Initialise with the trivial table --- We allow to initialise with all words of length <= k,n for rows and columns --- Normally one should take k = n = 0 -constructEmptyState :: LearnableAlphabet i => Int -> Int -> Teacher i -> State i -constructEmptyState k n teacher = - let aa = Teacher.alphabet teacher in - let ss = replicateSetUntil k aa in - let ssa = pairsWith (\s a -> s ++ [a]) ss aa in - let ee = replicateSetUntil n aa in - let t = fillTable teacher (ss `union` ssa) ee in - State{..} diff --git a/src/Angluin.hs b/src/Angluin.hs index 3231448..f12186f 100644 --- a/src/Angluin.hs +++ b/src/Angluin.hs @@ -1,112 +1,107 @@ -{-# language RecordWildCards #-} +{-# language FlexibleContexts #-} +{-# language PartialTypeSignatures #-} +{-# language TypeFamilies #-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} module Angluin where import AbstractLStar -import ObservationTable +import ObservationTableClass +import qualified BooleanObservationTable as OT import Teacher import Data.List (inits, tails) import Debug.Trace -import NLambda -import Prelude (Bool (..), Maybe (..), id, show, ($), (++), (.)) +import NLambda hiding (alphabet) +import Prelude (Bool (..), Maybe (..), error, show, ($), (++), (.)) --- This was actually a pessimisation (often), also it sometimes crashes. --- So I changed it to a no-op. -justOne :: (Contextual a, NominalType a) => Set a -> Set a -justOne = id -- mapFilter id . orbit [] . element --- We can determine its completeness with the following --- It returns all witnesses (of the form sa) for incompleteness -closednessTest :: LearnableAlphabet i => State i -> TestResult i -closednessTest State{..} = case solve (isEmpty defect) of +-- This returns all witnesses (of the form sa) for non-closedness +closednessTest :: (NominalType i, _) => table -> TestResult i +closednessTest t = case solve (isEmpty defect) of Just True -> Succes - Just False -> trace "Not closed" $ Failed (justOne defect) empty + Just False -> trace "Not closed" $ Failed defect empty + Nothing -> let err = error "@@@ Unsolvable (closednessTest) @@@" in Failed err err where - sss = map (row t) ss -- all the rows - hasEqRow = contains sss . row t -- has equivalent upper row - defect = filter (not . hasEqRow) ssa -- all rows without equivalent guy + allRows = map (row t) (rows t) + hasEqRow = contains allRows . row t + defect = filter (not . hasEqRow) (rowsExt t) -- We look for inconsistencies and return columns witnessing it -consistencyTestDirect :: LearnableAlphabet i => State i -> TestResult i -consistencyTestDirect State{..} = case solve (isEmpty defect) of +consistencyTestDirect :: (NominalType i, _) => table -> TestResult i +consistencyTestDirect t = case solve (isEmpty defect) of Just True -> Succes - Just False -> trace "Not consistent" $ Failed empty (justOne defect) + Just False -> trace "Not consistent" $ Failed empty defect + Nothing -> let err = error "@@@ Unsolvable (consistencyTestDirect) @@@" in Failed err err where - ssRows = map (\u -> (u, row t u)) ss + ssRows = map (\u -> (u, row t u)) (rows t) candidates = pairsWithFilter (\(u1,r1) (u2,r2) -> maybeIf (u1 `neq` u2 /\ r1 `eq` r2) (u1, u2)) ssRows ssRows - defect = triplesWithFilter (\(u1, u2) a v -> maybeIf (tableAt t (u1 ++ [a]) v `diff` tableAt t (u2 ++ [a]) v) (a:v)) candidates aa ee - diff a b = not (a `iff` b) - + defect = triplesWithFilter (\(u1, u2) a v -> maybeIf (tableAt t (u1 ++ [a]) v `neq` tableAt t (u2 ++ [a]) v) (a:v)) candidates (alph t) (cols t) -- Given a C&C table, constructs an automaton. The states are given by 2^E (not -- necessarily equivariant functions) -constructHypothesis :: LearnableAlphabet i => State i -> Automaton (BRow i) i -constructHypothesis State{..} = simplify $ automaton q aa d i f +constructHypothesis :: (NominalType i, _) => table -> Automaton (Row table) i +constructHypothesis t = simplify $ automaton q (alph t) d i f where - q = map (row t) ss - d = pairsWith (\s a -> (row t s, a, rowa t s a)) ss aa - i = singleton $ row t [] - f = mapFilter (\s -> maybeIf (toform $ apply t (s, [])) (row t s)) ss - toform = forAll id . map fromBool + q = map (row t) (rows t) + d = pairsWith (\s a -> (row t s, a, row t (s ++ [a]))) (rows t) (alph t) + i = singleton (rowEps t) + f = filter (`contains` []) q -- Extends the table with all prefixes of a set of counter examples. -useCounterExampleAngluin :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i -useCounterExampleAngluin teacher state@State{..} ces = - trace ("Using ce: " ++ show ces) $ - let ds = sum . map (fromList . inits) $ ces in - addRows teacher ds state +useCounterExampleAngluin :: (NominalType i, _) => Teacher i -> Set [i] -> table -> table +useCounterExampleAngluin teacher ces t = + let newRows = sum . map (fromList . inits) $ ces + newRowsRed = newRows \\ rows t + in addRows (mqToBool teacher) newRowsRed t --- This is the variant by Maler and Pnueli -useCounterExampleMP :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i -useCounterExampleMP teacher state@State{..} ces = - trace ("Using ce: " ++ show ces) $ - let de = sum . map (fromList . tails) $ ces in - addColumns teacher de state - --- Putting the above together in a learning algorithm -makeCompleteAngluin :: LearnableAlphabet i => TableCompletionHandler i -makeCompleteAngluin = makeCompleteWith [closednessTest, consistencyTestDirect] +-- This is the variant by Maler and Pnueli: Adds all suffixes as columns +useCounterExampleMP :: (NominalType i, _) => Teacher i -> Set [i] -> table -> table +useCounterExampleMP teacher ces t = + let newColumns = sum . map (fromList . tails) $ ces + newColumnsRed = newColumns \\ cols t + in addColumns (mqToBool teacher) newColumnsRed t -- Default: use counter examples in columns, which is slightly faster -learnAngluin :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i -learnAngluin teacher = learn makeCompleteAngluin useCounterExampleMP constructHypothesis teacher initial - where initial = constructEmptyState 0 0 teacher +learnAngluin :: (NominalType i, _) => Teacher i -> Automaton _ i +learnAngluin teacher = learnLoop useCounterExampleMP teacher (OT.initialBTable (mqToBool teacher) (alphabet teacher)) -- The "classical" version, where counter examples are added as rows -learnAngluinRows :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i -learnAngluinRows teacher = learn makeCompleteAngluin useCounterExampleAngluin constructHypothesis teacher initial - where initial = constructEmptyState 0 0 teacher +learnAngluinRows :: (NominalType i, _) => Teacher i -> Automaton _ i +learnAngluinRows teacher = learnLoop useCounterExampleAngluin teacher (OT.initialBTable (mqToBool teacher) (alphabet teacher)) - --- Below are some variations of the above functions with different --- performance characteristics. - --- Some coauthor's slower version -consistencyTest2 :: NominalType i => State i -> TestResult i -consistencyTest2 State{..} = case solve (isEmpty defect) of - Just True -> Succes - Just False -> trace "Not consistent" $ Failed empty columns - where - -- true for equal rows, but unequal extensions - -- we can safely skip equal sequences - candidate s1 s2 a = s1 `neq` s2 - /\ row t s1 `eq` row t s2 - /\ rowa t s1 a `neq` rowa t s2 a - defect = triplesWithFilter ( - \s1 s2 a -> maybeIf (candidate s1 s2 a) ((s1, s2, a), discrepancy (rowa t s1 a) (rowa t s2 a)) - ) ss ss aa - columns = sum $ map (\((_,_,a),es) -> map (a:) es) defect - --- Some coauthor's faster version -consistencyTest3 :: NominalType i => State i -> TestResult i -consistencyTest3 State{..} = case solve (isEmpty defect) of - Just True -> Succes - Just False -> trace "Not consistent" $ Failed empty columns - where - rowPairs = pairsWithFilter (\s1 s2 -> maybeIf (candidate0 s1 s2) (s1,s2)) ss ss - candidate0 s1 s2 = s1 `neq` s2 /\ row t s1 `eq` row t s2 - candidate1 s1 s2 a = rowa t s1 a `neq` rowa t s2 a - defect = pairsWithFilter ( - \(s1, s2) a -> maybeIf (candidate1 s1 s2 a) ((s1, s2, a), discrepancy (rowa t s1 a) (rowa t s2 a)) - ) rowPairs aa - columns = sum $ map (\((_,_,a),es) -> map (a:) es) defect +learnLoop :: (NominalType i, ObservationTable table i Bool, _) => _ -> Teacher i -> table -> Automaton (Row table) i +learnLoop cexHandler teacher t = + let + -- No worry, these are computed lazily + closednessRes = closednessTest t + consistencyRes = consistencyTestDirect t + hyp = constructHypothesis t + in + trace "1. Making it closed" $ + case closednessRes of + Failed newRows _ -> + let state2 = addRows (mqToBool teacher) newRows t in + trace ("newrows = " ++ show newRows) $ + learnLoop cexHandler teacher state2 + Succes -> + trace "2. Making it consistent" $ + case consistencyRes of + Failed _ newColumns -> + let state2 = addColumns (mqToBool teacher) newColumns t in + trace ("newcols = " ++ show newColumns) $ + learnLoop cexHandler teacher state2 + Succes -> + traceShow hyp $ + trace "3. Equivalent? " $ + eqloop t hyp + 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 = cexHandler teacher ces s2 in + trace ("Using ce: " ++ show ces) $ + learnLoop cexHandler teacher s3 + realces h ces = NLambda.filter (\(ce, a) -> a `neq` accepts h ce) $ membership teacher ces diff --git a/src/Bollig.hs b/src/Bollig.hs index 0384d4e..7dcc22b 100644 --- a/src/Bollig.hs +++ b/src/Bollig.hs @@ -13,7 +13,7 @@ import Teacher import Data.List (tails) import Debug.Trace (trace, traceShow) import NLambda hiding (alphabet) -import Prelude (Bool (..), Int, Maybe (..), Show (..), snd, ($), (++), (.)) +import Prelude (Bool (..), Int, Maybe (..), Show (..), ($), (++), (.)) -- Comparing two graphs of a function is inefficient in NLambda, -- because we do not have a map data structure. (So the only way @@ -23,17 +23,6 @@ import Prelude (Bool (..), Int, Maybe (..), Show (..), snd, ($), (++), (.)) -- This does hinder generalisations to other nominal join semi- -- lattices than the Booleans. --- The teacher interface is slightly inconvenient --- But this is for a good reason. The type [i] -> o --- doesn't work well in nlambda -mqToBool :: NominalType i => Teacher i -> MQ i Bool -mqToBool teacher words = answer - where - realQ = membership teacher words - (inw, outw) = partition snd realQ - answer = map (setB True) inw `union` map (setB False) outw - setB b (w, _) = (w, b) - rfsaClosednessTest :: (NominalType i, _) => Set (Row table) -> table -> TestResult i rfsaClosednessTest primesUpp t = case solve (isEmpty defect) of Just True -> Succes @@ -72,13 +61,13 @@ addCounterExample mq ces t = newColumnsRed = newColumns \\ cols t in addColumns mq newColumnsRed t --- 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) - -learnBollig :: (NominalType i, _) => Int -> Int -> Teacher i -> Automaton (Row (BOT.Table i)) i +learnBollig :: (NominalType i, _) => Int -> Int -> Teacher i -> Automaton _ i learnBollig k n teacher = learnBolligLoop teacher (BOT.initialBTableSize (mqToBool teacher) (alphabet teacher) k n) +-- Slow version +learnBolligOld :: (NominalType i, _) => Int -> Int -> Teacher i -> Automaton _ i +learnBolligOld k n teacher = learnBolligLoop teacher (SOT.initialBTableSize (mqToBool teacher) (alphabet teacher) k n) + learnBolligLoop :: (NominalType i, _) => Teacher i -> table -> Automaton (Row table) i learnBolligLoop teacher t = let diff --git a/src/ObservationTable.hs b/src/ObservationTable.hs deleted file mode 100644 index 00eaba2..0000000 --- a/src/ObservationTable.hs +++ /dev/null @@ -1,109 +0,0 @@ -{-# language ConstraintKinds #-} -{-# language DeriveAnyClass #-} -{-# language DeriveGeneric #-} -{-# language FlexibleContexts #-} -{-# language FlexibleInstances #-} -{-# language RecordWildCards #-} - -module ObservationTable where - -import NLambda hiding (fromJust) -import Teacher - -import Data.Maybe (fromJust) -import Debug.Trace (trace) -import GHC.Generics (Generic) -import Prelude (Bool (..), Eq, Ord, Show (..), id, uncurry, ($), (++), (.)) -import qualified Prelude () - - --- We represent functions as their graphs -type Fun a b = Set (a, b) - --- Basic manipulations on functions --- Note that this returns a set, rather than an element --- because we cannot extract a value from a singleton set -apply :: (NominalType a, NominalType b) => Fun a b -> a -> Set b -apply f a1 = mapFilter (\(a2, b) -> maybeIf (eq a1 a2) b) f - --- Returns the subset (of the domain) which exhibits --- different return values for the two functions -discrepancy :: (NominalType a, NominalType b) => Fun a b -> Fun a b -> Set a -discrepancy f1 f2 = - pairsWithFilter ( - \(a1,b1) (a2,b2) -> maybeIf (eq a1 a2 /\ neq b1 b2) a1 - ) f1 f2 - - --- An observation table is a function S x E -> O --- (Also includes SA x E -> O) -type Table i o = Fun ([i], [i]) o -type Row i o = Fun [i] o - --- This is a rather arbitrary set of constraints --- But I use them *everywhere*, so let's define them once and for all. -type LearnableAlphabet i = (Contextual i, NominalType i, Show i) - --- `row is` denotes the data of a single row --- that is, the function E -> O -row :: (NominalType i, NominalType o) => Table i o -> [i] -> Fun [i] o -row t is = mapFilter (\((a,b),c) -> maybeIf (eq is a) (b,c)) t - --- `rowa is a` is the row for the one letter extensions -rowa :: (NominalType i, NominalType o) => Table i o -> [i] -> i -> Fun [i] o -rowa t is a = row t (is ++ [a]) - -tableAt :: NominalType i => Table i Bool -> [i] -> [i] -> Formula -tableAt t s e = singleton True `eq` mapFilter (\((a,b),c) -> maybeIf (s `eq` a /\ b `eq` e) c) t - --- Teacher is restricted to Bools at the moment -type BTable i = Table i Bool -type BRow i = Row i Bool - --- fills part of the table. First parameter is the rows (with extension), --- second is columns. Although the teacher provides us formulas instead of --- booleans, we can partition the answers to obtain actual booleans. -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 - base0 = pairsWith (++) 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) - --- Data structure representing the state of the learning algorithm (NOT a --- state in the automaton) -data State i = State - { t :: BTable i -- the table - , ss :: Set [i] -- state sequences - , ssa :: Set [i] -- their one letter extensions - , ee :: Set [i] -- suffixes - , aa :: Set i -- alphabet (remains constant) - } - deriving (Show, Ord, Eq, Generic, NominalType, Conditional, Contextual) - --- Precondition: the set together with the current rows is prefix closed -addRows :: LearnableAlphabet i => Teacher i -> Set [i] -> State i -> State i -addRows teacher ds0 state@State{..} = - trace ("add rows: " ++ show ds) $ - state {t = t `union` dt, ss = ss `union` ds, ssa = ssa `union` dsa} - where - -- first remove redundancy - ds = ds0 \\ ss - -- extensions of new rows - dsa = pairsWith (\s a -> s ++ [a]) ds aa - -- For the new rows, we fill the table - -- note that `ds ee` is already filled - dt = fillTable teacher dsa ee - -addColumns :: LearnableAlphabet i => Teacher i -> Set [i] -> State i -> State i -addColumns teacher de0 state@State{..} = - trace ("add columns: " ++ show de) $ - state {t = t `union` dt, ee = ee `union` de} - where - -- first remove redundancy - de = de0 \\ ee - -- Fill that part of the table - dt = fillTable teacher (ss `union` ssa) de diff --git a/src/Teacher.hs b/src/Teacher.hs index 41c5adb..8b5a79d 100644 --- a/src/Teacher.hs +++ b/src/Teacher.hs @@ -3,6 +3,7 @@ module Teacher ( module Teachers.Teacher + , mqToBool , teacherWithTarget , teacherWithTargetNonDet , teacherWithIO @@ -16,6 +17,20 @@ import Teachers.Whitebox import NLambda hiding (alphabet) import qualified NLambda (alphabet) +import Prelude hiding (map) + + +-- The teacher interface is slightly inconvenient +-- But this is for a good reason. The type [i] -> o +-- doesn't work well in nlambda +mqToBool :: NominalType i => Teacher i -> Set [i] -> Set ([i], Bool) +mqToBool teacher qs = answer + where + realQ = membership teacher qs + (inw, outw) = partition snd realQ + answer = map (setB True) inw `union` map (setB False) outw + setB b (w, _) = (w, b) + -- We provide three ways to construct teachers: -- 1. Fully automatic