From f24ed31ac894fd28870c68ef2d8ce4b2dd10be8d Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Thu, 23 Jun 2016 14:50:30 +0200 Subject: [PATCH] Implemented NL* by Bollig et al (verbatim) --- src/AbstractLStar.hs | 81 ++++++++++++++++++++++++++++++++++++++++ src/Bollig.hs | 83 +++++++++++++++++++++++++++++++++++++++++ src/Main.hs | 5 +++ src/ObservationTable.hs | 15 ++++++-- 4 files changed, 180 insertions(+), 4 deletions(-) create mode 100644 src/AbstractLStar.hs create mode 100644 src/Bollig.hs diff --git a/src/AbstractLStar.hs b/src/AbstractLStar.hs new file mode 100644 index 0000000..b563238 --- /dev/null +++ b/src/AbstractLStar.hs @@ -0,0 +1,81 @@ +{-# LANGUAGE RecordWildCards #-} +module AbstractLStar where + +import ObservationTable +import Teacher + +import Control.DeepSeq (deepseq) +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 = State i -> Automaton (BRow i) 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 = addRows teacher newRows state in + let state3 = 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 :: LearnableAlphabet i + => TableCompletionHandler i + -> CounterExampleHandler i + -> HypothesisConstruction i + -> Teacher i + -> State i + -> Automaton (BRow i) i +learn makeComplete handleCounterExample constructHypothesis teacher s = + deepseq s $ -- This helps ordering the traces somewhat. + 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? " $ + let eq = equivalent teacher h in + traceShow eq $ + case eq of + Nothing -> h + Just ce -> do + let s3 = handleCounterExample teacher s2 ce + learn makeComplete handleCounterExample constructHypothesis teacher s3 + +-- Initial state is always the same in our case +constructEmptyState :: LearnableAlphabet i => Teacher i -> State i +constructEmptyState teacher = + let aa = Teacher.alphabet teacher in + let ss = singleton [] in + let ssa = pairsWith (\s a -> s ++ [a]) ss aa in + let ee = singleton [] in + let t = fillTable teacher (ss `union` ssa) ee in + State{..} + +--loopClassicalAngluin = loop makeCompleteConsistent useCounterExampleAngluin constructHypothesis +--loopClassicalMP = loop makeCompleteConsistent useCounterExampleRS constructHypothesis +--loopNonDet = loop makeCompleteConsistentNonDet useCounterExampleRS constructHypothesisNonDet + +--learn loop teacher = loop teacher (constructEmptyState teacher) diff --git a/src/Bollig.hs b/src/Bollig.hs new file mode 100644 index 0000000..730656c --- /dev/null +++ b/src/Bollig.hs @@ -0,0 +1,83 @@ +{-# LANGUAGE RecordWildCards #-} +module Bollig where + +import AbstractLStar +import ObservationTable +import Teacher + +import Data.List (tails) +import Debug.Trace +import NLambda +import qualified Prelude hiding () +import Prelude (Bool(..), Maybe(..), ($), (.), (++), fst, show) + +-- See also NLStar.hs for this hack +hackApproximate :: NominalType a => Set a -> Set (Set a) +hackApproximate set = empty + `union` map singleton set + `union` pairsWith (\x y -> singleton x `union` singleton y) set set + `union` triplesWith (\x y z -> singleton x `union` singleton y `union` singleton z) set set set + +rowUnion :: NominalType i => Set (BRow i) -> BRow i +rowUnion set = Prelude.uncurry union . setTrueFalse . partition (\(_, f) -> f) $ map (\is -> (is, exists fromBool (mapFilter (\(is2, b) -> maybeIf (is `eq` is2) b) flatSet))) allIs + where + flatSet = sum set + allIs = map fst flatSet + setTrueFalse (trueSet, falseSet) = (map (setSecond True) trueSet, map (setSecond False) falseSet) + setSecond a (x, _) = (x, a) + +primes :: NominalType a => (Set a -> a) -> Set a -> Set a +primes alg rows = filter (\r -> r `notMember` sumsWithout r) rows + where + sumsWithout r = map alg $ hackApproximate (rows \\ singleton r) + +boolImplies :: Bool -> Bool -> Bool +boolImplies True False = False +boolImplies _ _ = True + +sublang :: NominalType i => BRow i -> BRow i -> Formula +sublang r1 r2 = forAll fromBool $ pairsWithFilter (\(i1, f1) (i2, f2) -> maybeIf (i1 `eq` i2) (f1 `boolImplies` f2)) r1 r2 + +rfsaClosednessTest :: LearnableAlphabet i => State i -> TestResult i +rfsaClosednessTest 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 = pairsWithFilter (\u a -> maybeIf (rowa t u a `member` primesDifference) (u ++ [a])) ss aa + primesDifference = primes rowUnion (map (row t) $ ss `union` ssa) \\ map (row t) ss + +rfsaConsistencyTest :: LearnableAlphabet i => State i -> TestResult i +rfsaConsistencyTest State{..} = case solve (isEmpty defect) of + Just True -> Succes + Just False -> trace "Not consistent" $ Failed empty defect + Nothing -> trace "@@@ Unsolved Formula (rfsaConsistencyTest) @@@" $ + Failed empty defect + where + candidates = pairsWithFilter (\u1 u2 -> maybeIf (row t u1 `sublang` row t u2) (u1, u2)) ss ss + defect = triplesWithFilter (\(u1, u2) a v -> maybeIf (not (tableAt t (u1 ++ [a]) v) /\ tableAt t (u2++[a]) v) (a:v)) candidates aa ee + +constructHypothesisBollig :: NominalType i => State i -> Automaton (BRow i) i +constructHypothesisBollig State{..} = automaton q a d i f + where + q = primes rowUnion (map (row t) ss) + a = aa + i = filter (\r -> r `sublang` row t []) q + f = filter (\r -> singleton True `eq` mapFilter (\(i,b) -> maybeIf (i `eq` []) b) r) q + d0 = triplesWithFilter (\s a s2 -> maybeIf (row t s2 `sublang` rowa t s a) (row t s, a, row t s2)) ss aa ss + d = filter (\(q1,a,q2) -> q1 `member` q /\ q2 `member` q) d0 + +-- Copied from the classical DFA-algorithm, column version +useCECopy :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i +useCECopy teacher state@State{..} ces = + trace ("Using ce:" ++ show ces) $ + let de = sum . map (fromList . tails) $ ces in + addColumns teacher de state + +makeCompleteBollig :: LearnableAlphabet i => TableCompletionHandler i +makeCompleteBollig = makeCompleteWith [rfsaClosednessTest, rfsaConsistencyTest] + +learnBollig :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i +learnBollig teacher = learn makeCompleteBollig useCECopy constructHypothesisBollig teacher initial + where initial = constructEmptyState teacher diff --git a/src/Main.hs b/src/Main.hs index 77fdd53..388eb4a 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -1,5 +1,6 @@ {-# LANGUAGE RecordWildCards #-} +import Bollig import Examples import Functions import ObservationTable @@ -8,6 +9,7 @@ import NLStar import NLambda +import Control.DeepSeq import Data.List (inits, tails) import Debug.Trace import Prelude hiding (and, curry, filter, lookup, map, not, @@ -124,6 +126,9 @@ useCounterExample = useCounterExampleRS -- exactly accepts the language we are learning. loop :: LearnableAlphabet i => Teacher i -> State i -> Automaton (BRow i) i loop teacher s = + -- I put a deepseq here in order to let all traces be evaluated + -- in a decent order. Also it will be used anyways. + deepseq s $ trace "##################" $ trace "1. Making it complete and consistent" $ let s2 = makeCompleteConsistent teacher s in diff --git a/src/ObservationTable.hs b/src/ObservationTable.hs index 24b4560..c01cc1f 100644 --- a/src/ObservationTable.hs +++ b/src/ObservationTable.hs @@ -13,8 +13,9 @@ import Teacher 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) import qualified Prelude () @@ -36,6 +37,9 @@ row t is = mapFilter (\((a,b),c) -> maybeIf (eq is a) (b,c)) t 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 @@ -68,7 +72,9 @@ instance NominalType i => Conditional (State i) where -- 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{..} = state {t = t `union` dt, ss = ss `union` ds, ssa = ssa `union` dsa} +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 @@ -78,9 +84,10 @@ addRows teacher ds0 state@State{..} = state {t = t `union` dt, ss = ss `union` d -- 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{..} = state {t = t `union` dt, ee = ee `union` de} +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