Made a decent automated benchmark

.gitignore

@@ -3,4 +3,6 @@ dist/
 *.o
 *.hi
 *.prof
+*.code-workspace
+bench.csv
 

bench/Bench.hs

@@ -1,23 +1,93 @@
-{-# OPTIONS_GHC -Wno-missing-signatures #-}
+{-# language PartialTypeSignatures #-}
-import Bollig
+{-# OPTIONS_GHC -Wno-missing-signatures -Wno-partial-type-signatures #-}
+import Angluin (learnAngluin, learnAngluinRows)
+import Bollig (learnBollig)
 import Examples
 import Teacher
 
 import Gauge.Main
 import Gauge.Main.Options
+import NLambda
+
+{- Benchmarks can be run with `stack bench`. If you would like to run a
+   subset of benchmarks, you can do this with `stack bench --ba NomNLStar`
+   for example. May take a long time (so we only run once).
+
+   Note that we are using the whitebox equivalence checks, which may not
+   reflect "realistic" runtinme, because the representation of the
+   counterexamples is different.
+
+   The nondeterministic benchmarks are a bit subtle, because equivalence
+   is not decidable. We do a bounded bisimulation check, the bounds are
+   guessed to be sufficient, but not proven to be.
+
+   Examples.example4 is not used, because it takes a bit too long.
+-}
 
--- Run a single test since these are slow benchmarks
 myConfig = defaultConfig
   { quickMode = True
   , includeFirstIter = True
   , csvFile = Just "bench.csv"
   }
 
-main = defaultMainWith myConfig [
+-- Some bounds on the size of automata
-  bgroup "NomNLStar"
+fifoBound = 4
-    [ bench "NFA1    " $ whnf (learnBollig 0 0) (teacherWithTargetNonDet 2 Examples.exampleNFA1)
+stackBound = 4
-    , bench "NFA2 1  " $ whnf (learnBollig 0 0) (teacherWithTargetNonDet 3 (Examples.exampleNFA2 1))
+doublewordBound = 3
-    , bench "NFA2 2  " $ whnf (learnBollig 0 0) (teacherWithTargetNonDet 4 (Examples.exampleNFA2 2))
+nlastpositionBound = 4
-    , bench "Residual" $ whnf (learnBollig 1 0) (teacherWithTargetNonDet 2 Examples.exampleResidual1)
+
+main = defaultMainWith myConfig
+  [ bgroup "NomLStarR"
+    [ bgroup "Fifo" $
+      fmap (\n -> bench (show n) $ whnf lstar (target (fifoExample n))) [0..fifoBound]
+    , bgroup "Stack" $
+      fmap (\n -> bench (show n) $ whnf lstar (target (stackExample n))) [0..stackBound]
+    , bgroup "Double Word" $
+      fmap (\n -> bench (show n) $ whnf lstar (target (runningExample atoms n))) [0..doublewordBound]
+    , bgroup "n-last Position" $
+      fmap (\n -> bench (show n) $ whnf lstar (targetNonDet (n+2) (exampleNFA2 n))) [0..nlastpositionBound]
+    , bench "example1" $ whnf lstar (target example1)
+    , bench "example2" $ whnf lstar (target example2)
+    , bench "example3" $ whnf lstar (target example3)
+    --, bench "example4" $ whnf lstar (target example4)
+    , bench "example5" $ whnf lstar (target example5)
+    ]
+  , bgroup "NomLStarC"
+    [ bgroup "Fifo" $
+      fmap (\n -> bench (show n) $ whnf lstarCol (target (fifoExample n))) [0..fifoBound]
+    , bgroup "Stack" $
+      fmap (\n -> bench (show n) $ whnf lstarCol (target (stackExample n))) [0..stackBound]
+    , bgroup "Double Word" $
+      fmap (\n -> bench (show n) $ whnf lstarCol (target (runningExample atoms n))) [0..doublewordBound]
+    , bgroup "n-last Position" $
+      fmap (\n -> bench (show n) $ whnf lstarCol (targetNonDet (n+2) (exampleNFA2 n))) [0..nlastpositionBound]
+    , bench "example1" $ whnf lstarCol (target example1)
+    , bench "example2" $ whnf lstarCol (target example2)
+    , bench "example3" $ whnf lstarCol (target example3)
+    --, bench "example4" $ whnf lstarCol (target example4)
+    , bench "example5" $ whnf lstarCol (target example5)
+    ]
+  , bgroup "NomNLStar"
+    [ bgroup "n-last Position" $
+      fmap (\n -> bench (show n) $ whnf nlstar (targetNonDet (n+2) (exampleNFA2 n))) [0..nlastpositionBound]
+    , bench "example1" $ whnf nlstar (targetNonDet 3 example1)
+    , bench "example2" $ whnf nlstar (targetNonDet 2 example2)
+    , bench "example3" $ whnf nlstar (targetNonDet 2 example3)
+    --, bench "example4" $ whnf nlstar (targetNonDet 4 example4)
+    , bench "example5" $ whnf nlstar (targetNonDet 3 example5)
+    , bench "NFA1    " $ whnf nlstar (targetNonDet 2 exampleNFA1)
+    , bench "Residual" $ whnf nlstar (targetNonDet 2 exampleResidual1)
     ]
   ]
+
+-- Some (polymorphic) abbreviations
+lstar, lstarCol, nlstar :: _ => Teacher i -> Automaton _ i
+lstar = learnAngluinRows
+lstarCol = learnAngluin
+nlstar = learnBollig 0 0
+
+target :: _ => Automaton q i -> Teacher i
+target = teacherWithTarget
+
+targetNonDet :: _ => Int -> Automaton q i -> Teacher i
+targetNonDet = teacherWithTargetNonDet

nominal-lstar.cabal

@@ -60,3 +60,12 @@ benchmark bench
   build-depends:
     gauge,
     nominal-lstar
+
+test-suite test
+  import: stuff
+  hs-source-dirs: test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  build-depends:
+    gauge,
+    nominal-lstar

src/Angluin.hs

@@ -10,8 +10,10 @@ import Debug.Trace
 import NLambda
 import Prelude (Bool (..), Maybe (..), id, 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 = mapFilter id . orbit [] . element
+justOne = id -- mapFilter id . orbit [] . element
 
 -- We can determine its completeness with the following
 -- It returns all witnesses (of the form sa) for incompleteness

test/Spec.hs

@@ -0,0 +1,27 @@
+{-# language PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-missing-signatures -Wno-partial-type-signatures #-}
+import Angluin (learnAngluin)
+import Examples
+import Teacher
+
+import Gauge.Main
+import Gauge.Main.Options
+import NLambda
+
+{- TODO: choose test framework -}
+
+myConfig = defaultConfig
+  { quickMode = True
+  , includeFirstIter = True
+  , csvFile = Just "test.csv"
+  }
+
+main = defaultMainWith myConfig
+  [ bench "DW2" $ whnf lstarCol (target (runningExample atoms 2)) ]
+
+-- Some (polymorphic) abbreviations
+lstarCol :: _ => Teacher i -> Automaton _ i
+lstarCol = learnAngluin
+
+target :: _ => Automaton q i -> Teacher i
+target = teacherWithTarget