diff --git a/README.md b/README.md index 50edb59..79139cb 100644 --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ tell you what to do. (If you need any help, send me a message.) # Running Stack will produce a binary in the `.stack-works` directory, which can -be invoked directly. Alternatively one can run `stack exec NominalAngluin`. +be invoked directly. Alternatively one can run `stack exec nominal-lstar`. There is two modes of operation: Running the examples, or running it interactively. @@ -75,7 +75,7 @@ stack data structure): For example: ``` -stack exec NominalAngluin -- NomLStar EqDFA "Fifo 2" +stack exec nominal-lstar -- NomLStar EqDFA "Fifo 2" ``` The program will output all the intermediate hypotheses. And will terminate @@ -95,7 +95,7 @@ We proved by hand that the learnt model did indeed accept the language. Run the tool like so: ``` -stack exec NominalAngluin -- +stack exec nominal-lstar -- ``` (So similar to the above case, but without specifying the equivalence checker and example.) The tool will ask you membership queries and @@ -103,7 +103,7 @@ equivalence queries through the terminal. The alphabet is fixed in `Main.hs`, so change it if you need a different alphabet (it should work generically for any alphabet). -Additionally, one can run the `NominalAngluin2` executable instead, +Additionally, one can run the `nominal-lstar2` executable instead, if provides an easier to parse protocol for membership queries. Hence it is more suitable for automation. This will first ask for the alphabet which should be either `ATOMS` or `FIFO`. @@ -149,4 +149,5 @@ A: * Better support for interactive communication. * Optimisation: add only one row/column to fix closedness/consistency - +* Simpler observation table +* More efficient nominal NLStar diff --git a/app/Main.hs b/app/Main.hs index 5370666..322663b 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -2,10 +2,10 @@ import Angluin import Bollig import Examples -import ObservationTable +import ObservationTable (LearnableAlphabet) import Teacher -import NLambda +import NLambda hiding (automaton) import Prelude hiding (map) import System.Environment @@ -27,6 +27,7 @@ data Aut = Fifo Int | Stack Int | Running Int | NFA1 | Bollig Int | NonResidual -- existential wrapper data A = forall q i . (LearnableAlphabet i, Read i, NominalType q, Show q) => A (Automaton q i) +{- HLINT ignore "Redundant $" -} mainExample :: String -> String -> String -> IO () mainExample learnerName teacherName autName = do A automaton <- return $ case read autName of @@ -61,4 +62,20 @@ main = do case bla of [learnerName, teacherName, autName] -> mainExample learnerName teacherName autName [learnerName] -> mainWithIO learnerName - _ -> putStrLn "Give either 1 (for the IO teacher) or 3 (for automatic teacher) arguments" + _ -> help + +help :: IO () +help = do + putStrLn "Usage (for automated runs)" + putStrLn "" + putStrLn " nominal-lstar " + putStrLn "" + putStrLn "or (for manual runs)" + putStrLn "" + putStrLn " nominal-lstar " + putStrLn "" + putStrLn $ "where is any of " ++ show learners ++ ", is any of " ++ show teachers ++ ", and is any of " ++ show automata ++ ". (Replace 3 with any number you wish.)" + where + learners = [NomLStar, NomLStarCol, NomNLStar] + teachers = [EqDFA, EqNFA 3, EquivalenceIO] + automata = [Fifo 3, Stack 3, Running 3, NFA1, Bollig 3, NonResidual, Residual1, Residual2] diff --git a/app/Main2.hs b/app/Main2.hs index aafa5ec..1b95dae 100644 --- a/app/Main2.hs +++ b/app/Main2.hs @@ -7,6 +7,9 @@ import NLambda import System.Environment import System.IO +-- This Main2 file was used for automated benchmarking, and only accepts +-- a specific protocol. For normal usage, see Main.hs. + data Learner = NomLStar | NomLStarCol | NomNLStar deriving (Show, Read) diff --git a/nominal-lstar.cabal b/nominal-lstar.cabal index 6b317bf..ef99a39 100644 --- a/nominal-lstar.cabal +++ b/nominal-lstar.cabal @@ -38,14 +38,14 @@ library Teachers.Terminal, Teachers.Whitebox -executable NominalAngluin +executable nominal-lstar import: stuff hs-source-dirs: app main-is: Main.hs build-depends: nominal-lstar -executable NominalAngluin2 +executable nominal-lstar2 import: stuff hs-source-dirs: app main-is: Main2.hs diff --git a/run.sh b/run.sh index cf9a8dc..0665c86 100755 --- a/run.sh +++ b/run.sh @@ -4,7 +4,7 @@ # nominal-learning-ons repository mkfifo qs ans -time stack exec NominalAngluin2 NomLStarCol > qs < ans & +time stack exec nominal-lstar2 NomLStarCol > qs < ans & ../nominal-learning-orbitsets/external_teacher qs ans "$@" rm qs ans diff --git a/src/Angluin.hs b/src/Angluin.hs index 7cb098f..aec61ad 100644 --- a/src/Angluin.hs +++ b/src/Angluin.hs @@ -11,7 +11,7 @@ import NLambda import Prelude (Bool (..), Maybe (..), id, show, ($), (++), (.)) justOne :: (Contextual a, NominalType a) => Set a -> Set a -justOne s = mapFilter id . orbit [] . element $ s +justOne = mapFilter id . orbit [] . element -- We can determine its completeness with the following -- It returns all witnesses (of the form sa) for incompleteness @@ -39,14 +39,13 @@ consistencyTestDirect State{..} = case solve (isEmpty defect) of -- 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 a d i f +constructHypothesis State{..} = simplify $ automaton q aa d i f where q = map (row t) ss - a = aa 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 s = forAll id . map fromBool $ s + toform = forAll id . map fromBool -- Extends the table with all prefixes of a set of counter examples. useCounterExampleAngluin :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i diff --git a/src/Examples/Fifo.hs b/src/Examples/Fifo.hs index c815b33..a95d3f7 100644 --- a/src/Examples/Fifo.hs +++ b/src/Examples/Fifo.hs @@ -2,8 +2,9 @@ {-# language DeriveGeneric #-} module Examples.Fifo (DataInput(..), fifoExample) where +import NLambda hiding (states) + import GHC.Generics (Generic) -import NLambda import Prelude (Eq, Int, Maybe (..), Ord, Read, Show, length, reverse, ($), (+), (-), (.), (>=)) import qualified Prelude () diff --git a/src/Examples/RunningExample.hs b/src/Examples/RunningExample.hs index b05393b..e23b050 100644 --- a/src/Examples/RunningExample.hs +++ b/src/Examples/RunningExample.hs @@ -9,16 +9,14 @@ module Examples.RunningExample where but in terms of FO definable sets it is quite small. -} -import NLambda +import NLambda hiding (alphabet) --- Explicit Prelude, as NLambda has quite some clashes import Data.List (reverse) -import Prelude (Eq, Int, Ord, Show, ($), (-), (.)) +import GHC.Generics (Generic) +import Prelude (Eq, Int, Ord, Show, ($), (-)) import qualified Prelude () -import GHC.Generics (Generic) --- Parametric in the alphabet, because why not? data RunningExample a = Store [a] | Check [a] | Accept | Reject deriving (Eq, Ord, Show, Generic, NominalType, Contextual) @@ -35,10 +33,10 @@ runningExample alphabet depth = automaton `union` singleton Accept `union` singleton Reject) alphabet - (sums [pairsWith storeTrans alphabet (iwords i) | i <- [0..depth-2]] + (unions [pairsWith storeTrans alphabet (iwords i) | i <- [0..depth-2]] `union` pairsWith betweenTrans alphabet (iwords (depth-1)) - `union` sums [pairsWith checkGoodTrans alphabet (iwords i) | i <- [1..depth-1]] - `union` sums [triplesWithFilter checkBadTrans alphabet alphabet (iwords i) | i <- [1..depth-1]] + `union` unions [pairsWith checkGoodTrans alphabet (iwords i) | i <- [1..depth-1]] + `union` unions [triplesWithFilter checkBadTrans alphabet alphabet (iwords i) | i <- [1..depth-1]] `union` map (\a -> (Check [a], a, Accept)) alphabet `union` pairsWithFilter (\a b -> maybeIf (a `neq` b) (Check [a], b, Reject)) alphabet alphabet `union` map (Accept,, Reject) alphabet @@ -47,14 +45,11 @@ runningExample alphabet depth = automaton (singleton Accept) where -- these define the states - firstStates = sums [map Store $ iwords i | i <- [0..depth-1]] - secondStates = sums [map Check $ iwords i | i <- [1..depth]] + firstStates = unions [map Store $ iwords i | i <- [0..depth-1]] + secondStates = unions [map Check $ iwords i | i <- [1..depth]] iwords i = replicateSet i alphabet -- this is the general shape of an transition storeTrans a l = (Store l, a, Store (a:l)) betweenTrans a l = (Store l, a, Check (reverse (a:l))) checkGoodTrans a l = (Check (a:l), a, Check l) checkBadTrans a b l = maybeIf (a `neq` b) (Check (a:l), b, Reject) - -sums :: NominalType a => [Set a] -> Set a -sums = sum . fromList diff --git a/src/Examples/Stack.hs b/src/Examples/Stack.hs index 4a5418b..79751fd 100644 --- a/src/Examples/Stack.hs +++ b/src/Examples/Stack.hs @@ -2,9 +2,10 @@ {-# language DeriveGeneric #-} module Examples.Stack (DataInput(..), stackExample) where +import NLambda hiding (states) + import Examples.Fifo (DataInput (..)) import GHC.Generics (Generic) -import NLambda import Prelude (Eq, Int, Maybe (..), Ord, Show, length, ($), (.), (>=)) import qualified Prelude () diff --git a/src/Teachers/Whitebox.hs b/src/Teachers/Whitebox.hs index 27ab232..71946ac 100644 --- a/src/Teachers/Whitebox.hs +++ b/src/Teachers/Whitebox.hs @@ -2,81 +2,70 @@ module Teachers.Whitebox where import NLambda -import Control.Monad.Identity import Prelude hiding (filter, map, not, sum) --- I found it a bit easier to write a do-block below. So I needed this --- Conditional instance. -instance Conditional a => Conditional (Identity a) where - cond f x y = return (cond f (runIdentity x) (runIdentity y)) - -- Checks bisimulation of initial states (only for DFAs) --- returns some counter examples if not bisimilar +-- returns some counterexamples if not bisimilar -- returns empty set iff bisimilar bisim :: (NominalType i, NominalType q1, NominalType q2) => Automaton q1 i -> Automaton q2 i -> Set [i] -bisim aut1 aut2 = runIdentity $ go empty (pairsWith addEmptyWord (initialStates aut1) (initialStates aut2)) +bisim aut1 aut2 = go empty (pairsWith addEmptyWord (initialStates aut1) (initialStates aut2)) where - go rel todo = do - -- if elements are already in R, we can skip them - let todo2 = filter (\(_, x, y) -> (x, y) `notMember` rel) todo - -- split into correct pairs and wrong pairs - let (cont, ces) = partition (\(_, x, y) -> (x `member` finalStates aut1) <==> (y `member` finalStates aut2)) todo2 - let aa = NLambda.alphabet aut1 - -- the good pairs should make one step - let dtodo = sum (pairsWith (\(w, x, y) a -> pairsWith (\x2 y2 -> (a:w, x2, y2)) (d aut1 a x) (d aut2 a y)) cont aa) - -- if there are wrong pairs - ite (isNotEmpty ces) - -- then return counter examples - (return $ map getRevWord ces) - -- else continue with good pairs - (ite (isEmpty dtodo) - (return empty) - (go (rel `union` map stripWord cont) dtodo) - ) + go rel todo = + let -- if elements are already in R, we can skip them + todo2 = filter (\(_, x, y) -> (x, y) `notMember` rel) todo + -- split into correct pairs and wrong pairs + (cont, ces) = partition (\(_, x, y) -> (x `member` finalStates aut1) <==> (y `member` finalStates aut2)) todo2 + aa = NLambda.alphabet aut1 + -- the good pairs should make one step + dtodo = sum (pairsWith (\(w, x, y) a -> pairsWith (\x2 y2 -> (a:w, x2, y2)) (d aut1 a x) (d aut2 a y)) cont aa) + in -- if there are wrong pairs + ite (isNotEmpty ces) + -- then return counter examples + (map getRevWord ces) + -- else continue with good pairs + (ite (isEmpty dtodo) empty (go (rel `union` map stripWord cont) dtodo)) d aut a x = mapFilter (\(s, l, t) -> maybeIf (s `eq` x /\ l `eq` a) t) (delta aut) stripWord (_, x, y) = (x, y) getRevWord (w, _, _) = reverse w addEmptyWord x y = ([], x, y) --- Attempt at using a bisimlution up to to proof bisimulation between NFAs --- Because why not? Inspired by the Hacking non-determinism paper --- But they only consider finite sums (which is enough for finite sets) --- Here I have to do a bit of trickery, which is hopefully correct. --- I think it is correct, but not yet complete enough, we need more up-to. +-- Attempt at using a bisimlution up to to proof bisimulation between NFAs. +-- Inspired by the Hacking non-determinism paper. However, they only +-- consider finite sums (which is enough for finite sets, but not for +-- nominal sets). Here, I have to do a bit of trickery to get all sums. +-- I am not sure about correctness, but that is not really an issue for our +-- use-case. Note that deciding equivalence of NFAs is undecidable, so we +-- bound the bisimulation depth. bisimNonDet :: (Show i, Show q1, Show q2, NominalType i, NominalType q1, NominalType q2) => Int -> Automaton q1 i -> Automaton q2 i -> Set [i] -bisimNonDet n aut1 aut2 = runIdentity $ go empty (singleton ([], initialStates aut1, initialStates aut2)) +bisimNonDet n aut1 aut2 = go empty (singleton ([], initialStates aut1, initialStates aut2)) where - go rel todo0 = do - -- if elements are too long, we ignore them - let todo0b = filter (\(w,_,_) -> fromBool (length w <= n)) todo0 - -- if elements are already in R, we can skip them - let todo1 = filter (\(_, x, y) -> (x, y) `notMember` rel) todo0b - -- now we are going to do a up-to thingy - -- we look at all subsets x2 of x occuring in R (similarly for y) - let xbar x = mapFilter (\(x2, _) -> maybeIf (x2 `isSubsetOf` x) x2) rel - let ybar y = mapFilter (\(_, y2) -> maybeIf (y2 `isSubsetOf` y) y2) rel - -- and then the sums are expressed by these formulea kind of - let xform x y = x `eq` sum (xbar x) /\ forAll (\x2 -> exists (\y2 -> rel `contains` (x2, y2)) (ybar y)) (xbar x) - let yform x y = y `eq` sum (ybar y) /\ forAll (\y2 -> exists (\x2 -> rel `contains` (x2, y2)) (xbar x)) (ybar y) - let notSums x y = not (xform x y /\ yform x y) - -- filter out things expressed as sums - let todo2 = filter (\(_, x, y) -> notSums x y) todo1 - -- split into correct pairs and wrong pairs - let (cont, ces) = partition (\(_, x, y) -> (x `intersect` finalStates aut1) <==> (y `intersect` finalStates aut2)) todo2 - let aa = NLambda.alphabet aut1 - -- the good pairs should make one step - let dtodo = pairsWith (\(w, x, y) a -> (a:w, sumMap (d aut1 a) x, sumMap (d aut2 a) y)) cont aa - -- if there are wrong pairs - --trace "go" $ traceShow rel $ traceShow todo0 $ traceShow todo1 $ traceShow todo2 $ traceShow cont $ - ite (isNotEmpty ces) - -- then return counter examples - (return $ map getRevWord ces) - -- else continue with good pairs - (ite (isEmpty dtodo) - (return empty) - (go (rel `union` map stripWord cont) dtodo) - ) + go rel todo0 = + let -- if elements are too long, we ignore them + todo0b = filter (\(w,_,_) -> fromBool (length w <= n)) todo0 + -- if elements are already in R, we can skip them + todo1 = filter (\(_, x, y) -> (x, y) `notMember` rel) todo0b + -- now we are going to do a up-to thingy + -- we look at all subsets x2 of x occuring in R (similarly for y) + xbar x = mapFilter (\(x2, _) -> maybeIf (x2 `isSubsetOf` x) x2) rel + ybar y = mapFilter (\(_, y2) -> maybeIf (y2 `isSubsetOf` y) y2) rel + -- and then the sums are expressed by these formulea kind of + xform x y = x `eq` sum (xbar x) /\ forAll (\x2 -> exists (\y2 -> rel `contains` (x2, y2)) (ybar y)) (xbar x) + yform x y = y `eq` sum (ybar y) /\ forAll (\y2 -> exists (\x2 -> rel `contains` (x2, y2)) (xbar x)) (ybar y) + notSums x y = not (xform x y /\ yform x y) + -- filter out things expressed as sums + todo2 = filter (\(_, x, y) -> notSums x y) todo1 + -- split into correct pairs and wrong pairs + (cont, ces) = partition (\(_, x, y) -> (x `intersect` finalStates aut1) <==> (y `intersect` finalStates aut2)) todo2 + aa = NLambda.alphabet aut1 + -- the good pairs should make one step + dtodo = pairsWith (\(w, x, y) a -> (a:w, sumMap (d aut1 a) x, sumMap (d aut2 a) y)) cont aa + in -- if there are wrong pairs + ite (isNotEmpty ces) + -- then return counter examples + (map getRevWord ces) + -- else continue with good pairs + (ite (isEmpty dtodo) empty (go (rel `union` map stripWord cont) dtodo)) d aut a x = mapFilter (\(s, l, t) -> maybeIf (s `eq` x /\ l `eq` a) t) (delta aut) stripWord (_, x, y) = (x, y) getRevWord (w, _, _) = reverse w