mirror of
https://github.com/Jaxan/nominal-lstar.git
synced 2025-04-27 06:37:45 +02:00
95 lines
3.7 KiB
Haskell
95 lines
3.7 KiB
Haskell
{-# language PartialTypeSignatures #-}
|
|
{-# 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.
|
|
-}
|
|
|
|
myConfig :: Config
|
|
myConfig = defaultConfig
|
|
{ quickMode = True
|
|
, includeFirstIter = True
|
|
, csvFile = Just "bench.csv"
|
|
}
|
|
|
|
-- Some bounds on the size of automata
|
|
fifoBound = 4
|
|
stackBound = 4
|
|
doublewordBound = 3
|
|
nlastpositionBound = 4
|
|
|
|
main :: IO ()
|
|
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
|